From f9f35dc36f5249a2de18005ab59ae934e0fa7075 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 3 Aug 2009 20:50:11 +0000 Subject: Added "etransitivity". Added support for "injection" and "discriminate" on JMeq. Seized the opportunity to update coqlib.ml and to rely more on it for finding the equality lemmas. Fixed typos in coqcompat.ml. Propagated symmetry convert_concl fix to transitivity (see 11521). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Logic/JMeq.v | 59 ++++++++++++++++++++++++++++++++++----------------- 1 file changed, 40 insertions(+), 19 deletions(-) (limited to 'theories') diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 1211d3327..7d9e11296 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -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 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_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_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_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_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 B:Type) (f:A->B) (x y:A), JMeq x y -> JMeq (f x) (f y). +Proof. +intros A B f x y H; case JMeq_eq with (1 := H); trivial. Qed. (** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *) @@ -107,3 +124,7 @@ intro H. assert (true=false) by (destruct H; reflexivity). discriminate. Qed. + +(* Compatibility *) +Notation sym_JMeq := JMeq_sym (only parsing). +Notation trans_JMeq := JMeq_trans (only parsing). -- cgit v1.2.3