----------------------------------------------------------------------------------------------------
-- Correctness of arithmetic operations on Cantor Normal Forms
----------------------------------------------------------------------------------------------------

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

module CantorNormalForm.Arithmetic where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Empty
  renaming (rec to ⊥-rec)

open import CantorNormalForm.Base
open import CantorNormalForm.Addition public
open import CantorNormalForm.Subtraction public
open import CantorNormalForm.Multiplication public
open import CantorNormalForm.Division public
open import CantorNormalForm.Exponentiation public
open import CantorNormalForm.Classifiability
open import Abstract.Arithmetic _<_ _≤_ public


{- Addition is correct and unique -}

+r-preserves-sup :  {a} c {f}  a is-sup-of f  (c + a) is-sup-of  i  c + f i)
+r-preserves-sup {a} c {f} (f≤a , a-min-over-f) = c+f≤c+a , c+a-min-over-c+f
 where
  c+f≤c+a :  i  c + f i  c + a
  c+f≤c+a i = +r-is-≤-monotone c _ _ (f≤a i)
  c+a-min-over-c+f :  x  (∀ i  c + f i  x)  c + a  x
  c+a-min-over-c+f x c+f≤x = subst (c + a ≤_) c+⟨x-c⟩≡x c+a≤c+⟨x-c⟩
   where
    f≤x-c :  i  f i  x - c
    f≤x-c i = +≤→≤- c (f i) x (c+f≤x i)
    a≤x-c : a  x - c
    a≤x-c = a-min-over-f (x - c) f≤x-c
    c+a≤c+⟨x-c⟩ : c + a  c + (x - c)
    c+a≤c+⟨x-c⟩ = +r-is-≤-monotone c _ _ a≤x-c
    c+⟨x-c⟩≡x : c + (x - c)  x
    c+⟨x-c⟩≡x = sub-spec₀ c x (≤-trans (≤+r c (f 0)) (c+f≤x 0))

+-is-add : is-add _+_
+-is-add = case-zero , case-suc , case-lim
 where
  case-zero :  a c  is-zero a  c + a  c
  case-zero a c a-is-zero =
     c + a
    ≡⟨ cong (c +_) (is-zero→≡𝟎 a-is-zero) 
     c + 𝟎
    ≡⟨ +𝟎-is-identity 
     c 
  case-suc :  a b c d  a is-suc-of b  d is-suc-of (c + b)  c + a  d
  case-suc a b c d a-is-suc-of-b d-is-suc-of-c+d =
     c + a
    ≡⟨ cong (c +_) (sym (suc→+𝟏 a-is-suc-of-b)) 
     c + (b + 𝟏)
    ≡⟨ +-is-assoc c b 𝟏 
     (c + b) + 𝟏
    ≡⟨ suc→+𝟏 d-is-suc-of-c+d 
     d 
  case-lim :  a b c f f↑  a is-lim-of (f , f↑)  b is-sup-of  i  c + f i)  c + a  b
  case-lim a b c f f↑ a-is-sup-of-f b-is-sup-of-c+f = c+a≡b
   where
    c+a-is-sup-of-c+f : (c + a) is-sup-of  i  c + f i)
    c+a-is-sup-of-c+f = +r-preserves-sup c a-is-sup-of-f
    c+a≡b : c + a  b
    c+a≡b = sup-unique c+a-is-sup-of-c+f b-is-sup-of-c+f

add-is-unique : (_+'_ : Cnf  Cnf  Cnf)  is-add _+'_  _+_  _+'_
add-is-unique _+'_ (+'-is-add-zero , +'-is-add-suc , +'-is-add-lim) = funExt (funExt  goal)
 where
  goal :  c a  c + a  c +' a
  goal c = cf-ind  _  Cnf-is-set _ _) case-zero case-suc case-lim
   where
    case-zero : c + 𝟎  c +' 𝟎
    case-zero =
       c + 𝟎
      ≡⟨ +𝟎-is-identity 
       c
      ≡⟨ sym (+'-is-add-zero 𝟎 c 𝟎-is-zero) 
       c +' 𝟎 
    case-suc :  a  c + a  c +' a  c + (a + 𝟏)  c +' (a + 𝟏)
    case-suc a ih =
       c + (a + 𝟏)
      ≡⟨ +-is-assoc c a 𝟏 
       (c + a) + 𝟏
      ≡⟨ cong (_+ 𝟏) ih 
       (c +' a) + 𝟏
      ≡⟨ sym (+'-is-add-suc (a + 𝟏) a c ((c +' a) + 𝟏) (+𝟏-calc-suc a) (+𝟏-calc-suc (c +' a))) 
       c +' (a + 𝟏) 
    case-lim :  a f f↑  a is-lim-of (f , f↑)
              (∀ i  c + f i  c +' f i)
              c + a  c +' a
    case-lim a f f↑ a-is-sup-of-f ih =
       c + a
      ≡⟨ sym (+'-is-add-lim a (c + a) c f f↑ a-is-sup-of-f c+a-is-sup-of-c+'f) 
       c +' a 
     where
      c+a-is-sup-of-c+f : (c + a) is-sup-of  i  c + f i)
      c+a-is-sup-of-c+f = +r-preserves-sup c a-is-sup-of-f
      c+'f≤c+a :  i  (c +' f i)  c + a
      c+'f≤c+a i = ≤-trans (inr (ih i)) (fst c+a-is-sup-of-c+f i)
      c+a-min-over-c+'f :  x  (∀ i  (c +' f i)  x)  c + a  x
      c+a-min-over-c+'f x c+'f≤x = snd c+a-is-sup-of-c+f x c+f≤x
       where
        c+f≤x :  i  c + f i  x
        c+f≤x i = subst (_≤ x) (sym (ih i)) (c+'f≤x i)
      c+a-is-sup-of-c+'f : (c + a) is-sup-of  i  c +' f i)
      c+a-is-sup-of-c+'f = c+'f≤c+a , c+a-min-over-c+'f

Cnf-has-unique-add : has-unique-add
Cnf-has-unique-add = (_+_ , +-is-add) ,
                      (f , p)  Σ≡Prop (isProp⟨is-add⟩ Cnf-is-set) (add-is-unique f p))


{- Multiplication is correct and unique -}

open Multiplication (_+_ , +-is-add) hiding (_+_) public

·r-preserves-sup :  {a} c {f}  a is-sup-of f  (c · a) is-sup-of  i  c · f i)
·r-preserves-sup {a} 𝟎 {f} _ =  _  𝟎≤) ,  _ _  𝟎≤)
·r-preserves-sup {a} c@(ω^ _ + _ [ _ ]) {f} (f≤a , a-min-over-f) = c·f≤c·a , c·a-min-over-c·f
 where
  c·f≤c·a :  i  c · f i  c · a
  c·f≤c·a i = ·r-is-≤-monotone c _ _ (f≤a i)
  c·a-min-over-c·f :  x  (∀ i  c · f i  x)  c · a  x
  c·a-min-over-c·f x c·f≤x = c·a≤x
   where
    y : Cnf
    y = x / c [ <₁ ]
    f≤y :  i  f i  y
    f≤y i = greatest-div x c (f i) <₁ (c·f≤x i)
    a≤y : a  y
    a≤y = a-min-over-f y f≤y
    c·a≤c·y : c · a  c · y
    c·a≤c·y = ·r-is-≤-monotone c a y a≤y
    c·y≤x : c · y  x
    c·y≤x = div-spec x c <₁
    c·a≤x : c · a  x
    c·a≤x = ≤-trans c·a≤c·y c·y≤x

·-is-mul : is-mul _·_
·-is-mul = case-zero , case-suc , case-lim
 where
  case-zero :  a c  is-zero a  c · a  a
  case-zero a c a-is-zero =
     c · a
    ≡⟨ cong (c ·_) (is-zero→≡𝟎 a-is-zero) 
     c · 𝟎
    ≡⟨ ·𝟎-is-𝟎 c 
     𝟎
    ≡⟨ sym (is-zero→≡𝟎 a-is-zero) 
     a 
  case-suc :  a b c  a is-suc-of b  c · a  c · b + c
  case-suc a b c a-is-suc-of-b =
     c · a
    ≡⟨ cong (c ·_) (sym (suc→+𝟏 a-is-suc-of-b)) 
     c · (b + 𝟏)
    ≡⟨ ·+𝟏-spec c b 
     c · b + c 
  case-lim :  a b c f f↑  a is-lim-of (f , f↑)  b is-sup-of  i  c · f i)  c · a  b
  case-lim a b c f f↑ a-is-sup-of-f b-is-sup-of-c·f = c·a≡b
   where
    c·a-is-sup-of-c·f : (c · a) is-sup-of  i  c · f i)
    c·a-is-sup-of-c·f = ·r-preserves-sup c a-is-sup-of-f
    c·a≡b : c · a  b
    c·a≡b = sup-unique c·a-is-sup-of-c·f b-is-sup-of-c·f

mul-is-unique : (_·'_ : Cnf  Cnf  Cnf)  is-mul _·'_  _·_  _·'_
mul-is-unique _·'_ (·'-is-mul-zero , ·'-is-mul-suc , ·'-is-mul-lim) = funExt (funExt  goal)
 where
  goal :  c a  c · a  c ·' a
  goal c = cf-ind  _  Cnf-is-set _ _) case-zero case-suc case-lim
   where
    case-zero : c · 𝟎  c ·' 𝟎
    case-zero =
       c · 𝟎
      ≡⟨ ·𝟎-is-𝟎 c 
       𝟎
      ≡⟨ sym (·'-is-mul-zero 𝟎 c 𝟎-is-zero) 
       c ·' 𝟎 
    case-suc :  a  c · a  c ·' a  c · (a + 𝟏)  c ·' (a + 𝟏)
    case-suc a ih =
       c · (a + 𝟏)
      ≡⟨ ·+𝟏-spec c a 
       c · a + c
      ≡⟨ cong (_+ c) ih 
       (c ·' a) + c
      ≡⟨ sym (·'-is-mul-suc (a + 𝟏) a c (+𝟏-calc-suc a)) 
       c ·' (a + 𝟏) 
    case-lim :  a f f↑  a is-lim-of (f , f↑)
              (∀ i  c · f i  c ·' f i)
              c · a  c ·' a
    case-lim a f f↑ a-is-sup-of-f ih =
       c · a
      ≡⟨ sym (·'-is-mul-lim a (c · a) c f f↑ a-is-sup-of-f c·a-is-sup-of-c·'f) 
       c ·' a 
     where
      c·a-is-sup-of-c·f : (c · a) is-sup-of  i  c · f i)
      c·a-is-sup-of-c·f = ·r-preserves-sup c a-is-sup-of-f
      c·'f≤c·a :  i  (c ·' f i)  c · a
      c·'f≤c·a i = ≤-trans (inr (ih i)) (fst c·a-is-sup-of-c·f i)
      c·a-min-over-c·'f :  x  (∀ i  (c ·' f i)  x)  c · a  x
      c·a-min-over-c·'f x c·'f≤x = snd c·a-is-sup-of-c·f x c·f≤x
       where
        c·f≤x :  i  c · f i  x
        c·f≤x i = subst (_≤ x) (sym (ih i)) (c·'f≤x i)
      c·a-is-sup-of-c·'f : (c · a) is-sup-of  i  c ·' f i)
      c·a-is-sup-of-c·'f = c·'f≤c·a , c·a-min-over-c·'f

Cnf-has-unique-mul : has-unique-mul
Cnf-has-unique-mul = (_·_ , ·-is-mul) ,
                      (f , p)  Σ≡Prop (isProp⟨is-mul⟩ Cnf-is-set) (mul-is-unique f p))


{- Exponentiation with base ω is correct and unique -}

open Exponentiation
  (_+_ , +-is-add)
  (_·_ , ·-is-mul)
  hiding (_·_)
  public

ω^⟨⟩-is-exp-with-base-ω : ω^⟨_⟩ is-exp-with-base ω
ω^⟨⟩-is-exp-with-base-ω = case-zero , case-suc , case-lim ,  _ _ _ _ ωz  ⊥-rec (ω^≰𝟎 (ωz 𝟎)))
 where
  case-zero :  a b  is-zero a  b is-suc-of a  ω^⟨ a   b
  case-zero a b a-is-zero b-is-suc-of-a =
     ω^⟨ a 
    ≡⟨ cong ω^⟨_⟩ (is-zero→≡𝟎 a-is-zero) 
     ω^⟨ 𝟎 
    ≡⟨ cong (_+ 𝟏) (sym (is-zero→≡𝟎 a-is-zero)) 
     a + 𝟏
    ≡⟨ suc→+𝟏 b-is-suc-of-a 
     b 
  case-suc :  a b  a is-suc-of b  ω^⟨ a   ω^⟨ b  · ω
  case-suc a b a-is-suc-of-b =
     ω^⟨ a 
    ≡⟨ cong ω^⟨_⟩ (sym (suc→+𝟏 a-is-suc-of-b)) 
     ω^⟨ b + 𝟏 
    ≡⟨ refl 
     ω^⟨ b  · ω 
  case-lim :  a b f f↑  a is-lim-of (f , f↑)  _  b is-sup-of  i  ω^⟨ f i )  ω^⟨ a   b
  case-lim a 𝟎 f f↑ a-is-sup-of-f _ 𝟎-is-sup-of-ω^f = ⊥-rec (ω^≰𝟎 (fst 𝟎-is-sup-of-ω^f 0))
  case-lim a b@(ω^ u + v [ r ]) f f↑ a-is-sup-of-f _ b-is-sup-of-ω^f = goal
   where
    f≤u :  i  f i  u
    f≤u i = ≮→≥  u<fi  ≤→≯ (fst b-is-sup-of-ω^f i) (<₂ u<fi))
    a≤u : a  u
    a≤u = snd a-is-sup-of-f u f≤u
    ω^a≤b : ω^⟨ a   b
    ω^a≤b = ≤-trans (≤₂ {a} {u} {𝟎} {𝟎≤} {𝟎≤} a≤u) (≤₃ refl 𝟎≤)
    ω^f<ω^a :  i  ω^⟨ f i   ω^⟨ a 
    ω^f<ω^a i = ≤₂ (fst a-is-sup-of-f i)
    b≤ω^a : b  ω^⟨ a 
    b≤ω^a = snd b-is-sup-of-ω^f ω^⟨ a  ω^f<ω^a
    goal : ω^⟨ a   b
    goal = ≤-antisym ω^a≤b b≤ω^a


exp-is-unique : (exp : Cnf  Cnf)  exp is-exp-with-base ω  ω^⟨_⟩  exp
exp-is-unique exp exp-is-exp = funExt goal
 where
  goal :  a  ω^⟨ a   exp a
  goal = cf-ind  _  Cnf-is-set _ _) case-zero case-suc case-lim
   where
    case-zero : ω^⟨ 𝟎   exp 𝟎
    case-zero = sym (fst exp-is-exp 𝟎 𝟏 𝟎-is-zero (+𝟏-calc-suc 𝟎))
    case-suc :  a  ω^⟨ a   exp a  ω^⟨ a + 𝟏   exp (a + 𝟏)
    case-suc a ih =
       ω^⟨ a + 𝟏 
      ≡⟨ refl 
       ω^⟨ a  · ω
      ≡⟨ cong ( ω) ih 
       exp a · ω
      ≡⟨ sym (fst (snd exp-is-exp) (a + 𝟏) a (+𝟏-calc-suc a)) 
       exp (a + 𝟏) 
    case-lim :  a f f↑  a is-lim-of (f , f↑)  (∀ i  ω^⟨ f i   exp (f i))  ω^⟨ a   exp a
    case-lim a f f↑ a-is-sup-of-f ih = ω^a≡expa
      where
       expf≤ω^a :  i  exp (f i)  ω^⟨ a 
       expf≤ω^a i = ≤-trans (inr (ih i)) (≤₂ (fst a-is-sup-of-f i))
       ω^a-min-over-expf :  x  (∀ i  exp (f i)  x)  ω^⟨ a   x
       ω^a-min-over-expf 𝟎 h = ⊥-rec (ω^≰𝟎 (subst (_≤ 𝟎) (sym (ih 0)) (h 0)))
       ω^a-min-over-expf x@(ω^ u + v [ r ]) h = ω^a≤x
        where
         f≤u :  i  f i  u
         f≤u i = ≮→≥  u<fi  ≤→≯ (subst (_≤ _) (sym (ih i)) (h i)) (<₂ u<fi))
         a≤u : a  u
         a≤u = snd a-is-sup-of-f u f≤u
         ω^a≤x : ω^⟨ a   x
         ω^a≤x = ≤-trans (≤₂ {a} {u} {𝟎} {𝟎≤} {𝟎≤} a≤u) (≤₃ refl 𝟎≤)
       ω^a-is-sup-of-expf : ω^⟨ a  is-sup-of  i  exp (f i))
       ω^a-is-sup-of-expf = expf≤ω^a , ω^a-min-over-expf
       ω^a≡expa : ω^⟨ a   exp a
       ω^a≡expa = sym (fst (snd (snd exp-is-exp)) a (ω^⟨ a ) f f↑ a-is-sup-of-f
                            ωz  ω^≰𝟎 (ωz 𝟎)) ω^a-is-sup-of-expf)

Cnf-has-unique-exp-with-base-ω : has-unique-exp-with-base ω
Cnf-has-unique-exp-with-base-ω =
  (ω^⟨_⟩ , ω^⟨⟩-is-exp-with-base-ω) ,
   (f , p)  Σ≡Prop  _  isProp⟨is-exp⟩ Cnf-is-set _ _) (exp-is-unique f p))