Grace/Cumulus/Lattice/BoundedOrder.g17

Open in Workbench Download source

Imports

Bounded · Join

Declarations

Source

1-- Bounded lattices bundled as ordered sets, with bot(P) and top(P)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.BoundedOrder8import Bounded9import Join1011-- A bounded lattice is a lattice with a least and a greatest element; the12-- elements are determined by the order and read back as bot(P) and top(P).13predicate BoundedLattice (P : Set) :=14  Lattice(P) ∧ (∃ b, Least(points(P), le(P), points(P), b)) ∧15  (∃ t, Greatest(points(P), le(P), points(P), t))1617notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis BoundedLattice(P) for P.points18notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis BoundedLattice(P) for P.points19notation infix 50 "≤" => Le(P, _, _) via hypothesis BoundedLattice(P) for P.points2021instance BoundedLattice.lattice_of (P : Set)22  requires bounded : BoundedLattice(P)23  shows Lattice(P)24proof25  simp [BoundedLattice]2627theorem BoundedLattice.exists_least (P : Set)28  requires bounded : BoundedLattice(P)29  shows ∃ b, Least(points(P), le(P), points(P), b)30proof31  obtain ⟨lattice, least, greatest⟩ := bounded32  exact least3334theorem BoundedLattice.exists_greatest (P : Set)35  requires bounded : BoundedLattice(P)36  shows ∃ t, Greatest(points(P), le(P), points(P), t)37proof38  obtain ⟨lattice, least, greatest⟩ := bounded39  exact greatest4041defunique bot (P : Set) (b ∈ points(P)) := Least(points(P), le(P), points(P), b)42requires bounded : BoundedLattice(P)43proof44  obtain ⟨b, least⟩ := BoundedLattice.exists_least with bounded45  witness b46  refine ⟨Least.member with least, least⟩47uniqueness48  intros b bIn first c cIn second49  have order := IsLattice.order with (Lattice.unbundled with (BoundedLattice.lattice_of with bounded))50  exact Least.unique with order, first, second5152defunique top (P : Set) (t ∈ points(P)) := Greatest(points(P), le(P), points(P), t)53requires bounded : BoundedLattice(P)54proof55  obtain ⟨t, greatest⟩ := BoundedLattice.exists_greatest with bounded56  witness t57  refine ⟨Greatest.member with greatest, greatest⟩58uniqueness59  intros t tIn first u uIn second60  have order := IsLattice.order with (Lattice.unbundled with (BoundedLattice.lattice_of with bounded))61  exact Greatest.unique with order, first, second6263-- Bridges to the unbundled form IsBoundedLattice(A, r, bot, top).64instance BoundedLattice.unbundled (P : Set)65  requires bounded : BoundedLattice(P)66  shows IsBoundedLattice(points(P), le(P), bot(P), top(P))67proof68  have lattice := Lattice.unbundled with (BoundedLattice.lattice_of with bounded)69  have least := bot.selected with bounded70  have greatest := top.selected with bounded71  exact IsBoundedLattice.of_bounds with lattice, least.right, greatest.right7273theorem BoundedLattice.mk (A r b t : Set)74  requires bounded : IsBoundedLattice(A, r, b, t)75  shows BoundedLattice(Order.mk(A, r))76proof77  have lattice := Lattice.mk with (IsBoundedLattice.lattice with bounded)78  have least := IsBoundedLattice.least with bounded79  have greatest := IsBoundedLattice.greatest with bounded80  unfold BoundedLattice81  refine ⟨lattice, ?_, ?_⟩82  . witness b83    rw [Order.mk.points, Order.mk.le]84    exact least85  . witness t86    rw [Order.mk.points, Order.mk.le]87    exact greatest8889theorem bot.mk (A r b t : Set)90  requires bounded : IsBoundedLattice(A, r, b, t)91  shows bot(Order.mk(A, r)) = b92proof93  have bundled := BoundedLattice.mk with bounded94  have selected := bot.selected with bundled95  have least := IsBoundedLattice.least with bounded96  have order := IsLattice.order with (IsBoundedLattice.lattice with bounded)97  rw [Order.mk.points, Order.mk.le] at selected98  exact Least.unique with order, selected.right, least99100theorem top.mk (A r b t : Set)101  requires bounded : IsBoundedLattice(A, r, b, t)102  shows top(Order.mk(A, r)) = t103proof104  have bundled := BoundedLattice.mk with bounded105  have selected := top.selected with bundled106  have greatest := IsBoundedLattice.greatest with bounded107  have order := IsLattice.order with (IsBoundedLattice.lattice with bounded)108  rw [Order.mk.points, Order.mk.le] at selected109  exact Greatest.unique with order, selected.right, greatest110111-- Two elements are complementary when they meet at the bottom and join at112-- the top; under a hypothesis the conjuncts read a ⊓ b = bot(P) and113-- a ⊔ b = top(P).114predicate IsCompl (P a b : Set) :=115  b ∈ points(P) ∧ call2(inf(P), a, b) = bot(P) ∧ call2(sup(P), a, b) = top(P)116117-- The bounds are written ⊥ and ⊤ wherever a hypothesis in scope supplies118-- the bounded lattice; both lie in points(P).119notation constant "⊥" => bot(P) via hypothesis BoundedLattice(P) for P.points120notation constant "⊤" => top(P) via hypothesis BoundedLattice(P) for P.points121122section BoundedLatticeLaws123variable (P : Set)124hypothesis bounded : BoundedLattice(P)125126instance bot.member127  shows bot(P) ∈ points(P)128proof129  have selected := bot.selected with bounded130  exact selected.left131132instance top.member133  shows top(P) ∈ points(P)134proof135  have selected := top.selected with bounded136  exact selected.left137138theorem bot.isLeast139  shows IsLeast(P, points(P), bot(P))140proof141  unfold IsLeast142  have selected := bot.selected with bounded143  exact selected.right144145theorem top.isGreatest146  shows IsGreatest(P, points(P), top(P))147proof148  unfold IsGreatest149  have selected := top.selected with bounded150  exact selected.right151152theorem bot_le (a ∈ points(P))153  shows ⊥ ≤ a154proof155  unfold Le156  exact IsBoundedLattice.bottom_le with (BoundedLattice.unbundled with bounded),157    *158159theorem le_top (a ∈ points(P))160  shows a ≤ ⊤161proof162  unfold Le163  exact IsBoundedLattice.le_top with (BoundedLattice.unbundled with bounded), *164165theorem bot_unique (b : Set)166  requires least : IsLeast(P, points(P), b)167  shows b = bot(P)168proof169  unfold IsLeast at least170  exact IsBoundedLattice.bottom_unique with (BoundedLattice.unbundled with bounded), *171172theorem top_unique (t : Set)173  requires greatest : IsGreatest(P, points(P), t)174  shows t = top(P)175proof176  unfold IsGreatest at greatest177  exact IsBoundedLattice.top_unique with (BoundedLattice.unbundled with bounded), *178179theorem le_bot_iff (a ∈ points(P))180  shows a ≤ bot(P) ↔ a = bot(P)181proof182  have characterization := IsBoundedLattice.le_bottom_iff with (BoundedLattice.unbundled with bounded), *183  constructor184  . intro h185    exact characterization.forward with (Le.relates with h)186  . intro h187    exact Le.of_relates with (characterization.backward with h)188189theorem top_le_iff (a ∈ points(P))190  shows top(P) ≤ a ↔ a = top(P)191proof192  have characterization := IsBoundedLattice.top_le_iff with (BoundedLattice.unbundled with bounded), *193  constructor194  . intro h195    exact characterization.forward with (Le.relates with h)196  . intro h197    exact Le.of_relates with (characterization.backward with h)198199theorem sup_bot_eq (a ∈ points(P))200  shows a ⊔ bot(P) = a201proof202  rw sup.join203  exact join.bottom_right with (BoundedLattice.unbundled with bounded), *204205theorem bot_sup_eq (a ∈ points(P))206  shows bot(P) ⊔ a = a207proof208  rw sup.join209  exact join.bottom_left with (BoundedLattice.unbundled with bounded), *210211theorem inf_bot_eq (a ∈ points(P))212  shows a ⊓ bot(P) = bot(P)213proof214  rw inf.meet215  exact meet.bottom_right with (BoundedLattice.unbundled with bounded), *216217theorem bot_inf_eq (a ∈ points(P))218  shows bot(P) ⊓ a = bot(P)219proof220  rw inf.meet221  exact meet.bottom_left with (BoundedLattice.unbundled with bounded), *222223theorem sup_top_eq (a ∈ points(P))224  shows a ⊔ top(P) = top(P)225proof226  rw sup.join227  exact join.top_right with (BoundedLattice.unbundled with bounded), *228229theorem top_sup_eq (a ∈ points(P))230  shows top(P) ⊔ a = top(P)231proof232  rw sup.join233  exact join.top_left with (BoundedLattice.unbundled with bounded), *234235theorem inf_top_eq (a ∈ points(P))236  shows a ⊓ top(P) = a237proof238  rw inf.meet239  exact meet.top_right with (BoundedLattice.unbundled with bounded), *240241theorem top_inf_eq (a ∈ points(P))242  shows top(P) ⊓ a = a243proof244  rw inf.meet245  exact meet.top_left with (BoundedLattice.unbundled with bounded), *246247theorem sup_eq_bot_iff (a b ∈ points(P))248  shows a ⊔ b = bot(P) ↔ (a = bot(P) ∧ b = bot(P))249proof250  rw sup.join251  exact join.eq_bottom_iff with (BoundedLattice.unbundled with bounded), *252253theorem inf_eq_top_iff (a b ∈ points(P))254  shows a ⊓ b = top(P) ↔ (a = top(P) ∧ b = top(P))255proof256  rw inf.meet257  exact meet.eq_top_iff with (BoundedLattice.unbundled with bounded), *258259theorem bot.isLUB_empty260  shows IsLUB(P, ∅, bot(P))261proof262  unfold IsLUB263  exact IsBoundedLattice.supremum_empty with (BoundedLattice.unbundled with bounded), *264265theorem top.isGLB_empty266  shows IsGLB(P, ∅, top(P))267proof268  unfold IsGLB269  exact IsBoundedLattice.infimum_empty with (BoundedLattice.unbundled with bounded), *270271theorem BoundedLattice.nonempty_points272  shows Nonempty(points(P))273proof274  exact IsBoundedLattice.nonempty with (BoundedLattice.unbundled with bounded),275    *276277theorem IsCompl.member (a b : Set)278  requires compl : IsCompl(P, a, b)279  shows b ∈ points(P)280proof281  obtain ⟨bIn, meetEq, joinEq⟩ := compl282  exact bIn283284theorem IsCompl.inf_eq_bot (a b : Set)285  requires compl : IsCompl(P, a, b)286  shows a ⊓ b = bot(P)287proof288  obtain ⟨bIn, meetEq, joinEq⟩ := compl289  exact meetEq290291theorem IsCompl.sup_eq_top (a b : Set)292  requires compl : IsCompl(P, a, b)293  shows a ⊔ b = top(P)294proof295  obtain ⟨bIn, meetEq, joinEq⟩ := compl296  exact joinEq297298theorem IsCompl.unbundled (b : Set) (a ∈ points(P))299  requires compl : IsCompl(P, a, b)300  shows Complementary(points(P), le(P), bot(P), top(P), a, b)301proof302  obtain ⟨bIn, meetEq, joinEq⟩ := compl303  have meetBridge := inf.meet at P, a, b with *304  have joinBridge := sup.join at P, a, b with *305  unfold Complementary306  rw [← meetBridge, ← joinBridge]307  exact ⟨bIn, meetEq, joinEq⟩308309theorem IsCompl.of_complementary (b : Set) (a ∈ points(P))310  requires compl : Complementary(points(P), le(P), bot(P), top(P), a, b)311  shows IsCompl(P, a, b)312proof313  obtain ⟨bIn, meetEq, joinEq⟩ := compl314  have meetBridge := inf.meet at P, a, b with *315  have joinBridge := sup.join at P, a, b with *316  unfold IsCompl317  rw [meetBridge, joinBridge]318  exact ⟨bIn, meetEq, joinEq⟩319320theorem IsCompl.symm (b : Set) (a ∈ points(P))321  requires compl : IsCompl(P, a, b)322  shows IsCompl(P, b, a)323proof324  obtain ⟨bIn, meetEq, joinEq⟩ := compl325  have meetComm : b ⊓ a = a ⊓ b := inf_comm with *326  have supComm : b ⊔ a = a ⊔ b := sup_comm with *327  unfold IsCompl328  rw [meetComm, supComm]329  constructor330  . assumption331  . exact ⟨meetEq, joinEq⟩332333theorem IsCompl.bot_top334  shows IsCompl(P, bot(P), top(P))335proof336  have topIn : top(P) ∈ points(P) := top.member with *337  have meetEq : bot(P) ⊓ top(P) = bot(P) := inf_top_eq with *338  have joinEq : bot(P) ⊔ top(P) = top(P) := bot_sup_eq with *339  exact ⟨topIn, meetEq, joinEq⟩340341end BoundedLatticeLaws342343-- The bounded-lattice rewrite set.344tactic bounded_simp := simp [sup_bot_eq, bot_sup_eq, inf_bot_eq, bot_inf_eq, sup_top_eq, top_sup_eq, inf_top_eq, top_inf_eq, bot_le, le_top]345