summaryrefslogtreecommitdiff
path: root/theories/Logic/JMeq.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Logic/JMeq.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Logic/JMeq.v')
-rw-r--r--theories/Logic/JMeq.v75
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).