----------------------------------------------------------------------------------------------------
-- Addition of Cantor Normal Forms
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

module CantorNormalForm.Addition where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Empty
  renaming (rec to ⊥-rec)
open import Cubical.Data.Nat
  using (ℕ ; zero ; suc)

open import CantorNormalForm.Base


{- Addition -}

infixl  _+_

mutual

 _+_ : Cnf → Cnf → Cnf
 𝟎 + b = b
 a + 𝟎 = a
 (ω^ a + c [ r ]) + (ω^ b + d [ s ]) with <-tri a b
 ... | inl a<b = ω^ b + d [ s ]
 ... | inr a≥b = ω^ a + (c + ω^ b + d [ s ]) [ ≥left+ c _ r a≥b ]

 ≥left+ : {a : Cnf} (b c : Cnf)
        → a ≥ left b → a ≥ left c → a ≥ left (b + c)
 ≥left+ 𝟎 _ r s = s
 ≥left+ (ω^ _ + _ [ _ ]) 𝟎 r s = r
 ≥left+ (ω^ b + _ [ _ ]) (ω^ c + _ [ _ ]) r s with <-tri b c
 ... | inl b<c = s
 ... | inr b≥c = r

{- Some properties of addition -}

+𝟎-is-identity : {a : Cnf} → a + 𝟎 ≡ a
+𝟎-is-identity {𝟎} = refl
+𝟎-is-identity {ω^ a + b [ r ]} = refl

+-is-assoc : ∀ a b c → a + (b + c) ≡ (a + b) + c
+-is-assoc 𝟎 b c = refl
+-is-assoc (ω^ a + a' [ r ]) 𝟎 c = refl
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) 𝟎 = sym +𝟎-is-identity
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  with <-tri a b with <-tri b c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inl a<b | inl b<c with <-tri b c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inl a<b | inl b<c | inl _ with <-tri a c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inl a<b | inl b<c | inl _ | inl a<c = refl
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inl a<b | inl b<c | inl _ | inr a≥c = ⊥-rec (≤→≯ a≥c (<-trans a<b b<c))
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inl a<b | inl b<c | inr b≥c = ⊥-rec (≤→≯ b≥c b<c)
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inl a<b | inr b≥c with <-tri a b
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inl a<b | inr b≥c | inl _ with <-tri b c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inl a<b | inr b≥c | inl _ | inl b<c = ⊥-rec (≤→≯ b≥c b<c)
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inl a<b | inr b≥c | inl _ | inr _ = Cnf⁼ refl refl
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inl a<b | inr b≥c | inr a≥b = ⊥-rec (≤→≯ a≥b a<b)
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inr a≥b | inl b<c with <-tri a c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inr a≥b | inl b<c | inl a<c = refl
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inr a≥b | inl b<c | inr a≥c = Cnf⁼ refl (claim₁ ∙ IH)
 where
  IH : a' + (ω^ b + b' [ s ] + ω^ c + c' [ t ]) ≡ (a' + ω^ b + b' [ s ]) + ω^ c + c' [ t ]
  IH = +-is-assoc a' (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  claim₀ : ω^ c + c' [ t ] ≡ ω^ b + b' [ s ] + ω^ c + c' [ t ]
  claim₀ with <-tri b c
  claim₀ | inl _ = refl
  claim₀ | inr b≥c = ⊥-rec (≤→≯ b≥c b<c)
  claim₁ : a' + ω^ c + c' [ t ] ≡ a' + (ω^ b + b' [ s ] + ω^ c + c' [ t ])
  claim₁ = cong (a' +_) claim₀
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inr a≥b | inr b≥c with <-tri a c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inr a≥b | inr b≥c | inl a<c = ⊥-rec (≤→≯ (≤-trans b≥c a≥b) a<c)
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inr a≥b | inr b≥c | inr a≥c with <-tri a b
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inr a≥b | inr b≥c | inr a≥c | inl a<b = ⊥-rec (≤→≯ a≥b a<b)
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  | inr a≥b | inr b≥c | inr a≥c | inr _ = Cnf⁼ refl (claim₁ ∙ IH)
 where
  IH : a' + (ω^ b + b' [ s ] + ω^ c + c' [ t ]) ≡ (a' + ω^ b + b' [ s ]) + ω^ c + c' [ t ]
  IH = +-is-assoc a' (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
  claim₀ : ω^ b + (b' + ω^ c + c' [ t ]) [ _ ] ≡ ω^ b + b' [ s ] + ω^ c + c' [ t ]
  claim₀ with <-tri b c
  claim₀ | inl b<c = ⊥-rec (≤→≯ b≥c b<c)
  claim₀ | inr _ = Cnf⁼ refl refl
  claim₁ : a' + (ω^ b + (b' + ω^ c + c' [ t ]) [ _ ]) ≡ a' + (ω^ b + b' [ s ] + ω^ c + c' [ t ])
  claim₁ = cong (a' +_) claim₀

≤+r : ∀ a b → a ≤ a + b
≤+r 𝟎 b = 𝟎≤
≤+r (ω^ a + c [ r ]) 𝟎 = inr refl
≤+r (ω^ a + c [ r ]) (ω^ b + d [ s ]) with <-tri a b
... | inl a<b = inl (<₂ a<b)
... | inr a≥b = ≤₃ refl (≤+r c _)

<+r : ∀ a b → b > 𝟎 → a < a + b
<+r 𝟎 (ω^ b + d [ s ]) <₁ = <₁
<+r (ω^ a + c [ r ]) (ω^ b + d [ s ]) <₁ with <-tri a b
... | inl a<b = <₂ a<b
... | inr a≥b = <₃ refl (<+r c (ω^ b + d [ s ]) <₁ )

+r-is-<-monotone : ∀ a b c → b < c → a + b < a + c
+r-is-<-monotone 𝟎 b c b<c = b<c
+r-is-<-monotone (ω^ a + a' [ r ]) 𝟎 c <₁ = <+r _ c <₁
+r-is-<-monotone (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ]) (<₂ b<c)
  with <-tri a b with <-tri a c
... | inl a<b | inl a<c = <₂ b<c
... | inl a<b | inr a≥c = ⊥-rec (≤→≯ a≥c (<-trans a<b b<c))
... | inr a≥b | inl a<c = <₂ a<c
... | inr a≥b | inr a≥c = <₃ refl (+r-is-<-monotone a' _ _ (<₂ b<c))
+r-is-<-monotone (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ]) (<₃ b≡c b'<c')
  with <-tri a b with <-tri a c
... | inl a<b | inl a<c = <₃ b≡c b'<c'
... | inl a<b | inr a≥c = ⊥-rec (≤→≯ (≤-trans (inr (sym b≡c)) a≥c) a<b)
... | inr a≥b | inl a<c = ⊥-rec (≤→≯ (≤-trans (inr b≡c) a≥b) a<c)
... | inr a≥b | inr a≥c = <₃ refl (+r-is-<-monotone a' _ _ (<₃ b≡c b'<c'))

+r-is-≤-monotone : ∀ a b c → b ≤ c → a + b ≤ a + c
+r-is-≤-monotone a b c (inl b<c) = inl (+r-is-<-monotone a b c b<c)
+r-is-≤-monotone a b c (inr c≡b) = inr (cong (a +_) c≡b)

ω^+≡ω^⟨⟩+ : ∀ {a} b r → ω^ a + b [ r ] ≡ ω^⟨ a ⟩ + b
ω^+≡ω^⟨⟩+ {a} 𝟎 _ = Cnf⁼ refl refl
ω^+≡ω^⟨⟩+ {a} (ω^ b + c [ r ]) a≥b with <-tri a b
... | inl a<b = ⊥-rec (≤→≯ a≥b a<b)
... | inr _ = Cnf⁼ refl refl

+-left-cancel : ∀ a b → left a < left b → a + b ≡ b
+-left-cancel 𝟎 b _ = refl
+-left-cancel (ω^ a + c [ r ]) (ω^ b + d [ s ]) a<b with <-tri a b
... | inl _   = refl
... | inr a≥b = ⊥-rec (≤→≯ a≥b a<b)

left⟨+⟩ : ∀ a b → left a ≥ left b → left a ≡ left (a + b)
left⟨+⟩ 𝟎 b lb≤𝟎 = sym (≤𝟎→≡𝟎 lb≤𝟎)
left⟨+⟩ (ω^ a + c [ r ]) 𝟎 _ = refl
left⟨+⟩ (ω^ a + c [ r ]) (ω^ b + d [ s ]) a≥b with <-tri a b
... | inl a<b = ⊥-rec (≤→≯ a≥b a<b)
... | inr _   = refl

left⟨+⟩≤⁻¹ : ∀ a b c → left (a + b) ≤ c → (left a ≤ c) × (left b ≤ c)
left⟨+⟩≤⁻¹ 𝟎 b c t = 𝟎≤ , t
left⟨+⟩≤⁻¹ (ω^ a + a' [ r ]) 𝟎 c t = t , 𝟎≤
left⟨+⟩≤⁻¹ (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) c t with <-tri a b
... | inl a<b = ≤-trans (inl a<b) t , t
... | inr a≥b = t , ≤-trans a≥b t


{- Successor -}

<+𝟏 : ∀ {x} → x < x + 𝟏
<+𝟏 {𝟎} = <₁
<+𝟏 {ω^ a + b [ c ]} with <-tri a 𝟎
... | inr _ = <₃ refl <+𝟏

{- Some properties of successor -}

<→+𝟏≤ : ∀ {x y} → x < y → x + 𝟏 ≤ y
<→+𝟏≤ {𝟎} {ω^ c + d [ s ]} <₁ = 𝟏≤ω^
<→+𝟏≤ {ω^ a + b [ r ]} {ω^ c + d [ s ]} (<₂ a<c) with <-tri a 𝟎
... | inr _ = inl (<₂ a<c)
<→+𝟏≤ {ω^ a + b [ r ]} {ω^ c + d [ s ]} (<₃ a≡c b<d) with <-tri a 𝟎
... | inr _ = ≤₃ a≡c (<→+𝟏≤ b<d)

<+𝟏→≤ : ∀ {x y} → x < y + 𝟏 → x ≤ y
<+𝟏→≤ {𝟎} {y} _ = 𝟎≤
<+𝟏→≤ {ω^ a + b [ r ]} {𝟎} t = ⊥-rec (ω^≮𝟏 t)
<+𝟏→≤ {ω^ a + b [ r ]} {ω^ c + d [ s ]} t with <-tri c 𝟎
... | inr _ with ω^<-cases t
... | inl a<c = inl (<₂ a<c)
... | inr (a≡c , b<d+1) = ≤₃ a≡c (<+𝟏→≤ b<d+1)

ω^𝟎+-is-+𝟏 : (a : Cnf) (r : 𝟎 ≥ left a) → a + 𝟏 ≡ ω^ 𝟎 + a [ r ]
ω^𝟎+-is-+𝟏 𝟎 _ = Cnf⁼ refl refl
ω^𝟎+-is-+𝟏 ω^ a + b [ r ] (inr 𝟎≡a) with <-tri a 𝟎
... | inr _ = goal
 where
  𝟎≥lb : 𝟎 ≥ left b
  𝟎≥lb = subst (_≥ left b) (sym 𝟎≡a) r
  IH :  b + 𝟏 ≡ ω^ 𝟎 + b [ 𝟎≥lb ]
  IH = ω^𝟎+-is-+𝟏 b 𝟎≥lb
  goal : ω^ a + (b + 𝟏) [ _ ] ≡ ω^ 𝟎 + (ω^ a + b [ r ]) [ inr 𝟎≡a ]
  goal = Cnf⁼ (sym 𝟎≡a) (IH ∙ Cnf⁼ 𝟎≡a refl)

NtoC⟨suc⟩≡NtoC+𝟏 : ∀ n → NtoC (suc n) ≡ NtoC n + 𝟏
NtoC⟨suc⟩≡NtoC+𝟏 n = sym (ω^𝟎+-is-+𝟏 (NtoC n) _)