The Coq mailing list

[Helmut Brandl <helmut.brandl AT gmx.net>]

Just change ex to sig, see below.

On Apr 10, 2019, at 16:31, Morgan Sinclaire <morgansinclaire AT boisestate.edu> wrote:

I'm having trouble with extracting information from Prop, and specifically with the Prop/Type and ex/sig distinction which I wasn't aware of before. What I have is this definition:

Fixpoint valid (P : ftree) : Prop := ...

Where "ftree" is a certain infinitely-branching tree structure I've defined, and for this reason "valid" is undecidable in general.

Now I'm in the middle of a proof, where I have a hypothesis that looks like:

H : forall m : nat, exists t : ftree, valid t /\ [stuff about t]

And to complete my proof I need to produce a function of the form:

nat -> ftree

And by Curry-Howard, H should be such a function, but Coq doesn't believe so, because I can't extract computational information from "exists" (as discussed here, section 12.2).

Now, I know Coq does this because it wants to limit the amount of program extraction one can do, but in my case I want full Curry-Howard. So my first question is:

1) Can I "toggle" this feature in Coq so I can get full program extraction from "exists"?

If not, I don't know much about Sigma types, but I don't think I can just convert this "ex" into "sig" since the predicate "valid" is undecidable? I haven't worked with Type at all, so my other question:

You can use a sigma type. A sigma type contains a computable value and a proof that the value satisfies a predicate. In the extracted code only the value is visible, the proof is erased.

2) Is there an easy way to convert a Prop to a Type?

If so, I can change my definition of "valid" to be of type Type. Currently that definition is 63 lines and involves some Prop syntax such as "forall" and "/\", so any reference on how to do that in Type would be helpful so I can understand what I'm doing.

Thanks!