----------------------------------------------------------------------------------------------------
-- 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  _+_
infixr  _·_
infixr  _^_

{- 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 = } (x+-increasing (f ))
  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 )))
                   (≤-cocone _ (x+-increasing (g )))
                   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