Grace/Cumulus/Lattice/FixedPoints.g17

Open in Workbench Download source

Imports

Tarski · OrderHom

Declarations

Source

1-- Knaster–Tarski: least and greatest fixed points on a complete lattice2-- 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.FixedPoints8import Tarski9import OrderHom1011-- The prefixed, postfixed, and fixed points of a map on a bundled order,12-- and its least and greatest fixed points: the infimum of the prefixed13-- points and the supremum of the postfixed points. The definitions live in14-- the section of the ordered set, so they take P as their first parameter15-- and are written without it inside the section.16section FixedPoints17variable (P : Set)1819def prefixPoints (f : Set) : Set := latticePrefixed(f, points(P), le(P))20def postfixPoints (f : Set) : Set := latticePostfixed(f, points(P), le(P))21def fixedPoints (f : Set) : Set := latticeFixedPoints(f, points(P))22def lfp (f : Set) : Set := latticeLeastFixed(f, points(P), le(P))23def gfp (f : Set) : Set := latticeGreatestFixed(f, points(P), le(P))2425theorem prefixPoints.membership (f x : Set)26  shows x ∈ prefixPoints(f) ↔ (x ∈ points(P) ∧ relates(le(P), f(x), x))27proof28  simp [prefixPoints, latticePrefixed]2930theorem postfixPoints.membership (f x : Set)31  shows x ∈ postfixPoints(f) ↔ (x ∈ points(P) ∧ relates(le(P), x, f(x)))32proof33  simp [postfixPoints, latticePostfixed]3435theorem fixedPoints.membership (f x : Set)36  shows x ∈ fixedPoints(f) ↔ (x ∈ points(P) ∧ f(x) = x)37proof38  simp [fixedPoints, latticeFixedPoints]3940theorem prefixPoints.subset (f : Set)41  shows prefixPoints(f) ⊆ points(P)42proof43  unfold prefixPoints44  exact latticePrefixed.subset at f, points(P), le(P)4546theorem postfixPoints.subset (f : Set)47  shows postfixPoints(f) ⊆ points(P)48proof49  unfold postfixPoints50  exact latticePostfixed.subset at f, points(P), le(P)5152theorem fixedPoints.subset (f : Set)53  shows fixedPoints(f) ⊆ points(P)54proof55  unfold fixedPoints56  exact latticeFixedPoints.subset at f, points(P)5758theorem lfp.unfold (f : Set)59  shows lfp(f) = latticeLeastFixed(f, points(P), le(P))60proof61  simp [lfp]6263theorem gfp.unfold (f : Set)64  shows gfp(f) = latticeGreatestFixed(f, points(P), le(P))65proof66  simp [gfp]6768section FixedPointLaws69variable (f : Set)70hypothesis complete : CompleteLattice(P)71hypothesis monotone : MonotoneMap(f, P, P)7273theorem lfp.eq_sInf74  shows lfp(f) = sInf(P)(prefixPoints(f))75proof76  have subset := prefixPoints.subset at P, f77  rw [sInf.infimum, lfp.unfold, latticeLeastFixed.value]78  unfold prefixPoints79  rfl8081theorem gfp.eq_sSup82  shows gfp(f) = sSup(P)(postfixPoints(f))83proof84  have subset := postfixPoints.subset at P, f85  rw [sSup.supremum, gfp.unfold, latticeGreatestFixed.value]86  unfold postfixPoints87  rfl8889instance lfp.member90  shows lfp(f) ∈ points(P)91proof92  rw lfp.unfold93  exact latticeLeastFixed.member with (CompleteLattice.unbundled with complete)9495instance gfp.member96  shows gfp(f) ∈ points(P)97proof98  rw gfp.unfold99  exact latticeGreatestFixed.member with (CompleteLattice.unbundled with complete)100101theorem lfp_le (a ∈ points(P))102  requires prefixed : f(a) ≤ a103  shows lfp(f) ≤ a104proof105  rw lfp.unfold106  exact latticeLeastFixed.below with (CompleteLattice.unbundled with complete),107      *108109theorem le_gfp (a ∈ points(P))110  requires postfixed : a ≤ f(a)111  shows a ≤ gfp(f)112proof113  rw gfp.unfold114  exact latticeGreatestFixed.above with (CompleteLattice.unbundled with complete),115      *116117theorem lfp_le_fixed (a ∈ points(P))118  requires fixed : f(a) = a119  shows lfp(f) ≤ a120proof121  rw lfp.unfold122  exact latticeLeastFixed.least with (CompleteLattice.unbundled with complete),123      *124125theorem le_gfp_fixed (a ∈ points(P))126  requires fixed : f(a) = a127  shows a ≤ gfp(f)128proof129  rw gfp.unfold130  exact latticeGreatestFixed.greatest with (CompleteLattice.unbundled with complete),131      *132133theorem map_lfp_le134  shows f(lfp(f)) ≤ lfp(f)135proof136  rw lfp.unfold137  exact latticeLeastFixed.prefixed with (CompleteLattice.unbundled with complete),138      (MonotoneMap.unbundled with monotone)139140theorem le_map_gfp141  shows gfp(f) ≤ f(gfp(f))142proof143  rw gfp.unfold144  exact latticeGreatestFixed.postfixed with (CompleteLattice.unbundled with complete),145      (MonotoneMap.unbundled with monotone)146147theorem lfp_fixed148  shows f(lfp(f)) = lfp(f)149proof150  have prefixed : f(lfp(f)) ≤ lfp(f) := map_lfp_le with *151  have mapped : f(f(lfp(f))) ≤ f(lfp(f)) := MonotoneMap.map_le with *152  have postfixed : lfp(f) ≤ f(lfp(f)) := lfp_le with *153  exact le_antisymm with *154155theorem gfp_fixed156  shows f(gfp(f)) = gfp(f)157proof158  have postfixed : gfp(f) ≤ f(gfp(f)) := le_map_gfp with *159  have mapped : f(gfp(f)) ≤ f(f(gfp(f))) := MonotoneMap.map_le with *160  have prefixed : f(gfp(f)) ≤ gfp(f) := le_gfp with *161  exact le_antisymm with *162163theorem lfp.mem_fixedPoints164  shows lfp(f) ∈ fixedPoints(f)165proof166  have fixed : f(lfp(f)) = lfp(f) := lfp_fixed with *167  have member : lfp(f) ∈ points(P) := lfp.member with *168  apply fixedPoints.membership.backward169  exact ⟨member, fixed⟩170171theorem gfp.mem_fixedPoints172  shows gfp(f) ∈ fixedPoints(f)173proof174  have fixed : f(gfp(f)) = gfp(f) := gfp_fixed with *175  have member : gfp(f) ∈ points(P) := gfp.member with *176  apply fixedPoints.membership.backward177  exact ⟨member, fixed⟩178179theorem lfp.isLeast180  shows IsLeast(P, fixedPoints(f), lfp(f))181proof182  unfold IsLeast183  unfold fixedPoints184  rw lfp.unfold185  exact latticeLeastFixed.least_fixed with (CompleteLattice.unbundled with complete),186      (MonotoneMap.unbundled with monotone)187188theorem gfp.isGreatest189  shows IsGreatest(P, fixedPoints(f), gfp(f))190proof191  unfold IsGreatest192  unfold fixedPoints193  rw gfp.unfold194  exact latticeGreatestFixed.greatest_fixed with (CompleteLattice.unbundled with complete),195      (MonotoneMap.unbundled with monotone)196197theorem exists_fixed_point198  shows ∃ a ∈ points(P), f(a) = a199proof200  exact IsMonotoneMap.exists_fixed_point with (CompleteLattice.unbundled with complete),201      (MonotoneMap.unbundled with monotone)202203theorem fixedPoints.nonempty204  shows Nonempty(fixedPoints(f))205proof206  have member := lfp.mem_fixedPoints with *207  exact ⟨lfp(f), member⟩208209theorem lfp_le_gfp210  shows lfp(f) ≤ gfp(f)211proof212  have fixed : f(gfp(f)) = gfp(f) := gfp_fixed with *213  exact lfp_le_fixed with *214215end FixedPointLaws216end FixedPoints217