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.
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 =>
    match b return ~ P n -> before_witness (S n) with
      | stop _ p => fun not_p => match (not_p p) with end
      | next _ b => fun _ => b

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)

Definition constructive_indefinite_ground_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)).

Fixpoint linear_search_smallest (start : nat) (pr : before_witness start) :
  forall k : nat, start <= k < proj1_sig (linear_search start pr) -> ~P k.

Definition epsilon_smallest :
  (exists n : nat, P n)
  -> { n : nat | P n /\ forall k : nat, k < n -> ~P k }.

End ConstructiveIndefiniteGroundDescription_Direct.

Section ConstructiveIndefiniteGroundDescription_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.

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.