1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: JMeq.v,v 1.1.2.1 2004/07/16 19:31:29 herbelin Exp $ i*)
(** John Major's Equality as proposed by C. Mc Bride *)
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 sym_JMeq : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x).
NewDestruct 1; Trivial.
Qed.
Hints Immediate sym_JMeq.
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_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_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_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_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.
(** [JMeq] is equivalent to [(eq_dep Set [X]X)] *)
Require Eqdep.
Lemma JMeq_eq_dep : (A,B:Set)(x:A)(y:B)(JMeq x y)->(eq_dep Set [X]X A x B y).
Proof.
NewDestruct 1.
Apply eq_dep_intro.
Qed.
Lemma eq_dep_JMeq : (A,B:Set)(x:A)(y:B)(eq_dep Set [X]X A x B y)->(JMeq x y).
Proof.
NewDestruct 1.
Apply JMeq_refl.
Qed.
|
