fixed point theorems

1 files changed, 46 insertions, 0 deletions

diff --git a/SymbolicModalLogic/FixedPoints.lean b/SymbolicModalLogic/FixedPoints.lean
new file mode 100644
index 0000000..2074992
--- /dev/null
+++ b/SymbolicModalLogic/FixedPoints.lean
@@ -0,0 +1,46 @@
+import Mathlib
+
+namespace FixedPoints
+
+variable {α : Type} [CompleteLattice α]
+
+def lfp (f : α → α) : α := sInf { x | f x ≤ x }
+
+def gfp (f : α → α) : α := sSup { x | x ≤ f x }
+
+lemma lfp_isFixedPt (f : α → α) (h : Monotone f) : Function.IsFixedPt f (lfp f) := by
+  have hmem : f (lfp f) ≤ lfp f := by
+    rw [lfp, le_sInf_iff]
+    intro x hx
+    grw [h (sInf_le hx)]
+    exact hx
+  apply Std.IsPartialOrder.le_antisymm
+  · exact hmem
+  · exact (sInf_le (h hmem))
+
+lemma lfp_is_least (f : α → α) :
+    ∀ x, Function.IsFixedPt f x → lfp f ≤ x := by
+  intro x hfix
+  apply sInf_le
+  simp [show f x = x from hfix]
+
+-- TODO: Avoid repitition
+
+lemma gfp_isFixedPt (f : α → α) (h : Monotone f) : Function.IsFixedPt f (gfp f) := by
+  have hmem : gfp f ≤ f (gfp f) := by
+    rw [gfp, sSup_le_iff]
+    intro x hx
+    grw [show x ≤ f x from hx]
+    exact h (le_sSup hx)
+  apply Std.IsPartialOrder.le_antisymm
+  · apply le_sSup
+    exact h hmem
+  · exact hmem
+
+lemma gfp_is_greatest (f : α → α) :
+    ∀ x, Function.IsFixedPt f x → x ≤ gfp f := by
+  intro x hfix
+  apply le_sSup
+  simp [show f x = x from hfix]
+
+end FixedPoints