Zulip Chat Archive

Stream: new members

Topic: reasoning about empty set in lean


view this post on Zulip Marcus Klaas (Dec 02 2018 at 17:09):

Hi y'all. Sorry to bother again. I'm having trouble working with the empty set. Specifically, I'd like to prove that a set is not empty whenever I can produce a concrete element of it:

example : { x | x = nat.succ nat.zero }   := sorry

but so far, I haven't been successful. What can I do here?

view this post on Zulip Rob Lewis (Dec 02 2018 at 17:10):

set.ne_empty_of_mem will probably be helpful!

view this post on Zulip Rob Lewis (Dec 02 2018 at 17:10):

You'll have to import data.set.basic from mathlib.

view this post on Zulip Marcus Klaas (Dec 02 2018 at 17:10):

Thanks! I will try it.

view this post on Zulip Kenny Lau (Dec 02 2018 at 17:12):

no import needed :)

example : { x | x = nat.succ nat.zero }   :=
λ H, (congr_fun H 1).mp rfl

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 17:13):

...says the person with over 1 year's Lean experience ;-)

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 17:13):

import data.set.basic

example : { x | x = nat.succ nat.zero }   :=
begin
  rw set.ne_empty_iff_exists_mem,
  use 1,
  exact rfl, -- refl doesn't work!
end

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 17:14):

refl is really bad at set membership.

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 17:15):

example (a : ℕ) : a ∈ {x : ℕ | x = a} := by refl -- fails

view this post on Zulip Reid Barton (Dec 02 2018 at 17:15):

I wonder whether we could fool it into working somehow

view this post on Zulip Marcus Klaas (Dec 02 2018 at 17:15):

Hmmm I don't seem to have the mathlib tho.. can I install it using elan? I have found a way to do it ^^

view this post on Zulip Reid Barton (Dec 02 2018 at 17:15):

basically by adding what Kevin just wrote as a relfexivity lemma

view this post on Zulip Kevin Buzzard (Dec 02 2018 at 17:17):

@Marcus Klaas mathlib is great. It's not just for mathematicians. It has a bunch of useful tactics in, and a whole host of useful data structures. If you work with Lean projects (as I do -- all my files, even scratch files, are within a Lean project) then you can just make mathlib a dependency for that project and then leanpkg upgrade will download mathlib.


Last updated: May 12 2021 at 04:19 UTC