refactoring

1 files changed, 39 insertions, 34 deletions

diff --git a/SymbolicModalLogic/FixedPoints.lean b/SymbolicModalLogic/FixedPoints.lean
index 2074992..58d768c 100644
--- a/SymbolicModalLogic/FixedPoints.lean
+++ b/SymbolicModalLogic/FixedPoints.lean
@@ -1,46 +1,51 @@
 import Mathlib
 
-namespace FixedPoints
-
 variable {α : Type} [CompleteLattice α]
 
-def lfp (f : α → α) : α := sInf { x | f x ≤ x }
+structure Function.IsLeastFixedPt (f : α → α) (x : α) : Prop where
+  fixedPt : Function.IsFixedPt f x
+  least : ∀ y, Function.IsFixedPt f y → x ≤ y
 
-def gfp (f : α → α) : α := sSup { x | x ≤ f x }
+structure Function.IsGreatestFixedPt (f : α → α) (x : α) : Prop where
+  fixedPt : Function.IsFixedPt f x
+  greatest : ∀ y, Function.IsFixedPt f y → y ≤ 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))
+namespace FixedPoints
 
-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]
+def lfp (f : α → α) : α := sInf { x | f x ≤ x }
 
--- TODO: Avoid repitition
+def gfp (f : α → α) : α := sSup { x | x ≤ f x }
 
-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 lfp_isLeastFixedPt (f : α → α) (hf : Monotone f) : Function.IsLeastFixedPt f (lfp f) where
+  fixedPt := by
+    have hmem : f (lfp f) ≤ lfp f := by
+      rw [lfp, le_sInf_iff]
+      intro x hx
+      grw [hf (sInf_le hx)]
+      exact hx
+    apply Std.IsPartialOrder.le_antisymm
+    · exact hmem
+    · exact (sInf_le (hf hmem))
+  least := by
+    intro x hfix
+    apply sInf_le
+    simp [show f x = x from hfix]
 
-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]
+-- TODO: Avoid repitition
+lemma gfp_isGreatestFixedPt (f : α → α) (hf : Monotone f) : Function.IsGreatestFixedPt f (gfp f) where
+  fixedPt := 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 hf (le_sSup hx)
+    apply Std.IsPartialOrder.le_antisymm
+    · apply le_sSup
+      exact hf hmem
+    · exact hmem
+  greatest := by
+    intro x hfix
+    apply le_sSup
+    simp [show f x = x from hfix]
 
 end FixedPoints