Grace/Cumulus/Lattice/LatticeLaws.g17

Open in Workbench Download source

Imports

Lattice

Declarations

Source

1-- The equational laws of join and meet, and the order they determine2-- 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.LatticeLaws8import Lattice910-- Commutativity and idempotency1112theorem join.commutative (A r x y : Set)13  requires lattice : IsLattice(A, r)14  requires hx : x ∈ A15  requires hy : y ∈ A16  shows join(A, r, x, y) = join(A, r, y, x)17proof18  have supremum := join.supremum with lattice, hx, hy19  have swap := pair.commutative at x, y20  rw swap at supremum21  exact join.of_supremum with lattice, hy, hx, supremum2223theorem meet.commutative (A r x y : Set)24  requires lattice : IsLattice(A, r)25  requires hx : x ∈ A26  requires hy : y ∈ A27  shows meet(A, r, x, y) = meet(A, r, y, x)28proof29  have infimum := meet.infimum with lattice, hx, hy30  have swap := pair.commutative at x, y31  rw swap at infimum32  exact meet.of_infimum with lattice, hy, hx, infimum3334theorem join.idempotent (A r x : Set)35  requires lattice : IsLattice(A, r)36  requires hx : x ∈ A37  shows join(A, r, x, x) = x38proof39  have order := IsLattice.order with lattice40  have supremum := Supremum.singleton with order, hx41  have same := pair.self at x42  rw ← same at supremum43  symm44  exact join.of_supremum with lattice, hx, hx, supremum4546theorem meet.idempotent (A r x : Set)47  requires lattice : IsLattice(A, r)48  requires hx : x ∈ A49  shows meet(A, r, x, x) = x50proof51  have order := IsLattice.order with lattice52  have infimum := Infimum.singleton with order, hx53  have same := pair.self at x54  rw ← same at infimum55  symm56  exact meet.of_infimum with lattice, hx, hx, infimum5758-- The order is recovered from either operation.5960theorem join.of_le (A r x y : Set)61  requires lattice : IsLattice(A, r)62  requires hx : x ∈ A63  requires hy : y ∈ A64  requires hxy : relates(r, x, y)65  shows join(A, r, x, y) = y66proof67  have reflexive := IsLattice.reflexive with lattice68  have supremum : Supremum(A, r, {x, y}, y)69    apply Supremum.of_pair with hx, hy, hy, hxy, (reflexive with y, hy)70    intros b hb xb yb71    exact yb72  symm73  exact join.of_supremum with lattice, hx, hy, supremum7475theorem join.of_ge (A r x y : Set)76  requires lattice : IsLattice(A, r)77  requires hx : x ∈ A78  requires hy : y ∈ A79  requires hyx : relates(r, y, x)80  shows join(A, r, x, y) = x81proof82  have swap := join.commutative with lattice, hx, hy83  rw swap84  exact join.of_le with lattice, hy, hx, hyx8586theorem meet.of_le (A r x y : Set)87  requires lattice : IsLattice(A, r)88  requires hx : x ∈ A89  requires hy : y ∈ A90  requires hxy : relates(r, x, y)91  shows meet(A, r, x, y) = x92proof93  have reflexive := IsLattice.reflexive with lattice94  have infimum : Infimum(A, r, {x, y}, x)95    apply Infimum.of_pair with hx, hy, hx, (reflexive with x, hx), hxy96    intros b hb bx by_97    exact bx98  symm99  exact meet.of_infimum with lattice, hx, hy, infimum100101theorem meet.of_ge (A r x y : Set)102  requires lattice : IsLattice(A, r)103  requires hx : x ∈ A104  requires hy : y ∈ A105  requires hyx : relates(r, y, x)106  shows meet(A, r, x, y) = y107proof108  have swap := meet.commutative with lattice, hx, hy109  rw swap110  exact meet.of_le with lattice, hy, hx, hyx111112theorem join.eq_right_iff (A r x y : Set)113  requires lattice : IsLattice(A, r)114  requires hx : x ∈ A115  requires hy : y ∈ A116  shows relates(r, x, y) ↔ join(A, r, x, y) = y117proof118  constructor119  . intro hxy120    exact join.of_le with lattice, hx, hy, hxy121  . intro equal122    have upper := join.upper_left with lattice, hx, hy123    rw equal at upper124    exact upper125126theorem join.eq_left_iff (A r x y : Set)127  requires lattice : IsLattice(A, r)128  requires hx : x ∈ A129  requires hy : y ∈ A130  shows relates(r, y, x) ↔ join(A, r, x, y) = x131proof132  constructor133  . intro hyx134    exact join.of_ge with lattice, hx, hy, hyx135  . intro equal136    have upper := join.upper_right with lattice, hx, hy137    rw equal at upper138    exact upper139140theorem meet.eq_left_iff (A r x y : Set)141  requires lattice : IsLattice(A, r)142  requires hx : x ∈ A143  requires hy : y ∈ A144  shows relates(r, x, y) ↔ meet(A, r, x, y) = x145proof146  constructor147  . intro hxy148    exact meet.of_le with lattice, hx, hy, hxy149  . intro equal150    have lower := meet.lower_right with lattice, hx, hy151    rw equal at lower152    exact lower153154theorem meet.eq_right_iff (A r x y : Set)155  requires lattice : IsLattice(A, r)156  requires hx : x ∈ A157  requires hy : y ∈ A158  shows relates(r, y, x) ↔ meet(A, r, x, y) = y159proof160  constructor161  . intro hyx162    exact meet.of_ge with lattice, hx, hy, hyx163  . intro equal164    have lower := meet.lower_left with lattice, hx, hy165    rw equal at lower166    exact lower167168-- Absorption169170theorem join.absorb (A r x y : Set)171  requires lattice : IsLattice(A, r)172  requires hx : x ∈ A173  requires hy : y ∈ A174  shows join(A, r, x, meet(A, r, x, y)) = x175proof176  have meetA := meet.member with lattice, hx, hy177  have lower := meet.lower_left with lattice, hx, hy178  exact join.of_ge with lattice, hx, meetA, lower179180theorem join.absorb_swap (A r x y : Set)181  requires lattice : IsLattice(A, r)182  requires hx : x ∈ A183  requires hy : y ∈ A184  shows join(A, r, x, meet(A, r, y, x)) = x185proof186  have meetA := meet.member with lattice, hy, hx187  have lower := meet.lower_right with lattice, hy, hx188  exact join.of_ge with lattice, hx, meetA, lower189190theorem meet.absorb (A r x y : Set)191  requires lattice : IsLattice(A, r)192  requires hx : x ∈ A193  requires hy : y ∈ A194  shows meet(A, r, x, join(A, r, x, y)) = x195proof196  have joinA := join.member with lattice, hx, hy197  have upper := join.upper_left with lattice, hx, hy198  exact meet.of_le with lattice, hx, joinA, upper199200theorem meet.absorb_swap (A r x y : Set)201  requires lattice : IsLattice(A, r)202  requires hx : x ∈ A203  requires hy : y ∈ A204  shows meet(A, r, x, join(A, r, y, x)) = x205proof206  have joinA := join.member with lattice, hy, hx207  have upper := join.upper_right with lattice, hy, hx208  exact meet.of_le with lattice, hx, joinA, upper209210-- Bounds through join and meet211212theorem join.le_iff (A r x y b : Set)213  requires lattice : IsLattice(A, r)214  requires hx : x ∈ A215  requires hy : y ∈ A216  requires hb : b ∈ A217  shows relates(r, join(A, r, x, y), b) ↔ relates(r, x, b) ∧ relates(r, y, b)218proof219  have transitive := IsLattice.transitive with lattice220  have joinA := join.member with lattice, hx, hy221  constructor222  . intro below223    have xJ := join.upper_left with lattice, hx, hy224    have yJ := join.upper_right with lattice, hx, hy225    constructor226    . exact transitive with x, hx, join(A, r, x, y), joinA, b, hb, xJ, below227    . exact transitive with y, hy, join(A, r, x, y), joinA, b, hb, yJ, below228  . intro both229    exact join.least with lattice, hx, hy, hb, both.left, both.right230231theorem meet.ge_iff (A r x y b : Set)232  requires lattice : IsLattice(A, r)233  requires hx : x ∈ A234  requires hy : y ∈ A235  requires hb : b ∈ A236  shows relates(r, b, meet(A, r, x, y)) ↔ relates(r, b, x) ∧ relates(r, b, y)237proof238  have transitive := IsLattice.transitive with lattice239  have meetA := meet.member with lattice, hx, hy240  constructor241  . intro above242    have mX := meet.lower_left with lattice, hx, hy243    have mY := meet.lower_right with lattice, hx, hy244    constructor245    . exact transitive with b, hb, meet(A, r, x, y), meetA, x, hx, above, mX246    . exact transitive with b, hb, meet(A, r, x, y), meetA, y, hy, above, mY247  . intro both248    exact meet.greatest with lattice, hx, hy, hb, both.left, both.right249250theorem meet.le_join (A r x y : Set)251  requires lattice : IsLattice(A, r)252  requires hx : x ∈ A253  requires hy : y ∈ A254  shows relates(r, meet(A, r, x, y), join(A, r, x, y))255proof256  have transitive := IsLattice.transitive with lattice257  have meetA := meet.member with lattice, hx, hy258  have joinA := join.member with lattice, hx, hy259  have lower := meet.lower_left with lattice, hx, hy260  have upper := join.upper_left with lattice, hx, hy261  exact transitive with meet(A, r, x, y), meetA, x, hx, join(A, r, x, y),262      joinA, lower, upper263264-- Monotonicity265266theorem join.monotone (A r x y u v : Set)267  requires lattice : IsLattice(A, r)268  requires hx : x ∈ A269  requires hy : y ∈ A270  requires hu : u ∈ A271  requires hv : v ∈ A272  requires hxu : relates(r, x, u)273  requires hyv : relates(r, y, v)274  shows relates(r, join(A, r, x, y), join(A, r, u, v))275proof276  have transitive := IsLattice.transitive with lattice277  have joinA := join.member with lattice, hu, hv278  have uJ := join.upper_left with lattice, hu, hv279  have vJ := join.upper_right with lattice, hu, hv280  have xJ := transitive with x, hx, u, hu, join(A, r, u, v), joinA, hxu, uJ281  have yJ := transitive with y, hy, v, hv, join(A, r, u, v), joinA, hyv, vJ282  exact join.least with lattice, hx, hy, joinA, xJ, yJ283284theorem join.monotone_left (A r x y u : Set)285  requires lattice : IsLattice(A, r)286  requires hx : x ∈ A287  requires hy : y ∈ A288  requires hu : u ∈ A289  requires hxu : relates(r, x, u)290  shows relates(r, join(A, r, x, y), join(A, r, u, y))291proof292  have reflexive := IsLattice.reflexive with lattice293  exact join.monotone with lattice, hx, hy, hu, hy, hxu, (reflexive with y, hy)294295theorem join.monotone_right (A r x y v : Set)296  requires lattice : IsLattice(A, r)297  requires hx : x ∈ A298  requires hy : y ∈ A299  requires hv : v ∈ A300  requires hyv : relates(r, y, v)301  shows relates(r, join(A, r, x, y), join(A, r, x, v))302proof303  have reflexive := IsLattice.reflexive with lattice304  exact join.monotone with lattice, hx, hy, hx, hv, (reflexive with x, hx), hyv305306theorem meet.monotone (A r x y u v : Set)307  requires lattice : IsLattice(A, r)308  requires hx : x ∈ A309  requires hy : y ∈ A310  requires hu : u ∈ A311  requires hv : v ∈ A312  requires hxu : relates(r, x, u)313  requires hyv : relates(r, y, v)314  shows relates(r, meet(A, r, x, y), meet(A, r, u, v))315proof316  have transitive := IsLattice.transitive with lattice317  have meetA := meet.member with lattice, hx, hy318  have mX := meet.lower_left with lattice, hx, hy319  have mY := meet.lower_right with lattice, hx, hy320  have mU := transitive with meet(A, r, x, y), meetA, x, hx, u, hu, mX, hxu321  have mV := transitive with meet(A, r, x, y), meetA, y, hy, v, hv, mY, hyv322  exact meet.greatest with lattice, hu, hv, meetA, mU, mV323324theorem meet.monotone_left (A r x y u : Set)325  requires lattice : IsLattice(A, r)326  requires hx : x ∈ A327  requires hy : y ∈ A328  requires hu : u ∈ A329  requires hxu : relates(r, x, u)330  shows relates(r, meet(A, r, x, y), meet(A, r, u, y))331proof332  have reflexive := IsLattice.reflexive with lattice333  exact meet.monotone with lattice, hx, hy, hu, hy, hxu, (reflexive with y, hy)334335theorem meet.monotone_right (A r x y v : Set)336  requires lattice : IsLattice(A, r)337  requires hx : x ∈ A338  requires hy : y ∈ A339  requires hv : v ∈ A340  requires hyv : relates(r, y, v)341  shows relates(r, meet(A, r, x, y), meet(A, r, x, v))342proof343  have reflexive := IsLattice.reflexive with lattice344  exact meet.monotone with lattice, hx, hy, hx, hv, (reflexive with x, hx), hyv345346-- Associativity347348theorem join.associative (A r x y z : Set)349  requires lattice : IsLattice(A, r)350  requires hx : x ∈ A351  requires hy : y ∈ A352  requires hz : z ∈ A353  shows join(A, r, join(A, r, x, y), z) = join(A, r, x, join(A, r, y, z))354proof355  have transitive := IsLattice.transitive with lattice356  have xyA := join.member with lattice, hx, hy357  have yzA := join.member with lattice, hy, hz358  have uA := join.member with lattice, xyA, hz359  have xXY := join.upper_left with lattice, hx, hy360  have yXY := join.upper_right with lattice, hx, hy361  have yYZ := join.upper_left with lattice, hy, hz362  have zYZ := join.upper_right with lattice, hy, hz363  have xyU := join.upper_left with lattice, xyA, hz364  have zU := join.upper_right with lattice, xyA, hz365  have xU := transitive with x, hx, join(A, r, x, y), xyA, join(A, r, join(A,366      r, x, y), z), uA, xXY, xyU367  have yU := transitive with y, hy, join(A, r, x, y), xyA, join(A, r, join(A,368      r, x, y), z), uA, yXY, xyU369  have yzU := join.least with lattice, hy, hz, uA, yU, zU370  have supremum : Supremum(A, r, {x, join(A, r, y, z)}, join(A, r, join(A, r,371      x, y), z))372    apply Supremum.of_pair with hx, yzA, uA, xU, yzU373    intros b hb xb yzb374    have yb := transitive with y, hy, join(A, r, y, z), yzA, b, hb, yYZ, yzb375    have zb := transitive with z, hz, join(A, r, y, z), yzA, b, hb, zYZ, yzb376    have xyb := join.least with lattice, hx, hy, hb, xb, yb377    exact join.least with lattice, xyA, hz, hb, xyb, zb378  exact join.of_supremum with lattice, hx, yzA, supremum379380theorem meet.associative (A r x y z : Set)381  requires lattice : IsLattice(A, r)382  requires hx : x ∈ A383  requires hy : y ∈ A384  requires hz : z ∈ A385  shows meet(A, r, meet(A, r, x, y), z) = meet(A, r, x, meet(A, r, y, z))386proof387  have transitive := IsLattice.transitive with lattice388  have xyA := meet.member with lattice, hx, hy389  have yzA := meet.member with lattice, hy, hz390  have uA := meet.member with lattice, xyA, hz391  have xyX := meet.lower_left with lattice, hx, hy392  have xyY := meet.lower_right with lattice, hx, hy393  have yzY := meet.lower_left with lattice, hy, hz394  have yzZ := meet.lower_right with lattice, hy, hz395  have uXY := meet.lower_left with lattice, xyA, hz396  have uZ := meet.lower_right with lattice, xyA, hz397  have uX := transitive with meet(A, r, meet(A, r, x, y), z), uA, meet(A, r,398      x, y), xyA, x, hx, uXY, xyX399  have uY := transitive with meet(A, r, meet(A, r, x, y), z), uA, meet(A, r,400      x, y), xyA, y, hy, uXY, xyY401  have uYZ := meet.greatest with lattice, hy, hz, uA, uY, uZ402  have infimum : Infimum(A, r, {x, meet(A, r, y, z)}, meet(A, r, meet(A, r, x,403      y), z))404    apply Infimum.of_pair with hx, yzA, uA, uX, uYZ405    intros b hb bx byz406    have by_ := transitive with b, hb, meet(A, r, y, z), yzA, y, hy, byz, yzY407    have bz := transitive with b, hb, meet(A, r, y, z), yzA, z, hz, byz, yzZ408    have bxy := meet.greatest with lattice, hx, hy, hb, bx, by_409    exact meet.greatest with lattice, xyA, hz, hb, bxy, bz410  exact meet.of_infimum with lattice, hx, yzA, infimum411412theorem join.left_commutative (A r x y z : Set)413  requires lattice : IsLattice(A, r)414  requires hx : x ∈ A415  requires hy : y ∈ A416  requires hz : z ∈ A417  shows join(A, r, x, join(A, r, y, z)) = join(A, r, y, join(A, r, x, z))418proof419  have first := join.associative with lattice, hx, hy, hz420  have swap := join.commutative with lattice, hx, hy421  have second := join.associative with lattice, hy, hx, hz422  rw ← first423  rw swap424  exact second425426theorem meet.left_commutative (A r x y z : Set)427  requires lattice : IsLattice(A, r)428  requires hx : x ∈ A429  requires hy : y ∈ A430  requires hz : z ∈ A431  shows meet(A, r, x, meet(A, r, y, z)) = meet(A, r, y, meet(A, r, x, z))432proof433  have first := meet.associative with lattice, hx, hy, hz434  have swap := meet.commutative with lattice, hx, hy435  have second := meet.associative with lattice, hy, hx, hz436  rw ← first437  rw swap438  exact second439440-- The distributive and modular inequalities hold in every lattice.441442theorem meet.join_distributive_le (A r x y z : Set)443  requires lattice : IsLattice(A, r)444  requires hx : x ∈ A445  requires hy : y ∈ A446  requires hz : z ∈ A447  shows relates(r, join(A, r, meet(A, r, x, y), meet(A, r, x, z)),448    meet(A, r, x, join(A, r, y, z)))449proof450  have transitive := IsLattice.transitive with lattice451  have xyA := meet.member with lattice, hx, hy452  have xzA := meet.member with lattice, hx, hz453  have yzA := join.member with lattice, hy, hz454  have targetA := meet.member with lattice, hx, yzA455  have yYZ := join.upper_left with lattice, hy, hz456  have zYZ := join.upper_right with lattice, hy, hz457  have xyX := meet.lower_left with lattice, hx, hy458  have xyY := meet.lower_right with lattice, hx, hy459  have xzX := meet.lower_left with lattice, hx, hz460  have xzZ := meet.lower_right with lattice, hx, hz461  have xyYZ := transitive with meet(A, r, x, y), xyA, y, hy, join(A, r, y, z),462      yzA, xyY, yYZ463  have xzYZ := transitive with meet(A, r, x, z), xzA, z, hz, join(A, r, y, z),464      yzA, xzZ, zYZ465  have xyT := meet.greatest with lattice, hx, yzA, xyA, xyX, xyYZ466  have xzT := meet.greatest with lattice, hx, yzA, xzA, xzX, xzYZ467  exact join.least with lattice, xyA, xzA, targetA, xyT, xzT468469theorem join.meet_distributive_ge (A r x y z : Set)470  requires lattice : IsLattice(A, r)471  requires hx : x ∈ A472  requires hy : y ∈ A473  requires hz : z ∈ A474  shows relates(r, join(A, r, x, meet(A, r, y, z)),475    meet(A, r, join(A, r, x, y), join(A, r, x, z)))476proof477  have transitive := IsLattice.transitive with lattice478  have xyA := join.member with lattice, hx, hy479  have xzA := join.member with lattice, hx, hz480  have yzA := meet.member with lattice, hy, hz481  have targetA := meet.member with lattice, xyA, xzA482  have xXY := join.upper_left with lattice, hx, hy483  have xXZ := join.upper_left with lattice, hx, hz484  have yXY := join.upper_right with lattice, hx, hy485  have zXZ := join.upper_right with lattice, hx, hz486  have yzY := meet.lower_left with lattice, hy, hz487  have yzZ := meet.lower_right with lattice, hy, hz488  have xT := meet.greatest with lattice, xyA, xzA, hx, xXY, xXZ489  have yzXY := transitive with meet(A, r, y, z), yzA, y, hy, join(A, r, x, y),490      xyA, yzY, yXY491  have yzXZ := transitive with meet(A, r, y, z), yzA, z, hz, join(A, r, x, z),492      xzA, yzZ, zXZ493  have yzT := meet.greatest with lattice, xyA, xzA, yzA, yzXY, yzXZ494  exact join.least with lattice, hx, yzA, targetA, xT, yzT495496theorem join.modular_le (A r x y z : Set)497  requires lattice : IsLattice(A, r)498  requires hx : x ∈ A499  requires hy : y ∈ A500  requires hz : z ∈ A501  requires hyx : relates(r, y, x)502  shows503    relates(r, join(A, r, y, meet(A, r, x, z)), meet(A, r, x, join(A, r, y, z)))504proof505  have transitive := IsLattice.transitive with lattice506  have xzA := meet.member with lattice, hx, hz507  have yzA := join.member with lattice, hy, hz508  have targetA := meet.member with lattice, hx, yzA509  have yYZ := join.upper_left with lattice, hy, hz510  have zYZ := join.upper_right with lattice, hy, hz511  have xzX := meet.lower_left with lattice, hx, hz512  have xzZ := meet.lower_right with lattice, hx, hz513  have yT := meet.greatest with lattice, hx, yzA, hy, hyx, yYZ514  have xzYZ := transitive with meet(A, r, x, z), xzA, z, hz, join(A, r, y, z),515      yzA, xzZ, zYZ516  have xzT := meet.greatest with lattice, hx, yzA, xzA, xzX, xzYZ517  exact join.least with lattice, hy, xzA, targetA, yT, xzT518