The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

> replace /\ by + (needs type scope)

this was of course incorrect, /\ is like *

Gaëtan Gilbert

On 11/04/2019 09:47, Gaëtan Gilbert wrote:
> forall isn't Prop specific
> replace /\ by + (needs type scope)
>
> Also it may be that you can keep [valid] in Prop, only doing
>      Definition provable (A : formula) :=
>        { t : ftree | ftree_formula t = A /\ valid t }.
>
> ( { x : T | P } is notation for sig )
> See proj1_sig and proj2_sig for how to get information out of it.
>
> Gaëtan Gilbert
>
> On 11/04/2019 09:41, Morgan Sinclaire wrote:
> > Thank you for that information! However, that still doesn't settle 
> > /how/ to convert a given Prop into Type. I have little idea how to do 
> > this since I've never done anything nontrivial with Type. For 
> > instance, my current definition has Prop-specific syntax like "forall" 
> > and "/\" and I wouldn't know what their equivalents in Type would be. 
> > Is there a good reference for this?
> >
> > On Thu, Apr 11, 2019 at 12:09 AM Théo Zimmermann <theo.zimmi AT gmail.com 
> > <mailto:theo.zimmi AT gmail.com>> wrote:
> >
> >     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
> >     
> > <mailto: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
> >  
> > <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, 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