diff options
| author |  courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 13:44:44 +0000 |
|---|---|---|
| committer | courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 13:44:44 +0000 |
| commit | 6c892e6e04be39385e2338b973bf108a05836153 (patch) | |
| tree | aa535481158990b77f1e002ad7df101c1ebe571b /theories/Logic/JMeq.v | |
| parent | d619e901add481f1660d098e86bd3dcf02fc82e2 (diff) | |
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
Diffstat (limited to 'theories/Logic/JMeq.v')
| -rw-r--r-- | theories/Logic/JMeq.v | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index a44edfbf2..47a20a63d 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. |