{-# 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 _<_ _≤_
infixl 36 _·_ _•_
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
·𝟎-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)
·-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
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
_•_ : 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 ]) 0 = 𝟎≤
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} 𝟎 _ = 0 , <₁
Σn<•sn {a} (ω^ b + c [ r ]) (inl a>b) = 0 , <₂ 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₁
to-CNF-with-coefficients : ∀ a b r →
Σ[ n ∈ ℕ ] Σ[ d ∈ Cnf ] (ω^ a + b [ r ] ≡ ω^⟨ a ⟩ • n + d) × (left d < ω^⟨ a ⟩)
to-CNF-with-coefficients a 𝟎 _ = 1 , 𝟎 , Cnf⁼ refl refl , <₁
to-CNF-with-coefficients a y@(ω^ b + _ [ _ ]) (inl a>b) = 1 , 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)))