proof of correctness of chaotic iteration

chaotic.agda

open import Agda.Primitive

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

infixr 4 _,_

module _
  (A : ℕ → Set)
  (B : ℕ → Set)
  (J : Set)
  (f : J → Set → Set)
  (f-cont : (j : J) → f j (Σ ℕ A) → Σ ℕ (λ t → f j (A t)))
  (f-mono : {X Y : Set} (g : X → Y) (j : J) → f j X → f j Y)
  (B/z : {X : Set} → B zero → X)
  (B/s : (t : ℕ) → B (succ t) → Σ J (λ j → f j (B t)))
  (A/fair : (j : J) → Σ ℕ (λ t → f j (A t)) → Σ ℕ A)
  where

  thm : (s : ℕ) (b : B s) → Σ ℕ A
  thm zero b = B/z b
  thm (succ s) b = let (j , x) = B/s s b in A/fair j (f-cont j (f-mono (thm s) j x))

This is approximately a formalization of the following argument:

Suppose (fⱼ)_{j∈J} is an J-indexed family of monotone continuous functions P → P.
Suppose we have two sequences aₜ, bₜ, satisfying:
    b₀ = ⊥
    bₛ₊₁ ≤ ⋃ⱼ fⱼ(bₛ)        (†)
("b is some sequence that doesn't grow any faster than concurrently applying all the rules")
and
    ∀n,s. fⱼ(aₛ) ≤ ⋃ₜ aₜ    (‡)
("a is what we get applying a fair sequence, and so it has the property that
if we hit any particular value aₛ with fⱼ, then there's some future stage where
      we pick fⱼ and exceed fⱼ(aₛ)")

then,
*Claim*: ⋃ₜ bₜ ≤ ⋃ₜ aₜ
*Proof*:
Start with the "fair sequence" assumption
    ∀n,s. fⱼ(aₛ) ≤ ⋃ₜ aₜ
Use definition of ⋃:
    ∀n. ⋃ₜ fⱼ(aₜ) ≤ ⋃ₜ aₜ
Use continuity of fⱼ:
    ∀n. fⱼ(⋃ₜ aₜ) ≤ ⋃ₜ aₜ
Use definition of ⋃:
    ⋃ⱼ fⱼ(⋃ₜ aₜ) ≤ ⋃ₜ aₜ                       (*)
Note that monotonicity of ⋃ⱼ fⱼ(—) means that
    bₛ ≤ ⋃ₜ aₜ ⇒ ⋃ⱼ fⱼ(bₛ) ≤ ⋃ⱼ fⱼ(⋃ₜ aₜ)    (**)
so by transitivity and (**) and (*) we get
    bₛ ≤ ⋃ₜ aₜ ⇒ ⋃ⱼ fⱼ(bₛ) ≤ ⋃ₜ aₜ            (***)
by transitivity and (†) and (***) we get
    bₛ ≤ ⋃ₜ aₜ ⇒ bₛ₊₁ ≤ ⋃ₜ aₜ
by induction, we have
    ∀s. bₛ ≤ ⋃ₜ aₜ
use the definition of ⋃ one last time to see
    ⋃ₜ bₜ ≤ ⋃ₜ aₜ
∎