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.

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

Based on ideas from Benjamin Werner and Jean-François Monin

Contributed by Yevgeniy Makarov

Require Import Arith.

Section ConstructiveIndefiniteDescription.

Variable P : nat -> Prop.

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

To find a witness of P constructively, we define an algorithm that tries P on all natural numbers starting from 0 and going up. 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 Local acc x := (Acc R x).

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.

Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}.

Theorem constructive_indefinite_description_nat : (exists n : nat, P n) -> {n : nat | P n}.

End ConstructiveIndefiniteDescription.

Section ConstructiveEpsilon.

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 : Set.
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_description : (exists x : A, P x) -> {x : A | P x}.

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

Definition constructive_epsilon (E : exists x : A, P x) : A
  := proj1_sig (constructive_indefinite_description E).

Definition constructive_epsilon_spec (E : (exists x, P x)) : P (constructive_epsilon E)
  := proj2_sig (constructive_indefinite_description E).

End ConstructiveEpsilon.