feat(Order/OmegaCompletePartialOrder): least fixed point and Scott induction

Add `lfp` for ω-Scott continuous endofunctions on an ωCPO with `⊥`, defined
as the supremum of the iteration chain from `⊥`, together with its basic API
(`map_lfp`, `isFixedPt_lfp`, `lfp_le_fixed`, `isLeast_lfp`) and a Scott
induction principle `lfp_induction`.

Also add corresponding induction principles for `Part.fix`:
`fix_scott_induction` (ω-Scott continuous functional, admissible predicate)
and `fix_scott_induction_pointwise` (no continuity hypothesis, conclusion
of the form `Part.fix g x = some y → P x y`), supported by a helper
`exists_approx_eq_of_fix_eq_some`.

Author: tannerduve

Mathlib/Control/LawfulFix.lean

@@ -148,6 +148,15 @@ theorem fix_le {X : (a : _) → Part <| β a} (hX : f X ≤ X) : Part.fix f ≤
 
 variable {g : ((a : _) → Part <| β a) → (a : _) → Part <| β a}
 
+/-- If `y ∈ Part.fix g x`, then `y` is already in some finite approximation of `g` at `x`.
+The monotone analogue is `Part.Fix.mem_iff`. -/
+theorem exists_mem_approx_of_mem_fix {x} {y : β x}
+    (h : y ∈ Part.fix g x) : ∃ n, y ∈ Fix.approx g n x := by
+  by_cases h' : ∃ i, (Fix.approx g i x).Dom
+  · exact ⟨_, (Part.fix_def g h') ▸ h⟩
+  · rw [Part.fix_def' g h'] at h
+    exact absurd h (Part.notMem_none _)
+
 theorem fix_eq_ωSup_of_ωScottContinuous (hc : ωScottContinuous g) : Part.fix g =
     ωSup (approxChain (⟨g,hc.monotone⟩ : ((a : _) → Part <| β a) →o (a : _) → Part <| β a)) := by
   rw [← fix_eq_ωSup]
@@ -165,6 +174,33 @@ theorem fix_eq_of_ωScottContinuous (hc : ωScottContinuous g) :
     intro i
     exists i.succ
 
+/-- **Scott induction** for `Part.fix`: for an ω-Scott continuous functional `g` and a
+predicate `p` that holds at `⊥`, is preserved by `g`, and is closed under ωSup of chains,
+`p` holds at `Part.fix g`. -/
+theorem fix_scott_induction {p : (∀ a, Part (β a)) → Prop} (hc : ωScottContinuous g)
+    (h_bot : p ⊥) (h_step : ∀ f, p f → p (g f))
+    (h_sup : ∀ c : Chain (∀ a, Part (β a)), (∀ n, p (c n)) → p (ωSup c)) :
+    p (Part.fix g) := by
+  rw [fix_eq_ωSup_of_ωScottContinuous hc]
+  apply h_sup
+  intro n
+  induction n with
+  | zero => exact h_bot
+  | succ k ih => exact h_step _ ih
+
+/-- Pointwise Scott induction for `Part.fix`: to prove `P x y` whenever `y ∈ Part.fix g x`,
+it suffices that for any approximation `f` on which `P` holds pointwise, `g f` still satisfies
+`P` pointwise. No continuity hypothesis is needed. -/
+theorem fix_scott_induction_pointwise {P : ∀ a, β a → Prop}
+    (h_step : ∀ f, (∀ x y, y ∈ f x → P x y) → ∀ x y, y ∈ g f x → P x y)
+    {x} {y : β x} (h : y ∈ Part.fix g x) : P x y := by
+  obtain ⟨n, hn⟩ := exists_mem_approx_of_mem_fix h
+  suffices key : ∀ n x (y : β x), y ∈ Fix.approx g n x → P x y from key _ _ _ hn
+  intro n
+  induction n with
+  | zero => intro _ _ hh; exact absurd hh (Part.notMem_none _)
+  | succ _ ih => exact h_step _ ih
+
 end Part
 
 namespace Part

Mathlib/Order/OmegaCompletePartialOrder.lean

@@ -54,6 +54,7 @@ supremum helps define the meaning of recursive procedures.
 * [Chain-complete posets and directed sets with applications][markowsky1976]
 * [Recursive definitions of partial functions and their computations][cadiou1972]
 * [Semantics of Programming Languages: Structures and Techniques][gunter1992]
+* [Denotational Semantics][pitts2012denotational]
 -/
 
 @[expose] public section
@@ -854,6 +855,45 @@ theorem ωSup_iterate_le_fixedPoint (h : x ≤ f x) {a : α}
   obtain h_a := Eq.le h_a
   exact ωSup_iterate_le_prefixedPoint f x h h_a h_x_le_a
 
+section OrderBot
+
+variable [OrderBot α] (f : α →𝒄 α)
+
+/-- The least fixed point of an ω-Scott continuous function on an ω-complete partial order
+with a bottom element, defined as the supremum of the chain `⊥, f ⊥, f (f ⊥), …`. -/
+def lfp : α := ωSup (iterateChain f.toOrderHom ⊥ bot_le)
+
+/-- `lfp f` is a fixed point of `f`. -/
+theorem map_lfp : f (lfp f) = lfp f :=
+  ωSup_iterate_mem_fixedPoint f ⊥ bot_le
+
+theorem isFixedPt_lfp : IsFixedPt f (lfp f) := map_lfp f
+
+/-- `lfp f` is below every fixed point of `f`. -/
+theorem lfp_le_fixed {a : α} (h : f a = a) : lfp f ≤ a :=
+  ωSup_iterate_le_fixedPoint f ⊥ bot_le h bot_le
+
+/-- `lfp f` is the least fixed point of `f`. -/
+theorem isLeast_lfp : IsLeast (fixedPoints f) (lfp f) :=
+  ⟨isFixedPt_lfp f, fun _ ha => lfp_le_fixed f ha⟩
+
+/-- **Scott induction** for `lfp`: to prove a predicate `p` of `lfp f`, it suffices to show
+`p ⊥`, that `p` is preserved by `f`, and that `p` is closed under ωSup of chains. -/
+theorem lfp_induction {p : α → Prop} (h_bot : p ⊥) (h_step : ∀ a, p a → p (f a))
+    (h_sup : ∀ c : Chain α, (∀ n, p (c n)) → p (ωSup c)) : p (lfp f) := by
+  apply h_sup
+  intro n
+  induction n with
+  | zero => exact h_bot
+  | succ k ih =>
+    have hstep : iterateChain f.toOrderHom ⊥ bot_le (k + 1) =
+        f (iterateChain f.toOrderHom ⊥ bot_le k) :=
+      Function.iterate_succ_apply' ..
+    rw [hstep]
+    exact h_step _ ih
+
+end OrderBot
+
 end fixedPoints
 
 end OmegaCompletePartialOrder

docs/references.bib

@@ -4621,6 +4621,15 @@ @Book{            picado2012
   doi           = {10.1007/978-3-0348-0154-6}
 }
 
+@Misc{            pitts2012denotational,
+  title         = {Denotational Semantics},
+  author        = {Pitts, Andrew M.},
+  year          = {2012},
+  note          = {Lecture notes, Computer Laboratory, University of
+                  Cambridge},
+  url           = {https://www.cl.cam.ac.uk/teaching/1112/DenotSem/dens-notes-bw.pdf}
+}
+
 @Misc{            poeschel2017siegelsternberg,
   title         = {On the Siegel-Sternberg linearization theorem},
   author        = {Jürgen Pöschel},