{-# OPTIONS --cubical #-}
module Interpretations.CnfToBrw.Properties where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as Sum
open import Cubical.Data.Empty as ⊥
open import Cubical.Relation.Nullary
open import Cubical.Data.Nat as N
using (ℕ ; suc ; injSuc)
open import Cubical.Data.Nat.Order as N using ()
open import Cubical.Data.Bool
renaming (false to ff; true to tt)
open import PropTrunc
open import General-Properties
open import CantorNormalForm.Base as C
open import CantorNormalForm.Wellfoundedness as C
open import CantorNormalForm.Classifiability as C
open import CantorNormalForm.Addition as C
open import CantorNormalForm.Multiplication as C hiding (_·_)
open import CantorNormalForm.Subtraction as C
open import CantorNormalForm.LimitsAndTaboos
open import BrouwerTree.Base as B
open import BrouwerTree.Properties as B
open import BrouwerTree.Arithmetic as B
open import BrouwerTree.Arithmetic.Properties as B
open import BrouwerTree.Code.Results as B
open import BrouwerTree.Decidability
open import BrouwerTree.Decidability.Finite
open import Interpretations.CnfToBrw
open import BooleanSequence
open import Simulations Cnf C._≤_
CtoB-preserves-limits→MP :
(∀ {lf} f → (f↑ : is-<-increasing f) → lf C.is-lim-of (f , f↑) →
CtoB lf ≡ limit (CtoB ∘ f) {CtoB-preserves-increasing f↑}) → MP
CtoB-preserves-limits→MP hyp s ¬¬p = least-witness (λ n → s n ≡ tt)
(λ n → isSetBool (s n) tt)
(λ n → s n ≟ tt)
goal
where
¬s≡ff : ¬ (∀ i → s i ≡ ff)
¬s≡ff p = ¬¬p (λ { (n , sn=tt) → true≢false (sym sn=tt ∙ p n) })
ω+ω-min-over-s↑ : (c : Cnf) → (∀ i → (s ↑) i C.≤ c) → C.ω C.+ C.ω C.≤ c
ω+ω-min-over-s↑ c s≤c = ≮→≥ ¬c<ω+ω
where
¬c<ω+ω : ¬ (c C.< C.ω C.+ C.ω)
¬c<ω+ω c<ω+ω = let (n , c≤ω+n) = x<ω+ω→x≤ω+n c c<ω+ω
in ¬s≡ff (s↑-spec-<ω-back s n (λ i → C.≤-trans (s≤c i) c≤ω+n))
lim⟨s↑⟩=ω+ω : (C.ω C.+ C.ω) is-lim-of (s ↑ , s↑-inc s)
lim⟨s↑⟩=ω+ω = ((λ i → inl (s↑-bounded-by-ω+ω s i)) , ω+ω-min-over-s↑)
preserved-limit : limit (CtoB ∘ (s ↑)) ≡ B.ω B.+ B.ω
preserved-limit = sym (hyp (s ↑) (s↑-inc s) lim⟨s↑⟩=ω+ω)
∙ limit-pointwise-equal (λ n → ω^ (ω^ zero) B.+ one · ι n)
(λ n → B.ω B.+ ι n)
(λ n → cong₂ B._+_ B.ω^one≡ω (B.one·y≡y (ι n)))
shifted-preserved-limit : limit (λ n → CtoB ((s ↑) (suc n))) {λ k → CtoB-preserves-increasing (s↑-inc s) (suc k)} ≡ B.ω B.+ B.ω
shifted-preserved-limit = limit-pointwise-equal (λ n → CtoB ((s ↑) (suc n)))
(λ n → CtoB ((s ↑) (n N.+ 1)))
(λ n → cong (CtoB ∘ (s ↑)) (cong suc (sym (N.+-zero n)) ∙ sym (N.+-suc n 0)))
∙ sym (limit-drop-initial 1 (λ n → CtoB ((s ↑) n)))
∙ preserved-limit
index-found : ∥ Σ[ n ∈ ℕ ] B.ω B.< CtoB ((s ↑) (suc n)) ∥
index-found = below-limit-lemma B.ω (λ n → CtoB ((s ↑) (suc n))) (subst (B.ω B.<_) (sym shifted-preserved-limit) ω<ω+ω)
goal : ∥ Σ[ n ∈ ℕ ] s n ≡ tt ∥
goal = ∥-∥map (λ (n , p) → map-snd snd (s↑-spec->ω-back s n (CtoB-reflects-< (subst (λ z → z B.< CtoB ((s ↑) (suc n))) (sym ω^one≡ω) p)))) index-found
MP→CtoB-preserves-limits : MP →
(∀ {lf} f → (f↑ : is-<-increasing f) → lf C.is-lim-of (f , f↑) →
CtoB lf ≡ limit (CtoB ∘ f) {CtoB-preserves-increasing f↑})
MP→CtoB-preserves-limits mp {x} f f↑ xlimf = goal
where
islim-x : is-lim x
islim-x = ∣ (f , f↑) , xlimf ∣
x>0 : x > 𝟎
x>0 = lim>𝟎 islim-x
x-not-suc : ¬ (is-strong-suc x)
x-not-suc = lim-is-not-suc islim-x
g : ℕ → Cnf
g = fund-sequence x islim-x
g↑ : is-<-increasing g
g↑ = fund-sequence↑ x islim-x
xlimg : x C.is-lim-of (g , g↑)
xlimg = fst (snd (snd (CtoB-preserves-FS x x>0 x-not-suc)))
CtoBx≡lCtoB⟨g⟩ : CtoB x ≡ limit (λ n → CtoB (g n)) {CtoB-preserves-increasing g↑}
CtoBx≡lCtoB⟨g⟩ = CtoB-preserves-fund-sequence x islim-x
f≲g : f simulated-by g
f≲g = MP→limits-unique mp f {f↑} g {g↑} C.≤-refl xlimf xlimg
g≲f : g simulated-by f
g≲f = MP→limits-unique mp g {g↑} f {f↑} C.≤-refl xlimg xlimf
lCtoB⟨f⟩≡lCtoB⟨g⟩ : limit (λ n → CtoB (f n)) {CtoB-preserves-increasing f↑} ≡ limit (λ n → CtoB (g n)) {CtoB-preserves-increasing g↑}
lCtoB⟨f⟩≡lCtoB⟨g⟩ = bisim _ _ ((λ k → ∥-∥map (map-snd CtoB-≤-monotone) (f≲g k)) , (λ k → ∥-∥map (map-snd CtoB-≤-monotone) (g≲f k)))
goal : CtoB x ≡ limit (CtoB ∘ f)
goal = CtoBx≡lCtoB⟨g⟩ ∙ sym lCtoB⟨f⟩≡lCtoB⟨g⟩