Basic set equalities (e.g. `(s \ t)ᶜ = sᶜ ∪ t`)

Stream: new members

[Adomas Baliuka]

I needed the set equality (s \ t)ᶜ = sᶜ ∪ t, which doesn't seem to be in Mathlib, although it seems common (Wikipedia's "Set Complement" mentions it). That should mean it's very easy?! I did it eventually (see below for completeness) but isn't there a simple way to prove this in one line? The tactics I usually try exact?, aesop, simp_all, rfl, trivial, apply? couldn't do it...

import Mathlib
open Set
variable {s t : Set α} {x : α}

lemma mem_and_notmem_of_in_diff : x ∈ s \ t ↔ (x ∈ s ∧ x ∉ t) := by simp

lemma mem_and_notmem_of_notin_diff : x ∉ s \ t ↔ (x ∉ s ∨ x ∈ t) := by
    have := Iff.not (@mem_and_notmem_of_in_diff α s t x)
    push_neg at this
    convert this -- I was hoping to be done here...
    constructor
    intro h xins
    simp_all only [false_or]
    intro h
    by_cases xins : x ∈ s
    · right; exact h xins
    · left; assumption

lemma compl_diff_eq_union_compl : (s \ t)ᶜ = sᶜ ∪ t := by
    ext x
    constructor
    · intro h
      have := (Set.mem_compl_iff (s \ t) x).mp h
      exact mem_and_notmem_of_notin_diff.mp this
    · intro h
      simp at h
      apply mem_compl
      apply mem_and_notmem_of_notin_diff.mpr
      exact h

[Riccardo Brasca]

This

import Mathlib

open Set
variable {s t : Set α} {x : α}

lemma compl_diff_eq_union_compl : (s \ t)ᶜ = sᶜ ∪ t := by
    nth_rewrite 2 [← compl_compl t]
    rw [← compl_inter]
    rfl

also works, let me see if I find the exact statement you want.

[Joël Riou]

Alternatively, we can do

import Mathlib.Data.Set.Basic

lemma compl_diff_eq_union_compl {α : Type*} (s t : Set α) :
    (s \ t)ᶜ = sᶜ ∪ t := by
  ext x
  simp only [compl_sdiff, Set.mem_union, Set.mem_compl_iff]
  tauto

[Adomas Baliuka]

How did you do this so quickly? I don't assume it's by having all these lemma names memorized.

[Joël Riou]

I did ext; simp?; tauto!

[Riccardo Brasca]

import Mathlib

open Set
variable {s t : Set α} {x : α}

lemma compl_diff_eq_union_compl : (s \ t)ᶜ = sᶜ ∪ t := by
    simp [himp_eq, Set.union_comm]

[Riccardo Brasca]

OK let's stop the golfing competition... but it's a result we surely want.

[Adomas Baliuka]

Thanks! I guess the takeaway for me is to add simp? to my "list of things to try". (Could one make a multi-threaded tactic that just tries all of exact?, aesop, simp_all, rfl, trivial, apply?, simp? at the same time and shows the first hit (or fails)?)

Actually, maybe my goal does exist in Mathlib after all as compl_sdiff. It uses a "Heyting implication" (the reason I didn't find it using loogle), which I've never heard of before...

[Riccardo Brasca]

Yeah, this is a more serious question. Heyting implication is something in Boolean algebra (and Set α is a Boolean algebra), so simp is applying docs#compl_sdiff, that says

(x \ y)ᶜ = x ⇨ y

Now, for sets it is completely ridiculous to say that the RHS is simpler than the LHS.

[Riccardo Brasca]

@Yaël Dillies what do you think? (pinging you because git blames you as the author of compl_sdiff, but it can be wrong).

[Yaël Dillies]

Riccardo Brasca said:

Now, for sets it is completely ridiculous to say that the RHS is simpler than the LHS.

You're free to add

@[simp] lemma Set.himp_eq (s t : Set α) : s ⇨ t = t ∪ sᶜ := himp_eq

[Yaël Dillies]

I think it's a bit of a shame since s ⇨ t has a very nice interpretation: elements of s ⇨ t exactly are the elements a such that a ∈ s → a ∈ t.

[Eric Wieser]

That seems like it might be a good example to add to the docstring for himp

[Yaël Dillies]

I swear I wrote that example in a docstring somewhere already, but I'm happy to make it more prominent!

[Eric Wieser]

docs#HImp.himp