diff options
Diffstat (limited to 'theories/Bool')
| -rw-r--r--[-rwxr-xr-x] | theories/Bool/Bool.v | 440 | ||||
| -rw-r--r-- | theories/Bool/BoolEq.v | 2 | ||||
| -rw-r--r-- | theories/Bool/Bvector.v | 52 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Bool/DecBool.v | 2 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Bool/IfProp.v | 2 | ||||
| -rw-r--r-- | theories/Bool/Sumbool.v | 6 | ||||
| -rw-r--r--[-rwxr-xr-x] | theories/Bool/Zerob.v | 2 |
7 files changed, 312 insertions, 194 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 854eb9e3..ff87eb96 100755..100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -6,32 +6,28 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Bool.v,v 1.29.2.1 2004/07/16 19:31:01 herbelin Exp $ i*) +(*i $Id: Bool.v 8642 2006-03-17 10:09:02Z notin $ i*) -(** Booleans *) +(** ** Booleans *) (** The type [bool] is defined in the prelude as [Inductive bool : Set := true : bool | false : bool] *) -(** Interpretation of booleans as Proposition *) +(** Interpretation of booleans as propositions *) Definition Is_true (b:bool) := match b with | true => True | false => False end. -Hint Unfold Is_true: bool. -Lemma Is_true_eq_left : forall x:bool, x = true -> Is_true x. -Proof. - intros; rewrite H; auto with bool. -Qed. +(*****************) +(** Decidability *) +(*****************) -Lemma Is_true_eq_right : forall x:bool, true = x -> Is_true x. +Lemma bool_dec : forall b1 b2 : bool, {b1 = b2} + {b1 <> b2}. Proof. - intros; rewrite <- H; auto with bool. -Qed. - -Hint Immediate Is_true_eq_right Is_true_eq_left: bool. + decide equality. +Defined. (*******************) (** Discrimination *) @@ -40,24 +36,26 @@ Hint Immediate Is_true_eq_right Is_true_eq_left: bool. Lemma diff_true_false : true <> false. Proof. unfold not in |- *; intro contr; change (Is_true false) in |- *. -elim contr; simpl in |- *; trivial with bool. +elim contr; simpl in |- *; trivial. Qed. -Hint Resolve diff_true_false: bool v62. +Hint Resolve diff_true_false : bool v62. Lemma diff_false_true : false <> true. -Proof. +Proof. red in |- *; intros H; apply diff_true_false. symmetry in |- *. assumption. Qed. -Hint Resolve diff_false_true: bool v62. +Hint Resolve diff_false_true : bool v62. +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. Qed. -Hint Resolve eq_true_false_abs: bool. Lemma not_true_is_false : forall b:bool, b <> true -> b = false. +Proof. destruct b. intros. red in H; elim H. @@ -67,6 +65,7 @@ reflexivity. Qed. Lemma not_false_is_true : forall b:bool, b <> false -> b = true. +Proof. destruct b. intros. reflexivity. @@ -85,6 +84,8 @@ Definition leb (b1 b2:bool) := end. Hint Unfold leb: bool v62. +(* Infix "<=" := leb : bool_scope. *) + (*************) (** Equality *) (*************) @@ -97,24 +98,9 @@ Definition eqb (b1 b2:bool) : bool := | false, false => true end. -Lemma eqb_refl : forall x:bool, Is_true (eqb x x). -destruct x; simpl in |- *; auto with bool. -Qed. - -Lemma eqb_eq : forall x y:bool, Is_true (eqb x y) -> x = y. -destruct x; destruct y; simpl in |- *; tauto. -Qed. - -Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true. -destruct x; simpl in |- *; tauto. -Qed. - -Lemma Is_true_eq_true2 : forall x:bool, x = true -> Is_true x. -destruct x; simpl in |- *; auto with bool. -Qed. - 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. @@ -130,6 +116,7 @@ trivial with bool. Qed. Lemma eqb_reflx : forall b:bool, eqb b b = true. +Proof. intro b. case b. trivial with bool. @@ -137,6 +124,7 @@ 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. Qed. @@ -165,10 +153,7 @@ Definition xorb (b1 b2:bool) : bool := | false, false => false end. -Definition negb (b:bool) := match b with - | true => false - | false => true - end. +Definition negb (b:bool) := if b then false else true. Infix "||" := orb (at level 50, left associativity) : bool_scope. Infix "&&" := andb (at level 40, left associativity) : bool_scope. @@ -179,30 +164,37 @@ Delimit Scope bool_scope with bool. Bind Scope bool_scope with bool. -(**************************) -(** Lemmas about [negb] *) -(**************************) +(****************************) +(** De Morgan laws *) +(****************************) -Lemma negb_intro : forall b:bool, b = negb (negb b). +Lemma negb_orb : forall b1 b2:bool, negb (b1 || b2) = negb b1 && negb b2. Proof. -destruct b; reflexivity. + destruct b1; destruct b2; simpl in |- *; reflexivity. Qed. -Lemma negb_elim : forall b:bool, negb (negb b) = b. +Lemma negb_andb : forall b1 b2:bool, negb (b1 && b2) = negb b1 || negb b2. Proof. -destruct b; reflexivity. + destruct b1; destruct b2; simpl in |- *; reflexivity. Qed. - -Lemma negb_orb : forall b1 b2:bool, negb (b1 || b2) = negb b1 && negb b2. + +(********************************) +(** *** Properties of [negb] *) +(********************************) + +Lemma negb_involutive : forall b:bool, negb (negb b) = b. Proof. - destruct b1; destruct b2; simpl in |- *; reflexivity. +destruct b; reflexivity. Qed. -Lemma negb_andb : forall b1 b2:bool, negb (b1 && b2) = negb b1 || negb b2. +Lemma negb_involutive_reverse : forall b:bool, b = negb (negb b). Proof. - destruct b1; destruct b2; simpl in |- *; reflexivity. +destruct b; reflexivity. Qed. +Notation negb_elim := negb_involutive (only parsing). +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. @@ -215,12 +207,14 @@ destruct b; simpl in |- *; intro; apply diff_true_false; Qed. Lemma eqb_negb1 : forall b:bool, eqb (negb b) b = false. +Proof. 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. @@ -235,22 +229,25 @@ Proof. Qed. -(****************************) -(** A few lemmas about [or] *) -(****************************) +(********************************) +(** *** Properties of [orb] *) +(********************************) -Lemma orb_prop : forall a b:bool, a || b = true -> a = true \/ b = true. -destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); - auto with bool. -Qed. +Lemma orb_true_elim : + forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}. +Proof. +destruct b1; simpl in |- *; auto with bool. +Defined. -Lemma orb_prop2 : forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b. +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. Qed. Lemma orb_true_intro : 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. @@ -258,37 +255,45 @@ rewrite H; trivial with bool. Qed. Hint Resolve orb_true_intro: bool v62. -Lemma orb_b_true : forall b:bool, b || true = true. +Lemma orb_false_intro : + forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false. +Proof. +intros b1 b2 H1 H2; rewrite H1; rewrite H2; trivial with bool. +Qed. +Hint Resolve orb_false_intro: bool v62. + +(** [true] is a zero for [orb] *) + +Lemma orb_true_r : forall b:bool, b || true = true. +Proof. auto with bool. Qed. -Hint Resolve orb_b_true: bool v62. +Hint Resolve orb_true_r: bool v62. -Lemma orb_true_b : forall b:bool, true || b = true. +Lemma orb_true_l : forall b:bool, true || b = true. +Proof. trivial with bool. Qed. -Definition orb_true_elim : - forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}. -destruct b1; simpl in |- *; auto with bool. -Defined. +Notation orb_b_true := orb_true_r (only parsing). +Notation orb_true_b := orb_true_l (only parsing). -Lemma orb_false_intro : - forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false. -intros b1 b2 H1 H2; rewrite H1; rewrite H2; trivial with bool. -Qed. -Hint Resolve orb_false_intro: bool v62. +(** [false] is neutral for [orb] *) -Lemma orb_b_false : forall b:bool, b || false = b. +Lemma orb_false_r : forall b:bool, b || false = b. Proof. destruct b; trivial with bool. Qed. -Hint Resolve orb_b_false: bool v62. +Hint Resolve orb_false_r: bool v62. -Lemma orb_false_b : forall b:bool, false || b = b. +Lemma orb_false_l : forall b:bool, false || b = b. Proof. destruct b; trivial with bool. Qed. -Hint Resolve orb_false_b: bool v62. +Hint Resolve orb_false_l: bool v62. + +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. @@ -300,49 +305,48 @@ Proof. auto with bool. Qed. -Lemma orb_neg_b : forall b:bool, b || negb b = true. +(** Complementation *) + +Lemma orb_negb_r : forall b:bool, b || negb b = true. Proof. destruct b; reflexivity. Qed. -Hint Resolve orb_neg_b: bool v62. +Hint Resolve orb_negb_r: bool v62. + +Notation orb_neg_b := orb_negb_r (only parsing). + +(** Commutativity *) Lemma orb_comm : forall b1 b2:bool, b1 || b2 = b2 || b1. +Proof. destruct b1; destruct b2; reflexivity. Qed. +(** Associativity *) + Lemma orb_assoc : forall b1 b2 b3:bool, b1 || (b2 || b3) = b1 || b2 || b3. Proof. destruct b1; destruct b2; destruct b3; reflexivity. Qed. +Hint Resolve orb_comm orb_assoc: bool v62. -Hint Resolve orb_comm orb_assoc orb_b_false orb_false_b: bool v62. - -(*****************************) -(** A few lemmas about [and] *) -(*****************************) +(*********************************) +(** *** 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. Qed. Hint Resolve andb_prop: bool v62. -Definition andb_true_eq : +Lemma andb_true_eq : forall a b:bool, true = a && b -> true = a /\ true = b. Proof. destruct a; destruct b; auto. Defined. -Lemma andb_prop2 : - 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. -Qed. -Hint Resolve andb_prop2: bool v62. - Lemma andb_true_intro : forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true. Proof. @@ -350,61 +354,130 @@ Proof. Qed. Hint Resolve andb_true_intro: bool v62. -Lemma andb_true_intro2 : - forall b1 b2:bool, Is_true b1 -> Is_true b2 -> Is_true (b1 && b2). -Proof. - destruct b1; destruct b2; simpl in |- *; tauto. -Qed. -Hint Resolve andb_true_intro2: 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. 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. Qed. -Lemma andb_b_false : forall b:bool, b && false = false. +(** [false] is a zero for [andb] *) + +Lemma andb_false_r : forall b:bool, b && false = false. +Proof. destruct b; auto with bool. Qed. -Lemma andb_false_b : forall b:bool, false && b = false. +Lemma andb_false_l : forall b:bool, false && b = false. +Proof. trivial with bool. Qed. -Lemma andb_b_true : forall b:bool, b && true = b. +Notation andb_b_false := andb_false_r (only parsing). +Notation andb_false_b := andb_false_l (only parsing). + +(** [true] is neutral for [andb] *) + +Lemma andb_true_r : forall b:bool, b && true = b. +Proof. destruct b; auto with bool. Qed. -Lemma andb_true_b : forall b:bool, true && b = b. +Lemma andb_true_l : forall b:bool, true && b = b. +Proof. trivial with bool. Qed. -Definition andb_false_elim : +Notation andb_b_true := andb_true_r (only parsing). +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. Defined. Hint Resolve andb_false_elim: bool v62. -Lemma andb_neg_b : forall b:bool, b && negb b = false. +(** Complementation *) + +Lemma andb_negb_r : forall b:bool, b && negb b = false. +Proof. destruct b; reflexivity. Qed. -Hint Resolve andb_neg_b: bool v62. +Hint Resolve andb_negb_r: bool v62. + +Notation andb_neg_b := andb_negb_r (only parsing). + +(** Commutativity *) Lemma andb_comm : forall b1 b2:bool, b1 && b2 = b2 && b1. +Proof. 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. Qed. Hint Resolve andb_comm andb_assoc: bool v62. -(*******************************) -(** Properties of [xorb] *) -(*******************************) +(*******************************************) +(** *** Properties mixing [andb] and [orb] *) +(*******************************************) + +(** Distributivity *) + +Lemma andb_orb_distrib_r : + forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3. +Proof. +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. +Qed. + +Lemma orb_andb_distrib_r : + forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3). +Proof. +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). +Proof. +destruct b1; destruct b2; destruct b3; reflexivity. +Qed. + +(* Compatibility *) +Notation demorgan1 := andb_orb_distrib_r (only parsing). +Notation demorgan2 := andb_orb_distrib_l (only parsing). +Notation demorgan3 := orb_andb_distrib_r (only parsing). +Notation demorgan4 := orb_andb_distrib_l (only parsing). + +(** Absorption *) + +Lemma absoption_andb : forall b1 b2:bool, b1 && (b1 || b2) = b1. +Proof. + destruct b1; destruct b2; simpl in |- *; reflexivity. +Qed. + +Lemma absoption_orb : forall b1 b2:bool, b1 || b1 && b2 = b1. +Proof. + destruct b1; destruct b2; simpl in |- *; reflexivity. +Qed. + +(***********************************) +(** *** Properties of [xorb] *) +(***********************************) Lemma xorb_false : forall b:bool, xorb b false = b. Proof. @@ -473,71 +546,156 @@ Proof. intros. rewrite H. rewrite xorb_assoc. rewrite xorb_nilpotent. apply xorb_false. Qed. -(*******************************) -(** De Morgan's law *) -(*******************************) +(** Lemmas about the [b = true] embedding of [bool] to [Prop] *) -Lemma demorgan1 : - forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3. -destruct b1; destruct b2; destruct b3; reflexivity. +Lemma eq_true_iff_eq : forall b1 b2, (b1 = true <-> b2 = true) -> b1 = b2. +Proof. + intros b1 b2; case b1; case b2; intuition. Qed. -Lemma demorgan2 : - forall b1 b2 b3:bool, (b1 || b2) && b3 = b1 && b3 || b2 && b3. -destruct b1; destruct b2; destruct b3; reflexivity. +Notation bool_1 := eq_true_iff_eq. (* Compatibility *) + +Lemma eq_true_negb_classical : forall b:bool, negb b <> true -> b = true. +Proof. + destruct b; intuition. Qed. -Lemma demorgan3 : - forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3). -destruct b1; destruct b2; destruct b3; reflexivity. +Notation bool_3 := eq_true_negb_classical. (* Compatibility *) + +Lemma eq_true_not_negb : forall b:bool, b <> true -> negb b = true. +Proof. + destruct b; intuition. Qed. -Lemma demorgan4 : - forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3). -destruct b1; destruct b2; destruct b3; reflexivity. +Notation bool_6 := eq_true_not_negb. (* Compatibility *) + +Hint Resolve eq_true_not_negb : bool. + +(* An interesting lemma for auto but too strong to keep compatibility *) + +Lemma absurd_eq_bool : forall b b':bool, False -> b = b'. +Proof. + contradiction. Qed. -Lemma absoption_andb : forall b1 b2:bool, b1 && (b1 || b2) = b1. +(* A more specific one that preserves compatibility with old hint bool_3 *) + +Lemma absurd_eq_true : forall b, False -> b = true. Proof. - destruct b1; destruct b2; simpl in |- *; reflexivity. + contradiction. Qed. +Hint Resolve absurd_eq_true. -Lemma absoption_orb : forall b1 b2:bool, b1 || b1 && b2 = b1. +(* A specific instance of trans_eq that preserves compatibility with + old hint bool_2 *) + +Lemma trans_eq_bool : forall x y z:bool, x = y -> y = z -> x = z. Proof. - destruct b1; destruct b2; simpl in |- *; reflexivity. + apply trans_eq. +Qed. +Hint Resolve trans_eq_bool. + +(*****************************************) +(** *** Reflection of [bool] into [Prop] *) +(*****************************************) + +(** [Is_true] and equality *) + +Hint Unfold Is_true: bool. + +Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true. +Proof. +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. +Qed. + +Lemma Is_true_eq_right : forall x:bool, true = x -> Is_true x. +Proof. + intros; rewrite <- H; auto with bool. +Qed. + +Notation Is_true_eq_true2 := Is_true_eq_right (only parsing). + +Hint Immediate Is_true_eq_right Is_true_eq_left: bool. + +Lemma eqb_refl : forall x:bool, Is_true (eqb x x). +Proof. + destruct x; simpl; auto with bool. +Qed. + +Lemma eqb_eq : forall x y:bool, Is_true (eqb x y) -> x = y. +Proof. + destruct x; destruct y; simpl; tauto. Qed. +(** [Is_true] and connectives *) + +Lemma orb_prop_elim : + forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b. +Proof. + destruct a; destruct b; simpl; tauto. +Qed. -(** Misc. equalities between booleans (to be used by Auto) *) +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). +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). +Proof. + destruct b1; destruct b2; simpl in |- *; tauto. +Qed. +Hint Resolve andb_prop_intro: bool v62. -Lemma bool_1 : forall b1 b2:bool, (b1 = true <-> b2 = true) -> b1 = b2. +Notation andb_true_intro2 := + (fun b1 b2 H1 H2 => andb_prop_intro b1 b2 (conj H1 H2)) + (only parsing). + +Lemma andb_prop_elim : + 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. +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. Proof. - intros b1 b2; case b1; case b2; intuition. + destruct b1; destruct b2; simpl in *; intuition. Qed. -Lemma bool_2 : forall b1 b2:bool, b1 = b2 -> b1 = true -> b2 = true. +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. Qed. -Lemma bool_3 : forall b:bool, negb b <> true -> b = true. +Lemma negb_prop_elim : forall b, Is_true (negb b) -> ~ Is_true b. Proof. - destruct b; intuition. + destruct b; intuition. Qed. -Lemma bool_4 : forall b:bool, b = true -> negb b <> true. +Lemma negb_prop_intro : forall b, ~ Is_true b -> Is_true (negb b). Proof. - destruct b; intuition. + destruct b; simpl in *; intuition. Qed. -Lemma bool_5 : forall b:bool, negb b = true -> b <> true. +Lemma negb_prop_classical : forall b, ~ Is_true (negb b) -> Is_true b. Proof. - destruct b; intuition. + destruct b; intuition. Qed. -Lemma bool_6 : forall b:bool, b <> true -> negb b = true. +Lemma negb_prop_involutive : forall b, Is_true b -> ~ Is_true (negb b). Proof. - destruct b; intuition. + destruct b; intuition. Qed. - -Hint Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6. diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index e038b3da..806ac70f 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BoolEq.v,v 1.4.2.1 2004/07/16 19:31:02 herbelin Exp $ i*) +(*i $Id: BoolEq.v 5920 2004-07-16 20:01:26Z herbelin $ i*) (* Cuihtlauac Alvarado - octobre 2000 *) (** Properties of a boolean equality *) diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 51d940cf..b58ed280 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Bvector.v,v 1.6.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) +(*i $Id: Bvector.v 6844 2005-03-16 13:09:55Z herbelin $ i*) (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) @@ -17,7 +17,7 @@ Require Import Arith. Open Local Scope nat_scope. (* -On s'inspire de PolyList pour fabriquer les vecteurs de bits. +On s'inspire de List.v pour fabriquer les vecteurs de bits. La dimension du vecteur est un paramètre trop important pour se contenter de la fonction "length". La première idée est de faire un record avec la liste et la longueur. @@ -26,42 +26,9 @@ de nombreux lemmes pour gerer les longueurs. La seconde idée est de faire un type dépendant dans lequel la longueur est un paramètre de construction. Cela complique un peu les inductions structurelles, la solution qui a ma préférence -est alors d'utiliser un terme de preuve comme définition. - -(En effet une définition comme : -Fixpoint Vunaire [n:nat; v:(vector n)]: (vector n) := -Cases v of - | Vnil => Vnil - | (Vcons a p v') => (Vcons (f a) p (Vunaire p v')) -end. -provoque ce message d'erreur : -Coq < Error: Inference of annotation not yet implemented in this case). - - - Inductive list [A : Set] : Set := - nil : (list A) | cons : A->(list A)->(list A). - head = [A:Set; l:(list A)] Cases l of - | nil => Error - | (cons x _) => (Value x) - end - : (A:Set)(list A)->(option A). - tail = [A:Set; l:(list A)]Cases l of - | nil => (nil A) - | (cons _ m) => m - end - : (A:Set)(list A)->(list A). - length = [A:Set] Fix length {length [l:(list A)] : nat := - Cases l of - | nil => O - | (cons _ m) => (S (length m)) - end} - : (A:Set)(list A)->nat. - map = [A,B:Set; f:(A->B)] Fix map {map [l:(list A)] : (list B) := - Cases l of - | nil => (nil B) - | (cons a t) => (cons (f a) (map t)) - end} - : (A,B:Set)(A->B)->(list A)->(list B) +est alors d'utiliser un terme de preuve comme définition, car le +mécanisme d'inférence du type du filtrage n'est pas aussi puissant que +celui implanté par les tactiques d'élimination. *) Section VECTORS. @@ -141,13 +108,6 @@ Proof. exact (Vcons a (S (S n)) (f H0)). Defined. -(* -Lemma S_minus_S : (n,p:nat) (gt n (S p)) -> (S (minus n (S p)))=(minus n p). -Proof. - Intros. -Save. -*) - Lemma Vtrunc : forall n p:nat, n > p -> vector n -> vector (n - p). Proof. induction p as [| p f]; intros H v. @@ -203,7 +163,7 @@ Implicit Arguments Vcons [A n]. Section BOOLEAN_VECTORS. -(* +(* Un vecteur de bits est un vecteur sur l'ensemble des booléens de longueur fixe. ATTENTION : le stockage s'effectue poids FAIBLE en tête. On en extrait le bit de poids faible (head) et la fin du vecteur (tail). diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 1998fb8e..b95b25fd 100755..100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: DecBool.v,v 1.6.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) +(*i $Id: DecBool.v 8642 2006-03-17 10:09:02Z notin $ i*) Set Implicit Arguments. diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index a00449d8..0a98c32a 100755..100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: IfProp.v,v 1.7.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) +(*i $Id: IfProp.v 8642 2006-03-17 10:09:02Z notin $ i*) Require Import Bool. diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 8188f038..2842437d 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Sumbool.v,v 1.12.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) +(*i $Id: Sumbool.v 7235 2005-07-15 17:11:57Z coq $ i*) (** Here are collected some results about the type sumbool (see INIT/Specif.v) [sumbool A B], which is written [{A}+{B}], is the informative @@ -63,8 +63,8 @@ Defined. End connectives. -Hint Resolve sumbool_and sumbool_or sumbool_not: core. - +Hint Resolve sumbool_and sumbool_or: core. +Hint Immediate sumbool_not : core. (** Any decidability function in type [sumbool] can be turned into a function returning a boolean with the corresponding specification: *) diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index b654e556..c9abf94a 100755..100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zerob.v,v 1.8.2.1 2004/07/16 19:31:03 herbelin Exp $ i*) +(*i $Id: Zerob.v 8642 2006-03-17 10:09:02Z notin $ i*) Require Import Arith. Require Import Bool. |