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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
(************************************************************************)
(* 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 9077 2006-08-24 08:44:32Z herbelin $ i*)
(** John Major's Equality as proposed by Conor McBride
Reference:
[McBride] Elimination with a Motive, Proceedings of TYPES 2000,
LNCS 2277, pp 197-216, 2002.
*)
Set Implicit Arguments.
Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
JMeq_refl : JMeq x x.
Reset JMeq_rect.
Hint Resolve JMeq_refl.
Lemma sym_JMeq : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
destruct 1; trivial.
Qed.
Hint Immediate sym_JMeq.
Lemma trans_JMeq :
forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
destruct 1; 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.
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.
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.
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.
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.
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.
Qed.
(** [JMeq] is equivalent to [(eq_dep Type [X]X)] *)
Require Import Eqdep.
Lemma JMeq_eq_dep :
forall (A B:Type) (x:A) (y:B), JMeq x y -> eq_dep Type (fun X => X) A x B y.
Proof.
destruct 1.
apply eq_dep_intro.
Qed.
Lemma eq_dep_JMeq :
forall (A B:Type) (x:A) (y:B), eq_dep Type (fun X => X) A x B y -> JMeq x y.
Proof.
destruct 1.
apply JMeq_refl.
Qed.
|
