The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

In addition to the remark of Matthieu, you can prove the two
following results:

Theorem elem_prop (A:Set) (P:A->Prop) : (exists a:A, P a) -> inhabited A.
Proof.
  intros (a & _); exact (inhabits a).
Qed.

Theorem elem_set (A:Set) (P:A->Prop) : { a:A | P a } -> A.
Proof.
  intros (a & _); exact a.
Qed.

But in Coq, it is *not possible* to destruct a proof
(term of type A : Prop) while building a data (term of
type A : Type).

One of the consequences of this feature is that you do not
need realizers (proofs) for axioms (of type Prop) when you
extract programs. Coq programs cannot use the actual value
of proofs to compute their results. They can only use the
fact that a proof exists (though there is an exception
when there is *at most one* possible proof, eg you can
destruct A /\ B or False to build a term of type C : Type).

Hence, if you replace the logical (non-informative) "exists a, P a"
with the informative { a | P a }, then you can easily prove
elem_set.

Also, one can analyse a proof while building another
proof (eg as in theorem elem_prop).

As a general remark, be aware that reasoning about proofs is
usually very difficult because they constitute very complicated
programs. Unless it is absolutely needed, you do not want
to go down this path.

Best,

Dominique

-----------------------------------

On 11/18/2015 05:23 PM, Matthieu Sozeau wrote:
> Hi Patricia, 
> 
>   I guess you wanted to send this to 
> coq-club AT inria.fr
> <mailto:coq-club AT inria.fr>
>  instead of 
> coqdev AT inria.fr
> <mailto:coqdev AT inria.fr>
>  which is the developer mailing list.
> The short answer is you cannot eliminate an existential in Prop to 
> something in Set. This is a difference with the subset type {x : A | P
> x} which is also available in Coq.
> 
> Best,
> -- Matthieu
> 
> On Wed, Nov 18, 2015 at 4:32 PM Patricia Peratto 
> <psperatto AT vera.com.uy
> <mailto:psperatto AT vera.com.uy>>
>  wrote:
> 
>     I'm making a proof that involves the existential quantifier.
> 
>     I'want to get from a proof of a formula with this
>     quantifier the element that exists and the proof
>     of the proposition, i.e. "a" in the theorem below.
> 
>     Theorem elem (A:Set)(P:A->Prop) :
>     (exists a:A, P a) -> A.
>     intro.
>     elim H.
> 
>     When I try to prove elem, in elim H, I get
>     the message:
> 
>     Error: Cannot find the elimination combinator ex_rec, the
>     elimination of the
>     inductive definition ex on sort Set is probably not allowed.
> 
>     How can I do to get "a" and the proof of "(P a)"?
> 
>     Regards
>     Patricia
>