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.