1
<html xmlns="http://www.w3.org/1999/xhtml">
3
<meta http-equiv="Content-Type" content="text/html; charset="><link rel="stylesheet" href="style.css" type="text/css"><title>Coq.Logic.Eqdep_dec</title>
8
<h1>Library Coq.Logic.Eqdep_dec</h1>
13
<table width="100%"><tr class="doc"><td>
14
We prove that there is only one proof of <code>x=x</code>, i.e <code>(refl_equal ? x)</code>.
15
This holds if the equality upon the set of <code>x</code> is decidable.
16
A corollary of this theorem is the equality of the right projections
17
of two equal dependent pairs.
20
Author: Thomas Kleymann |<tms@dcs.ed.ac.uk>| in Lego
21
adapted to Coq by B. Barras
24
Credit: Proofs up to <code>K_dec</code> follows an outline by Michael Hedberg
32
<table width="100%"><tr class="doc"><td>
33
We need some dependent elimination schemes
38
Set <code class="keyword">Implicit</code> Arguments.<br/>
43
<table width="100%"><tr class="doc"><td>
44
Bijection between <code>eq</code> and <code>eqT</code>
47
<code class="keyword">Definition</code> <a name="eq2eqT"></a>eq2eqT (A:Set) (x y:A) (eqxy:x = y) : <br/>
48
x = y :=<br/>
49
match eqxy in (_ = y) return x = y with<br/>
50
| <a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> => <a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> x<br/>
51
end.<br/>
54
<code class="keyword">Definition</code> <a name="eqT2eq"></a>eqT2eq (A:Set) (x y:A) (eqTxy:x = y) : <br/>
55
x = y :=<br/>
56
match eqTxy in (_ = y) return x = y with<br/>
57
| <a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> => <a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> x<br/>
58
end.<br/>
61
<code class="keyword">Lemma</code> <a name="eq_eqT_bij"></a>eq_eqT_bij : forall (A:Set) (x y:A) (p:x = y), p = <a href="Coq.Logic.Eqdep_dec.html#eqT2eq">eqT2eq</a> (<a href="Coq.Logic.Eqdep_dec.html#eq2eqT">eq2eqT</a> p).<br/>
63
case p; reflexivity.<br/>
64
<code class="keyword">Qed</code>.<br/>
67
<code class="keyword">Lemma</code> <a name="eqT_eq_bij"></a>eqT_eq_bij : forall (A:Set) (x y:A) (p:x = y), p = <a href="Coq.Logic.Eqdep_dec.html#eq2eqT">eq2eqT</a> (<a href="Coq.Logic.Eqdep_dec.html#eqT2eq">eqT2eq</a> p).<br/>
69
case p; reflexivity.<br/>
70
<code class="keyword">Qed</code>.<br/>
73
<code class="keyword">Section</code> DecidableEqDep.<br/>
76
<code class="keyword">Variable</code> A : Type.<br/>
79
<code class="keyword">Let</code> comp (x y y':A) (eq1:x = y) (eq2:x = y') : y = y' :=<br/>
80
<a href="Coq.Init.Logic.html#eq_ind">eq_ind</a> _ (fun a => a = y') eq2 _ eq1.<br/>
83
<code class="keyword">Remark</code> trans_sym_eqT : forall (x y:A) (u:x = y), comp u u = <a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> y.<br/>
86
<code class="keyword">Qed</code>.<br/>
89
<code class="keyword">Variable</code> eq_dec : forall x y:A, x = y \/ x <> y.<br/>
92
<code class="keyword">Variable</code> x : A.<br/>
95
<code class="keyword">Let</code> nu (y:A) (u:x = y) : x = y :=<br/>
96
match eq_dec x y with<br/>
97
| <a href="Coq.Init.Logic.html#or_introl">or_introl</a> eqxy => eqxy<br/>
98
| <a href="Coq.Init.Logic.html#or_intror">or_intror</a> neqxy => <a href="Coq.Init.Logic.html#False_ind">False_ind</a> _ (neqxy u)<br/>
99
end.<br/>
102
<code class="keyword">Let</code> nu_constant : forall (y:A) (u v:x = y), nu u = nu v.<br/>
104
unfold nu in |- *.<br/>
105
case (eq_dec x y); intros.<br/>
109
case n; trivial.<br/>
110
<code class="keyword">Qed</code>.<br/>
113
<code class="keyword">Let</code> nu_inv (y:A) (v:x = y) : x = y := comp (nu (<a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> x)) v.<br/>
116
<code class="keyword">Remark</code> nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u.<br/>
118
case u; unfold nu_inv in |- *.<br/>
119
apply <a href="Coq.Logic.Eqdep_dec.html#trans_sym_eqT">trans_sym_eqT</a>.<br/>
120
<code class="keyword">Qed</code>.<br/>
123
<code class="keyword">Theorem</code> <a name="eq_proofs_unicity"></a>eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.<br/>
125
elim <a href="Coq.Logic.Eqdep_dec.html#nu_left_inv">nu_left_inv</a> with (u:= p1).<br/>
126
elim <a href="Coq.Logic.Eqdep_dec.html#nu_left_inv">nu_left_inv</a> with (u:= p2).<br/>
127
elim nu_constant with y p1 p2.<br/>
129
<code class="keyword">Qed</code>.<br/>
132
<code class="keyword">Theorem</code> <a name="K_dec"></a>K_dec :<br/>
133
forall P:x = x -> Prop, P (<a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> x) -> forall p:x = x, P p.<br/>
135
elim <a href="Coq.Logic.Eqdep_dec.html#eq_proofs_unicity">eq_proofs_unicity</a> with x (<a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> x) p.<br/>
137
<code class="keyword">Qed</code>.<br/>
142
<table width="100%"><tr class="doc"><td>
148
<code class="keyword">Let</code> proj (P:A -> Prop) (exP:<a href="Coq.Init.Logic.html#ex">ex</a> P) (def:P x) : P x :=<br/>
149
match exP with<br/>
150
| <a href="Coq.Init.Logic.html#ex_intro">ex_intro</a> x' prf =><br/>
151
match eq_dec x' x with<br/>
152
| <a href="Coq.Init.Logic.html#or_introl">or_introl</a> eqprf => <a href="Coq.Init.Logic.html#eq_ind">eq_ind</a> x' P prf x eqprf<br/>
153
| _ => def<br/>
154
end<br/>
155
end.<br/>
158
<code class="keyword">Theorem</code> <a name="inj_right_pair"></a>inj_right_pair :<br/>
159
forall (P:A -> Prop) (y y':P x),<br/>
160
<a href="Coq.Init.Logic.html#ex_intro">ex_intro</a> P x y = <a href="Coq.Init.Logic.html#ex_intro">ex_intro</a> P x y' -> y = y'.<br/>
162
cut (proj (<a href="Coq.Init.Logic.html#ex_intro">ex_intro</a> P x y) y = proj (<a href="Coq.Init.Logic.html#ex_intro">ex_intro</a> P x y') y).<br/>
164
case (eq_dec x x).<br/>
166
elim e using <a href="Coq.Logic.Eqdep_dec.html#K_dec">K_dec</a>; trivial.<br/>
170
case n; trivial.<br/>
175
<code class="keyword">Qed</code>.<br/>
178
<code class="keyword">End</code> DecidableEqDep.<br/>
183
<table width="100%"><tr class="doc"><td>
184
We deduce the <code>K</code> axiom for (decidable) Set
187
<code class="keyword">Theorem</code> <a name="K_dec_set"></a>K_dec_set :<br/>
188
forall A:Set,<br/>
189
(forall x y:A, {x = y} + {x <> y}) -><br/>
190
forall (x:A) (P:x = x -> Prop), P (<a href="Coq.Init.Logic.html#refl_equal">refl_equal</a> x) -> forall p:x = x, P p.<br/>
192
rewrite <a href="Coq.Logic.Eqdep_dec.html#eq_eqT_bij">eq_eqT_bij</a>.<br/>
193
elim (<a href="Coq.Logic.Eqdep_dec.html#eq2eqT">eq2eqT</a> p) using <a href="Coq.Logic.Eqdep_dec.html#K_dec">K_dec</a>.<br/>
195
case (H x0 y); intros.<br/>
196
elim e; left; reflexivity.<br/>
199
right; red in |- *; intro neq; apply n; elim neq; reflexivity.<br/>
203
<code class="keyword">Qed</code>.</code>
204
<hr/><a href="index.html">Index</a><hr/><font size="-1">This page has been generated by <a href="http://www.lri.fr/~filliatr/coqdoc/">coqdoc</a></font>
b'\\ No newline at end of file'
added
removed
library/Coq.Logic.Eqdep_dec.html
