From a07627c4567ac28e7903755a955665dc8e347e9e Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 12 Apr 2001 04:58:24 +0000
Subject: Ajout de l'egalite de John Major

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1580 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile              |  3 ++-
 TODO                  |  3 +++
 theories/Logic/JMeq.v | 37 +++++++++++++++++++++++++++++++++++++
 3 files changed, 42 insertions(+), 1 deletion(-)
 create mode 100644 theories/Logic/JMeq.v

diff --git a/Makefile b/Makefile
index 1f5fe73077..67f50a1529 100644
--- a/Makefile
+++ b/Makefile
@@ -340,7 +340,8 @@ clean::
 LOGICVO=theories/Logic/Classical.vo          theories/Logic/Classical_Type.vo \
       theories/Logic/Classical_Pred_Set.vo   theories/Logic/Eqdep.vo          \
       theories/Logic/Classical_Pred_Type.vo  theories/Logic/Classical_Prop.vo \
-      theories/Logic/Eqdep_dec.vo            theories/Logic/Decidable.vo
+      theories/Logic/Eqdep_dec.vo            theories/Logic/Decidable.vo \
+      theories/Logic/JMeq.v
 
 ARITHVO=theories/Arith/Arith.vo         theories/Arith/Gt.vo          \
 	theories/Arith/Between.vo       theories/Arith/Le.vo          \
diff --git a/TODO b/TODO
index 528319468b..dc40c02a26 100644
--- a/TODO
+++ b/TODO
@@ -45,3 +45,6 @@ Doc:
   + Set Printing Coercions
 
 
+- Suggestions de la formation
+	Dans le Intros pattern on pourrait interpreter les _ 
+comme des hypotheses sur lesquelles on ferait Clear immediatement
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
new file mode 100644
index 0000000000..2f8eda34f5
--- /dev/null
+++ b/theories/Logic/JMeq.v
@@ -0,0 +1,37 @@
+(*s John Major's Equality - C. Mc Bride *)
+
+Set Implicit Arguments.
+
+Inductive JMeq [A:Set;x:A] : (B:Set)B->Prop := 
+	JMeq_refl : (JMeq x x).
+
+Hints Resolve JMeq_refl.
+
+Lemma JMeq_sym : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x).
+Destruct 1; Trivial.
+Save.
+
+Hints Immediate JMeq_sym.
+
+Lemma JMeq_trans : (A,B,C:Set)(x:A)(y:B)(z:C)
+	(JMeq x y)->(JMeq y z)->(JMeq x z).
+Destruct 1; Trivial.
+Save.
+
+Axiom JMeq_eq : (A:Set)(x,y:A)(JMeq x y)->(x=y).
+
+Lemma JMeq_eq_ind : (A:Set)(x,y:A)(P:A->Prop)(P x)->(JMeq x y)->(P y).
+Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial.
+Save.
+
+Lemma JMeq_eq_rec : (A:Set)(x,y:A)(P:A->Set)(P x)->(JMeq x y)->(P y).
+Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial.
+Save.
+
+Lemma JMeq_eq_ind_r : (A:Set)(x,y:A)(P:A->Prop)(P y)->(JMeq x y)->(P x).
+Intros A x y P H H'; Case JMeq_eq with 1:=(JMeq_sym H'); Trivial.
+Save.
+
+Lemma JMeq_eq_rec_r : (A:Set)(x,y:A)(P:A->Set)(P y)->(JMeq x y)->(P x).
+Intros A x y P H H'; Case JMeq_eq with 1:=(JMeq_sym H'); Trivial.
+Save.
-- 
cgit v1.2.3