----------------------------------------------------------------------------------------------------
-- 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 hiding (succ)
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  𝟎                𝟎               = refl
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 = B.≤-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 ]) =
    additive-principal-ω^-closure {c = ε₀}
                                  (ω^-mono-< (subst (λ z → CtoB a B.< z) (sym ε₀≡ω^ε₀) (CNF<ω^ε₀ a)))
                                  (CNF<ω^ε₀ b)