Library Coq.Logic.ConstructiveEpsilon

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

Require Import Arith.

Section ConstructiveIndefiniteGroundDescription_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 (n:nat) : Prop :=
  | stop : P n -> before_witness n
  | : before_witness (S n) -> before_witness n.

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)

Definition inv_before_witness :
  forall n, before_witness n -> ~(P n) -> before_witness (S n) :=
  fun n b not_p =>
    match b with
      | stop _ p => match not_p p with end
      | next _ b => b

Basic program
Fixpoint prog_linear_search start (b : before_witness start) : nat :=
  match P_dec start with
    | left yes => start
    | right no => prog_linear_search (S start) (inv_before_witness start b no)

rel_ls = relational version of linear search
Inductive rel_ls : nat -> nat -> Prop :=
| Rstop : forall {found}, P found -> rel_ls found found
| Rnext : forall {start found}, ~(P start) -> rel_ls (S start) found -> rel_ls start found.

Following the Braga method, the output is packed with a proof of its conformity wrt rel_ls
A variant where the computational contents is closer to prog_linear_search (no deconstruction/reconstruction of the result), using a suitable abstraction of the postcondition. The predicate rel_ls start is abstracted into Q, with an additional implication rq they are equivalent (but only one direction is needed); and as linear search is tail recursive, Q can be fixed (but rq varies, behaving like a logical continuation).
Start at 0
Definition linear_search_from_0_conform (e : exists n, P n) : {n:nat | rel_ls 0 n} :=
    let b := let (n, p) := e in O_witness n (stop n p) in
    linear_search_conform 0 b.

Partial correctness properties
rel_ls entails P on the output
Theorem rel_ls_post : forall {start found}, rel_ls start found -> P found.

rel_ls entails minimality of the output
For compatibility with previous version
Main definitions
NB. The previous version used a negative formulation: forall k, k < n -> ~P k Lemmas le_not_lt and lt_not_le can help if needed.
In simple situations like here, a direct proof that prog_linear_search satisfies rel_ls can be provided. On the computational side of the proof, the fixpoint (coming from before_witness_dep_ind) has to come first, before the pattern matching on P_dec, so we get a slight mismatch between the program prog_linear_search and the proof; in particular, there is a duplication for Rstop.

Scheme before_witness_dep_ind := Induction for before_witness Sort Prop.

Lemma linear_search_rel : forall start b, rel_ls start (prog_linear_search start b).

Start at 0
Definition linear_search_from_0 (e : exists n, P n) : nat :=
    let b := let (n, p) := e in O_witness n (stop n p) in
    prog_linear_search 0 b.

Lemma linear_search_from_0_rel (e : exists n, P n) :
  rel_ls 0 (linear_search_from_0 e).

Main definitions
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.

Lemma P_implies_acc : forall x : nat, P x -> acc x.

Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x.

Corollary P_eventually_implies_acc_ex : (exists n : nat, P n) -> acc 0.

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.

Variable A : Type.
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}.

Lemma constructive_indefinite_ground_description : (exists x : A, P x) -> {x : A | P x}.

Lemma constructive_definite_ground_description : (exists! x : A, P x) -> {x : A | P x}.

Definition constructive_ground_epsilon (E : exists x : A, P x) : A
  := proj1_sig (constructive_indefinite_ground_description E).

Definition constructive_ground_epsilon_spec (E : (exists x, P x)) : P (constructive_ground_epsilon E)
  := proj2_sig (constructive_indefinite_ground_description E).

End ConstructiveGroundEpsilon.