Comparaison JMeq/eq_dep

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

1 files changed, 26 insertions, 4 deletions

diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index a2e156b9f..1211d3327 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -68,20 +68,42 @@ Lemma JMeq_rect_r :
 intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
 Qed.
 
-(** [JMeq] is equivalent to [(eq_dep Type [X]X)] *)
+(** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *)
 
 Require Import Eqdep.
 
-Lemma JMeq_eq_dep :
+Lemma JMeq_eq_dep_id :
  forall (A B:Type) (x:A) (y:B), JMeq x y -> eq_dep Type (fun X => X) A x B y.
 Proof.
 destruct 1.
 apply eq_dep_intro.
 Qed.
 
-Lemma eq_dep_JMeq :
+Lemma eq_dep_id_JMeq :
  forall (A B:Type) (x:A) (y:B), eq_dep Type (fun X => X) A x B y -> JMeq x y.
 Proof.
 destruct 1.
-apply JMeq_refl. 
+apply JMeq_refl.
+Qed.
+
+(** [eq_dep U P p x q y] is strictly finer than [JMeq (P p) x (P q) y] *)
+
+Lemma eq_dep_JMeq :
+ forall U P p x q y, eq_dep U P p x q y -> JMeq x y.
+Proof.
+destruct 1.
+apply JMeq_refl.
+Qed.
+
+Lemma eq_dep_strictly_stronger_JMeq :
+ exists U, exists P, exists p, exists q, exists x, exists y,
+  JMeq x y /\ ~ eq_dep U P p x q y.
+Proof.
+exists bool. exists (fun _ => True). exists true. exists false.
+exists I. exists I.
+split.
+trivial.
+intro H.
+assert (true=false) by (destruct H; reflexivity).
+discriminate.
 Qed.