----------------------------------------------------------------------------------------------------
-- Multiplication of Cantor Normal Forms
----------------------------------------------------------------------------------------------------

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

module CantorNormalForm.Multiplication where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sum
open import Cubical.Data.Empty
  renaming (rec to ⊥-rec)
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
  using (ℕ ; zero ; suc)
open import Cubical.Data.Nat.Order.Recursive
  renaming (_<_ to _<ᴺ_)
  using ()

open import CantorNormalForm.Base
open import CantorNormalForm.Addition

open import Abstract.ZerSucLim _<_ _≤_


{- Multiplication -}

infixl  _·_ _•_

mutual

 _·_ : Cnf → Cnf → Cnf
 𝟎 · b = 𝟎
 a · 𝟎 = 𝟎
 a · (ω^ 𝟎 + d [ r ]) = a + a · d
 (ω^ a + c [ r ]) · (ω^ b@(ω^ _ + _ [ _ ]) + d [ s ]) =
     ω^ (a + b) + (ω^ a + c [ r ] · d) [ ≥left· (ω^ a + c [ r ]) b d <₁ s ]

 ≥left· : ∀ x b d → b > 𝟎 → b ≥ left d → left x + b ≥ left (x · d)
 ≥left· 𝟎 b d b>𝟎 _ = 𝟎≤
 ≥left· x@(ω^ a + c [ r ]) b@(ω^ _ + _ [ _ ]) 𝟎 <₁ _ = 𝟎≤
 ≥left· x@(ω^ a + c [ r ]) b@(ω^ _ + _ [ _ ]) (ω^ 𝟎 + d' [ t ]) <₁ _ = goal
  where
   claim : a + b ≥ a
   claim = ≤+r a b
   IH : a + b ≥ left (x · d')
   IH = ≥left· x b d' <₁ (≤-trans t 𝟎≤)
   goal : a + b ≥ left (x + x · d')
   goal = ≥left+ x (x · d') claim IH
 ≥left· x@(ω^ a + c [ r ]) b@(ω^ _ + _ [ _ ]) (ω^ d@(ω^ _ + _ [ _ ]) + d' [ _ ]) <₁ d≤b = goal
  where
   goal : a + b ≥ a + d
   goal = +r-is-≤-monotone a d b d≤b

{- Some properties of multiplication -}

·𝟎-is-𝟎 : ∀ a → a · 𝟎 ≡ 𝟎
·𝟎-is-𝟎  𝟎               = refl
·𝟎-is-𝟎 (ω^ a + b [ r ]) = refl

·𝟏-is-identity : ∀ a → a · 𝟏 ≡ a
·𝟏-is-identity  𝟎               = refl
·𝟏-is-identity (ω^ a + b [ r ]) = refl

·+𝟏-spec : (a b : Cnf) → a · (b + 𝟏) ≡ a · b + a
·+𝟏-spec 𝟎 b = refl
·+𝟏-spec (ω^ a + c [ r ]) 𝟎 = refl
·+𝟏-spec (ω^ a + c [ r ]) (ω^ b + d [ s ]) with <-tri b 𝟎
·+𝟏-spec x@(ω^ a + c [ r ]) (ω^ 𝟎 + d [ s ]) | inr _ = goal
 where
  IH : x · (d + 𝟏) ≡ x · d + x
  IH = ·+𝟏-spec x d
  claim₀ : x + x · (d + 𝟏) ≡ x + (x · d + x)
  claim₀ = cong (x +_) IH
  claim₁ : x + (x · d + x) ≡ x + x · d + x
  claim₁ = +-is-assoc x (x · d) x
  goal : x + x · (d + 𝟏) ≡ (x + x · d) + x
  goal = claim₀ ∙ claim₁
·+𝟏-spec x@(ω^ a + c [ r ]) (ω^ y@(ω^ _ + _ [ _ ]) + d [ s ]) | inr _ =
   ω^ (a + y) + x · (d + 𝟏) [ _ ]
  ≡⟨ ω^+≡ω^⟨⟩+ _ _ ⟩
   ω^⟨ a + y ⟩ + x · (d + 𝟏)
  ≡⟨ cong (ω^⟨ a + y ⟩ +_) (·+𝟏-spec x d) ⟩
   ω^⟨ a + y ⟩ + (x · d + x)
  ≡⟨ +-is-assoc ω^⟨ a + y ⟩ (x · d) x ⟩
   ω^⟨ a + y ⟩ + x · d + x
  ≡⟨ cong (_+ x) (sym (ω^+≡ω^⟨⟩+ _ _)) ⟩
   ω^ (a + y) + x · d [ _ ] + x ∎

ω^·ω^>𝟎 : ∀ a b → a > 𝟎 → b > 𝟎 → a · b > 𝟎
ω^·ω^>𝟎 a@(ω^ _ + _ [ _ ]) (ω^ 𝟎 + b' [ s ]) <₁ <₁ = <∘≤-in-< <₁ (≤+r a (a · b'))
ω^·ω^>𝟎 a@(ω^ _ + _ [ _ ]) (ω^ b@(ω^ _ + _ [ _ ]) + b' [ s ]) <₁ <₁ = <₁

left⟨·nat⟩ : ∀ a b → left b ≡ 𝟎 → left a ≡ left (a + a · b)
left⟨·nat⟩ 𝟎 b _ = refl
left⟨·nat⟩ (ω^ a + c [ r ]) 𝟎 e = refl
left⟨·nat⟩ x@(ω^ a + c [ r ]) (ω^ 𝟎 + d [ s ]) _ = goal
 where
  IH : a ≡ left (x + x · d)
  IH = left⟨·nat⟩ x d (≤𝟎→≡𝟎 s)
  goal : a ≡ left (x + (x + x · d))
  goal = left⟨+⟩ x (x + x · d) (inr IH)
left⟨·nat⟩ (ω^ a + c [ r ]) (ω^ b@(ω^ _ + _ [ _ ]) + d [ s ]) b≡𝟎 = ⊥-rec (ω≢𝟎 b≡𝟎)

left⟨·nat⟩⁻¹ : ∀ a b → a > 𝟎 → left (a · b) ≤ left a → left b ≡ 𝟎
left⟨·nat⟩⁻¹ _ 𝟎 <₁ _ = refl
left⟨·nat⟩⁻¹ _ (ω^ 𝟎 + _ [ _ ]) <₁ _ = refl
left⟨·nat⟩⁻¹ _ (ω^ (ω^ _ + _ [ _ ]) + _ [ _ ]) <₁ v = ⊥-rec (≤→≯ v (<+r _ _ <₁))

·nat<ω^ : ∀ a b c {d u} → left b ≡ 𝟎 → c > 𝟎 → a · b < ω^ (left a + c) + d [ u ]
·nat<ω^ a 𝟎 (ω^ c + c' [ t ]) e <₁ = subst (_< ω^ (left a + _) + _ [ _ ]) (sym (·𝟎-is-𝟎 a)) <₁
·nat<ω^ 𝟎 (ω^ 𝟎 + b' [ s ]) (ω^ c + c' [ t ]) e <₁ = <₁
·nat<ω^ x@(ω^ a + a' [ r ]) (ω^ 𝟎 + b' [ s ]) z@(ω^ c + c' [ t ]) {d} {u} e <₁ = goal
 where
  IH : x · b' < ω^ (a + z) + d [ u ]
  IH = ·nat<ω^ x b' z (≤𝟎→≡𝟎 s) <₁
  claim₀ : x + x · b' < x + ω^ (a + z) + d [ u ]
  claim₀ = +r-is-<-monotone x (x · b') (ω^ (a + z) + d [ u ]) IH
  claim₁ : x + ω^ (a + z) + d [ u ] ≡ ω^ (a + z) + d [ u ]
  claim₁ with <-tri a (a + z)
  claim₁ | inl a<a+z = refl
  claim₁ | inr a≥a+z = ⊥-rec (≤→≯ a≥a+z (<+r a z <₁))
  goal : x + x · b' < ω^ (a + z) + d [ u ]
  goal = subst (_ <_) claim₁ claim₀
·nat<ω^ a (ω^ (ω^ _ + _ [ _ ]) + b' [ s ]) (ω^ c + c' [ t ]) e <₁ = ⊥-rec (ω≢𝟎 e)

ω^·-is-<-monotone : ∀ x y z → x > 𝟎 → y < z → x · y < x · z
ω^·-is-<-monotone x@(ω^ _ + _ [ _ ]) 𝟎 y@(ω^ _ + _ [ _ ]) <₁ <₁ = ω^·ω^>𝟎 x y <₁ <₁
ω^·-is-<-monotone x@(ω^ _ + _ [ _ ])
                  y@(ω^ 𝟎 + b' [ s ])
                  z@(ω^ 𝟎 + c' [ t ]) <₁ (<₃ e b'<c') = goal
 where
  IH : x · b' < x · c'
  IH = ω^·-is-<-monotone x b' c' <₁ b'<c'
  goal : x + x · b' < x + x · c'
  goal = +r-is-<-monotone x _ _ IH
ω^·-is-<-monotone x@(ω^ a + _ [ _ ])
                  y@(ω^ 𝟎 + _ [ _ ])
                  z@(ω^ c@(ω^ _ + _ [ _ ]) + c' [ _ ]) <₁ _ = goal
 where
  goal : x · y < ω^ (a + c) + x · c' [ _ ]
  goal = ·nat<ω^ x y c refl <₁
ω^·-is-<-monotone x@(ω^ _ + _ [ _ ])
                  y@(ω^ (ω^ _ + _ [ _ ]) + _ [ _ ])
                  z@(ω^ 𝟎 + _ [ _ ]) <₁ y<z = ⊥-rec (<→≯ y<z (<₂ <₁))
ω^·-is-<-monotone x@(ω^ a + _ [ _ ])
                  y@(ω^ b@(ω^ _ + _ [ _ ]) + b' [ _ ])
                  z@(ω^ c@(ω^ _ + _ [ _ ]) + c' [ _ ]) <₁ (<₂ b<c) = goal
 where
  goal : ω^ (a + b) + x · b' [ _ ] < ω^ (a + c) + x · c' [ _ ]
  goal = <₂ (+r-is-<-monotone a b c b<c)
ω^·-is-<-monotone x@(ω^ a + a' [ r ])
                  y@(ω^ b@(ω^ _ + _ [ _ ]) + b' [ s ])
                  z@(ω^ c@(ω^ _ + _ [ _ ]) + c' [ t ]) <₁ (<₃ b≡c b'<c') = goal
 where
  IH : x · b' < x · c'
  IH = ω^·-is-<-monotone x b' c' <₁ b'<c'
  goal : ω^ (a + b) + x · b' [ _ ] < ω^ (a + c) + x · c' [ _ ]
  goal = <₃ (cong (a +_) b≡c) IH

·r-is-≤-monotone : ∀ a b c → b ≤ c → a · b ≤ a · c
·r-is-≤-monotone 𝟎 b c b≤c = inr refl
·r-is-≤-monotone (ω^ a + a' [ r ]) b c (inl b<c) = inl (ω^·-is-<-monotone _ _ _ <₁ b<c)
·r-is-≤-monotone (ω^ a + a' [ r ]) b c (inr c≡b) = inr (cong ((ω^ a + a' [ r ]) ·_) c≡b)

l·-is-≤-monotone : ∀ a b c → a ≤ b → a · c ≤ b · c
l·-is-≤-monotone 𝟎 b c a≤b = 𝟎≤  -- : 𝟎 ≤ b · c
l·-is-≤-monotone a@(ω^ _ + _ [ _ ])
                 b@𝟎
                 c
                 a≤b = ⊥-rec (ω^≰𝟎 a≤b)
l·-is-≤-monotone a@(ω^ _ + _ [ _ ])
                 b@(ω^ _ + _ [ _ ])
                 c@𝟎
                 a≤b = ≤-refl  -- : 𝟎 ≤ 𝟎
l·-is-≤-monotone a@(ω^ _ + _ [ _ ])
                 b@(ω^ _ + _ [ _ ])
                 c@(ω^ 𝟎 + z [ _ ])
                 a≤b = ≤-trans a+a·z≤b+a·z b+a·z≤b+b·z  -- : a + a · z ≤ b + b · z
 where
  a+a·z≤b+a·z : a + a · z ≤ b + a · z
  a+a·z≤b+a·z = l+-is-≤-monotone a b (a · z) a≤b
  b+a·z≤b+b·z : b + a · z ≤ b + b · z
  b+a·z≤b+b·z = +r-is-≤-monotone b (a · z) (b · z) (l·-is-≤-monotone a b z a≤b)
l·-is-≤-monotone a@(ω^ u + _ [ _ ])
                 b@(ω^ v + _ [ _ ])
                 c@(ω^ w@(ω^ _ + _ [ _ ]) + z [ _ ])
                 a≤b = ≤₂' u+w≤v+w a·z≤b·z
                  -- : ω^ (u + w) + a · z [ _ ] ≤ ω^ (v + w) + b · z [ _ ]
 where
  u≤v : u ≤ v
  u≤v = ≤₂⁻¹ a≤b
  u+w≤v+w : u + w ≤ v + w
  u+w≤v+w = l+-is-≤-monotone u v w u≤v
  a·z≤b·z : a · z ≤ b · z
  a·z≤b·z = l·-is-≤-monotone a b z a≤b


·-is-left-distributive : ∀ x y z → x · (y + z) ≡ x · y + x · z
·-is-left-distributive 𝟎 y z = refl
·-is-left-distributive (ω^ a + a' [ r ]) 𝟎 z = refl
·-is-left-distributive (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) 𝟎 = sym +𝟎-is-identity
·-is-left-distributive x@(ω^ a + a' [ r ]) y@(ω^ 𝟎 + b' [ s ]) z@(ω^ 𝟎 + c' [ t ]) = goal
 where
  IH : x · (b' + z) ≡ x · b' + x · z -- ≡ x · b' + (x + x · c')
  IH = ·-is-left-distributive x b' z
  claim₀ : x + x · (b' + z) ≡ x + (x · b' + x · z)
  claim₀ = cong (x +_) IH
  claim₁ : x + (x · b' + x · z) ≡ (x + x · b') + (x + x · c')
  claim₁ = +-is-assoc x (x · b') (x · z)
  goal : x + x · (b' + z) ≡ (x + x · b') + (x + x · c')
  goal = claim₀ ∙ claim₁
·-is-left-distributive x@(ω^ a + a' [ r ])
                       y@(ω^ 𝟎 + b' [ s ])
                       z@(ω^ c@(ω^ v + v' [ _ ]) + c' [ t ]) = goal
 where
  claim₀ : a ≡ left (x + x · b')
  claim₀ = left⟨·nat⟩ x b' (≤𝟎→≡𝟎 s)
  a<a+c : a < a + c
  a<a+c = <+r a c <₁
  claim₁ : left (x + x · b') < a + c
  claim₁ = subst (_< a + c) claim₀ a<a+c
  goal : ω^ (a + c) + x · c' [ _ ] ≡ (x + x · b') + (ω^ (a + c) + x · c' [ _ ])
  goal = sym (+-left-cancel (x + x · b') _ claim₁)
·-is-left-distributive x@(ω^ a + a' [ r ])
                       y@(ω^ b@(ω^ u + u' [ _ ]) + b' [ s ])
                       z@(ω^ 𝟎 + c' [ t ]) =
    ω^ (a + b) + x · (b' + z) [ _ ]
   ≡⟨ ω^+≡ω^⟨⟩+ _ _ ⟩
    ω^⟨ a + b ⟩ + x · (b' + z)
   ≡⟨ cong (ω^⟨ a + b ⟩ +_) IH ⟩
    ω^⟨ a + b ⟩ + (x · b' + x · z)
   ≡⟨ +-is-assoc ω^⟨ a + b ⟩ (x · b') (x · z) ⟩
    (ω^⟨ a + b ⟩ + x · b') + x · z
   ≡⟨ cong (_+ x · z) (sym (ω^+≡ω^⟨⟩+ _ _)) ⟩
    (ω^ (a + b) + x · b' [ _ ]) + x · z ∎
 where
  IH : x · (b' + z) ≡ x · b' + x · z
  IH = ·-is-left-distributive x b' z
·-is-left-distributive x@(ω^ a + a' [ r ])
                       y@(ω^ b@(ω^ u + u' [ _ ]) + b' [ s ])
                       z@(ω^ c@(ω^ v + v' [ _ ]) + c' [ t ]) = goal
 where
  goal : x · (y + z) ≡ x · y + x · z
  goal with <-tri b c with <-tri u v with <-tri (a + b) (a + c)
  goal | inl b<c | inl u<v | inl a+b<a+c = refl
  goal | inl b<c | inl u<v | inr a+b≥a+c = ⊥-rec (≤→≯ a+b≥a+c (+r-is-<-monotone a b c b<c))
  goal | inl b<c | inr (inl u>v) | inl a+b<a+c = ⊥-rec (<→≯ b<c (<₂ u>v))
  goal | inl b<c | inr (inr u≡v) | inl a+b<a+c with <-tri u' v'
  goal | inl b<c | inr (inr u≡v) | inl a+b<a+c | inl u'<v' = refl
  goal | inl b<c | inr (inr u≡v) | inl a+b<a+c | inr u'≥v' = ⊥-rec (≤→≯ u'≥v' (<₃⁻¹ u≡v b<c))
  goal | inl b<c | inr u≥v | inr a+b≥a+c = ⊥-rec (≤→≯ a+b≥a+c (+r-is-<-monotone a b c b<c))
  goal | inr b≥c | inl u<v | inl a+b<a+c = ⊥-rec (≤→≯ (+r-is-≤-monotone a c b b≥c) a+b<a+c)
  goal | inr b≥c | inl u<v | inr a+b≥a+c = ⊥-rec (≤→≯ b≥c (<₂ u<v))
  goal | inr b≥c | inr u≥v | inl a+b<a+c = ⊥-rec (≤→≯ (+r-is-≤-monotone a c b b≥c) a+b<a+c)
  goal | inr b≥c | inr (inl u>v) | inr a+b≥a+c = Goal
   where
    IH : x · (b' + z) ≡ x · b' + x · z
    IH = ·-is-left-distributive x b' z
    Goal : ω^ (a + b) + x · (b' + z) [ _ ] ≡  ω^ (a + b) + (x · b' + x · z) [ _ ]
    Goal = Cnf⁼ refl IH
  goal | inr b≥c | inr (inr u≡v) | inr a+b≥a+c with <-tri u' v'
  goal | inr b≥c | inr (inr u≡v) | inr a+b≥a+c | inl u'<v' = ⊥-rec (≤→≯ b≥c (<₃ u≡v u'<v'))
  goal | inr b≥c | inr (inr u≡v) | inr a+b≥a+c | inr (inl u'>v') = Goal
   where
    IH : x · (b' + z) ≡ x · b' + x · z
    IH = ·-is-left-distributive x b' z
    Goal : ω^ (a + b) + x · (b' + z) [ _ ] ≡ ω^ (a + b) + (x · b' + x · z) [ _ ]
    Goal = Cnf⁼ refl IH
  goal | inr b≥c | inr (inr u≡v) | inr a+b≥a+c | inr (inr u'≡v') = Goal
   where
    IH : x · (b' + z) ≡ x · b' + x · z
    IH = ·-is-left-distributive x b' z
    Goal : ω^ (a + b) + x · (b' + z) [ _ ] ≡ ω^ (a + b) + (x · b' + x · z) [ _ ]
    Goal = Cnf⁼ refl IH

·ω^⟨⟩≡ω^⟨left+⟩ : ∀ a b → a > 𝟎 → b > 𝟎 → a · ω^⟨ b ⟩ ≡ ω^⟨ left a + b ⟩
·ω^⟨⟩≡ω^⟨left+⟩ x@(ω^ a + c [ r ]) y@(ω^ b + d [ s ]) <₁ <₁ = refl


ω^𝟎+-is-𝟏+ : ∀ a r → 𝟏 + a ≡ ω^ 𝟎 + a [ r ]
ω^𝟎+-is-𝟏+ 𝟎 r = Cnf⁼ refl refl
ω^𝟎+-is-𝟏+ (ω^ a + b [ s ]) (inr 𝟎≡a) with <-tri 𝟎 a
... | inl 𝟎<a = ⊥-rec (<-irreflexive 𝟎≡a 𝟎<a)
... | inr 𝟎≥a = Cnf⁼ refl refl

𝟏·-is-identity : ∀ a → 𝟏 · a ≡ a
𝟏·-is-identity 𝟎 = refl
𝟏·-is-identity ω^ 𝟎 + b [ r ] =
   𝟏 + 𝟏 · b
  ≡⟨ cong (𝟏 +_) (𝟏·-is-identity b) ⟩
   𝟏 + b
  ≡⟨ ω^𝟎+-is-𝟏+ b r ⟩
   ω^ 𝟎 + b [ r ] ∎
𝟏·-is-identity ω^ (ω^ x + y [ s ]) + b [ r ] = Cnf⁼ refl (𝟏·-is-identity b)

·ω^+-spec₀ : ∀ a {b r} → a · (ω^ 𝟎 + b [ r ]) ≡ a + a · b
·ω^+-spec₀ 𝟎 = refl
·ω^+-spec₀ ω^ _ + _ [ _ ] = refl

·ω^+-spec₁ : ∀ a b r y s →
  Σ[ c ∈ Cnf ] Σ[ t ∈ a ≥ left c ] (ω^ a + b [ r ]) · (ω^ 𝟎 + y [ s ]) ≡ ω^ a + c [ t ]
·ω^+-spec₁ a b r 𝟎 s = b , r , refl
·ω^+-spec₁ a b r (ω^ 𝟎 + v [ s' ]) s = c' , t' , p'
 where
  IH : Σ[ c ∈ Cnf ] Σ[ t ∈ a ≥ left c ] (ω^ a + b [ r ]) · (ω^ 𝟎 + v [ s' ]) ≡ ω^ a + c [ t ]
  IH = ·ω^+-spec₁ a b r v s'
  c : Cnf
  c = fst IH
  t : a ≥ left c
  t = fst (snd IH)
  p : (ω^ a + b [ r ]) · (ω^ 𝟎 + v [ s' ]) ≡ ω^ a + c [ t ]
  p = snd (snd IH)
  c' : Cnf
  c' = b + (ω^ a + c [ t ])
  t' : a ≥ left c'
  t' = ≥left+ b _ r ≤-refl
  q  : (ω^ a + b [ r ]) + (ω^ a + c [ t ]) ≡ ω^ a + c' [ t' ]
  -- ≡ ω^ a + (b + (ω^ a + c [ t ])) [ ≥left+ b _ r ≤-refl ]
  q with <-tri a a
  ... | inl a<a = ⊥-rec (<-irrefl a<a)
  ... | inr a≥a = Cnf⁼ refl refl
  p' : (ω^ a + b [ r ]) · (ω^ 𝟎 + (ω^ 𝟎 + v [ s' ]) [ s ])
     ≡ ω^ a + c' [ t' ]
  p' =
     (ω^ a + b [ r ]) · (ω^ 𝟎 + (ω^ 𝟎 + v [ s' ]) [ s ])
    ≡⟨ refl ⟩
     (ω^ a + b [ r ]) + ((ω^ a + b [ r ]) · (ω^ 𝟎 + v [ s' ]))
    ≡⟨ cong ((ω^ a + b [ r ]) +_) p ⟩
     (ω^ a + b [ r ]) + (ω^ a + c [ t ])
    ≡⟨ q ⟩
     ω^ a + c' [ t' ] ∎
·ω^+-spec₁ a b r (ω^ (ω^ _ + _ [ _ ]) + v [ t ]) s = ⊥-rec (ω^≰𝟎 s)

·ω^+-spec₂ : ∀ {a b r} c {d s} → (c>𝟎 : c > 𝟎)
          → (ω^ a + b [ r ]) · (ω^ c + d [ s ])
          ≡ ω^ (a + c) + ((ω^ a + b [ r ]) · d) [ ≥left· (ω^ a + b [ r ]) c d c>𝟎 s ]
·ω^+-spec₂ (ω^ _ + _ [ _ ]) <₁ = refl

·-is-assoc : ∀ a b c → a · (b · c) ≡ (a · b) · c
·-is-assoc 𝟎 b c = refl
·-is-assoc a@(ω^ a₁ + x [ r ]) 𝟎 c = refl
·-is-assoc a@(ω^ a₁ + x [ r ]) b@(ω^ 𝟎 + y [ s ]) 𝟎 = sym (·𝟎-is-𝟎 (a · b))
·-is-assoc a@(ω^ a₁ + x [ r ]) b@(ω^ (ω^ _ + _ [ _ ]) + y [ s ]) 𝟎 = refl
·-is-assoc a@(ω^ a₁ + x [ r ]) b@(ω^ 𝟎 + y [ s ]) c@(ω^ 𝟎 + z [ t ]) =
   a · (b · c)
  ≡⟨ refl ⟩
   a · (b + b · z)
  ≡⟨ ·-is-left-distributive a b (b · z) ⟩
   a · b + a · (b · z)
  ≡⟨ cong (a · b +_) (·-is-assoc a b z) ⟩
   a · b + a · b · z
  ≡⟨ sym (·ω^+-spec₀ (a · b)) ⟩
   (a · b) · c ∎
·-is-assoc a@(ω^ a₁ + x [ r ])
           b@(ω^ 𝟎 + y [ s ])
           c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ t ]) =
   a · (b · c)
  ≡⟨ refl ⟩
   ω^ (a₁ + c₁) + a · (b · z) [ _ ]
  ≡⟨ Cnf⁼ refl q ⟩
   ω^ (a₁ + c₁) + (ω^ a₁ + u [ t' ]) · z [ _ ]
  ≡⟨ refl ⟩
   (ω^ a₁ + u [ t' ]) · c
  ≡⟨ cong (_· c) (sym p) ⟩
   (a · b) · c ∎
 where
  fact : Σ[ u ∈ Cnf ] Σ[ t' ∈ a₁ ≥ left u ] a · b ≡ ω^ a₁ + u [ t' ]
  fact = ·ω^+-spec₁ a₁ x r y s
  u : Cnf
  u = fst fact
  t' : a₁ ≥ left u
  t' = fst (snd fact)
  p : a · b ≡ ω^ a₁ + u [ t' ]
  p = snd (snd fact)
  q : a · (b · z) ≡ (ω^ a₁ + u [ t' ]) · z
  q = ·-is-assoc a b z ∙ cong (_· z) p
·-is-assoc a@(ω^ a₁ + x [ r ])
           b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ s ])
           c@(ω^ 𝟎 + z [ t ]) =
   a · (b · c)
  ≡⟨ refl ⟩
   a · (b + b · z)
  ≡⟨ ·-is-left-distributive a b (b · z) ⟩
   a · b + a · (b · z)
  ≡⟨ cong (a · b +_) (·-is-assoc a b z) ⟩
   a · b + (a · b) · z
  ≡⟨ refl ⟩
   (a · b) · c ∎
·-is-assoc a@(ω^ a₁ + x [ r ])
           b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ s ])
           c@(ω^ c₁@(ω^ _ + _ [ _ ]) + z [ t ]) =
   a · (b · c)
  ≡⟨ refl ⟩
   a · ω^ (b₁ + c₁) + (b · z) [ _ ]
  ≡⟨ ·ω^+-spec₂ (b₁ + c₁) (<-trans <₁ (<+r b₁ c₁ <₁)) ⟩
   ω^ (a₁ + (b₁ + c₁)) + (a · (b · z)) [ _ ]
  ≡⟨ Cnf⁼ (+-is-assoc a₁ b₁ c₁) (·-is-assoc a b z) ⟩
   ω^ (a₁ + b₁ + c₁) + a · b · z [ _ ]
  ≡⟨ refl ⟩
   (a · b) · c ∎

fin·fin<ω : ∀ a b → left a ≡ 𝟎 → left b ≡ 𝟎 → a · b < ω
fin·fin<ω a@𝟎 b _ _ = <₁  -- : 𝟎 < ω
fin·fin<ω a@(ω^ _ + _ [ _ ]) b@𝟎 _ _ = <₁  -- : 𝟎 < ω
fin·fin<ω a@(ω^ 𝟎 + _ [ _ ]) b@(ω^ 𝟎 + y [ s ]) _ _ = a+a·y<ω  -- : a + a · y < ω
 where
  a·y<ω : a · y < ω
  a·y<ω = fin·fin<ω a y refl (≤𝟎→≡𝟎 s)
  a+a·y<ω : a + a · y < ω
  a+a·y<ω = fin+fin<ω a (a · y) refl (<ω→fin a·y<ω)
fin·fin<ω a@(ω^ 𝟎 + _ [ _ ]) b@(ω^ y@(ω^ _ + _ [ _ ]) + _ [ _ ]) _ y≡𝟎 = ⊥-rec (ω≢𝟎 y≡𝟎)
fin·fin<ω a@(ω^ x@(ω^ _ + _ [ _ ]) + _ [ _ ]) b@(ω^ _ + _ [ _ ]) x≡𝟎 _ = ⊥-rec (ω≢𝟎 x≡𝟎)

≤l· : ∀ a b → a > 𝟎 → b ≤ a · b
≤l· a@(ω^ _ + _ [ _ ]) 𝟎 <₁ = ≤-refl  -- : 𝟎 ≤ 𝟎
≤l· a@(ω^ _ + _ [ _ ]) b@(ω^ 𝟎 + y [ s ]) <₁ = goal
 where
  b≡𝟏+y : b ≡ 𝟏 + y
  b≡𝟏+y = ω^+≡ω^⟨⟩+ y s
  y≤a·y : y ≤ a · y
  y≤a·y = ≤l· a y <₁
  𝟏+y≤a+a·y : 𝟏 + y ≤ a + a · y
  𝟏+y≤a+a·y = +-is-≤-monotone 𝟏 a y (a · y) 𝟏≤ω^ y≤a·y
  goal : b ≤ a + a · y
  goal = subst (_≤ a + a · y) (sym b≡𝟏+y) 𝟏+y≤a+a·y
≤l· a@(ω^ a₁ + _ [ _ ]) b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ]) <₁ = goal
 where
  y≤a·y : y ≤ a · y
  y≤a·y = ≤l· a y <₁
  goal : b ≤ ω^ (a₁ + b₁) + (a · y) [ _ ]
  goal = ≤₂' (≤l+ b₁ a₁) y≤a·y

<l· : ∀ a b → a > 𝟏 → b > 𝟎 → left a ≥ left b → b < a · b
<l· a@(ω^ a₁ + a' [ _ ])
    b@(ω^ 𝟎 + 𝟎 [ _ ]) a>𝟏
    <₁ a₁≥𝟎 = ≤∘<-in-< (inr (Cnf⁼ refl refl)) a>𝟏
<l· a@(ω^ a₁ + a' [ _ ])
    b@(ω^ 𝟎 + b'@(ω^ _ + _ [ _ ]) [ s ]) a>𝟏
    <₁ a₁≥𝟎 = goal
 where
  a·⟨b'+𝟏⟩≡a·b'+a : a · (b' + 𝟏) ≡ a · b' + a
  a·⟨b'+𝟏⟩≡a·b'+a = ·+𝟏-spec a b'
  b'+𝟏≡b : b' + 𝟏 ≡ b
  b'+𝟏≡b = ω^𝟎+-is-+𝟏 b' s
  a·b≡a·b'+a : a · b ≡ a · b' + a
  a·b≡a·b'+a = subst (λ x → a · x ≡ a · b' + a) b'+𝟏≡b a·⟨b'+𝟏⟩≡a·b'+a
  b'≤a·b' : b' ≤ a · b'
  b'≤a·b' = ≤l· a b' <₁
  b'+𝟏≤a·b'+𝟏 : b' + 𝟏 ≤ a · b' + 𝟏
  b'+𝟏≤a·b'+𝟏 = l+-is-≤-monotone b' (a · b') 𝟏 b'≤a·b'
  a·b'+𝟏<a·b'+a : a · b' + 𝟏 < a · b' + a
  a·b'+𝟏<a·b'+a = +r-is-<-monotone (a · b') 𝟏 a a>𝟏
  b'+𝟏<a·b'+a : b' + 𝟏 < a · b' + a
  b'+𝟏<a·b'+a = ≤∘<-in-< b'+𝟏≤a·b'+𝟏 a·b'+𝟏<a·b'+a
  goal : b < a · b
  goal = subst2 _<_ b'+𝟏≡b (sym a·b≡a·b'+a) b'+𝟏<a·b'+a
<l· a@(ω^ a₁ + a' [ _ ])
    b@(ω^ b₁@(ω^ _ + _ [ _ ]) + b' [ _ ]) (<₂ <₁)
    <₁ a₁≥b₁ = <₂ goal
 where
  goal : b₁ < a₁ + b₁
  goal = <l+ b₁ a₁ <₁ (≤₂⁻¹ a₁≥b₁)
<l· a@(ω^ a₁ + a' [ _ ])
    b@(ω^ b₁@(ω^ _ + _ [ _ ]) + b' [ _ ]) (<₃ 𝟎≡a₁ _)
    <₁ a₁≥b₁ = ⊥-rec (ω^≰𝟎 (≤-trans a₁≥b₁ (inr 𝟎≡a₁)))

≤·r : ∀ a b → b > 𝟎 → a ≤ a · b
≤·r 𝟎 b@(ω^ _ + _ [ _ ]) <₁ = ≤-refl  -- : 𝟎 ≤ 𝟎
≤·r a@(ω^ _ + _ [ _ ]) b@(ω^ 𝟎 + y [ _ ]) <₁ = ≤+r a (a · y)  -- : a ≤ a + a · y
≤·r a@(ω^ a₁ + x [ _ ]) b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ]) <₁ = goal
 where
  a₁<a₁+b₁ : a₁ < a₁ + b₁
  a₁<a₁+b₁ = <+r a₁ b₁ <₁
  goal : a ≤ ω^ (a₁ + b₁) + (a · y) [ _ ]
  goal = inl (<₂ a₁<a₁+b₁)

ω^ω^-is-mul-indecomposable : ∀ a b {c} →
    a < ω^⟨ ω^⟨ c ⟩ ⟩ → b < ω^⟨ ω^⟨ c ⟩ ⟩ → a · b < ω^⟨ ω^⟨ c ⟩ ⟩
ω^ω^-is-mul-indecomposable 𝟎 b _ _ = <₁
ω^ω^-is-mul-indecomposable a@(ω^ _ + _ [ _ ]) 𝟎 a< b< = <₁
ω^ω^-is-mul-indecomposable a@(ω^ _ + _ [ _ ])
                           b@(ω^ 𝟎 + y [ s ])
                           {c} a< b< = goal
 where
  IH : a · y < ω^⟨ ω^⟨ c ⟩ ⟩
  IH = ω^ω^-is-mul-indecomposable a y a< (<-trans (right< 𝟎 y s) b<)
  goal : a + a · y < ω^⟨ ω^⟨ c ⟩ ⟩
  goal = ω^-is-add-indecomposable a (a · y) a< IH
ω^ω^-is-mul-indecomposable a@(ω^ a₁ + x [ _ ])
                           b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ])
                           {c} (<₂ a₁<) (<₂ b₁<) = goal
 where
  a₁+b₁<ω^c : a₁ + b₁ < ω^⟨ c ⟩
  a₁+b₁<ω^c = ω^-is-add-indecomposable a₁ b₁ a₁< b₁<
  goal : ω^ (a₁ + b₁) + a · y [ _ ] < ω^⟨ ω^⟨ c ⟩ ⟩
  goal = <₂ a₁+b₁<ω^c

·ω^-is-add-indecomposable : ∀ a b c d → c > 𝟎 → d > 𝟎 →
    a < c · ω^⟨ d ⟩ → b < c · ω^⟨ d ⟩ → a + b < c · ω^⟨ d ⟩
·ω^-is-add-indecomposable 𝟎 b _ _ <₁ <₁ a< b< = b<
·ω^-is-add-indecomposable a@(ω^ _ + _ [ _ ]) 𝟎 _ _ <₁ <₁ a< b< = a<
·ω^-is-add-indecomposable a@(ω^ a₁ + x [ _ ])
                          b@(ω^ b₁ + y [ _ ])
                          c@(ω^ _ + _ [ _ ])
                          d@(ω^ _ + _ [ _ ]) <₁ <₁ a< b< with <-tri a₁ b₁ with a<
... | inl a₁<b₁ | _ = b<
... | inr a₁≥b₁ | <₂ r = <₂ r

ω^⟨·ω^⟩-is-mul-indecomposable : ∀ a b c d → c > 𝟎 → d > 𝟎 →
    a < ω^⟨ c · ω^⟨ d ⟩ ⟩ → b < ω^⟨ c · ω^⟨ d ⟩ ⟩ → a · b < ω^⟨ c · ω^⟨ d ⟩ ⟩
ω^⟨·ω^⟩-is-mul-indecomposable 𝟎 b _ _ <₁ <₁ a< b< = <₁
ω^⟨·ω^⟩-is-mul-indecomposable a@(ω^ _ + _ [ _ ]) 𝟎 _ _ <₁ <₁ a< b< = <₁
ω^⟨·ω^⟩-is-mul-indecomposable a@(ω^ _ + _ [ _ ])
                              b@(ω^ 𝟎 + y [ s ])
                              c d <₁ <₁ a< b< = goal
 where
  IH : a · y < ω^⟨ c · ω^⟨ d ⟩ ⟩
  IH = ω^⟨·ω^⟩-is-mul-indecomposable a y c d <₁ <₁ a< (<-trans (right< 𝟎 y s) b<)
  goal : a + a · y < ω^⟨ c · ω^⟨ d ⟩ ⟩
  goal = ω^-is-add-indecomposable a (a · y) a< IH
ω^⟨·ω^⟩-is-mul-indecomposable a@(ω^ a₁ + x [ _ ])
                              b@(ω^ b₁@(ω^ _ + _ [ _ ]) + y [ _ ])
                              c d <₁ <₁ (<₂ a₁<) (<₂ b₁<) = goal
 where
  claim : a₁ + b₁ < c · ω^⟨ d ⟩
  claim = ·ω^-is-add-indecomposable a₁ b₁ c d <₁ <₁ a₁< b₁<
  goal : ω^ (a₁ + b₁) + a · y [ _ ] < ω^⟨ c · ω^⟨ d ⟩ ⟩
  goal = <₂ claim

·ω^ω^-cancel : ∀ a b r {c} → left a < c
             → (ω^ a + b [ r ]) · ω^⟨ ω^⟨ c ⟩ ⟩ ≡ ω^⟨ ω^⟨ c ⟩ ⟩
·ω^ω^-cancel a b r {c} la<c =
   (ω^ a + b [ r ]) · ω^⟨ ω^⟨ c ⟩ ⟩
  ≡⟨ refl ⟩
   ω^⟨ a + ω^⟨ c ⟩ ⟩
  ≡⟨ cong ω^⟨_⟩ (+-left-cancel a ω^⟨ c ⟩ la<c) ⟩
   ω^⟨ ω^⟨ c ⟩ ⟩ ∎

·ω^⟨·ω^⟩-cancel : ∀ a b c → a > 𝟎 → b > 𝟎 → left (left a) < left b + c
                → a · ω^⟨ b · ω^⟨ c ⟩ ⟩ ≡ ω^⟨ b · ω^⟨ c ⟩ ⟩
·ω^⟨·ω^⟩-cancel a@(ω^ a₁ + _ [ _ ]) b@(ω^ b₁ + _ [ _ ]) 𝟎 <₁ <₁ la₁<b₁+𝟎 =
   a · ω^⟨ b ⟩
  ≡⟨ refl ⟩
   ω^⟨ a₁ + b ⟩
  ≡⟨ cong ω^⟨_⟩ (+-left-cancel a₁ b la₁<b₁) ⟩
   ω^⟨ b ⟩ ∎
 where
  la₁<b₁ : left a₁ < b₁
  la₁<b₁ = <∘≤-in-< la₁<b₁+𝟎 (inr (sym +𝟎-is-identity))
·ω^⟨·ω^⟩-cancel a@(ω^ a₁ + x [ r ])
                b@(ω^ b₁ + _ [ _ ])
                c@(ω^ _ + _ [ _ ]) <₁ <₁ la₁<b₁+c =
   a · ω^⟨ b · ω^⟨ c ⟩ ⟩
  ≡⟨ refl ⟩
   a · ω^⟨ ω^⟨ b₁ + c ⟩ ⟩
  ≡⟨ ·ω^ω^-cancel a₁ x r la₁<b₁+c ⟩
   ω^⟨ ω^⟨ b₁ + c ⟩ ⟩
  ≡⟨ refl ⟩
   ω^⟨ b · ω^⟨ c ⟩ ⟩ ∎


-- Multiplication with natural numbers

_•_ : Cnf → ℕ → Cnf
a • n = a · NtoC n

•suc-spec : ∀ a n → a • suc n ≡ a • n + a
•suc-spec a n = claim₀ ∙ claim₁
 where
  claim₀ : a • suc n ≡ a · (NtoC n + 𝟏)
  claim₀ = cong (a ·_) (NtoC⟨suc⟩≡NtoC+𝟏 n)
  claim₁ : a · (NtoC n + 𝟏) ≡ a • n + a
  claim₁ = ·+𝟏-spec a (NtoC n)

•suc-spec' : ∀ a n → a • suc n ≡ a + a • n
•suc-spec' 𝟎 n = refl
•suc-spec' (ω^ _ + _ [ _ ]) n = refl

ω^•-is-<-increasing : ∀ a → a > 𝟎 → is-<-increasing (a •_)
ω^•-is-<-increasing a@(ω^ _ + _ [ _ ]) <₁ n = subst (a • n <_) claim₁ claim₀
 where
  claim₀ : a • n < a • n + a
  claim₀ = <+r _ a <₁
  claim₁ : a • n + a ≡ a • suc n
  claim₁ = sym (•suc-spec a n)

left•≤ : ∀ a n → left (a • n) ≤ left a
left•≤ 𝟎 n = inr refl
left•≤ x@(ω^ a + b [ r ])  = 𝟎≤
left•≤ x@(ω^ a + b [ r ]) (suc n) = goal
 where
  claim₀ : x • suc n ≡ x • n + x
  claim₀ = •suc-spec x n
  claim₁ : left (x • n + x) ≤ a
  claim₁ = ≥left+ (x • n) x (left•≤ x n) (inr refl)
  goal : left (x • suc n) ≤ a
  goal = subst (λ z → left z ≤ a) (sym claim₀) claim₁

Σn<•sn : ∀ {a} b → a ≥ left b → Σ[ n ∈ ℕ ] b < ω^⟨ a ⟩ • suc n
Σn<•sn {a} 𝟎 _ =  , <₁
Σn<•sn {a} (ω^ b + c [ r ]) (inl a>b) =  , <₂ a>b
Σn<•sn {a} (ω^ b + c [ r ]) (inr a≡b) = suc n , goal
 where
  r' : a ≥ left c
  r' = subst (_≥ left c) (sym a≡b) r
  IH : Σ[ n ∈ ℕ ] c < ω^⟨ a ⟩ • suc n
  IH = Σn<•sn {a} c r'
  n : ℕ
  n = fst IH
  claim₁ : ω^ b + c [ r ] < ω^ a + ω^⟨ a ⟩ • suc n [ left•≤ ω^⟨ a ⟩ (suc n) ]
  claim₁ = <₃ (sym a≡b) (snd IH)
  claim₂ : ω^ a + ω^⟨ a ⟩ • suc n [ _ ] ≡ ω^⟨ a ⟩ + ω^⟨ a ⟩ • suc n
  claim₂ = ω^+≡ω^⟨⟩+ _ _
  claim₃ : ω^⟨ a ⟩ + ω^⟨ a ⟩ • suc n ≡ ω^⟨ a ⟩ • suc (suc n)
  claim₃ = sym (•suc-spec' ω^⟨ a ⟩ (suc n))
  goal : ω^ b + c [ r ] < ω^⟨ a ⟩ • suc (suc n)
  goal = subst (ω^ b + c [ r ] <_) (claim₂ ∙ claim₃) claim₁


{- Converting to CNF's of the form "ω ^ a • n + d" with n ∈ ℕ and d < a -}

to-CNF-with-coefficients : ∀ a b r →
  Σ[ n ∈ ℕ ] Σ[ d ∈ Cnf ] (ω^ a + b [ r ] ≡ ω^⟨ a ⟩ • n + d) × (left d < ω^⟨ a ⟩)
to-CNF-with-coefficients a 𝟎 _ =  , 𝟎 , Cnf⁼ refl refl , <₁
to-CNF-with-coefficients a y@(ω^ b + _ [ _ ]) (inl a>b) =  , y , ω^+≡ω^⟨⟩+ _ _ , <-trans a>b left<
to-CNF-with-coefficients a y@(ω^ b + b' [ s ]) (inr a≡b) = suc n , d , goal₀ , goal₁
 where
  IH : Σ[ n ∈ ℕ ] Σ[ d ∈ Cnf ] (ω^ b + b' [ s ] ≡ ω^⟨ b ⟩ • n + d) × (left d < ω^⟨ b ⟩)
  IH = to-CNF-with-coefficients b b' s
  n : ℕ
  n = fst IH
  d : Cnf
  d = fst (snd IH)
  goal₀ : ω^ a + y [ _ ] ≡ ω^⟨ a ⟩ • suc n + d
  goal₀ =
    ω^ a + y [ _ ]
   ≡⟨ ω^+≡ω^⟨⟩+ _ _ ⟩
    ω^⟨ a ⟩ + y
   ≡⟨ cong (ω^⟨ a ⟩ +_) (fst (snd (snd IH))) ⟩
    ω^⟨ a ⟩ + (ω^⟨ b ⟩ • n + d)
   ≡⟨ cong (λ z → ω^⟨ a ⟩ + (ω^⟨ z ⟩ • n + d)) (sym a≡b) ⟩
    ω^⟨ a ⟩ + (ω^⟨ a ⟩ • n + d)
   ≡⟨ +-is-assoc ω^⟨ a ⟩ (ω^⟨ a ⟩ • n) d ⟩
    (ω^⟨ a ⟩ + ω^⟨ a ⟩ • n) + d
   ≡⟨ cong (_+ d) (•suc-spec' ω^⟨ a ⟩ n) ⟩
    ω^⟨ a ⟩ • suc n + d ∎
  goal₁ : left d < ω^⟨ a ⟩
  goal₁ = subst (λ z → left d < ω^⟨ z ⟩) (sym a≡b) (snd (snd (snd IH)))