Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 55 insertions, 20 deletions

diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index c3573ac3..fc4555a4 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: JMeq.v 9849 2007-05-22 20:40:04Z herbelin $ i*)
+(*i $Id$ i*)
 
 (** John Major's Equality as proposed by Conor McBride
 
@@ -28,44 +28,61 @@ Set Elimination Schemes.
 
 Hint Resolve JMeq_refl.
 
-Lemma sym_JMeq : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
+Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
+Proof.
 destruct 1; trivial.
 Qed.
 
-Hint Immediate sym_JMeq.
+Hint Immediate JMeq_sym.
 
-Lemma trans_JMeq :
+Lemma JMeq_trans :
  forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
-destruct 1; trivial.
+Proof.
+destruct 2; trivial.
 Qed.
 
 Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
 
-Lemma JMeq_ind : forall (A:Type) (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.
+Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop),
+  P x -> forall y, JMeq x y -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
-Lemma JMeq_rec : forall (A:Type) (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.
+Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set),
+  P x -> forall y, JMeq x y -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
-Lemma JMeq_rect : forall (A:Type) (x y:A) (P:A->Type), P x -> JMeq x y -> P y.
-intros A x y P H H'; case JMeq_eq with (1 := H'); trivial.
+Lemma JMeq_rect : forall (A:Type) (x:A) (P:A->Type),
+  P x -> forall y, JMeq x y -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
+Qed.
+
+Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop),
+   P x -> forall y, JMeq y x -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
 Qed.
 
-Lemma JMeq_ind_r :
- forall (A:Type) (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 := sym_JMeq H'); trivial.
+Lemma JMeq_rec_r : forall (A:Type) (x:A) (P:A -> Set),
+   P x -> forall y, JMeq y x -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
 Qed.
 
-Lemma JMeq_rec_r :
- forall (A:Type) (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.
+Lemma JMeq_rect_r : forall (A:Type) (x:A) (P:A -> Type),
+   P x -> forall y, JMeq y x -> P y.
+Proof.
+intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
 Qed.
 
-Lemma JMeq_rect_r :
- forall (A:Type) (x y:A) (P:A -> Type), P y -> JMeq x y -> P x.
-intros A x y P H H'; case JMeq_eq with (1 := sym_JMeq H'); trivial.
+Lemma JMeq_congr :
+ forall (A:Type) (x:A) (B:Type) (f:A->B) (y:A), JMeq x y -> f x = f y.
+Proof.
+intros A x B f y H; case JMeq_eq with (1 := H); trivial.
 Qed.
 
 (** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *)
@@ -107,3 +124,21 @@ intro H.
 assert (true=false) by (destruct H; reflexivity).
 discriminate.
 Qed.
+
+(** However, when the dependencies are equal, [JMeq (P p) x (P q) y]
+    is as strong as [eq_dep U P p x q y] (this uses [JMeq_eq]) *)
+
+Lemma JMeq_eq_dep : 
+  forall U (P:U->Prop) p q (x:P p) (y:P q), 
+  p = q -> JMeq x y -> eq_dep U P p x q y.
+Proof.
+intros.
+destruct H.
+apply JMeq_eq in H0 as ->.
+reflexivity.
+Qed.
+
+
+(* Compatibility *)
+Notation sym_JMeq := JMeq_sym (only parsing).
+Notation trans_JMeq := JMeq_trans (only parsing).