Grace/Cumulus/Lattice/Lattice.g17

Open in Workbench Download source

Imports

Bounds

Declarations

Source

1-- Lattices: ordered sets in which every pair has a join and a meet2-- 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.Lattice8import Bounds910predicate IsLattice (A r : Set) :=11  IsPartialOrder(A, r) ∧12  (∀ x ∈ A, ∀ y ∈ A,13    (∃ s, Supremum(A, r, {x, y}, s)) ∧ (∃ i, Infimum(A, r, {x, y}, i)))1415theorem IsLattice.order (A r : Set)16  requires h : IsLattice(A, r)17  shows IsPartialOrder(A, r)18proof19  simp [IsLattice]2021theorem IsLattice.reflexive (A r : Set)22  requires h : IsLattice(A, r)23  shows ReflexiveOn(A, r)24proof25  exact IsPartialOrder.reflexive with (IsLattice.order with h)2627theorem IsLattice.transitive (A r : Set)28  requires h : IsLattice(A, r)29  shows TransitiveOn(A, r)30proof31  exact IsPartialOrder.transitive with (IsLattice.order with h)3233theorem IsLattice.antisymmetric (A r : Set)34  requires h : IsLattice(A, r)35  shows AntisymmetricOn(A, r)36proof37  exact IsPartialOrder.antisymmetric with (IsLattice.order with h)3839theorem IsLattice.exists_supremum (A r x y : Set)40  requires h : IsLattice(A, r)41  requires hx : x ∈ A42  requires hy : y ∈ A43  shows ∃ s, Supremum(A, r, {x, y}, s)44proof45  rcases h with ⟨order, pairs⟩46  have both := pairs with x, hx, y, hy47  exact both.left4849theorem IsLattice.exists_infimum (A r x y : Set)50  requires h : IsLattice(A, r)51  requires hx : x ∈ A52  requires hy : y ∈ A53  shows ∃ i, Infimum(A, r, {x, y}, i)54proof55  rcases h with ⟨order, pairs⟩56  have both := pairs with x, hx, y, hy57  exact both.right5859-- The join of two elements is the supremum of the pair, and the meet is60-- its infimum. Both are determined uniquely by antisymmetry.6162defunique join (A r x y : Set) (z ∈ A) := Supremum(A, r, {x, y}, z)63requires lattice : IsLattice(A, r)64requires hx : x ∈ A65requires hy : y ∈ A66proof67  obtain ⟨s, hs⟩ := IsLattice.exists_supremum with lattice, hx, hy68  witness s69  refine ⟨Supremum.member with hs, hs⟩70uniqueness71  intros s sA first t tA second72  exact Supremum.unique with (IsLattice.order with lattice), first, second7374defunique meet (A r x y : Set) (z ∈ A) := Infimum(A, r, {x, y}, z)75requires lattice : IsLattice(A, r)76requires hx : x ∈ A77requires hy : y ∈ A78proof79  obtain ⟨i, hi⟩ := IsLattice.exists_infimum with lattice, hx, hy80  witness i81  refine ⟨Infimum.member with hi, hi⟩82uniqueness83  intros i iA first j jA second84  exact Infimum.unique with (IsLattice.order with lattice), first, second8586theorem join.member (A r x y : Set)87  requires lattice : IsLattice(A, r)88  requires hx : x ∈ A89  requires hy : y ∈ A90  shows join(A, r, x, y) ∈ A91proof92  have selected := join.selected with lattice, hx, hy93  exact selected.left9495theorem join.supremum (A r x y : Set)96  requires lattice : IsLattice(A, r)97  requires hx : x ∈ A98  requires hy : y ∈ A99  shows Supremum(A, r, {x, y}, join(A, r, x, y))100proof101  have selected := join.selected with lattice, hx, hy102  exact selected.right103104theorem join.upper_left (A r x y : Set)105  requires lattice : IsLattice(A, r)106  requires hx : x ∈ A107  requires hy : y ∈ A108  shows relates(r, x, join(A, r, x, y))109proof110  exact Supremum.pair_left with (join.supremum with lattice, hx, hy)111112theorem join.upper_right (A r x y : Set)113  requires lattice : IsLattice(A, r)114  requires hx : x ∈ A115  requires hy : y ∈ A116  shows relates(r, y, join(A, r, x, y))117proof118  exact Supremum.pair_right with (join.supremum with lattice, hx, hy)119120theorem join.least (A r x y b : Set)121  requires lattice : IsLattice(A, r)122  requires hx : x ∈ A123  requires hy : y ∈ A124  requires hb : b ∈ A125  requires hxb : relates(r, x, b)126  requires hyb : relates(r, y, b)127  shows relates(r, join(A, r, x, y), b)128proof129  have supremum := join.supremum with lattice, hx, hy130  exact Supremum.pair_least with supremum, hb, hxb, hyb131132theorem join.of_supremum (A r x y z : Set)133  requires lattice : IsLattice(A, r)134  requires hx : x ∈ A135  requires hy : y ∈ A136  requires h : Supremum(A, r, {x, y}, z)137  shows z = join(A, r, x, y)138proof139  have order := IsLattice.order with lattice140  have supremum := join.supremum with lattice, hx, hy141  exact Supremum.unique with order, h, supremum142143theorem meet.member (A r x y : Set)144  requires lattice : IsLattice(A, r)145  requires hx : x ∈ A146  requires hy : y ∈ A147  shows meet(A, r, x, y) ∈ A148proof149  have selected := meet.selected with lattice, hx, hy150  exact selected.left151152theorem meet.infimum (A r x y : Set)153  requires lattice : IsLattice(A, r)154  requires hx : x ∈ A155  requires hy : y ∈ A156  shows Infimum(A, r, {x, y}, meet(A, r, x, y))157proof158  have selected := meet.selected with lattice, hx, hy159  exact selected.right160161theorem meet.lower_left (A r x y : Set)162  requires lattice : IsLattice(A, r)163  requires hx : x ∈ A164  requires hy : y ∈ A165  shows relates(r, meet(A, r, x, y), x)166proof167  exact Infimum.pair_left with (meet.infimum with lattice, hx, hy)168169theorem meet.lower_right (A r x y : Set)170  requires lattice : IsLattice(A, r)171  requires hx : x ∈ A172  requires hy : y ∈ A173  shows relates(r, meet(A, r, x, y), y)174proof175  exact Infimum.pair_right with (meet.infimum with lattice, hx, hy)176177theorem meet.greatest (A r x y b : Set)178  requires lattice : IsLattice(A, r)179  requires hx : x ∈ A180  requires hy : y ∈ A181  requires hb : b ∈ A182  requires hbx : relates(r, b, x)183  requires hby : relates(r, b, y)184  shows relates(r, b, meet(A, r, x, y))185proof186  have infimum := meet.infimum with lattice, hx, hy187  exact Infimum.pair_greatest with infimum, hb, hbx, hby188189theorem meet.of_infimum (A r x y z : Set)190  requires lattice : IsLattice(A, r)191  requires hx : x ∈ A192  requires hy : y ∈ A193  requires h : Infimum(A, r, {x, y}, z)194  shows z = meet(A, r, x, y)195proof196  have order := IsLattice.order with lattice197  have infimum := meet.infimum with lattice, hx, hy198  exact Infimum.unique with order, h, infimum199200-- A lattice may be built from any choice of pairwise suprema and infima.201202theorem IsLattice.of_pairs (A r : Set)203  requires order : IsPartialOrder(A, r)204  requires suprema : ∀ x ∈ A, ∀ y ∈ A, ∃ s, Supremum(A, r, {x, y}, s)205  requires infima : ∀ x ∈ A, ∀ y ∈ A, ∃ i, Infimum(A, r, {x, y}, i)206  shows IsLattice(A, r)207proof208  constructor209  . exact order210  . intros x hx y hy211    have supremum := suprema with x, hx, y, hy212    have infimum := infima with x, hx, y, hy213    constructor214    . exact supremum215    . exact infimum216217-- The dual of a lattice is a lattice, with join and meet exchanged.218219theorem IsLattice.converse (A r : Set)220  requires lattice : IsLattice(A, r)221  shows IsLattice(A, converse(r, A, A))222proof223  have order := IsLattice.order with lattice224  apply IsLattice.of_pairs with (IsPartialOrder.converse with order)225  . intros x hx y hy226    obtain ⟨i, hi⟩ := IsLattice.exists_infimum with lattice, hx, hy227    refine ⟨i, Infimum.converse with hi⟩228  . intros x hx y hy229    obtain ⟨s, hs⟩ := IsLattice.exists_supremum with lattice, hx, hy230    refine ⟨s, Supremum.converse with hs⟩231232theorem join.converse (A r x y : Set)233  requires lattice : IsLattice(A, r)234  requires hx : x ∈ A235  requires hy : y ∈ A236  shows join(A, converse(r, A, A), x, y) = meet(A, r, x, y)237proof238  have dual := IsLattice.converse with lattice239  have infimum := meet.infimum with lattice, hx, hy240  have supremum := Infimum.converse with infimum241  symm242  exact join.of_supremum with dual, hx, hy, supremum243244theorem meet.converse (A r x y : Set)245  requires lattice : IsLattice(A, r)246  requires hx : x ∈ A247  requires hy : y ∈ A248  shows meet(A, converse(r, A, A), x, y) = join(A, r, x, y)249proof250  have dual := IsLattice.converse with lattice251  have supremum := join.supremum with lattice, hx, hy252  have infimum := Supremum.converse with supremum253  symm254  exact meet.of_infimum with dual, hx, hy, infimum255