diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-29 17:28:49 +0000 |
commit | 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 (patch) | |
tree | 77c0021911e3696a8c98e35a51840800db4be2a9 /theories/Bool/BoolEq.v | |
parent | 9058fb97426307536f56c3e7447be2f70798e081 (diff) |
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
Diffstat (limited to 'theories/Bool/BoolEq.v')
-rw-r--r-- | theories/Bool/BoolEq.v | 61 |
1 files changed, 31 insertions, 30 deletions
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 |