diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /theories7/Bool/BoolEq.v |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories7/Bool/BoolEq.v')
-rw-r--r-- | theories7/Bool/BoolEq.v | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/theories7/Bool/BoolEq.v b/theories7/Bool/BoolEq.v new file mode 100644 index 00000000..b670dbdd --- /dev/null +++ b/theories7/Bool/BoolEq.v @@ -0,0 +1,72 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: BoolEq.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*) +(* Cuihtlauac Alvarado - octobre 2000 *) + +(** Properties of a boolean equality *) + + +Require Export Bool. + +Section Bool_eq_dec. + + Variable A : Set. + + Variable beq : A -> A -> bool. + + Variable beq_refl : (x:A)true=(beq x x). + + Variable beq_eq : (x,y:A)true=(beq x y)->x=y. + + Definition beq_eq_true : (x,y:A)x=y->true=(beq x y). + Proof. + Intros x y H. + Case H. + Apply beq_refl. + Defined. + + Definition beq_eq_not_false : (x,y:A)x=y->~false=(beq x y). + Proof. + 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. + Proof. + Exact [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)}. + Proof. + Intros. + Exists (beq x y). + Constructor. + Defined. + + Definition not_eq_false_beq : (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. + Defined. + + Definition eq_dec : (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. + Defined. + +End Bool_eq_dec. |