From 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 29 Nov 2003 17:28:49 +0000 Subject: Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bool.v | 549 ++++++++++++++++++++++++------------------------ theories/Bool/BoolEq.v | 61 +++--- theories/Bool/Bvector.v | 189 ++++++++--------- theories/Bool/DecBool.v | 22 +- theories/Bool/IfProp.v | 53 ++--- theories/Bool/Sumbool.v | 51 ++--- theories/Bool/Zerob.v | 34 +-- 7 files changed, 484 insertions(+), 475 deletions(-) (limited to 'theories/Bool') diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 3d0a7a2f1..fa786550c 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -14,131 +14,130 @@ [Inductive bool : Set := true : bool | false : bool] *) (** Interpretation of booleans as Proposition *) -Definition Is_true := [b:bool](Cases b of - true => True - | false => False - end). -Hints Unfold Is_true : bool. +Definition Is_true (b:bool) := + match b with + | true => True + | false => False + end. +Hint Unfold Is_true: bool. -Lemma Is_true_eq_left : (x:bool)x=true -> (Is_true x). +Lemma Is_true_eq_left : forall x:bool, x = true -> Is_true x. Proof. - Intros; Rewrite H; Auto with bool. + intros; rewrite H; auto with bool. Qed. -Lemma Is_true_eq_right : (x:bool)true=x -> (Is_true x). +Lemma Is_true_eq_right : forall x:bool, true = x -> Is_true x. Proof. - Intros; Rewrite <- H; Auto with bool. + intros; rewrite <- H; auto with bool. Qed. -Hints Immediate Is_true_eq_right Is_true_eq_left : bool. +Hint Immediate Is_true_eq_right Is_true_eq_left: bool. (*******************) (** Discrimination *) (*******************) -Lemma diff_true_false : ~true=false. +Lemma diff_true_false : true <> false. Proof. -Unfold not; Intro contr; Change (Is_true false). -Elim contr; Simpl; Trivial with bool. +unfold not in |- *; intro contr; change (Is_true false) in |- *. +elim contr; simpl in |- *; trivial with bool. Qed. -Hints Resolve diff_true_false : bool v62. +Hint Resolve diff_true_false: bool v62. -Lemma diff_false_true : ~false=true. +Lemma diff_false_true : false <> true. Proof. -Red; Intros H; Apply diff_true_false. -Symmetry. -Assumption. +red in |- *; intros H; apply diff_true_false. +symmetry in |- *. +assumption. Qed. -Hints Resolve diff_false_true : bool v62. +Hint Resolve diff_false_true: bool v62. -Lemma eq_true_false_abs : (b:bool)(b=true)->(b=false)->False. -Intros b H; Rewrite H; Auto with bool. +Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False. +intros b H; rewrite H; auto with bool. Qed. -Hints Resolve eq_true_false_abs : bool. +Hint Resolve eq_true_false_abs: bool. -Lemma not_true_is_false : (b:bool)~b=true->b=false. -NewDestruct b. -Intros. -Red in H; Elim H. -Reflexivity. -Intros abs. -Reflexivity. +Lemma not_true_is_false : forall b:bool, b <> true -> b = false. +destruct b. +intros. +red in H; elim H. +reflexivity. +intros abs. +reflexivity. Qed. -Lemma not_false_is_true : (b:bool)~b=false->b=true. -NewDestruct b. -Intros. -Reflexivity. -Intro H; Red in H; Elim H. -Reflexivity. +Lemma not_false_is_true : forall b:bool, b <> false -> b = true. +destruct b. +intros. +reflexivity. +intro H; red in H; elim H. +reflexivity. Qed. (**********************) (** Order on booleans *) (**********************) -Definition leb := [b1,b2:bool] - Cases b1 of - | true => b2=true - | false => True +Definition leb (b1 b2:bool) := + match b1 with + | true => b2 = true + | false => True end. -Hints Unfold leb : bool v62. +Hint Unfold leb: bool v62. (*************) (** Equality *) (*************) -Definition eqb : bool->bool->bool := - [b1,b2:bool] - Cases b1 b2 of - true true => true - | true false => false - | false true => false - | false false => true - end. +Definition eqb (b1 b2:bool) : bool := + match b1, b2 with + | true, true => true + | true, false => false + | false, true => false + | false, false => true + end. -Lemma eqb_refl : (x:bool)(Is_true (eqb x x)). -NewDestruct x; Simpl; Auto with bool. +Lemma eqb_refl : forall x:bool, Is_true (eqb x x). +destruct x; simpl in |- *; auto with bool. Qed. -Lemma eqb_eq : (x,y:bool)(Is_true (eqb x y))->x=y. -NewDestruct x; NewDestruct y; Simpl; Tauto. +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 : (x:bool) (Is_true x) -> x=true. -NewDestruct x; Simpl; Tauto. +Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true. +destruct x; simpl in |- *; tauto. Qed. -Lemma Is_true_eq_true2 : (x:bool) x=true -> (Is_true x). -NewDestruct x; Simpl; Auto with bool. +Lemma Is_true_eq_true2 : forall x:bool, x = true -> Is_true x. +destruct x; simpl in |- *; auto with bool. Qed. -Lemma eqb_subst : - (P:bool->Prop)(b1,b2:bool)(eqb b1 b2)=true->(P b1)->(P b2). -Unfold eqb . -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. +Lemma eqb_subst : + forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2. +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 : (b:bool)(eqb b b)=true. -Intro b. -Case b. -Trivial with bool. -Trivial with bool. +Lemma eqb_reflx : forall b:bool, eqb b b = true. +intro b. +case b. +trivial with bool. +trivial with bool. Qed. -Lemma eqb_prop : (a,b:bool)(eqb a b)=true -> a=b. -NewDestruct a; NewDestruct b; Simpl; Intro; - Discriminate H Orelse Reflexivity. +Lemma eqb_prop : forall a b:bool, eqb a b = true -> a = b. +destruct a; destruct b; simpl in |- *; intro; discriminate H || reflexivity. Qed. @@ -146,36 +145,34 @@ Qed. (** Logical combinators *) (************************) -Definition ifb : bool -> bool -> bool -> bool - := [b1,b2,b3:bool](Cases b1 of true => b2 | false => b3 end). +Definition ifb (b1 b2 b3:bool) : bool := + match b1 with + | true => b2 + | false => b3 + end. -Definition andb : bool -> bool -> bool - := [b1,b2:bool](ifb b1 b2 false). +Definition andb (b1 b2:bool) : bool := ifb b1 b2 false. -Definition orb : bool -> bool -> bool - := [b1,b2:bool](ifb b1 true b2). +Definition orb (b1 b2:bool) : bool := ifb b1 true b2. -Definition implb : bool -> bool -> bool - := [b1,b2:bool](ifb b1 b2 true). +Definition implb (b1 b2:bool) : bool := ifb b1 b2 true. -Definition xorb : bool -> bool -> bool - := [b1,b2:bool] - Cases b1 b2 of - true true => false - | true false => true - | false true => true - | false false => false - end. +Definition xorb (b1 b2:bool) : bool := + match b1, b2 with + | true, true => false + | true, false => true + | false, true => true + | false, false => false + end. -Definition negb := [b:bool]Cases b of - true => false - | false => true - end. +Definition negb (b:bool) := match b with + | true => false + | false => true + end. -Infix "||" orb (at level 4, left associativity) : bool_scope. -Infix "&&" andb (at level 3, no associativity) : bool_scope - V8only (at level 40, left associativity). -V8Notation "- b" := (negb b) : bool_scope. +Infix "||" := orb (at level 50, left associativity) : bool_scope. +Infix "&&" := andb (at level 40, left associativity) : bool_scope. +Notation "- b" := (negb b) : bool_scope. Open Local Scope bool_scope. @@ -183,54 +180,55 @@ Open Local Scope bool_scope. (** Lemmas about [negb] *) (**************************) -Lemma negb_intro : (b:bool)b=(negb (negb b)). +Lemma negb_intro : forall b:bool, b = - - b. Proof. -NewDestruct b; Reflexivity. +destruct b; reflexivity. Qed. -Lemma negb_elim : (b:bool)(negb (negb b))=b. +Lemma negb_elim : forall b:bool, - - b = b. Proof. -NewDestruct b; Reflexivity. +destruct b; reflexivity. Qed. -Lemma negb_orb : (b1,b2:bool) - (negb (orb b1 b2)) = (andb (negb b1) (negb b2)). +Lemma negb_orb : forall b1 b2:bool, - (b1 || b2) = - b1 && - b2. Proof. - NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. + destruct b1; destruct b2; simpl in |- *; reflexivity. Qed. -Lemma negb_andb : (b1,b2:bool) - (negb (andb b1 b2)) = (orb (negb b1) (negb b2)). +Lemma negb_andb : forall b1 b2:bool, - (b1 && b2) = - b1 || - b2. Proof. - NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. + destruct b1; destruct b2; simpl in |- *; reflexivity. Qed. -Lemma negb_sym : (b,b':bool)(b'=(negb b))->(b=(negb b')). +Lemma negb_sym : forall b b':bool, b' = - b -> b = - b'. Proof. -NewDestruct b; NewDestruct b'; Intros; Simpl; Trivial with bool. +destruct b; destruct b'; intros; simpl in |- *; trivial with bool. Qed. -Lemma no_fixpoint_negb : (b:bool)~(negb b)=b. +Lemma no_fixpoint_negb : forall b:bool, - b <> b. Proof. -NewDestruct b; Simpl; Unfold not; Intro; Apply diff_true_false; Auto with bool. +destruct b; simpl in |- *; unfold not in |- *; intro; apply diff_true_false; + auto with bool. Qed. -Lemma eqb_negb1 : (b:bool)(eqb (negb b) b)=false. -NewDestruct b. -Trivial with bool. -Trivial with bool. +Lemma eqb_negb1 : forall b:bool, eqb (- b) b = false. +destruct b. +trivial with bool. +trivial with bool. Qed. -Lemma eqb_negb2 : (b:bool)(eqb b (negb b))=false. -NewDestruct b. -Trivial with bool. -Trivial with bool. +Lemma eqb_negb2 : forall b:bool, eqb b (- b) = false. +destruct b. +trivial with bool. +trivial with bool. Qed. -Lemma if_negb : (A:Set) (b:bool) (x,y:A) (if (negb b) then x else y)=(if b then y else x). +Lemma if_negb : + forall (A:Set) (b:bool) (x y:A), + (if - b then x else y) = (if b then y else x). Proof. - NewDestruct b;Trivial. + destruct b; trivial. Qed. @@ -238,304 +236,305 @@ Qed. (** A few lemmas about [or] *) (****************************) -Lemma orb_prop : - (a,b:bool)(orb a b)=true -> (a = true)\/(b = true). -NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); Auto with bool. +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_prop2 : - (a,b:bool)(Is_true (orb a b)) -> (Is_true a)\/(Is_true b). -NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); Auto with bool. +Lemma orb_prop2 : forall a b:bool, Is_true (a || b) -> Is_true a \/ Is_true b. +destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); + auto with bool. Qed. -Lemma orb_true_intro - : (b1,b2:bool)(b1=true)\/(b2=true)->(orb b1 b2)=true. -NewDestruct b1; Auto with bool. -NewDestruct 1; Intros. -Elim diff_true_false; Auto with bool. -Rewrite H; Trivial with bool. +Lemma orb_true_intro : + forall b1 b2:bool, b1 = true \/ b2 = true -> b1 || b2 = true. +destruct b1; auto with bool. +destruct 1; intros. +elim diff_true_false; auto with bool. +rewrite H; trivial with bool. Qed. -Hints Resolve orb_true_intro : bool v62. +Hint Resolve orb_true_intro: bool v62. -Lemma orb_b_true : (b:bool)(orb b true)=true. -Auto with bool. +Lemma orb_b_true : forall b:bool, b || true = true. +auto with bool. Qed. -Hints Resolve orb_b_true : bool v62. +Hint Resolve orb_b_true: bool v62. -Lemma orb_true_b : (b:bool)(orb true b)=true. -Trivial with bool. +Lemma orb_true_b : forall b:bool, true || b = true. +trivial with bool. Qed. -Definition orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}. -NewDestruct b1; Simpl; Auto with bool. +Definition orb_true_elim : + forall b1 b2:bool, b1 || b2 = true -> {b1 = true} + {b2 = true}. +destruct b1; simpl in |- *; auto with bool. Defined. -Lemma orb_false_intro - : (b1,b2:bool)(b1=false)->(b2=false)->(orb b1 b2)=false. -Intros b1 b2 H1 H2; Rewrite H1; Rewrite H2; Trivial with bool. +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. -Hints Resolve orb_false_intro : bool v62. +Hint Resolve orb_false_intro: bool v62. -Lemma orb_b_false : (b:bool)(orb b false)=b. +Lemma orb_b_false : forall b:bool, b || false = b. Proof. - NewDestruct b; Trivial with bool. + destruct b; trivial with bool. Qed. -Hints Resolve orb_b_false : bool v62. +Hint Resolve orb_b_false: bool v62. -Lemma orb_false_b : (b:bool)(orb false b)=b. +Lemma orb_false_b : forall b:bool, false || b = b. Proof. - NewDestruct b; Trivial with bool. + destruct b; trivial with bool. Qed. -Hints Resolve orb_false_b : bool v62. +Hint Resolve orb_false_b: bool v62. -Lemma orb_false_elim : - (b1,b2:bool)(orb b1 b2)=false -> (b1=false)/\(b2=false). +Lemma orb_false_elim : + forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false. Proof. - NewDestruct b1. - Intros; Elim diff_true_false; Auto with bool. - NewDestruct b2. - Intros; Elim diff_true_false; Auto with bool. - Auto with bool. + destruct b1. + intros; elim diff_true_false; auto with bool. + destruct b2. + intros; elim diff_true_false; auto with bool. + auto with bool. Qed. -Lemma orb_neg_b : - (b:bool)(orb b (negb b))=true. +Lemma orb_neg_b : forall b:bool, b || - b = true. Proof. - NewDestruct b; Reflexivity. + destruct b; reflexivity. Qed. -Hints Resolve orb_neg_b : bool v62. +Hint Resolve orb_neg_b: bool v62. -Lemma orb_sym : (b1,b2:bool)(orb b1 b2)=(orb b2 b1). -NewDestruct b1; NewDestruct b2; Reflexivity. +Lemma orb_comm : forall b1 b2:bool, b1 || b2 = b2 || b1. +destruct b1; destruct b2; reflexivity. Qed. -Lemma orb_assoc : (b1,b2,b3:bool)(orb b1 (orb b2 b3))=(orb (orb b1 b2) b3). +Lemma orb_assoc : forall b1 b2 b3:bool, b1 || (b2 || b3) = b1 || b2 || b3. Proof. - NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. + destruct b1; destruct b2; destruct b3; reflexivity. Qed. -Hints Resolve orb_sym orb_assoc orb_b_false orb_false_b : bool v62. +Hint Resolve orb_comm orb_assoc orb_b_false orb_false_b: bool v62. (*****************************) (** A few lemmas about [and] *) (*****************************) -Lemma andb_prop : - (a,b:bool)(andb a b) = true -> (a = true)/\(b = true). +Lemma andb_prop : forall a b:bool, a && b = true -> a = true /\ b = true. Proof. - NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); - Auto with bool. + destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); + auto with bool. Qed. -Hints Resolve andb_prop : bool v62. +Hint Resolve andb_prop: bool v62. -Definition andb_true_eq : (a,b:bool) true = (andb a b) -> true = a /\ true = b. +Definition andb_true_eq : + forall a b:bool, true = a && b -> true = a /\ true = b. Proof. - NewDestruct a; NewDestruct b; Auto. + destruct a; destruct b; auto. Defined. -Lemma andb_prop2 : - (a,b:bool)(Is_true (andb a b)) -> (Is_true a)/\(Is_true b). +Lemma andb_prop2 : + forall a b:bool, Is_true (a && b) -> Is_true a /\ Is_true b. Proof. - NewDestruct a; NewDestruct b; Simpl; Try (Intro H;Discriminate H); - Auto with bool. + destruct a; destruct b; simpl in |- *; try (intro H; discriminate H); + auto with bool. Qed. -Hints Resolve andb_prop2 : bool v62. +Hint Resolve andb_prop2: bool v62. -Lemma andb_true_intro : (b1,b2:bool)(b1=true)/\(b2=true)->(andb b1 b2)=true. +Lemma andb_true_intro : + forall b1 b2:bool, b1 = true /\ b2 = true -> b1 && b2 = true. Proof. - NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool. + destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. Qed. -Hints Resolve andb_true_intro : bool v62. +Hint Resolve andb_true_intro: bool v62. -Lemma andb_true_intro2 : - (b1,b2:bool)(Is_true b1)->(Is_true b2)->(Is_true (andb b1 b2)). +Lemma andb_true_intro2 : + forall b1 b2:bool, Is_true b1 -> Is_true b2 -> Is_true (b1 && b2). Proof. - NewDestruct b1; NewDestruct b2; Simpl; Tauto. + destruct b1; destruct b2; simpl in |- *; tauto. Qed. -Hints Resolve andb_true_intro2 : bool v62. +Hint Resolve andb_true_intro2: bool v62. -Lemma andb_false_intro1 - : (b1,b2:bool)(b1=false)->(andb b1 b2)=false. -NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool. +Lemma andb_false_intro1 : forall b1 b2:bool, b1 = false -> b1 && b2 = false. +destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. Qed. -Lemma andb_false_intro2 - : (b1,b2:bool)(b2=false)->(andb b1 b2)=false. -NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool. +Lemma andb_false_intro2 : forall b1 b2:bool, b2 = false -> b1 && b2 = false. +destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. Qed. -Lemma andb_b_false : (b:bool)(andb b false)=false. -NewDestruct b; Auto with bool. +Lemma andb_b_false : forall b:bool, b && false = false. +destruct b; auto with bool. Qed. -Lemma andb_false_b : (b:bool)(andb false b)=false. -Trivial with bool. +Lemma andb_false_b : forall b:bool, false && b = false. +trivial with bool. Qed. -Lemma andb_b_true : (b:bool)(andb b true)=b. -NewDestruct b; Auto with bool. +Lemma andb_b_true : forall b:bool, b && true = b. +destruct b; auto with bool. Qed. -Lemma andb_true_b : (b:bool)(andb true b)=b. -Trivial with bool. +Lemma andb_true_b : forall b:bool, true && b = b. +trivial with bool. Qed. -Definition andb_false_elim : - (b1,b2:bool)(andb b1 b2)=false -> {b1=false}+{b2=false}. -NewDestruct b1; Simpl; Auto with bool. +Definition andb_false_elim : + forall b1 b2:bool, b1 && b2 = false -> {b1 = false} + {b2 = false}. +destruct b1; simpl in |- *; auto with bool. Defined. -Hints Resolve andb_false_elim : bool v62. +Hint Resolve andb_false_elim: bool v62. -Lemma andb_neg_b : - (b:bool)(andb b (negb b))=false. -NewDestruct b; Reflexivity. +Lemma andb_neg_b : forall b:bool, b && - b = false. +destruct b; reflexivity. Qed. -Hints Resolve andb_neg_b : bool v62. +Hint Resolve andb_neg_b: bool v62. -Lemma andb_sym : (b1,b2:bool)(andb b1 b2)=(andb b2 b1). -NewDestruct b1; NewDestruct b2; Reflexivity. +Lemma andb_comm : forall b1 b2:bool, b1 && b2 = b2 && b1. +destruct b1; destruct b2; reflexivity. Qed. -Lemma andb_assoc : (b1,b2,b3:bool)(andb b1 (andb b2 b3))=(andb (andb b1 b2) b3). -NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. +Lemma andb_assoc : forall b1 b2 b3:bool, b1 && (b2 && b3) = b1 && b2 && b3. +destruct b1; destruct b2; destruct b3; reflexivity. Qed. -Hints Resolve andb_sym andb_assoc : bool v62. +Hint Resolve andb_comm andb_assoc: bool v62. (*******************************) (** Properties of [xorb] *) (*******************************) -Lemma xorb_false : (b:bool) (xorb b false)=b. +Lemma xorb_false : forall b:bool, xorb b false = b. Proof. - NewDestruct b; Trivial. + destruct b; trivial. Qed. -Lemma false_xorb : (b:bool) (xorb false b)=b. +Lemma false_xorb : forall b:bool, xorb false b = b. Proof. - NewDestruct b; Trivial. + destruct b; trivial. Qed. -Lemma xorb_true : (b:bool) (xorb b true)=(negb b). +Lemma xorb_true : forall b:bool, xorb b true = - b. Proof. - Trivial. + trivial. Qed. -Lemma true_xorb : (b:bool) (xorb true b)=(negb b). +Lemma true_xorb : forall b:bool, xorb true b = - b. Proof. - NewDestruct b; Trivial. + destruct b; trivial. Qed. -Lemma xorb_nilpotent : (b:bool) (xorb b b)=false. +Lemma xorb_nilpotent : forall b:bool, xorb b b = false. Proof. - NewDestruct b; Trivial. + destruct b; trivial. Qed. -Lemma xorb_comm : (b,b':bool) (xorb b b')=(xorb b' b). +Lemma xorb_comm : forall b b':bool, xorb b b' = xorb b' b. Proof. - NewDestruct b; NewDestruct b'; Trivial. + destruct b; destruct b'; trivial. Qed. -Lemma xorb_assoc : (b,b',b'':bool) (xorb (xorb b b') b'')=(xorb b (xorb b' b'')). +Lemma xorb_assoc : + forall b b' b'':bool, xorb (xorb b b') b'' = xorb b (xorb b' b''). Proof. - NewDestruct b; NewDestruct b'; NewDestruct b''; Trivial. + destruct b; destruct b'; destruct b''; trivial. Qed. -Lemma xorb_eq : (b,b':bool) (xorb b b')=false -> b=b'. +Lemma xorb_eq : forall b b':bool, xorb b b' = false -> b = b'. Proof. - NewDestruct b; NewDestruct b'; Trivial. - Unfold xorb. Intros. Rewrite H. Reflexivity. + destruct b; destruct b'; trivial. + unfold xorb in |- *. intros. rewrite H. reflexivity. Qed. -Lemma xorb_move_l_r_1 : (b,b',b'':bool) (xorb b b')=b'' -> b'=(xorb b b''). +Lemma xorb_move_l_r_1 : + 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. + intros. rewrite <- (false_xorb b'). rewrite <- (xorb_nilpotent b). rewrite xorb_assoc. + rewrite H. reflexivity. Qed. -Lemma xorb_move_l_r_2 : (b,b',b'':bool) (xorb b b')=b'' -> b=(xorb b'' b'). +Lemma xorb_move_l_r_2 : + 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. + 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 : (b,b',b'':bool) b=(xorb b' b'') -> (xorb b' b)=b''. +Lemma xorb_move_r_l_1 : + 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. + intros. rewrite H. rewrite <- xorb_assoc. rewrite xorb_nilpotent. apply false_xorb. Qed. -Lemma xorb_move_r_l_2 : (b,b',b'':bool) b=(xorb b' b'') -> (xorb b b'')=b'. +Lemma xorb_move_r_l_2 : + 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. + intros. rewrite H. rewrite xorb_assoc. rewrite xorb_nilpotent. apply xorb_false. Qed. (*******************************) (** De Morgan's law *) (*******************************) -Lemma demorgan1 : (b1,b2,b3:bool) - (andb b1 (orb b2 b3)) = (orb (andb b1 b2) (andb b1 b3)). -NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. +Lemma demorgan1 : + forall b1 b2 b3:bool, b1 && (b2 || b3) = b1 && b2 || b1 && b3. +destruct b1; destruct b2; destruct b3; reflexivity. Qed. -Lemma demorgan2 : (b1,b2,b3:bool) - (andb (orb b1 b2) b3) = (orb (andb b1 b3) (andb b2 b3)). -NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. +Lemma demorgan2 : + forall b1 b2 b3:bool, (b1 || b2) && b3 = b1 && b3 || b2 && b3. +destruct b1; destruct b2; destruct b3; reflexivity. Qed. -Lemma demorgan3 : (b1,b2,b3:bool) - (orb b1 (andb b2 b3)) = (andb (orb b1 b2) (orb b1 b3)). -NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. +Lemma demorgan3 : + forall b1 b2 b3:bool, b1 || b2 && b3 = (b1 || b2) && (b1 || b3). +destruct b1; destruct b2; destruct b3; reflexivity. Qed. -Lemma demorgan4 : (b1,b2,b3:bool) - (orb (andb b1 b2) b3) = (andb (orb b1 b3) (orb b2 b3)). -NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. +Lemma demorgan4 : + forall b1 b2 b3:bool, b1 && b2 || b3 = (b1 || b3) && (b2 || b3). +destruct b1; destruct b2; destruct b3; reflexivity. Qed. -Lemma absoption_andb : (b1,b2:bool) - (andb b1 (orb b1 b2)) = b1. +Lemma absoption_andb : forall b1 b2:bool, b1 && (b1 || b2) = b1. Proof. - NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. + destruct b1; destruct b2; simpl in |- *; reflexivity. Qed. -Lemma absoption_orb : (b1,b2:bool) - (orb b1 (andb b1 b2)) = b1. +Lemma absoption_orb : forall b1 b2:bool, b1 || b1 && b2 = b1. Proof. - NewDestruct b1; NewDestruct b2; Simpl; Reflexivity. + destruct b1; destruct b2; simpl in |- *; reflexivity. Qed. (** Misc. equalities between booleans (to be used by Auto) *) -Lemma bool_1 : (b1,b2:bool)(b1=true <-> b2=true) -> b1=b2. +Lemma bool_1 : forall b1 b2:bool, (b1 = true <-> b2 = true) -> b1 = b2. Proof. - Intros b1 b2; Case b1; Case b2; Intuition. + intros b1 b2; case b1; case b2; intuition. Qed. -Lemma bool_2 : (b1,b2:bool)b1=b2 -> b1=true -> b2=true. +Lemma bool_2 : forall b1 b2:bool, b1 = b2 -> b1 = true -> b2 = true. Proof. - Intros b1 b2; Case b1; Case b2; Intuition. + intros b1 b2; case b1; case b2; intuition. Qed. -Lemma bool_3 : (b:bool) ~(negb b)=true -> b=true. +Lemma bool_3 : forall b:bool, - b <> true -> b = true. Proof. - NewDestruct b; Intuition. + destruct b; intuition. Qed. -Lemma bool_4 : (b:bool) b=true -> ~(negb b)=true. +Lemma bool_4 : forall b:bool, b = true -> - b <> true. Proof. - NewDestruct b; Intuition. + destruct b; intuition. Qed. -Lemma bool_5 : (b:bool) (negb b)=true -> ~b=true. +Lemma bool_5 : forall b:bool, - b = true -> b <> true. Proof. - NewDestruct b; Intuition. + destruct b; intuition. Qed. -Lemma bool_6 : (b:bool) ~b=true -> (negb b)=true. +Lemma bool_6 : forall b:bool, b <> true -> - b = true. Proof. - NewDestruct b; Intuition. + destruct b; intuition. Qed. -Hints Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6. +Hint Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6. \ No newline at end of file diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index 61204ba30..ef48e6272 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -20,53 +20,54 @@ Section Bool_eq_dec. Variable beq : A -> A -> bool. - Variable beq_refl : (x:A)true=(beq x x). + Variable beq_refl : forall x:A, true = beq x x. - Variable beq_eq : (x,y:A)true=(beq x y)->x=y. + Variable beq_eq : forall x y:A, true = beq x y -> x = y. - Definition beq_eq_true : (x,y:A)x=y->true=(beq x y). + Definition beq_eq_true : forall x y:A, x = y -> true = beq x y. Proof. - Intros x y H. - Case H. - Apply beq_refl. + intros x y H. + case H. + apply beq_refl. Defined. - Definition beq_eq_not_false : (x,y:A)x=y->~false=(beq x y). + Definition beq_eq_not_false : forall x y:A, x = y -> false <> beq x y. Proof. - Intros x y e. - Rewrite <- beq_eq_true; Trivial; Discriminate. + intros x y e. + rewrite <- beq_eq_true; trivial; discriminate. Defined. - Definition beq_false_not_eq : (x,y:A)false=(beq x y)->~x=y. + Definition beq_false_not_eq : forall x y:A, false = beq x y -> x <> y. Proof. - Exact [x,y:A; H:(false=(beq x y)); e:(x=y)](beq_eq_not_false x y e H). + exact + (fun (x y:A) (H:false = beq x y) (e:x = y) => beq_eq_not_false x y e H). Defined. - Definition exists_beq_eq : (x,y:A){b:bool | b=(beq x y)}. + Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}. Proof. - Intros. - Exists (beq x y). - Constructor. + intros. + exists (beq x y). + constructor. Defined. - Definition not_eq_false_beq : (x,y:A)~x=y->false=(beq x y). + Definition not_eq_false_beq : forall x y:A, x <> y -> false = beq x y. Proof. - Intros x y H. - Symmetry. - Apply not_true_is_false. - Intro. - Apply H. - Apply beq_eq. - Symmetry. - Assumption. + intros x y H. + symmetry in |- *. + apply not_true_is_false. + intro. + apply H. + apply beq_eq. + symmetry in |- *. + assumption. Defined. - Definition eq_dec : (x,y:A){x=y}+{~x=y}. + Definition eq_dec : forall x y:A, {x = y} + {x <> y}. Proof. - Intros x y; Case (exists_beq_eq x y). - Intros b; Case b; Intro H. - Left; Apply beq_eq; Assumption. - Right; Apply beq_false_not_eq; Assumption. + intros x y; case (exists_beq_eq x y). + intros b; case b; intro H. + left; apply beq_eq; assumption. + right; apply beq_false_not_eq; assumption. Defined. -End Bool_eq_dec. +End Bool_eq_dec. \ No newline at end of file diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 792d6a067..86b59db26 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -12,9 +12,8 @@ Require Export Bool. Require Export Sumbool. -Require Arith. +Require Import Arith. -V7only [Import nat_scope.]. Open Local Scope nat_scope. (* @@ -82,64 +81,64 @@ de taille n dans les vecteurs de taille n en appliquant f terme Variable A : Set. -Inductive vector: nat -> Set := - | Vnil : (vector O) - | Vcons : (a:A) (n:nat) (vector n) -> (vector (S n)). +Inductive vector : nat -> Set := + | Vnil : vector 0 + | Vcons : forall (a:A) (n:nat), vector n -> vector (S n). -Definition Vhead : (n:nat) (vector (S n)) -> A. +Definition Vhead : forall n:nat, vector (S n) -> A. Proof. - Intros n v; Inversion v; Exact a. + intros n v; inversion v; exact a. Defined. -Definition Vtail : (n:nat) (vector (S n)) -> (vector n). +Definition Vtail : forall n:nat, vector (S n) -> vector n. Proof. - Intros n v; Inversion v; Exact H0. + intros n v; inversion v; exact H0. Defined. -Definition Vlast : (n:nat) (vector (S n)) -> A. +Definition Vlast : forall n:nat, vector (S n) -> A. Proof. - NewInduction n as [|n f]; Intro v. - Inversion v. - Exact a. + induction n as [| n f]; intro v. + inversion v. + exact a. - Inversion v. - Exact (f H0). + inversion v. + exact (f H0). Defined. -Definition Vconst : (a:A) (n:nat) (vector n). +Definition Vconst : forall (a:A) (n:nat), vector n. Proof. - NewInduction n as [|n v]. - Exact Vnil. + induction n as [| n v]. + exact Vnil. - Exact (Vcons a n v). + exact (Vcons a n v). Defined. -Lemma Vshiftout : (n:nat) (vector (S n)) -> (vector n). +Lemma Vshiftout : forall n:nat, vector (S n) -> vector n. Proof. - NewInduction n as [|n f]; Intro v. - Exact Vnil. + induction n as [| n f]; intro v. + exact Vnil. - Inversion v. - Exact (Vcons a n (f H0)). + inversion v. + exact (Vcons a n (f H0)). Defined. -Lemma Vshiftin : (n:nat) A -> (vector n) -> (vector (S n)). +Lemma Vshiftin : forall n:nat, A -> vector n -> vector (S n). Proof. - NewInduction n as [|n f]; Intros a v. - Exact (Vcons a O v). + induction n as [| n f]; intros a v. + exact (Vcons a 0 v). - Inversion v. - Exact (Vcons a (S n) (f a H0)). + inversion v. + exact (Vcons a (S n) (f a H0)). Defined. -Lemma Vshiftrepeat : (n:nat) (vector (S n)) -> (vector (S (S n))). +Lemma Vshiftrepeat : forall n:nat, vector (S n) -> vector (S (S n)). Proof. - NewInduction n as [|n f]; Intro v. - Inversion v. - Exact (Vcons a (1) v). + induction n as [| n f]; intro v. + inversion v. + exact (Vcons a 1 v). - Inversion v. - Exact (Vcons a (S (S n)) (f H0)). + inversion v. + exact (Vcons a (S (S n)) (f H0)). Defined. (* @@ -149,50 +148,50 @@ Proof. Save. *) -Lemma Vtrunc : (n,p:nat) (gt n p) -> (vector n) -> (vector (minus n p)). +Lemma Vtrunc : forall n p:nat, n > p -> vector n -> vector (n - p). Proof. - NewInduction p as [|p f]; Intros H v. - Rewrite <- minus_n_O. - Exact v. + induction p as [| p f]; intros H v. + rewrite <- minus_n_O. + exact v. - Apply (Vshiftout (minus n (S p))). + apply (Vshiftout (n - S p)). -Rewrite minus_Sn_m. -Apply f. -Auto with *. -Exact v. -Auto with *. +rewrite minus_Sn_m. +apply f. +auto with *. +exact v. +auto with *. Defined. -Lemma Vextend : (n,p:nat) (vector n) -> (vector p) -> (vector (plus n p)). +Lemma Vextend : forall n p:nat, vector n -> vector p -> vector (n + p). Proof. - NewInduction n as [|n f]; Intros p v v0. - Simpl; Exact v0. + induction n as [| n f]; intros p v v0. + simpl in |- *; exact v0. - Inversion v. - Simpl; Exact (Vcons a (plus n p) (f p H0 v0)). + inversion v. + simpl in |- *; exact (Vcons a (n + p) (f p H0 v0)). Defined. Variable f : A -> A. -Lemma Vunary : (n:nat)(vector n)->(vector n). +Lemma Vunary : forall n:nat, vector n -> vector n. Proof. - NewInduction n as [|n g]; Intro v. - Exact Vnil. + induction n as [| n g]; intro v. + exact Vnil. - Inversion v. - Exact (Vcons (f a) n (g H0)). + inversion v. + exact (Vcons (f a) n (g H0)). Defined. Variable g : A -> A -> A. -Lemma Vbinary : (n:nat)(vector n)->(vector n)->(vector n). +Lemma Vbinary : forall n:nat, vector n -> vector n -> vector n. Proof. - NewInduction n as [|n h]; Intros v v0. - Exact Vnil. + induction n as [| n h]; intros v v0. + exact Vnil. - Inversion v; Inversion v0. - Exact (Vcons (g a a0) n (h H0 H2)). + inversion v; inversion v0. + exact (Vcons (g a a0) n (h H0 H2)). Defined. End VECTORS. @@ -211,56 +210,58 @@ ATTENTION : Tous les d (ils ne travaillent que sur des vecteurs au moins de longueur un). *) -Definition Bvector := (vector bool). +Definition Bvector := vector bool. -Definition Bnil := (Vnil bool). +Definition Bnil := Vnil bool. -Definition Bcons := (Vcons bool). +Definition Bcons := Vcons bool. -Definition Bvect_true := (Vconst bool true). +Definition Bvect_true := Vconst bool true. -Definition Bvect_false := (Vconst bool false). +Definition Bvect_false := Vconst bool false. -Definition Blow := (Vhead bool). +Definition Blow := Vhead bool. -Definition Bhigh := (Vtail bool). +Definition Bhigh := Vtail bool. -Definition Bsign := (Vlast bool). +Definition Bsign := Vlast bool. -Definition Bneg := (Vunary bool negb). +Definition Bneg := Vunary bool negb. -Definition BVand := (Vbinary bool andb). +Definition BVand := Vbinary bool andb. -Definition BVor := (Vbinary bool orb). +Definition BVor := Vbinary bool orb. -Definition BVxor := (Vbinary bool xorb). +Definition BVxor := Vbinary bool xorb. -Definition BshiftL := [n:nat; bv : (Bvector (S n)); carry:bool] - (Bcons carry n (Vshiftout bool n bv)). +Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) := + Bcons carry n (Vshiftout bool n bv). -Definition BshiftRl := [n:nat; bv : (Bvector (S n)); carry:bool] - (Bhigh (S n) (Vshiftin bool (S n) carry bv)). +Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) := + Bhigh (S n) (Vshiftin bool (S n) carry bv). -Definition BshiftRa := [n:nat; bv : (Bvector (S n))] - (Bhigh (S n) (Vshiftrepeat bool n bv)). +Definition BshiftRa (n:nat) (bv:Bvector (S n)) := + Bhigh (S n) (Vshiftrepeat bool n bv). -Fixpoint BshiftL_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) := -Cases p of - | O => bv - | (S p') => (BshiftL n (BshiftL_iter n bv p') false) -end. +Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} : + Bvector (S n) := + match p with + | O => bv + | S p' => BshiftL n (BshiftL_iter n bv p') false + end. -Fixpoint BshiftRl_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) := -Cases p of - | O => bv - | (S p') => (BshiftRl n (BshiftRl_iter n bv p') false) -end. +Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} : + Bvector (S n) := + match p with + | O => bv + | S p' => BshiftRl n (BshiftRl_iter n bv p') false + end. -Fixpoint BshiftRa_iter [n:nat; bv:(Bvector (S n)); p:nat]:(Bvector (S n)) := -Cases p of - | O => bv - | (S p') => (BshiftRa n (BshiftRa_iter n bv p')) -end. +Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) {struct p} : + Bvector (S n) := + match p with + | O => bv + | S p' => BshiftRa n (BshiftRa_iter n bv p') + end. End BOOLEAN_VECTORS. - diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 28ef57eac..8a15e7624 100755 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -10,18 +10,22 @@ Set Implicit Arguments. -Definition ifdec : (A,B:Prop)(C:Set)({A}+{B})->C->C->C - := [A,B,C,H,x,y]if H then [_]x else [_]y. +Definition ifdec (A B:Prop) (C:Set) (H:{A} + {B}) (x y:C) : C := + if H then fun _ => x else fun _ => y. -Theorem ifdec_left : (A,B:Prop)(C:Set)(H:{A}+{B})~B->(x,y:C)(ifdec H x y)=x. -Intros; Case H; Auto. -Intro; Absurd B; Trivial. +Theorem ifdec_left : + forall (A B:Prop) (C:Set) (H:{A} + {B}), + ~ B -> forall x y:C, ifdec H x y = x. +intros; case H; auto. +intro; absurd B; trivial. Qed. -Theorem ifdec_right : (A,B:Prop)(C:Set)(H:{A}+{B})~A->(x,y:C)(ifdec H x y)=y. -Intros; Case H; Auto. -Intro; Absurd A; Trivial. +Theorem ifdec_right : + forall (A B:Prop) (C:Set) (H:{A} + {B}), + ~ A -> forall x y:C, ifdec H x y = y. +intros; case H; auto. +intro; absurd A; trivial. Qed. -Unset Implicit Arguments. +Unset Implicit Arguments. \ No newline at end of file diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 48180678f..bde404cf7 100755 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -8,42 +8,43 @@ (*i $Id$ i*) -Require Bool. +Require Import Bool. -Inductive IfProp [A,B:Prop] : bool-> Prop - := Iftrue : A -> (IfProp A B true) - | Iffalse : B -> (IfProp A B false). +Inductive IfProp (A B:Prop) : bool -> Prop := + | Iftrue : A -> IfProp A B true + | Iffalse : B -> IfProp A B false. -Hints Resolve Iftrue Iffalse : bool v62. +Hint Resolve Iftrue Iffalse: bool v62. -Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A. -NewDestruct 1; Intros; Auto with bool. -Case diff_true_false; Auto with bool. +Lemma Iftrue_inv : forall (A B:Prop) (b:bool), IfProp A B b -> b = true -> A. +destruct 1; intros; auto with bool. +case diff_true_false; auto with bool. Qed. -Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B. -NewDestruct 1; Intros; Auto with bool. -Case diff_true_false; Trivial with bool. +Lemma Iffalse_inv : + forall (A B:Prop) (b:bool), IfProp A B b -> b = false -> B. +destruct 1; intros; auto with bool. +case diff_true_false; trivial with bool. Qed. -Lemma IfProp_true : (A,B:Prop)(IfProp A B true) -> A. -Intros. -Inversion H. -Assumption. +Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A. +intros. +inversion H. +assumption. Qed. -Lemma IfProp_false : (A,B:Prop)(IfProp A B false) -> B. -Intros. -Inversion H. -Assumption. +Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B. +intros. +inversion H. +assumption. Qed. -Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B. -NewDestruct 1; Auto with bool. +Lemma IfProp_or : forall (A B:Prop) (b:bool), IfProp A B b -> A \/ B. +destruct 1; auto with bool. Qed. -Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}. -NewDestruct b; Intro H. -Left; Inversion H; Auto with bool. -Right; Inversion H; Auto with bool. -Qed. +Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}. +destruct b; intro H. +left; inversion H; auto with bool. +right; inversion H; auto with bool. +Qed. \ No newline at end of file diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 779969e6f..815bcda41 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -15,21 +15,23 @@ (** A boolean is either [true] or [false], and this is decidable *) -Definition sumbool_of_bool : (b:bool) {b=true}+{b=false}. +Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}. Proof. - NewDestruct b; Auto. + destruct b; auto. Defined. -Hints Resolve sumbool_of_bool : bool. +Hint Resolve sumbool_of_bool: bool. -Definition bool_eq_rec : (b:bool)(P:bool->Set) - ((b=true)->(P true))->((b=false)->(P false))->(P b). -NewDestruct b; Auto. +Definition bool_eq_rec : + forall (b:bool) (P:bool -> Set), + (b = true -> P true) -> (b = false -> P false) -> P b. +destruct b; auto. Defined. -Definition bool_eq_ind : (b:bool)(P:bool->Prop) - ((b=true)->(P true))->((b=false)->(P false))->(P b). -NewDestruct b; Auto. +Definition bool_eq_ind : + forall (b:bool) (P:bool -> Prop), + (b = true -> P true) -> (b = false -> P false) -> P b. +destruct b; auto. Defined. @@ -39,39 +41,38 @@ Defined. Section connectives. -Variables A,B,C,D : Prop. +Variables A B C D : Prop. -Hypothesis H1 : {A}+{B}. -Hypothesis H2 : {C}+{D}. +Hypothesis H1 : {A} + {B}. +Hypothesis H2 : {C} + {D}. -Definition sumbool_and : {A/\C}+{B\/D}. +Definition sumbool_and : {A /\ C} + {B \/ D}. Proof. -Case H1; Case H2; Auto. +case H1; case H2; auto. Defined. -Definition sumbool_or : {A\/C}+{B/\D}. +Definition sumbool_or : {A \/ C} + {B /\ D}. Proof. -Case H1; Case H2; Auto. +case H1; case H2; auto. Defined. -Definition sumbool_not : {B}+{A}. +Definition sumbool_not : {B} + {A}. Proof. -Case H1; Auto. +case H1; auto. Defined. End connectives. -Hints Resolve sumbool_and sumbool_or sumbool_not : core. +Hint Resolve sumbool_and sumbool_or sumbool_not: core. (** Any decidability function in type [sumbool] can be turned into a function returning a boolean with the corresponding specification: *) -Definition bool_of_sumbool : - (A,B:Prop) {A}+{B} -> { b:bool | if b then A else B }. +Definition bool_of_sumbool : + forall A B:Prop, {A} + {B} -> {b : bool | if b then A else B}. Proof. -Intros A B H. -Elim H; [ Intro; Exists true; Assumption - | Intro; Exists false; Assumption ]. +intros A B H. +elim H; [ intro; exists true; assumption | intro; exists false; assumption ]. Defined. -Implicits bool_of_sumbool. +Implicit Arguments bool_of_sumbool. \ No newline at end of file diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index 788025161..6487d08e9 100755 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -8,29 +8,31 @@ (*i $Id$ i*) -Require Arith. -Require Bool. +Require Import Arith. +Require Import Bool. -V7only [Import nat_scope.]. Open Local Scope nat_scope. -Definition zerob : nat->bool - := [n:nat]Cases n of O => true | (S _) => false end. +Definition zerob (n:nat) : bool := + match n with + | O => true + | S _ => false + end. -Lemma zerob_true_intro : (n:nat)(n=O)->(zerob n)=true. -NewDestruct n; [Trivial with bool | Inversion 1]. +Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true. +destruct n; [ trivial with bool | inversion 1 ]. Qed. -Hints Resolve zerob_true_intro : bool. +Hint Resolve zerob_true_intro: bool. -Lemma zerob_true_elim : (n:nat)(zerob n)=true->(n=O). -NewDestruct n; [Trivial with bool | Inversion 1]. +Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0. +destruct n; [ trivial with bool | inversion 1 ]. Qed. -Lemma zerob_false_intro : (n:nat)~(n=O)->(zerob n)=false. -NewDestruct n; [NewDestruct 1; Auto with bool | Trivial with bool]. +Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false. +destruct n; [ destruct 1; auto with bool | trivial with bool ]. Qed. -Hints Resolve zerob_false_intro : bool. +Hint Resolve zerob_false_intro: bool. -Lemma zerob_false_elim : (n:nat)(zerob n)=false -> ~(n=O). -NewDestruct n; [Intro H; Inversion H | Auto with bool]. -Qed. +Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0. +destruct n; [ intro H; inversion H | auto with bool ]. +Qed. \ No newline at end of file -- cgit v1.2.3