The Coq mailing list

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

Oops sorry for that! There is a decidibility hypothesis
on Q n missing there (as Yannick Forster pointed me out ;-)

> 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 }

The correct definition for re is of course:

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

It is always a good idea to type-check your terms before
posting them ;-) see below for proofs

DLW

Section RE_reif.

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

  Definition re {X} (P : X -> Prop) :=
     { Q : nat -> X -> Prop
         & (forall n, dec (Q n))
         * (forall x, P x <-> exists n, Q n x) }%type.

  Variables (CE : forall P : nat -> Prop, dec P -> (exists x, P x) -> {
x | P x })
            (s : nat -> nat*nat) (Hs : forall p, exists n, s n = p).

  Theorem RE_reif (P : nat -> Prop) : re P -> (exists x, P x) -> { x | P
x }.
  Proof.
    intros (Q & H1 & H2) H3.
    set (R n := let (x,y) := s n in Q x y).
    destruct CE with R as (n & Hn).
    + intros n; unfold R; destruct (s n); apply H1.
    + destruct H3 as (x & Hx).
      apply H2 in Hx.
      destruct Hx as (y & Hy).
      destruct (Hs (y,x)) as (n & Hn).
      exists n; red; rewrite Hn; trivial.
    + red in Hn.
      destruct (s n) as (x,y).
      exists y; apply H2; exists x; trivial.
  Qed.

End RE_reif.

> 
> 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
>>
>>
>