第69章：無限の三つの意味——基数・尽きない観察・無限図式#

namespace FormalLab.Bridges.ThreeNotionsOfInfinity

open _root_.CategoryTheory
open FormalLab.Mathematics.FunctionProperties
open FormalLab.Mathematics.Cardinality
open FormalLab.Recursion.CoinductivePredicates
open FormalLab.CategoryFoundations.FinalCoalgebras
open FormalLab.Bridges.CoinductionAndFinalCoalgebras

universe u

theorem natCountablyInfinite : CountablyInfinite Nat := by
  refine ⟨id, ?_⟩
  exact ⟨fun _ _ h => h, fun n => ⟨n, rfl⟩⟩

example : CountablyInfinite EvenNat := evenCountablyInfinite

theorem boolStreamsNotEnumeratedByNat :
    ¬ ∃ table : Nat → (Nat → Bool), IsSurjective table :=
  noSurjectionToBoolPowers

def toggleMachine : _root_.CategoryTheory.Endofunctor.Coalgebra
    (streamFunctor Bool) where
  V := Bool
  str := ↾fun state => (state, !state)

def alternating (initial : Bool) : Nat → Bool :=
  unfold toggleMachine initial

example : alternating false 0 = false := rfl
example : alternating false 1 = true := rfl
example : alternating false 2 = false := rfl
example : alternating false 3 = true := rfl

def finitePrefix {A : Type u} : Nat → (Nat → A) → List A
  | 0, _ => []
  | n + 1, stream => stream 0 :: finitePrefix n (fun k => stream (k + 1))

theorem finitePrefix_length {A : Type u} (n : Nat) (stream : Nat → A) :
    (finitePrefix n stream).length = n := by
  induction n generalizing stream with
  | zero => rfl
  | succ n ih => simp [finitePrefix, ih]

#eval finitePrefix 8 (alternating false)

def invisibleNatMachine : _root_.CategoryTheory.Endofunctor.Coalgebra
    (streamFunctor Unit) where
  V := Nat
  str := ↾fun n => ((), n + 1)

theorem invisibleNatMachine_same_behavior (left right : Nat) :
    unfold invisibleNatMachine left = unfold invisibleNatMachine right := by
  funext n
  exact Subsingleton.elim _ _

example (left right : Nat) :
    Bisimilar (observe invisibleNatMachine) (observe invisibleNatMachine)
      (next invisibleNatMachine) (next invisibleNatMachine) (left, right) :=
  bisimilar_of_behaviorallyEqual invisibleNatMachine
    (invisibleNatMachine_same_behavior left right)

structure InverseSequence where
  obj : Nat → Type u
  restrict : ∀ n, obj (n + 1) → obj n

def CompatibleThread (D : InverseSequence.{u}) :=
  {values : ∀ n, D.obj n // ∀ n, D.restrict n (values (n + 1)) = values n}

structure SequenceCone (D : InverseSequence.{u}) (X : Type u) where
  leg : ∀ n, X → D.obj n
  compatible : ∀ n x, D.restrict n (leg (n + 1) x) = leg n x

def threadProjection (D : InverseSequence.{u}) (n : Nat) :
    CompatibleThread D → D.obj n :=
  fun thread => thread.1 n

def threadLift {D : InverseSequence.{u}} {X : Type u}
    (cone : SequenceCone D X) : X → CompatibleThread D :=
  fun x => ⟨fun n => cone.leg n x, fun n => cone.compatible n x⟩

theorem threadLift_fac {D : InverseSequence.{u}} {X : Type u}
    (cone : SequenceCone D X) (n : Nat) :
    threadProjection D n ∘ threadLift cone = cone.leg n := rfl

theorem threadLift_unique {D : InverseSequence.{u}} {X : Type u}
    (cone : SequenceCone D X) (candidate : X → CompatibleThread D)
    (fac : ∀ n, threadProjection D n ∘ candidate = cone.leg n) :
    candidate = threadLift cone := by
  funext x
  apply Subtype.ext
  funext n
  exact congrFun (fac n) x

def unitSequence : InverseSequence where
  obj _ := Unit
  restrict _ := id

theorem unitSequence_thread_unique (left right : CompatibleThread unitSequence) :
    left = right := by
  apply Subtype.ext
  funext n
  change left.1 n = right.1 n
  exact Unit.ext _ _

def boolPrefixSequence : InverseSequence where
  obj n := Fin n → Bool
  restrict _ longer := fun position => longer position.castSucc

def streamToThread (stream : Nat → Bool) : CompatibleThread boolPrefixSequence :=
  ⟨fun _ position => stream position.val, by
    intro n
    rfl⟩

def threadToStream (thread : CompatibleThread boolPrefixSequence) : Nat → Bool :=
  fun n => thread.1 (n + 1) ⟨n, Nat.lt_add_one n⟩

theorem threadToStream_streamToThread (stream : Nat → Bool) :
    threadToStream (streamToThread stream) = stream := by
  funext n
  rfl