IntervalObjectApproximation
Todd Waugh Ambridge, January 2024
# Interval object finite approximations
{-# OPTIONS --without-K --safe #-}
open import MLTT.Spartan
open import UF.FunExt
open import Naturals.Addition renaming (_+_ to _+ℕ_)
open import UF.Base
open import MLTT.SpartanList hiding (_∷_;⟨_⟩;[_])
open import TWA.Thesis.Chapter2.Vectors
open import TWA.Thesis.Chapter2.Sequences
open import TWA.Thesis.Chapter5.IntervalObject
module TWA.Thesis.Chapter5.IntervalObjectApproximation
(fe : FunExt)
(io : Interval-object fe 𝓤)
where
open basic-interval-object-development fe io hiding (−1 ; O ; +1)
first-_ : {A : 𝓥 ̇ } (n : ℕ) → (ℕ → A) → Vec A n
first- n = Seq-to-Vec n
append-one : {X : 𝓥 ̇ } {n : ℕ} → X → Vec X n → Vec X (succ n)
append-one {𝓥} {X} {0} y ⟨⟩ = y :: ⟨⟩
append-one {𝓥} {X} {succ n} y (x :: xs) = x :: append-one y xs
m : {n : ℕ} → Vec 𝕀 (succ n) → 𝕀
m {0} (x :: ⟨⟩) = x
m {succ n} (x :: xs) = x ⊕ m xs
n-approx : (x y : ℕ → 𝕀) (n : ℕ) → 𝓤 ̇
n-approx x y n = Σ (z , w) ꞉ 𝕀 × 𝕀
, m (append-one z ((first- n) x))
＝ m (append-one w ((first- n) y))
approximation : 𝓤 ̇
approximation = (x y : ℕ → 𝕀) → Π (n-approx x y) → M x ＝ M y
multi-canc : (w z : 𝕀) (y : ℕ → 𝕀) (n : ℕ)
→ m (append-one w ((first- n) y))
＝ m (append-one z ((first- n) y))
→ w ＝ z
multi-canc w .w y 0 refl = refl
multi-canc w z y (succ n) e
= multi-canc w z (y ∘ succ) n
(⊕-canc _ _ _ (⊕-comm _ _ ∙ e ∙ ⊕-comm _ _))
one-sided-approx : (x : 𝕀) (y : ℕ → 𝕀)
→ ((n : ℕ)
→ Σ w ꞉ 𝕀 , x ＝ m (append-one w ((first- n) y)))
→ x ＝ M y
one-sided-approx x y f = M-prop₂ ws y γ where
ws : ℕ → 𝕀
ws 0 = x
ws (succ i) = pr₁ (f (succ i))
γ : (i : ℕ) → ws i ＝ (y i ⊕ ws (succ i))
γ 0 = pr₂ (f 1)
γ (succ i) = multi-canc
(ws (succ i))
(y (succ i) ⊕ ws (succ (succ i)))
y
(succ i) (pr₂ (f (succ i)) ⁻¹
∙ (pr₂ (f (succ (succ i)))
∙ δ'' y (ws (succ (succ i))) i))
where
δ'' : (y : ℕ → 𝕀) (z : 𝕀) (i : ℕ)
→ m (append-one z ((first- (succ (succ i))) y))
＝ m (append-one (y (succ i) ⊕ z) ((first- (succ i)) y))
δ'' y z 0 = refl
δ'' y z (succ i) = ap (y 0 ⊕_) (δ'' (y ∘ succ) z i)
_++'_ : {n : ℕ} {X : 𝓤 ̇ } → Vec X n → (ℕ → X) → (ℕ → X)
_++'_ {n} {X} v α = Vec-to-Seq n α v
m-prop₁ : (n : ℕ) (a b c : ℕ → 𝕀) (e : 𝕀)
→ (m (append-one e ((first- succ n) a))
⊕ M ((first- n) b ++' λ i → (c (succ (i +ℕ n)))))
＝ M ((append-one (a n ⊕ e) ((first- n) λ i → a i ⊕ b i))
++' (λ i → c (succ (i +ℕ n))))
m-prop₁ 0 a b c e = M-prop₁ _ ⁻¹
m-prop₁ (succ n) a b c e
= ap ((a 0 ⊕ (a 1 ⊕ m (append-one e ((first- n) (a ∘ succ ∘ succ))))) ⊕_)
(M-prop₁ ((first- succ n) b ++' (λ i → c (succ (i +ℕ succ n)))))
∙ ⊕-tran _ _ _ _
∙ ap ((a 0 ⊕ b 0) ⊕_) (m-prop₁ n (tail a) (tail b) (tail c) e)
∙ M-prop₁ (append-one (a (succ n) ⊕ e)
((first- succ n) (λ i → a i ⊕ b i))
++' (λ i → c (succ (i +ℕ succ n)))) ⁻¹
M-append-＝ : (x : ℕ → 𝕀) (n : ℕ)
→ M x
＝ M (append-one (x n) ((first- n) x)
++' (λ i → x (succ (i +ℕ n))))
M-append-＝ x 0 = M-prop₁ x
∙ M-prop₁
(append-one (x 0) ((first- 0) x)
++' (λ i → x (succ (i +ℕ 0)))) ⁻¹
M-append-＝ x (succ n) = M-prop₁ x
∙ ap (x 0 ⊕_) (M-append-＝ (tail x) n)
∙ M-prop₁
(append-one (x (succ n)) ((first- succ n) x)
++' (λ i → x (succ (i +ℕ succ n)))) ⁻¹
M-append-++-＝ : (x y : ℕ → 𝕀) (n : ℕ)
→ M (λ i → x i ⊕ y i)
＝ (m (append-one (y n) ((first- succ n) x))
⊕ M (((first- n) y) ++' (λ i → (x (succ (i +ℕ n)))
⊕ (y (succ (i +ℕ n))))))
M-append-++-＝ x y n = M-append-＝ (λ i → x i ⊕ y i) n
∙ m-prop₁ n x y (λ i → x i ⊕ y i) (y n) ⁻¹
append-++-= : (x y : ℕ → 𝕀) (w : 𝕀) (n : ℕ)
→ ((append-one w ((first- n) x)) ++' y)
＝ (((first- n) x) ++' (w ∷ y))
append-++-= x y w 0 = dfunext (fe 𝓤₀ 𝓤) (ℕ-induction refl λ _ _ → refl)
append-++-= x y w (succ n) = dfunext (fe 𝓤₀ 𝓤) (ℕ-induction refl
(λ k _ → happly (append-++-= (tail x) y w n) k))
tail-_ : {X : 𝓤 ̇ } → ℕ → (ℕ → X) → (ℕ → X)
(tail- 0) α = α
(tail- succ n) α = tail ((tail- n) α)
M→m : (α : ℕ → 𝕀) (n : ℕ)
→ M α ＝ m (append-one (M ((tail- n) α)) ((first- n) α))
M→m α 0 = refl
M→m α (succ n) = M-prop₁ α
∙ ap (α 0 ⊕_)
(transport
(λ - → M (tail α)
＝ m (append-one (M -) ((first- n) (tail α))))
(γ α n) (M→m (tail α) n))
where
γ : (α : ℕ → 𝕀) (n : ℕ) → ((tail- n) (tail α)) ＝ ((tail- succ n) α)
γ α 0 = refl
γ α (succ n) = ap tail (γ α n)
tail-first' : {X : 𝓤 ̇ } {m : ℕ}
→ (a : Vec X (succ m)) (β : ℕ → X) (n : ℕ)
→ (tail- succ n) (a ++' β)
＝ (tail- n) (tl {𝓤} {m} {λ _ → X} a ++' β)
tail-first' {X} {m} (_ :: xs) β 0 = refl
tail-first' {X} {m} (_ :: xs) β (succ n)
= ap tail (tail-first' {X} {m} (_ :: xs) β n)
tail-first : {X : 𝓤 ̇ }
→ (α β : ℕ → X) (n : ℕ)
→ (tail- n) (((first- n) α) ++' β) ＝ β
tail-first α β 0 = refl
tail-first α β (succ n)
= tail-first' ((first- (succ n)) α) β n ∙ tail-first (tail α) β n
first-first : {X : 𝓤 ̇ }
→ (α β : ℕ → X) (n : ℕ)
→ ((first- n) ((first- n) α ++' β)) ＝ (first- n) α
first-first α β 0 = refl
first-first α β (succ n) = ap (α 0 ::_) (first-first (tail α) β n)
approx-holds : approximation
approx-holds x y f = ⊕-canc (M x) (M y) (M (tail z)) γ
where
z w : ℕ → 𝕀
z n = pr₁ (pr₁ (f n))
w n = pr₂ (pr₁ (f n))
w'' : (n : ℕ) → (ℕ → 𝕀)
w'' n = (y n ⊕ w (succ n))
∷ (λ i → x (succ (i +ℕ n))
⊕ z (succ (succ (i +ℕ n))))
γ'' : (n : ℕ) → m (append-one (z n) ((first- n) x))
＝ m (append-one (w n) ((first- n) y))
γ'' n = pr₂ (f n)
γ' : (n : ℕ) → Σ w* ꞉ 𝕀 , M (λ i → x i ⊕ (tail z) i)
＝ m (append-one w* ((first- n) (λ i → y i ⊕ (tail z) i)))
γ' n = M (w'' n)
, (M-append-++-＝ x (tail z) n
∙ ap (_⊕ M ((first- n) (tail z) ++' (λ i → x (succ (i +ℕ n))
⊕ tail z (succ (i +ℕ n)))))
(γ'' (succ n))
∙ m-prop₁ n y (tail z) (λ i → x i ⊕ (tail z) i) (w (succ n))
∙ ap M (append-++-= (λ i → y i ⊕ (tail z) i)
(λ i → x (succ (i +ℕ n)) ⊕ (tail z) (succ (i +ℕ n)))
(w'' n 0) n)
∙ M→m (((first- n) (λ i → y i ⊕ (tail z) i) ++' (w'' n))) n
∙ (ap (λ - → m (append-one (M -)
((first- n)
((first- n)
(λ i → y i ⊕ (tail z) i) ++' (w'' n)))))
(tail-first (λ i → y i ⊕ (tail z) i) (w'' n) n)
∙ ap (λ - → m (append-one (M (w'' n)) -))
(first-first (λ i → y i ⊕ (tail z) i) (w'' n) n)))
γ : (M x ⊕ M (z ∘ succ)) ＝ (M y ⊕ M (z ∘ succ))
γ = M-hom x (z ∘ succ)
∙ one-sided-approx
(M (λ i → x i ⊕ pr₁ (pr₁ (f (succ i)))))
(λ i → y i ⊕ z (succ i))
γ'
∙ M-hom y (z ∘ succ) ⁻¹
n-approx' : (ℕ → 𝕀) → (ℕ → 𝕀) → ℕ → 𝓤 ̇
n-approx' x y n = Σ (z , w) ꞉ 𝕀 × 𝕀
, m (append-one z ((first- (succ n)) x))
＝ m (append-one w ((first- (succ n)) y))
n-approx'→n-approx
: (x y : ℕ → 𝕀) → Π (n-approx' x y) → Π (n-approx x y)
n-approx'→n-approx x y f 0 = (u , u) , refl
n-approx'→n-approx x y f (succ n) = f n
fg-n-approx' : {X : 𝓥 ̇ } → (f g : X → ℕ → 𝕀) → ℕ → 𝓤 ⊔ 𝓥 ̇
fg-n-approx' f g n
= (∀ x → n-approx' (f x) (g x) n)
→ (∀ x → n-approx' (f x) (g x) (succ n))
fg-approx-holds : {X : 𝓥 ̇ } (f g : X → ℕ → 𝕀)
→ Π (fg-n-approx' f g)
→ ∀ x → M (f x) ＝ M (g x)
fg-approx-holds {_} {X} f g h x
= approx-holds (f x) (g x) (n-approx'→n-approx (f x) (g x) (γ x))
where
γ : (x : X) → Π (n-approx' (f x) (g x))
γ x 0 = (g x 0 , f x 0) , ⊕-comm _ _
γ x (succ n) = h n (λ y → γ y n) x
cancellation-holds : cancellative fe _⊕_
cancellation-holds a b c f = M-idem a ⁻¹ ∙ γ ∙ M-idem b
where
n-approx-c : (i : ℕ)
→ m (append-one c ((first- i) (λ _ → a)))
＝ m (append-one c ((first- i) (λ _ → b)))
n-approx-c 0 = refl
n-approx-c 1 = f
n-approx-c (succ (succ i))
= ( a ⊕ (a ⊕ wa)) ＝⟨ ap (_⊕ (a ⊕ wa)) (⊕-idem a ⁻¹) ⟩
((a ⊕ a) ⊕ (a ⊕ wa)) ＝⟨ ap ((a ⊕ a) ⊕_) (n-approx-c (succ i)) ⟩
((a ⊕ a) ⊕ (b ⊕ wb)) ＝⟨ ⊕-tran a a b wb ⟩
((a ⊕ b) ⊕ (a ⊕ wb)) ＝⟨ ap (λ - → (a ⊕ b) ⊕ (a ⊕ -)) (IH₂ ⁻¹) ⟩
((a ⊕ b) ⊕ (a ⊕ wa)) ＝⟨ ap ((a ⊕ b) ⊕_) (n-approx-c (succ i)) ⟩
((a ⊕ b) ⊕ (b ⊕ wb)) ＝⟨ ap (_⊕ (b ⊕ wb)) (⊕-comm a b) ⟩
((b ⊕ a) ⊕ (b ⊕ wb)) ＝⟨ ⊕-tran b a b wb ⟩
((b ⊕ b) ⊕ (a ⊕ wb)) ＝⟨ ap (λ - → (b ⊕ b) ⊕ (a ⊕ -)) (IH₂ ⁻¹) ⟩
((b ⊕ b) ⊕ (a ⊕ wa)) ＝⟨ ap ((b ⊕ b) ⊕_) (n-approx-c (succ i)) ⟩
((b ⊕ b) ⊕ (b ⊕ wb)) ＝⟨ ap (_⊕ (b ⊕ wb)) (⊕-idem b) ⟩
( b ⊕ (b ⊕ wb)) ∎
where
wa = m (append-one c ((first- i) (λ _ → a)) )
wb = m (append-one c ((first- i) (λ _ → b)))
IH₂ : wa ＝ wb
IH₂ = n-approx-c i
γ : M (λ _ → a) ＝ M (λ _ → b)
γ = approx-holds (λ _ → a) (λ _ → b) (λ i → (c , c) :: n-approx-c i)