Grace/Cumulus/Lattice/Tarski.g17

Open in Workbench Download source

Imports

Monotone

Declarations

Source

1-- Fixed points of monotone maps 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.Tarski8import Monotone910def latticePrefixed (f A r : Set) : Set := { x ∈ A | relates(r, f(x), x) }11def latticePostfixed (f A r : Set) : Set := { x ∈ A | relates(r, x, f(x)) }12def latticeFixedPoints (f A : Set) : Set := { x ∈ A | f(x) = x }1314-- The least fixed point is the infimum of the prefixed points, and the15-- greatest fixed point is the supremum of the postfixed points.16def latticeLeastFixed (f A r : Set) : Set :=17  infimum(A, r, latticePrefixed(f, A, r))18def latticeGreatestFixed (f A r : Set) : Set :=19  supremum(A, r, latticePostfixed(f, A, r))2021theorem latticeLeastFixed.value (f A r : Set)22  shows latticeLeastFixed(f, A, r) = infimum(A, r, latticePrefixed(f, A, r))23proof24  simp [latticeLeastFixed]2526theorem latticeGreatestFixed.value (f A r : Set)27  shows28    latticeGreatestFixed(f, A, r) = supremum(A, r, latticePostfixed(f, A, r))29proof30  simp [latticeGreatestFixed]3132theorem latticePrefixed.subset (f A r : Set)33  shows latticePrefixed(f, A, r) ⊆ A34proof35  intros x hx36  have member := latticePrefixed.membership.forward with hx37  exact member.left3839theorem latticePostfixed.subset (f A r : Set)40  shows latticePostfixed(f, A, r) ⊆ A41proof42  intros x hx43  have member := latticePostfixed.membership.forward with hx44  exact member.left4546theorem latticeFixedPoints.subset (f A : Set)47  shows latticeFixedPoints(f, A) ⊆ A48proof49  intros x hx50  have member := latticeFixedPoints.membership.forward with hx51  exact member.left5253-- The least fixed point5455theorem latticeLeastFixed.member (f A r : Set)56  requires complete : IsCompleteLattice(A, r)57  shows latticeLeastFixed(f, A, r) ∈ A58proof59  have value := latticeLeastFixed.value at f, A, r60  rw value61  exact infimum.member with complete, (latticePrefixed.subset at f, A, r)6263theorem latticeLeastFixed.below (f A r x : Set)64  requires complete : IsCompleteLattice(A, r)65  requires hx : x ∈ A66  requires prefixed : relates(r, f(x), x)67  shows relates(r, latticeLeastFixed(f, A, r), x)68proof69  have value := latticeLeastFixed.value at f, A, r70  rw value71  have member : x ∈ latticePrefixed(f, A, r) :=72    latticePrefixed.membership.backward with ⟨hx, prefixed⟩73  exact infimum.below with complete, (latticePrefixed.subset at f, A, r), member7475theorem latticeLeastFixed.prefixed (f A r : Set)76  requires complete : IsCompleteLattice(A, r)77  requires monotone : IsMonotoneMap(f, A, r, A, r)78  shows relates(r, f(latticeLeastFixed(f, A, r)), latticeLeastFixed(f, A, r))79proof80  have order := IsCompleteLattice.order with complete81  have transitive := IsPartialOrder.transitive with order82  have bounded := latticePrefixed.subset at f, A, r83  have leastA := latticeLeastFixed.member at f, A, r with complete84  have valueA := IsMonotoneMap.apply_member with monotone, leastA85  have lower : LowerBound(A, r, latticePrefixed(f, A, r),86      f(latticeLeastFixed(f, A, r)))87    refine ⟨valueA, bounded, ?_⟩88    intros x hx89    have member := latticePrefixed.membership.forward with hx90    have below := latticeLeastFixed.below with complete, member.left,91        member.right92    have mapped := IsMonotoneMap.preserves with monotone, leastA, member.left,93        below94    have fxA := IsMonotoneMap.apply_member with monotone, member.left95    exact transitive with f(latticeLeastFixed(f, A, r)), valueA, f(x), fxA, x,96        member.left, mapped, member.right97  have value := latticeLeastFixed.value at f, A, r98  rw value99  rw value at lower100  rw value at valueA101  exact infimum.greatest with complete, bounded, valueA, lower102103theorem latticeLeastFixed.fixed (f A r : Set)104  requires complete : IsCompleteLattice(A, r)105  requires monotone : IsMonotoneMap(f, A, r, A, r)106  shows f(latticeLeastFixed(f, A, r)) = latticeLeastFixed(f, A, r)107proof108  have order := IsCompleteLattice.order with complete109  have antisymmetric := IsPartialOrder.antisymmetric with order110  have leastA := latticeLeastFixed.member at f, A, r with complete111  have valueA := IsMonotoneMap.apply_member with monotone, leastA112  have prefixed := latticeLeastFixed.prefixed with complete, monotone113  have mapped := IsMonotoneMap.preserves with monotone, valueA, leastA, prefixed114  have above := latticeLeastFixed.below with complete, valueA, mapped115  exact antisymmetric with f(latticeLeastFixed(f, A, r)), valueA,116      latticeLeastFixed(f, A, r), leastA, prefixed, above117118theorem latticeLeastFixed.least (f A r x : Set)119  requires complete : IsCompleteLattice(A, r)120  requires hx : x ∈ A121  requires fixed : f(x) = x122  shows relates(r, latticeLeastFixed(f, A, r), x)123proof124  have reflexive := IsPartialOrder.reflexive with125      (IsCompleteLattice.order with complete)126  have prefixed : relates(r, f(x), x)127    rw fixed128    exact reflexive with x, hx129  exact latticeLeastFixed.below with complete, hx, prefixed130131theorem latticeLeastFixed.least_fixed (f A r : Set)132  requires complete : IsCompleteLattice(A, r)133  requires monotone : IsMonotoneMap(f, A, r, A, r)134  shows Least(A, r, latticeFixedPoints(f, A), latticeLeastFixed(f, A, r))135proof136  have leastA := latticeLeastFixed.member at f, A, r with complete137  have fixed := latticeLeastFixed.fixed with complete, monotone138  constructor139  . exact latticeFixedPoints.membership.backward with ⟨leastA, fixed⟩140  . refine ⟨leastA, (latticeFixedPoints.subset at f, A), ?_⟩141    intros x hx142    have member := latticeFixedPoints.membership.forward with hx143    exact latticeLeastFixed.least with complete, member.left, member.right144145-- The greatest fixed point146147theorem latticeGreatestFixed.member (f A r : Set)148  requires complete : IsCompleteLattice(A, r)149  shows latticeGreatestFixed(f, A, r) ∈ A150proof151  have value := latticeGreatestFixed.value at f, A, r152  rw value153  exact supremum.member with complete, (latticePostfixed.subset at f, A, r)154155theorem latticeGreatestFixed.above (f A r x : Set)156  requires complete : IsCompleteLattice(A, r)157  requires hx : x ∈ A158  requires postfixed : relates(r, x, f(x))159  shows relates(r, x, latticeGreatestFixed(f, A, r))160proof161  have value := latticeGreatestFixed.value at f, A, r162  rw value163  have member : x ∈ latticePostfixed(f, A, r) :=164    latticePostfixed.membership.backward with ⟨hx, postfixed⟩165  exact supremum.above with complete, (latticePostfixed.subset at f, A, r),166      member167168theorem latticeGreatestFixed.postfixed (f A r : Set)169  requires complete : IsCompleteLattice(A, r)170  requires monotone : IsMonotoneMap(f, A, r, A, r)171  shows172    relates(r, latticeGreatestFixed(f, A, r), f(latticeGreatestFixed(f, A, r)))173proof174  have order := IsCompleteLattice.order with complete175  have transitive := IsPartialOrder.transitive with order176  have bounded := latticePostfixed.subset at f, A, r177  have greatestA := latticeGreatestFixed.member at f, A, r with complete178  have valueA := IsMonotoneMap.apply_member with monotone, greatestA179  have upper : UpperBound(A, r, latticePostfixed(f, A, r),180      f(latticeGreatestFixed(f, A, r)))181    refine ⟨valueA, bounded, ?_⟩182    intros x hx183    have member := latticePostfixed.membership.forward with hx184    have above := latticeGreatestFixed.above with complete, member.left,185        member.right186    have mapped := IsMonotoneMap.preserves with monotone, member.left,187        greatestA, above188    have fxA := IsMonotoneMap.apply_member with monotone, member.left189    exact transitive with x, member.left, f(x), fxA, f(latticeGreatestFixed(f,190        A, r)), valueA, member.right, mapped191  have value := latticeGreatestFixed.value at f, A, r192  rw value193  rw value at upper194  rw value at valueA195  exact supremum.least with complete, bounded, valueA, upper196197theorem latticeGreatestFixed.fixed (f A r : Set)198  requires complete : IsCompleteLattice(A, r)199  requires monotone : IsMonotoneMap(f, A, r, A, r)200  shows f(latticeGreatestFixed(f, A, r)) = latticeGreatestFixed(f, A, r)201proof202  have order := IsCompleteLattice.order with complete203  have antisymmetric := IsPartialOrder.antisymmetric with order204  have greatestA := latticeGreatestFixed.member at f, A, r with complete205  have valueA := IsMonotoneMap.apply_member with monotone, greatestA206  have postfixed := latticeGreatestFixed.postfixed with complete, monotone207  have mapped := IsMonotoneMap.preserves with monotone, greatestA, valueA,208      postfixed209  have below := latticeGreatestFixed.above with complete, valueA, mapped210  exact antisymmetric with f(latticeGreatestFixed(f, A, r)), valueA,211      latticeGreatestFixed(f, A, r), greatestA, below, postfixed212213theorem latticeGreatestFixed.greatest (f A r x : Set)214  requires complete : IsCompleteLattice(A, r)215  requires hx : x ∈ A216  requires fixed : f(x) = x217  shows relates(r, x, latticeGreatestFixed(f, A, r))218proof219  have reflexive := IsPartialOrder.reflexive with220      (IsCompleteLattice.order with complete)221  have postfixed : relates(r, x, f(x))222    rw fixed223    exact reflexive with x, hx224  exact latticeGreatestFixed.above with complete, hx, postfixed225226theorem latticeGreatestFixed.greatest_fixed (f A r : Set)227  requires complete : IsCompleteLattice(A, r)228  requires monotone : IsMonotoneMap(f, A, r, A, r)229  shows Greatest(A, r, latticeFixedPoints(f, A), latticeGreatestFixed(f, A, r))230proof231  have greatestA := latticeGreatestFixed.member at f, A, r with complete232  have fixed := latticeGreatestFixed.fixed with complete, monotone233  constructor234  . exact latticeFixedPoints.membership.backward with ⟨greatestA, fixed⟩235  . refine ⟨greatestA, (latticeFixedPoints.subset at f, A), ?_⟩236    intros x hx237    have member := latticeFixedPoints.membership.forward with hx238    exact latticeGreatestFixed.greatest with complete, member.left, member.right239240-- Consequences241242theorem IsMonotoneMap.exists_fixed_point (f A r : Set)243  requires complete : IsCompleteLattice(A, r)244  requires monotone : IsMonotoneMap(f, A, r, A, r)245  shows ∃ x ∈ A, f(x) = x246proof247  refine ⟨latticeLeastFixed(f, A, r), (latticeLeastFixed.member at f, A,248      r with complete), (latticeLeastFixed.fixed with complete, monotone)⟩249250theorem latticeFixedPoints.nonempty (f A r : Set)251  requires complete : IsCompleteLattice(A, r)252  requires monotone : IsMonotoneMap(f, A, r, A, r)253  shows Nonempty(latticeFixedPoints(f, A))254proof255  have least := latticeLeastFixed.least_fixed with complete, monotone256  refine ⟨latticeLeastFixed(f, A, r), Least.member with least⟩257258theorem latticeLeastFixed.le_greatest (f A r : Set)259  requires complete : IsCompleteLattice(A, r)260  requires monotone : IsMonotoneMap(f, A, r, A, r)261  shows relates(r, latticeLeastFixed(f, A, r), latticeGreatestFixed(f, A, r))262proof263  have greatestA := latticeGreatestFixed.member at f, A, r with complete264  have fixed := latticeGreatestFixed.fixed with complete, monotone265  exact latticeLeastFixed.least with complete, greatestA, fixed266267theorem latticeFixedPoints.unique_of_eq (f A r : Set)268  requires complete : IsCompleteLattice(A, r)269  requires monotone : IsMonotoneMap(f, A, r, A, r)270  requires same : latticeLeastFixed(f, A, r) = latticeGreatestFixed(f, A, r)271  shows ∀ x ∈ A, f(x) = x → x = latticeLeastFixed(f, A, r)272proof273  have antisymmetric := IsPartialOrder.antisymmetric with274      (IsCompleteLattice.order with complete)275  have leastA := latticeLeastFixed.member at f, A, r with complete276  intros x hx fixed277  have below := latticeLeastFixed.least with complete, hx, fixed278  have above := latticeGreatestFixed.greatest with complete, hx, fixed279  rw ← same at above280  exact antisymmetric with x, hx, latticeLeastFixed(f, A, r), leastA, above,281      below282