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
|
(************************************************************************)
(* 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] follows an outline by Michael Hedberg
*)
(** We need some dependent elimination schemes *)
Set Implicit Arguments.
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_eq : 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_eq.
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.
elim 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.
|
