Stream: Coq users

Topic: Large inductive example from CPDT accepte


view this post on Zulip 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

view this post on Zulip Janno (Jul 22 2022 at 13:47):

It is rejected for me on 8.15.1

view this post on Zulip Daniel Hilst Selli (Jul 22 2022 at 13:48):

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

view this post on Zulip Janno (Jul 22 2022 at 13:48):

Can you do Print exp. and show the output?

view this post on Zulip 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 _ _

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 13:49):

fails for me

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 13:50):

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

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 13:51):

can you test this in a standalone file?

view this post on Zulip 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.

view this post on Zulip 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) ?

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 13:52):

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

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 13:52):

@Kenji Maillard no, this is too impredicative

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 13:53):

impredicative strong sums break strong normalization

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 13:54):

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

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 13:54):

(or however that's called in Coq)

view this post on Zulip Gaëtan Gilbert (Jul 22 2022 at 13:54):

this is accepted with impredicative-set, but squashed

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jul 22 2022 at 13:55):

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

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Daniel Hilst Selli (Jul 22 2022 at 14:47):

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

view this post on Zulip Daniel Hilst Selli (Jul 22 2022 at 14:49):

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

view this post on Zulip 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

view this post on Zulip 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: Feb 06 2023 at 13:03 UTC