diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-17 11:30:23 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-04-17 11:30:23 +0000 |
commit | cc1be0bf512b421336e81099aa6906ca47e4257a (patch) | |
tree | c25fa8ed965729d7a85efa3b3292fdf7f442963d /theories/Bool/Bool.v | |
parent | ebf9aa9f97ef0d49ed1b799c9213f78efad4fec7 (diff) |
Uniformisation (Qed/Save et Implicits Arguments)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Bool/Bool.v')
-rwxr-xr-x | theories/Bool/Bool.v | 102 |
1 files changed, 51 insertions, 51 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 1942ca6b3..cfd6f656a 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -23,12 +23,12 @@ Hints Unfold Is_true : bool. Lemma Is_true_eq_left : (x:bool)x=true -> (Is_true x). Proof. Intros; Rewrite H; Auto with bool. -Save. +Qed. Lemma Is_true_eq_right : (x:bool)true=x -> (Is_true x). Proof. Intros; Rewrite <- H; Auto with bool. -Save. +Qed. Hints Immediate Is_true_eq_right Is_true_eq_left : bool. @@ -40,7 +40,7 @@ Lemma diff_true_false : ~true=false. Goal. Unfold not; Intro contr; Change (Is_true false). Elim contr; Simpl; Trivial with bool. -Save. +Qed. Hints Resolve diff_true_false : bool v62. Lemma diff_false_true : ~false=true. @@ -48,12 +48,12 @@ Goal. Red; Intros H; Apply diff_true_false. Symmetry. Assumption. -Save. +Qed. Hints 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. -Save. +Qed. Hints Resolve eq_true_false_abs : bool. Lemma not_true_is_false : (b:bool)~b=true->b=false. @@ -63,7 +63,7 @@ Red in H; Elim H. Reflexivity. Intros abs. Reflexivity. -Save. +Qed. Lemma not_false_is_true : (b:bool)~b=false->b=true. NewDestruct b. @@ -71,7 +71,7 @@ Intros. Reflexivity. Intro H; Red in H; Elim H. Reflexivity. -Save. +Qed. (**********************) (** Order on booleans *) @@ -99,19 +99,19 @@ Definition eqb : bool->bool->bool := Lemma eqb_refl : (x:bool)(Is_true (eqb x x)). NewDestruct x; Simpl; Auto with bool. -Save. +Qed. Lemma eqb_eq : (x,y:bool)(Is_true (eqb x y))->x=y. NewDestruct x; NewDestruct y; Simpl; Tauto. -Save. +Qed. Lemma Is_true_eq_true : (x:bool) (Is_true x) -> x=true. NewDestruct x; Simpl; Tauto. -Save. +Qed. Lemma Is_true_eq_true2 : (x:bool) x=true -> (Is_true x). NewDestruct x; Simpl; Auto with bool. -Save. +Qed. Lemma eqb_subst : (P:bool->Prop)(b1,b2:bool)(eqb b1 b2)=true->(P b1)->(P b2). @@ -127,19 +127,19 @@ Case b2. Intros H. Inversion_clear H. Trivial with bool. -Save. +Qed. Lemma eqb_reflx : (b:bool)(eqb b b)=true. Intro b. Case b. Trivial with bool. Trivial with bool. -Save. +Qed. Lemma eqb_prop : (a,b:bool)(eqb a b)=true -> a=b. NewDestruct a; NewDestruct b; Simpl; Intro; Discriminate H Orelse Reflexivity. -Save. +Qed. (************************) @@ -180,12 +180,12 @@ Definition negb := [b:bool]Cases b of Lemma negb_intro : (b:bool)b=(negb (negb b)). Goal. Induction b; Reflexivity. -Save. +Qed. Lemma negb_elim : (b:bool)(negb (negb b))=b. Goal. Induction b; Reflexivity. -Save. +Qed. Lemma negb_orb : (b1,b2:bool) (negb (orb b1 b2)) = (andb (negb b1) (negb b2)). @@ -202,24 +202,24 @@ Qed. Lemma negb_sym : (b,b':bool)(b'=(negb b))->(b=(negb b')). Goal. Induction b; Induction b'; Intros; Simpl; Trivial with bool. -Save. +Qed. Lemma no_fixpoint_negb : (b:bool)~(negb b)=b. Goal. Induction b; Simpl; Unfold not; Intro; Apply diff_true_false; Auto with bool. -Save. +Qed. Lemma eqb_negb1 : (b:bool)(eqb (negb b) b)=false. NewDestruct b. Trivial with bool. Trivial with bool. -Save. +Qed. Lemma eqb_negb2 : (b:bool)(eqb b (negb b))=false. NewDestruct b. Trivial with bool. Trivial with bool. -Save. +Qed. Lemma if_negb : (A:Set) (b:bool) (x,y:A) (if (negb b) then x else y)=(if b then y else x). @@ -235,12 +235,12 @@ Qed. Lemma orb_prop : (a,b:bool)(orb a b)=true -> (a = true)\/(b = true). Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool. -Save. +Qed. Lemma orb_prop2 : (a,b:bool)(Is_true (orb a b)) -> (Is_true a)\/(Is_true b). Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool. -Save. +Qed. Lemma orb_true_intro : (b1,b2:bool)(b1=true)\/(b2=true)->(orb b1 b2)=true. @@ -248,37 +248,37 @@ NewDestruct b1; Auto with bool. NewDestruct 1; Intros. Elim diff_true_false; Auto with bool. Rewrite H; Trivial with bool. -Save. +Qed. Hints Resolve orb_true_intro : bool v62. Lemma orb_b_true : (b:bool)(orb b true)=true. Auto with bool. -Save. +Qed. Hints Resolve orb_b_true : bool v62. Lemma orb_true_b : (b:bool)(orb true b)=true. Trivial with bool. -Save. +Qed. Lemma orb_true_elim : (b1,b2:bool)(orb b1 b2)=true -> {b1=true}+{b2=true}. NewDestruct b1; Simpl; Auto with bool. -Save. +Qed. 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. -Save. +Qed. Hints Resolve orb_false_intro : bool v62. Lemma orb_b_false : (b:bool)(orb b false)=b. Proof. NewDestruct b; Trivial with bool. -Save. +Qed. Hints Resolve orb_b_false : bool v62. Lemma orb_false_b : (b:bool)(orb false b)=b. Proof. NewDestruct b; Trivial with bool. -Save. +Qed. Hints Resolve orb_false_b : bool v62. Lemma orb_false_elim : @@ -289,23 +289,23 @@ Proof. NewDestruct b2. Intros; Elim diff_true_false; Auto with bool. Auto with bool. -Save. +Qed. Lemma orb_neg_b : (b:bool)(orb b (negb b))=true. Proof. NewDestruct b; Reflexivity. -Save. +Qed. Hints Resolve orb_neg_b : bool v62. Lemma orb_sym : (b1,b2:bool)(orb b1 b2)=(orb b2 b1). NewDestruct b1; NewDestruct b2; Reflexivity. -Save. +Qed. Lemma orb_assoc : (b1,b2,b3:bool)(orb b1 (orb b2 b3))=(orb (orb b1 b2) b3). Proof. NewDestruct b1; NewDestruct b2; NewDestruct b3; Reflexivity. -Save. +Qed. Hints Resolve orb_sym orb_assoc orb_b_false orb_false_b : bool v62. @@ -319,7 +319,7 @@ Lemma andb_prop : Proof. Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool. -Save. +Qed. Hints Resolve andb_prop : bool v62. Definition andb_true_eq : (a,b:bool) true = (andb a b) -> true = a /\ true = b. @@ -332,67 +332,67 @@ Lemma andb_prop2 : Proof. Induction a; Induction b; Simpl; Try (Intro H;Discriminate H); Auto with bool. -Save. +Qed. Hints Resolve andb_prop2 : bool v62. Lemma andb_true_intro : (b1,b2:bool)(b1=true)/\(b2=true)->(andb b1 b2)=true. Proof. NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool. -Save. +Qed. Hints Resolve andb_true_intro : bool v62. Lemma andb_true_intro2 : (b1,b2:bool)(Is_true b1)->(Is_true b2)->(Is_true (andb b1 b2)). Proof. NewDestruct b1; NewDestruct b2; Simpl; Tauto. -Save. +Qed. Hints 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. -Save. +Qed. Lemma andb_false_intro2 : (b1,b2:bool)(b2=false)->(andb b1 b2)=false. NewDestruct b1; NewDestruct b2; Simpl; Tauto Orelse Auto with bool. -Save. +Qed. Lemma andb_b_false : (b:bool)(andb b false)=false. NewDestruct b; Auto with bool. -Save. +Qed. Lemma andb_false_b : (b:bool)(andb false b)=false. Trivial with bool. -Save. +Qed. Lemma andb_b_true : (b:bool)(andb b true)=b. NewDestruct b; Auto with bool. -Save. +Qed. Lemma andb_true_b : (b:bool)(andb true b)=b. Trivial with bool. -Save. +Qed. Lemma andb_false_elim : (b1,b2:bool)(andb b1 b2)=false -> {b1=false}+{b2=false}. NewDestruct b1; Simpl; Auto with bool. -Save. +Qed. Hints Resolve andb_false_elim : bool v62. Lemma andb_neg_b : (b:bool)(andb b (negb b))=false. NewDestruct b; Reflexivity. -Save. +Qed. Hints Resolve andb_neg_b : bool v62. Lemma andb_sym : (b1,b2:bool)(andb b1 b2)=(andb b2 b1). NewDestruct b1; NewDestruct b2; Reflexivity. -Save. +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. -Save. +Qed. Hints Resolve andb_sym andb_assoc : bool v62. @@ -469,22 +469,22 @@ Qed. 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. -Save. +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. -Save. +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. -Save. +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. -Save. +Qed. Lemma absoption_andb : (b1,b2:bool) (andb b1 (orb b1 b2)) = b1. |