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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: JMeq.v 13323 2010-07-24 15:57:30Z 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.
Unset Elimination Schemes.
Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
JMeq_refl : JMeq x x.
Set Elimination Schemes.
Hint Resolve JMeq_refl.
Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
Proof.
destruct 1; trivial.
Qed.
Hint Immediate JMeq_sym.
Lemma JMeq_trans :
forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
Proof.
destruct 2; trivial.
Qed.
Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop),
P x -> forall y, JMeq x y -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.
Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set),
P x -> forall y, JMeq x y -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.
Lemma JMeq_rect : forall (A:Type) (x:A) (P:A->Type),
P x -> forall y, JMeq x y -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
Qed.
Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop),
P x -> forall y, JMeq y x -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.
Lemma JMeq_rec_r : forall (A:Type) (x:A) (P:A -> Set),
P x -> forall y, JMeq y x -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.
Lemma JMeq_rect_r : forall (A:Type) (x:A) (P:A -> Type),
P x -> forall y, JMeq y x -> P y.
Proof.
intros A x P H y H'; case JMeq_eq with (1 := JMeq_sym H'); trivial.
Qed.
Lemma JMeq_congr :
forall (A:Type) (x:A) (B:Type) (f:A->B) (y:A), JMeq x y -> f x = f y.
Proof.
intros A x B f y H; case JMeq_eq with (1 := H); trivial.
Qed.
(** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *)
Require Import Eqdep.
Lemma JMeq_eq_dep_id :
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_id_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.
(** [eq_dep U P p x q y] is strictly finer than [JMeq (P p) x (P q) y] *)
Lemma eq_dep_JMeq :
forall U P p x q y, eq_dep U P p x q y -> JMeq x y.
Proof.
destruct 1.
apply JMeq_refl.
Qed.
Lemma eq_dep_strictly_stronger_JMeq :
exists U, exists P, exists p, exists q, exists x, exists y,
JMeq x y /\ ~ eq_dep U P p x q y.
Proof.
exists bool. exists (fun _ => True). exists true. exists false.
exists I. exists I.
split.
trivial.
intro H.
assert (true=false) by (destruct H; reflexivity).
discriminate.
Qed.
(** However, when the dependencies are equal, [JMeq (P p) x (P q) y]
is as strong as [eq_dep U P p x q y] (this uses [JMeq_eq]) *)
Lemma JMeq_eq_dep :
forall U (P:U->Prop) p q (x:P p) (y:P q),
p = q -> JMeq x y -> eq_dep U P p x q y.
Proof.
intros.
destruct H.
apply JMeq_eq in H0 as ->.
reflexivity.
Qed.
(* Compatibility *)
Notation sym_JMeq := JMeq_sym (only parsing).
Notation trans_JMeq := JMeq_trans (only parsing).
|
