unique term inhabiting the unit

Stream: mathlib4

[Dean Young]

I'm looking for answers to these two questions:

def constituent  : Unit := ?
def uniqueness : forall (x : Unit), forall (y : Unit) (x = y) := ?

[Kevin Buzzard]

Right click on the definition of Unit and jump to its definition to see the answers!

[Mario Carneiro]

I think even the docstring will answer one of them

[Kevin Buzzard]

It's spelt like this by the way:

def constituent : Unit := sorry
def uniqueness : ∀ (x : Unit) (y : Unit), (x = y) := sorry

(maybe jumping to definition doesn't work if there are syntax errors everywhere)

[Kevin Buzzard]

Actually the second one isn't immediately obvious from the definition :-(

def constituent : Unit := Unit.unit
def uniqueness : ∀ (x : Unit) (y : Unit), (x = y) := Subsingleton.elim

[Mario Carneiro]

the second question is less obvious, the exact answer is PUnit.subsingleton but Subsingleton.elim is the more general version

[Mario Carneiro]

we should put info about Subsingleton in the Unit docstring

[Yaël Dillies]

The second shouldn't be a def, Kevin :wink:

[Kevin Buzzard]

import Mathlib

def constituent : Unit := Unit.unit
theorem uniqueness : ∀ (x : Unit) (y : Unit), (x = y) := by library_search -- works

[Kevin Buzzard]

library_search is a useful tool to answer questions of the form "how do I do this thing which is probably in the library"

[Scott Kovach]

mildly interesting: I tried library_search here and it gave me fun a b ↦ rfl, avoiding the case analysis needed in lean3. can anyone explain why rfl alone works in lean4?

[Eric Wieser]

I think this might be a weird case of the new structure eta feature that makes Prod.Mk x.1 x.2 = x, but for Unit which has no arguments

[Scott Kovach]

you're right! but actually intentionally supported: https://github.com/leanprover/lean4/issues/777#issuecomment-977970138