The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi,

Having an undecidable predicate certainly rules out expressing it in
bool, but it does not rule out expressing it in Type. There are two
differences between Prop and Type: impredicative Prop vs predicate
Type hierarchy and the erasable status of Prop vs the extractable
status of Type (and BTW the fact that Coq used to have an extractable
impredicative sort Set shows that the two questions are separate:
https://coq.inria.fr/refman/language/cic.html#the-calculus-of-inductive-constructions-with-impredicative-set).
The decidability of a proposition hasn't anything to do with this. If
you define a predicate in Type, it is not more decidable than if you
define it in Prop. The difference is that if you are able to prove
that an element is in your predicate in Type, then you can extract a
computation from this proof (not the same thing, as this is not
generic but for a single element).

Thëo

Le jeu. 11 avr. 2019 à 07:33, Morgan Sinclaire
<morgansinclaire AT boisestate.edu>
 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 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