Grace/Cumulus/Lattice/Distributive.g17

Open in Workbench Download source

Imports

Complete

Declarations

Source

1-- Distributive and modular lattices, cancellation, and unique complements2-- 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.Distributive8import Complete910predicate IsDistributiveLattice (A r : Set) :=11  IsLattice(A, r) ∧12  (∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A,13    meet(A, r, x, join(A, r, y, z)) = join(A, r, meet(A, r, x, y), meet(A, r, x, z)))1415predicate IsModularLattice (A r : Set) :=16  IsLattice(A, r) ∧17  (∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A, relates(r, y, x) →18    meet(A, r, x, join(A, r, y, z)) = join(A, r, y, meet(A, r, x, z)))1920predicate BoundedDistributiveLattice (A r bot top : Set) :=21  IsDistributiveLattice(A, r) ∧ Least(A, r, A, bot) ∧ Greatest(A, r, A, top)2223theorem IsDistributiveLattice.lattice (A r : Set)24  requires h : IsDistributiveLattice(A, r)25  shows IsLattice(A, r)26proof27  simp [IsDistributiveLattice]2829theorem IsDistributiveLattice.meet_join (A r x y z : Set)30  requires h : IsDistributiveLattice(A, r)31  requires hx : x ∈ A32  requires hy : y ∈ A33  requires hz : z ∈ A34  shows35    meet(A, r, x, join(A, r, y, z)) = join(A, r, meet(A, r, x, y), meet(A, r, x, z))36proof37  rcases h with ⟨lattice, law⟩38  exact law with x, hx, y, hy, z, hz3940theorem IsDistributiveLattice.meet_join_right (A r x y z : Set)41  requires h : IsDistributiveLattice(A, r)42  requires hx : x ∈ A43  requires hy : y ∈ A44  requires hz : z ∈ A45  shows46    meet(A, r, join(A, r, x, y), z) = join(A, r, meet(A, r, x, z), meet(A, r, y, z))47proof48  have lattice := IsDistributiveLattice.lattice with h49  have xyA := join.member with lattice, hx, hy50  have outer := meet.commutative with lattice, xyA, hz51  have leftSwap := meet.commutative with lattice, hz, hx52  have rightSwap := meet.commutative with lattice, hz, hy53  have expand := IsDistributiveLattice.meet_join with h, hz, hx, hy54  rw [outer, expand, leftSwap, rightSwap]55  rfl5657-- The dual distributive law follows from the first.5859theorem IsDistributiveLattice.join_meet (A r x y z : Set)60  requires h : IsDistributiveLattice(A, r)61  requires hx : x ∈ A62  requires hy : y ∈ A63  requires hz : z ∈ A64  shows65    join(A, r, x, meet(A, r, y, z)) = meet(A, r, join(A, r, x, y), join(A, r, x, z))66proof67  have lattice := IsDistributiveLattice.lattice with h68  have xyA := join.member with lattice, hx, hy69  have zxA := meet.member with lattice, hz, hx70  have zyA := meet.member with lattice, hz, hy71  have expand := IsDistributiveLattice.meet_join with h, xyA, hx, hz72  have absorbFirst : meet(A, r, join(A, r, x, y), x) = x73    have swap := meet.commutative with lattice, xyA, hx74    rw swap75    exact meet.absorb with lattice, hx, hy76  have swapSecond := meet.commutative with lattice, xyA, hz77  have expandSecond := IsDistributiveLattice.meet_join with h, hz, hx, hy78  have regroup := join.associative with lattice, hx, zxA, zyA79  have absorbSecond := join.absorb_swap with lattice, hx, hz80  have swapLast := meet.commutative with lattice, hz, hy81  symm82  rw [expand, absorbFirst, swapSecond, expandSecond, ← regroup, absorbSecond,83      swapLast]84  rfl8586theorem IsDistributiveLattice.of_join_meet (A r : Set)87  requires lattice : IsLattice(A, r)88  requires law : ∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ A,89    join(A, r, x, meet(A, r, y, z)) = meet(A, r, join(A, r, x, y), join(A, r, x, z))90  shows IsDistributiveLattice(A, r)91proof92  constructor93  . exact lattice94  . intros x hx y hy z hz95    have xyA := meet.member with lattice, hx, hy96    have zxA := join.member with lattice, hz, hx97    have zyA := join.member with lattice, hz, hy98    have expand := law with meet(A, r, x, y), xyA, x, hx, z, hz99    have absorbFirst : join(A, r, meet(A, r, x, y), x) = x100      have swap := join.commutative with lattice, xyA, hx101      rw swap102      exact join.absorb with lattice, hx, hy103    have swapSecond := join.commutative with lattice, xyA, hz104    have expandSecond := law with z, hz, x, hx, y, hy105    have regroup := meet.associative with lattice, hx, zxA, zyA106    have absorbSecond := meet.absorb_swap with lattice, hx, hz107    have swapLast := join.commutative with lattice, hz, hy108    symm109    rw [expand, absorbFirst, swapSecond, expandSecond, ← regroup,110        absorbSecond, swapLast]111    rfl112113theorem IsDistributiveLattice.join_meet_right (A r x y z : Set)114  requires h : IsDistributiveLattice(A, r)115  requires hx : x ∈ A116  requires hy : y ∈ A117  requires hz : z ∈ A118  shows119    join(A, r, meet(A, r, x, y), z) = meet(A, r, join(A, r, x, z), join(A, r, y, z))120proof121  have lattice := IsDistributiveLattice.lattice with h122  have xyA := meet.member with lattice, hx, hy123  have outer := join.commutative with lattice, xyA, hz124  have leftSwap := join.commutative with lattice, hz, hx125  have rightSwap := join.commutative with lattice, hz, hy126  have expand := IsDistributiveLattice.join_meet with h, hz, hx, hy127  rw [outer, expand, leftSwap, rightSwap]128  rfl129130theorem IsDistributiveLattice.converse (A r : Set)131  requires h : IsDistributiveLattice(A, r)132  shows IsDistributiveLattice(A, converse(r, A, A))133proof134  have lattice := IsDistributiveLattice.lattice with h135  constructor136  . exact IsLattice.converse with lattice137  . intros x hx y hy z hz138    have yzA := meet.member with lattice, hy, hz139    have xyA := join.member with lattice, hx, hy140    have xzA := join.member with lattice, hx, hz141    have inner := join.converse with lattice, hy, hz142    have outer := meet.converse with lattice, hx, yzA143    have leftDual := meet.converse with lattice, hx, hy144    have rightDual := meet.converse with lattice, hx, hz145    have joined := join.converse with lattice, xyA, xzA146    rw [inner, outer, leftDual, rightDual, joined]147    exact IsDistributiveLattice.join_meet with h, hx, hy, hz148149-- Modularity150151theorem IsModularLattice.lattice (A r : Set)152  requires h : IsModularLattice(A, r)153  shows IsLattice(A, r)154proof155  simp [IsModularLattice]156157theorem IsModularLattice.law (A r x y z : Set)158  requires h : IsModularLattice(A, r)159  requires hx : x ∈ A160  requires hy : y ∈ A161  requires hz : z ∈ A162  requires hyx : relates(r, y, x)163  shows meet(A, r, x, join(A, r, y, z)) = join(A, r, y, meet(A, r, x, z))164proof165  rcases h with ⟨lattice, law⟩166  exact law with x, hx, y, hy, z, hz, hyx167168theorem IsDistributiveLattice.modular (A r : Set)169  requires h : IsDistributiveLattice(A, r)170  shows IsModularLattice(A, r)171proof172  have lattice := IsDistributiveLattice.lattice with h173  constructor174  . exact lattice175  . intros x hx y hy z hz hyx176    have expand := IsDistributiveLattice.meet_join with h, hx, hy, hz177    have below := meet.of_ge with lattice, hx, hy, hyx178    rw [expand, below]179    rfl180181-- Cancellation: in a distributive lattice an element is determined by its182-- meet and join with any fixed element.183184theorem IsDistributiveLattice.cancel (A r x y z : Set)185  requires h : IsDistributiveLattice(A, r)186  requires hx : x ∈ A187  requires hy : y ∈ A188  requires hz : z ∈ A189  requires meets : meet(A, r, x, y) = meet(A, r, x, z)190  requires joins : join(A, r, x, y) = join(A, r, x, z)191  shows y = z192proof193  have lattice := IsDistributiveLattice.lattice with h194  have startAbsorb := meet.absorb_swap with lattice, hy, hx195  have expand := IsDistributiveLattice.meet_join with h, hy, hx, hz196  have swap := meet.commutative with lattice, hy, hx197  have collect := IsDistributiveLattice.meet_join_right with h, hx, hy, hz198  have endAbsorb := meet.absorb_swap with lattice, hz, hx199  have xzA := join.member with lattice, hx, hz200  have endSwap := meet.commutative with lattice, xzA, hz201  symm at startAbsorb202  symm at collect203  calc204    y = meet(A, r, y, join(A, r, x, y)) := startAbsorb205    _ = meet(A, r, y, join(A, r, x, z)) := by simp [joins]206    _ = join(A, r, meet(A, r, y, x), meet(A, r, y, z)) := expand207    _ = join(A, r, meet(A, r, x, y), meet(A, r, y, z)) := by simp [swap]208    _ = join(A, r, meet(A, r, x, z), meet(A, r, y, z)) := by simp [meets]209    _ = meet(A, r, join(A, r, x, y), z) := collect210    _ = meet(A, r, join(A, r, x, z), z) := by simp [joins]211    _ = meet(A, r, z, join(A, r, x, z)) := endSwap212    _ = z := endAbsorb213214-- Bounded distributive lattices and the uniqueness of complements215216theorem BoundedDistributiveLattice.distributive (A r bot top : Set)217  requires h : BoundedDistributiveLattice(A, r, bot, top)218  shows IsDistributiveLattice(A, r)219proof220  simp [BoundedDistributiveLattice]221222theorem BoundedDistributiveLattice.lattice (A r bot top : Set)223  requires h : BoundedDistributiveLattice(A, r, bot, top)224  shows IsLattice(A, r)225proof226  exact IsDistributiveLattice.lattice with227      (BoundedDistributiveLattice.distributive with h)228229theorem BoundedDistributiveLattice.bounded (A r bot top : Set)230  requires h : BoundedDistributiveLattice(A, r, bot, top)231  shows IsBoundedLattice(A, r, bot, top)232proof233  rcases h with ⟨distributive, least, greatest⟩234  have lattice := IsDistributiveLattice.lattice with distributive235  exact IsBoundedLattice.of_bounds with lattice, least, greatest236237theorem BoundedDistributiveLattice.of_bounds (A r bot top : Set)238  requires distributive : IsDistributiveLattice(A, r)239  requires bounded : IsBoundedLattice(A, r, bot, top)240  shows BoundedDistributiveLattice(A, r, bot, top)241proof242  refine ⟨distributive, IsBoundedLattice.least with bounded,243      IsBoundedLattice.greatest with bounded⟩244245theorem BoundedDistributiveLattice.converse (A r bot top : Set)246  requires h : BoundedDistributiveLattice(A, r, bot, top)247  shows BoundedDistributiveLattice(A, converse(r, A, A), top, bot)248proof249  have distributive := BoundedDistributiveLattice.distributive with h250  have bounded := BoundedDistributiveLattice.bounded with h251  exact BoundedDistributiveLattice.of_bounds with252      (IsDistributiveLattice.converse with distributive), (IsBoundedLattice.converse with bounded)253254theorem Complementary.unique (A r bot top x y z : Set)255  requires h : BoundedDistributiveLattice(A, r, bot, top)256  requires hx : x ∈ A257  requires hy : Complementary(A, r, bot, top, x, y)258  requires hz : Complementary(A, r, bot, top, x, z)259  shows y = z260proof261  have distributive := BoundedDistributiveLattice.distributive with h262  have yA := Complementary.member with hy263  have zA := Complementary.member with hz264  have meetY := Complementary.meet with hy265  have meetZ := Complementary.meet with hz266  have joinY := Complementary.join with hy267  have joinZ := Complementary.join with hz268  have meets : meet(A, r, x, y) = meet(A, r, x, z)269    rw [meetY, meetZ]270    rfl271  have joins : join(A, r, x, y) = join(A, r, x, z)272    rw [joinY, joinZ]273    rfl274  exact IsDistributiveLattice.cancel with distributive, hx, yA, zA, meets, joins275276-- The powerset lattice is distributive.277278theorem powersetOrder.distributive (X : Set)279  shows IsDistributiveLattice(𝒫(X), powersetOrder(X))280proof281  constructor282  . exact powersetOrder.lattice at X283  . intros B hB C hC D hD284    have CX := powerset.membership_iff.forward with hC285    have DX := powerset.membership_iff.forward with hD286    have BX := powerset.membership_iff.forward with hB287    have unionIn : C ∪ D ∈ 𝒫(X) :=288      powerset.membership_iff.backward with (union2.subset with CX, DX)289    have leftIn : B ∩ C ∈ 𝒫(X) :=290      powerset.membership_iff.backward with (Subset.transitive with (intersection.subset_left at B, C), BX)291    have rightIn : B ∩ D ∈ 𝒫(X) :=292      powerset.membership_iff.backward with (Subset.transitive with (intersection.subset_left at B, D), BX)293    have innerJoin := powersetOrder.join with hC, hD294    have outerMeet := powersetOrder.meet with hB, unionIn295    have leftMeet := powersetOrder.meet with hB, hC296    have rightMeet := powersetOrder.meet with hB, hD297    have outerJoin := powersetOrder.join with leftIn, rightIn298    rw [innerJoin, outerMeet, leftMeet, rightMeet, outerJoin]299    exact intersection.union2_distrib at B, C, D300301theorem powersetOrder.bounded_distributive (X : Set)302  shows BoundedDistributiveLattice(𝒫(X), powersetOrder(X), ∅, X)303proof304  exact BoundedDistributiveLattice.of_bounds with305      (powersetOrder.distributive at X), (powersetOrder.bounded at X)306