Writing `if set is empty` and getting element from singleton

Stream: new members

[An Qi Zhang]

Hello! I was wondering if it's possible to use a Set s being empty (s = ∅) in the condition of an if-then-else statement? When I write this directly in Lean, it throws an error saying it failed to synthesize (Decidable s = ∅), so is there a specific way I need to write this to implement checking if a set is empty in Lean?

Also, if I have a Prop that states a set is singleton, how do I "extract" the single element from Set s?

Here's a MWE to help illustrate the two questions above:

import Mathlib

abbrev SetNat := Set Nat

def Set.isSingleton {α : Type} (s : Set α) : Prop := ∃ e, s = {e}

def empty_or_singleton (sn : SetNat) : Prop := sn = ∅ ∨ sn.isSingleton

/- Either return none or the single element from a set -/
def GetNat (sn : SetNat) (h_e_or_s : empty_or_singleton sn) : Option Nat :=
  if sn = ∅ then -- How do I state this case without a `failed to synthesize` message?
    none
  else
    -- Here, I want to use h_e_or_s to get the unique nat out of sn. How do I do this?
    sorry

[Kevin Buzzard]

Quick fix: write open scoped Classical in before the declaration

[Kevin Buzzard]

Then all decidability problems magically go away

[Kevin Buzzard]

And write if h : sn = \empty to get the hypothesis h which you need

[Aaron Liu]

import Mathlib

abbrev SetNat := Set Nat

def Set.isSingleton {α : Type} (s : Set α) : Prop := ∃ e, s = {e}

-- this already exists as `Set.Subsingleton`
def EmptyOrSingleton (sn : SetNat) : Prop := sn = ∅ ∨ sn.isSingleton

/- Either return none or the single element from a set -/
noncomputable def getNat (sn : SetNat) (h_e_or_s : EmptyOrSingleton sn) : Option Nat :=
  by classical exact
  if h : sn = ∅ then
    none
  else
    (some (h_e_or_s.resolve_left h).choose)

theorem getNat_empty : getNat ∅ (Or.inl rfl) = none := by
  rw [getNat, dif_pos rfl]

theorem getNat_singleton (x : Nat) : getNat {x} (Or.inr ⟨x, rfl⟩) = some x := by
  rw [getNat, dif_neg (Set.singleton_ne_empty x)]
  have hx {e : Nat} (hx : ({x} : SetNat) = {e}) : x = e :=
    Set.singleton_eq_singleton_iff.mp hx
  generalize_proofs he
  rw [← hx he.choose_spec]

[Eric Wieser]

Kevin Buzzard said:

Quick fix: write open scoped Classical in before the declaration

A slightly better rule is "write it before the if"