Grace/Cumulus/Lattice/DistribLattice.g17

Open in Workbench Download source

Imports

Distributive · CompleteLattice

Declarations

Source

1-- Distributive and modular lattices bundled as ordered sets2-- 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.DistribLattice8import Distributive9import CompleteLattice1011-- Distributivity and modularity as properties of the bundled order.12predicate DistributiveLattice (P : Set) := IsDistributiveLattice(points(P), le(P))13predicate ModularLattice (P : Set) := IsModularLattice(points(P), le(P))1415notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis DistributiveLattice(P) for P.points16notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis DistributiveLattice(P) for P.points17notation infix 50 "≤" => Le(P, _, _) via hypothesis DistributiveLattice(P) for P.points18notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis ModularLattice(P) for P.points19notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis ModularLattice(P) for P.points20notation infix 50 "≤" => Le(P, _, _) via hypothesis ModularLattice(P) for P.points2122instance DistributiveLattice.unbundled (P : Set)23  requires distributive : DistributiveLattice(P)24  shows IsDistributiveLattice(points(P), le(P))25proof26  simp [DistributiveLattice]2728theorem DistributiveLattice.mk (A r : Set)29  requires distributive : IsDistributiveLattice(A, r)30  shows DistributiveLattice(Order.mk(A, r))31proof32  unfold DistributiveLattice33  rw [Order.mk.points, Order.mk.le]34  exact distributive3536instance DistributiveLattice.lattice_of (P : Set)37  requires distributive : DistributiveLattice(P)38  shows Lattice(P)39proof40  unfold Join.Lattice41  exact IsDistributiveLattice.lattice with42      (DistributiveLattice.unbundled with distributive)4344instance ModularLattice.unbundled (P : Set)45  requires modular : ModularLattice(P)46  shows IsModularLattice(points(P), le(P))47proof48  simp [ModularLattice]4950theorem ModularLattice.mk (A r : Set)51  requires modular : IsModularLattice(A, r)52  shows ModularLattice(Order.mk(A, r))53proof54  unfold ModularLattice55  rw [Order.mk.points, Order.mk.le]56  exact modular5758instance ModularLattice.lattice_of (P : Set)59  requires modular : ModularLattice(P)60  shows Lattice(P)61proof62  unfold Join.Lattice63  exact IsModularLattice.lattice with (ModularLattice.unbundled with modular)6465theorem DistributiveLattice.modular_of (P : Set)66  requires distributive : DistributiveLattice(P)67  shows ModularLattice(P)68proof69  unfold ModularLattice70  exact IsDistributiveLattice.modular with71      (DistributiveLattice.unbundled with distributive)7273theorem DistributiveLattice.dual (P : Set)74  requires distributive : DistributiveLattice(P)75  shows DistributiveLattice(dual(P))76proof77  unfold dual78  apply DistributiveLattice.mk79  exact IsDistributiveLattice.converse with80      (DistributiveLattice.unbundled with distributive)8182section DistributiveLaws83variable (P : Set)84hypothesis distributive : DistributiveLattice(P)8586theorem inf_sup_left (a b c ∈ points(P))87  shows a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)88proof89  simp [sup.join, inf.meet]90  exact IsDistributiveLattice.meet_join with *9192theorem inf_sup_right (a b c ∈ points(P))93  shows (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)94proof95  simp [sup.join, inf.meet]96  exact IsDistributiveLattice.meet_join_right with *9798theorem sup_inf_left (a b c ∈ points(P))99  shows a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)100proof101  simp [sup.join, inf.meet]102  exact IsDistributiveLattice.join_meet with *103104theorem sup_inf_right (a b c ∈ points(P))105  shows (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)106proof107  simp [sup.join, inf.meet]108  exact IsDistributiveLattice.join_meet_right with *109110theorem eq_of_inf_eq_sup_eq (a b c ∈ points(P))111  requires meets : a ⊓ b = a ⊓ c112  requires joins : a ⊔ b = a ⊔ c113  shows b = c114proof115  simp [sup.join, inf.meet] at meets116  simp [sup.join, inf.meet] at joins117  exact IsDistributiveLattice.cancel with *118119end DistributiveLaws120121-- A lattice is distributive when either distributive law holds.122theorem DistributiveLattice.of_inf_sup_left (P : Set)123  requires lattice : Lattice(P)124  requires law : ∀ a b c ∈ points(P), a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)125  shows DistributiveLattice(P)126proof127  unfold DistributiveLattice128  constructor129  . exact Lattice.unbundled with lattice130  . intros a aIn b bIn c cIn131    have bridged := law with a, aIn, b, bIn, c, cIn132    simp [sup.join, inf.meet] at bridged133    exact bridged134135theorem DistributiveLattice.of_sup_inf_left (P : Set)136  requires lattice : Lattice(P)137  requires law : ∀ a b c ∈ points(P), a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)138  shows DistributiveLattice(P)139proof140  unfold DistributiveLattice141  apply IsDistributiveLattice.of_join_meet with (Lattice.unbundled with lattice)142  intros a aIn b bIn c cIn143  have bridged := law with a, aIn, b, bIn, c, cIn144  simp [sup.join, inf.meet] at bridged145  exact bridged146147section ModularLaws148variable (P : Set)149hypothesis modular : ModularLattice(P)150151theorem inf_sup_assoc_of_le (a b c ∈ points(P))152  requires hba : b ≤ a153  shows a ⊓ (b ⊔ c) = b ⊔ (a ⊓ c)154proof155  simp [sup.join, inf.meet]156  exact IsModularLattice.law with *157158end ModularLaws159160section ComplementLaws161variable (P : Set)162hypothesis distributive : DistributiveLattice(P)163hypothesis bounded : BoundedLattice(P)164165theorem BoundedLattice.bounded_distributive166  shows BoundedDistributiveLattice(points(P), le(P), bot(P), top(P))167proof168  exact BoundedDistributiveLattice.of_bounds with169      (DistributiveLattice.unbundled with distributive),170      (BoundedLattice.unbundled with bounded)171172theorem IsCompl.unique (b c : Set) (a ∈ points(P))173  requires first : IsCompl(P, a, b)174  requires second : IsCompl(P, a, c)175  shows b = c176proof177  have both := BoundedLattice.bounded_distributive with distributive, bounded178  have firstC := IsCompl.unbundled with bounded, first179  have secondC := IsCompl.unbundled with bounded, second180  exact Complementary.unique with both, assumption, firstC, secondC181182end ComplementLaws183184instance powersetLattice.distributive (X : Set)185  shows DistributiveLattice(powersetLattice(X))186proof187  unfold powersetLattice188  exact DistributiveLattice.mk with (powersetOrder.distributive at X)189