Grace/Cumulus/Lattice/Bounded.g17

Open in Workbench Download source

Imports

LatticeLaws

Declarations

Source

1-- Bounded lattices: least and greatest elements, and complementary pairs2-- 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.Bounded8import LatticeLaws910predicate IsBoundedLattice (A r bot top : Set) :=11  IsLattice(A, r) ∧ Least(A, r, A, bot) ∧ Greatest(A, r, A, top)1213-- Two elements are complementary when they meet at the bottom and join14-- at the top.15predicate Complementary (A r bot top x y : Set) :=16  y ∈ A ∧ meet(A, r, x, y) = bot ∧ join(A, r, x, y) = top1718theorem IsBoundedLattice.lattice (A r bot top : Set)19  requires h : IsBoundedLattice(A, r, bot, top)20  shows IsLattice(A, r)21proof22  simp [IsBoundedLattice]2324theorem IsBoundedLattice.least (A r bot top : Set)25  requires h : IsBoundedLattice(A, r, bot, top)26  shows Least(A, r, A, bot)27proof28  simp [IsBoundedLattice]2930theorem IsBoundedLattice.greatest (A r bot top : Set)31  requires h : IsBoundedLattice(A, r, bot, top)32  shows Greatest(A, r, A, top)33proof34  simp [IsBoundedLattice]3536theorem IsBoundedLattice.of_bounds (A r bot top : Set)37  requires lattice : IsLattice(A, r)38  requires least : Least(A, r, A, bot)39  requires greatest : Greatest(A, r, A, top)40  shows IsBoundedLattice(A, r, bot, top)41proof42  refine ⟨lattice, least, greatest⟩4344theorem IsBoundedLattice.bottom_member (A r bot top : Set)45  requires h : IsBoundedLattice(A, r, bot, top)46  shows bot ∈ A47proof48  exact Least.member with (IsBoundedLattice.least with h)4950theorem IsBoundedLattice.top_member (A r bot top : Set)51  requires h : IsBoundedLattice(A, r, bot, top)52  shows top ∈ A53proof54  exact Greatest.member with (IsBoundedLattice.greatest with h)5556theorem IsBoundedLattice.bottom_le (A r bot top x : Set)57  requires h : IsBoundedLattice(A, r, bot, top)58  requires hx : x ∈ A59  shows relates(r, bot, x)60proof61  exact Least.below with (IsBoundedLattice.least with h), hx6263theorem IsBoundedLattice.le_top (A r bot top x : Set)64  requires h : IsBoundedLattice(A, r, bot, top)65  requires hx : x ∈ A66  shows relates(r, x, top)67proof68  exact Greatest.above with (IsBoundedLattice.greatest with h), hx6970theorem IsBoundedLattice.nonempty (A r bot top : Set)71  requires h : IsBoundedLattice(A, r, bot, top)72  shows Nonempty(A)73proof74  refine ⟨bot, IsBoundedLattice.bottom_member with h⟩7576theorem IsBoundedLattice.bottom_unique (A r bot top c : Set)77  requires h : IsBoundedLattice(A, r, bot, top)78  requires hc : Least(A, r, A, c)79  shows c = bot80proof81  have order := IsLattice.order with (IsBoundedLattice.lattice with h)82  exact Least.unique with order, hc, (IsBoundedLattice.least with h)8384theorem IsBoundedLattice.top_unique (A r bot top c : Set)85  requires h : IsBoundedLattice(A, r, bot, top)86  requires hc : Greatest(A, r, A, c)87  shows c = top88proof89  have order := IsLattice.order with (IsBoundedLattice.lattice with h)90  exact Greatest.unique with order, hc, (IsBoundedLattice.greatest with h)9192theorem IsBoundedLattice.le_bottom_iff (A r bot top x : Set)93  requires h : IsBoundedLattice(A, r, bot, top)94  requires hx : x ∈ A95  shows relates(r, x, bot) ↔ x = bot96proof97  have lattice := IsBoundedLattice.lattice with h98  have antisymmetric := IsLattice.antisymmetric with lattice99  have reflexive := IsLattice.reflexive with lattice100  have botA := IsBoundedLattice.bottom_member with h101  constructor102  . intro below103    have above := IsBoundedLattice.bottom_le with h, hx104    exact antisymmetric with x, hx, bot, botA, below, above105  . intro equal106    rw equal107    exact reflexive with bot, botA108109theorem IsBoundedLattice.top_le_iff (A r bot top x : Set)110  requires h : IsBoundedLattice(A, r, bot, top)111  requires hx : x ∈ A112  shows relates(r, top, x) ↔ x = top113proof114  have lattice := IsBoundedLattice.lattice with h115  have antisymmetric := IsLattice.antisymmetric with lattice116  have reflexive := IsLattice.reflexive with lattice117  have topA := IsBoundedLattice.top_member with h118  constructor119  . intro above120    have below := IsBoundedLattice.le_top with h, hx121    exact antisymmetric with x, hx, top, topA, below, above122  . intro equal123    rw equal124    exact reflexive with top, topA125126-- The bottom and top as units and absorbing elements127128theorem join.bottom_right (A r bot top x : Set)129  requires h : IsBoundedLattice(A, r, bot, top)130  requires hx : x ∈ A131  shows join(A, r, x, bot) = x132proof133  have lattice := IsBoundedLattice.lattice with h134  have botA := IsBoundedLattice.bottom_member with h135  exact join.of_ge with lattice, hx, botA,136    (IsBoundedLattice.bottom_le with h, hx)137138theorem join.bottom_left (A r bot top x : Set)139  requires h : IsBoundedLattice(A, r, bot, top)140  requires hx : x ∈ A141  shows join(A, r, bot, x) = x142proof143  have lattice := IsBoundedLattice.lattice with h144  have botA := IsBoundedLattice.bottom_member with h145  exact join.of_le with lattice, botA, hx,146    (IsBoundedLattice.bottom_le with h, hx)147148theorem meet.bottom_right (A r bot top x : Set)149  requires h : IsBoundedLattice(A, r, bot, top)150  requires hx : x ∈ A151  shows meet(A, r, x, bot) = bot152proof153  have lattice := IsBoundedLattice.lattice with h154  have botA := IsBoundedLattice.bottom_member with h155  exact meet.of_ge with lattice, hx, botA,156    (IsBoundedLattice.bottom_le with h, hx)157158theorem meet.bottom_left (A r bot top x : Set)159  requires h : IsBoundedLattice(A, r, bot, top)160  requires hx : x ∈ A161  shows meet(A, r, bot, x) = bot162proof163  have lattice := IsBoundedLattice.lattice with h164  have botA := IsBoundedLattice.bottom_member with h165  exact meet.of_le with lattice, botA, hx,166    (IsBoundedLattice.bottom_le with h, hx)167168theorem join.top_right (A r bot top x : Set)169  requires h : IsBoundedLattice(A, r, bot, top)170  requires hx : x ∈ A171  shows join(A, r, x, top) = top172proof173  have lattice := IsBoundedLattice.lattice with h174  have topA := IsBoundedLattice.top_member with h175  exact join.of_le with lattice, hx, topA, (IsBoundedLattice.le_top with h, hx)176177theorem join.top_left (A r bot top x : Set)178  requires h : IsBoundedLattice(A, r, bot, top)179  requires hx : x ∈ A180  shows join(A, r, top, x) = top181proof182  have lattice := IsBoundedLattice.lattice with h183  have topA := IsBoundedLattice.top_member with h184  exact join.of_ge with lattice, topA, hx, (IsBoundedLattice.le_top with h, hx)185186theorem meet.top_right (A r bot top x : Set)187  requires h : IsBoundedLattice(A, r, bot, top)188  requires hx : x ∈ A189  shows meet(A, r, x, top) = x190proof191  have lattice := IsBoundedLattice.lattice with h192  have topA := IsBoundedLattice.top_member with h193  exact meet.of_le with lattice, hx, topA, (IsBoundedLattice.le_top with h, hx)194195theorem meet.top_left (A r bot top x : Set)196  requires h : IsBoundedLattice(A, r, bot, top)197  requires hx : x ∈ A198  shows meet(A, r, top, x) = x199proof200  have lattice := IsBoundedLattice.lattice with h201  have topA := IsBoundedLattice.top_member with h202  exact meet.of_ge with lattice, topA, hx, (IsBoundedLattice.le_top with h, hx)203204theorem join.eq_bottom_iff (A r bot top x y : Set)205  requires h : IsBoundedLattice(A, r, bot, top)206  requires hx : x ∈ A207  requires hy : y ∈ A208  shows join(A, r, x, y) = bot ↔ x = bot ∧ y = bot209proof210  have lattice := IsBoundedLattice.lattice with h211  constructor212  . intro equal213    have xJ := join.upper_left with lattice, hx, hy214    have yJ := join.upper_right with lattice, hx, hy215    rw equal at xJ216    rw equal at yJ217    constructor218    . exact IsBoundedLattice.le_bottom_iff.forward with h, hx, xJ219    . exact IsBoundedLattice.le_bottom_iff.forward with h, hy, yJ220  . intro both221    rw [both.left, both.right]222    exact join.idempotent with lattice, (IsBoundedLattice.bottom_member with h)223224theorem meet.eq_top_iff (A r bot top x y : Set)225  requires h : IsBoundedLattice(A, r, bot, top)226  requires hx : x ∈ A227  requires hy : y ∈ A228  shows meet(A, r, x, y) = top ↔ x = top ∧ y = top229proof230  have lattice := IsBoundedLattice.lattice with h231  constructor232  . intro equal233    have mX := meet.lower_left with lattice, hx, hy234    have mY := meet.lower_right with lattice, hx, hy235    rw equal at mX236    rw equal at mY237    constructor238    . exact IsBoundedLattice.top_le_iff.forward with h, hx, mX239    . exact IsBoundedLattice.top_le_iff.forward with h, hy, mY240  . intro both241    rw [both.left, both.right]242    exact meet.idempotent with lattice, (IsBoundedLattice.top_member with h)243244-- The bounds as suprema and infima245246theorem IsBoundedLattice.supremum_empty (A r bot top : Set)247  requires h : IsBoundedLattice(A, r, bot, top)248  shows Supremum(A, r, ∅, bot)249proof250  exact Supremum.empty_iff.backward with (IsBoundedLattice.least with h)251252theorem IsBoundedLattice.infimum_empty (A r bot top : Set)253  requires h : IsBoundedLattice(A, r, bot, top)254  shows Infimum(A, r, ∅, top)255proof256  exact Infimum.empty_iff.backward with (IsBoundedLattice.greatest with h)257258theorem IsBoundedLattice.supremum_whole (A r bot top : Set)259  requires h : IsBoundedLattice(A, r, bot, top)260  shows Supremum(A, r, A, top)261proof262  exact Supremum.whole_iff.backward with (IsBoundedLattice.greatest with h)263264theorem IsBoundedLattice.infimum_whole (A r bot top : Set)265  requires h : IsBoundedLattice(A, r, bot, top)266  shows Infimum(A, r, A, bot)267proof268  exact Infimum.whole_iff.backward with (IsBoundedLattice.least with h)269270theorem IsBoundedLattice.converse (A r bot top : Set)271  requires h : IsBoundedLattice(A, r, bot, top)272  shows IsBoundedLattice(A, converse(r, A, A), top, bot)273proof274  have lattice := IsBoundedLattice.lattice with h275  refine ⟨IsLattice.converse with lattice,276    Greatest.converse with (IsBoundedLattice.greatest with h),277    Least.converse with (IsBoundedLattice.least with h)⟩278279-- Complementary pairs280281theorem Complementary.member (A r bot top x y : Set)282  requires h : Complementary(A, r, bot, top, x, y)283  shows y ∈ A284proof285  simp [Complementary]286287theorem Complementary.meet (A r bot top x y : Set)288  requires h : Complementary(A, r, bot, top, x, y)289  shows meet(A, r, x, y) = bot290proof291  rcases h with ⟨member, meetEq, joinEq⟩292  exact meetEq293294theorem Complementary.join (A r bot top x y : Set)295  requires h : Complementary(A, r, bot, top, x, y)296  shows join(A, r, x, y) = top297proof298  rcases h with ⟨member, meetEq, joinEq⟩299  exact joinEq300301theorem Complementary.symmetric (A r bot top x y : Set)302  requires bounded : IsBoundedLattice(A, r, bot, top)303  requires hx : x ∈ A304  requires h : Complementary(A, r, bot, top, x, y)305  shows Complementary(A, r, bot, top, y, x)306proof307  have lattice := IsBoundedLattice.lattice with bounded308  have hy := Complementary.member with h309  have meetSwap := meet.commutative with lattice, hy, hx310  have joinSwap := join.commutative with lattice, hy, hx311  refine ⟨hx, ?_, ?_⟩312  . rw meetSwap313    exact Complementary.meet with h314  . rw joinSwap315    exact Complementary.join with h316317theorem Complementary.bottom_top (A r bot top : Set)318  requires bounded : IsBoundedLattice(A, r, bot, top)319  shows Complementary(A, r, bot, top, bot, top)320proof321  have botA := IsBoundedLattice.bottom_member with bounded322  have topA := IsBoundedLattice.top_member with bounded323  refine ⟨topA, (meet.bottom_left with bounded, topA),324      (join.top_right with bounded, botA)⟩325326theorem Complementary.top_bottom (A r bot top : Set)327  requires bounded : IsBoundedLattice(A, r, bot, top)328  shows Complementary(A, r, bot, top, top, bot)329proof330  have botA := IsBoundedLattice.bottom_member with bounded331  have topA := IsBoundedLattice.top_member with bounded332  refine ⟨botA, (meet.bottom_right with bounded, topA),333      (join.top_left with bounded, botA)⟩334335theorem Complementary.converse (A r bot top x y : Set)336  requires bounded : IsBoundedLattice(A, r, bot, top)337  requires hx : x ∈ A338  requires h : Complementary(A, r, bot, top, x, y)339  shows Complementary(A, converse(r, A, A), top, bot, x, y)340proof341  have lattice := IsBoundedLattice.lattice with bounded342  have hy := Complementary.member with h343  have joinDual := join.converse with lattice, hx, hy344  have meetDual := meet.converse with lattice, hx, hy345  refine ⟨hy, ?_, ?_⟩346  . rw meetDual347    exact Complementary.join with h348  . rw joinDual349    exact Complementary.meet with h350