Ende Jin (Oct 07 2022 at 19:48): 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.
Is this problem purely about engineering or there are some theoretical limits causing this extraction impossible?
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?
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*)
For 1. it's essentially about engineering in your case but it has also some other potential foundational consequences
Pierre-Marie Pédrot (Oct 07 2022 at 19:51):For 3. this is the dreaded template polymorphism
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
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
Pierre-Marie Pédrot (Oct 07 2022 at 20:09):well actually it is template poly, but has no template argument
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
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
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
Pierre-Marie Pédrot (Oct 07 2022 at 20:15):(precisely because template poly must read your mind)
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
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?
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: Apr 20 2024 at 09:01 UTC