Zulip Chat Archive

Stream: general

Topic: large vs small elimination


Reid Barton (Mar 29 2019 at 21:05):

For each inductive type or structure Lean has to decide whether to generate large or small eliminators (eliminating to a type in an arbitrary universe, or only to a proposition). As I understand it, the algorithm is something like this.

  • If the target universe of the inductive type is a Type (Sort u for u >= 1), then always generate a large eliminator.
  • If the target universe is Prop, then only generate a large eliminator if there's at most one constructor and all of its fields are Props.

However, with universe polymorphism, the target universe might be Prop for some values of the universe parameters but not others. Currently Lean just rejects such definitions. That means you cannot define a structure like

universe u
structure a (x : Sort u) : Sort u := (f : x)

You have to use a target universe of Sort (max u 1) or similar. This causes some minor issues in #824 where we want to replace Type by Sort in category theory.

Would it be possible/sound for Lean to instead do the following?

  • Solve for the universe variable substitutions which cause the target universe to become Prop = Sort 0, if possible. (This can be done in a simple syntax-directed way: max u v = 0 iff u = 0 and v = 0; imax u v = 0 iff v = 0; u+1 is never 0; etc.)
  • If there are such substitutions, then apply them before doing the large eliminator check for Props.

In the example, a large eliminator would be generated for a, because when the target universe is Prop, the field f is also a Prop.

Are there other reasons that Lean needs to know whether or not the target universe is a Prop?

Mario Carneiro (Mar 29 2019 at 21:42):

This would obviously require a modification to lean's kernel, but I can confirm soundness against the paper proof.

Mario Carneiro (Mar 29 2019 at 21:43):

I think lean will accept inductive types in Sort u under some circumstances; there are weird consequences in general, but it should be fine for large eliminating inductives

Mario Carneiro (Mar 29 2019 at 21:45):

In particular, lean seems to have no trouble with the structure you gave, if you use an inductive instead:

inductive {u} foo (α : Sort u) : Sort u
| mk : α  foo

Reid Barton (Mar 29 2019 at 21:45):

Oh interesting

Reid Barton (Mar 29 2019 at 21:47):

It only generates a small eliminator, though

Mario Carneiro (Mar 29 2019 at 21:50):

ah yes, that's the weird consequence

Mario Carneiro (Mar 29 2019 at 21:51):

that's why the structure won't work, of course


Last updated: Dec 20 2023 at 11:08 UTC