Grace/Cumulus/Lattice/LinearLattice.g17

Open in Workbench Download source

Imports

Distributive

Declarations

Source

1-- Linear orders are distributive lattices2-- 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.LinearLattice8import Distributive910theorem IsLinearOrder.total (A r x y : Set)11  requires h : IsLinearOrder(A, r)12  requires hx : x ∈ A13  requires hy : y ∈ A14  shows relates(r, x, y) ∨ relates(r, y, x)15proof16  rcases h with ⟨partial, total⟩17  exact total with x, hx, y, hy1819theorem IsLinearOrder.converse (A r : Set)20  requires h : IsLinearOrder(A, r)21  shows IsLinearOrder(A, converse(r, A, A))22proof23  have order := IsLinearOrder.partial with h24  constructor25  . exact IsPartialOrder.converse with order26  . intros x hx y hy27    have cases := IsLinearOrder.total with h, hx, hy28    cases cases with xy | yx29    . right30      exact converse.relates with hx, hy, xy31    . left32      exact converse.relates with hy, hx, yx3334-- In a linear order the join of two elements is the larger and the meet35-- is the smaller.3637theorem IsLinearOrder.lattice (A r : Set)38  requires h : IsLinearOrder(A, r)39  shows IsLattice(A, r)40proof41  have order := IsLinearOrder.partial with h42  have reflexive := IsPartialOrder.reflexive with order43  apply IsLattice.of_pairs with order44  . intros x hx y hy45    have cases := IsLinearOrder.total with h, hx, hy46    cases cases with xy | yx47    . witness y48      apply Supremum.of_pair with hx, hy, hy, xy, (reflexive with y, hy)49      intros b hb xb yb50      exact yb51    . witness x52      apply Supremum.of_pair with hx, hy, hx, (reflexive with x, hx), yx53      intros b hb xb yb54      exact xb55  . intros x hx y hy56    have cases := IsLinearOrder.total with h, hx, hy57    cases cases with xy | yx58    . witness x59      apply Infimum.of_pair with hx, hy, hx, (reflexive with x, hx), xy60      intros b hb bx byBound61      exact bx62    . witness y63      apply Infimum.of_pair with hx, hy, hy, yx, (reflexive with y, hy)64      intros b hb bx byBound65      exact byBound6667theorem IsLinearOrder.join_cases (A r x y : Set)68  requires h : IsLinearOrder(A, r)69  requires hx : x ∈ A70  requires hy : y ∈ A71  shows join(A, r, x, y) = x ∨ join(A, r, x, y) = y72proof73  have lattice := IsLinearOrder.lattice with h74  have cases := IsLinearOrder.total with h, hx, hy75  cases cases with xy | yx76  . right77    exact join.of_le with lattice, hx, hy, xy78  . left79    exact join.of_ge with lattice, hx, hy, yx8081theorem IsLinearOrder.meet_cases (A r x y : Set)82  requires h : IsLinearOrder(A, r)83  requires hx : x ∈ A84  requires hy : y ∈ A85  shows meet(A, r, x, y) = x ∨ meet(A, r, x, y) = y86proof87  have lattice := IsLinearOrder.lattice with h88  have cases := IsLinearOrder.total with h, hx, hy89  cases cases with xy | yx90  . left91    exact meet.of_le with lattice, hx, hy, xy92  . right93    exact meet.of_ge with lattice, hx, hy, yx9495theorem IsLinearOrder.join_member_pair (A r x y : Set)96  requires h : IsLinearOrder(A, r)97  requires hx : x ∈ A98  requires hy : y ∈ A99  shows join(A, r, x, y) ∈ {x, y}100proof101  have cases := IsLinearOrder.join_cases with h, hx, hy102  cases cases with left | right103  . rw left104    exact pair.left at x, y105  . rw right106    exact pair.right at x, y107108theorem IsLinearOrder.meet_member_pair (A r x y : Set)109  requires h : IsLinearOrder(A, r)110  requires hx : x ∈ A111  requires hy : y ∈ A112  shows meet(A, r, x, y) ∈ {x, y}113proof114  have cases := IsLinearOrder.meet_cases with h, hx, hy115  cases cases with left | right116  . rw left117    exact pair.left at x, y118  . rw right119    exact pair.right at x, y120121-- Distributivity, first when the two joined elements are comparable in a122-- known direction, then in general.123124theorem IsLinearOrder.distributive_of_le (A r x y z : Set)125  requires h : IsLinearOrder(A, r)126  requires hx : x ∈ A127  requires hy : y ∈ A128  requires hz : z ∈ A129  requires hyz : relates(r, y, z)130  shows131    meet(A, r, x, join(A, r, y, z)) = join(A, r, meet(A, r, x, y), meet(A, r, x, z))132proof133  have lattice := IsLinearOrder.lattice with h134  have transitive := IsLattice.transitive with lattice135  have joinValue := join.of_le with lattice, hy, hz, hyz136  rw joinValue137  have casesXY := IsLinearOrder.total with h, hx, hy138  cases casesXY with xy | yx139  . have xz := transitive with x, hx, y, hy, z, hz, xy, hyz140    have meetY := meet.of_le with lattice, hx, hy, xy141    have meetZ := meet.of_le with lattice, hx, hz, xz142    rw [meetY, meetZ]143    symm144    exact join.idempotent with lattice, hx145  . have meetY := meet.of_ge with lattice, hx, hy, yx146    rw meetY147    have casesXZ := IsLinearOrder.total with h, hx, hz148    cases casesXZ with xz | zx149    . have meetZ := meet.of_le with lattice, hx, hz, xz150      rw meetZ151      symm152      exact join.of_le with lattice, hy, hx, yx153    . have meetZ := meet.of_ge with lattice, hx, hz, zx154      rw meetZ155      symm156      exact join.of_le with lattice, hy, hz, hyz157158theorem IsLinearOrder.distributive (A r : Set)159  requires h : IsLinearOrder(A, r)160  shows IsDistributiveLattice(A, r)161proof162  have lattice := IsLinearOrder.lattice with h163  constructor164  . exact lattice165  . intros x hx y hy z hz166    have cases := IsLinearOrder.total with h, hy, hz167    cases cases with yz | zy168    . exact IsLinearOrder.distributive_of_le with h, hx, hy, hz, yz169    . have swapJoin := join.commutative with lattice, hy, hz170      have xyA := meet.member with lattice, hx, hy171      have xzA := meet.member with lattice, hx, hz172      have swapMeets := join.commutative with lattice, xyA, xzA173      rw [swapJoin, swapMeets]174      exact IsLinearOrder.distributive_of_le with h, hx, hz, hy, zy175176theorem IsLinearOrder.modular (A r : Set)177  requires h : IsLinearOrder(A, r)178  shows IsModularLattice(A, r)179proof180  exact IsDistributiveLattice.modular with (IsLinearOrder.distributive with h)181