Zulip Chat Archive

Stream: new members

Topic: Nonempty or empty


view this post on Zulip 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.

view this post on Zulip Patrick Stevens (Jul 12 2020 at 15:12):

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

view this post on Zulip Patrick Stevens (Jul 12 2020 at 15:13):

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

view this post on Zulip Reid Barton (Jul 12 2020 at 15:13):

This version is not provable

view this post on Zulip Johan Commelin (Jul 12 2020 at 15:14):

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

view this post on Zulip 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.

view this post on Zulip Ruben Van de Velde (Jul 12 2020 at 15:16):

Maybe #xy

view this post on Zulip Johan Commelin (Jul 12 2020 at 15:31):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Jul 12 2020 at 16:59):

Thanks all!

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip Mario Carneiro (Jul 12 2020 at 20:27):

the correct statement is not (nonempty A) :)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Kenny Lau (Jul 12 2020 at 20:35):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Jul 12 2020 at 21:00):

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

view this post on Zulip Scott Morrison (Jul 12 2020 at 23:17):

Me too!

view this post on Zulip 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