## Stream: new members

### Topic: Nonempty or empty

#### Heather Macbeth (Jul 12 2020 at 15:10):

Is there a lemma which will divide my proof into cases, depending on whether or not a type α is nonempty? I tried things like

example (α : Type*) : (α = empty) ∨ nonempty α := by library_search


with no luck.

#### Patrick Stevens (Jul 12 2020 at 15:12):

Could you quickly run over why you want this? I fear an #XY

#### Patrick Stevens (Jul 12 2020 at 15:13):

er, however we summon a link to something like https://en.wikipedia.org/wiki/XY_problem

#### Reid Barton (Jul 12 2020 at 15:13):

This version is not provable

#### Johan Commelin (Jul 12 2020 at 15:14):

@Heather Macbeth by_cases h : nonempty \a should work. I hope...

#### Rob Lewis (Jul 12 2020 at 15:14):

if h : nonempty α then _ else _, or tactic mode by_cases h : nonempty α, which are on some level going down to em. You probably don't want the negated case to say α = empty.

Maybe #xy

#### Johan Commelin (Jul 12 2020 at 15:31):

Why all the XY? This seems like a very reasonable case split to me.

#### Jalex Stark (Jul 12 2020 at 16:24):

i've had success with by_cases h: nonempty \a, and then later haveI := h to tell typeclass inference what happened

#### Bhavik Mehta (Jul 12 2020 at 16:54):

I think if you do resetI after the cases you won't get duplicated names in your goal state - not that this matters that much in this case but it might be tidier at least

Thanks all!

#### Kyle Miller (Jul 12 2020 at 20:15):

Heather Macbeth said:

example (α : Type*) : (α = empty) ∨ nonempty α := by library_search


Is this statement true? It seems it would imply types have some kind of extensional equality in Lean. Is there a way to fill in the following sorry?

inductive my_empty : Type

example : my_empty = empty := sorry


#### Heather Macbeth (Jul 12 2020 at 20:18):

Yeah, I think it's not true, this was meant to be a placeholder for whatever the correct statement was :)

#### Mario Carneiro (Jul 12 2020 at 20:27):

the correct statement is not (nonempty A) :)

#### Kyle Miller (Jul 12 2020 at 20:28):

Ok, thanks, I wasn't sure whether empty types were somehow special.

It would be silly, but there could be an is_empty typeclass:

class inductive {u} is_empty (α : Sort u) : Prop
| intro (no_val : α → false) : is_empty

example (α : Type*) : is_empty α ∨ nonempty α :=
begin
by_cases h : nonempty α,
right, assumption,
left,
constructor, intro x,
apply h,
exact nonempty.intro x,
end


#### Mario Carneiro (Jul 12 2020 at 20:33):

Once upon a time there was a version of not that worked on types. It was dropped for lack of use

#### Mario Carneiro (Jul 12 2020 at 20:34):

I realize not nonempty looks a bit funny but it has exactly the desired meaning; you can prove it is equivalent to A -> false and use it in the obvious way fairly easily

#### Kenny Lau (Jul 12 2020 at 20:35):

I guess the problem is that currently there is no idiomatic way to say "this type is empty"

#### Kenny Lau (Jul 12 2020 at 20:35):

A -> false, A \equiv empty, \n (nonempty A), etc

#### Mario Carneiro (Jul 12 2020 at 20:36):

If you search for those three I hope you will find the last one being most common

#### Kevin Buzzard (Jul 12 2020 at 20:51):

Chris Hughes and I were talking about this on Thursday at Xena and he encouraged me to use A -> false

#### Bhavik Mehta (Jul 12 2020 at 21:00):

Yeah I (independently) thought the first was the standard idiom in mathlib

Me too!

#### Scott Morrison (Jul 12 2020 at 23:17):

Sounds like we should standardise a bit here --- possibly by introducing a declaration specifically for this??

Last updated: May 11 2021 at 22:14 UTC