Grace/Cumulus/Lattice/Boolean.g17

Open in Workbench Download source

Imports

Distributive

Declarations

Source

1-- Boolean algebras: complemented distributive bounded lattices2-- 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.Boolean8import Distributive910predicate IsBooleanAlgebra (A r bot top : Set) :=11  BoundedDistributiveLattice(A, r, bot, top) ∧12  (∀ x ∈ A, ∃ y, Complementary(A, r, bot, top, x, y))1314theorem IsBooleanAlgebra.bounded_distributive (A r bot top : Set)15  requires h : IsBooleanAlgebra(A, r, bot, top)16  shows BoundedDistributiveLattice(A, r, bot, top)17proof18  simp [IsBooleanAlgebra]1920theorem IsBooleanAlgebra.distributive (A r bot top : Set)21  requires h : IsBooleanAlgebra(A, r, bot, top)22  shows IsDistributiveLattice(A, r)23proof24  exact BoundedDistributiveLattice.distributive with25      (IsBooleanAlgebra.bounded_distributive with h)2627theorem IsBooleanAlgebra.bounded (A r bot top : Set)28  requires h : IsBooleanAlgebra(A, r, bot, top)29  shows IsBoundedLattice(A, r, bot, top)30proof31  exact BoundedDistributiveLattice.bounded with32      (IsBooleanAlgebra.bounded_distributive with h)3334theorem IsBooleanAlgebra.lattice (A r bot top : Set)35  requires h : IsBooleanAlgebra(A, r, bot, top)36  shows IsLattice(A, r)37proof38  exact IsBoundedLattice.lattice with (IsBooleanAlgebra.bounded with h)3940theorem IsBooleanAlgebra.exists_complement (A r bot top x : Set)41  requires h : IsBooleanAlgebra(A, r, bot, top)42  requires hx : x ∈ A43  shows ∃ y, Complementary(A, r, bot, top, x, y)44proof45  rcases h with ⟨bounded, complemented⟩46  exact complemented with x, hx4748-- The complement of an element is its unique complementary element.4950defunique latticeComplement (A r bot top x : Set) (y ∈ A) :=51  Complementary(A, r, bot, top, x, y)52requires boolean : IsBooleanAlgebra(A, r, bot, top)53requires hx : x ∈ A54proof55  obtain ⟨y, hy⟩ := IsBooleanAlgebra.exists_complement with boolean, hx56  witness y57  refine ⟨Complementary.member with hy, hy⟩58uniqueness59  intros y yA first z zA second60  have bounded := IsBooleanAlgebra.bounded_distributive with boolean61  exact Complementary.unique with bounded, hx, first, second6263theorem latticeComplement.member (A r bot top x : Set)64  requires boolean : IsBooleanAlgebra(A, r, bot, top)65  requires hx : x ∈ A66  shows latticeComplement(A, r, bot, top, x) ∈ A67proof68  have selected := latticeComplement.selected with boolean, hx69  exact selected.left7071theorem latticeComplement.complementary (A r bot top x : Set)72  requires boolean : IsBooleanAlgebra(A, r, bot, top)73  requires hx : x ∈ A74  shows Complementary(A, r, bot, top, x, latticeComplement(A, r, bot, top, x))75proof76  have selected := latticeComplement.selected with boolean, hx77  exact selected.right7879theorem latticeComplement.meet (A r bot top x : Set)80  requires boolean : IsBooleanAlgebra(A, r, bot, top)81  requires hx : x ∈ A82  shows meet(A, r, x, latticeComplement(A, r, bot, top, x)) = bot83proof84  exact Complementary.meet with (latticeComplement.complementary with boolean,85      hx)8687theorem latticeComplement.join (A r bot top x : Set)88  requires boolean : IsBooleanAlgebra(A, r, bot, top)89  requires hx : x ∈ A90  shows join(A, r, x, latticeComplement(A, r, bot, top, x)) = top91proof92  exact Complementary.join with (latticeComplement.complementary with boolean,93      hx)9495theorem latticeComplement.meet_left (A r bot top x : Set)96  requires boolean : IsBooleanAlgebra(A, r, bot, top)97  requires hx : x ∈ A98  shows meet(A, r, latticeComplement(A, r, bot, top, x), x) = bot99proof100  have lattice := IsBooleanAlgebra.lattice with boolean101  have swap := meet.commutative with lattice,102      (latticeComplement.member with boolean, hx), hx103  rw swap104  exact latticeComplement.meet with boolean, hx105106theorem latticeComplement.join_left (A r bot top x : Set)107  requires boolean : IsBooleanAlgebra(A, r, bot, top)108  requires hx : x ∈ A109  shows join(A, r, latticeComplement(A, r, bot, top, x), x) = top110proof111  have lattice := IsBooleanAlgebra.lattice with boolean112  have swap := join.commutative with lattice,113      (latticeComplement.member with boolean, hx), hx114  rw swap115  exact latticeComplement.join with boolean, hx116117theorem latticeComplement.of_complementary (A r bot top x y : Set)118  requires boolean : IsBooleanAlgebra(A, r, bot, top)119  requires hx : x ∈ A120  requires h : Complementary(A, r, bot, top, x, y)121  shows y = latticeComplement(A, r, bot, top, x)122proof123  have bounded := IsBooleanAlgebra.bounded_distributive with boolean124  have selected := latticeComplement.complementary with boolean, hx125  exact Complementary.unique with bounded, hx, h, selected126127theorem latticeComplement.involutive (A r bot top x : Set)128  requires boolean : IsBooleanAlgebra(A, r, bot, top)129  requires hx : x ∈ A130  shows131    latticeComplement(A, r, bot, top, latticeComplement(A, r, bot, top, x)) = x132proof133  have bounded := IsBooleanAlgebra.bounded with boolean134  have complementA := latticeComplement.member with boolean, hx135  have selected := latticeComplement.complementary with boolean, hx136  have symmetric := Complementary.symmetric with bounded, hx, selected137  symm138  exact latticeComplement.of_complementary with boolean, complementA, symmetric139140theorem latticeComplement.bottom (A r bot top : Set)141  requires boolean : IsBooleanAlgebra(A, r, bot, top)142  shows latticeComplement(A, r, bot, top, bot) = top143proof144  have bounded := IsBooleanAlgebra.bounded with boolean145  have botA := IsBoundedLattice.bottom_member with bounded146  symm147  exact latticeComplement.of_complementary with boolean, botA,148      (Complementary.bottom_top with bounded)149150theorem latticeComplement.top (A r bot top : Set)151  requires boolean : IsBooleanAlgebra(A, r, bot, top)152  shows latticeComplement(A, r, bot, top, top) = bot153proof154  have bounded := IsBooleanAlgebra.bounded with boolean155  have topA := IsBoundedLattice.top_member with bounded156  symm157  exact latticeComplement.of_complementary with boolean, topA,158      (Complementary.top_bottom with bounded)159160theorem latticeComplement.injective (A r bot top x y : Set)161  requires boolean : IsBooleanAlgebra(A, r, bot, top)162  requires hx : x ∈ A163  requires hy : y ∈ A164  requires same :165    latticeComplement(A, r, bot, top, x) = latticeComplement(A, r, bot, top, y)166  shows x = y167proof168  have twiceX := latticeComplement.involutive with boolean, hx169  have twiceY := latticeComplement.involutive with boolean, hy170  rw ← twiceX171  rw ← twiceY172  rw same173  rfl174175-- De Morgan's laws176177theorem latticeComplement.join_eq (A r bot top x y : Set)178  requires boolean : IsBooleanAlgebra(A, r, bot, top)179  requires hx : x ∈ A180  requires hy : y ∈ A181  shows latticeComplement(A, r, bot, top, join(A, r, x, y)) =182    meet(A, r, latticeComplement(A, r, bot, top, x), latticeComplement(A, r, bot, top, y))183proof184  have distributive := IsBooleanAlgebra.distributive with boolean185  have bounded := IsBooleanAlgebra.bounded with boolean186  have lattice := IsBooleanAlgebra.lattice with boolean187  have xA := latticeComplement.member with boolean, hx188  have yA := latticeComplement.member with boolean, hy189  have joinA := join.member with lattice, hx, hy190  have meetA := meet.member with lattice, xA, yA191  have meetBottom : meet(A, r, join(A, r, x, y), meet(A, r,192      latticeComplement(A, r, bot, top, x), latticeComplement(A, r, bot, top,193      y))) = bot194    have expand := IsDistributiveLattice.meet_join_right with distributive, hx,195        hy, meetA196    have regroupX := meet.associative with lattice, hx, xA, yA197    have swapInner := meet.commutative with lattice, xA, yA198    have regroupY := meet.associative with lattice, hy, yA, xA199    have cancelX := latticeComplement.meet with boolean, hx200    have cancelY := latticeComplement.meet with boolean, hy201    have absorbX := meet.bottom_left with bounded, yA202    have absorbY := meet.bottom_left with bounded, xA203    have botA := IsBoundedLattice.bottom_member with bounded204    rw [expand, ← regroupX, cancelX, absorbX, swapInner, ← regroupY, cancelY,205        absorbY]206    exact join.idempotent with lattice, botA207  have joinTop : join(A, r, join(A, r, x, y), meet(A, r, latticeComplement(A,208      r, bot, top, x), latticeComplement(A, r, bot, top, y))) = top209    have expand := IsDistributiveLattice.join_meet with distributive, joinA, xA,210        yA211    have swapOuter := join.commutative with lattice, hx, hy212    have regroupX := join.associative with lattice, hy, hx, xA213    have cancelX := latticeComplement.join with boolean, hx214    have absorbX := join.top_right with bounded, hy215    have regroupY := join.associative with lattice, hx, hy, yA216    have cancelY := latticeComplement.join with boolean, hy217    have absorbY := join.top_right with bounded, hx218    have topA := IsBoundedLattice.top_member with bounded219    rw expand220    rw [regroupY, cancelY, absorbY]221    rw [swapOuter, regroupX, cancelX, absorbX]222    exact meet.idempotent with lattice, topA223  have complementary : Complementary(A, r, bot, top, join(A, r, x, y), meet(A,224      r, latticeComplement(A, r, bot, top, x), latticeComplement(A, r, bot,225      top, y)))226    refine ⟨meetA, meetBottom, joinTop⟩227  symm228  exact latticeComplement.of_complementary with boolean, joinA, complementary229230theorem latticeComplement.meet_eq (A r bot top x y : Set)231  requires boolean : IsBooleanAlgebra(A, r, bot, top)232  requires hx : x ∈ A233  requires hy : y ∈ A234  shows latticeComplement(A, r, bot, top, meet(A, r, x, y)) =235    join(A, r, latticeComplement(A, r, bot, top, x), latticeComplement(A, r, bot, top, y))236proof237  have lattice := IsBooleanAlgebra.lattice with boolean238  have xA := latticeComplement.member with boolean, hx239  have yA := latticeComplement.member with boolean, hy240  have joinA := join.member with lattice, xA, yA241  have deMorgan := latticeComplement.join_eq with boolean, xA, yA242  have twiceX := latticeComplement.involutive with boolean, hx243  have twiceY := latticeComplement.involutive with boolean, hy244  rw [twiceX, twiceY] at deMorgan245  rw ← deMorgan246  exact latticeComplement.involutive with boolean, joinA247248-- Order and complements249250theorem latticeComplement.le_iff_meet_bottom (A r bot top a b : Set)251  requires boolean : IsBooleanAlgebra(A, r, bot, top)252  requires ha : a ∈ A253  requires hb : b ∈ A254  shows255    relates(r, a, latticeComplement(A, r, bot, top, b)) ↔ meet(A, r, a, b) = bot256proof257  have distributive := IsBooleanAlgebra.distributive with boolean258  have bounded := IsBooleanAlgebra.bounded with boolean259  have lattice := IsBooleanAlgebra.lattice with boolean260  have reflexive := IsLattice.reflexive with lattice261  have bA := latticeComplement.member with boolean, hb262  have abA := meet.member with lattice, ha, hb263  constructor264  . intro below265    have bounded2 := meet.monotone with lattice, ha, hb, bA, hb, below,266        (reflexive with b, hb)267    have cancel := latticeComplement.meet_left with boolean, hb268    rw cancel at bounded2269    exact IsBoundedLattice.le_bottom_iff.forward with bounded, abA, bounded2270  . intro disjoint271    have unit := meet.top_right with bounded, ha272    have cover := latticeComplement.join with boolean, hb273    have expand := IsDistributiveLattice.meet_join with distributive, ha, hb, bA274    have abBotA := meet.member with lattice, ha, bA275    have absorb := join.bottom_left with bounded, abBotA276    symm at absorb277    symm at expand278    have equation : meet(A, r, a, latticeComplement(A, r, bot, top, b)) = a279      calc280        meet(A, r, a, latticeComplement(A, r, bot, top, b)) = join(A, r, bot, meet(A, r, a, latticeComplement(A, r, bot, top, b))) :=281          absorb282        _ = join(A, r, meet(A, r, a, b), meet(A, r, a, latticeComplement(A, r, bot, top, b))) :=283          by simp [disjoint]284        _ = meet(A, r, a, join(A, r, b, latticeComplement(A, r, bot, top, b))) := expand285        _ = meet(A, r, a, top) := by simp [cover]286        _ = a := unit287    exact meet.eq_left_iff.backward with lattice, ha, bA, equation288289theorem latticeComplement.antitone (A r bot top x y : Set)290  requires boolean : IsBooleanAlgebra(A, r, bot, top)291  requires hx : x ∈ A292  requires hy : y ∈ A293  requires hxy : relates(r, x, y)294  shows295    relates(r, latticeComplement(A, r, bot, top, y), latticeComplement(A, r, bot, top, x))296proof297  have bounded := IsBooleanAlgebra.bounded with boolean298  have lattice := IsBooleanAlgebra.lattice with boolean299  have reflexive := IsLattice.reflexive with lattice300  have yA := latticeComplement.member with boolean, hy301  have yxA := meet.member with lattice, yA, hx302  have below := meet.monotone with lattice, yA, hx, yA, hy,303      (reflexive with latticeComplement(A, r, bot, top, y), yA), hxy304  have cancel := latticeComplement.meet_left with boolean, hy305  rw cancel at below306  have disjoint := IsBoundedLattice.le_bottom_iff.forward with bounded, yxA,307    below308  exact latticeComplement.le_iff_meet_bottom.backward with boolean, yA, hx,309      disjoint310311theorem latticeComplement.le_iff (A r bot top x y : Set)312  requires boolean : IsBooleanAlgebra(A, r, bot, top)313  requires hx : x ∈ A314  requires hy : y ∈ A315  shows relates(r, x, y) ↔316    relates(r, latticeComplement(A, r, bot, top, y), latticeComplement(A, r, bot, top, x))317proof318  constructor319  . intro hxy320    exact latticeComplement.antitone with boolean, hx, hy, hxy321  . intro reversed322    have xA := latticeComplement.member with boolean, hx323    have yA := latticeComplement.member with boolean, hy324    have twice := latticeComplement.antitone with boolean, yA, xA, reversed325    have twiceX := latticeComplement.involutive with boolean, hx326    have twiceY := latticeComplement.involutive with boolean, hy327    rw [twiceX, twiceY] at twice328    exact twice329330theorem IsBooleanAlgebra.converse (A r bot top : Set)331  requires boolean : IsBooleanAlgebra(A, r, bot, top)332  shows IsBooleanAlgebra(A, converse(r, A, A), top, bot)333proof334  have bounded := IsBooleanAlgebra.bounded with boolean335  have distributive := IsBooleanAlgebra.bounded_distributive with boolean336  constructor337  . exact BoundedDistributiveLattice.converse with distributive338  . intros x hx339    have selected := latticeComplement.complementary with boolean, hx340    refine ⟨latticeComplement(A, r, bot, top, x),341        (Complementary.converse with bounded, hx, selected)⟩342343-- The powerset of X is a Boolean algebra whose complements are relative344-- complements in X.345346theorem powersetOrder.complementary (X B : Set)347  requires hB : B ∈ 𝒫(X)348  shows Complementary(𝒫(X), powersetOrder(X), ∅, X, B, X ∖ B)349proof350  have BX := powerset.membership_iff.forward with hB351  have differenceIn : X ∖ B ∈ 𝒫(X) :=352    powerset.membership_iff.backward with (difference.subset_left at X, B)353  have meetValue := powersetOrder.meet with hB, differenceIn354  have joinValue := powersetOrder.join with hB, differenceIn355  refine ⟨differenceIn, ?_, ?_⟩356  . rw meetValue357    have swap := intersection.commutative at B, X ∖ B358    rw swap359    exact difference.intersection_eq at X, B360  . rw joinValue361    exact difference.union2_of_subset with BX362363theorem powersetOrder.boolean (X : Set)364  shows IsBooleanAlgebra(𝒫(X), powersetOrder(X), ∅, X)365proof366  constructor367  . exact powersetOrder.bounded_distributive at X368  . intros B hB369    refine ⟨X ∖ B, powersetOrder.complementary with hB⟩370371theorem powersetOrder.complement_value (X B : Set)372  requires hB : B ∈ 𝒫(X)373  shows latticeComplement(𝒫(X), powersetOrder(X), ∅, X, B) = X ∖ B374proof375  have boolean := powersetOrder.boolean at X376  symm377  exact latticeComplement.of_complementary with boolean, hB,378      (powersetOrder.complementary with hB)379