Grace/Cumulus/Lattice/BooleanAlgebra.g17

Open in Workbench Download source

Imports

Boolean · Linear

Declarations

Source

1-- Boolean algebras bundled as ordered sets, with the complement compl(P)2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Lattice.BooleanAlgebra8import Boolean9import Linear1011-- A Boolean algebra is a bounded distributive lattice in which every12-- element has a complement; the complement is read back as compl(P)(a).13-- Only the bounded-lattice projection is an instance, so that Lattice(P)14-- has one derivation from a Boolean hypothesis.15predicate BooleanAlgebra (P : Set) :=16  DistributiveLattice(P) ∧ BoundedLattice(P) ∧17  (∀ a ∈ points(P), ∃ b, IsCompl(P, a, b))1819notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis BooleanAlgebra(P) for P.points20notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis BooleanAlgebra(P) for P.points21notation infix 50 "≤" => Le(P, _, _) via hypothesis BooleanAlgebra(P) for P.points2223theorem BooleanAlgebra.distributive_of (P : Set)24  requires boolean : BooleanAlgebra(P)25  shows DistributiveLattice(P)26proof27  obtain ⟨distributive, bounded, complemented⟩ := boolean28  exact distributive2930instance BooleanAlgebra.bounded_of (P : Set)31  requires boolean : BooleanAlgebra(P)32  shows BoundedLattice(P)33proof34  obtain ⟨distributive, bounded, complemented⟩ := boolean35  exact bounded3637theorem BooleanAlgebra.lattice_of (P : Set)38  requires boolean : BooleanAlgebra(P)39  shows Lattice(P)40proof41  exact BoundedLattice.lattice_of with (BooleanAlgebra.bounded_of with boolean)4243theorem BooleanAlgebra.exists_isCompl (P a : Set)44  requires boolean : BooleanAlgebra(P)45  requires aIn : a ∈ points(P)46  shows ∃ b, IsCompl(P, a, b)47proof48  obtain ⟨distributive, bounded, complemented⟩ := boolean49  exact complemented with a, aIn5051-- Bridges to the unbundled form IsBooleanAlgebra(A, r, bot, top).52instance BooleanAlgebra.unbundled (P : Set)53  requires boolean : BooleanAlgebra(P)54  shows IsBooleanAlgebra(points(P), le(P), bot(P), top(P))55proof56  have distributive := BooleanAlgebra.distributive_of with boolean57  have bounded := BooleanAlgebra.bounded_of with boolean58  have both := BoundedLattice.bounded_distributive with distributive, bounded59  constructor60  . exact both61  . intros a aIn62    obtain ⟨b, compl⟩ := BooleanAlgebra.exists_isCompl with boolean, aIn63    witness b64    exact IsCompl.unbundled with bounded, compl6566theorem BooleanAlgebra.mk (A r b t : Set)67  requires boolean : IsBooleanAlgebra(A, r, b, t)68  shows BooleanAlgebra(Order.mk(A, r))69proof70  have boundedU := IsBooleanAlgebra.bounded with boolean71  have bounded := BoundedLattice.mk with boundedU72  have distributive := DistributiveLattice.mk with73      (IsBooleanAlgebra.distributive with boolean)74  have botEq := bot.mk with boundedU75  have topEq := top.mk with boundedU76  refine ⟨distributive, bounded, ?_⟩77  intros a aIn78  rw Order.mk.points at aIn79  obtain ⟨c, compl⟩ := IsBooleanAlgebra.exists_complement with boolean, aIn80  witness c81  have aIn2 : a ∈ points(Order.mk(A, r))82    rw Order.mk.points83    exact aIn84  apply IsCompl.of_complementary with bounded, aIn285  rw [Order.mk.points, Order.mk.le, botEq, topEq]86  exact compl8788defgraph compl (P : Set) (a ∈ points(P)) : points(P) :=89  latticeComplement(points(P), le(P), bot(P), top(P), a)90requires boolean : BooleanAlgebra(P)91proof92  exact latticeComplement.member with93      (BooleanAlgebra.unbundled with boolean), member9495-- The complement is written aᶜ, and the bounds ⊥ and ⊤, wherever a96-- hypothesis in scope supplies the Boolean algebra.97notation postfix 90 "ᶜ" => apply(compl(P), _) via hypothesis BooleanAlgebra(P) for P.points98notation constant "⊥" => bot(P) via hypothesis BooleanAlgebra(P) for P.points99notation constant "⊤" => top(P) via hypothesis BooleanAlgebra(P) for P.points100101section BooleanLaws102variable (P : Set)103hypothesis boolean : BooleanAlgebra(P)104105-- The bundled complement is the unbundled one.106theorem compl.complement (a ∈ points(P))107  shows compl(P)(a) = latticeComplement(points(P), le(P), bot(P), top(P), a)108proof109  exact compl.value with boolean, assumption110111instance compl.member (a ∈ points(P))112  shows compl(P)(a) ∈ points(P)113proof114  rw compl.complement115  exact latticeComplement.member with116      (BooleanAlgebra.unbundled with boolean), assumption117118theorem compl.isCompl (a ∈ points(P))119  shows IsCompl(P, a, compl(P)(a))120proof121  have complementary := latticeComplement.complementary with122      (BooleanAlgebra.unbundled with boolean), assumption123  rw compl.complement124  exact IsCompl.of_complementary with125      (BooleanAlgebra.bounded_of with boolean), assumption126127theorem inf_compl_eq_bot (a ∈ points(P))128  shows a ⊓ aᶜ = ⊥129proof130  rw [inf.meet, compl.complement]131  exact latticeComplement.meet with132      (BooleanAlgebra.unbundled with boolean), assumption133134theorem sup_compl_eq_top (a ∈ points(P))135  shows a ⊔ compl(P)(a) = top(P)136proof137  rw [sup.join, compl.complement]138  exact latticeComplement.join with139      (BooleanAlgebra.unbundled with boolean), assumption140141theorem compl_inf_eq_bot (a ∈ points(P))142  shows compl(P)(a) ⊓ a = bot(P)143proof144  rw [inf.meet, compl.complement]145  exact latticeComplement.meet_left with146      (BooleanAlgebra.unbundled with boolean), assumption147148theorem compl_sup_eq_top (a ∈ points(P))149  shows compl(P)(a) ⊔ a = top(P)150proof151  rw [sup.join, compl.complement]152  exact latticeComplement.join_left with153      (BooleanAlgebra.unbundled with boolean), assumption154155theorem IsCompl.compl_eq (b : Set) (a ∈ points(P))156  requires compl : IsCompl(P, a, b)157  shows b = compl(P)(a)158proof159  have complementary := IsCompl.unbundled with160      (BooleanAlgebra.bounded_of with boolean), compl161  rw compl.complement162  exact latticeComplement.of_complementary with163      (BooleanAlgebra.unbundled with boolean), assumption, complementary164165theorem compl_compl (a ∈ points(P))166  shows (aᶜ)ᶜ = a167proof168  have complIn : compl(P)(a) ∈ points(P) := compl.member with *169  rw [compl.complement, compl.complement]170  exact latticeComplement.involutive with171      (BooleanAlgebra.unbundled with boolean), assumption172173theorem compl_bot174  shows compl(P)(bot(P)) = top(P)175proof176  have botIn : bot(P) ∈ points(P) := bot.member with *177  rw compl.complement178  exact latticeComplement.bottom with (BooleanAlgebra.unbundled with boolean)179180theorem compl_top181  shows compl(P)(top(P)) = bot(P)182proof183  have topIn : top(P) ∈ points(P) := top.member with *184  rw compl.complement185  exact latticeComplement.top with (BooleanAlgebra.unbundled with boolean)186187theorem compl_injective (a b ∈ points(P))188  requires same : compl(P)(a) = compl(P)(b)189  shows a = b190proof191  rw [compl.complement, compl.complement] at same192  exact latticeComplement.injective with193      (BooleanAlgebra.unbundled with boolean), *194195theorem compl_sup (a b ∈ points(P))196  shows compl(P)(a ⊔ b) = compl(P)(a) ⊓ compl(P)(b)197proof198  have supIn : a ⊔ b ∈ points(P) := sup.member with *199  have complA : compl(P)(a) ∈ points(P) := compl.member with *200  have complB : compl(P)(b) ∈ points(P) := compl.member with *201  simp [sup.join, inf.meet, compl.complement]202  exact latticeComplement.join_eq with203      (BooleanAlgebra.unbundled with boolean), *204205theorem compl_inf (a b ∈ points(P))206  shows compl(P)(a ⊓ b) = compl(P)(a) ⊔ compl(P)(b)207proof208  have infIn : a ⊓ b ∈ points(P) := inf.member with *209  have complA : compl(P)(a) ∈ points(P) := compl.member with *210  have complB : compl(P)(b) ∈ points(P) := compl.member with *211  simp [sup.join, inf.meet, compl.complement]212  exact latticeComplement.meet_eq with213      (BooleanAlgebra.unbundled with boolean), *214215theorem le_compl_iff_inf_eq_bot (a b ∈ points(P))216  shows a ≤ compl(P)(b) ↔ a ⊓ b = bot(P)217proof218  rw [inf.meet, compl.complement]219  have characterization := latticeComplement.le_iff_meet_bottom at points(P),220      le(P), bot(P), top(P), a, b with (BooleanAlgebra.unbundled with boolean),221      assumption, assumption222  constructor223  . intro h224    exact characterization.forward with (Le.relates with h)225  . intro h226    exact Le.of_relates with (characterization.backward with h)227228theorem compl_le_compl (a b ∈ points(P))229  requires hab : a ≤ b230  shows compl(P)(b) ≤ compl(P)(a)231proof232  rw [compl.complement, compl.complement]233  unfold Le234  exact latticeComplement.antitone with (BooleanAlgebra.unbundled with boolean),235      assumption, assumption, (Le.relates with hab)236237theorem compl_le_compl_iff_le (a b ∈ points(P))238  shows compl(P)(b) ≤ compl(P)(a) ↔ a ≤ b239proof240  rw [compl.complement, compl.complement]241  have characterization := latticeComplement.le_iff at points(P), le(P),242      bot(P), top(P), a, b with (BooleanAlgebra.unbundled with boolean),243      assumption, assumption244  constructor245  . intro h246    exact Le.of_relates with (characterization.backward with (Le.relates with h))247  . intro h248    exact Le.of_relates with (characterization.forward with (Le.relates with h))249250end BooleanLaws251252-- The powerset of a set is a Boolean algebra whose complement is the253-- relative complement.254instance powersetLattice.boolean (X : Set)255  shows BooleanAlgebra(powersetLattice(X))256proof257  unfold powersetLattice258  exact BooleanAlgebra.mk with (powersetOrder.boolean at X)259260section PowersetBoolean261variable (X : Set)262hypothesis boolean : BooleanAlgebra(powersetLattice(X))263264theorem powersetLattice.compl (B ∈ 𝒫(X))265  shows compl(powersetLattice(X))(B) = X ∖ B266proof267  have complete : CompleteLattice(powersetLattice(X)) := powersetLattice.complete at X268  have BIn : B ∈ points(powersetLattice(X)) := powersetLattice.member at X, B with269      *270  have botEq := powersetLattice.bot with complete271  have topEq := powersetLattice.top with complete272  rw [compl.complement, powersetLattice.points, powersetLattice.le, botEq, topEq]273  exact powersetOrder.complement_value with *274275end PowersetBoolean276277-- The Boolean rewrite set: double complements, the complements of the278-- bounds, and the meet and join of an element with its complement.279tactic boolean_simp := simp [compl_compl, compl_bot, compl_top, inf_compl_eq_bot, sup_compl_eq_top, compl_inf_eq_bot, compl_sup_eq_top]280