```----------------------------------------------------------------------------------------------------
-- An order-preserving embedding from Cantor Normal Forms to Brouwer trees
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

module Interpretations.CnfToBrw where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Nat
using (ℕ ; zero ; suc ; +-comm)

open import CantorNormalForm.Everything as C
open import BrouwerTree.Everything as B

{- The interpretation -}

CtoB : Cnf → Brw
CtoB  𝟎               = zero
CtoB (ω^ a + b [ _ ]) = B.ω^ (CtoB a) B.+ CtoB b

{- CtoB is monotone wrt both < and ≤ -}

CtoB-monotone : {a b : Cnf} → a C.< b → CtoB a B.< CtoB b
CtoB-monotone  {𝟎}              {ω^ b + d [ s ]}  <₁
= B.≤-trans (B.zero<ω^c (CtoB b)) (B.x+-mono (B.≤-zero {CtoB d}))
CtoB-monotone {ω^ a + c [ r ]} {ω^ b + d [ s ]} (<₂ a<b)
= B.<∘≤-in-< (lemma (ω^ a + c [ r ]) a<b) (B.x+-mono (B.≤-zero {CtoB d}))
where
lemma : ∀ a {b} → left a C.< b → CtoB a B.< B.ω^ (CtoB b)
lemma  𝟎               {b} _   = B.zero<ω^c (CtoB b)
lemma (ω^ a + c [ r ]) {b} a<b =
additive-principal-ω^-closure {c = CtoB b} (B.ω^-mono-< (CtoB-monotone a<b))
(lemma c (C.≤∘<-in-< r a<b))
CtoB-monotone {ω^ a + c [ r ]} {ω^ b + d [ s ]} (<₃ a≡b c<d)
= B.<∘≤-in-< (B.x+-mono-< (CtoB-monotone c<d))
(≤-refl-≡ (cong (λ z → ω^ (CtoB z) B.+ CtoB d) a≡b))

CtoB-≤-monotone : {a b : Cnf} → a C.≤ b → CtoB a B.≤ CtoB b
CtoB-≤-monotone (inl a<b) = B.<-in-≤ (CtoB-monotone a<b)
CtoB-≤-monotone (inr b≡a) = ≤-refl-≡ (cong CtoB (sym b≡a))

{- CtoB reflects both < and ≤ -}

CtoB-reflects-< : {a b : Cnf} → CtoB a B.< CtoB b → a C.< b
CtoB-reflects-< {a} {b} Ba<Bb with <-tri a b
... | inl a<b = a<b
... | inr (inl b<a) = ⊥.rec (B.<-irreflexive (CtoB a) (B.<-trans _ _ _ Ba<Bb (CtoB-monotone b<a)))
... | inr (inr a≡b) = ⊥.rec (B.<-irreflexive (CtoB b) (subst (λ z → CtoB z B.< CtoB b) a≡b Ba<Bb))

CtoB-reflects-≤ : {a b : Cnf} → CtoB a B.≤ CtoB b → a C.≤ b
CtoB-reflects-≤ {a} {b} a≤b with <-tri a b
... | inl a<b = inl a<b
... | inr (inl b<a) = ⊥.rec (B.<-irreflexive _ (B.<∘≤-in-< (CtoB-monotone b<a) a≤b))
... | inr (inr a≡b) = inr (sym a≡b)

{- CtoB is injective -}

CtoB-injective : {a b : Cnf} → CtoB a ≡ CtoB b → a ≡ b
CtoB-injective p = C.≤-antisym (CtoB-reflects-≤ (B.≤-refl-≡ p))
(CtoB-reflects-≤ (B.≤-refl-≡ (sym p)))

{- CtoB preserves arithmetic operations -}

CtoB-preserves-suc : (a : Cnf) → CtoB (a C.+ 𝟏) ≡ B.succ (CtoB a)
CtoB-preserves-suc 𝟎 = refl
CtoB-preserves-suc (ω^ a + b [ r ]) with <-tri a 𝟎
... | inr _ =
ω^ (CtoB a) B.+ CtoB (b C.+ 𝟏)
≡⟨ cong (ω^ (CtoB a) B.+_) (CtoB-preserves-suc b) ⟩
ω^ (CtoB a) B.+ B.succ (CtoB b)
≡⟨ refl ⟩
B.succ (ω^ (CtoB a) B.+ CtoB b) ∎

CtoB-preserves-add : (a b : Cnf) → CtoB (a C.+ b) ≡ CtoB a B.+ CtoB b
CtoB-preserves-add  𝟎               (ω^ b + d [ s ]) = sym (zero+y≡y _)
CtoB-preserves-add (ω^ a + c [ r ])  𝟎               = refl
CtoB-preserves-add (ω^ a + c [ r ]) (ω^ b + d [ s ]) with <-tri a b
... | inl a<b =
ω^ (CtoB b) B.+ CtoB d
≡⟨ cong (B._+ CtoB d) (sym ω^a+ω^b≡ω^b) ⟩
(ω^ (CtoB a) B.+ ω^ (CtoB b)) B.+ CtoB d
≡⟨ sym (+-assoc (CtoB d)) ⟩
ω^ (CtoB a) B.+ ω^ (CtoB b) B.+ CtoB d
≡⟨ cong (λ z → _ B.+ z B.+ CtoB d) (sym c+ω^b≡ω^b) ⟩
ω^ (CtoB a) B.+ (CtoB c B.+ ω^ (CtoB b)) B.+ CtoB d
≡⟨ cong (ω^ (CtoB a) B.+_) (sym (+-assoc (CtoB d))) ⟩
ω^ (CtoB a) B.+ CtoB c B.+ ω^ (CtoB b) B.+ CtoB d
≡⟨ +-assoc (ω^ (CtoB b) B.+ CtoB d) ⟩
(ω^ (CtoB a) B.+ CtoB c) B.+ ω^ (CtoB b) B.+ CtoB d ∎
where
ω^a<ω^b : ω^ (CtoB a) B.< ω^ (CtoB b)
ω^a<ω^b = CtoB-monotone {ω^⟨ a ⟩} {ω^⟨ b ⟩} (<₂ a<b)
ω^a+ω^b≡ω^b : ω^ (CtoB a) B.+ ω^ (CtoB b) ≡ ω^ (CtoB b)
ω^a+ω^b≡ω^b = additive-principal-ω^ (CtoB b) _ ω^a<ω^b
c<ω^b : CtoB c B.< ω^ (CtoB b)
c<ω^b = CtoB-monotone {c} {ω^⟨ b ⟩} (<₂'' (C.≤∘<-in-< r a<b))
c+ω^b≡ω^b : CtoB c B.+ ω^ (CtoB b) ≡ ω^ (CtoB b)
c+ω^b≡ω^b = additive-principal-ω^ (CtoB b) _ c<ω^b
... | inr a≥b =
ω^ (CtoB a) B.+ CtoB (c C.+ ω^ b + d [ s ])
≡⟨ cong (ω^ (CtoB a) B.+_) (CtoB-preserves-add c (ω^ b + d [ s ])) ⟩
ω^ (CtoB a) B.+ CtoB c B.+ ω^ (CtoB b) B.+ CtoB d
≡⟨ +-assoc (ω^ (CtoB b) B.+ CtoB d) ⟩
(ω^ (CtoB a) B.+ CtoB c) B.+ ω^ (CtoB b) B.+ CtoB d ∎

private
NviaCtoB : ℕ → Brw
NviaCtoB n = CtoB (NtoC n)

NviaCtoB≡ι : (n : ℕ) → NviaCtoB n ≡ ι n
NviaCtoB≡ι zero = refl
NviaCtoB≡ι (suc n) = cong (one B.+_) (NviaCtoB≡ι n) ∙ sym (ι-+-commutes 1 n) ∙ cong ι (+-comm n 1)

CtoB-preserves-mul-nat : (a : Cnf) (n : ℕ) → CtoB (a • n) ≡ CtoB a B.· NviaCtoB n
CtoB-preserves-mul-nat 𝟎 0 = refl
CtoB-preserves-mul-nat 𝟎 (suc n) = sym (zero·y≡zero (NviaCtoB (suc n)))
CtoB-preserves-mul-nat (ω^ _ + _ [ _ ]) 0 = refl
CtoB-preserves-mul-nat a@(ω^ _ + _ [ _ ]) (suc n) =
CtoB (a • suc n)
≡⟨ cong CtoB (•suc-spec' a n) ⟩
CtoB (a C.+ a • n)
≡⟨ CtoB-preserves-add a (a • n) ⟩
CtoB a B.+ CtoB (a • n)
≡⟨ cong (CtoB a B.+_) (CtoB-preserves-mul-nat a n) ⟩
CtoB a B.+ CtoB a B.· NviaCtoB n
≡⟨ cong (B._+ CtoB a B.· NviaCtoB n) (sym (zero+y≡y (CtoB a))) ⟩
(zero B.+ CtoB a) B.+ CtoB a B.· NviaCtoB n
≡⟨ ·-+-distributivity (NviaCtoB n) ⟩
CtoB a B.· (succ zero B.+ NviaCtoB n) ∎

CtoB-preserves-mul : (a b : Cnf) → CtoB (a C.· b) ≡ CtoB a B.· CtoB b
CtoB-preserves-mul  𝟎                𝟎               = refl
CtoB-preserves-mul  𝟎               (ω^ b + d [ s ]) = sym (zero·y≡zero (CtoB (ω^ b + d [ s ])))
CtoB-preserves-mul (ω^ a + c [ r ])  𝟎               = refl
CtoB-preserves-mul x@(ω^ a + c [ r ]) (ω^ 𝟎 + d [ s ]) =
CtoB (x C.+ x C.· d)
≡⟨ CtoB-preserves-add x (x C.· d) ⟩
CtoB x B.+ CtoB (x C.· d)
≡⟨ cong (_ B.+_) (CtoB-preserves-mul _ d) ⟩
CtoB x B.+ CtoB x B.· CtoB d
≡⟨ cong (B._+ CtoB x B.· CtoB d) (sym (zero+y≡y _)) ⟩
CtoB x B.· ω^ zero B.+ CtoB x B.· CtoB d
≡⟨ ·-+-distributivity (CtoB d) ⟩
CtoB x B.· (ω^ zero B.+ CtoB d) ∎
CtoB-preserves-mul (ω^ a + c [ r ]) (ω^ b@(ω^ b' + b'' [ _ ]) + d [ s ]) =
(ω^ (CtoB (a C.+ b))) B.+ CtoB ((ω^ a + c [ r ]) C.· d)
≡⟨ cong (λ z → (ω^ z) B.+ CtoB ((ω^ a + c [ r ]) C.· d)) (CtoB-preserves-add a b) ⟩
(ω^ (CtoB a B.+ CtoB b)) B.+ CtoB ((ω^ a + c [ r ]) C.· d)
≡⟨ cong ((ω^ (CtoB a B.+ CtoB b)) B.+_) (CtoB-preserves-mul _ d) ⟩
(ω^ (CtoB a B.+ CtoB b)) B.+ (ω^ (CtoB a) B.+ CtoB c) B.· CtoB d
≡⟨ cong (B._+ (ω^ (CtoB a) B.+ CtoB c) B.· CtoB d) goal ⟩
(ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b) B.+ (ω^ (CtoB a) B.+ CtoB c) B.· CtoB d
≡⟨ ·-+-distributivity (CtoB d) ⟩
(ω^ (CtoB a) B.+ CtoB c) B.· (ω^ (CtoB b) B.+ CtoB d) ∎
where
fact : Σ[ n ∈ ℕ ] (ω^ a + c [ r ] C.< ω^⟨ a ⟩ • suc n)
fact = Σn<•sn (ω^ a + c [ r ]) (inr refl)
n : ℕ
n = suc (fst fact)
t : ω^ a + c [ r ] C.< ω^⟨ a ⟩ • n
t = snd fact
claim₀ : ω^ (CtoB a) B.+ CtoB c B.< CtoB (ω^⟨ a ⟩ • n)
claim₀ = CtoB-monotone t
claim₁ : CtoB (ω^⟨ a ⟩ • n) ≡ CtoB (ω^⟨ a ⟩) B.· NviaCtoB n
claim₁ = CtoB-preserves-mul-nat ω^⟨ a ⟩ n
claim₂ : ω^ (CtoB a) B.+ CtoB c B.< CtoB (ω^⟨ a ⟩) B.· NviaCtoB n
claim₂ = subst (ω^ (CtoB a) B.+ CtoB c B.<_) claim₁ claim₀
claim₃ : (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b) B.≤
(CtoB (ω^⟨ a ⟩) B.· NviaCtoB n) B.· ω^ (CtoB b)
claim₃ = ·x-mono (ω^ (CtoB b)) (B.<-in-≤ claim₂)
claim₄ : NviaCtoB n B.· ω^ (CtoB b) ≡ ω^ (CtoB b)
claim₄ = cong (B._· ω^ (CtoB b)) (NviaCtoB≡ι n) ∙
ω^x-absorbs-finite {x = CtoB b} (B.<∘≤-in-< (zero<ω^c (CtoB b'))
(x+-mono {ω^ (CtoB b')} (≤-zero {CtoB b''})))
claim₅ : (CtoB (ω^⟨ a ⟩) B.· NviaCtoB n) B.· ω^ (CtoB b) ≡ ω^ (CtoB a B.+ CtoB b)
claim₅ =
(ω^ (CtoB a) B.· NviaCtoB n) B.· ω^ (CtoB b)
≡⟨ sym (·-assoc (ω^ (CtoB b))) ⟩
ω^ (CtoB a) B.· (NviaCtoB n B.· ω^ (CtoB b))
≡⟨ cong (CtoB (ω^⟨ a ⟩) B.·_) claim₄ ⟩
ω^ (CtoB a) B.· ω^ (CtoB b)
≡⟨ sym (exp-homomorphism {B.ω} {CtoB a} {CtoB b}) ⟩
ω^ (CtoB a B.+ CtoB b) ∎
claim₆ : (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b) B.≤ ω^ (CtoB a B.+ CtoB b)
claim₆ = subst ((ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b) B.≤_) claim₅ claim₃
claim₇ : ω^ (CtoB a B.+ CtoB b) ≡ ω^ (CtoB a) B.· ω^ (CtoB b)
claim₇ = exp-homomorphism {B.ω} {CtoB a} {CtoB b}
claim₈ : ω^ (CtoB a) B.· ω^ (CtoB b) B.≤ (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b)
claim₈ = ·x-mono (ω^ (CtoB b)) (CtoB-≤-monotone {ω^⟨ a ⟩} {ω^ a + c [ r ]} (≤₃ refl 𝟎≤))
claim₉ : ω^ (CtoB a B.+ CtoB b) B.≤ (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b)
claim₉ = subst (B._≤ (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b)) (sym claim₇) claim₈
goal : ω^ (CtoB a B.+ CtoB b) ≡ (ω^ (CtoB a) B.+ CtoB c) B.· ω^ (CtoB b)
goal = antisym claim₉ claim₆

CtoB-preserves-exp-with-base-ω : (a : Cnf) → CtoB (ω^⟨ a ⟩) ≡ ω^ (CtoB a)
CtoB-preserves-exp-with-base-ω a = refl

{- The interpretation of any CNF is below ε₀ -}

CNF<ε₀ : (a : Cnf) → CtoB a B.< ε₀
CNF<ε₀ a = subst (λ z → CtoB a B.< z) (sym ε₀≡ω^ε₀) (CNF<ω^ε₀ a) where
CNF<ω^ε₀ : (a : Cnf) → CtoB a B.< ω^ ε₀
CNF<ω^ε₀ 𝟎 = zero<lim
CNF<ω^ε₀ (ω^ a + b [ r ]) =