diff options
| -rwxr-xr-x | theories/Logic/Eqdep.v | 16 | ||||
| -rw-r--r-- | theories/Logic/JMeq.v | 16 |
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. |