The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Le 11/04/2019 à 09:41, Morgan Sinclaire a écrit :
> 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?

- "forall" works also on "Type".
- use "*" (ie "prod") for "/\".
- use "{x : A | P x}" (ie "sig") or {x : A & P x} (ie "sigT")  for "exists",
- use "+" (ie "sumor") for "\/".

You can still use "False" as the empty type.




> 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