The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi Morgan,

are you sure ftree infinitely branches? your predicate is a fixpoint though.

it depends on where your existential quantification is coming from. If it's a part of the statement of your lemma, you can indeed simply replace it with `sig` and it has some chance to work.

if the quantification comes from your predicate, you are in a bigger trouble. to begin with, your predicate needs to be turned a Type, and potentially other pain comes. you want to first revise your definitions and theorems and see if you depend on some elimination from other definitions in Prop. If that's the case, the change you need to make to turn your predicate into a Type is very hard to measure. judging from the size of your predicate, it might be difficult. more information is going to be helpful.

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Helmut Brandl <helmut.brandl AT gmx.net>
Sent: April 10, 2019 5:35 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] "exists" Extraction

 

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!