diff options
author | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-12 04:58:24 +0000 |
---|---|---|
committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-12 04:58:24 +0000 |
commit | a07627c4567ac28e7903755a955665dc8e347e9e (patch) | |
tree | c32660e3d17fb2dc739906c08dbc740785e323a5 /theories/Logic/JMeq.v | |
parent | 1cf49df11855525e05f65587be7198ecfdebc9e7 (diff) |
Ajout de l'egalite de John Major
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1580 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/JMeq.v')
-rw-r--r-- | theories/Logic/JMeq.v | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v new file mode 100644 index 000000000..2f8eda34f --- /dev/null +++ b/theories/Logic/JMeq.v @@ -0,0 +1,37 @@ +(*s John Major's Equality - C. Mc Bride *) + +Set Implicit Arguments. + +Inductive JMeq [A:Set;x:A] : (B:Set)B->Prop := + JMeq_refl : (JMeq x x). + +Hints Resolve JMeq_refl. + +Lemma JMeq_sym : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x). +Destruct 1; Trivial. +Save. + +Hints Immediate JMeq_sym. + +Lemma JMeq_trans : (A,B,C:Set)(x:A)(y:B)(z:C) + (JMeq x y)->(JMeq y z)->(JMeq x z). +Destruct 1; Trivial. +Save. + +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). +Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial. +Save. + +Lemma JMeq_eq_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. +Save. + +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. +Save. + +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. +Save. |