This provides with a proof of the constructive form of definite
and indefinite descriptions for Sigma^0_1-formulas (hereafter called
"small" formulas), which infers the sigma-existence (i.e.,
Type-existence) of a witness to a decidable predicate over a
countable domain from the regular existence (i.e.,
Prop-existence).
Coq does not allow case analysis on sort
Prop when the goal is in
not in
Prop. 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
Type. 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
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.