Grace/Cumulus/Lattice/CompleteLattice.g17

Open in Workbench Download source

Imports

Complete · BoundedOrder

Declarations

Source

1-- Complete lattices bundled as ordered sets, with sSup(P) and sInf(P), and2-- the powerset lattice3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Lattice.CompleteLattice9import Complete10import BoundedOrder1112-- A complete lattice is a property of the bundled order; the supremum and13-- infimum of a subset are the set functions sSup(P) and sInf(P) on the14-- powerset of the points, applied as sSup(P)(S).15predicate CompleteLattice (P : Set) := IsCompleteLattice(points(P), le(P))1617notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis CompleteLattice(P) for P.points18notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis CompleteLattice(P) for P.points19notation infix 50 "≤" => Le(P, _, _) via hypothesis CompleteLattice(P) for P.points2021instance CompleteLattice.unbundled (P : Set)22  requires complete : CompleteLattice(P)23  shows IsCompleteLattice(points(P), le(P))24proof25  simp [CompleteLattice]2627theorem CompleteLattice.mk (A r : Set)28  requires complete : IsCompleteLattice(A, r)29  shows CompleteLattice(Order.mk(A, r))30proof31  unfold CompleteLattice32  rw [Order.mk.points, Order.mk.le]33  exact complete3435theorem CompleteLattice.lattice_of (P : Set)36  requires complete : CompleteLattice(P)37  shows Lattice(P)38proof39  unfold Join.Lattice40  exact IsCompleteLattice.lattice with (CompleteLattice.unbundled with complete)4142instance CompleteLattice.bounded_of (P : Set)43  requires complete : CompleteLattice(P)44  shows BoundedLattice(P)45proof46  have unbundled := CompleteLattice.unbundled with complete47  have bounded := IsCompleteLattice.bounded with unbundled48  have lattice : Lattice(P) := CompleteLattice.lattice_of with complete49  refine ⟨lattice, ?_, ?_⟩50  . witness supremum(points(P), le(P), ∅)51    exact IsBoundedLattice.least with bounded52  . witness supremum(points(P), le(P), points(P))53    exact IsBoundedLattice.greatest with bounded5455theorem CompleteLattice.subset_of_member (P S : Set)56  requires member : S ∈ 𝒫(points(P))57  shows S ⊆ points(P)58proof59  exact powerset.membership_iff.forward with member6061defgraph sSup (P : Set) (S ∈ 𝒫(points(P))) : points(P) := supremum(points(P), le(P), S)62requires complete : CompleteLattice(P)63proof64  have subset := CompleteLattice.subset_of_member with member65  exact supremum.member with (CompleteLattice.unbundled with complete), subset6667defgraph sInf (P : Set) (S ∈ 𝒫(points(P))) : points(P) := infimum(points(P), le(P), S)68requires complete : CompleteLattice(P)69proof70  have subset := CompleteLattice.subset_of_member with member71  exact infimum.member with (CompleteLattice.unbundled with complete), subset7273-- The supremum and infimum of a subset S of the points are written ⨆ S74-- and ⨅ S, and the bounds ⊥ and ⊤, wherever a hypothesis in scope supplies75-- the complete lattice; each value lies in points(P).76notation prefix 90 "⨆" => apply(sSup(P), _) via hypothesis CompleteLattice(P) for P.points77notation prefix 90 "⨅" => apply(sInf(P), _) via hypothesis CompleteLattice(P) for P.points78notation constant "⊥" => bot(P) via hypothesis CompleteLattice(P) for P.points79notation constant "⊤" => top(P) via hypothesis CompleteLattice(P) for P.points8081section CompleteLatticeLaws82variable (P : Set)83hypothesis complete : CompleteLattice(P)8485-- The bundled operations are the unbundled supremum and infimum.86theorem sSup.supremum (S : Set)87  requires hS : S ⊆ points(P)88  shows sSup(P)(S) = supremum(points(P), le(P), S)89proof90  have member : S ∈ 𝒫(points(P)) := powerset.membership_iff.backward with hS91  exact sSup.value with complete, member9293theorem sInf.infimum (S : Set)94  requires hS : S ⊆ points(P)95  shows sInf(P)(S) = infimum(points(P), le(P), S)96proof97  have member : S ∈ 𝒫(points(P)) := powerset.membership_iff.backward with hS98  exact sInf.value with complete, member99100instance sSup.member (S : Set)101  requires hS : S ⊆ points(P)102  shows sSup(P)(S) ∈ points(P)103proof104  rw sSup.supremum105  exact supremum.member with *106107instance sInf.member (S : Set)108  requires hS : S ⊆ points(P)109  shows sInf(P)(S) ∈ points(P)110proof111  rw sInf.infimum112  exact infimum.member with *113114theorem sSup.isLUB (S : Set)115  requires hS : S ⊆ points(P)116  shows IsLUB(P, S, sSup(P)(S))117proof118  unfold IsLUB119  rw sSup.supremum120  exact supremum.supremum with *121122theorem sInf.isGLB (S : Set)123  requires hS : S ⊆ points(P)124  shows IsGLB(P, S, sInf(P)(S))125proof126  unfold IsGLB127  rw sInf.infimum128  exact infimum.infimum with *129130theorem le_sSup (S a : Set)131  requires hS : S ⊆ points(P)132  requires aIn : a ∈ S133  shows a ≤ ⨆ S134proof135  unfold Le136  rw sSup.supremum137  exact supremum.above with *138139theorem sSup_le (S : Set) (b ∈ points(P))140  requires hS : S ⊆ points(P)141  requires bound : ∀ x ∈ S, x ≤ b142  shows sSup(P)(S) ≤ b143proof144  unfold Le145  rw sSup.supremum146  have bIn : b ∈ points(P) by assumption147  have above : ∀ x ∈ S, relates(le(P), x, b)148    intros x xIn149    exact Le.relates with (bound with x, xIn)150  have upper : UpperBound(points(P), le(P), S, b) := ⟨bIn, hS, above⟩151  exact supremum.least with *152153theorem sInf_le (S a : Set)154  requires hS : S ⊆ points(P)155  requires aIn : a ∈ S156  shows ⨅ S ≤ a157proof158  unfold Le159  rw sInf.infimum160  exact infimum.below with *161162theorem le_sInf (S : Set) (b ∈ points(P))163  requires hS : S ⊆ points(P)164  requires bound : ∀ x ∈ S, b ≤ x165  shows b ≤ sInf(P)(S)166proof167  unfold Le168  rw sInf.infimum169  have bIn : b ∈ points(P) by assumption170  have below : ∀ x ∈ S, relates(le(P), b, x)171    intros x xIn172    exact Le.relates with (bound with x, xIn)173  have lower : LowerBound(points(P), le(P), S, b) := ⟨bIn, hS, below⟩174  exact infimum.greatest with *175176theorem sSup_le_iff (S : Set) (b ∈ points(P))177  requires hS : S ⊆ points(P)178  shows sSup(P)(S) ≤ b ↔ ∀ x ∈ S, x ≤ b179proof180  constructor181  . intros h x xIn182    have xIn2 : x ∈ points(P) := hS with x, xIn183    have above : x ≤ sSup(P)(S) := le_sSup with *184    exact le_trans with above, h185  . intro bound186    exact sSup_le with *187188theorem le_sInf_iff (S : Set) (b ∈ points(P))189  requires hS : S ⊆ points(P)190  shows b ≤ sInf(P)(S) ↔ ∀ x ∈ S, b ≤ x191proof192  constructor193  . intros h x xIn194    have xIn2 : x ∈ points(P) := hS with x, xIn195    have below : sInf(P)(S) ≤ x := sInf_le with *196    exact le_trans with h, below197  . intro bound198    exact le_sInf with *199200theorem sSup.of_isLUB (S s : Set)201  requires hS : S ⊆ points(P)202  requires lub : IsLUB(P, S, s)203  shows s = sSup(P)(S)204proof205  unfold IsLUB at lub206  rw sSup.supremum207  exact supremum.of_supremum with *208209theorem sInf.of_isGLB (S i : Set)210  requires hS : S ⊆ points(P)211  requires glb : IsGLB(P, S, i)212  shows i = sInf(P)(S)213proof214  unfold IsGLB at glb215  rw sInf.infimum216  exact infimum.of_infimum with *217218theorem sSup_le_sSup (S T : Set)219  requires hST : S ⊆ T220  requires hT : T ⊆ points(P)221  shows sSup(P)(S) ≤ sSup(P)(T)222proof223  unfold Le224  have hS : S ⊆ points(P) := Subset.transitive with hST, hT225  rw [sSup.supremum, sSup.supremum]226  exact supremum.monotone with *227228theorem sInf_le_sInf (S T : Set)229  requires hST : S ⊆ T230  requires hT : T ⊆ points(P)231  shows sInf(P)(T) ≤ sInf(P)(S)232proof233  unfold Le234  have hS : S ⊆ points(P) := Subset.transitive with hST, hT235  rw [sInf.infimum, sInf.infimum]236  exact infimum.antitone with *237238theorem sSup_pair (a b ∈ points(P))239  shows sSup(P)({a, b}) = a ⊔ b240proof241  have hS : {a, b} ⊆ points(P) by simp242  rw [sSup.supremum, sup.join]243  exact supremum.pair with *244245theorem sInf_pair (a b ∈ points(P))246  shows sInf(P)({a, b}) = a ⊓ b247proof248  have hS : {a, b} ⊆ points(P) by simp249  rw [sInf.infimum, inf.meet]250  exact infimum.pair with *251252theorem sSup_singleton (a ∈ points(P))253  shows sSup(P)({a}) = a254proof255  have hS : {a} ⊆ points(P) by simp256  rw sSup.supremum257  exact supremum.singleton with *258259theorem sInf_singleton (a ∈ points(P))260  shows sInf(P)({a}) = a261proof262  have hS : {a} ⊆ points(P) by simp263  rw sInf.infimum264  exact infimum.singleton with *265266theorem sSup_empty267  shows sSup(P)(∅) = bot(P)268proof269  have hS : ∅ ⊆ points(P) := empty.subset at points(P)270  have least : IsLeast(P, points(P), sSup(P)(∅))271    unfold IsLeast272    rw sSup.supremum273    exact supremum.empty with *274  exact bot_unique with *275276theorem sInf_empty277  shows sInf(P)(∅) = top(P)278proof279  have hS : ∅ ⊆ points(P) := empty.subset at points(P)280  have greatest : IsGreatest(P, points(P), sInf(P)(∅))281    unfold IsGreatest282    rw sInf.infimum283    exact infimum.empty with *284  exact top_unique with *285286theorem sSup_univ287  shows sSup(P)(points(P)) = top(P)288proof289  have hS : points(P) ⊆ points(P) := Subset.reflexive at points(P)290  have greatest : IsGreatest(P, points(P), sSup(P)(points(P)))291    unfold IsGreatest292    rw sSup.supremum293    exact supremum.whole with *294  exact top_unique with *295296theorem sInf_univ297  shows sInf(P)(points(P)) = bot(P)298proof299  have hS : points(P) ⊆ points(P) := Subset.reflexive at points(P)300  have least : IsLeast(P, points(P), sInf(P)(points(P)))301    unfold IsLeast302    rw sInf.infimum303    exact infimum.whole with *304  exact bot_unique with *305306theorem sSup_union (S T : Set)307  requires hS : S ⊆ points(P)308  requires hT : T ⊆ points(P)309  shows sSup(P)(S ∪ T) = sSup(P)(S) ⊔ sSup(P)(T)310proof311  have hST : S ∪ T ⊆ points(P) := union2.subset with *312  rw [sup.join, sSup.supremum, sSup.supremum, sSup.supremum]313  exact supremum.union2 with *314315theorem sInf_union (S T : Set)316  requires hS : S ⊆ points(P)317  requires hT : T ⊆ points(P)318  shows sInf(P)(S ∪ T) = sInf(P)(S) ⊓ sInf(P)(T)319proof320  have hST : S ∪ T ⊆ points(P) := union2.subset with *321  rw [inf.meet, sInf.infimum, sInf.infimum, sInf.infimum]322  exact infimum.union2 with *323324end CompleteLatticeLaws325326-- The powerset of a set under inclusion is a complete lattice: join is327-- union, meet is intersection, and the supremum of a family is its union.328def powersetLattice (X : Set) : Set := Order.mk(𝒫(X), powersetOrder(X))329330theorem powersetLattice.points (X : Set)331  shows points(powersetLattice(X)) = 𝒫(X)332proof333  simp [powersetLattice, Order.mk.points]334335theorem powersetLattice.le (X : Set)336  shows le(powersetLattice(X)) = powersetOrder(X)337proof338  simp [powersetLattice, Order.mk.le]339340instance powersetLattice.complete (X : Set)341  shows CompleteLattice(powersetLattice(X))342proof343  unfold powersetLattice344  exact CompleteLattice.mk with (IsCompleteLattice.powerset at X)345346section PowersetLattice347variable (X : Set)348hypothesis complete : CompleteLattice(powersetLattice(X))349350theorem powersetLattice.member (B : Set)351  requires hB : B ∈ 𝒫(X)352  shows B ∈ points(powersetLattice(X))353proof354  rw powersetLattice.points355  exact hB356357theorem powersetLattice.le_iff (B C ∈ 𝒫(X))358  shows B ≤ C ↔ B ⊆ C359proof360  have characterization := powersetOrder.relates at X, B, C with *361  rw ← powersetLattice.le at characterization362  constructor363  . intro h364    exact characterization.forward with (Le.relates with h)365  . intro h366    exact Le.of_relates with (characterization.backward with h)367368theorem powersetLattice.sup (B C ∈ 𝒫(X))369  shows B ⊔ C = B ∪ C370proof371  have BIn : B ∈ points(powersetLattice(X)) := powersetLattice.member at X, B with *372  have CIn : C ∈ points(powersetLattice(X)) := powersetLattice.member at X, C with *373  rw [sup.join, powersetLattice.points, powersetLattice.le]374  exact powersetOrder.join with *375376theorem powersetLattice.inf (B C ∈ 𝒫(X))377  shows B ⊓ C = B ∩ C378proof379  have BIn : B ∈ points(powersetLattice(X)) := powersetLattice.member at X, B with *380  have CIn : C ∈ points(powersetLattice(X)) := powersetLattice.member at X, C with *381  rw [inf.meet, powersetLattice.points, powersetLattice.le]382  exact powersetOrder.meet with *383384theorem powersetLattice.sSup (S : Set)385  requires hS : S ⊆ 𝒫(X)386  shows sSup(powersetLattice(X))(S) = ⋃(S)387proof388  have subset : S ⊆ points(powersetLattice(X))389    rw powersetLattice.points390    exact hS391  rw [sSup.supremum, powersetLattice.points, powersetLattice.le]392  exact powersetOrder.supremum_value with *393394theorem powersetLattice.sInf (S : Set)395  requires hS : S ⊆ 𝒫(X)396  shows sInf(powersetLattice(X))(S) = relativeIntersection(X, S)397proof398  have subset : S ⊆ points(powersetLattice(X))399    rw powersetLattice.points400    exact hS401  rw [sInf.infimum, powersetLattice.points, powersetLattice.le]402  exact powersetOrder.infimum_value with *403404theorem powersetLattice.bot405  shows bot(powersetLattice(X)) = ∅406proof407  unfold powersetLattice408  exact bot.mk with (powersetOrder.bounded at X)409410theorem powersetLattice.top411  shows top(powersetLattice(X)) = X412proof413  unfold powersetLattice414  exact top.mk with (powersetOrder.bounded at X)415416end PowersetLattice417