{-# OPTIONS --cubical --safe #-}
module CantorNormalForm.Division 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 CantorNormalForm.Base
open import CantorNormalForm.Wellfoundedness
open import CantorNormalForm.Addition
open import CantorNormalForm.Subtraction
open import CantorNormalForm.Multiplication
infixr 36 _/_[_]
private
P : Cnf → Type
P a = ∀ b → b > 𝟎 → Σ[ c ∈ Cnf ] Σ[ d ∈ Cnf ] (a ≡ b · c + d) × (d < b)
div-step : ∀ x → (∀ y → y < x → P y) → P x
div-step x h y@(ω^ b + b' [ s ]) <₁ with <-tri x y
div-step x h y@(ω^ b + b' [ s ]) <₁ | inl x<y = 𝟎 , x , refl , x<y
div-step x h y@(ω^ b + b' [ s ]) <₁ | inr (inr x≡y) = 𝟏 , 𝟎 , x≡y , <₁
div-step x@(ω^ a + a' [ r ]) h y@(ω^ b + b' [ s ]) <₁ | inr (inl (<₂ b<a)) = goal
where
IH : Σ[ c ∈ Cnf ] Σ[ d ∈ Cnf ] (a' ≡ y · c + d) × (d < y)
IH = h a' (right< a a' r) y <₁
c d : Cnf
c = fst IH
d = fst (snd IH)
a'≡y·c+d : a' ≡ y · c + d
a'≡y·c+d = fst (snd (snd IH))
d<y : d < y
d<y = snd (snd (snd IH))
a-b>𝟎 : a - b > 𝟎
a-b>𝟎 = sub-spec₂ a b b<a
b+a-b≡a : b + (a - b) ≡ a
b+a-b≡a = sub-spec₀ b a (inl b<a)
fact : y · ω^⟨ a - b ⟩ ≡ ω^⟨ a ⟩
fact = ·ω^⟨⟩≡ω^⟨left+⟩ y (a - b) <₁ a-b>𝟎 ∙ Cnf⁼ b+a-b≡a refl
u : Cnf
u = ω^⟨ a - b ⟩ + c
x≡y·u+d : x ≡ y · u + d
x≡y·u+d =
ω^ a + a' [ _ ]
≡⟨ ω^+≡ω^⟨⟩+ _ _ ⟩
ω^⟨ a ⟩ + a'
≡⟨ cong (_+ a') (sym fact) ⟩
y · ω^⟨ a - b ⟩ + a'
≡⟨ cong (y · ω^⟨ a - b ⟩ +_) a'≡y·c+d ⟩
y · ω^⟨ a - b ⟩ + (y · c + d)
≡⟨ +-is-assoc (y · ω^⟨ a - b ⟩) (y · c) d ⟩
y · ω^⟨ a - b ⟩ + y · c + d
≡⟨ cong (_+ d) (sym (·-is-left-distributive y ω^⟨ a - b ⟩ c)) ⟩
y · u + d ∎
goal : Σ[ u ∈ Cnf ] Σ[ d ∈ Cnf ] (x ≡ y · u + d) × (d < y)
goal = u , d , x≡y·u+d , d<y
div-step x@(ω^ a + a' [ r ]) h y@(ω^ b + b' [ s ]) <₁ | inr (inl (<₃ b≡a b'<a')) =
c + 𝟏 , d , x≡y·⟨c+1⟩+d , d<y
where
IH : Σ[ c ∈ Cnf ] Σ[ d ∈ Cnf ] (a' - b' ≡ y · c + d) × (d < y)
IH = h (a' - b') (≤∘<-in-< (sub-spec₃ a' b') (right< a a' r)) y <₁
c d : Cnf
c = fst IH
d = fst (snd IH)
a'-b'≡y·c+d : a' - b' ≡ y · c + d
a'-b'≡y·c+d = fst (snd (snd IH))
d<y : d < y
d<y = snd (snd (snd IH))
claim₀ : left (a' - b') ≤ a
claim₀ = left⟨-⟩≤ a' a b' r
claim₁ : left (y · c + d) ≤ a
claim₁ = subst (λ z → left z ≤ a) a'-b'≡y·c+d claim₀
claim₂ : left (y · c) ≤ a
claim₂ = fst (left⟨+⟩≤⁻¹ (y · c) d a claim₁)
lc≡𝟎 : left c ≡ 𝟎
lc≡𝟎 = left⟨·nat⟩⁻¹ y c <₁ (subst (left (y · c) ≤_) (sym b≡a) claim₂)
n : ℕ
n = fst (left≡𝟎-is-nat c lc≡𝟎)
c≡n : c ≡ NtoC n
c≡n = snd (left≡𝟎-is-nat c lc≡𝟎)
x≡y·⟨c+1⟩+d : x ≡ y · (c + 𝟏) + d
x≡y·⟨c+1⟩+d =
ω^ a + a' [ r ]
≡⟨ ω^+≡ω^⟨⟩+ a' r ⟩
ω^⟨ a ⟩ + a'
≡⟨ cong (ω^⟨ a ⟩ +_) (sym (sub-spec₀ b' a' (inl b'<a'))) ⟩
ω^⟨ a ⟩ + (b' + (a' - b'))
≡⟨ +-is-assoc ω^⟨ a ⟩ b' (a' - b') ⟩
(ω^⟨ a ⟩ + b') + (a' - b')
≡⟨ cong (λ z → (ω^⟨ z ⟩ + b') + (a' - b')) (sym b≡a) ⟩
(ω^⟨ b ⟩ + b') + (a' - b')
≡⟨ cong (_+ (a' - b')) (sym (ω^+≡ω^⟨⟩+ b' s)) ⟩
y + (a' - b')
≡⟨ cong (y +_) a'-b'≡y·c+d ⟩
y + (y · c + d)
≡⟨ +-is-assoc y (y · c) d ⟩
y + y · c + d
≡⟨ cong (λ z → (y + y · z) + d) c≡n ⟩
y + y • n + d
≡⟨ cong (_+ d) (sym (•suc-spec' y n)) ⟩
y • (suc n) + d
≡⟨ cong (_+ d) (•suc-spec y n) ⟩
(y • n + y) + d
≡⟨ cong (λ z → (y · z + y) + d) (sym c≡n) ⟩
(y · c + y) + d
≡⟨ cong (_+ d) (sym (·+𝟏-spec y c)) ⟩
y · (c + 𝟏) + d ∎
Thm[div] : (a b : Cnf) → b > 𝟎
→ Σ[ c ∈ Cnf ] Σ[ d ∈ Cnf ] (a ≡ b · c + d) × (d < b)
Thm[div] = wf-ind div-step
_/_[_] : (a b : Cnf) → b > 𝟎 → Cnf
a / b [ r ] = fst (Thm[div] a b r)
div-spec : ∀ a b → (r : b > 𝟎) → b · (a / b [ r ]) ≤ a
div-spec a b b>𝟎 = goal
where
c d : Cnf
c = a / b [ b>𝟎 ]
d = fst (snd (Thm[div] a b b>𝟎))
a≡b·c+d : a ≡ b · c + d
a≡b·c+d = fst (snd (snd (Thm[div] a b b>𝟎)))
b·c≤b·c+d : b · c ≤ b · c + d
b·c≤b·c+d = ≤+r (b · c) d
goal : b · c ≤ a
goal = ≤-trans b·c≤b·c+d (inr a≡b·c+d)
greatest-div : ∀ a b c → (r : b > 𝟎) → b · c ≤ a → c ≤ a / b [ r ]
greatest-div a b c b>𝟎 b·c≤a = ≮→≥ c'≮c
where
c' d : Cnf
c' = a / b [ b>𝟎 ]
d = fst (snd (Thm[div] a b b>𝟎))
a≡b·c'+d : a ≡ b · c' + d
a≡b·c'+d = fst (snd (snd (Thm[div] a b b>𝟎)))
d<b : d < b
d<b = snd (snd (snd (Thm[div] a b b>𝟎)))
c'≮c : c' < c → ⊥
c'≮c c'<c = ≤→≯ b·c≤a a<b·c
where
c'+𝟏≤c : c' + 𝟏 ≤ c
c'+𝟏≤c = <→+𝟏≤ c'<c
b·⟨c'+𝟏⟩≤b·c : b · (c' + 𝟏) ≤ b · c
b·⟨c'+𝟏⟩≤b·c = ·r-is-≤-monotone b (c' + 𝟏) c c'+𝟏≤c
b·⟨c'+𝟏⟩≡b·c'+b : b · (c' + 𝟏) ≡ b · c' + b
b·⟨c'+𝟏⟩≡b·c'+b = ·+𝟏-spec b c'
b·c'+d<b·c'+b : b · c' + d < b · c' + b
b·c'+d<b·c'+b = +r-is-<-monotone (b · c') d b d<b
a<b·c'+b : a < b · c' + b
a<b·c'+b = subst (_< b · c' + b) (sym a≡b·c'+d) b·c'+d<b·c'+b
a<b·⟨c'+1⟩ : a < b · (c' + 𝟏)
a<b·⟨c'+1⟩ = subst (a <_) (sym b·⟨c'+𝟏⟩≡b·c'+b) a<b·c'+b
a<b·c : a < b · c
a<b·c = <∘≤-in-< a<b·⟨c'+1⟩ b·⟨c'+𝟏⟩≤b·c