refactor(order/boolean_algebra): generalized Boolean algebras (#6775)

We add ["generalized Boolean algebras"](https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Generalizations), following a [suggestion](#6469 (comment)) of @jsm28. Now `boolean_algebra` extends `generalized_boolean_algebra` and `boolean_algebra.core`:

```lean
class generalized_boolean_algebra (α : Type u) extends semilattice_sup_bot α, semilattice_inf_bot α,
  distrib_lattice α, has_sdiff α :=
(sup_inf_sdiff : ∀a b:α, (a ⊓ b) ⊔ (a \ b) = a)
(inf_inf_sdiff : ∀a b:α, (a ⊓ b) ⊓ (a \ b) = ⊥)

class boolean_algebra.core (α : Type u) extends bounded_distrib_lattice α, has_compl α :=
(inf_compl_le_bot : ∀x:α, x ⊓ xᶜ ≤ ⊥)
(top_le_sup_compl : ∀x:α, ⊤ ≤ x ⊔ xᶜ)

class boolean_algebra (α : Type u) extends generalized_boolean_algebra α, boolean_algebra.core α :=
(sdiff_eq : ∀x y:α, x \ y = x ⊓ yᶜ)
```

I also added a module doc for `order/boolean_algebra`.

Many lemmas about set difference both for `finset`s and `set`s now follow from their `generalized_boolean_algebra` counterparts and I've removed the (fin)set-specific proofs.

`finset.sdiff_subset_self` was removed in favor of the near-duplicate `finset.sdiff_subset` (the latter has more explicit arguments).

archive/imo/imo1998_q2.lean

@@ -175,7 +175,7 @@ begin
   have hst' : (s \ t).card = 2*z + 1, { rw [hst, finset.diag_card, ← hJ], refl, },
   rw [finset.filter_and, ← finset.sdiff_sdiff_self_left s t, finset.card_sdiff],
   { rw hst', rw add_assoc at hs, apply nat.le_sub_right_of_add_le hs, },
-  { apply finset.sdiff_subset_self, },
+  { apply finset.sdiff_subset, },
 end
 
 lemma A_card_lower_bound [fintype C] {z : ℕ} (hJ : fintype.card J = 2*z + 1) :

docs/references.bib

@@ -328,6 +328,17 @@ @Book{            gouvea1997
   url           = {https://doi.org/10.1007/978-3-642-59058-0}
 }
 
+@Book{            Gratzer2011,
+  author        = {Gr{\"a}tzer, George},
+  title         = {Lattice Theory: Foundation},
+  year          = {2011},
+  publisher     = {Springer, Basel},
+  pages         = {xxx+614},
+  isbn          = {978-3-0348-0018-1},
+  doi           = {10.1007/978-3-0348-0018-1},
+  mrnumber      = {2768581},
+}
+
 @Article{         Gusakov2021,
   author        = {Alena Gusakov and Bhavik Mehta and Kyle A. Miller},
   title         = {Formalizing Hall's Marriage Theorem in Lean},
@@ -785,6 +796,16 @@ @Article{         Stone1979
   mrreviewer    = {J. Segal}
 }
 
+@Article{         Stone1935,
+  author        = {Stone, M. H.},
+  year          = {1935},
+  title         = {Postulates for Boolean Algebras and Generalized Boolean Algebras},
+  journal       = {American Journal of Mathematics},
+  volume        = {57},
+  issue         = {4},
+  doi           = {10.2307/2371008}
+}
+
 @Book{            tao2010,
   author        = {Tao, Terence},
   title         = {An Epsilon of Room, I: Real Analysis: Pages from Year

src/algebra/big_operators/basic.lean

@@ -1031,8 +1031,7 @@ lemma prod_erase [decidable_eq α] (s : finset α) {f : α → β} {a : α} (h :
   ∏ x in s.erase a, f x = ∏ x in s, f x :=
 begin
   rw ←sdiff_singleton_eq_erase,
-  apply prod_subset sdiff_subset_self,
-  intros x hx hnx,
+  refine prod_subset (sdiff_subset _ _) (λ x hx hnx, _),
   rw sdiff_singleton_eq_erase at hnx,
   rwa eq_of_mem_of_not_mem_erase hx hnx
 end

src/algebra/punit_instances.lean

@@ -49,7 +49,7 @@ by refine
   compl := λ _, star,
   sdiff := λ _ _, star,
   .. };
-intros; trivial
+intros; trivial <|> simp only [eq_iff_true_of_subsingleton]
 
 instance : canonically_ordered_add_monoid punit :=
 by refine

src/algebra/ring/boolean_ring.lean

@@ -53,7 +53,7 @@ lemma add_eq_zero : a + b = 0 ↔ a = b :=
 calc a + b = 0 ↔ a = -b : add_eq_zero_iff_eq_neg
            ... ↔ a = b  : by rw neg_eq
 
-lemma mul_add_mul : a*b + b*a = 0 :=
+@[simp] lemma mul_add_mul : a*b + b*a = 0 :=
 have a + b = a + b + (a*b + b*a) :=
   calc a + b = (a + b) * (a + b)       : by rw mul_self
          ... = a*a + a*b + (b*a + b*b) : by rw [add_mul, mul_add, mul_add]
@@ -64,6 +64,8 @@ by rwa self_eq_add_right at this
 @[simp] lemma sub_eq_add : a - b = a + b :=
 by rw [sub_eq_add_neg, add_right_inj, neg_eq]
 
+@[simp] lemma mul_one_add_self : a * (1 + a) = 0 := by rw [mul_add, mul_one, mul_self, add_self]
+
 end boolean_ring
 
 namespace boolean_ring
@@ -107,6 +109,27 @@ calc (a + b + a * b) * (a + c + a * c) =
 lemma le_sup_inf (a b c : α) : (a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c :=
 by { dsimp only [(⊔), (⊓)], rw [le_sup_inf_aux, add_self, mul_self, zero_add] }
 
+/-- The "set difference" operation in a Boolean ring is `x * (1 + y)`. -/
+def has_sdiff : has_sdiff α := ⟨λ a b, a * (1 + b)⟩
+/-- The bottom element of a Boolean ring is `0`. -/
+def has_bot : has_bot α := ⟨0⟩
+
+localized "attribute [instance, priority 100] boolean_ring.has_sdiff" in
+  boolean_algebra_of_boolean_ring
+localized "attribute [instance, priority 100] boolean_ring.has_bot" in
+  boolean_algebra_of_boolean_ring
+
+lemma sup_inf_sdiff (a b : α) : a ⊓ b ⊔ a \ b = a :=
+calc a * b + a * (1 + b) + (a * b) * (a * (1 + b)) =
+       a * b + a * (1 + b) + a * a * (b * (1 + b)) : by ac_refl
+... = a * b + (a + a * b)           : by rw [mul_one_add_self, mul_zero, add_zero, mul_add, mul_one]
+... = a + (a * b + a * b)                          : by ac_refl
+... = a                                            : by rw [add_self, add_zero]
+
+lemma inf_inf_sdiff (a b : α) : a ⊓ b ⊓ (a \ b) = ⊥ :=
+calc a * b * (a * (1 + b)) = a * a * (b * (1 + b)) : by ac_refl
+                       ... = 0                     : by rw [mul_one_add_self, mul_zero]
+
 /--
 The Boolean algebra structure on a Boolean ring.
 
@@ -117,16 +140,16 @@ The data is defined so that:
 * `⊥` unfolds to `0`
 * `⊤` unfolds to `1`
 * `aᶜ` unfolds to `1 + a`
-* `a \ b` unfolds to `a * (1 + a)`
+* `a \ b` unfolds to `a * (1 + b)`
 -/
 def to_boolean_algebra : boolean_algebra α :=
 { le_sup_inf := le_sup_inf,
   top := 1,
   le_top := λ a, show a + 1 + a * 1 = 1, by assoc_rw [mul_one, add_comm, add_self, add_zero],
-  bot := 0,
   bot_le := λ a, show 0 + a + 0 * a = a, by rw [zero_mul, zero_add, add_zero],
   compl := λ a, 1 + a,
-  sdiff := λ a b, a * (1 + b),
+  sup_inf_sdiff := sup_inf_sdiff,
+  inf_inf_sdiff := inf_inf_sdiff,
   inf_compl_le_bot := λ a,
     show a*(1+a) + 0 + a*(1+a)*0 = 0,
     by norm_num [mul_add, mul_self, add_self],
@@ -137,7 +160,9 @@ def to_boolean_algebra : boolean_algebra α :=
       rw [←add_assoc, add_self],
     end,
   sdiff_eq := λ a b, rfl,
-  .. lattice.mk' sup_comm sup_assoc inf_comm inf_assoc sup_inf_self inf_sup_self }
+  .. lattice.mk' sup_comm sup_assoc inf_comm inf_assoc sup_inf_self inf_sup_self,
+  .. has_sdiff,
+  .. has_bot }
 
 localized "attribute [instance, priority 100] boolean_ring.to_boolean_algebra" in
   boolean_algebra_of_boolean_ring

src/analysis/calculus/deriv.lean

@@ -273,7 +273,7 @@ has_deriv_at_filter_iff_tendsto_slope
 
 @[simp] lemma has_deriv_within_at_diff_singleton :
   has_deriv_within_at f f' (s \ {x}) x ↔ has_deriv_within_at f f' s x :=
-by simp only [has_deriv_within_at_iff_tendsto_slope, sdiff_idem_right]
+by simp only [has_deriv_within_at_iff_tendsto_slope, sdiff_idem]
 
 @[simp] lemma has_deriv_within_at_Ioi_iff_Ici [partial_order 𝕜] :
   has_deriv_within_at f f' (Ioi x) x ↔ has_deriv_within_at f f' (Ici x) x :=

src/data/finset/basic.lean

@@ -240,8 +240,11 @@ instance : partial_order (finset α) :=
 theorem subset.antisymm_iff {s₁ s₂ : finset α} : s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁ :=
 le_antisymm_iff
 
-@[simp] theorem le_iff_subset {s₁ s₂ : finset α} : s₁ ≤ s₂ ↔ s₁ ⊆ s₂ := iff.rfl
-@[simp] theorem lt_iff_ssubset {s₁ s₂ : finset α} : s₁ < s₂ ↔ s₁ ⊂ s₂ := iff.rfl
+@[simp] theorem le_eq_subset : ((≤) : finset α → finset α → Prop) = (⊆) := rfl
+@[simp] theorem lt_eq_subset : ((<) : finset α → finset α → Prop) = (⊂) := rfl
+
+theorem le_iff_subset {s₁ s₂ : finset α} : s₁ ≤ s₂ ↔ s₁ ⊆ s₂ := iff.rfl
+theorem lt_iff_ssubset {s₁ s₂ : finset α} : s₁ < s₂ ↔ s₁ ⊂ s₂ := iff.rfl
 
 @[simp, norm_cast] lemma coe_ssubset {s₁ s₂ : finset α} : (s₁ : set α) ⊂ s₂ ↔ s₁ ⊂ s₂ :=
 show (s₁ : set α) ⊂ s₂ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁,
@@ -811,12 +814,14 @@ instance : lattice (finset α) :=
   inf_le_right := inter_subset_right,
   ..finset.partial_order }
 
-@[simp] theorem sup_eq_union (s t : finset α) : s ⊔ t = s ∪ t := rfl
-@[simp] theorem inf_eq_inter (s t : finset α) : s ⊓ t = s ∩ t := rfl
+@[simp] theorem sup_eq_union : ((⊔) : finset α → finset α → finset α) = (∪) := rfl
+@[simp] theorem inf_eq_inter : ((⊓) : finset α → finset α → finset α) = (∩) := rfl
 
 instance : semilattice_inf_bot (finset α) :=
 { bot := ∅, bot_le := empty_subset, ..finset.lattice }
 
+@[simp] lemma bot_eq_empty : (⊥ : finset α) = ∅ := rfl
+
 instance {α : Type*} [decidable_eq α] : semilattice_sup_bot (finset α) :=
 { ..finset.semilattice_inf_bot, ..finset.lattice }
 
@@ -921,74 +926,77 @@ instance : has_sdiff (finset α) := ⟨λs₁ s₂, ⟨s₁.1 - s₂.1, nodup_of
 @[simp] theorem mem_sdiff {a : α} {s₁ s₂ : finset α} :
   a ∈ s₁ \ s₂ ↔ a ∈ s₁ ∧ a ∉ s₂ := mem_sub_of_nodup s₁.2
 
+@[simp] theorem inter_sdiff_self (s₁ s₂ : finset α) : s₁ ∩ (s₂ \ s₁) = ∅ :=
+eq_empty_of_forall_not_mem $
+by simp only [mem_inter, mem_sdiff]; rintro x ⟨h, _, hn⟩; exact hn h
+
+instance : generalized_boolean_algebra (finset α) :=
+{ sup_inf_sdiff := λ x y, by { simp only [ext_iff, mem_union, mem_sdiff, inf_eq_inter, sup_eq_union,
+      mem_inter], tauto },
+  inf_inf_sdiff := λ x y, by { simp only [ext_iff, inter_sdiff_self, inter_empty, inter_assoc,
+      false_iff, inf_eq_inter, not_mem_empty], tauto },
+  ..finset.has_sdiff,
+  ..finset.distrib_lattice,
+  ..finset.semilattice_inf_bot }
+
 lemma not_mem_sdiff_of_mem_right {a : α} {s t : finset α} (h : a ∈ t) : a ∉ s \ t :=
 by simp only [mem_sdiff, h, not_true, not_false_iff, and_false]
 
-theorem sdiff_union_of_subset {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : (s₂ \ s₁) ∪ s₁ = s₂ :=
-ext $ λ a, by simpa only [mem_sdiff, mem_union, or_comm,
-  or_and_distrib_left, dec_em, and_true] using or_iff_right_of_imp (@h a)
-
 theorem union_sdiff_of_subset {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : s₁ ∪ (s₂ \ s₁) = s₂ :=
-(union_comm _ _).trans (sdiff_union_of_subset h)
+sup_sdiff_of_le h
+
+theorem sdiff_union_of_subset {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : (s₂ \ s₁) ∪ s₁ = s₂ :=
+(union_comm _ _).trans (union_sdiff_of_subset h)
 
 theorem inter_sdiff (s t u : finset α) : s ∩ (t \ u) = s ∩ t \ u :=
 by { ext x, simp [and_assoc] }
 
-@[simp] theorem inter_sdiff_self (s₁ s₂ : finset α) : s₁ ∩ (s₂ \ s₁) = ∅ :=
-eq_empty_of_forall_not_mem $
-by simp only [mem_inter, mem_sdiff]; rintro x ⟨h, _, hn⟩; exact hn h
-
 @[simp] theorem sdiff_inter_self (s₁ s₂ : finset α) : (s₂ \ s₁) ∩ s₁ = ∅ :=
-(inter_comm _ _).trans (inter_sdiff_self _ _)
+inf_sdiff_self_left
 
 @[simp] theorem sdiff_self (s₁ : finset α) : s₁ \ s₁ = ∅ :=
-by ext; simp
+sdiff_self
 
 theorem sdiff_inter_distrib_right (s₁ s₂ s₃ : finset α) : s₁ \ (s₂ ∩ s₃) = (s₁ \ s₂) ∪ (s₁ \ s₃) :=
-by ext; simp only [and_or_distrib_left, mem_union, not_and_distrib, mem_sdiff, mem_inter]
+sdiff_inf
 
 @[simp] theorem sdiff_inter_self_left (s₁ s₂ : finset α) : s₁ \ (s₁ ∩ s₂) = s₁ \ s₂ :=
-by simp only [sdiff_inter_distrib_right, sdiff_self, empty_union]
+sdiff_inf_self_left
 
 @[simp] theorem sdiff_inter_self_right (s₁ s₂ : finset α) : s₁ \ (s₂ ∩ s₁) = s₁ \ s₂ :=
-by simp only [sdiff_inter_distrib_right, sdiff_self, union_empty]
+sdiff_inf_self_right
 
 @[simp] theorem sdiff_empty {s₁ : finset α} : s₁ \ ∅ = s₁ :=
-ext (by simp)
+sdiff_bot
 
 @[mono]
 theorem sdiff_subset_sdiff {s₁ s₂ t₁ t₂ : finset α} (h₁ : t₁ ⊆ t₂) (h₂ : s₂ ⊆ s₁) :
   t₁ \ s₁ ⊆ t₂ \ s₂ :=
-by simpa only [subset_iff, mem_sdiff, and_imp] using λ a m₁ m₂, and.intro (h₁ m₁) (mt (@h₂ _) m₂)
-
-theorem sdiff_subset_self {s₁ s₂ : finset α} : s₁ \ s₂ ⊆ s₁ :=
-suffices s₁ \ s₂ ⊆ s₁ \ ∅, by simpa [sdiff_empty] using this,
-sdiff_subset_sdiff (subset.refl _) (empty_subset _)
+sdiff_le_sdiff ‹t₁ ≤ t₂› ‹s₂ ≤ s₁›
 
 @[simp, norm_cast] lemma coe_sdiff (s₁ s₂ : finset α) : ↑(s₁ \ s₂) = (s₁ \ s₂ : set α) :=
 set.ext $ λ _, mem_sdiff
 
 @[simp] theorem union_sdiff_self_eq_union {s t : finset α} : s ∪ (t \ s) = s ∪ t :=
-ext $ λ a, by simp only [mem_union, mem_sdiff, or_iff_not_imp_left,
-  imp_and_distrib, and_iff_left id]
+sup_sdiff_self_right
 
 @[simp] theorem sdiff_union_self_eq_union {s t : finset α} : (s \ t) ∪ t = s ∪ t :=
-by rw [union_comm, union_sdiff_self_eq_union, union_comm]
+sup_sdiff_self_left
 
 lemma union_sdiff_symm {s t : finset α} : s ∪ (t \ s) = t ∪ (s \ t) :=
-by rw [union_sdiff_self_eq_union, union_sdiff_self_eq_union, union_comm]
+sup_sdiff_symm
 
 lemma sdiff_union_inter (s t : finset α) : (s \ t) ∪ (s ∩ t) = s :=
-by { simp only [ext_iff, mem_union, mem_sdiff, mem_inter], tauto }
+by { rw union_comm, exact sup_inf_sdiff _ _ }
 
 @[simp] lemma sdiff_idem (s t : finset α) : s \ t \ t = s \ t :=
-by { simp only [ext_iff, mem_sdiff], tauto }
+sdiff_idem
 
 lemma sdiff_eq_empty_iff_subset {s t : finset α} : s \ t = ∅ ↔ s ⊆ t :=
-by { rw [subset_iff, ext_iff], simp }
+sdiff_eq_bot_iff
 
 @[simp] lemma empty_sdiff (s : finset α) : ∅ \ s = ∅ :=
-by { rw sdiff_eq_empty_iff_subset, exact empty_subset _ }
+bot_sdiff
 
 lemma insert_sdiff_of_not_mem (s : finset α) {t : finset α} {x : α} (h : x ∉ t) :
   (insert x s) \ t = insert x (s \ t) :=
@@ -1017,25 +1025,29 @@ begin
 end
 
 @[simp] lemma sdiff_subset (s t : finset α) : s \ t ⊆ s :=
-by simp [subset_iff, mem_sdiff] {contextual := tt}
+show s \ t ≤ s, from sdiff_le
 
 lemma union_sdiff_distrib (s₁ s₂ t : finset α) : (s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t :=
-by { simp only [ext_iff, mem_sdiff, mem_union], tauto }
+sup_sdiff
 
 lemma sdiff_union_distrib (s t₁ t₂ : finset α) : s \ (t₁ ∪ t₂) = (s \ t₁) ∩ (s \ t₂) :=
-by { simp only [ext_iff, mem_union, mem_sdiff, mem_inter], tauto }
+sdiff_sup
 
 lemma union_sdiff_self (s t : finset α) : (s ∪ t) \ t = s \ t :=
-by rw [union_sdiff_distrib, sdiff_self, union_empty]
+sup_sdiff_right_self
 
 lemma sdiff_singleton_eq_erase (a : α) (s : finset α) : s \ singleton a = erase s a :=
 by { ext, rw [mem_erase, mem_sdiff, mem_singleton], tauto }
 
 lemma sdiff_sdiff_self_left (s t : finset α) : s \ (s \ t) = s ∩ t :=
-by { simp only [ext_iff, mem_sdiff, mem_inter], tauto }
+sdiff_sdiff_right_self
+
+lemma sdiff_eq_sdiff_iff_inter_eq_inter {s t₁ t₂ : finset α} : s \ t₁ = s \ t₂ ↔ s ∩ t₁ = s ∩ t₂ :=
+sdiff_eq_sdiff_iff_inf_eq_inf
 
-lemma inter_eq_inter_of_sdiff_eq_sdiff {s t₁ t₂ : finset α} : s \ t₁ = s \ t₂ → s ∩ t₁ = s ∩ t₂ :=
-by { simp only [ext_iff, mem_sdiff, mem_inter], intros b c, replace b := b c, split; tauto }
+lemma union_eq_sdiff_union_sdiff_union_inter (s t : finset α) :
+  s ∪ t = (s \ t) ∪ (t \ s) ∪ (s ∩ t) :=
+sup_eq_sdiff_sup_sdiff_sup_inf
 
 end decidable_eq
 
@@ -1308,7 +1320,7 @@ theorem sdiff_eq_filter (s₁ s₂ : finset α) :
 
 theorem sdiff_eq_self (s₁ s₂ : finset α) :
   s₁ \ s₂ = s₁ ↔ s₁ ∩ s₂ ⊆ ∅ :=
-by { simp [subset.antisymm_iff,sdiff_subset_self],
+by { simp [subset.antisymm_iff],
      split; intro h,
      { transitivity' ((s₁ \ s₂) ∩ s₂), mono, simp },
      { calc  s₁ \ s₂
@@ -1385,7 +1397,7 @@ trans (filter_congr (λ _ _, ⟨eq.symm, eq.symm⟩)) (filter_eq s b)
 
 lemma filter_ne [decidable_eq β] (s : finset β) (b : β) :
   s.filter (λ a, b ≠ a) = s.erase b :=
-by { ext, simp only [mem_filter, mem_erase, ne.def], cc, }
+by { ext, simp only [mem_filter, mem_erase, ne.def], tauto, }
 
 lemma filter_ne' [decidable_eq β] (s : finset β) (b : β) :
   s.filter (λ a, a ≠ b) = s.erase b :=

src/data/finset/fold.lean

@@ -115,7 +115,6 @@ begin
   { intros a s has ih, rw [fold_insert has, ih, insert_eq], }
 end
 
-@[simp]
 lemma fold_sup_bot_singleton [decidable_eq α] (s : finset α) :
   finset.fold (⊔) ⊥ singleton s = s :=
 fold_union_empty_singleton s

src/data/finset/powerset.lean

@@ -160,7 +160,9 @@ lemma powerset_len_sup [decidable_eq α] (u : finset α) (n : ℕ) (hn : n < u.c
   (powerset_len n.succ u).sup id = u :=
 begin
   apply le_antisymm,
-  { simp [mem_powerset_len, and.comm] },
+  { simp_rw [sup_le_iff, mem_powerset_len],
+    rintros x ⟨h, -⟩,
+    exact h },
   { rw [sup_eq_bUnion, le_iff_subset, subset_iff],
     cases (nat.succ_le_of_lt hn).eq_or_lt with h' h',
     { simp [h'] },

src/data/fintype/basic.lean

@@ -60,13 +60,11 @@ instance : order_top (finset α) :=
 
 instance [decidable_eq α] : boolean_algebra (finset α) :=
 { compl := λ s, univ \ s,
-  sdiff_eq := λ s t, by simp [ext_iff],
   inf_compl_le_bot := λ s x hx, by simpa using hx,
   top_le_sup_compl := λ s x hx, by simp,
-  ..finset.distrib_lattice,
-  ..finset.semilattice_inf_bot,
+  sdiff_eq := λ s t, by simp [ext_iff, compl],
   ..finset.order_top,
-  ..finset.has_sdiff }
+  ..finset.generalized_boolean_algebra }
 
 lemma compl_eq_univ_sdiff [decidable_eq α] (s : finset α) : sᶜ = univ \ s := rfl