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
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
|
(************************************************************************)
(* 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$ i*)
(** We prove that there is only one proof of [x=x], i.e [refl_equal x].
This holds if the equality upon the set of [x] is decidable.
A corollary of this theorem is the equality of the right projections
of two equal dependent pairs.
Author: Thomas Kleymann |<tms@dcs.ed.ac.uk>| in Lego
adapted to Coq by B. Barras
Credit: Proofs up to [K_dec] follow an outline by Michael Hedberg
Table of contents:
1. Streicher's K and injectivity of dependent pair hold on decidable types
1.1. Definition of the functor that builds properties of dependent equalities
from a proof of decidability of equality for a set in Type
1.2. Definition of the functor that builds properties of dependent equalities
from a proof of decidability of equality for a set in Set
*)
(************************************************************************)
(** * Streicher's K and injectivity of dependent pair hold on decidable types *)
Set Implicit Arguments.
Section EqdepDec.
Variable A : Type.
Let comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' :=
eq_ind _ (fun a => a = y') eq2 _ eq1.
Remark trans_sym_eq : forall (x y:A) (u:x = y), comp u u = refl_equal y.
Proof.
intros.
case u; trivial.
Qed.
Variable eq_dec : forall x y:A, x = y \/ x <> y.
Variable x : A.
Let nu (y:A) (u:x = y) : x = y :=
match eq_dec x y with
| or_introl eqxy => eqxy
| or_intror neqxy => False_ind _ (neqxy u)
end.
Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v.
intros.
unfold nu in |- *.
case (eq_dec x y); intros.
reflexivity.
case n; trivial.
Qed.
Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (refl_equal x)) v.
Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u.
Proof.
intros.
case u; unfold nu_inv in |- *.
apply trans_sym_eq.
Qed.
Theorem eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.
Proof.
intros.
elim nu_left_inv with (u := p1).
elim nu_left_inv with (u := p2).
elim nu_constant with y p1 p2.
reflexivity.
Qed.
Theorem K_dec :
forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p.
Proof.
intros.
elim eq_proofs_unicity with x (refl_equal x) p.
trivial.
Qed.
(** The corollary *)
Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x :=
match exP with
| ex_intro x' prf =>
match eq_dec x' x with
| or_introl eqprf => eq_ind x' P prf x eqprf
| _ => def
end
end.
Theorem inj_right_pair :
forall (P:A -> Prop) (y y':P x),
ex_intro P x y = ex_intro P x y' -> y = y'.
Proof.
intros.
cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y).
simpl in |- *.
case (eq_dec x x).
intro e.
elim e using K_dec; trivial.
intros.
case n; trivial.
case H.
reflexivity.
Qed.
End EqdepDec.
Require Import EqdepFacts.
(** We deduce axiom [K] for (decidable) types *)
Theorem K_dec_type :
forall A:Type,
(forall x y:A, {x = y} + {x <> y}) ->
forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
Proof.
intros A eq_dec x P H p.
elim p using K_dec; intros.
case (eq_dec x0 y); [left|right]; assumption.
trivial.
Qed.
Theorem K_dec_set :
forall A:Set,
(forall x y:A, {x = y} + {x <> y}) ->
forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
Proof fun A => K_dec_type (A:=A).
(** We deduce the [eq_rect_eq] axiom for (decidable) types *)
Theorem eq_rect_eq_dec :
forall A:Type,
(forall x y:A, {x = y} + {x <> y}) ->
forall (p:A) (Q:A -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
Proof.
intros A eq_dec.
apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)).
Qed.
(** We deduce the injectivity of dependent equality for decidable types *)
Theorem eq_dep_eq_dec :
forall A:Type,
(forall x y:A, {x = y} + {x <> y}) ->
forall (P:A->Type) (p:A) (x y:P p), eq_dep A P p x p y -> x = y.
Proof (fun A eq_dec => eq_rect_eq__eq_dep_eq A (eq_rect_eq_dec eq_dec)).
Unset Implicit Arguments.
(************************************************************************)
(** ** Definition of the functor that builds properties of dependent equalities on decidable sets in Type *)
(** The signature of decidable sets in [Type] *)
Module Type DecidableType.
Parameter U:Type.
Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
End DecidableType.
(** The module [DecidableEqDep] collects equality properties for decidable
set in [Type] *)
Module DecidableEqDep (M:DecidableType).
Import M.
(** Invariance by Substitution of Reflexive Equality Proofs *)
Lemma eq_rect_eq :
forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
Proof eq_rect_eq_dec eq_dec.
(** Injectivity of Dependent Equality *)
Theorem eq_dep_eq :
forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y.
Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq).
(** Uniqueness of Identity Proofs (UIP) *)
Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
Proof (eq_dep_eq__UIP U eq_dep_eq).
(** Uniqueness of Reflexive Identity Proofs *)
Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x.
Proof (UIP__UIP_refl U UIP).
(** Streicher's axiom K *)
Lemma Streicher_K :
forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
Proof (K_dec_type eq_dec).
(** Injectivity of equality on dependent pairs in [Type] *)
Lemma inj_pairT2 :
forall (P:U -> Type) (p:U) (x y:P p),
existT P p x = existT P p y -> x = y.
Proof eq_dep_eq__inj_pairT2 U eq_dep_eq.
(** Proof-irrelevance on subsets of decidable sets *)
Lemma inj_pairP2 :
forall (P:U -> Prop) (x:U) (p q:P x),
ex_intro P x p = ex_intro P x q -> p = q.
Proof.
intros.
apply inj_right_pair with (A:=U).
intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption.
assumption.
Qed.
End DecidableEqDep.
(************************************************************************)
(** ** B Definition of the functor that builds properties of dependent equalities on decidable sets in Set *)
(** The signature of decidable sets in [Set] *)
Module Type DecidableSet.
Parameter U:Set.
Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
End DecidableSet.
(** The module [DecidableEqDepSet] collects equality properties for decidable
set in [Set] *)
Module DecidableEqDepSet (M:DecidableSet).
Import M.
Module N:=DecidableEqDep(M).
(** Invariance by Substitution of Reflexive Equality Proofs *)
Lemma eq_rect_eq :
forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
Proof eq_rect_eq_dec eq_dec.
(** Injectivity of Dependent Equality *)
Theorem eq_dep_eq :
forall (P:U->Type) (p:U) (x y:P p), eq_dep U P p x p y -> x = y.
Proof N.eq_dep_eq.
(** Uniqueness of Identity Proofs (UIP) *)
Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.
Proof N.UIP.
(** Uniqueness of Reflexive Identity Proofs *)
Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x.
Proof N.UIP_refl.
(** Streicher's axiom K *)
Lemma Streicher_K :
forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
Proof N.Streicher_K.
(** Injectivity of equality on dependent pairs with second component
in [Type] *)
Lemma inj_pairT2 :
forall (P:U -> Type) (p:U) (x y:P p),
existT P p x = existT P p y -> x = y.
Proof N.inj_pairT2.
(** Proof-irrelevance on subsets of decidable sets *)
Lemma inj_pairP2 :
forall (P:U -> Prop) (x:U) (p q:P x),
ex_intro P x p = ex_intro P x q -> p = q.
Proof N.inj_pairP2.
(** Injectivity of equality on dependent pairs in [Set] *)
Lemma inj_pair2 :
forall (P:U -> Set) (p:U) (x y:P p),
existS P p x = existS P p y -> x = y.
Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq.
End DecidableEqDepSet.
|
