feat(data/fintype/order): bool is a boolean algebra (#11694)

Provide the `boolean_algebra` instance for `bool` and use the machinery from `data.fintype.order` to deduce `complete_boolean_algebra bool` and `complete_linear_order bool`.

src/data/bool/basic.lean

@@ -138,6 +138,11 @@ theorem eq_tt_of_bnot_eq_ff : ∀ {a : bool}, bnot a = ff → a = tt := dec_triv
 
 theorem eq_ff_of_bnot_eq_tt : ∀ {a : bool}, bnot a = tt → a = ff := dec_trivial
 
+@[simp] lemma band_bnot_self : ∀ x, x && !x = ff := dec_trivial
+@[simp] lemma bnot_band_self : ∀ x, !x && x = ff := dec_trivial
+@[simp] lemma bor_bnot_self : ∀ x, x || !x = tt := dec_trivial
+@[simp] lemma bnot_bor_self : ∀ x, !x || x = tt := dec_trivial
+
 theorem bxor_comm : ∀ a b, bxor a b = bxor b a := dec_trivial
 @[simp] theorem bxor_assoc : ∀ a b c, bxor (bxor a b) c = bxor a (bxor b c) := dec_trivial
 theorem bxor_left_comm : ∀ a b c, bxor a (bxor b c) = bxor b (bxor a c) := dec_trivial

src/data/fintype/order.lean

@@ -38,6 +38,7 @@ Those are marked as `def` to avoid typeclass loops.
 We provide a few instances for concrete types:
 * `fin.complete_linear_order`
 * `bool.complete_linear_order`
+* `bool.complete_boolean_algebra`
 -/
 
 open finset
@@ -141,3 +142,4 @@ noncomputable instance {n : ℕ} : complete_linear_order (fin (n + 1)) :=
 fintype.to_complete_linear_order _
 
 noncomputable instance : complete_linear_order bool := fintype.to_complete_linear_order _
+noncomputable instance : complete_boolean_algebra bool := fintype.to_complete_boolean_algebra _

src/order/boolean_algebra.lean

@@ -808,3 +808,18 @@ instance pi.boolean_algebra {ι : Type u} {α : ι → Type v} [∀ i, boolean_a
   .. pi.has_compl,
   .. pi.bounded_order,
   .. pi.distrib_lattice }
+
+instance : boolean_algebra bool := boolean_algebra.of_core
+{ sup := bor,
+  le_sup_left := bool.left_le_bor,
+  le_sup_right := bool.right_le_bor,
+  sup_le := λ _ _ _, bool.bor_le,
+  inf := band,
+  inf_le_left := bool.band_le_left,
+  inf_le_right := bool.band_le_right,
+  le_inf := λ _ _ _, bool.le_band,
+  le_sup_inf := dec_trivial,
+  compl := bnot,
+  inf_compl_le_bot := λ a, a.band_bnot_self.le,
+  top_le_sup_compl := λ a, a.bor_bnot_self.ge,
+  ..bool.linear_order, ..bool.bounded_order }

src/order/lattice.lean

@@ -940,3 +940,6 @@ See note [reducible non-instances]. -/
   ..hf_inj.lattice f map_sup map_inf, }
 
 end lift
+
+--To avoid noncomputability poisoning from `bool.complete_boolean_algebra`
+instance : distrib_lattice bool := linear_order.to_distrib_lattice