Grace/Cumulus/Lattice/Sublattices.g17

Open in Workbench Download source

Imports

Sublattice · CompleteLattice

Declarations

Source

1-- Sublattices of a bundled lattice and the restricted order2-- 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.Sublattices8import Sublattice9import CompleteLattice1011-- A sublattice is a subset of the points closed under join and meet.12predicate Sublattice (P B : Set) := IsSublattice(points(P), le(P), B)1314notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis Sublattice(P, B) for P.points15notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis Sublattice(P, B) for P.points16notation infix 50 "≤" => Le(P, _, _) via hypothesis Sublattice(P, B) for P.points1718instance Sublattice.unbundled (P B : Set)19  requires sub : Sublattice(P, B)20  shows IsSublattice(points(P), le(P), B)21proof22  simp [Sublattice]2324theorem Sublattice.mk (A r B : Set)25  requires sub : IsSublattice(A, r, B)26  shows Sublattice(Order.mk(A, r), B)27proof28  unfold Sublattice29  rw [Order.mk.points, Order.mk.le]30  exact sub3132instance Sublattice.lattice_of (P B : Set)33  requires sub : Sublattice(P, B)34  shows Lattice(P)35proof36  unfold Join.Lattice37  exact IsSublattice.lattice with (Sublattice.unbundled with sub)3839theorem Sublattice.subset_points (P B : Set)40  requires sub : Sublattice(P, B)41  shows B ⊆ points(P)42proof43  exact IsSublattice.subset with (Sublattice.unbundled with sub)4445theorem Sublattice.mem_points (P B x : Set)46  requires sub : Sublattice(P, B)47  requires xIn : x ∈ B48  shows x ∈ points(P)49proof50  have subset := Sublattice.subset_points with sub51  exact subset with x, xIn5253section SublatticeClosure54variable (P B : Set)55hypothesis sub : Sublattice(P, B)5657instance Sublattice.sup_mem (a b : Set)58  requires aIn : a ∈ B59  requires bIn : b ∈ B60  shows a ⊔ b ∈ B61proof62  have aCarrier := Sublattice.mem_points with sub, aIn63  have bCarrier := Sublattice.mem_points with sub, bIn64  rw sup.join65  exact IsSublattice.join_closed with (Sublattice.unbundled with sub), aIn, bIn6667instance Sublattice.inf_mem (a b : Set)68  requires aIn : a ∈ B69  requires bIn : b ∈ B70  shows a ⊓ b ∈ B71proof72  have aCarrier := Sublattice.mem_points with sub, aIn73  have bCarrier := Sublattice.mem_points with sub, bIn74  rw inf.meet75  exact IsSublattice.meet_closed with (Sublattice.unbundled with sub), aIn, bIn7677end SublatticeClosure7879theorem Sublattice.univ (P : Set)80  requires lattice : Lattice(P)81  shows Sublattice(P, points(P))82proof83  unfold Sublattice84  exact IsSublattice.whole with (Lattice.unbundled with lattice)8586theorem Sublattice.inter (P B C : Set)87  requires hB : Sublattice(P, B)88  requires hC : Sublattice(P, C)89  shows Sublattice(P, B ∩ C)90proof91  unfold Sublattice92  exact IsSublattice.intersection with (Sublattice.unbundled with hB),93      (Sublattice.unbundled with hC)9495-- The order restricted to a subset, as a bundled order.96def suborder (P B : Set) : Set := Order.mk(B, restrictOrder(le(P), B))9798theorem suborder.points (P B : Set)99  shows points(suborder(P, B)) = B100proof101  simp [suborder, Order.mk.points]102103theorem suborder.le (P B : Set)104  shows le(suborder(P, B)) = restrictOrder(le(P), B)105proof106  simp [suborder, Order.mk.le]107108theorem suborder.partial_order (P B : Set)109  requires order : PartialOrder(P)110  requires hB : B ⊆ points(P)111  shows PartialOrder(suborder(P, B))112proof113  unfold suborder114  apply PartialOrder.mk115  exact restrictOrder.partial with (PartialOrder.unbundled with order), hB116117instance Sublattice.lattice_suborder (P B : Set)118  requires sub : Sublattice(P, B)119  shows Lattice(suborder(P, B))120proof121  unfold suborder122  apply Lattice.mk123  exact IsSublattice.restricted with (Sublattice.unbundled with sub)124125-- Join and meet in the restricted lattice agree with those of P; the126-- restricted operation is written as its application, since the operands127-- lie in both carriers.128section Suborder129variable (P B : Set)130hypothesis sub : Sublattice(P, B)131132theorem Sublattice.sup_suborder (a b : Set)133  requires aIn : a ∈ B134  requires bIn : b ∈ B135  shows call2(sup(suborder(P, B)), a, b) = a ⊔ b136proof137  have restricted : Lattice(suborder(P, B)) := Sublattice.lattice_suborder with138      sub139  have aCarrier := Sublattice.mem_points with sub, aIn140  have bCarrier := Sublattice.mem_points with sub, bIn141  have aSub : a ∈ points(suborder(P, B))142    rw suborder.points143    exact aIn144  have bSub : b ∈ points(suborder(P, B))145    rw suborder.points146    exact bIn147  have inner := sup.join at suborder(P, B), a, b with restricted148  have outer := sup.join at P, a, b with *149  rw [inner, outer, suborder.points, suborder.le]150  exact IsSublattice.join with (Sublattice.unbundled with sub), aIn, bIn151152theorem Sublattice.inf_suborder (a b : Set)153  requires aIn : a ∈ B154  requires bIn : b ∈ B155  shows call2(inf(suborder(P, B)), a, b) = a ⊓ b156proof157  have restricted : Lattice(suborder(P, B)) := Sublattice.lattice_suborder with158      sub159  have aCarrier := Sublattice.mem_points with sub, aIn160  have bCarrier := Sublattice.mem_points with sub, bIn161  have aSub : a ∈ points(suborder(P, B))162    rw suborder.points163    exact aIn164  have bSub : b ∈ points(suborder(P, B))165    rw suborder.points166    exact bIn167  have inner := inf.meet at suborder(P, B), a, b with restricted168  have outer := inf.meet at P, a, b with *169  rw [inner, outer, suborder.points, suborder.le]170  exact IsSublattice.meet with (Sublattice.unbundled with sub), aIn, bIn171172end Suborder173