Zulip Chat Archive

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.

Ruben Van de Velde (Jul 12 2020 at 15:16):

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

Heather Macbeth (Jul 12 2020 at 16:59):

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

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

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: Dec 20 2023 at 11:08 UTC