----------------------------------------------------------------------------------------------------
-- 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)