Grace/Cumulus/Lattice/Order.g17

Open in Workbench Download source

Imports

Bounds

Declarations

• Order structure
• Preorder predicate
• PartialOrder predicate
• LinearOrder predicate
• Le predicate
• Le.relates theorem derivation
• Le.of_relates theorem derivation
• Le.iff theorem derivation
• Preorder.unbundled instance derivation
• PartialOrder.unbundled instance derivation
• LinearOrder.unbundled instance derivation
• Preorder.mk theorem derivation
• PartialOrder.mk theorem derivation
• LinearOrder.mk theorem derivation
• PartialOrder.preorder_of instance derivation
• LinearOrder.partial_order theorem derivation
• IsPreorder.relation theorem derivation
• le_refl theorem derivation
• le_trans theorem derivation
• le_antisymm theorem derivation
• le_antisymm_iff theorem derivation
• le_total theorem derivation
• upperBounds def
• lowerBounds def
• IsLUB predicate
• IsGLB predicate
• IsLeast predicate
• IsGreatest predicate
• upperBounds.of_upper_bound theorem derivation
• lowerBounds.of_lower_bound theorem derivation
• IsLUB.unique theorem derivation
• IsGLB.unique theorem derivation
• IsLUB.member theorem derivation
• IsGLB.member theorem derivation
• IsLUB.le_of_mem theorem derivation
• IsGLB.le_of_mem theorem derivation
• IsLUB.le_of_upper theorem derivation
• IsGLB.ge_of_lower theorem derivation
• IsGreatest.isLUB theorem derivation
• IsLeast.isGLB theorem derivation
• dual def
• dual.points theorem derivation
• dual.le theorem derivation
• PartialOrder.dual theorem derivation
• IsLUB.dual theorem derivation
• IsGLB.dual theorem derivation

Source

1-- Ordered sets bundled as one set, with the order written ≤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.Order8import Bounds910-- An ordered set is a structure of its points and its order relation,11-- Order.mk(A, r). The projections read the two back: P.points is the12-- underlying set and P.le the relation on it, so that every order structure13-- is a property of the one set P. The order structures below are separate14-- predicates over the same data, so Order carries no laws of its own.15structure Order16  | points le : Set1718-- The projection laws of a constructed order as one rewrite set.19tactic order_projections := simp [Order.mk.points, Order.mk.le]2021-- The order structures, as properties of the bundled set. Each is the22-- unbundled predicate at the projections, so a hypothesis Preorder(P)23-- opens to IsPreorder(points(P), le(P)).24predicate Preorder (P : Set) := IsPreorder(points(P), le(P))25predicate PartialOrder (P : Set) := IsPartialOrder(points(P), le(P))26predicate LinearOrder (P : Set) := IsLinearOrder(points(P), le(P))2728-- The order of P as a predicate of its own, written a ≤ b wherever a29-- hypothesis in scope supplies the ordered set; the operands' membership in30-- points(P) selects it when several are in scope. A fact a ≤ b opens to31-- relates(le(P), a, b) wherever local evidence is consulted.32predicate Le (P a b : Set) := relates(le(P), a, b)3334notation infix 50 "≤" => Le(P, _, _) via hypothesis Preorder(P) for P.points35notation infix 50 "≤" => Le(P, _, _) via hypothesis PartialOrder(P) for P.points36notation infix 50 "≤" => Le(P, _, _) via hypothesis LinearOrder(P) for P.points3738theorem Le.relates (P a b : Set)39  requires h : Le(P, a, b)40  shows relates(le(P), a, b)41proof42  simp [Le]4344theorem Le.of_relates (P a b : Set)45  requires h : relates(le(P), a, b)46  shows Le(P, a, b)47proof48  simp [Le]4950theorem Le.iff (P a b : Set)51  shows Le(P, a, b) ↔ relates(le(P), a, b)52proof53  simp [Le]5455-- Bridges to the unbundled predicates: a structure on (A, r) is one on56-- Order.mk(A, r), and the instances let `with *` read the unbundled form57-- off a bundled hypothesis.58instance Preorder.unbundled (P : Set)59  requires order : Preorder(P)60  shows IsPreorder(points(P), le(P))61proof62  simp [Preorder]6364instance PartialOrder.unbundled (P : Set)65  requires order : PartialOrder(P)66  shows IsPartialOrder(points(P), le(P))67proof68  simp [PartialOrder]6970instance LinearOrder.unbundled (P : Set)71  requires order : LinearOrder(P)72  shows IsLinearOrder(points(P), le(P))73proof74  simp [LinearOrder]7576theorem Preorder.mk (A r : Set)77  requires order : IsPreorder(A, r)78  shows Preorder(Order.mk(A, r))79proof80  unfold Preorder81  rw [Order.mk.points, Order.mk.le]82  exact order8384theorem PartialOrder.mk (A r : Set)85  requires order : IsPartialOrder(A, r)86  shows PartialOrder(Order.mk(A, r))87proof88  unfold PartialOrder89  rw [Order.mk.points, Order.mk.le]90  exact order9192theorem LinearOrder.mk (A r : Set)93  requires order : IsLinearOrder(A, r)94  shows LinearOrder(Order.mk(A, r))95proof96  unfold LinearOrder97  rw [Order.mk.points, Order.mk.le]98  exact order99100instance PartialOrder.preorder_of (P : Set)101  requires order : PartialOrder(P)102  shows Preorder(P)103proof104  unfold Preorder105  exact IsPartialOrder.preorder with (PartialOrder.unbundled with order)106107theorem LinearOrder.partial_order (P : Set)108  requires order : LinearOrder(P)109  shows PartialOrder(P)110proof111  unfold PartialOrder112  exact IsLinearOrder.partial with (LinearOrder.unbundled with order)113114-- The order relation lives on the points.115theorem IsPreorder.relation (P : Set)116  requires order : Preorder(P)117  shows RelationBetween(le(P), points(P), points(P))118proof119  obtain ⟨relation, rest⟩ := Preorder.unbundled with order120  exact relation121122section PreorderLaws123variable (P : Set)124hypothesis order : Preorder(P)125126theorem le_refl (a ∈ points(P))127  shows a ≤ a128proof129  obtain ⟨relation, reflexive, transitive⟩ := Preorder.unbundled with order130  unfold Le131  exact reflexive with a, assumption132133theorem le_trans (a b c ∈ points(P))134  requires hab : a ≤ b135  requires hbc : b ≤ c136  shows a ≤ c137proof138  obtain ⟨relation, reflexive, transitive⟩ := Preorder.unbundled with order139  unfold Le140  exact transitive with a, assumption, b, assumption, c, assumption, hab, hbc141142end PreorderLaws143144section PartialOrderLaws145variable (P : Set)146hypothesis order : PartialOrder(P)147148theorem le_antisymm (a b ∈ points(P))149  requires hab : a ≤ b150  requires hba : b ≤ a151  shows a = b152proof153  have antisymmetric := IsPartialOrder.antisymmetric with (PartialOrder.unbundled with order)154  exact antisymmetric with a, assumption, b, assumption, hab, hba155156theorem le_antisymm_iff (a b ∈ points(P))157  shows a = b ↔ (a ≤ b ∧ b ≤ a)158proof159  constructor160  . intro same161    rw same162    have reflexive : b ≤ b := le_refl with *163    exact ⟨reflexive, reflexive⟩164  . intro both165    obtain ⟨hab, hba⟩ := both166    exact le_antisymm with *167168end PartialOrderLaws169170section LinearOrderLaws171variable (P : Set)172hypothesis order : LinearOrder(P)173174theorem le_total (a b ∈ points(P))175  shows a ≤ b ∨ b ≤ a176proof177  obtain ⟨partial, total⟩ := LinearOrder.unbundled with order178  have both := total with a, assumption, b, assumption179  cases both with ab | ba180  . left181    exact Le.of_relates with ab182  . right183    exact Le.of_relates with ba184185end LinearOrderLaws186187-- Bounds of a subset of a bundled order.188def upperBounds (P S : Set) : Set := { b ∈ points(P) | ∀ x ∈ S, relates(le(P), x, b) }189def lowerBounds (P S : Set) : Set := { b ∈ points(P) | ∀ x ∈ S, relates(le(P), b, x) }190predicate IsLUB (P S s : Set) := Supremum(points(P), le(P), S, s)191predicate IsGLB (P S i : Set) := Infimum(points(P), le(P), S, i)192predicate IsLeast (P S a : Set) := Least(points(P), le(P), S, a)193predicate IsGreatest (P S a : Set) := Greatest(points(P), le(P), S, a)194195theorem upperBounds.of_upper_bound (P S b : Set)196  requires bound : UpperBound(points(P), le(P), S, b)197  shows b ∈ upperBounds(P, S)198proof199  obtain ⟨bIn, subset, above⟩ := bound200  apply upperBounds.membership.backward201  exact ⟨bIn, above⟩202203theorem lowerBounds.of_lower_bound (P S b : Set)204  requires bound : LowerBound(points(P), le(P), S, b)205  shows b ∈ lowerBounds(P, S)206proof207  obtain ⟨bIn, subset, below⟩ := bound208  apply lowerBounds.membership.backward209  exact ⟨bIn, below⟩210211section BoundLaws212variable (P : Set)213hypothesis order : PartialOrder(P)214215theorem IsLUB.unique (S s t : Set)216  requires first : IsLUB(P, S, s)217  requires second : IsLUB(P, S, t)218  shows s = t219proof220  unfold IsLUB at first221  unfold IsLUB at second222  exact Supremum.unique with *223224theorem IsGLB.unique (S i j : Set)225  requires first : IsGLB(P, S, i)226  requires second : IsGLB(P, S, j)227  shows i = j228proof229  unfold IsGLB at first230  unfold IsGLB at second231  exact Infimum.unique with *232233theorem IsLUB.member (S s : Set)234  requires lub : IsLUB(P, S, s)235  shows s ∈ points(P)236proof237  unfold IsLUB at lub238  exact Supremum.member with lub239240theorem IsGLB.member (S i : Set)241  requires glb : IsGLB(P, S, i)242  shows i ∈ points(P)243proof244  unfold IsGLB at glb245  exact Infimum.member with glb246247theorem IsLUB.le_of_mem (S s x : Set)248  requires lub : IsLUB(P, S, s)249  requires xIn : x ∈ S250  shows x ≤ s251proof252  unfold IsLUB at lub253  unfold Le254  exact Supremum.above with lub, xIn255256theorem IsGLB.le_of_mem (S i x : Set)257  requires glb : IsGLB(P, S, i)258  requires xIn : x ∈ S259  shows i ≤ x260proof261  unfold IsGLB at glb262  unfold Le263  exact Infimum.below with glb, xIn264265theorem IsLUB.le_of_upper (S s b : Set)266  requires lub : IsLUB(P, S, s)267  requires bound : b ∈ upperBounds(P, S)268  shows s ≤ b269proof270  obtain ⟨upper, least⟩ := lub271  obtain ⟨bIn, above⟩ := upperBounds.membership.forward with bound272  have subset := UpperBound.subset with upper273  unfold Le274  exact least with b, bIn, ⟨bIn, subset, above⟩275276theorem IsGLB.ge_of_lower (S i b : Set)277  requires glb : IsGLB(P, S, i)278  requires bound : b ∈ lowerBounds(P, S)279  shows b ≤ i280proof281  obtain ⟨lower, greatest⟩ := glb282  obtain ⟨bIn, below⟩ := lowerBounds.membership.forward with bound283  have subset := LowerBound.subset with lower284  unfold Le285  exact greatest with b, bIn, ⟨bIn, subset, below⟩286287theorem IsGreatest.isLUB (S a : Set)288  requires greatest : IsGreatest(P, S, a)289  shows IsLUB(P, S, a)290proof291  unfold IsGreatest at greatest292  unfold IsLUB293  exact Greatest.supremum with *294295theorem IsLeast.isGLB (S a : Set)296  requires least : IsLeast(P, S, a)297  shows IsGLB(P, S, a)298proof299  unfold IsLeast at least300  unfold IsGLB301  exact Least.infimum with *302303end BoundLaws304305-- The dual of a bundled order reverses the relation; suprema and infima306-- exchange.307def dual (P : Set) : Set := Order.mk(points(P), converse(le(P), points(P), points(P)))308309theorem dual.points (P : Set)310  shows points(dual(P)) = points(P)311proof312  simp [dual, Order.mk.points]313314theorem dual.le (P : Set)315  shows le(dual(P)) = converse(le(P), points(P), points(P))316proof317  simp [dual, Order.mk.le]318319theorem PartialOrder.dual (P : Set)320  requires order : PartialOrder(P)321  shows PartialOrder(dual(P))322proof323  unfold dual324  apply PartialOrder.mk325  exact IsPartialOrder.converse with (PartialOrder.unbundled with order)326327theorem IsLUB.dual (P S s : Set)328  requires order : PartialOrder(P)329  requires lub : IsLUB(P, S, s)330  shows IsGLB(dual(P), S, s)331proof332  unfold IsLUB at lub333  unfold IsGLB334  rw [dual.points, dual.le]335  exact Supremum.converse with *336337theorem IsGLB.dual (P S i : Set)338  requires order : PartialOrder(P)339  requires glb : IsGLB(P, S, i)340  shows IsLUB(dual(P), S, i)341proof342  unfold IsGLB at glb343  unfold IsLUB344  rw [dual.points, dual.le]345  exact Infimum.converse with *346