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

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,47 @@ theorem fix_eq_of_ωScottContinuous (hc : ωScottContinuous g) :
     intro i
     exists i.succ
 
+/-- `Part.fix g` is the least fixed point of the ω-Scott continuous functional `g`. -/
+theorem fix_eq_lfp (hc : ωScottContinuous g) :
+    Part.fix g = ContinuousHom.lfp (.ofFun g hc) := by
+  have h : approxChain (⟨g, hc.monotone⟩ : (∀ a, Part (β a)) →o _) =
+      fixedPoints.iterateChain ⟨g, hc.monotone⟩ ⊥ bot_le := by
+    apply Chain.ext
+    funext n
+    change Fix.approx _ n = g^[n] ⊥
+    induction n with
+    | zero => rfl
+    | succ n ih =>
+      change g (Fix.approx _ n) = g^[n + 1] ⊥
+      rw [ih, ← Function.iterate_succ_apply' g n ⊥]
+  rw [fix_eq_ωSup_of_ωScottContinuous hc]
+  change _ = ωSup _
+  rw [h]
+  rfl
+
+/-- **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_lfp hc]
+  exact ContinuousHom.lfp_induction _ h_bot h_step h_sup
+
+/-- Induction on membership in `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_induction_mem {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
@@ -806,6 +807,24 @@ open Function
 def iterateChain (f : α →o α) (x : α) (h : x ≤ f x) : Chain α :=
   ⟨fun n => f^[n] x, f.monotone.monotone_iterate_of_le_map h⟩
 
+/-- **Scott induction** from a seed `x ≤ f x`: if `p` holds at `x`, is preserved by the monotone
+function `f`, and is closed under `ωSup` of chains, then `p` holds at the supremum of the iterate
+chain `x, f x, f (f x), …`. The textbook Scott induction is the special case `x := ⊥`, see
+`ContinuousHom.lfp_induction`. -/
+theorem ωSup_iterate_induction {f : α →o α} {x : α} (h : x ≤ f x) {p : α → Prop}
+    (h_x : p x) (h_step : ∀ a, p a → p (f a))
+    (h_sup : ∀ c : Chain α, (∀ n, p (c n)) → p (ωSup c)) :
+    p (ωSup (iterateChain f x h)) := by
+  apply h_sup
+  intro n
+  induction n with
+  | zero => exact h_x
+  | succ k ih =>
+    have : iterateChain f x h (k + 1) = f (iterateChain f x h k) :=
+      Function.iterate_succ_apply' ..
+    rw [this]
+    exact h_step _ ih
+
 variable (f : α →𝒄 α) (x : α)
 
 /-- The supremum of iterating a function on x arbitrary often is a fixed point -/
@@ -856,4 +875,36 @@ theorem ωSup_iterate_le_fixedPoint (h : x ≤ f x) {a : α}
 
 end fixedPoints
 
+namespace ContinuousHom
+
+open Function fixedPoints
+
+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) :=
+  ωSup_iterate_induction bot_le h_bot h_step h_sup
+
+end ContinuousHom
+
 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},