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
|
(************************************************************************)
(* 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: Eqdep_dec.v,v 1.14.2.1 2004/07/16 19:31:06 herbelin Exp $ 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] follows an outline by Michael Hedberg
*)
(** We need some dependent elimination schemes *)
Set Implicit Arguments.
(** Bijection between [eq] and [eqT] *)
Definition eq2eqT (A:Set) (x y:A) (eqxy:x = y) :
x = y :=
match eqxy in (_ = y) return x = y with
| refl_equal => refl_equal x
end.
Definition eqT2eq (A:Set) (x y:A) (eqTxy:x = y) :
x = y :=
match eqTxy in (_ = y) return x = y with
| refl_equal => refl_equal x
end.
Lemma eq_eqT_bij : forall (A:Set) (x y:A) (p:x = y), p = eqT2eq (eq2eqT p).
intros.
case p; reflexivity.
Qed.
Lemma eqT_eq_bij : forall (A:Set) (x y:A) (p:x = y), p = eq2eqT (eqT2eq p).
intros.
case p; reflexivity.
Qed.
Section DecidableEqDep.
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_eqT : forall (x y:A) (u:x = y), comp u u = refl_equal y.
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.
intros.
case u; unfold nu_inv in |- *.
apply trans_sym_eqT.
Qed.
Theorem eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.
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.
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'.
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 DecidableEqDep.
(** We deduce the [K] axiom for (decidable) Set *)
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.
intros.
rewrite eq_eqT_bij.
elim (eq2eqT p) using K_dec.
intros.
case (H x0 y); intros.
elim e; left; reflexivity.
right; red in |- *; intro neq; apply n; elim neq; reflexivity.
trivial.
Qed.
|
