Grace/Cumulus/Lattice/Join.g17

Open in Workbench Download source

Imports

LatticeLaws · Order

Declarations

Source

1-- Lattices bundled as ordered sets, with join and meet written ⊔ and ⊓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.Join8import LatticeLaws9import Order1011-- A lattice as a property of a bundled order. The join and meet of two12-- elements are set functions sup(P) and inf(P) on points(P) × points(P),13-- applied as a ⊔ b and a ⊓ b wherever a hypothesis Lattice(P) is in scope.14predicate Lattice (P : Set) := IsLattice(points(P), le(P))1516instance Lattice.unbundled (P : Set)17  requires lattice : Lattice(P)18  shows IsLattice(points(P), le(P))19proof20  simp [Lattice]2122theorem Lattice.mk (A r : Set)23  requires lattice : IsLattice(A, r)24  shows Lattice(Order.mk(A, r))25proof26  unfold Lattice27  rw [Order.mk.points, Order.mk.le]28  exact lattice2930instance Lattice.partial_order (P : Set)31  requires lattice : Lattice(P)32  shows PartialOrder(P)33proof34  unfold Order.PartialOrder35  exact IsLattice.order with (Lattice.unbundled with lattice)3637def pairJoin (P p : Set) : Set :=38  join(points(P), le(P), firstOf(points(P), points(P), p), secondOf(points(P), points(P), p))39def pairMeet (P p : Set) : Set :=40  meet(points(P), le(P), firstOf(points(P), points(P), p), secondOf(points(P), points(P), p))4142theorem pairJoin.pair (P a b : Set)43  requires aIn : a ∈ points(P)44  requires bIn : b ∈ points(P)45  shows pairJoin(P, (a, b)) = join(points(P), le(P), a, b)46proof47  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *48  obtain ⟨firstIn, y, yIn, shape⟩ := firstOf.selected with pairIn49  obtain ⟨secondIn, x, xIn, shape2⟩ := secondOf.selected with pairIn50  have coordinates := orderedPair.injective with shape51  have coordinates2 := orderedPair.injective with shape252  unfold pairJoin53  cc5455theorem pairMeet.pair (P a b : Set)56  requires aIn : a ∈ points(P)57  requires bIn : b ∈ points(P)58  shows pairMeet(P, (a, b)) = meet(points(P), le(P), a, b)59proof60  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *61  obtain ⟨firstIn, y, yIn, shape⟩ := firstOf.selected with pairIn62  obtain ⟨secondIn, x, xIn, shape2⟩ := secondOf.selected with pairIn63  have coordinates := orderedPair.injective with shape64  have coordinates2 := orderedPair.injective with shape265  unfold pairMeet66  cc6768defgraph sup (P : Set) (p ∈ points(P) × points(P)) : points(P) := pairJoin(P, p)69requires lattice : Lattice(P)70proof71  have unbundled := Lattice.unbundled with lattice72  have first := firstOf.selected with member73  have second := secondOf.selected with member74  unfold pairJoin75  exact join.member with unbundled, first.left, second.left7677defgraph inf (P : Set) (p ∈ points(P) × points(P)) : points(P) := pairMeet(P, p)78requires lattice : Lattice(P)79proof80  have unbundled := Lattice.unbundled with lattice81  have first := firstOf.selected with member82  have second := secondOf.selected with member83  unfold pairMeet84  exact meet.member with unbundled, first.left, second.left8586notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis Lattice(P) for P.points87notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis Lattice(P) for P.points88notation infix 50 "≤" => Le(P, _, _) via hypothesis Lattice(P) for P.points8990section LatticeOperations91variable (P : Set)92hypothesis lattice : Lattice(P)9394-- The bundled operations are the unbundled join and meet.95theorem sup.join (a b ∈ points(P))96  shows a ⊔ b = join(points(P), le(P), a, b)97proof98  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *99  have value := sup.value at P, (a, b) with lattice, pairIn100  have pair := pairJoin.pair at P, a, b with *101  unfold call2102  cc103104theorem inf.meet (a b ∈ points(P))105  shows a ⊓ b = meet(points(P), le(P), a, b)106proof107  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *108  have value := inf.value at P, (a, b) with lattice, pairIn109  have pair := pairMeet.pair at P, a, b with *110  unfold call2111  cc112113instance sup.member (a b ∈ points(P))114  shows a ⊔ b ∈ points(P)115proof116  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *117  have function := sup.function with lattice118  unfold call2119  exact FunctionBetween.apply_closed with function, pairIn120121instance inf.member (a b ∈ points(P))122  shows a ⊓ b ∈ points(P)123proof124  have pairIn : (a, b) ∈ points(P) × points(P) := product.pair with *125  have function := inf.function with lattice126  unfold call2127  exact FunctionBetween.apply_closed with function, pairIn128129-- The defining properties of join and meet.130theorem le_sup_left (a b ∈ points(P))131  shows a ≤ a ⊔ b132proof133  unfold Le134  rw sup.join135  exact join.upper_left with *136137theorem le_sup_right (a b ∈ points(P))138  shows b ≤ a ⊔ b139proof140  unfold Le141  rw sup.join142  exact join.upper_right with *143144theorem sup_le (a b c ∈ points(P))145  requires hac : a ≤ c146  requires hbc : b ≤ c147  shows a ⊔ b ≤ c148proof149  unfold Le150  rw sup.join151  exact join.least with *152153theorem inf_le_left (a b ∈ points(P))154  shows a ⊓ b ≤ a155proof156  unfold Le157  rw inf.meet158  exact meet.lower_left with *159160theorem inf_le_right (a b ∈ points(P))161  shows a ⊓ b ≤ b162proof163  unfold Le164  rw inf.meet165  exact meet.lower_right with *166167theorem le_inf (a b c ∈ points(P))168  requires hab : a ≤ b169  requires hac : a ≤ c170  shows a ≤ b ⊓ c171proof172  unfold Le173  rw inf.meet174  exact meet.greatest with *175176theorem sup.isLUB (a b ∈ points(P))177  shows IsLUB(P, {a, b}, a ⊔ b)178proof179  unfold IsLUB180  rw sup.join181  exact join.supremum with *182183theorem inf.isGLB (a b ∈ points(P))184  shows IsGLB(P, {a, b}, a ⊓ b)185proof186  unfold IsGLB187  rw inf.meet188  exact meet.infimum with *189190theorem sup.of_isLUB (s : Set) (a b ∈ points(P))191  requires lub : IsLUB(P, {a, b}, s)192  shows s = a ⊔ b193proof194  unfold IsLUB at lub195  rw sup.join196  exact join.of_supremum with *197198theorem inf.of_isGLB (i : Set) (a b ∈ points(P))199  requires glb : IsGLB(P, {a, b}, i)200  shows i = a ⊓ b201proof202  unfold IsGLB at glb203  rw inf.meet204  exact meet.of_infimum with *205206end LatticeOperations207208-- The equational laws of join and meet, and the order they determine.209section LatticeLaws210variable (P : Set)211hypothesis lattice : Lattice(P)212213theorem sup_comm (a b ∈ points(P))214  shows a ⊔ b = b ⊔ a215proof216  have first : a ⊔ b ≤ b ⊔ a := sup_le with (le_sup_right with *), (le_sup_left with *)217  have second : b ⊔ a ≤ a ⊔ b := sup_le with (le_sup_right with *), (le_sup_left with *)218  exact le_antisymm with *219220theorem inf_comm (a b ∈ points(P))221  shows a ⊓ b = b ⊓ a222proof223  have first : a ⊓ b ≤ b ⊓ a := le_inf with (inf_le_right with *), (inf_le_left with *)224  have second : b ⊓ a ≤ a ⊓ b := le_inf with (inf_le_right with *), (inf_le_left with *)225  exact le_antisymm with *226227theorem sup_idem (a ∈ points(P))228  shows a ⊔ a = a229proof230  rw sup.join231  exact join.idempotent with *232233theorem inf_idem (a ∈ points(P))234  shows a ⊓ a = a235proof236  rw inf.meet237  exact meet.idempotent with *238239theorem sup_eq_right (a b ∈ points(P))240  requires hab : a ≤ b241  shows a ⊔ b = b242proof243  rw sup.join244  exact join.of_le with *245246theorem sup_eq_left (a b ∈ points(P))247  requires hba : b ≤ a248  shows a ⊔ b = a249proof250  rw sup.join251  exact join.of_ge with *252253theorem inf_eq_left (a b ∈ points(P))254  requires hab : a ≤ b255  shows a ⊓ b = a256proof257  rw inf.meet258  exact meet.of_le with *259260theorem inf_eq_right (a b ∈ points(P))261  requires hba : b ≤ a262  shows a ⊓ b = b263proof264  rw inf.meet265  exact meet.of_ge with *266267theorem sup_eq_right_iff (a b ∈ points(P))268  shows a ≤ b ↔ a ⊔ b = b269proof270  constructor271  . intro hab272    exact sup_eq_right with *273  . intro same274    have upper : a ≤ a ⊔ b := le_sup_left with *275    rwa same at upper276277theorem inf_eq_left_iff (a b ∈ points(P))278  shows a ≤ b ↔ a ⊓ b = a279proof280  constructor281  . intro hab282    exact inf_eq_left with *283  . intro same284    have lower : a ⊓ b ≤ b := inf_le_right with *285    rwa same at lower286287theorem sup_assoc (a b c ∈ points(P))288  shows (a ⊔ b) ⊔ c = a ⊔ (b ⊔ c)289proof290  simp [sup.join]291  exact join.associative with *292293theorem inf_assoc (a b c ∈ points(P))294  shows (a ⊓ b) ⊓ c = a ⊓ (b ⊓ c)295proof296  simp [inf.meet]297  exact meet.associative with *298299theorem sup_left_comm (a b c ∈ points(P))300  shows a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)301proof302  simp [sup.join]303  exact join.left_commutative with *304305theorem inf_left_comm (a b c ∈ points(P))306  shows a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c)307proof308  simp [inf.meet]309  exact meet.left_commutative with *310311theorem sup_absorb (a b ∈ points(P))312  shows a ⊔ (a ⊓ b) = a313proof314  simp [sup.join, inf.meet]315  exact join.absorb with *316317theorem inf_absorb (a b ∈ points(P))318  shows a ⊓ (a ⊔ b) = a319proof320  simp [sup.join, inf.meet]321  exact meet.absorb with *322323theorem sup_le_iff (a b c ∈ points(P))324  shows a ⊔ b ≤ c ↔ (a ≤ c ∧ b ≤ c)325proof326  constructor327  . intro h328    have left : a ≤ a ⊔ b := le_sup_left with *329    have right : b ≤ a ⊔ b := le_sup_right with *330    constructor331    . exact le_trans with left, h332    . exact le_trans with right, h333  . intro both334    obtain ⟨hac, hbc⟩ := both335    exact sup_le with *336337theorem le_inf_iff (a b c ∈ points(P))338  shows a ≤ b ⊓ c ↔ (a ≤ b ∧ a ≤ c)339proof340  constructor341  . intro h342    have left : b ⊓ c ≤ b := inf_le_left with *343    have right : b ⊓ c ≤ c := inf_le_right with *344    constructor345    . exact le_trans with h, left346    . exact le_trans with h, right347  . intro both348    obtain ⟨hab, hac⟩ := both349    exact le_inf with *350351theorem sup_le_sup (a b c d ∈ points(P))352  requires hac : a ≤ c353  requires hbd : b ≤ d354  shows a ⊔ b ≤ c ⊔ d355proof356  unfold Le357  rw [sup.join, sup.join]358  exact join.monotone with *359360theorem inf_le_inf (a b c d ∈ points(P))361  requires hac : a ≤ c362  requires hbd : b ≤ d363  shows a ⊓ b ≤ c ⊓ d364proof365  unfold Le366  rw [inf.meet, inf.meet]367  exact meet.monotone with *368369theorem sup_le_sup_left (a b c ∈ points(P))370  requires hbc : b ≤ c371  shows a ⊔ b ≤ a ⊔ c372proof373  unfold Le374  rw [sup.join, sup.join]375  exact join.monotone_right with *376377theorem sup_le_sup_right (a b c ∈ points(P))378  requires hab : a ≤ b379  shows a ⊔ c ≤ b ⊔ c380proof381  unfold Le382  rw [sup.join, sup.join]383  exact join.monotone_left with *384385theorem inf_le_inf_left (a b c ∈ points(P))386  requires hbc : b ≤ c387  shows a ⊓ b ≤ a ⊓ c388proof389  unfold Le390  rw [inf.meet, inf.meet]391  exact meet.monotone_right with *392393theorem inf_le_inf_right (a b c ∈ points(P))394  requires hab : a ≤ b395  shows a ⊓ c ≤ b ⊓ c396proof397  unfold Le398  rw [inf.meet, inf.meet]399  exact meet.monotone_left with *400401theorem le_sup_of_le_left (a b c ∈ points(P))402  requires hab : a ≤ b403  shows a ≤ b ⊔ c404proof405  exact le_trans with hab, (le_sup_left with *)406407theorem le_sup_of_le_right (a b c ∈ points(P))408  requires hac : a ≤ c409  shows a ≤ b ⊔ c410proof411  exact le_trans with hac, (le_sup_right with *)412413theorem inf_le_of_left_le (a b c ∈ points(P))414  requires hac : a ≤ c415  shows a ⊓ b ≤ c416proof417  exact le_trans with (inf_le_left with *), hac418419theorem inf_le_of_right_le (a b c ∈ points(P))420  requires hbc : b ≤ c421  shows a ⊓ b ≤ c422proof423  exact le_trans with (inf_le_right with *), hbc424425theorem inf_le_sup (a b ∈ points(P))426  shows a ⊓ b ≤ a ⊔ b427proof428  unfold Le429  rw [inf.meet, sup.join]430  exact meet.le_join with *431432-- The distributive and modular inequalities, which hold in every lattice.433theorem sup_inf_le_inf_sup (a b c ∈ points(P))434  shows (a ⊓ b) ⊔ (a ⊓ c) ≤ a ⊓ (b ⊔ c)435proof436  unfold Le437  rw [inf.meet, inf.meet, sup.join, sup.join, inf.meet]438  exact meet.join_distributive_le with *439440theorem sup_inf_le_inf_sup_sup (a b c ∈ points(P))441  shows a ⊔ (b ⊓ c) ≤ (a ⊔ b) ⊓ (a ⊔ c)442proof443  unfold Le444  rw [inf.meet, sup.join, sup.join, sup.join, inf.meet]445  exact join.meet_distributive_ge with *446447theorem sup_inf_le_of_le (a b c ∈ points(P))448  requires hba : b ≤ a449  shows b ⊔ (a ⊓ c) ≤ a ⊓ (b ⊔ c)450proof451  unfold Le452  rw [inf.meet, sup.join, sup.join, inf.meet]453  exact join.modular_le with *454455end LatticeLaws456457-- The lattice rewrite set: idempotency, absorption, associativity, and the458-- bounds of a join and a meet, each applied where the memberships of its459-- elements are in scope.460tactic lattice_simp := simp [sup_idem, inf_idem, sup_absorb, inf_absorb, sup_assoc, inf_assoc, le_sup_left, le_sup_right, inf_le_left, inf_le_right, le_refl]461