Zulip Chat Archive

Stream: lean4

Topic: pEmpty


Kevin Buzzard (Jun 17 2021 at 22:27):

inductive pEmpty : Sort u
/-
invalid universe polymorphic type, the resultant universe is not Prop (i.e., 0),
  but it may be Prop for some parameter values (solution: use 'u+1' or 'max 1 u'
  u
-/

Works fine in Lean 3. This inductive pEmpty : Type u works fine in Lean 4 but is there a way of leaving Prop open as a possibility?

Daniel Selsam (Jun 17 2021 at 23:28):

FYI there is a similar restriction in Lean3 but apparently only for structures:

structure foo : Sort u
/-
invalid universe polymorphic structure declaration,
the resultant universe is not Prop (i.e., 0),
but it may be Prop for some parameter values (solution: use 'l+1' or 'max 1 l')
-/

Daniel Selsam (Jun 17 2021 at 23:43):

FYI there is also a 5-year-old TODO to generate two recursors for such inductives: https://github.com/leanprover-community/lean/blob/master/src/kernel/inductive/inductive.cpp#L321-L322

Mario Carneiro (Jun 17 2021 at 23:49):

Because this is a large-eliminating type, it would actually be fine to have a Sort u inductive here. The kernel will accept the type and produce the right result, but the elaborator has the wrong heuristic and is rejecting the type

Daniel Selsam (Jun 17 2021 at 23:50):

Yes, I think the elaborator check is unnecessarily aggressive in this case. @Kevin Buzzard I suggest you create an issue for this.

Mario Carneiro (Jun 17 2021 at 23:51):

The same comment applies to Sort u structures

Mario Carneiro (Jun 17 2021 at 23:51):

as long as the inductive specification is large-eliminating, you can do the obvious thing to construct the projections

Mario Carneiro (Jun 17 2021 at 23:53):

(concretely, that means that a structure with no fields or with only Prop fields can live in Sort u)

Kevin Buzzard (Jun 18 2021 at 07:56):

lean4#537

Gabriel Ebner (Jun 18 2021 at 07:58):

You could also take a leaf out of the core Lean book and disable the check:

set_option bootstrap.inductiveCheckResultingUniverse false in
inductive PUnit : Sort u where
  | unit : PUnit

Last updated: Dec 20 2023 at 11:08 UTC