# Proofs' role in Coq extractions

Though what chi said is correct, in this case you can actually extract the witness `p`

from the existence proof. When you have a boolean predicate `P : nat -> bool`

, if `exists p, P p = true`

, you can compute some `p`

that satisfies the predicate by running the following function from 0:

```
find p := if P p then p else find (S p)
```

You cannot write this function directly in Coq, but it is possible to do so by crafting a special inductive proposition. This pattern is implemented in the choice module of the mathematical components library:

```
From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
(* == is the boolean equality test *)
Definition even n := exists p, (n == 2 * p) = true.
Definition div_2_even_number n (nP : even n) : {p | (n == 2 * p) = true} :=
Sub (xchoose nP) (xchooseP nP).
```

The `xchoose : (exists n, P n = true) -> nat`

function performs the above search, and `xchooseP`

shows that the its result satisfies the boolean predicate. (The actual types are more general than this, but when instantiated to `nat`

they yield this signature.) I have used the boolean equality operator to simplify the code, but it would have been possible to use `=`

instead.

That being said, if you care about running your code, programming in this fashion is terribly inefficient: you need to perform `n / 2`

`nat`

comparisons to test divide `n`

. It is much better to write a simply typed version of the division function:

```
Fixpoint div2 n :=
match n with
| 0 | 1 => 0
| S (S n) => S (div2 n)
end.
```

You are working with types in different sorts.

```
> Check (Nat.Even 8).
Nat.Even 8
: Prop
> Check {p:nat | 8=p+p}.
{p : nat | 8 = p + p}
: Set
```

A feature of the Coq type system is that you can not eliminate a value whose type is in `Prop`

to obtain something whose type is not in `Prop`

(roughly -- some exception is done by Coq for `Prop`

types which carry no information, like `True`

and `False`

, but we are not in that case). Roughly put you can not use a proof of a proposition for anything but to prove another proposition.

This limitation is unfortunately required to allow `Prop`

to be impredicative (we want `forall P: Prop, P->P`

to be a type in sort `Prop`

) and to be consistent with the law of excluded middle. We can not have everything or we meet Berardi's paradox.