The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Morgan,

I was wondering whether your tree structure was abstract or whether
it was somehow "enumerable" in which case you could have an easy
way out. Looking at the below rule

 | w_rule_a : formula -> nat -> (nat -> ftree) -> ftree

this lets some hope that the nodes of your trees could
be enumerated by nat.

Then you could use a slight generalization of Constructive
Epsilon. Indeed, Constructive Epsilon states that decidable
predicates over nat can be reified from Prop to Type.

CE: forall P : nat -> Prop, dec P -> (exists x, P x) -> { x | P x }.

where dec {X} (P : X -> Prop) := { P x } + { ~ P x }.

The algorithm corresponding to unbounded minimization.

You can easily weaken your hypothesis into
"P is recursively enumerable" ie

re {X} (P : X -> Prop) := { Q : nat -> X -> Prop
                          | forall x, P x <-> exists n, Q n x }

and prove

forall P : nat -> Prop, re P -> (exists x, P x) -> { x | P x }.

To do so, you simply surjectively encode pairs of nats by a
single nat and use CE.

So if your "valid" predicate, though not decidable,
is  still "recursively enumerable", you could be able
to find an easy way out.

Otherwise, general reification

(X -> inhabited Y) -> inhabited (X -> Y)

is not possible without adding axioms.
Which means (in case you want to avoid extra axioms)
that you need to rethink your hole argument.

It is certainly possible to move "valid" to Type
but if you use a lot of tools from the standard
library, this might involve rewriting all of them
in Type (at least for non-decidable ones).

If you want to stick with Prop, you might consider
replacing predicates like (exists t, valid t) with
a somewhat (a bit) weaker inductive predicate
over Prop, ie merging ftree with valid in a single
inductive definition.

Best of luck,

Dominique

Le 11/04/2019 à 07:32, Morgan Sinclaire a écrit :
> 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
> <https://github.com/Morgan-Sinclaire/Gentzen/blob/master/gentzen.v> 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
>  
> <mailto: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
>     
> <mailto: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
>         <http://adam.chlipala.net/cpdt/cpdt.pdf>, 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
> 
>