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.
The method based on
before_witness (2009) can be seen as an ancestor
of the first ingredient of the Braga method, by Dominique Larchey-Wendling
and Jean-François Monin (Types'18, then in more details in
[1]).
In this approach, the termination certificate is usually combined
with an inductive relational presentation of the recursive function
of interest. This became especially useful here since the introduction
of
epsilon_smallest, stating that the output of the linear search
algorithm is minimal, whereas in the 2009 version, the only
postcondition considered stated that the output satisfies
P.
In this file, the linear search program is named
prog_linear_search
because
linear_search happens to be the name of a similar but
different program in the 2009 version: both programs take as input a
natural number
start and a termination certificate, and
the output of
prog_linear_search is a natural number
n
whereas the output of
linear_search is
n packed with a proof
of
(P n). The inductive relation for linear search is named
rel_ls.
The Braga method usually consists in defining a function
f_conform
intended to be extracted as (the OCaml translation of) an n-ary
function
f, with inputs
x... and output type
{y | R x... y}
where
R is an inductive n+1-ary relational presentation of
f.
An additional input of
f_conform is a termination certificate
whose type can be derived from
R. Partial correctness properties
are proved on
R, then transported on
f_conform (an alternative,
not considered for linear search, is to simulate an inductive-recursive
scheme for
f_conform).
In the present case, the Coq name of
f is then
prog_linear_search,
R is
rel_ls and the type of the termination certificate is named
before_witness.
In simple situations such as linear search, one can as well
directly define the type of the termination certificate and
the n+1-ary Coq version of
f.
Several variants of the proofs are offered for the record:
- a version that follows the steps in [1], named linear_search_conform;
- a variant of the latter, named linear_search_conform_alt,
where the recursive call is no longer encapsulated in a
pattern-matching (avoiding packing-unpacking steps which
are for instance removed at extraction at the price of
an additional optimization step).
- a version where prog_linear_search is directly programmed
and its conformity to rel_ls (by dependent induction on
the termination certificate), and then the properties of
its output are separately proven.
It is interesting to see that in the last version, the conformity
proof slightly deviates from the definition of
prog_linear_search,
resulting in an unpleasant duplication of proof obligations, because
the first pattern-matching is performed on
P_dec start in the
function and on the termination certificate in the conformity proof.
This deviation seems to be unavoidable because crucial proof steps
require the guard argument of the fixpoint to start with a constructor.
The three programs
prog_linear_search,
linear_search_conform
and
linear_search_conform_alt are purposely presented in a
very similar manner, using
refine and postponing proof obligations
related to conformity to
rel_ls.
[1] Dominique Larchey-Wendling and Jean-François Monin.
The Braga Method: Extracting Certified Algorithms from
Complex Recursive Schemes in Coq, chapter 8, pages 305--386.
In K. Mainzer, P. Schuster, and H. Schwichtenberg, editors.
Proof and Computation II: From Proof Theory and Univalent
Mathematics to Program Extraction and Verification.
World Scientific, September 2021.
Based on ideas from Benjamin Werner and Jean-François Monin
Contributed by Yevgeniy Makarov and Jean-François Monin
Following the Braga method, the output is packed with a proof of its conformity wrt rel_ls