In mathematics there are two kinds of existence:
The concrete or informative existence happens when we show that something exists by constructing a specific instance, which is then available.
The abstract or non-informative existence happens when we know that something exists by indirect means, or because the constucted witness has been hidden away from us by some mechanism.
An example that students come accross is this:
Theorem: There is a non-computable function $f : \mathbb{N} \to \mathbb{N}$.
Abstract existence proof: there are uncountably many function $\mathbb{N} \to \mathbb{N}$ but only countably many Turing machines, therefore some functions must be non-computable. $\Box$
Concrete existence proof: we claim that the function $h : \mathbb{N} \to \mathbb{N}$ defined by
$$
h(n) = \begin{cases}
1 & \text{if $n$-th Turing machine halts on input $n$},\\
0 & \text{otherwise.}
\end{cases}
$$
is not computable. (Insert here the standard proof that $h$ is not-computable.) $\Box$
I hope this conveys the idea clearly enough. First-order logic only expresses the abstract existence. Martin-Löf type theory only expresses the concrete existence.
Coq can express both kinds of existence. The abstract one is exists
and the concrete one is sig
. So if you want to actually extract witnesses, then you should be using sig
, not exists
.
In Coq sig (fun (x : A) => P x)
is written in the more readable notation {x : A | P x}
. Here is the extraction function you asked for:
Definition extract {A B : Type} (P : A -> B -> Prop) :
(forall a, { b : B | P a b }) -> { f : A -> B | forall a, P a (f a) }
:=
fun g => exist (fun f => forall a, P a (f a)) (fun a => proj1_sig (g a)) (fun a => proj2_sig (g a)).
It is possible to do violence to Coq and extract functions from the wrong existence by postulating various choice principles (as in Coq.Logic.ChoiceFacts
), but it's just better to use the correct form of existence.
P.S. The difference between informative and non-informative facts extends to all of logic and is not specific to existence. We may distinguish between informative facts, where knowing a fact also gives us the ability to inspect the reason for knowing it, and the non-informative facts, where we simply know a fact, but have no access to any reason as to why the fact holds. In Coq the non-informative facts are in Prop
, whereas the informative ones are in Type
.