empty type

Stream: general

[David Spivak]

I'm brand new to lean. How do I map out of the Empty type?
For example, I want to write this:

def bang0 { T : Type } : Empty -> T :=          -- what goes here?

[Scott Morrison]

Hi David!

[Scott Morrison]

I would probably write:

import Mathlib.Tactic.Common -- or import Std.Tactic.RCases if you're happy to use Std but not Mathlib

def bang0 { T : Type } : Empty -> T := by
  rintro ⟨⟩

[Scott Morrison]

which says: "introduce an argument, at the same time deconstructing it", and Lean works out that there was no way to deconstruct an Empty.

[David Spivak]

Hey Scott!! Thanks! I think I have work to do, because it says "unknown package 'mathlib'," which seems like a me problem.

[Scott Morrison]

Just updated my code block to include imports. You're allowed to say #mwe to people who forget to do that. :-)

[Scott Morrison]

If you're in a brand new project with no imports, then

def bang0 { T : Type } : Empty -> T := by
  intro x
  cases x

[Scott Morrison]

But we should get you up to speed with Mathlib, because it has lots of goodies that make writing proofs easier.

[David Spivak]

That got it. Thanks!

[Scott Morrison]

Did you already create a project using lake new?

[Scott Morrison]

Once you've got imports working, I can show you the tactics that you would use to find the answer above even if you didn't already know it.

[David Spivak]

no, it's all just in my local repo. I don't know about lake new.

[David Spivak]

bang0 didn't work as well as i hoped: I have a type that reduces to Empty, but Lean doesn't seem to know that; I try calling bang0 and Lean doesn't realize it applies.

[David Spivak]

Anyway, thanks Scott, but I should stop for the night; I'm feeling the RSI flaring up a bit. Lean is too fun! I'll look into Lake and mathlib soon.

[Johan Commelin]

David Spivak said:

bang0 didn't work as well as i hoped: I have a type that reduces to Empty, but Lean doesn't seem to know that; I try calling bang0 and Lean doesn't realize it applies.

It depends a bit on what you mean by "reduces", but it might be possible to use Empty.elim or something like that. Then Lean will try to unify your expression with Empty and hopefully realise that it works.

[Kevin Buzzard]

Note that "the empty type Empty" is different to "a type which I can prove has no terms"; unlike in set theory there is more than one empty type in type theory. The most effective way to ask questions here is to post a #mwe (this is a link explaining more).

[Ioannis Konstantoulas]

Isn't the simplest way to map out Empty.rec ?

example {out : Sort u} : Empty → out :=
  Empty.rec

[Eric Wieser]

docs#isEmptyElim is more general

[David Spivak]

Empty.rec works!!!! Thanks!

[Matthew Ballard]

import Std

example {out : Sort u} : Empty → out := fun.

There were a couple of fun threads on this (which I cannot track down at the moment). Do we have the dot?

[Eric Wieser]

Yes, but it requires import Std (or less)