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
|
(************************************************************************)
(* 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: ConstructiveEpsilon.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(*i $Id: ConstructiveEpsilon.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** This module proves the constructive description schema, which
infers the sigma-existence (i.e., [Set]-existence) of a witness to a
predicate from the regular existence (i.e., [Prop]-existence). One
requires that the underlying set is countable and that the predicate
is decidable. *)
(** Coq does not allow case analysis on sort [Prop] when the goal is in
[Set]. Therefore, one cannot eliminate [exists n, P n] in order to
show [{n : nat | P n}]. However, one can perform a recursion on an
inductive predicate in sort [Prop] so that the returning type of the
recursion is in [Set]. This trick is described in Coq'Art book, Sect.
14.2.3 and 15.4. In particular, this trick is used in the proof of
[Fix_F] in the module Coq.Init.Wf. There, recursion is done on an
inductive predicate [Acc] and the resulting type is in [Type].
To find a witness of [P] constructively, we program the well-known
linear search algorithm that tries P on all natural numbers starting
from 0 and going up. Such an algorithm needs a suitable termination
certificate. We offer two ways for providing this termination
certificate: a direct one, based on an ad-hoc predicate called
[before_witness], and another one based on the predicate [Acc].
For the first one we provide explicit and short proof terms. *)
(** Based on ideas from Benjamin Werner and Jean-François Monin *)
(** Contributed by Yevgeniy Makarov and Jean-François Monin *)
(* -------------------------------------------------------------------- *)
(* Direct version *)
Section ConstructiveIndefiniteDescription_Direct.
Variable P : nat -> Prop.
Hypothesis P_dec : forall n, {P n}+{~(P n)}.
(** The termination argument is [before_witness n], which says that
any number before any witness (not necessarily the [x] of [exists x :A, P x])
makes the search eventually stops. *)
Inductive before_witness : nat -> Prop :=
| stop : forall n, P n -> before_witness n
| next : forall n, before_witness (S n) -> before_witness n.
(* Computation of the initial termination certificate *)
Fixpoint O_witness (n : nat) : before_witness n -> before_witness 0 :=
match n return (before_witness n -> before_witness 0) with
| 0 => fun b => b
| S n => fun b => O_witness n (next n b)
end.
(* Inversion of [inv_before_witness n] in a way such that the result
is structurally smaller even in the [stop] case. *)
Definition inv_before_witness :
forall n, before_witness n -> ~(P n) -> before_witness (S n) :=
fun n b =>
match b in before_witness n return ~ P n -> before_witness (S n) with
| stop n p => fun not_p => match (not_p p) with end
| next n b => fun _ => b
end.
Fixpoint linear_search m (b : before_witness m) : {n : nat | P n} :=
match P_dec m with
| left yes => exist (fun n => P n) m yes
| right no => linear_search (S m) (inv_before_witness m b no)
end.
Definition constructive_indefinite_description_nat :
(exists n, P n) -> {n:nat | P n} :=
fun e => linear_search O (let (n, p) := e in O_witness n (stop n p)).
End ConstructiveIndefiniteDescription_Direct.
(************************************************************************)
(* Version using the predicate [Acc] *)
Require Import Arith.
Section ConstructiveIndefiniteDescription_Acc.
Variable P : nat -> Prop.
Hypothesis P_decidable : forall n : nat, {P n} + {~ P n}.
(** The predicate [Acc] delineates elements that are accessible via a
given relation [R]. An element is accessible if there are no infinite
[R]-descending chains starting from it.
To use [Fix_F], we define a relation R and prove that if [exists n, P n]
then 0 is accessible with respect to R. Then, by induction on the
definition of [Acc R 0], we show [{n : nat | P n}].
The relation [R] describes the connection between the two successive
numbers we try. Namely, [y] is [R]-less then [x] if we try [y] after
[x], i.e., [y = S x] and [P x] is false. Then the absence of an
infinite [R]-descending chain from 0 is equivalent to the termination
of our searching algorithm. *)
Let R (x y : nat) : Prop := x = S y /\ ~ P y.
Notation Local acc x := (Acc R x).
Lemma P_implies_acc : forall x : nat, P x -> acc x.
Proof.
intros x H. constructor.
intros y [_ not_Px]. absurd (P x); assumption.
Qed.
Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x.
Proof.
intros x n; generalize x; clear x; induction n as [|n IH]; simpl.
apply P_implies_acc.
intros x H. constructor. intros y [fxy _].
apply IH. rewrite fxy.
replace (n + S x) with (S (n + x)); auto with arith.
Defined.
Corollary P_eventually_implies_acc_ex : (exists n : nat, P n) -> acc 0.
Proof.
intros H; elim H. intros x Px. apply P_eventually_implies_acc with (n := x).
replace (x + 0) with x; auto with arith.
Defined.
(** In the following statement, we use the trick with recursion on
[Acc]. This is also where decidability of [P] is used. *)
Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}.
Proof.
intros Acc_0. pattern 0. apply Fix_F with (R := R); [| assumption].
clear Acc_0; intros x IH.
destruct (P_decidable x) as [Px | not_Px].
exists x; simpl; assumption.
set (y := S x).
assert (Ryx : R y x). unfold R; split; auto.
destruct (IH y Ryx) as [n Hn].
exists n; assumption.
Defined.
Theorem constructive_indefinite_description_nat_Acc :
(exists n : nat, P n) -> {n : nat | P n}.
Proof.
intros H; apply acc_implies_P_eventually.
apply P_eventually_implies_acc_ex; assumption.
Defined.
End ConstructiveIndefiniteDescription_Acc.
(************************************************************************)
Section ConstructiveEpsilon_nat.
Variable P : nat -> Prop.
Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}.
Definition constructive_epsilon_nat (E : exists n : nat, P n) : nat
:= proj1_sig (constructive_indefinite_description_nat P P_decidable E).
Definition constructive_epsilon_spec_nat (E : (exists n, P n)) : P (constructive_epsilon_nat E)
:= proj2_sig (constructive_indefinite_description_nat P P_decidable E).
End ConstructiveEpsilon_nat.
(************************************************************************)
Section ConstructiveEpsilon.
(** For the current purpose, we say that a set [A] is countable if
there are functions [f : A -> nat] and [g : nat -> A] such that [g] is
a left inverse of [f]. *)
Variable A : Set.
Variable f : A -> nat.
Variable g : nat -> A.
Hypothesis gof_eq_id : forall x : A, g (f x) = x.
Variable P : A -> Prop.
Hypothesis P_decidable : forall x : A, {P x} + {~ P x}.
Definition P' (x : nat) : Prop := P (g x).
Lemma P'_decidable : forall n : nat, {P' n} + {~ P' n}.
Proof.
intro n; unfold P'; destruct (P_decidable (g n)); auto.
Defined.
Lemma constructive_indefinite_description : (exists x : A, P x) -> {x : A | P x}.
Proof.
intro H. assert (H1 : exists n : nat, P' n).
destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption.
apply (constructive_indefinite_description_nat P' P'_decidable) in H1.
destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption.
Defined.
Lemma constructive_definite_description : (exists! x : A, P x) -> {x : A | P x}.
Proof.
intros; apply constructive_indefinite_description; firstorder.
Defined.
Definition constructive_epsilon (E : exists x : A, P x) : A
:= proj1_sig (constructive_indefinite_description E).
Definition constructive_epsilon_spec (E : (exists x, P x)) : P (constructive_epsilon E)
:= proj2_sig (constructive_indefinite_description E).
End ConstructiveEpsilon.
|
