第30章：領域理論・連続写像・再帰方程式#

namespace FormalLab.Recursion.DomainTheory

universe u v

structure OmegaChain {D : Type u} (le : D → D → Prop) where
  term : Nat → D
  increasing : ∀ n, le (term n) (term (n + 1))

structure PointedOmegaCPO (D : Type u) where
  le : D → D → Prop
  refl : ∀ x, le x x
  trans : ∀ {x y z}, le x y → le y z → le x z
  antisymm : ∀ {x y}, le x y → le y x → x = y
  bottom : D
  bottom_le : ∀ x, le bottom x
  supremum : OmegaChain le → D
  le_supremum : ∀ (chain : OmegaChain le) n, le (chain.term n) (supremum chain)
  supremum_le : ∀ (chain : OmegaChain le) upper,
    (∀ n, le (chain.term n) upper) → le (supremum chain) upper

def mapChain {D : Type u} {E : Type v}
    (source : PointedOmegaCPO D) (target : PointedOmegaCPO E)
    (f : D → E)
    (monotone : ∀ {x y}, source.le x y → target.le (f x) (f y))
    (chain : OmegaChain source.le) : OmegaChain target.le where
  term n := f (chain.term n)
  increasing n := monotone (chain.increasing n)

structure ScottContinuous {D : Type u} (domain : PointedOmegaCPO D) (f : D → D) where
  monotone : ∀ {x y}, domain.le x y → domain.le (f x) (f y)
  preservesSupremum : ∀ chain : OmegaChain domain.le,
    f (domain.supremum chain) =
      domain.supremum (mapChain domain domain f monotone chain)

def approximant {D : Type u} (domain : PointedOmegaCPO D) (f : D → D) : Nat → D
  | 0 => domain.bottom
  | n + 1 => f (approximant domain f n)

theorem approximantIncreasing {D : Type u} (domain : PointedOmegaCPO D) (f : D → D)
    (monotone : ∀ {x y}, domain.le x y → domain.le (f x) (f y)) :
    ∀ n, domain.le (approximant domain f n) (approximant domain f (n + 1)) := by
  intro n
  induction n with
  | zero => exact domain.bottom_le _
  | succ n hypothesis => exact monotone hypothesis

def approximationChain {D : Type u} (domain : PointedOmegaCPO D) (f : D → D)
    (monotone : ∀ {x y}, domain.le x y → domain.le (f x) (f y)) :
    OmegaChain domain.le where
  term := approximant domain f
  increasing := approximantIncreasing domain f monotone

def kleeneFixedPoint {D : Type u} (domain : PointedOmegaCPO D) (f : D → D)
    (continuous : ScottContinuous domain f) : D :=
  domain.supremum (approximationChain domain f continuous.monotone)

theorem kleene_is_fixed {D : Type u} (domain : PointedOmegaCPO D) (f : D → D)
    (continuous : ScottContinuous domain f) :
    f (kleeneFixedPoint domain f continuous) = kleeneFixedPoint domain f continuous := by
  unfold kleeneFixedPoint
  rw [continuous.preservesSupremum]
  apply domain.antisymm
  · apply domain.supremum_le
    intro n
    exact domain.le_supremum
      (approximationChain domain f continuous.monotone) (n + 1)
  · apply domain.supremum_le
    intro n
    cases n with
    | zero => exact domain.bottom_le _
    | succ n =>
        exact domain.le_supremum
          (mapChain domain domain f continuous.monotone
            (approximationChain domain f continuous.monotone)) n

theorem approximantBelowPrefixpoint {D : Type u} (domain : PointedOmegaCPO D)
    (f : D → D) (continuous : ScottContinuous domain f) {upper : D}
    (preFixed : domain.le (f upper) upper) :
    ∀ n, domain.le (approximant domain f n) upper := by
  intro n
  induction n with
  | zero => exact domain.bottom_le upper
  | succ n hypothesis =>
      exact domain.trans (continuous.monotone hypothesis) preFixed

theorem kleene_least_prefixpoint {D : Type u} (domain : PointedOmegaCPO D)
    (f : D → D) (continuous : ScottContinuous domain f) {upper : D}
    (preFixed : domain.le (f upper) upper) :
    domain.le (kleeneFixedPoint domain f continuous) upper := by
  apply domain.supremum_le
  exact approximantBelowPrefixpoint domain f continuous preFixed

def FlatLe {A : Type u} : Option A → Option A → Prop
  | none, _ => True
  | some left, some right => left = right
  | some _, none => False

theorem flat_refl {A : Type u} (x : Option A) : FlatLe x x := by
  cases x <;> simp [FlatLe]

theorem flat_trans {A : Type u} {x y z : Option A} :
    FlatLe x y → FlatLe y z → FlatLe x z := by
  cases x <;> cases y <;> cases z <;> simp [FlatLe]
  intro equal₁ equal₂
  exact equal₁.trans equal₂

theorem flat_antisymm {A : Type u} {x y : Option A} :
    FlatLe x y → FlatLe y x → x = y := by
  cases x <;> cases y <;> simp [FlatLe]
  intro equal _
  cases equal
  rfl

def partialMap {A : Type u} {B : Type v} (f : A → B) : Option A → Option B
  | none => none
  | some value => some (f value)

theorem partialMapMonotone {A : Type u} {B : Type v} (f : A → B)
    {x y : Option A} (information : FlatLe x y) :
    FlatLe (partialMap f x) (partialMap f y) := by
  cases x <;> cases y <;> simp [FlatLe, partialMap] at information ⊢
  cases information
  rfl

def factorialApproximation : Nat → Nat → Option Nat
  | 0, _ => none
  | _ + 1, 0 => some 1
  | fuel + 1, n + 1 =>
      partialMap (fun result => (n + 1) * result) (factorialApproximation fuel n)

theorem factorialApproximation_insufficient : factorialApproximation 3 3 = none := rfl

theorem factorialApproximation_sufficient : factorialApproximation 4 3 = some 6 := rfl