golfing Subsingleton Empty

Stream: lean4

[Kevin Buzzard]

I am supposed to give a lecture on numbers to some physicists/philosophers in a month or so, and I thought I'd try defining naturals as equivalence classes of finite types. I'm pretty sure I could do it in Lean 3 without too much trouble so I thought I'd try in Lean 4 as it sounds like a nice beginner exercise. When proving that subsingleton types were finite I ran into the issue that Subsingleton Empty is not yet an instance in Lean 4 (or maybe I am missing an import). In Lean 3 one could do

def foo : ∀ (a b : empty), a = b.

example : subsingleton empty := subsingleton.intro foo

-- this is the equation compiler being super-smart to make foo and then we can feed it into the constructor. But of course it would be nicer if we didn't have to make foo at all. Without the auxiliary definition in Lean 3 one can't (as far as I know) invoke the equation compiler, and one has to do something like

example : subsingleton empty := subsingleton.intro $ λ a b, by cases a

or (with mathlib)

import tactic

example : subsingleton empty := subsingleton.intro $ by rintro ⟨⟩

In Lean 4 the tactic proof works fine

instance : Subsingleton Empty where
  allEq := λ a b => by cases a;

but is there some nifty equation compiler trickery which can make this even smaller than the Lean 3 proofs?

[Sebastian Ullrich]

The Lean 4 equivalent is

instance : Subsingleton Empty where
  allEq a b := nomatch a

[Sebastian Ullrich]

(for maximum golfing elide the b)

[Mario Carneiro]

how about

instance : Subsingleton Empty where
  allEq := nofun

?

[Mario Carneiro]

it is unfortunate that there isn't a way to express nomatch a as match a <something> because the latter would also apply to all pattern matching contexts like def, let rec, match, fun, intro etc

[Mario Carneiro]

remind me why <something> can't be the empty string?

[Mario Carneiro]

It could be surrounded by parentheses if it's ever ambiguous. So (fun) is the empty function, (match a) is nomatch, intro... not sure