Stream: Coq users

Topic: Large inductive example from CPDT accepte

Daniel Hilst Selli (Jul 22 2022 at 13:45):

I was reading this http://adam.chlipala.net/cpdt/html/Universes.html
And it gives me this example, which was supposed to be rejected by Coq but is accepted, is there any heuristics going on that I'm not aware of?

Inductive exp : Set -> Set :=
| Const : forall T : Set, T -> exp T
| Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
| Eq : forall T, exp T -> exp T -> exp bool.

Also he says This definition is large in the sense that at least one of its constructors takes an argument whose type has type Type. But I don't see what constructor takes a type here, I tried the example expecting to get the problematic constructor highlighted in the PG but no, it's just accepted

Janno (Jul 22 2022 at 13:47):

It is rejected for me on 8.15.1

Daniel Hilst Selli (Jul 22 2022 at 13:48):

Maybe I have a flag enabled that I'm not aware of

Janno (Jul 22 2022 at 13:48):

Can you do Print exp. and show the output?

Daniel Hilst Selli (Jul 22 2022 at 13:49):

Inductive exp : Set -> Set :=
    Const : forall T : Set, T -> exp T
  | Pair : forall T1 T2 : Set, exp T1 -> exp T2 -> exp (T1 * T2)
  | Eq : forall T : Set, exp T -> exp T -> exp bool.

Arguments exp _%type_scope
Arguments Const _%type_scope _
Arguments Pair (_ _)%type_scope _ _
Arguments Eq _%type_scope _ _

Paolo Giarrusso (Jul 22 2022 at 13:49):

fails for me

Janno (Jul 22 2022 at 13:50):

Okay, I suspect you do have some flag enabled. I was hoping Coq had just replaced -> Set with -> Type (it does that for Prop sometimes) but the output looks exactly the same as the definition so it can't be that.

Paolo Giarrusso (Jul 22 2022 at 13:50):

@Daniel Hilst Selli this is large because Const takes a Set

Paolo Giarrusso (Jul 22 2022 at 13:51):

can you test this in a standalone file?

Daniel Hilst Selli (Jul 22 2022 at 13:52):

Okay, is something in my editor :

coqc /tmp/Foo.v
File "/tmp/Foo.v", line 1, characters 0-168:
Error: Large non-propositional inductive types must be in Type.

Kenji Maillard (Jul 22 2022 at 13:52):

The 3 constructors are taking arguments in Type (or rather in Set). For your definition to be accepted I guess Set is set to be impredicative in some way (for instance with the option -impredicative-set) ?

Paolo Giarrusso (Jul 22 2022 at 13:52):

you might be using some library that disables universe checking, _or_ some setting in _CoqProject

Paolo Giarrusso (Jul 22 2022 at 13:52):

@Kenji Maillard no, this is too impredicative

Paolo Giarrusso (Jul 22 2022 at 13:53):

impredicative strong sums break strong normalization

Paolo Giarrusso (Jul 22 2022 at 13:54):

you can use -type-in-type :-)

Paolo Giarrusso (Jul 22 2022 at 13:54):

(or however that's called in Coq)

Gaëtan Gilbert (Jul 22 2022 at 13:54):

this is accepted with impredicative-set, but squashed

Kenji Maillard (Jul 22 2022 at 13:54):

This work though:

Inductive exp : Prop -> Prop :=
    Const : forall T : Prop, T -> exp T
  | Pair : forall T1 T2 : Prop, exp T1 -> exp T2 -> exp (T1 /\ T2)
  | Eq : forall T : Prop, exp T -> exp T -> exp True.

Paolo Giarrusso (Jul 22 2022 at 13:55):

I spoke too quickly: the problem is with _injective_ constructors.

Daniel Hilst Selli (Jul 22 2022 at 13:56):

Okay, I was using PG for a long time in the same living emacs process I closed emacs, start it again, and open the file with the example and now it rejects on the editor too, so I suspect that there is some configuration getting persisted which I don't know why but at last I know how to work around it, thanks, guys!

Daniel Hilst Selli (Jul 22 2022 at 13:59):

So about the question, because in the Const forall T : Set, T type is Set and exp type is Set -> Set this is considered large, right?

Paolo Giarrusso (Jul 22 2022 at 14:02):

Basically yes. Another large datatype, working but squashed with -impredicative-set — here we can define it but can't extract the T out of it:

Inductive exp : Set :=
| Const : forall T : Set, T -> exp.

(* | Const : forall T : Set, T -> exp T. *)
(* | Pair : forall T1 T2, exp T1 -> exp T2 -> exp (T1 * T2)
| Eq : forall T, exp T -> exp T -> exp bool. *)
Definition f (e : exp) : Set.
Proof.
  Fail destruct e.

Gaëtan Gilbert (Jul 22 2022 at 14:06):

Daniel Hilst Selli said:

So about the question, because in the Const forall T : Set, T type is Set and exp type is Set -> Set this is considered large, right?

there is no forall T : Set, T, it's parenthesized as forall T : Set, (T -> exp T)
it's large because the argument of Const T : Set is large ie because its type Set is in Type > Set

Daniel Hilst Selli (Jul 22 2022 at 14:47):

Oh I was reading it as (forall T : Set, T) -> exp

Daniel Hilst Selli (Jul 22 2022 at 14:49):

So, is it correct to say that I cannot parameterize a Set by another Set?

Gaëtan Gilbert (Jul 22 2022 at 15:06):

no, you can do eg Inductive prod (A B : Set) : Set := pair : A -> B -> prod A B. without problem

Gaëtan Gilbert (Jul 22 2022 at 15:07):

note here that A and B are parameters of the inductive (on the left of the :) not just arguments to the constructor

Last updated: Apr 18 2024 at 06:01 UTC