The Coq mailing list

[Morgan Sinclaire <morgansinclaire AT boisestate.edu>]

Thank you for the responses, but I want to emphasize again that my predicate "valid" is not decidable, otherwise I could've just made it boolean in the first place. I think that rules out Sigma types, but I'd like to be wrong about that. I am glad I know about ConstructiveGroundEpsilon now, and that certainly looks close to what I need, but if the "P : A -> Prop" is supposed to be be my "valid" predicate, then that also won't work because it's not undecidable.

Here is my current code for full details, the relevant stuff starts on line 3643. Let me try to explain my situation a little bit more fully (but without going into all the weeds):

I have a data structure called ftree ("formula tree") which consists of infinitely branching trees decorated with formulas. The definition has 19 constructors corresponding to the rules of inference in this system, and looks like:

Inductive ftree : Type :=
| node : formula -> ftree            (* axiom *)
...
| w_rule_a : formula -> nat -> (nat -> ftree) -> ftree
...

It is infinitely branching because of w_rule_a. What I'm trying to do is represent proofs in a certain infinitary logic, so the infinite branching is there intentionally. I can decidably extract the formula at the root of an ftree (the conclusion of a proof):

Fixpoint ftree_formula (P : ftree) : formula :=
match P with
| node A => A
...
| w_rule_a A n g => univ n A
...

Where "univ n A" denotes the formula "forall x_n, A". I say that an a given ftree P is valid iff it actually represents a proof in this infinitary system:

Fixpoint valid (P : ftree) : Prop :=
match P with
| node A => PA_omega_axiom A = true
...
| w_rule_a A n g => forall (m : nat),
    ftree_formula (g m) = substitution A n (represent m) /\ valid (g m)
...

Where "substitution A n (represent m)" denotes the formula "A[m/x_n]", so the w_rule_a means that if we have a function g: nat -> ftree such that for every m, (g m) is a proof of A(m), then we can infer forall x_n A(x_n).

So in this infinitary system, it is not decidable to determine if a given ftree is valid, since that would require reasoning about the halting of any given g.

Finally, I define the predicate on formulas:

Definition provable (A : formula) : Prop :=

  exists (t : ftree), ftree_formula t = A /\ valid t.

Now I'm trying to prove a technical lemma that involves inducting over ftree, and the place I'm stuck is:

A : formula
n : nat
H : forall m : nat,
    exists t : ftree, ftree_formula t = substitution A n (represent m) /\ valid t
______________________________________(1/1)
exists t : ftree, ftree_formula t = univ n A /\ valid t

So to prove the goal, I need to use "w_rule_a", which means I need a function g: nat -> ftree satisfying the required properties. By Curry-Howard, that function should be H itself, but this doesn't seem to work because I (apparently) can't extract the needed computational content from H.

So is it completely hopeless since valid is undecidable in general? I feel like what I'm trying to do makes sense if one takes Curry-Howard literally, and if so there should be some workaround.

P.S. One other thing I tried was defining "provable" instead as a sig:

Definition provable (A : formula) : Type :=
  {t : ftree | ftree_formula t = A /\ valid t}.

But then the induction setup I'm using to prove this lemma totally breaks, with the error:

Cannot find the elimination combinator PA_omega_theorem_rec, the elimination of the inductive definition PA_omega_theorem on sort Set is probably not allowed.

 

I don't think I can avoid that, but if this is the recommended route, I'll probably have to give more details about this lemma.

On Wed, Apr 10, 2019 at 7:01 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

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