diff options
Diffstat (limited to 'theories/Logic/JMeq.v')
| -rw-r--r-- | theories/Logic/JMeq.v | 75 |
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). |