empty definition

Stream: general

[Violeta Hernández]

So, you know how unit is defined as punit.{0}? I wonder why the same isn't true for empty and pempty.{0}

[Yaël Dillies]

You mean pempty.{1}, right? pempty.{0} would be docs#false.

[Patrick Johnson]

The docstring for unit seems to be incorrect. Shouldn't it be punit.{1}?

[Reid Barton]

It probably predates Sort.

[Kevin Buzzard]

Good catch! I occasionally PR docstrings to core Lean and they're welcomed! In fact I suspect that my only contributions to core Lean are docstring additions/edits ;-)

[Violeta Hernández]

There's a few extra definitional equalities we could get, actually

[Violeta Hernández]

true could be def-eq to punit.{0}, false could be def-eq to pempty.{0}, and empty could be def-eq to pempty.{1}

[Violeta Hernández]

Sure, the extra convenience gains would be minor, but I can't see any way this could make things less convenient

[Violeta Hernández]

(of course, every time I've said this I've been wrong)

[Eric Wieser]

Would there be any point though?

[Eric Wieser]

I feel like the cost of confusing mathematicians by saying "oh, we call false pempty sometimes" already outweighs whatever minor benefit you're thinking of

[Violeta Hernández]

We'd get a few extra lemmas for free from their punit and pempty counterparts

[Violeta Hernández]

That's about it

[Eric Wieser]

Aren't those lemmas ones we already get from the is_empty version?

[Violeta Hernández]

That's fair

[Violeta Hernández]

The change empty = pempty.{1} should still make sense, though?

[Violeta Hernández]

If for nothing else, just for consistency with unit = punit.{1}

[Yaël Dillies]

I'm also happy for false to be redefined as pempty.{0}, but true shouldn't be redefined as punit.{0} because then we have the wrong name for the constructor (this is not a problem for false because there are no constructors!).

[Reid Barton]

false would have the wrong name for the eliminator though right?

[Junyan Xu]

Currently you can write:

• ⟨⟩, true.intro or trivial to construct a term of type true,
• ⟨⟩, () or unit.star to construct a term of type unit,
• ⟨⟩ or punit.star to construct a term of type punit,
  so ⟨⟩ is the most versatile/universal constructor. I don't know where () is defined! Seems there isn't a notation declaration.

[Yaël Dillies]

Reid Barton said:

false would have the wrong name for the eliminator though right?

You can provide false.elim separately.

[Yaël Dillies]

Isn't () handled separately by Lean because it's round brackets?

[Patrick Johnson]

Junyan Xu said:

I don't know where () is defined! Seems there isn't a notation declaration.

I think it's here.

[Yaël Dillies]

Ah yeah, so I was right.

[Junyan Xu]

Thanks! Should we / is it easy to make () universe polymorphic as well?

Yaël Dillies said:

Reid Barton said:

false would have the wrong name for the eliminator though right?

You can provide false.elim separately.

Don't we now have both docs#false.elim and docs#empty.elim / docs#pempty.elim? Interestingly false.elim is defined in terms of false.rec while the other two are defined by pattern matching (where there's no pattern).

[Yaël Dillies]

Don't those get compiled to the same thing anyway?

[Junyan Xu]

I think so, but in the docs the former shows one equation while the latter two show nothing.

[Junyan Xu]

Actually, doesn't seem to be the same syntactically:

@[inline]
def false.elim : Π {C : Sort u}, false → C :=
λ {C : Sort u} (h : false), false.rec C h
def empty.elim : Π {C : Sort u_1}, empty → C :=
λ {C : Sort u_1}, empty.elim._main
def pempty.elim : Π {C : Sort u_1}, pempty → C :=
λ {C : Sort u_1}, pempty.elim._main

[Junyan Xu]

from #print

[Junyan Xu]

and

def empty.elim._main : Π {C : Sort _aux_param_0}, empty → C :=
λ {C : Sort _aux_param_0} (ᾰ : empty), empty.cases_on (λ (ᾰ : empty), C) ᾰ

@[reducible]
protected def pempty.cases_on : Π (motive : pempty → Sort l) (n : pempty), motive n :=
λ (motive : pempty → Sort l) (n : pempty), pempty.rec motive n

so pattern matching definitions unfolds to cases_on; only when you unfold again you recover rec.

[Junyan Xu]

Other observations:
docs#psum, docs#sum and docs#or have the same constructor names inl, inr. or is not a special case of psum because it produces a Prop which is always a subsingleton, while psum produces a Type given two Props (so decidable p could in fact be defined to be psum (¬p) p).

psum currently has type Sort u → Sort v → Sort (max 1 u v). However, the following is also accepted by Lean:

inductive psum' (α : Sort u) (β : Sort v) : Sort (max u v)
| inl (a : α) : psum'
| inr (b : β) : psum'

It removes the 1 from max 1 u v, so should be as robust as the current sum against universe unification issues! (Maybe there is a small problem with the +1 from Type to Sort, I'm not sure.) Should it be promoted to the official sum (with or a special case)? We can then provide a separate psum just for the only special case Prop → Prop → Type that's not covered and use it to define docs#decidable.

docs#and has constructor names left and right while docs#prod and docs#pprod have the names fst and snd. In this case, it doesn't seem useful to have pprod : Prop → Prop → Type, since it doesn't retain any additional information like in the sum case, and if you want the resulting type to be in Type you can just lift it, so we may as well use one definition to encompass them all:

inductive pprod' (α : Sort u) (β : Sort v) : Sort (max u v)
| mk (fst : α) (snd : β) : pprod'

However, if you use structure then Lean complains:

structure pprod'' (α : Sort u) (β : Sort v) : Sort (max u v) :=
(fst : α) (snd : β)
/- 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') -/

Is it possible to make structure accept this? If we're unable to use structure, I think we lose the nice projections...

[Eric Wieser]

However, the following is also accepted by Lean:

#check psum'.rec tells you this isn't a useful definition

[Eric Wieser]

It only has a small eliminator

[Eric Wieser]

Which is why you can't pull the same trick for pprod, because the projections need large eliminators

[Junyan Xu]

Thanks! In hindsight it's clear the recursor can't be made universe polymorphic.