diff options
Diffstat (limited to 'theories/Bool/Bool.v')
| -rw-r--r-- | theories/Bool/Bool.v | 308 |
1 files changed, 162 insertions, 146 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index ff87eb96..e126ad35 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Bool.v 8642 2006-03-17 10:09:02Z notin $ i*) - -(** ** Booleans *) +(*i $Id: Bool.v 9246 2006-10-17 14:01:18Z herbelin $ i*) (** The type [bool] is defined in the prelude as [Inductive bool : Set := true : bool | false : bool] *) @@ -16,34 +14,34 @@ (** Interpretation of booleans as propositions *) Definition Is_true (b:bool) := match b with - | true => True - | false => False + | true => True + | false => False end. -(*****************) -(** Decidability *) -(*****************) +(*******************) +(** * Decidability *) +(*******************) Lemma bool_dec : forall b1 b2 : bool, {b1 = b2} + {b1 <> b2}. Proof. decide equality. Defined. -(*******************) -(** Discrimination *) -(*******************) +(*********************) +(** * Discrimination *) +(*********************) Lemma diff_true_false : true <> false. Proof. -unfold not in |- *; intro contr; change (Is_true false) in |- *. -elim contr; simpl in |- *; trivial. + unfold not in |- *; intro contr; change (Is_true false) in |- *. + elim contr; simpl in |- *; trivial. Qed. Hint Resolve diff_true_false : bool v62. Lemma diff_false_true : false <> true. Proof. -red in |- *; intros H; apply diff_true_false. -symmetry in |- *. + red in |- *; intros H; apply diff_true_false. + symmetry in |- *. assumption. Qed. Hint Resolve diff_false_true : bool v62. @@ -51,92 +49,92 @@ Hint Extern 1 (false <> true) => exact diff_false_true. Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False. Proof. -intros b H; rewrite H; auto with bool. + intros b H; rewrite H; auto with bool. Qed. Lemma not_true_is_false : forall b:bool, b <> true -> b = false. Proof. -destruct b. -intros. -red in H; elim H. -reflexivity. -intros abs. -reflexivity. + destruct b. + intros. + red in H; elim H. + reflexivity. + intros abs. + reflexivity. Qed. Lemma not_false_is_true : forall b:bool, b <> false -> b = true. Proof. -destruct b. -intros. -reflexivity. -intro H; red in H; elim H. -reflexivity. + destruct b. + intros. + reflexivity. + intro H; red in H; elim H. + reflexivity. Qed. (**********************) -(** Order on booleans *) +(** * Order on booleans *) (**********************) Definition leb (b1 b2:bool) := match b1 with - | true => b2 = true - | false => True + | true => b2 = true + | false => True end. Hint Unfold leb: bool v62. (* Infix "<=" := leb : bool_scope. *) (*************) -(** Equality *) +(** * Equality *) (*************) Definition eqb (b1 b2:bool) : bool := match b1, b2 with - | true, true => true - | true, false => false - | false, true => false - | false, false => true + | true, true => true + | true, false => false + | false, true => false + | false, false => true end. Lemma eqb_subst : - forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2. -Proof. -unfold eqb in |- *. -intros P b1. -intros b2. -case b1. -case b2. -trivial with bool. -intros H. -inversion_clear H. -case b2. -intros H. -inversion_clear H. -trivial with bool. + forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2. +Proof. + unfold eqb in |- *. + intros P b1. + intros b2. + case b1. + case b2. + trivial with bool. + intros H. + inversion_clear H. + case b2. + intros H. + inversion_clear H. + trivial with bool. Qed. Lemma eqb_reflx : forall b:bool, eqb b b = true. Proof. -intro b. -case b. -trivial with bool. -trivial with bool. + intro b. + case b. + trivial with bool. + trivial with bool. Qed. Lemma eqb_prop : forall a b:bool, eqb a b = true -> a = b. Proof. -destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity. + destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity. Qed. (************************) -(** Logical combinators *) +(** * Logical combinators *) (************************) Definition ifb (b1 b2 b3:bool) : bool := match b1 with - | true => b2 - | false => b3 + | true => b2 + | false => b3 end. Definition andb (b1 b2:bool) : bool := ifb b1 b2 false. @@ -147,10 +145,10 @@ Definition implb (b1 b2:bool) : bool := ifb b1 b2 true. Definition xorb (b1 b2:bool) : bool := match b1, b2 with - | true, true => false - | true, false => true - | false, true => true - | false, false => false + | true, true => false + | true, false => true + | false, true => true + | false, false => false end. Definition negb (b:bool) := if b then false else true. @@ -165,7 +163,7 @@ Delimit Scope bool_scope with bool. Bind Scope bool_scope with bool. (****************************) -(** De Morgan laws *) +(** * De Morgan laws *) (****************************) Lemma negb_orb : forall b1 b2:bool, negb (b1 || b2) = negb b1 && negb b2. @@ -179,17 +177,17 @@ Proof. Qed. (********************************) -(** *** Properties of [negb] *) +(** * Properties of [negb] *) (********************************) Lemma negb_involutive : forall b:bool, negb (negb b) = b. Proof. -destruct b; reflexivity. + destruct b; reflexivity. Qed. Lemma negb_involutive_reverse : forall b:bool, b = negb (negb b). Proof. -destruct b; reflexivity. + destruct b; reflexivity. Qed. Notation negb_elim := negb_involutive (only parsing). @@ -197,68 +195,68 @@ Notation negb_intro := negb_involutive_reverse (only parsing). Lemma negb_sym : forall b b':bool, b' = negb b -> b = negb b'. Proof. -destruct b; destruct b'; intros; simpl in |- *; trivial with bool. + destruct b; destruct b'; intros; simpl in |- *; trivial with bool. Qed. Lemma no_fixpoint_negb : forall b:bool, negb b <> b. Proof. -destruct b; simpl in |- *; intro; apply diff_true_false; - auto with bool. + destruct b; simpl in |- *; intro; apply diff_true_false; + auto with bool. Qed. Lemma eqb_negb1 : forall b:bool, eqb (negb b) b = false. Proof. -destruct b. -trivial with bool. -trivial with bool. + destruct b. + trivial with bool. + trivial with bool. Qed. Lemma eqb_negb2 : forall b:bool, eqb b (negb b) = false. Proof. -destruct b. -trivial with bool. -trivial with bool. + destruct b. + trivial with bool. + trivial with bool. Qed. Lemma if_negb : - forall (A:Set) (b:bool) (x y:A), - (if negb b then x else y) = (if b then y else x). + forall (A:Set) (b:bool) (x y:A), + (if negb b then x else y) = (if b then y else x). Proof. destruct b; trivial. Qed. (********************************) -(** *** Properties of [orb] *) +(** * Properties of [orb] *) (********************************) Lemma orb_true_elim : forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}. Proof. -destruct b1; simpl in |- *; auto with bool. + destruct b1; simpl in |- *; auto with bool. Defined. Lemma orb_prop : forall a b:bool, a || b = true -> a = true \/ b = true. Proof. -destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); - auto with bool. + destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); + auto with bool. Qed. Lemma orb_true_intro : - forall b1 b2:bool, b1 = true \/ b2 = true -> b1 || b2 = true. + forall b1 b2:bool, b1 = true \/ b2 = true -> b1 || b2 = true. Proof. -destruct b1; auto with bool. -destruct 1; intros. -elim diff_true_false; auto with bool. -rewrite H; trivial with bool. + destruct b1; auto with bool. + destruct 1; intros. + elim diff_true_false; auto with bool. + rewrite H; trivial with bool. Qed. Hint Resolve orb_true_intro: bool v62. Lemma orb_false_intro : - forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false. + forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false. Proof. -intros b1 b2 H1 H2; rewrite H1; rewrite H2; trivial with bool. + intros b1 b2 H1 H2; rewrite H1; rewrite H2; trivial with bool. Qed. Hint Resolve orb_false_intro: bool v62. @@ -266,13 +264,13 @@ Hint Resolve orb_false_intro: bool v62. Lemma orb_true_r : forall b:bool, b || true = true. Proof. -auto with bool. + auto with bool. Qed. Hint Resolve orb_true_r: bool v62. Lemma orb_true_l : forall b:bool, true || b = true. Proof. -trivial with bool. + trivial with bool. Qed. Notation orb_b_true := orb_true_r (only parsing). @@ -296,7 +294,7 @@ Notation orb_b_false := orb_false_r (only parsing). Notation orb_false_b := orb_false_l (only parsing). Lemma orb_false_elim : - forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false. + forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false. Proof. destruct b1. intros; elim diff_true_false; auto with bool. @@ -319,7 +317,7 @@ Notation orb_neg_b := orb_negb_r (only parsing). Lemma orb_comm : forall b1 b2:bool, b1 || b2 = b2 || b1. Proof. -destruct b1; destruct b2; reflexivity. + destruct b1; destruct b2; reflexivity. Qed. (** Associativity *) @@ -330,14 +328,14 @@ Proof. Qed. Hint Resolve orb_comm orb_assoc: bool v62. -(*********************************) -(** *** Properties of [andb] *) -(*********************************) +(*******************************) +(** * Properties of [andb] *) +(*******************************) Lemma andb_prop : forall a b:bool, a && b = true -> a = true /\ b = true. Proof. destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); - auto with bool. + auto with bool. Qed. Hint Resolve andb_prop: bool v62. @@ -348,7 +346,7 @@ Proof. Defined. Lemma andb_true_intro : - forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true. + forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true. Proof. destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. Qed. @@ -356,24 +354,24 @@ Hint Resolve andb_true_intro: bool v62. Lemma andb_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false. Proof. -destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. + destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. Qed. Lemma andb_false_intro2 : forall b1 b2:bool, b2 = false -> b1 && b2 = false. Proof. -destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. + destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. Qed. (** [false] is a zero for [andb] *) Lemma andb_false_r : forall b:bool, b && false = false. Proof. -destruct b; auto with bool. + destruct b; auto with bool. Qed. Lemma andb_false_l : forall b:bool, false && b = false. Proof. -trivial with bool. + trivial with bool. Qed. Notation andb_b_false := andb_false_r (only parsing). @@ -383,12 +381,12 @@ Notation andb_false_b := andb_false_l (only parsing). Lemma andb_true_r : forall b:bool, b && true = b. Proof. -destruct b; auto with bool. + destruct b; auto with bool. Qed. Lemma andb_true_l : forall b:bool, true && b = b. Proof. -trivial with bool. + trivial with bool. Qed. Notation andb_b_true := andb_true_r (only parsing). @@ -397,7 +395,7 @@ Notation andb_true_b := andb_true_l (only parsing). Lemma andb_false_elim : forall b1 b2:bool, b1 && b2 = false -> {b1 = false} + {b2 = false}. Proof. -destruct b1; simpl in |- *; auto with bool. + destruct b1; simpl in |- *; auto with bool. Defined. Hint Resolve andb_false_elim: bool v62. @@ -405,7 +403,7 @@ Hint Resolve andb_false_elim: bool v62. Lemma andb_negb_r : forall b:bool, b && negb b = false. Proof. -destruct b; reflexivity. + destruct b; reflexivity. Qed. Hint Resolve andb_negb_r: bool v62. @@ -415,46 +413,46 @@ Notation andb_neg_b := andb_negb_r (only parsing). Lemma andb_comm : forall b1 b2:bool, b1 && b2 = b2 && b1. Proof. -destruct b1; destruct b2; reflexivity. + destruct b1; destruct b2; reflexivity. Qed. (** Associativity *) Lemma andb_assoc : forall b1 b2 b3:bool, b1 && (b2 && b3) = b1 && b2 && b3. Proof. -destruct b1; destruct b2; destruct b3; reflexivity. + destruct b1; destruct b2; destruct b3; reflexivity. Qed. Hint Resolve andb_comm andb_assoc: bool v62. (*******************************************) -(** *** Properties mixing [andb] and [orb] *) +(** * Properties mixing [andb] and [orb] *) (*******************************************) (** Distributivity *) Lemma andb_orb_distrib_r : - forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3. + forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3. Proof. -destruct b1; destruct b2; destruct b3; reflexivity. + destruct b1; destruct b2; destruct b3; reflexivity. Qed. Lemma andb_orb_distrib_l : forall b1 b2 b3:bool, (b1 || b2) && b3 = b1 && b3 || b2 && b3. Proof. -destruct b1; destruct b2; destruct b3; reflexivity. + destruct b1; destruct b2; destruct b3; reflexivity. Qed. Lemma orb_andb_distrib_r : - forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3). + forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3). Proof. -destruct b1; destruct b2; destruct b3; reflexivity. + destruct b1; destruct b2; destruct b3; reflexivity. Qed. Lemma orb_andb_distrib_l : - forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3). + forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3). Proof. -destruct b1; destruct b2; destruct b3; reflexivity. + destruct b1; destruct b2; destruct b3; reflexivity. Qed. (* Compatibility *) @@ -475,46 +473,64 @@ Proof. destruct b1; destruct b2; simpl in |- *; reflexivity. Qed. -(***********************************) -(** *** Properties of [xorb] *) -(***********************************) +(*********************************) +(** * Properties of [xorb] *) +(*********************************) -Lemma xorb_false : forall b:bool, xorb b false = b. +(** [false] is neutral for [xorb] *) + +Lemma xorb_false_r : forall b:bool, xorb b false = b. Proof. destruct b; trivial. Qed. -Lemma false_xorb : forall b:bool, xorb false b = b. +Lemma xorb_false_l : forall b:bool, xorb false b = b. Proof. destruct b; trivial. Qed. -Lemma xorb_true : forall b:bool, xorb b true = negb b. +Notation xorb_false := xorb_false_r (only parsing). +Notation false_xorb := xorb_false_l (only parsing). + +(** [true] is "complementing" for [xorb] *) + +Lemma xorb_true_r : forall b:bool, xorb b true = negb b. Proof. trivial. Qed. -Lemma true_xorb : forall b:bool, xorb true b = negb b. +Lemma xorb_true_l : forall b:bool, xorb true b = negb b. Proof. destruct b; trivial. Qed. +Notation xorb_true := xorb_true_r (only parsing). +Notation true_xorb := xorb_true_l (only parsing). + +(** Nilpotency (alternatively: identity is a inverse for [xorb]) *) + Lemma xorb_nilpotent : forall b:bool, xorb b b = false. Proof. destruct b; trivial. Qed. +(** Commutativity *) + Lemma xorb_comm : forall b b':bool, xorb b b' = xorb b' b. Proof. destruct b; destruct b'; trivial. Qed. -Lemma xorb_assoc : - forall b b' b'':bool, xorb (xorb b b') b'' = xorb b (xorb b' b''). +(** Associativity *) + +Lemma xorb_assoc_reverse : + forall b b' b'':bool, xorb (xorb b b') b'' = xorb b (xorb b' b''). Proof. destruct b; destruct b'; destruct b''; trivial. Qed. +Notation xorb_assoc := xorb_assoc_reverse (only parsing). (* Compatibility *) + Lemma xorb_eq : forall b b':bool, xorb b b' = false -> b = b'. Proof. destruct b; destruct b'; trivial. @@ -522,26 +538,26 @@ Proof. Qed. Lemma xorb_move_l_r_1 : - forall b b' b'':bool, xorb b b' = b'' -> b' = xorb b b''. + forall b b' b'':bool, xorb b b' = b'' -> b' = xorb b b''. Proof. intros. rewrite <- (false_xorb b'). rewrite <- (xorb_nilpotent b). rewrite xorb_assoc. rewrite H. reflexivity. Qed. Lemma xorb_move_l_r_2 : - forall b b' b'':bool, xorb b b' = b'' -> b = xorb b'' b'. + forall b b' b'':bool, xorb b b' = b'' -> b = xorb b'' b'. Proof. intros. rewrite xorb_comm in H. rewrite (xorb_move_l_r_1 b' b b'' H). apply xorb_comm. Qed. Lemma xorb_move_r_l_1 : - forall b b' b'':bool, b = xorb b' b'' -> xorb b' b = b''. + forall b b' b'':bool, b = xorb b' b'' -> xorb b' b = b''. Proof. intros. rewrite H. rewrite <- xorb_assoc. rewrite xorb_nilpotent. apply false_xorb. Qed. Lemma xorb_move_r_l_2 : - forall b b' b'':bool, b = xorb b' b'' -> xorb b b'' = b'. + forall b b' b'':bool, b = xorb b' b'' -> xorb b b'' = b'. Proof. intros. rewrite H. rewrite xorb_assoc. rewrite xorb_nilpotent. apply xorb_false. Qed. @@ -550,24 +566,24 @@ Qed. Lemma eq_true_iff_eq : forall b1 b2, (b1 = true <-> b2 = true) -> b1 = b2. Proof. - intros b1 b2; case b1; case b2; intuition. + intros b1 b2; case b1; case b2; intuition. Qed. -Notation bool_1 := eq_true_iff_eq. (* Compatibility *) +Notation bool_1 := eq_true_iff_eq (only parsing). (* Compatibility *) Lemma eq_true_negb_classical : forall b:bool, negb b <> true -> b = true. Proof. destruct b; intuition. Qed. -Notation bool_3 := eq_true_negb_classical. (* Compatibility *) +Notation bool_3 := eq_true_negb_classical (only parsing). (* Compatibility *) Lemma eq_true_not_negb : forall b:bool, b <> true -> negb b = true. Proof. destruct b; intuition. Qed. -Notation bool_6 := eq_true_not_negb. (* Compatibility *) +Notation bool_6 := eq_true_not_negb (only parsing). (* Compatibility *) Hint Resolve eq_true_not_negb : bool. @@ -596,7 +612,7 @@ Qed. Hint Resolve trans_eq_bool. (*****************************************) -(** *** Reflection of [bool] into [Prop] *) +(** * Reflection of [bool] into [Prop] *) (*****************************************) (** [Is_true] and equality *) @@ -605,9 +621,9 @@ Hint Unfold Is_true: bool. Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true. Proof. -destruct x; simpl in |- *; tauto. + destruct x; simpl in |- *; tauto. Qed. - + Lemma Is_true_eq_left : forall x:bool, x = true -> Is_true x. Proof. intros; rewrite H; auto with bool. @@ -635,7 +651,7 @@ Qed. (** [Is_true] and connectives *) Lemma orb_prop_elim : - forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b. + forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b. Proof. destruct a; destruct b; simpl; tauto. Qed. @@ -643,13 +659,13 @@ Qed. Notation orb_prop2 := orb_prop_elim (only parsing). Lemma orb_prop_intro : - forall a b:bool, Is_true a \/ Is_true b -> Is_true (a || b). + forall a b:bool, Is_true a \/ Is_true b -> Is_true (a || b). Proof. destruct a; destruct b; simpl; tauto. Qed. Lemma andb_prop_intro : - forall b1 b2:bool, Is_true b1 /\ Is_true b2 -> Is_true (b1 && b2). + forall b1 b2:bool, Is_true b1 /\ Is_true b2 -> Is_true (b1 && b2). Proof. destruct b1; destruct b2; simpl in |- *; tauto. Qed. @@ -660,42 +676,42 @@ Notation andb_true_intro2 := (only parsing). Lemma andb_prop_elim : - forall a b:bool, Is_true (a && b) -> Is_true a /\ Is_true b. + forall a b:bool, Is_true (a && b) -> Is_true a /\ Is_true b. Proof. destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); - auto with bool. + auto with bool. Qed. Hint Resolve andb_prop_elim: bool v62. Notation andb_prop2 := andb_prop_elim (only parsing). Lemma eq_bool_prop_intro : - forall b1 b2, (Is_true b1 <-> Is_true b2) -> b1 = b2. + forall b1 b2, (Is_true b1 <-> Is_true b2) -> b1 = b2. Proof. - destruct b1; destruct b2; simpl in *; intuition. + destruct b1; destruct b2; simpl in *; intuition. Qed. Lemma eq_bool_prop_elim : forall b1 b2, b1 = b2 -> (Is_true b1 <-> Is_true b2). Proof. - intros b1 b2; case b1; case b2; intuition. + intros b1 b2; case b1; case b2; intuition. Qed. Lemma negb_prop_elim : forall b, Is_true (negb b) -> ~ Is_true b. Proof. - destruct b; intuition. + destruct b; intuition. Qed. Lemma negb_prop_intro : forall b, ~ Is_true b -> Is_true (negb b). Proof. - destruct b; simpl in *; intuition. + destruct b; simpl in *; intuition. Qed. Lemma negb_prop_classical : forall b, ~ Is_true (negb b) -> Is_true b. Proof. - destruct b; intuition. + destruct b; intuition. Qed. Lemma negb_prop_involutive : forall b, Is_true b -> ~ Is_true (negb b). Proof. - destruct b; intuition. + destruct b; intuition. Qed. |