Stream: Coq users

Topic: Some Questions on Extraction


view this post on Zulip Ende Jin (Oct 07 2022 at 19:48):

I bumped into this error when extracting a function

The informative inductive type prod has a Prop instance
in is_exp_def.PN_allclauses_complete (or in its mutual block).
This happens when a sort-polymorphic singleton inductive type
has logical parameters, such as (I,I) : (True * True) : Prop.
The Ocaml extraction cannot handle this situation yet.
Instead, use a sort-monomorphic type such as (True /\ True)
or extract to Haskell.

  1. Is this problem purely about engineering or there are some theoretical limits causing this extraction impossible?

  2. I am using Type and Prop in a mixed way and thus I cannot just change every product type to conjunction type. What is the usual solution to it?

  3. I notice something weird:

Inductive Box (A : Prop) : Type :=
  | box : A -> Box A.

Check ((Box (1 = 1) /\ (2 = 2))). (* Why  can this be  type checked? *)

Fail Check (({k & k = 1} : Type) /\ 2 = 2).  (* I can understand this part because I always think Type is above Prop*)

view this post on Zulip Pierre-Marie Pédrot (Oct 07 2022 at 19:50):

For 1. it's essentially about engineering in your case but it has also some other potential foundational consequences

view this post on Zulip Pierre-Marie Pédrot (Oct 07 2022 at 19:51):

For 3. this is the dreaded template polymorphism

view this post on Zulip Gaëtan Gilbert (Oct 07 2022 at 20:08):

3 is not template poly, it's because Inductive foo ... : Type := ... means "put foo in the lowest possible universe" which in this case s Prop

view this post on Zulip Pierre-Marie Pédrot (Oct 07 2022 at 20:09):

OK, it's not template polymorphic but the fact it falls in Prop is precisely because of the broken syntax for template poly

view this post on Zulip Pierre-Marie Pédrot (Oct 07 2022 at 20:09):

well actually it is template poly, but has no template argument

view this post on Zulip Pierre-Marie Pédrot (Oct 07 2022 at 20:10):

so this doesn't change anything for the kernel but impacts the autogenerated recursors and some other stuff like injection tactic

view this post on Zulip Gaëtan Gilbert (Oct 07 2022 at 20:14):

even if we remove template poly that doesn't mean we would change the weird syntax imo

view this post on Zulip Pierre-Marie Pédrot (Oct 07 2022 at 20:14):

I always found infuriating that I explicitely write Type and Coq decides to put it in Prop nonetheless

view this post on Zulip Pierre-Marie Pédrot (Oct 07 2022 at 20:15):

(precisely because template poly must read your mind)

view this post on Zulip Ende Jin (Oct 07 2022 at 20:20):

Ok for 2 it seems like I can avoid it by using sigT2? where {A & B & C} by putting product type in B and conjunction prop in C, then extraction will be happy I don't have to mix them.

Now I finally know what this weird sigT2 is used for

view this post on Zulip Pierre-Marie Pédrot (Oct 07 2022 at 20:22):

@Ende Jin are you relying on the fact that prod A B : Prop when A : Prop and B : Prop in your code?

view this post on Zulip Pierre-Marie Pédrot (Oct 07 2022 at 20:22):

Otherwise you could redefine the product so as for it to not be template poly and you wouldn't have any trouble with extraction


Last updated: Feb 01 2023 at 11:04 UTC