第79章：再帰型の意味論——構文・近似・関手不動点を接続する#

namespace FormalLab.Bridges.RecursiveTypeSemantics

open _root_.CategoryTheory
open _root_.CategoryTheory.Endofunctor
open _root_.CategoryTheory.Limits
open FormalLab.TypeTheory.RecursiveTypes
open FormalLab.Recursion.DomainTheory
open FormalLab.CategoryFoundations.InitialAlgebras

universe u

example : unfoldType natBody = .sum .unit recursiveNat := rfl

example : recursiveNat ≠ .sum .unit recursiveNat := by decide

structure FixedObject (F : Type u ⥤ Type u) where
  carrier : Type u
  roll : F.obj carrier → carrier
  unroll : carrier → F.obj carrier
  roll_unroll : ∀ value, roll (unroll value) = value
  unroll_roll : ∀ layer, unroll (roll layer) = layer

def FixedObject.algebra {F : Type u ⥤ Type u} (D : FixedObject F) : Algebra F where
  a := D.carrier
  str := ↾D.roll

def FixedObject.coalgebra {F : Type u ⥤ Type u} (D : FixedObject F) : Coalgebra F where
  V := D.carrier
  str := ↾D.unroll

def natUnroll : Nat → Unit ⊕ Nat
  | 0 => .inl ()
  | n + 1 => .inr n

def natFixedObject : FixedObject onePlusFunctor where
  carrier := Nat
  roll := natStructure
  unroll := natUnroll
  roll_unroll value := by cases value <;> rfl
  unroll_roll layer := by
    cases layer with
    | inl inhabitant => cases inhabitant; rfl
    | inr n => rfl

example (n : Nat) : natFixedObject.roll (natFixedObject.unroll n) = n :=
  natFixedObject.roll_unroll n

example (layer : Unit ⊕ Nat) :
    natFixedObject.unroll (natFixedObject.roll layer) = layer :=
  natFixedObject.unroll_roll layer

example : IsInitial natFixedObject.algebra := natIsInitial

def OnePlusStage : Nat → Type
  | 0 => Empty
  | n + 1 => Unit ⊕ OnePlusStage n

def includeStage : {n : Nat} → OnePlusStage n → OnePlusStage (n + 1)
  | 0, value => nomatch value
  | _ + 1, .inl inhabitant => .inl inhabitant
  | n + 1, .inr value => .inr (includeStage (n := n) value)

def stageValue : {n : Nat} → OnePlusStage n → Nat
  | 0, value => nomatch value
  | _ + 1, .inl _ => 0
  | _ + 1, .inr value => stageValue value + 1

theorem includeStage_preserves_value {n : Nat} (value : OnePlusStage n) :
    stageValue (includeStage value) = stageValue value := by
  induction n with
  | zero => exact Empty.elim value
  | succ n ih =>
      cases value with
      | inl inhabitant => rfl
      | inr rest =>
          simp only [includeStage, stageValue]
          rw [ih rest]

def natAtStage : (n : Nat) → OnePlusStage (n + 1)
  | 0 => .inl ()
  | n + 1 => .inr (natAtStage n)

theorem natAtStage_value (n : Nat) : stageValue (natAtStage n) = n := by
  induction n with
  | zero => rfl
  | succ n ih => simp [natAtStage, stageValue, ih]

example {D : Type u} (domain : PointedOmegaCPO D) (f : D → D)
    (continuous : ScottContinuous domain f) :
    f (kleeneFixedPoint domain f continuous) = kleeneFixedPoint domain f continuous :=
  kleene_is_fixed domain f continuous

def delayedValue (steps value fuel : Nat) : Option Nat :=
  if steps < fuel then some value else none

theorem delayedValue_increasing (steps value fuel : Nat) :
    FlatLe (delayedValue steps value fuel) (delayedValue steps value (fuel + 1)) := by
  by_cases current : steps < fuel
  · have next : steps < fuel + 1 := by omega
    simp [delayedValue, current, next, FlatLe]
  · by_cases next : steps < fuel + 1
    · simp [delayedValue, current, next, FlatLe]
    · simp [delayedValue, current, next, FlatLe]

example (steps value : Nat) : delayedValue steps value (steps + 1) = some value := by
  simp [delayedValue]

theorem delayedValue_before (steps value fuel : Nat) (early : fuel ≤ steps) :
    delayedValue steps value fuel = none := by
  simp [delayedValue, Nat.not_lt.mpr early]

def predicatePullback {X Y : Type u} (f : X → Y) : (Y → Bool) → (X → Bool) :=
  fun predicate x => predicate (f x)

theorem predicatePullback_id {X : Type u} :
    predicatePullback (fun x : X => x) = id := rfl

theorem predicatePullback_comp {X Y Z : Type u} (f : X → Y) (g : Y → Z) :
    predicatePullback (g ∘ f) = predicatePullback f ∘ predicatePullback g := rfl

def AlgebraicallyCompleteFor (F : Type u ⥤ Type u) : Prop :=
  Nonempty (Σ A : Algebra F, IsInitial A)

structure AlgebraicallyCompactSolution (F : Type u ⥤ Type u) where
  fixed : FixedObject F
  initial : IsInitial fixed.algebra
  terminal : IsTerminal fixed.coalgebra

theorem compact_is_complete {F : Type u ⥤ Type u}
    (solution : AlgebraicallyCompactSolution F) : AlgebraicallyCompleteFor F :=
  ⟨⟨solution.fixed.algebra, solution.initial⟩⟩

example : AlgebraicallyCompleteFor onePlusFunctor.{0} :=
  ⟨⟨natAlgebra, natIsInitial⟩⟩

def loopingCoalgebra : Coalgebra onePlusFunctor where
  V := Unit
  str := ↾fun _ => Sum.inr ()

theorem natUnroll_ne_self_inr (n : Nat) : natUnroll n ≠ Sum.inr n := by
  cases n <;> simp [natUnroll]

theorem no_loop_to_nat (f : loopingCoalgebra ⟶ natFixedObject.coalgebra) : False := by
  have preservation := types_congr_hom f.h ()
  exact natUnroll_ne_self_inr (f.f ()) preservation.symm

theorem natFixed_not_terminal : IsEmpty (IsTerminal natFixedObject.coalgebra) :=
  ⟨fun terminal => no_loop_to_nat (terminal.from loopingCoalgebra)⟩