----------------------------------------------------------------------------------------------------
-- 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  m N.≤ k  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 · ι m
ι-·-commutes n zero = refl
ι-·-commutes n (suc m) = ι-+-commutes (m  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↑ 0)
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))  k N.≤ (suc n)  (k N+ k)
  n+2·k≤⟨n+1⟩·2k n k = subst  z  z N.≤ (suc n)  (k N+ k))
                             (sym (N+-assoc k k (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
ω↑↑  0      = one
ω↑↑ (suc i) = ω^ (ω↑↑ i)

ω↑↑-↑ : increasing ω↑↑
ω↑↑-↑  0      = subst  z  one < z) (sym ω^one≡ω) (<-cocone-simple ι {k = 1})
ω↑↑-↑ (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 ))