ConstructiveEpsilon.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*)

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 ∃ 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

(* -------------------------------------------------------------------- *)

(* Direct version *)

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 ∃ x :A, P x) makes the search eventually stops.

Inductive before_witness (n:nat) : Prop :=
  | stop : P n -> before_witness n
  | next : before_witness (S n) -> before_witness n.

(* Computation of the initial termination certificate *)
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)
  end.

(* Inversion of [inv_before_witness n] in a way such that the result
is structurally smaller even in the [stop] case. *)
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
    end.

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)
  end.

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.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k : nat),
start0 <= k <
proj1_sig
  (linear_search start0 pr0) ->
~ P k
start:nat
pr:before_witness start
forall k : nat,
start <= k < proj1_sig (linear_search start pr) ->
~ P k
Proof.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k : nat),
start0 <= k <
proj1_sig
  (linear_search start0 pr0) ->
~ P k
start:nat
pr:before_witness start
forall k : nat,
start <= k < proj1_sig (linear_search start pr) ->
~ P k
  (* Recursion on pr, which is the distance between start and linear_search *)
  intros.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < proj1_sig (linear_search start pr)
~ P k destruct (P_dec start) eqn:Pstart.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < proj1_sig (linear_search start pr)
p:P start
Pstart:P_dec start = left p
~ P k
P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < proj1_sig (linear_search start pr)
n:~ P start
Pstart:P_dec start = right n
~ P k
  - (* P start, k cannot exist *)P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < proj1_sig (linear_search start pr)
p:P start
Pstart:P_dec start = left p
~ P k
    intros.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < proj1_sig (linear_search start pr)
p:P start
Pstart:P_dec start = left p
~ P k assert (proj1_sig (linear_search start pr) = start).P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < proj1_sig (linear_search start pr)
p:P start
Pstart:P_dec start = left p
proj1_sig (linear_search start pr) = start
P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < proj1_sig (linear_search start pr)
p:P start
Pstart:P_dec start = left p
H0:proj1_sig (linear_search start pr) = start
~ P k
    {P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < proj1_sig (linear_search start pr)
p:P start
Pstart:P_dec start = left p
proj1_sig (linear_search start pr) = start unfold linear_search.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < proj1_sig (linear_search start pr)
p:P start
Pstart:P_dec start = left p
proj1_sig
  ((fix
    linear_search (m : nat) (b : before_witness m)
                  {struct b} : {n : nat | P n} :=
      match P_dec m with
      | left yes => exist (fun n : nat => P n) m yes
      | right no =>
          linear_search (S m)
            (inv_before_witness m b no)
      end) start pr) = start destruct pr; rewrite -> Pstart; reflexivity. }P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < proj1_sig (linear_search start pr)
p:P start
Pstart:P_dec start = left p
H0:proj1_sig (linear_search start pr) = start
~ P k
    rewrite -> H0 in H.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < start
p:P start
Pstart:P_dec start = left p
H0:proj1_sig (linear_search start pr) = start
~ P k destruct H.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k
H1:k < start
p:P start
Pstart:P_dec start = left p
H0:proj1_sig (linear_search start pr) = start
~ P k apply (le_lt_trans start k) in H1.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k
H1:start < start
p:P start
Pstart:P_dec start = left p
H0:proj1_sig (linear_search start pr) = start
~ P k
P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k
H1:k < start
p:P start
Pstart:P_dec start = left p
H0:proj1_sig (linear_search start pr) = start
start <= k
    apply lt_irrefl in H1.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k
H1:False
p:P start
Pstart:P_dec start = left p
H0:proj1_sig (linear_search start pr) = start
~ P k
P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k
H1:k < start
p:P start
Pstart:P_dec start = left p
H0:proj1_sig (linear_search start pr) = start
start <= k contradiction.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k
H1:k < start
p:P start
Pstart:P_dec start = left p
H0:proj1_sig (linear_search start pr) = start
start <= k assumption.
  - (* ~P start, step once in the search and use induction hypothesis *)P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness start
k:nat
H:start <= k < proj1_sig (linear_search start pr)
n:~ P start
Pstart:P_dec start = right n
~ P k
    destruct pr.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr : before_witness start0)
  (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr) ->
~ P k0
start:nat
p:P start
k:nat
H:start <= k <
proj1_sig (linear_search start (stop start p))
n:~ P start
Pstart:P_dec start = right n
~ P k
P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start <= k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k contradiction.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start <= k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k destruct H.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start <= k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k apply le_lt_or_eq in H.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start < k \/ start = k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k destruct H.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start < k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k
P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start = k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k
    apply (linear_search_smallest (S start) pr).P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start < k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
S start <= k < proj1_sig (linear_search (S start) pr)
P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start = k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k split.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start < k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
S start <= k
P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start < k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
k < proj1_sig (linear_search (S start) pr)
P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start = k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k assumption.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start < k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
k < proj1_sig (linear_search (S start) pr)
P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start = k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k
    simpl in H0.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start < k
H0:k <
proj1_sig
  match P_dec start with
  | left yes =>
      exist (fun n0 : nat => P n0) start yes
  | right _ => linear_search (S start) pr
  end
n:~ P start
Pstart:P_dec start = right n
k < proj1_sig (linear_search (S start) pr)
P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start = k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k rewrite -> Pstart in H0.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start < k
H0:k < proj1_sig (linear_search (S start) pr)
n:~ P start
Pstart:P_dec start = right n
k < proj1_sig (linear_search (S start) pr)
P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start = k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k assumption.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start0 : nat)
  (pr0 : before_witness
           start0) (k0 : nat),
start0 <= k0 <
proj1_sig
  (linear_search start0 pr0) ->
~ P k0
start:nat
pr:before_witness (S start)
k:nat
H:start = k
H0:k <
proj1_sig (linear_search start (next start pr))
n:~ P start
Pstart:P_dec start = right n
~ P k subst.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
linear_search_smallest:forall (start : nat)
  (pr0 : before_witness start)
  (k0 : nat),
start <= k0 <
proj1_sig
  (linear_search start pr0) ->
~ P k0
k:nat
pr:before_witness (S k)
n:~ P k
Pstart:P_dec k = right n
H0:k < proj1_sig (linear_search k (next k pr))
~ P k assumption.
Defined.

Definition epsilon_smallest :
  (exists n : nat, P n)
  -> { n : nat | P n /\ forall k : nat, k < n -> ~P k }.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
(exists n : nat, P n) ->
{n : nat | P n /\ (forall k : nat, k < n -> ~ P k)}
Proof.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
(exists n : nat, P n) ->
{n : nat | P n /\ (forall k : nat, k < n -> ~ P k)}
  intros.P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
H:exists n : nat, P n
{n : nat | P n /\ (forall k : nat, k < n -> ~ P k)} pose (wit := (let (n, p) := H in O_witness n (stop n p))).P:nat -> Prop
P_dec:forall n : nat, {P n} + {~ P n}
H:exists n : nat, P n
wit:=let (n, p) := H in O_witness n (stop n p):before_witness 0
{n : nat | P n /\ (forall k : nat, k < n -> ~ P k)}
  destruct (linear_search 0 wit) as [n pr] eqn:ls.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
H:exists n0 : nat, P n0
wit:=let (n0, p) := H in O_witness n0 (stop n0 p):before_witness 0
n:nat
pr:P n
ls:linear_search 0 wit =
exist (fun n0 : nat => P n0) n pr
{n0 : nat | P n0 /\ (forall k : nat, k < n0 -> ~ P k)} exists n.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
H:exists n0 : nat, P n0
wit:=let (n0, p) := H in O_witness n0 (stop n0 p):before_witness 0
n:nat
pr:P n
ls:linear_search 0 wit =
exist (fun n0 : nat => P n0) n pr
P n /\ (forall k : nat, k < n -> ~ P k) split.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
H:exists n0 : nat, P n0
wit:=let (n0, p) := H in O_witness n0 (stop n0 p):before_witness 0
n:nat
pr:P n
ls:linear_search 0 wit =
exist (fun n0 : nat => P n0) n pr
P n
P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
H:exists n0 : nat, P n0
wit:=let (n0, p) := H in O_witness n0 (stop n0 p):before_witness 0
n:nat
pr:P n
ls:linear_search 0 wit =
exist (fun n0 : nat => P n0) n pr
forall k : nat, k < n -> ~ P k assumption.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
H:exists n0 : nat, P n0
wit:=let (n0, p) := H in O_witness n0 (stop n0 p):before_witness 0
n:nat
pr:P n
ls:linear_search 0 wit =
exist (fun n0 : nat => P n0) n pr
forall k : nat, k < n -> ~ P k intros.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
H:exists n0 : nat, P n0
wit:=let (n0, p) := H in O_witness n0 (stop n0 p):before_witness 0
n:nat
pr:P n
ls:linear_search 0 wit =
exist (fun n0 : nat => P n0) n pr
k:nat
H0:k < n
~ P k
  apply (linear_search_smallest 0 wit).P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
H:exists n0 : nat, P n0
wit:=let (n0, p) := H in O_witness n0 (stop n0 p):before_witness 0
n:nat
pr:P n
ls:linear_search 0 wit =
exist (fun n0 : nat => P n0) n pr
k:nat
H0:k < n
0 <= k < proj1_sig (linear_search 0 wit) split.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
H:exists n0 : nat, P n0
wit:=let (n0, p) := H in O_witness n0 (stop n0 p):before_witness 0
n:nat
pr:P n
ls:linear_search 0 wit =
exist (fun n0 : nat => P n0) n pr
k:nat
H0:k < n
0 <= k
P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
H:exists n0 : nat, P n0
wit:=let (n0, p) := H in O_witness n0 (stop n0 p):before_witness 0
n:nat
pr:P n
ls:linear_search 0 wit =
exist (fun n0 : nat => P n0) n pr
k:nat
H0:k < n
k < proj1_sig (linear_search 0 wit) apply le_0_n.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
H:exists n0 : nat, P n0
wit:=let (n0, p) := H in O_witness n0 (stop n0 p):before_witness 0
n:nat
pr:P n
ls:linear_search 0 wit =
exist (fun n0 : nat => P n0) n pr
k:nat
H0:k < n
k < proj1_sig (linear_search 0 wit)
  rewrite -> ls.P:nat -> Prop
P_dec:forall n0 : nat, {P n0} + {~ P n0}
H:exists n0 : nat, P n0
wit:=let (n0, p) := H in O_witness n0 (stop n0 p):before_witness 0
n:nat
pr:P n
ls:linear_search 0 wit =
exist (fun n0 : nat => P n0) n pr
k:nat
H0:k < n
k < proj1_sig (exist (fun n0 : nat => P n0) n pr) assumption.
Qed.

End ConstructiveIndefiniteGroundDescription_Direct.

(************************************************************************)

(* Version using the predicate [Acc] *)

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 ∃ 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.

Notation acc x := (Acc R x).

Lemma P_implies_acc : forall x : nat, P x -> acc x.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
forall x : nat, P x -> acc x
Proof.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
forall x : nat, P x -> acc x
intros x H.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y : nat => x0 = S y /\ ~ P y:nat -> nat -> Prop
x:nat
H:P x
acc x constructor.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y : nat => x0 = S y /\ ~ P y:nat -> nat -> Prop
x:nat
H:P x
forall y : nat, R y x -> acc y
intros y [_ not_Px].P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y0 : nat => x0 = S y0 /\ ~ P y0:nat -> nat -> Prop
x:nat
H:P x
y:nat
not_Px:~ P x
acc y absurd (P x); assumption.
Qed.

Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
forall x n : nat, P (n + x) -> acc x
Proof.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
forall x n : nat, P (n + x) -> acc x
intros x n; generalize x; clear x; induction n as [|n IH]; simpl.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
forall x : nat, P x -> acc x
P:nat -> Prop
P_decidable:forall n0 : nat, {P n0} + {~ P n0}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
n:nat
IH:forall x : nat, P (n + x) -> acc x
forall x : nat, P (S (n + x)) -> acc x
apply P_implies_acc.P:nat -> Prop
P_decidable:forall n0 : nat, {P n0} + {~ P n0}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
n:nat
IH:forall x : nat, P (n + x) -> acc x
forall x : nat, P (S (n + x)) -> acc x
intros x H.P:nat -> Prop
P_decidable:forall n0 : nat, {P n0} + {~ P n0}
R:=fun x0 y : nat => x0 = S y /\ ~ P y:nat -> nat -> Prop
n:nat
IH:forall x0 : nat, P (n + x0) -> acc x0
x:nat
H:P (S (n + x))
acc x constructor.P:nat -> Prop
P_decidable:forall n0 : nat, {P n0} + {~ P n0}
R:=fun x0 y : nat => x0 = S y /\ ~ P y:nat -> nat -> Prop
n:nat
IH:forall x0 : nat, P (n + x0) -> acc x0
x:nat
H:P (S (n + x))
forall y : nat, R y x -> acc y intros y [fxy _].P:nat -> Prop
P_decidable:forall n0 : nat, {P n0} + {~ P n0}
R:=fun x0 y0 : nat => x0 = S y0 /\ ~ P y0:nat -> nat -> Prop
n:nat
IH:forall x0 : nat, P (n + x0) -> acc x0
x:nat
H:P (S (n + x))
y:nat
fxy:y = S x
acc y
apply IH.P:nat -> Prop
P_decidable:forall n0 : nat, {P n0} + {~ P n0}
R:=fun x0 y0 : nat => x0 = S y0 /\ ~ P y0:nat -> nat -> Prop
n:nat
IH:forall x0 : nat, P (n + x0) -> acc x0
x:nat
H:P (S (n + x))
y:nat
fxy:y = S x
P (n + y) rewrite fxy.P:nat -> Prop
P_decidable:forall n0 : nat, {P n0} + {~ P n0}
R:=fun x0 y0 : nat => x0 = S y0 /\ ~ P y0:nat -> nat -> Prop
n:nat
IH:forall x0 : nat, P (n + x0) -> acc x0
x:nat
H:P (S (n + x))
y:nat
fxy:y = S x
P (n + S x)
replace (n + S x) with (S (n + x)); auto with arith.
Defined.

Corollary P_eventually_implies_acc_ex : (exists n : nat, P n) -> acc 0.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
(exists n : nat, P n) -> acc 0
Proof.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
(exists n : nat, P n) -> acc 0
intros H; elim H.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
H:exists n : nat, P n
forall x : nat, P x -> acc 0 intros x Px.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y : nat => x0 = S y /\ ~ P y:nat -> nat -> Prop
H:exists n : nat, P n
x:nat
Px:P x
acc 0 apply P_eventually_implies_acc with (n := x).P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y : nat => x0 = S y /\ ~ P y:nat -> nat -> Prop
H:exists n : nat, P n
x:nat
Px:P x
P (x + 0)
replace (x + 0) with x; auto with arith.
Defined.

In the following statement, we use the trick with recursion on Acc. This is also where decidability of P is used.

Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
acc 0 -> {n : nat | P n}
Proof.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
acc 0 -> {n : nat | P n}
intros Acc_0.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
Acc_0:acc 0
{n : nat | P n} pattern 0.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
Acc_0:acc 0
(fun _ : nat => {n0 : nat | P n0}) 0 apply Fix_F with (R := R); [| assumption].P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
Acc_0:acc 0
forall x : nat,
(forall y : nat, R y x -> {n : nat | P n}) ->
{n : nat | P n}
clear Acc_0; intros x IH.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y : nat => x0 = S y /\ ~ P y:nat -> nat -> Prop
x:nat
IH:forall y : nat, R y x -> {n : nat | P n}
{n : nat | P n}
destruct (P_decidable x) as [Px | not_Px].P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y : nat => x0 = S y /\ ~ P y:nat -> nat -> Prop
x:nat
IH:forall y : nat, R y x -> {n : nat | P n}
Px:P x
{n : nat | P n}
P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y : nat => x0 = S y /\ ~ P y:nat -> nat -> Prop
x:nat
IH:forall y : nat, R y x -> {n : nat | P n}
not_Px:~ P x
{n : nat | P n}
exists x; simpl; assumption.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y : nat => x0 = S y /\ ~ P y:nat -> nat -> Prop
x:nat
IH:forall y : nat, R y x -> {n : nat | P n}
not_Px:~ P x
{n : nat | P n}
set (y := S x).P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y0 : nat => x0 = S y0 /\ ~ P y0:nat -> nat -> Prop
x:nat
IH:forall y0 : nat, R y0 x -> {n : nat | P n}
not_Px:~ P x
y:=S x:nat
{n : nat | P n}
assert (Ryx : R y x).P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y0 : nat => x0 = S y0 /\ ~ P y0:nat -> nat -> Prop
x:nat
IH:forall y0 : nat, R y0 x -> {n : nat | P n}
not_Px:~ P x
y:=S x:nat
R y x
P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y0 : nat => x0 = S y0 /\ ~ P y0:nat -> nat -> Prop
x:nat
IH:forall y0 : nat, R y0 x -> {n : nat | P n}
not_Px:~ P x
y:=S x:nat
Ryx:R y x
{n : nat | P n} unfold R; split; auto.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x0 y0 : nat => x0 = S y0 /\ ~ P y0:nat -> nat -> Prop
x:nat
IH:forall y0 : nat, R y0 x -> {n : nat | P n}
not_Px:~ P x
y:=S x:nat
Ryx:R y x
{n : nat | P n}
destruct (IH y Ryx) as [n Hn].P:nat -> Prop
P_decidable:forall n0 : nat, {P n0} + {~ P n0}
R:=fun x0 y0 : nat => x0 = S y0 /\ ~ P y0:nat -> nat -> Prop
x:nat
IH:forall y0 : nat, R y0 x -> {n0 : nat | P n0}
not_Px:~ P x
y:=S x:nat
Ryx:R y x
n:nat
Hn:P n
{n0 : nat | P n0}
exists n; assumption.
Defined.

Theorem constructive_indefinite_ground_description_nat_Acc :
  (exists n : nat, P n) -> {n : nat | P n}.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
(exists n : nat, P n) -> {n : nat | P n}
Proof.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
(exists n : nat, P n) -> {n : nat | P n}
intros H; apply acc_implies_P_eventually.P:nat -> Prop
P_decidable:forall n : nat, {P n} + {~ P n}
R:=fun x y : nat => x = S y /\ ~ P y:nat -> nat -> Prop
H:exists n : nat, P n
acc 0
apply P_eventually_implies_acc_ex; assumption.
Defined.

End ConstructiveIndefiniteGroundDescription_Acc.

(************************************************************************)

Section ConstructiveGroundEpsilon_nat.

Variable P : nat -> Prop.

Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}.

Definition constructive_ground_epsilon_nat (E : exists n : nat, P n) : nat
  := proj1_sig (constructive_indefinite_ground_description_nat P P_decidable E).

Definition constructive_ground_epsilon_spec_nat (E : (exists n, P n)) : P (constructive_ground_epsilon_nat E)
  := proj2_sig (constructive_indefinite_ground_description_nat P P_decidable E).

End ConstructiveGroundEpsilon_nat.

(************************************************************************)

Section ConstructiveGroundEpsilon.

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}.A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
forall n : nat, {P' n} + {~ P' n}
Proof.A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
forall n : nat, {P' n} + {~ P' n}
intro n; unfold P'; destruct (P_decidable (g n)); auto.
Defined.

Lemma constructive_indefinite_ground_description : (exists x : A, P x) -> {x : A | P x}.A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
(exists x : A, P x) -> {x : A | P x}
Proof.A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
(exists x : A, P x) -> {x : A | P x}
intro H.A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
H:exists x : A, P x
{x : A | P x} assert (H1 : exists n : nat, P' n).A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
H:exists x : A, P x
exists n : nat, P' n
A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
H:exists x : A, P x
H1:exists n : nat, P' n
{x : A | P x}
destruct H as [x Hx].A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x0 : A, g (f x0) = x0
P:A -> Prop
P_decidable:forall x0 : A, {P x0} + {~ P x0}
x:A
Hx:P x
exists n : nat, P' n
A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
H:exists x : A, P x
H1:exists n : nat, P' n
{x : A | P x} exists (f x); unfold P'.A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x0 : A, g (f x0) = x0
P:A -> Prop
P_decidable:forall x0 : A, {P x0} + {~ P x0}
x:A
Hx:P x
P (g (f x))
A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
H:exists x : A, P x
H1:exists n : nat, P' n
{x : A | P x} rewrite gof_eq_id; assumption.A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
H:exists x : A, P x
H1:exists n : nat, P' n
{x : A | P x}
apply (constructive_indefinite_ground_description_nat P' P'_decidable)  in H1.A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
H:exists x : A, P x
H1:{n : nat | P' n}
{x : A | P x}
destruct H1 as [n Hn].A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
H:exists x : A, P x
n:nat
Hn:P' n
{x : A | P x} exists (g n); unfold P' in Hn; assumption.
Defined.

Lemma constructive_definite_ground_description : (exists! x : A, P x) -> {x : A | P x}.A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
(exists ! x : A, P x) -> {x : A | P x}
Proof.A:Type
f:A -> nat
g:nat -> A
gof_eq_id:forall x : A, g (f x) = x
P:A -> Prop
P_decidable:forall x : A, {P x} + {~ P x}
(exists ! x : A, P x) -> {x : A | P x}
  intros; apply constructive_indefinite_ground_description; firstorder.
Defined.

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.

(* begin hide *)
(* Compatibility: the qualificative "ground" was absent from the initial
names of the results in this file but this had introduced confusion
with the similarly named statement in Description.v *)
Notation constructive_indefinite_description_nat :=
  constructive_indefinite_ground_description_nat (only parsing).
Notation constructive_epsilon_spec_nat :=
  constructive_ground_epsilon_spec_nat (only parsing).
Notation constructive_epsilon_nat :=
  constructive_ground_epsilon_nat (only parsing).
Notation constructive_indefinite_description :=
  constructive_indefinite_ground_description (only parsing).
Notation constructive_definite_description :=
  constructive_definite_ground_description (only parsing).
Notation constructive_epsilon_spec :=
  constructive_ground_epsilon_spec (only parsing).
Notation constructive_epsilon :=
  constructive_ground_epsilon (only parsing).
(* end hide *)