From 6c892e6e04be39385e2338b973bf108a05836153 Mon Sep 17 00:00:00 2001 From: courant Date: Thu, 14 Nov 2002 13:44:44 +0000 Subject: JMeq now treated as an equality by tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3232 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Logic/JMeq.v | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'theories/Logic') diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index a44edfbf27..47a20a63d9 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -14,34 +14,35 @@ Set Implicit Arguments. Inductive JMeq [A:Set;x:A] : (B:Set)B->Prop := JMeq_refl : (JMeq x x). +Reset JMeq_ind. Hints Resolve JMeq_refl. -Lemma JMeq_sym : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x). +Lemma sym_JMeq : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x). NewDestruct 1; Trivial. Qed. -Hints Immediate JMeq_sym. +Hints Immediate sym_JMeq. -Lemma JMeq_trans : (A,B,C:Set)(x:A)(y:B)(z:C) +Lemma trans_JMeq : (A,B,C:Set)(x:A)(y:B)(z:C) (JMeq x y)->(JMeq y z)->(JMeq x z). NewDestruct 1; Trivial. Qed. Axiom JMeq_eq : (A:Set)(x,y:A)(JMeq x y)->(x=y). -Lemma JMeq_eq_ind : (A:Set)(x,y:A)(P:A->Prop)(P x)->(JMeq x y)->(P y). +Lemma JMeq_ind : (A:Set)(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. Qed. -Lemma JMeq_eq_rec : (A:Set)(x,y:A)(P:A->Set)(P x)->(JMeq x y)->(P y). +Lemma JMeq_rec : (A:Set)(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. Qed. -Lemma JMeq_eq_ind_r : (A:Set)(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:=(JMeq_sym H'); Trivial. +Lemma JMeq_ind_r : (A:Set)(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. Qed. -Lemma JMeq_eq_rec_r : (A:Set)(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:=(JMeq_sym H'); Trivial. +Lemma JMeq_rec_r : (A:Set)(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. Qed. -- cgit v1.2.3