----------------------------------------------------------------------------------------------------
-- Arithmetic operations on Brouwer trees
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

module BrouwerTree.Arithmetic where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Path
open import Cubical.Foundations.Function

open import Cubical.Data.Nat
  using (; zero; suc)
  renaming (_+_ to _N+_)
open import Cubical.Data.Sum
open import Cubical.Data.Empty as 

open import Cubical.Relation.Nullary

open import Cubical.HITs.PropositionalTruncation.Properties
  renaming (rec to ∥-∥rec)

open import BrouwerTree.Base
open import BrouwerTree.Properties
open import BrouwerTree.Code
open import BrouwerTree.Code.Results


infixr 35 _+_
infixr 36 _·_
infixr 37 _^_

{- Addition -}

mutual
  _+_ : Brw  Brw  Brw
  x + zero = x
  x + (succ y) = succ (x + y)
  x + (limit f {f↑}) = limit  n  x + f n)  k  x+-mono (f↑ k)}
  x + (bisim f {f↑} g {g↑} (f≲g , g≲f) i) = bisim  n  x + f n)
                                                  {x+-preserves--increasing f↑}
                                                   n  x + g n)
                                                  {x+-preserves--increasing g↑}
                                                  (x+-preserves-≲ f≲g , x+-preserves-≲ g≲f)
                                                  i
  x + (trunc y z p q i j) = trunc (x + y) (x + z)  j  x + (p j))  j  x + (q j)) i j

  x+-mono : {x y z : Brw}  y  z  x + y  x + z
  x+-mono ≤-zero = x+-increasing _
  x+-mono (≤-trans y≤z z≤w) = ≤-trans (x+-mono y≤z) (x+-mono z≤w)
  x+-mono (≤-succ-mono y≤z) = ≤-succ-mono (x+-mono y≤z)
  x+-mono (≤-cocone f {k = k} y≤fk) = ≤-cocone _ {k = k} (x+-mono y≤fk)
  x+-mono (≤-limiting f fk≤z) = ≤-limiting _ λ k  x+-mono (fk≤z k)
  x+-mono (≤-trunc p q i) = ≤-trunc (x+-mono p) (x+-mono q) i

  -- Agda does not see that the recursive call on `fk≤gl` is structurally smaller,
  -- because it has been uncovered under the propositional truncation. In the
  -- "official" induction principle, we instead get a family of truncated inductive hypothesis,
  -- and here we can uncover the k-th one because we are proving a proposition.
  -- To work around this, we mark the definition as terminating.
  {-# TERMINATING #-}
  x+-preserves-≲ :  {x f g}  f  g  ((x +_)  f)  ((x +_)  g)
  x+-preserves-≲ f≲g k = ∥-∥rec propTruncIsProp  (l , fk≤gl)   l , x+-mono fk≤gl ) (f≲g k)

  x+-increasing :  {x} (z : Brw)  x  x + z
  x+-increasing {x} zero = ≤-refl
  x+-increasing {x} (succ z) = ≤-succ-incr (x+-increasing z)
  x+-increasing {x} (limit f) = ≤-cocone _ {k = 5} (x+-increasing (f 5))
  x+-increasing {x} (bisim f {f↑} g {g↑} (f≲g , g≲f) i) =
      isProp→PathP {B = λ i  x  bisim _ _ (x+-preserves-≲ f≲g , x+-preserves-≲ g≲f) i}
                    i  ≤-trunc)
                   (≤-cocone _ (x+-increasing (f 5)))
                   (≤-cocone _ (x+-increasing (g 5)))
                   i
  x+-increasing {x} (trunc y z p q i j) =
      isProp→SquareP {B = λ i j  x  trunc (x + y) (x + z)  j  x + p j)  j  x + q j) i j}
                      i j  ≤-trunc)
                      j  x+-increasing y)
                      j  x+-increasing z)
                      j  x+-increasing (p j))
                      j  x+-increasing (q j))
                     i j

  x+-preserves--increasing :  {x f}  increasing f  increasing  n  x + f n)
  x+-preserves--increasing f↑ k = x+-mono (f↑ k)

zero+y≡y :  y  zero + y  y
zero+y≡y =
  Brw-ind  y  zero + y  y)
           x  Brw-is-set _ _)
          refl
          (cong succ)
           {f} {f↑} ih  bisim  n  zero + f n) f
                                 ((λ k   k , subst  z  z  f k) (sym (ih k)) ≤-refl ) ,
                                   k   k , subst  z  f k  z) (sym (ih k)) ≤-refl )))

+x-increasing :  {y}  (x : Brw)  x  y + x
+x-increasing {y} =
  Brw-ind  x  x  y + x)
           x  ≤-trunc)
          ≤-zero
          ≤-succ-mono
           {f} {f↑} ih  ≤-limiting f  k  ≤-trans (ih k) (≤-cocone-simple  n  y + f n))))

+x-mono :  {x y} (z  : Brw)  x  y  x + z  y + z
+x-mono {x} {y} =
  Brw-ind  z  x  y  x + z  y + z)
           z  isProp→ ≤-trunc)
           p  p)
           ih p  ≤-succ-mono (ih p))
           {f} {f↑} ih p  weakly-bisimilar→lim≤lim  n  x + f n)
                                                       n  y + f n)
                                                       k   k , ih k p ))

+-mono :  {x y x' y'}  x  x'  y  y'  x + y  x' + y'
+-mono {x} {y} {x'} {y'} p q = ≤-trans (+x-mono y p) (x+-mono q)

x+-mono-< : {x y z : Brw}  y < z  x + y < x + z
x+-mono-< {x} {y} {z} y<z = x+-mono y<z


{- # Multiplication -}

mutual

  _·_ : Brw  Brw  Brw
  x · zero = zero
  x · (succ y) = x · y + x
  x · (limit f {f↑}) with decZero x
  ... | yes x≡zero = zero
  ... | no x≢zero = limit  n  x · (f n)) {x·-increasing x≢zero f↑}
  x · (bisim f {f↑} g {g↑} (f≲g , g≲f) i) with decZero x
  ... | yes x≡zero = refl {x = zero} i
  ... | no x≢zero = bisim  n  x · f n) {x·-increasing x≢zero f↑}
                           n  x · g n) {x·-increasing x≢zero g↑}
                          (x·-preserves-≲ f≲g , x·-preserves-≲ g≲f) i
  x · (trunc y z p q i j) =  trunc (x · y) (x · z)  j  x · (p j))  j  x · (q j)) i j

  x·-mono :  {x y z : Brw}  y  z  x · y  x · z
  x·-mono ≤-zero = ≤-zero
  x·-mono (≤-trans y≤w w≤z) = ≤-trans (x·-mono y≤w) (x·-mono w≤z)
  x·-mono {x} (≤-succ-mono {y} {z} y≤z) = +x-mono x (x·-mono {x} y≤z)
  x·-mono {x} {y} (≤-cocone f {k = k} y≤z) with decZero x
  ... | yes x≡zero = subst  z  z  zero) (sym (zero·y≡zero y)  cong ( y) (sym x≡zero)) ≤-refl
  ... | no x≢zero = ≤-cocone  n  x · f n) {k = k} (x·-mono y≤z)
  x·-mono {x} (≤-limiting f f≤z) with decZero x
  ... | yes x≡zero = ≤-zero
  ... | no x≢zero = ≤-limiting  n  x · f n) λ k  x·-mono (f≤z k)
  x·-mono (≤-trunc p q i) = ≤-trunc (x·-mono p) (x·-mono q) i

  zero·y≡zero :  y  zero · y  zero
  zero·y≡zero zero = refl
  zero·y≡zero (succ y) = zero·y≡zero y
  zero·y≡zero (limit f) = refl
  zero·y≡zero (bisim f g x i) = refl
  zero·y≡zero (trunc x y p q i j) =
    isProp→SquareP {B = λ i j  trunc (zero · x) (zero · y)
                                       j₁  zero · p j₁)  j₁  zero · q j₁) i j
                               zero}
                    i j  Brw-is-set _ _)
                    j  zero·y≡zero x)
                    j  zero·y≡zero y)
                    j  zero·y≡zero (p j))
                    j  zero·y≡zero (q j)) i j

  x·-mono-< : {x y z : Brw}  ¬ (x  zero)  y < z  x · y < x · z
  x·-mono-< {x} x≢zero y<z = <∘≤-in-< (x+-mono-< (zero≠x→zero<x _ λ zero≡x  x≢zero (sym zero≡x)))
                                      (x·-mono {x} y<z)

  x·-increasing :  {x f}  ¬ (x  zero)  increasing f  increasing  n  x · f n)
  x·-increasing {x} {f} x≢zero f↑ k = x·-mono-< x≢zero (f↑ k)

  -- See the discussion in Line 58.
  {-# TERMINATING #-}
  x·-preserves-≲ :  {x f g}  f  g  ((x ·_)  f)  ((x ·_)  g)
  x·-preserves-≲ f≲g k = ∥-∥rec propTruncIsProp  { (l , fk≤gl)   l , x·-mono fk≤gl  }) (f≲g k)


·x-mono :  {x y}  (z : Brw)  x  y  x · z  y · z
·x-mono {x} {y} z x≤y = Brw-ind  z  x · z  y · z)
                                 z  ≤-trunc)
                                ≤-refl
                                 {z} ih  +-mono ih x≤y)
                                (limit-case x≤y)
                                z
 where
  limit-case :  {x} {y} {f} {f↑}  x  y  (∀ k  (x · f k)  (y · f k)) 
                 (x · limit f {f↑})  (y · limit f {f↑})
  limit-case {x} {y} {f} {f↑} x≤y ih with decZero x | decZero y
  ... | yes x≡zero | _ = ≤-zero
  ... | no x≢zero | yes y≡zero =
    ⊥.rec (<-irreflexive _ (subst  z  zero < z) y≡zero
                                  (<∘≤-in-< (zero≠x→zero<x _ λ zero≡x  x≢zero (sym zero≡x)) x≤y)))
  ... | no x≢zero | no y≠zero = weakly-bisimilar→lim≤lim  n  x · f n)
                                                          n  y · f n)
                                                          k   k , ih k )

+-not-zero-not-zero :  {a b}  ¬ (a  zero)  ¬ (b + a  zero)
+-not-zero-not-zero {a} {b} =
  Brw-ind  a  ¬ (a  zero)  ¬ (b + a  zero))
           a  isProp→ (isProp¬ _))
           a≢zero  ⊥.rec (a≢zero refl))
           _ _  λ zero≡succ  zero≠succ (sym zero≡succ))
           _ _  λ lim≡succ  zero≠lim (sym lim≡succ))
          a

·-no-zero-divisors :  {a b}  ¬ (a  zero)  ¬ (b  zero)  ¬ (a · b)  zero
·-no-zero-divisors {a} {b} =
  Brw-ind  b  ¬ (a  zero)  ¬ (b  zero)  ¬ (a · b)  zero)
           x  isProp→ (isProp→ (isProp¬ _)))
           _ nonsense  nonsense)
           _ a≢zero _  +-not-zero-not-zero a≢zero)
           {f} {f↑} ih a≢zero _  limitcase a f f↑ ih a≢zero)
          b
  where
    limitcase :  a f f↑  (∀ k  ¬ a  zero  ¬ f k  zero  ¬ a · f k  zero) 
                  ¬ a  zero  ¬ a · limit f {f↑}  zero
    limitcase a f f↑ ih a≢zero with decZero a
    ... | yes a≡zero = ⊥.rec (a≢zero a≡zero)
    ... | no _ = λ p  (zero≠lim (sym p))

{- # Exponentiation -}

mutual

  _^_ : Brw  Brw  Brw
  a ^ zero = one
  a ^ (succ x) = a ^ x · a
  a ^ (limit f {f↑}) with decZeroOneMany a
  ... | inl a≡zero = zero
  ... | inr (inl a≡one) = one
  ... | inr (inr one<a) = limit  n  a ^ (f n)) {^-preserves-increasing one<a f↑}
  a ^ (bisim f {f↑} g {g↑} (f≲g , g≲f) i) with decZeroOneMany a
  ... | inl a≡zero = zero
  ... | inr (inl a≡one) = one
  ... | inr (inr one<a) = bisim  n  a ^ (f n)) {^-preserves-increasing one<a f↑}
                                 n  a ^ (g n)) {^-preserves-increasing one<a g↑}
                                (^-preserves-≲ (one<x→x≢zero one<a) f≲g ,
                                 ^-preserves-≲ (one<x→x≢zero one<a) g≲f)
                                i
  a ^ (trunc x y p q i j) = trunc (a ^ x) (a ^ y)  j  (a ^ (p j)))  j  (a ^ (q j))) i j

  zero≢a^ :  {a}  (y : Brw)  ¬ (a  zero)  ¬ zero  a ^ y
  zero≢a^ zero a≢zero = zero≠succ
  zero≢a^ (succ y) a≢zero p = ·-no-zero-divisors  p  (zero≢a^ y a≢zero) (sym p)) a≢zero (sym p)
  zero≢a^ {a} (limit f) a≢zero with decZeroOneMany a
  ... | inl a≡zero = ⊥.rec (a≢zero a≡zero)
  ... | inr (inl a≡one) = zero≠succ
  ... | inr (inr one<a) = zero≠lim
  zero≢a^ {a} (bisim f {f↑} g {g↑} (f≲g , g≲f) i) a≢zero with decZeroOneMany a
  ... | inl a≡zero = ⊥.rec (a≢zero a≡zero)
  ... | inr (inl a≡one) = zero≠succ
  ... | inr (inr one<a) =
    isProp→PathP {B = λ i  ¬ zero  bisim  n  a ^ f n)
                                            n  a ^ g n)
                                           (^-preserves-≲ (one<x→x≢zero one<a) f≲g ,
                                            ^-preserves-≲ (one<x→x≢zero one<a) g≲f) i}
                  i  isProp¬ _)
                 zero≠lim
                 zero≠lim
                 i
  zero≢a^ {a} (trunc x y p q i j) a≢zero =
    isProp→SquareP {B = λ i j  ¬ zero  a ^ (trunc x y p q i j)}
                    i j  isProp¬ _)
                   refl
                   refl
                    j  zero≢a^ (p j) a≢zero)
                    j  zero≢a^ (q j) a≢zero)
                   i j

  one^y≡one :  y  one ^ y  one
  one^y≡one zero = refl
  one^y≡one (succ y) = zero+y≡y (one ^ y)  one^y≡one y
  one^y≡one (limit f) = refl
  one^y≡one (bisim f g p i) = refl
  one^y≡one (trunc x y p q i j) =
    isProp→SquareP {B = λ i j  trunc (one ^ x) (one ^ y)
                                       j₁  one ^ p j₁)  j₁  one ^ q j₁) i j
                               one}
                    i j  Brw-is-set _ _)
                   refl
                   refl
                    j  one^y≡one (p j))
                    j  one^y≡one (q j))
                   i j

  a^-mono : {a x y : Brw}  ¬ (a  zero)  x  y  a ^ x  a ^ y
  a^-mono a≢zero (≤-zero {y}) = zero≠x→zero<x _ (zero≢a^ y a≢zero)
  a^-mono a≢zero (≤-trans x≤z z≤y) = ≤-trans (a^-mono a≢zero x≤z) (a^-mono a≢zero z≤y)
  a^-mono {a} a≢zero (≤-succ-mono {x} {y} x≤y) = ·x-mono a (a^-mono a≢zero x≤y)
  a^-mono {a} a≢zero (≤-cocone {x} f {k = k} x≤fk) with decZeroOneMany a
  ... | inl a≡zero = ⊥.rec (a≢zero a≡zero)
  ... | inr (inl a≡one) = subst  z  z  one) (sym (cong (_^ x) a≡one  one^y≡one x)) ≤-refl
  ... | inr (inr one<a) = ≤-cocone  n  a ^ (f n)) {k = k} (a^-mono a≢zero x≤fk)
  a^-mono {a} a≢zero (≤-limiting f {f↑} {y} f≤y) with decZeroOneMany a
  ... | inl a≡zero = ⊥.rec (a≢zero a≡zero)
  ... | inr (inl a≡one) = subst  z  one  z) (sym (cong (_^ y) a≡one  one^y≡one y)) ≤-refl
  ... | inr (inr one<a) = ≤-limiting  n  a ^ (f n))  k  a^-mono a≢zero (f≤y k))
  a^-mono a≢zero (≤-trunc p q i) = ≤-trunc (a^-mono a≢zero p) (a^-mono a≢zero q) i

  -- See the discussion in Line 58.
  {-# TERMINATING #-}
  ^-preserves-≲ :  {a f g}  ¬ a  zero  f  g  ((a ^_)  f)  ((a ^_)  g)
  ^-preserves-≲ a≢zero f≲g k = ∥-∥rec propTruncIsProp
                                       { (l , fk≤gl)   l , a^-mono a≢zero fk≤gl  })
                                      (f≲g k)

  ^-preserves-increasing :  {a f}  one < a  increasing f  increasing  n  a ^ f n)
  ^-preserves-increasing {a} {f} one<a f↑ k =
    <∘≤-in-< (subst  z  z < a ^ f k · a)
                    (zero+y≡y (a ^ (f k)))
                    (x·-mono-<  p  zero≢a^ (f k) (one<x→x≢zero one<a)  (sym p)) one<a))
             (a^-mono (one<x→x≢zero one<a) (f↑ k))

{- # Powers of ω, in particular -}

ω : Brw
ω = limit ι {ι-increasing}

ω^ : Brw  Brw
ω^ b = ω ^ b

ω^-mono : {x y : Brw}  x  y  ω^ x  ω^ y
ω^-mono = a^-mono λ ω≡zero  zero≠lim (sym ω≡zero)

ω^-preserves-increasing :  {f}  increasing f  increasing  n  ω ^ f n)
ω^-preserves-increasing f↑ = ^-preserves-increasing one<lim f↑

-- ω^ b satisfies the expected equations definitionally:

ω^zero≡one : ω^ zero  one
ω^zero≡one = refl

ω^⟨sx⟩≡ω^x·ω :  x  ω^ (succ x)  ω^ x · ω
ω^⟨sx⟩≡ω^x·ω x = refl

ω^⟨limf⟩≡lim⟨ω^⟨fn⟩⟩ :  f f↑  ω^ (limit f {f↑})  limit  n  ω^ (f n))
ω^⟨limf⟩≡lim⟨ω^⟨fn⟩⟩ f f↑ = refl