feat(order/bounded_lattice): define the distrib_lattice_bot typecla…

…ss (#8507)

Typeclass for a distributive lattice with a least element.

This typeclass is used to generalize `disjoint_sup_left` and similar.

It inserts itself in the hierarchy between `semilattice_sup_bot, semilattice_inf_bot` and `generalized_boolean_algebra`, `bounded_distrib_lattice`. I am doing it through `extends`.

src/order/boolean_algebra.lean

@@ -84,8 +84,7 @@ operation `\` (called `sdiff`, after "set difference") satisfying `(a ⊓ b) ⊔
 
 This is a generalization of Boolean algebras which applies to `finset α` for arbitrary
 (not-necessarily-`fintype`) `α`. -/
-class generalized_boolean_algebra (α : Type u) extends semilattice_sup_bot α, semilattice_inf_bot α,
-  distrib_lattice α, has_sdiff α :=
+class generalized_boolean_algebra (α : Type u) extends distrib_lattice_bot α, has_sdiff α :=
 (sup_inf_sdiff : ∀a b:α, (a ⊓ b) ⊔ (a \ b) = a)
 (inf_inf_sdiff : ∀a b:α, (a ⊓ b) ⊓ (a \ b) = ⊥)
 

src/order/bounded_lattice.lean

@@ -3,10 +3,10 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import order.lattice
 import data.option.basic
-import tactic.pi_instances
 import logic.nontrivial
+import order.lattice
+import tactic.pi_instances
 
 /-!
 # ⊤ and ⊥, bounded lattices and variants
@@ -23,11 +23,18 @@ instances for `Prop` and `fun`.
 * `semilattice_<sup/inf>_<top/bot>`: Semilattice with a join/meet and a top/bottom element (all four
   combinations). Typical examples include `ℕ`.
 * `bounded_lattice α`: Lattice with a top and bottom element.
+* `distrib_lattice_bot α`: Distributive lattice with a bottom element. It captures the properties
+  of `disjoint` that are common to `generalized_boolean_algebra` and `bounded_distrib_lattice`.
 * `bounded_distrib_lattice α`: Bounded and distributive lattice. Typical examples include `Prop` and
   `set α`.
 * `is_compl x y`: In a bounded lattice, predicate for "`x` is a complement of `y`". Note that in a
   non distributive lattice, an element can have several complements.
 * `is_complemented α`: Typeclass stating that any element of a lattice has a complement.
+
+## Implementation notes
+
+We didn't define `distrib_lattice_top` because the dual notion of `disjoint` isn't really used
+anywhere.
 -/
 
 /-! ### Top, bottom element -/
@@ -280,8 +287,11 @@ begin
   injection H1; injection H2; injection H3; congr'
 end
 
+/-- A `distrib_lattice_bot` is a distributive lattice with a least element. -/
+class distrib_lattice_bot α extends distrib_lattice α, semilattice_inf_bot α, semilattice_sup_bot α
+
 /-- A bounded distributive lattice is exactly what it sounds like. -/
-class bounded_distrib_lattice α extends distrib_lattice α, bounded_lattice α
+class bounded_distrib_lattice α extends distrib_lattice_bot α, bounded_lattice α
 
 lemma inf_eq_bot_iff_le_compl {α : Type u} [bounded_distrib_lattice α] {a b c : α}
   (h₁ : b ⊔ c = ⊤) (h₂ : b ⊓ c = ⊥) : a ⊓ b = ⊥ ↔ a ≤ c :=
@@ -403,10 +413,23 @@ by refine_struct { sup := (⊔), top := ⊤, .. pi.partial_order }; tactic.pi_in
 instance pi.lattice {ι : Type*} {α : ι → Type*} [Π i, lattice (α i)] : lattice (Π i, α i) :=
 { .. pi.semilattice_sup, .. pi.semilattice_inf }
 
+instance pi.distrib_lattice {ι : Type*} {α : ι → Type*} [Π i, distrib_lattice (α i)] :
+  distrib_lattice (Π i, α i) :=
+by refine_struct {  .. pi.lattice }; tactic.pi_instance_derive_field
+
 instance pi.bounded_lattice {ι : Type*} {α : ι → Type*} [Π i, bounded_lattice (α i)] :
   bounded_lattice (Π i, α i) :=
 { .. pi.semilattice_sup_top, .. pi.semilattice_inf_bot }
 
+instance pi.distrib_lattice_bot {ι : Type*} {α : ι → Type*} [Π i, distrib_lattice_bot (α i)] :
+  distrib_lattice_bot (Π i, α i) :=
+{ .. pi.distrib_lattice, .. pi.order_bot }
+
+instance pi.bounded_distrib_lattice {ι : Type*} {α : ι → Type*}
+  [Π i, bounded_distrib_lattice (α i)] :
+  bounded_distrib_lattice (Π i, α i) :=
+{ .. pi.bounded_lattice, .. pi.distrib_lattice }
+
 lemma eq_bot_of_bot_eq_top {α : Type*} [bounded_lattice α] (hα : (⊥ : α) = ⊤) (x : α) :
   x = (⊥ : α) :=
 eq_bot_mono le_top (eq.symm hα)
@@ -968,6 +991,9 @@ instance [semilattice_sup_top α] : semilattice_inf_bot (order_dual α) :=
 instance [bounded_lattice α] : bounded_lattice (order_dual α) :=
 { .. order_dual.lattice α, .. order_dual.order_top α, .. order_dual.order_bot α }
 
+/- If you define `distrib_lattice_top`, add the `order_dual` instances between `distrib_lattice_bot`
+and `distrib_lattice_top` here -/
+
 instance [bounded_distrib_lattice α] : bounded_distrib_lattice (order_dual α) :=
 { .. order_dual.bounded_lattice α, .. order_dual.distrib_lattice α }
 
@@ -1002,6 +1028,10 @@ instance [semilattice_inf_bot α] [semilattice_inf_bot β] : semilattice_inf_bot
 instance [bounded_lattice α] [bounded_lattice β] : bounded_lattice (α × β) :=
 { .. prod.lattice α β, .. prod.order_top α β, .. prod.order_bot α β }
 
+instance [distrib_lattice_bot α] [distrib_lattice_bot β] :
+  distrib_lattice_bot (α × β) :=
+{ .. prod.distrib_lattice α β, .. prod.order_bot α β }
+
 instance [bounded_distrib_lattice α] [bounded_distrib_lattice β] :
   bounded_distrib_lattice (α × β) :=
 { .. prod.bounded_lattice α β, .. prod.distrib_lattice α β }
@@ -1076,12 +1106,8 @@ end
 
 end bounded_lattice
 
-section bounded_distrib_lattice
-/-
-TODO: these lemmas don't require the existence of `⊤` and should be generalized to
-distrib_lattice_with_bot (which doesn't exist yet).
--/
-variables [bounded_distrib_lattice α] {a b c : α}
+section distrib_lattice_bot
+variables [distrib_lattice_bot α] {a b c : α}
 
 @[simp] lemma disjoint_sup_left : disjoint (a ⊔ b) c ↔ disjoint a c ∧ disjoint b c :=
 by simp only [disjoint_iff, inf_sup_right, sup_eq_bot_iff]
@@ -1102,7 +1128,7 @@ lemma disjoint.left_le_of_le_sup_left {a b c : α} (h : a ≤ c ⊔ b) (hd : dis
 @le_of_inf_le_sup_le _ _ a b c ((disjoint_iff.mp hd).symm ▸ bot_le)
   ((@sup_comm _ _ c b) ▸ (sup_le h le_sup_left))
 
-end bounded_distrib_lattice
+end distrib_lattice_bot
 
 section semilattice_inf_bot
 

src/order/partial_sups.lean

@@ -122,9 +122,8 @@ begin
 end
 
 /- Note this lemma requires a distributive lattice, so is not useful (or true) in situations such as
-submodules.
-Can be generalized to (the yet inexistent) `distrib_lattice_bot`. -/
-lemma partial_sups_disjoint_of_disjoint [bounded_distrib_lattice α]
+submodules. -/
+lemma partial_sups_disjoint_of_disjoint [distrib_lattice_bot α]
   (f : ℕ → α) (h : pairwise (disjoint on f)) {m n : ℕ} (hmn : m < n) :
   disjoint (partial_sups f m) (f n) :=
 begin

src/order/symm_diff.lean

@@ -168,6 +168,13 @@ calc a Δ b = a ↔ a Δ b = a Δ ⊥ : by rw symm_diff_bot
 calc a Δ b = ⊥ ↔ a Δ b = a Δ a : by rw symm_diff_self
            ... ↔     a = b     : by rw [symm_diff_right_inj, eq_comm]
 
+lemma disjoint.disjoint_symm_diff_of_disjoint {a b c : α} (ha : disjoint a c) (hb : disjoint b c) :
+  disjoint (a Δ b) c :=
+begin
+  rw symm_diff_eq_sup_sdiff_inf,
+  exact (ha.sup_left hb).disjoint_sdiff_left,
+end
+
 end generalized_boolean_algebra
 
 section boolean_algebra
@@ -207,12 +214,4 @@ calc a Δ (b Δ c) = (a ⊓ ((b ⊓ c) ⊔ (bᶜ ⊓ cᶜ))) ⊔
                                                        { apply inf_left_right_swap }
                                                      end
 
--- TODO: move this to generalized_boolean_algebra when we have a distrib_lattice_with_bot typeclass
-lemma disjoint.disjoint_symm_diff_of_disjoint {a b c : α} (h1 : disjoint a c) (h2 : disjoint b c) :
-  disjoint (a Δ b) c :=
-begin
-  rw [symm_diff_eq_sup_sdiff_inf],
-  exact (h1.sup_left h2).disjoint_sdiff_left,
-end
-
 end boolean_algebra