Instantly share code, notes, and snippets.

# jcreedcmu/chaotic.agda

Last active March 18, 2024 00:09
Show Gist options
• Save jcreedcmu/711fb5a38cdfb29fc7882f82038db325 to your computer and use it in GitHub Desktop.
proof of correctness of chaotic iteration
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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))

### jcreedcmu commented Mar 17, 2024 • edited

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*:
∀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ₜ
∎
``````