The Coq mailing list

[CHA Reeseo <reeseo AT formal.korea.ac.kr>]

Dear all,

I am a PhD student studying formal methods in Korea university.  (I think
I have not introduced myself properly yet.)  I have two elementary
questions about proof-irrelevance or something.

Sometimes I want to define functions which calculate values (in sort Set)
depending not on the mere existence but on the concrete structure of some
proofs (in sort Prop).  As a simplified example, let me try to define a
function which converts each proof of 'ex P' into a corresponding
certified value:

    Coq < Definition foo {P} : (exists x, P x) -> { n:nat | P n }.
       ...
    foo < intros P H.
    1 subgoal

      P : nat -> Prop
      H : exists x : nat, P x
      ============================
       {n : nat | P n}

Though H already contains all the information needed (a natural number
together with a proof that that number satisfies P), I cannot extract
those information in this situation.  Any attempt such as 'destruct H',
'case H' or 'elim H' fails.  Even the definition of my own 'ex_rec' (for
eliminatig H) is also rejected:

    Definition my_ex_rec {A:Type} {P:A->Prop} {S:Set}
                         (f : forall x, P x -> S) (e:ex P) : S :=
      match e with
      | ex_intro x H => f x H
      end.

QUESTION 1: Is there really no way to retrieve detailed information from
the proofs of inductive predicates (whose final type is Prop) when the
current goal has sort Set?

                    *              *              *

By using eexists, (I thought) I detoured to a subgoal having sort Prop.
Now, even H can be destructed without any complaint:

    foo < eexists.
    1 subgoal

      P : nat -> Prop
      H : exists x : nat, P x
      ============================
       P ?6

    foo < destruct H as [x H].
    1 subgoal

      P : nat -> Prop
      x : nat
      H : P x
      ============================
       P ?7

QUESTION 2: Why 'eexact H' fails here?

    foo < eexact H.
    Toplevel input, characters 0-8:
    > eexact H.
    > ^^^^^^^^
    Error: Impossible to unify "?7" with "x".

Thanks in advance.  :^)

-- 
CHA Reeseo
http://www.reeseo.net/