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
The predicate
To use
Set when the goal is 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 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
Acc_iter 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
Acc_iter, 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}.
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) := (x = S y /\ ~ P y).
Notation Local "'acc' x" := (Acc R x) (at level 10).
Lemma P_implies_acc : forall x : nat, P x -> acc x.
Proof.
intros x H. constructor.
intros y [_ not_Px]. absurd (P x); assumption.
Qed.
Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x.
Proof.
intros x n; generalize x; clear x; induction n as [|n IH]; simpl.
apply P_implies_acc.
intros x H. constructor. intros y [fxy _].
apply IH. rewrite fxy.
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.
Proof.
intros H; elim H. intros x Px. apply P_eventually_implies_acc with (n := x).
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}.
Proof.
intros Acc_0. pattern 0. apply Acc_iter with (R := R); [| assumption].
clear Acc_0; intros x IH.
destruct (P_decidable x) as [Px | not_Px].
exists x; simpl; assumption.
set (y := S x).
assert (Ryx : R y x). unfold R; split; auto.
destruct (IH y Ryx) as [n Hn].
exists n; assumption.
Defined.
Theorem constructive_indefinite_description_nat : (exists n : nat, P n) -> {n : nat | P n}.
Proof.
intros H; apply acc_implies_P_eventually.
apply P_eventually_implies_acc_ex; assumption.
Defined.
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 : 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}.
Proof.
intro n; unfold P'; destruct (P_decidable (g n)); auto.
Defined.
Lemma constructive_indefinite_description : (exists x : A, P x) -> {x : A | P x}.
Proof.
intro H. assert (H1 : exists n : nat, P' n).
destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption.
apply (constructive_indefinite_description_nat P' P'_decidable) in H1.
destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption.
Defined.
Lemma constructive_definite_description : (exists! x : A, P x) -> {x : A | P x}.
Proof.
intros; apply constructive_indefinite_description; firstorder.
Defined.
Definition epsilon (E : exists x : A, P x) : A
:= proj1_sig (constructive_indefinite_description E).
Definition epsilon_spec (E : (exists x, P x)) : P (epsilon E)
:= proj2_sig (constructive_indefinite_description E).
End ConstructiveEpsilon.
Theorem choice :
forall (A B : Type) (f : B -> nat) (g : nat -> B),
(forall x : B, g (f x) = x) ->
forall (R : A -> B -> Prop),
(forall (x : A) (y : B), {R x y} + {~ R x y}) ->
(forall x : A, exists y : B, R x y) ->
(exists f : A -> B, forall x : A, R x (f x)).
Proof.
intros A B f g gof_eq_id R R_dec H.
exists (fun x : A => epsilon B f g gof_eq_id (R x) (R_dec x) (H x)).
intro x.
apply (epsilon_spec B f g gof_eq_id (R x) (R_dec x) (H x)).
Qed.