The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Morgan,

I am not Coq expert, so take my answer with grain of salt.  For your first question, you can have a look at constructiveEpsilon[1] library, specially  ConstructiveGroundEpsilon.

Variable A : Type.
Variable f : A -> nat.
Variable g : nat -> A.

Hypothesis gof_eq_id : forall x : A, g (f x) = x.
Variable P : A -> Prop.
Hypothesis P_decidable : forall x : A, {P x} + {~ P x}.

Definition P' (x : nat) : Prop := P (g x).

Lemma P'_decidable : forall n : nat, {P' n} + {~ P' n}.
Lemma constructive_indefinite_ground_description : (exists x : A, P x) -> {x : A | P x}.

If you can show one to one correspondence with nat and your type ftree with proof of gof_eq_id and  P_decidable, then using constructive_indefinite_ground_description you can turn (exists x : A, P x) to {x : A | P x} (computational content) which is probably you are looking for.

I don't have any precise answer for your second question, but have a look at Arthur's answer about Prop and bool [2]. If you can turn your connectives in Fixpoint valid (P : ftree) : Prop := ... in such a way that it returns bool then you would have function which computes.  Also, feel free to share your code.

Best,

Mukesh

On Thu, Apr 11, 2019 at 7:31 AM 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:

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!

[1] https://coq.inria.fr/library/Coq.Logic.ConstructiveEpsilon.html

[2] https://stackoverflow.com/questions/31554453/why-are-logical-connectives-and-booleans-separate-in-coq/31568076#31568076