Renommage K; equivalence JMeq et eq_dep sur Type

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3879 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 29 insertions, 3 deletions

diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index 25ead98971..40a50837dc 100755
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -110,19 +110,29 @@ Elim p1 using eq_indd.
 Apply eq_dep_intro.
 Qed.
 
-(** Streicher axiom K is a direct instance of UIP *)
+(** Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *)
 
-Lemma Streicher_K : (U:Type)(x:U)(p:x=x)p=(refl_equal U x).
+Lemma UIP_refl : (U:Type)(x:U)(p:x=x)p=(refl_equal U x).
 Proof.
 Intros; Apply UIP.
 Qed.
 
+(** Streicher axiom K is a direct consequence of Uniqueness of
+    Reflexive Identity Proofs *)
+
+Lemma Streicher_K : (U:Type)(x:U)(P:x=x->Prop)
+  (P (refl_equal ? x))->(p:x=x)(P p).
+Proof.
+Intros; Rewrite UIP_refl; Assumption.
+Qed.
+
 (** We finally recover eq_rec_eq (alternatively eq_rect_eq) from K *)
 
 Lemma eq_rec_eq : (U:Type)(P:U->Set)(p:U)(x:(P p))(h:p=p)
   x=(eq_rec U p P x p h).
+Proof.
 Intros.
-Rewrite Streicher_K with p:=h.
+Apply Streicher_K with p:=h.
 Reflexivity.
 Qed.
 
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 47a20a63d9..04c62b3a1f 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -46,3 +46,19 @@ Qed.
 Lemma JMeq_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:=(sym_JMeq H'); Trivial.
 Qed.
+
+(** [JMeq] is equivalent to [(eq_dep Set [X]X)] *)
+
+Require Eqdep.
+
+Lemma JMeq_eq_dep : (A,B:Set)(x:A)(y:B)(JMeq x y)->(eq_dep Set [X]X A x B y).
+Proof.
+NewDestruct 1.
+Apply eq_dep_intro.
+Qed.
+
+Lemma eq_dep_JMeq : (A,B:Set)(x:A)(y:B)(eq_dep Set [X]X A x B y)->(JMeq x y).
+Proof.
+NewDestruct 1.
+Apply JMeq_refl. 
+Qed.