Library Coq.Logic.ConstructiveEpsilon
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
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.
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.
In the following statement, we use the trick with recursion on
Acc. This is also where decidability of P is used.
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.