----------------------------------------------------------------------------------------------------
-- Properties of arithmetic operations on Brouwer trees
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

module BrouwerTree.Arithmetic.Properties where

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

open import Cubical.Data.Nat
  using (ℕ; zero; suc; ·-comm)
  renaming (_+_ to _N+_; _·_ to _N·_; +-assoc to N+-assoc)
import Cubical.Data.Nat.Order as N
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Empty as ⊥

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

open import Cubical.Relation.Nullary

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


{- More general lemmas -}

N≤-k· : ∀ {m n k} → m N.≤ n → k N· m N.≤ k N· n
N≤-k· {m} {n} {k} m≤n = subst (λ z → fst z N.≤ snd z)
                              (λ i → ·-comm m k i , ·-comm n k i)
                              (N.≤-·k m≤n)

ι-+-commutes : ∀ n m → ι (m N+ n) ≡ ι n + ι m
ι-+-commutes n zero = refl
ι-+-commutes n (suc m) = cong succ (ι-+-commutes n m)

ι-·-commutes : ∀ n m → ι (m N· n) ≡ ι n · ι m
ι-·-commutes n zero = refl
ι-·-commutes n (suc m) = ι-+-commutes (m N· n) n ∙ cong (_+ ι n) (ι-·-commutes n m)

increasing→monotone : ∀ {f : ℕ → Brw} → increasing f → ∀ {n m} → n N.≤ m → f n ≤ f m
increasing→monotone {f} f↑ {n} {m} (k , k+n≡m) = helper {n} {m} k k+n≡m where
  helper : ∀ {n} {m} → (k : ℕ) → k N+ n ≡ m → f n ≤ f m
  helper zero n≡m = ≤-refl-≡ (cong f n≡m)
  helper {n} {m} (suc k) sk+n≡m = subst (λ z → f n ≤ f z) sk+n≡m
                                        (≤-trans (helper k refl) (<-in-≤ (f↑ (k N+ n))))

increasing→zero<fsuc : ∀ {f : ℕ → Brw} {k} → increasing f → zero < f (suc k)
increasing→zero<fsuc {f} {zero} f↑ = ≤∘<-in-< ≤-zero (f↑ )
increasing→zero<fsuc {f} {suc k} f↑ = <-trans _ _ _ (increasing→zero<fsuc {f} {k} f↑) (f↑ (suc k))

succ-from : Brw → ℕ → Brw
succ-from x zero = x
succ-from x (suc n) = succ (succ-from x n)

succ-from-increasing : {x : Brw} → increasing (succ-from x)
succ-from-increasing zero = ≤-refl
succ-from-increasing (suc k) = ≤-succ-mono (succ-from-increasing k)

{- Lemmas about properties of arithmetic operations -}

+-assoc : ∀ {a b} c → a + (b + c) ≡ (a + b) + c
+-assoc {a} {b} =
  Brw-ind (λ c → a + (b + c) ≡ (a + b) + c)
          (λ c → isSetBrw _ _)
          refl
          (λ {x} ih → cong succ ih)
          (λ {f} {f↑} ih → limit-pointwise-equal _ _ ih)

·-+-distributivity : ∀ {a b} c → a · b + a · c ≡ a · (b + c)
·-+-distributivity {a} {b} =
  Brw-ind (λ c → a · b + a · c ≡ a · (b + c))
          (λ c → isSetBrw _ _)
          refl
          (λ {x} ih → +-assoc {a · b} {a · x} a ∙ cong (_+ a) ih)
          limitCase
 where
  limitCase : ∀ {f} {f↑} → (∀ k → a · b + a · f k ≡ a · (b + f k)) →
                a · b + a · limit f {f↑} ≡ a · (b + limit f {f↑})
  limitCase {f} {f↑} ih with decZero a
  ... | yes a≡zero = cong (_· b) a≡zero ∙ zero·y≡zero b
  ... | no a≡zero = limit-pointwise-equal _ _ ih


·-assoc : ∀ {a b} c → a · (b · c) ≡ (a · b) · c
·-assoc {a} {b} =
  Brw-ind (λ c → a · (b · c) ≡ (a · b) · c)
          (λ c → isSetBrw _ _)
          refl
          (λ {a'} ih → sym (·-+-distributivity {a} {b · a'} b) ∙ cong (λ z → z + a · b) ih)
          limitCase
 where
  limitCase : ∀ {f} {f↑} → (∀ k → a · b · f k ≡ (a · b) · f k) →
                a · b · limit f ≡ (a · b) · limit f {f↑}
  limitCase {f} {f↑} ih with decZero b | decZero (a · b)
  limitCase {f} {f↑} ih | yes b≡zero | yes ab≡zero = refl
  limitCase {f} {f↑} ih | yes b≡zero | no  ab≢zero =
      ⊥.rec (ab≢zero (subst (λ z → a · z ≡ zero) (sym b≡zero) refl))
  limitCase {f} {f↑} ih | no  b≢zero | yes ab≡zero with decZero a
  limitCase {f} {f↑} ih | no  b≢zero | yes ab≡zero | yes a≡zero = refl
  limitCase {f} {f↑} ih | no  b≢zero | yes ab≡zero | no  a≢zero =
      ⊥.rec (·-no-zero-divisors a≢zero b≢zero ab≡zero)
  limitCase {f} {f↑} ih | no  b≢zero | no  ab≢zero with decZero a
  limitCase {f} {f↑} ih | no  b≢zero | no  ab≢zero | yes a≡zero =
      ⊥.rec (ab≢zero (subst (λ z → z · b ≡ zero) (sym a≡zero) (zero·y≡zero b)))
  limitCase {f} {f↑} ih | no  b≢zero | no  ab≢zero | no  a≢zero =
      bisim (λ n → a · b · f n) (λ n → (a · b) · f n)
            ((λ k → ∣ k , ≤-refl-≡ (ih k) ∣) , λ k → ∣ k , ≤-refl-≡ (sym (ih k)) ∣)

exp-homomorphism : ∀ {a b c} → a ^ (b + c) ≡ a ^ b · a ^ c
exp-homomorphism {a} {b} {c} =
  Brw-ind (λ c → a ^ (b + c) ≡ a ^ b · a ^ c)
          (λ c → isSetBrw _ _)
          (sym (zero+y≡y (a ^ b)))
          (λ {a'} ih → cong (_· a) ih ∙ sym (·-assoc {a ^ b} {a ^ a'} a))
          limitCase
          c
 where
  limitCase : ∀ {f} {f↑} → (∀ k → a ^ (b + f k) ≡ a ^ b · a ^ f k) →
                a ^ (b + limit f {f↑}) ≡ a ^ b · a ^ limit f {f↑}
  limitCase {f} {f↑} ih with decZeroOneMany a
  limitCase {f} {f↑} ih | inl a≡zero = refl
  limitCase {f} {f↑} ih | inr (inl a≡one) = sym (zero+y≡y (a ^ b) ∙ cong (_^ b) a≡one ∙ one^y≡one b)
  limitCase {f} {f↑} ih | inr (inr one<a) with decZero (a ^ b)
  limitCase {f} {f↑} ih | inr (inr one<a) | yes a^b≡zero =
      ⊥.rec (zero≢a^ b (one<x→x≢zero one<a) (sym a^b≡zero))
  limitCase {f} {f↑} ih | inr (inr one<a) | no  a^b≢zero =
      bisim (λ n → a ^ (b + f n)) (λ n → a ^ b · a ^ f n)
            ((λ k → ∣ k , ≤-refl-≡ (ih k) ∣) , λ k → ∣ k , ≤-refl-≡ (sym (ih k)) ∣)

one·y≡y : (y : Brw) → one · y ≡ y
one·y≡y =
  Brw-ind (λ y → one · y ≡ y)
          (λ y → isSetBrw _ _)
          refl
          (cong succ)
          (λ {f} {f↑} ih → bisim (λ n → one · f n) f
                                 ((λ k → ∣ k , ≤-refl-≡ (ih k) ∣) ,
                                  (λ k → ∣ k , ≤-refl-≡ (sym (ih k)) ∣)))

ω=ω^1 : ω ≡ ω^ one
ω=ω^1 = bisim ι (λ n → one · ι n)
              ((λ k → ∣ k , ≤-refl-≡ (sym (one·y≡y (ι k))) ∣) ,
               (λ k → ∣ k , ≤-refl-≡ (one·y≡y (ι k)) ∣))

ω-absorbs-finite : ∀ n → ι (suc n) · ω ≡ ω
ω-absorbs-finite zero =
  bisim (λ n → succ zero · ι n) ι
        ((λ k → ∣ k , ≤-refl-≡ (one·y≡y (ι k)) ∣) ,
         (λ k → ∣ k , ≤-refl-≡ (sym (one·y≡y (ι k))) ∣))
ω-absorbs-finite (suc n) =
  bisim (λ k → succ (succ (ι n)) · ι k) (λ k → succ (ι n) · ι k)
        ((λ k → ∣ k N+ k , subst (λ z → fst z ≤ snd z)
                                 (λ i → (cong ι (·-comm (suc (suc n)) k) ∙
                                         ι-·-commutes (suc (suc n)) k) i ,
                                        (cong ι (·-comm (suc n) (k N+ k)) ∙
                                         ι-·-commutes (suc n) (k N+ k)) i)
                                 (increasing→monotone ι-increasing (n+2·k≤⟨n+1⟩·2k n k)) ∣) ,
         (λ k → ∣ k , ·x-mono (ι k) ≤-succ-incr-simple ∣))
  ∙ ω-absorbs-finite n
 where
  n+2·k≤⟨n+1⟩·2k : ∀ n k → (suc (suc n)) N· k N.≤ (suc n) N· (k N+ k)
  n+2·k≤⟨n+1⟩·2k n k = subst (λ z → z N.≤ (suc n) N· (k N+ k))
                             (sym (N+-assoc k k (n N· k)))
                             (N.≤-k+ {k = k N+ k} (N≤-k· {k = n} (N.≤-+k {k = k} N.zero-≤)))

ω^x-absorbs-finite : ∀ {x n} → zero < x → ι (suc n) · ω^ x ≡ ω^ x
ω^x-absorbs-finite {x} {n} =
  Brw-ind (λ x → zero < x → ι (suc n) · ω^ x ≡ ω^ x)
          (λ x → isProp→ (isSetBrw _ _))
          (λ zero<zero → ⊥.rec (<-irreflexive _ zero<zero))
          sucCase
          (λ {f} {f↑} ih _ →
             limit-skip-first (λ k → succ (ι n) · ω ^ f k)
           ∙ bisim (λ k → succ (ι n) · ω ^ f (suc k)) (λ k → ω ^ f k)
                   ((λ k → ∣ suc k , ≤-refl-≡ (ih (suc k) (increasing→zero<fsuc f↑)) ∣) ,
                    (λ k → ∣ k , ≤-trans (ω^-mono (<-in-≤ (f↑ k)))
                                         (≤-refl-≡ (sym (ih (suc k)(increasing→zero<fsuc f↑)))) ∣)))
          x
 where
  sucCase : ∀ {x'} → (zero < x' → ι (suc n) · ω^ x' ≡ ω^ x') →
              zero < succ x' → ι (suc n) · ω^ (succ x') ≡ ω^ (succ x')
  sucCase {x'} ih zero<sx' with decZero x'
  ... | yes x'≡zero = subst (λ z → ι (suc n) · z ≡ z)
                            (ω=ω^1 ∙ cong (λ z → ω^ (succ z)) (sym x'≡zero))
                            (ω-absorbs-finite n)
  ... | no  x'≢zero = ·-assoc {ι (suc n)} {ω^ x'} ω
                    ∙ cong (_· ω) (ih (zero≠x→zero<x _ (λ zero≡x → x'≢zero (sym zero≡x))))


{- Lemmas about ω^ c -}

ω^-mono-< : {x y : Brw} → x < y → ω^ x < ω^ y
ω^-mono-< {x} {y} x<y with decZero (ω^ x)
... | yes ω^x≡zero = ⊥.rec (zero≢a^ x (λ ω≡zero → zero≠lim (sym ω≡zero)) (sym ω^x≡zero) )
... | no ω^x≢zero = ≤-trans (ω^-preserves-increasing {succ-from x} succ-from-increasing zero)
                            (ω^-mono x<y)

zero<ω^c : (c : Brw) → zero < ω^ c
zero<ω^c c = zero≠x→zero<x _ (zero≢a^ c λ ω≡zero → zero≠lim (sym ω≡zero))

a<omega^a : {a : Brw} → a ≤ ω^ a
a<omega^a {a} =
  Brw-ind (λ a → a ≤ ω^ a)
          (λ a → ≤-trunc)
          ≤-zero
          (λ {a} ih → ≤-trans (≤-succ-mono ih) (ω^-mono-< (<-succ-incr-simple {a})))
          (λ {f} {f↑} ih → weakly-bisimilar→lim≤lim f _ λ k → ∣ k , ih k ∣)
          a

ω^one≡ω : ω^ one ≡ ω
ω^one≡ω = bisim _ _ ((λ k → ∣ k , ≤-refl-≡ (one·y≡y _) ∣) ,
                     (λ k → ∣ k , ≤-refl-≡ (sym (one·y≡y _)) ∣))

{- Brouwer ordinals of the form ω^ c are additive principal -}

is-additive-principal : Brw → Type
is-additive-principal x = (a : Brw) → a < x → a + x ≡ x

is-additive-principal-≤ : ∀ {x} → (∀ a → a < x → a + x ≤ x) → is-additive-principal x
is-additive-principal-≤ {x} p a a<x =
  antisym (p a a<x) (subst (λ z → z ≤ a + x) (zero+y≡y x) (+x-mono x ≤-zero))

additive-principal-ω^ : ∀ (c : Brw) → is-additive-principal (ω^ c)
additive-principal-ω^ =
  Brw-ind (λ c → is-additive-principal (ω^ c))
          (λ c → isPropΠ (λ a → isProp→ (isSetBrw _ _)))
          (λ a sa≤one → cong succ (x≤zero→x≡zero (≤-succ-mono⁻¹ sa≤one)))
          (λ {c} _ → additive-principal-ω^succ c)
          (λ {f} {f↑} ih → additive-principal-ω^lim f f↑ ih)
 where
  additive-principal-ω^succ : ∀ c → is-additive-principal (ω^ (succ c))
  additive-principal-ω^succ c with decZero (ω^ c)
  ... | yes x = λ a a<zero → ⊥.rec (succ≰zero a<zero)
  ... | no qq =
    is-additive-principal-≤ (λ a a<ω^c·ω →
      weakly-bisimilar→lim≤lim _ _
        (λ k → ∥-∥rec propTruncIsProp
          (λ (l , a<ω^c·l ) →
            ∣ k N+ l , ≤-trans (+x-mono (ω^ c · ι k) (<-in-≤ a<ω^c·l))
                               (≤-refl-≡ (·-+-distributivity {ω^ c} {ι l} (ι k)
                                        ∙ cong (ω^ c ·_) (sym (ι-+-commutes l k)))) ∣)
        (below-limit-lemma _ _ a<ω^c·ω)))

  additive-principal-ω^lim : ∀ f f↑ → ((k : ℕ) → is-additive-principal (ω^ (f k))) →
                               is-additive-principal (ω^ (limit f {f↑}))
  additive-principal-ω^lim f f↑ ih =
    is-additive-principal-≤ (λ a a<ω^fn →
                               weakly-bisimilar→lim≤lim _ _
                                 (λ k → ∥-∥rec propTruncIsProp (λ (l , a<ω^fl) → helper k l a<ω^fl)
                                                               (below-limit-lemma _ _ a<ω^fn)))
   where
    helper : ∀ {a} k l (a<ω^fn : a < ω^ (f l)) → ∃[ n ∈ ℕ ] (a + ω ^ f k) ≤ (ω ^ f n)
    helper {a} k l a<ω^fl with k N.≟ l
    ... | N.lt k<l =
      ∣ l , ≤-trans (x+-mono {a} {ω^ (f k)} {ω^ (f l)}
                            (ω^-mono (increasing→monotone f↑ (N.<-weaken k<l))))
                    (≤-refl-≡ (ih l a a<ω^fl)) ∣
    ... | N.eq k≡l = ∣ l , ≤-refl-≡ (cong (λ z → a + ω^ (f z)) k≡l ∙ ih l a a<ω^fl) ∣
    ... | N.gt l<k =
      ∣ k , ≤-refl-≡ (ih k a (≤-trans a<ω^fl (ω^-mono (increasing→monotone f↑ (N.<-weaken l<k))))) ∣

additive-principal-ω^-closure : ∀ {a b c} → a < ω^ c → b < ω^ c → a + b < ω^ c
additive-principal-ω^-closure {a} {b} {c} a<ω^c b<ω^c =
  <∘≤-in-< (x+-mono-< b<ω^c) (≤-refl-≡ (additive-principal-ω^ c a a<ω^c))

{- Definitions of ε₀ and proof that it is a fixed point of ω^ -}

ω↑↑ : ℕ → Brw
ω↑↑        = one
ω↑↑ (suc i) = ω^ (ω↑↑ i)

ω↑↑-↑ : increasing ω↑↑
ω↑↑-↑        = subst (λ z → one < z) (sym ω^one≡ω) (<-cocone-simple ι {k = })
ω↑↑-↑ (suc i) = ω^-mono-< (ω↑↑-↑ i)

ε₀ : Brw
ε₀ = limit ω↑↑ {ω↑↑-↑}

ε₀≡ω^ε₀ : ε₀ ≡ ω^ ε₀
ε₀≡ω^ε₀ = antisym (weakly-bisimilar→lim≤lim ω↑↑ (λ n → limit ι ^ ω↑↑ n)
                                            (λ k → ∣ k , a<omega^a ∣))
                  (weakly-bisimilar→lim≤lim (λ n → limit ι ^ ω↑↑ n) ω↑↑
                                            (λ k → ∣ suc k , ≤-refl ∣))