{-# OPTIONS --cubical --safe #-}
module CantorNormalForm.Arithmetic where
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Empty
renaming (rec to ⊥-rec)
open import CantorNormalForm.Base
open import CantorNormalForm.Addition public
open import CantorNormalForm.Subtraction public
open import CantorNormalForm.Multiplication public
open import CantorNormalForm.Division public
open import CantorNormalForm.Exponentiation public
open import CantorNormalForm.Classifiability
open import Abstract.Arithmetic _<_ _≤_ public
+r-preserves-sup : ∀ {a} c {f} → a is-sup-of f → (c + a) is-sup-of (λ i → c + f i)
+r-preserves-sup {a} c {f} (f≤a , a-min-over-f) = c+f≤c+a , c+a-min-over-c+f
where
c+f≤c+a : ∀ i → c + f i ≤ c + a
c+f≤c+a i = +r-is-≤-monotone c _ _ (f≤a i)
c+a-min-over-c+f : ∀ x → (∀ i → c + f i ≤ x) → c + a ≤ x
c+a-min-over-c+f x c+f≤x = subst (c + a ≤_) c+⟨x-c⟩≡x c+a≤c+⟨x-c⟩
where
f≤x-c : ∀ i → f i ≤ x - c
f≤x-c i = +≤→≤- c (f i) x (c+f≤x i)
a≤x-c : a ≤ x - c
a≤x-c = a-min-over-f (x - c) f≤x-c
c+a≤c+⟨x-c⟩ : c + a ≤ c + (x - c)
c+a≤c+⟨x-c⟩ = +r-is-≤-monotone c _ _ a≤x-c
c+⟨x-c⟩≡x : c + (x - c) ≡ x
c+⟨x-c⟩≡x = sub-spec₀ c x (≤-trans (≤+r c (f 0)) (c+f≤x 0))
+-is-add : is-add _+_
+-is-add = case-zero , case-suc , case-lim
where
case-zero : ∀ a c → is-zero a → c + a ≡ c
case-zero a c a-is-zero =
c + a
≡⟨ cong (c +_) (is-zero→≡𝟎 a-is-zero) ⟩
c + 𝟎
≡⟨ +𝟎-is-identity ⟩
c ∎
case-suc : ∀ a b c d → a is-suc-of b → d is-suc-of (c + b) → c + a ≡ d
case-suc a b c d a-is-suc-of-b d-is-suc-of-c+d =
c + a
≡⟨ cong (c +_) (sym (suc→+𝟏 a-is-suc-of-b)) ⟩
c + (b + 𝟏)
≡⟨ +-is-assoc c b 𝟏 ⟩
(c + b) + 𝟏
≡⟨ suc→+𝟏 d-is-suc-of-c+d ⟩
d ∎
case-lim : ∀ a b c f f↑ → a is-lim-of (f , f↑) → b is-sup-of (λ i → c + f i) → c + a ≡ b
case-lim a b c f f↑ a-is-sup-of-f b-is-sup-of-c+f = c+a≡b
where
c+a-is-sup-of-c+f : (c + a) is-sup-of (λ i → c + f i)
c+a-is-sup-of-c+f = +r-preserves-sup c a-is-sup-of-f
c+a≡b : c + a ≡ b
c+a≡b = sup-unique c+a-is-sup-of-c+f b-is-sup-of-c+f
add-is-unique : (_+'_ : Cnf → Cnf → Cnf) → is-add _+'_ → _+_ ≡ _+'_
add-is-unique _+'_ (+'-is-add-zero , +'-is-add-suc , +'-is-add-lim) = funExt (funExt ∘ goal)
where
goal : ∀ c a → c + a ≡ c +' a
goal c = cf-ind (λ _ → Cnf-is-set _ _) case-zero case-suc case-lim
where
case-zero : c + 𝟎 ≡ c +' 𝟎
case-zero =
c + 𝟎
≡⟨ +𝟎-is-identity ⟩
c
≡⟨ sym (+'-is-add-zero 𝟎 c 𝟎-is-zero) ⟩
c +' 𝟎 ∎
case-suc : ∀ a → c + a ≡ c +' a → c + (a + 𝟏) ≡ c +' (a + 𝟏)
case-suc a ih =
c + (a + 𝟏)
≡⟨ +-is-assoc c a 𝟏 ⟩
(c + a) + 𝟏
≡⟨ cong (_+ 𝟏) ih ⟩
(c +' a) + 𝟏
≡⟨ sym (+'-is-add-suc (a + 𝟏) a c ((c +' a) + 𝟏) (+𝟏-calc-suc a) (+𝟏-calc-suc (c +' a))) ⟩
c +' (a + 𝟏) ∎
case-lim : ∀ a f f↑ → a is-lim-of (f , f↑)
→ (∀ i → c + f i ≡ c +' f i)
→ c + a ≡ c +' a
case-lim a f f↑ a-is-sup-of-f ih =
c + a
≡⟨ sym (+'-is-add-lim a (c + a) c f f↑ a-is-sup-of-f c+a-is-sup-of-c+'f) ⟩
c +' a ∎
where
c+a-is-sup-of-c+f : (c + a) is-sup-of (λ i → c + f i)
c+a-is-sup-of-c+f = +r-preserves-sup c a-is-sup-of-f
c+'f≤c+a : ∀ i → (c +' f i) ≤ c + a
c+'f≤c+a i = ≤-trans (inr (ih i)) (fst c+a-is-sup-of-c+f i)
c+a-min-over-c+'f : ∀ x → (∀ i → (c +' f i) ≤ x) → c + a ≤ x
c+a-min-over-c+'f x c+'f≤x = snd c+a-is-sup-of-c+f x c+f≤x
where
c+f≤x : ∀ i → c + f i ≤ x
c+f≤x i = subst (_≤ x) (sym (ih i)) (c+'f≤x i)
c+a-is-sup-of-c+'f : (c + a) is-sup-of (λ i → c +' f i)
c+a-is-sup-of-c+'f = c+'f≤c+a , c+a-min-over-c+'f
Cnf-has-unique-add : has-unique-add
Cnf-has-unique-add = (_+_ , +-is-add) ,
(λ (f , p) → Σ≡Prop (isProp⟨is-add⟩ Cnf-is-set) (add-is-unique f p))
open Multiplication (_+_ , +-is-add) hiding (_+_) public
·r-preserves-sup : ∀ {a} c {f} → a is-sup-of f → (c · a) is-sup-of (λ i → c · f i)
·r-preserves-sup {a} 𝟎 {f} _ = (λ _ → 𝟎≤) , (λ _ _ → 𝟎≤)
·r-preserves-sup {a} c@(ω^ _ + _ [ _ ]) {f} (f≤a , a-min-over-f) = c·f≤c·a , c·a-min-over-c·f
where
c·f≤c·a : ∀ i → c · f i ≤ c · a
c·f≤c·a i = ·r-is-≤-monotone c _ _ (f≤a i)
c·a-min-over-c·f : ∀ x → (∀ i → c · f i ≤ x) → c · a ≤ x
c·a-min-over-c·f x c·f≤x = c·a≤x
where
y : Cnf
y = x / c [ <₁ ]
f≤y : ∀ i → f i ≤ y
f≤y i = greatest-div x c (f i) <₁ (c·f≤x i)
a≤y : a ≤ y
a≤y = a-min-over-f y f≤y
c·a≤c·y : c · a ≤ c · y
c·a≤c·y = ·r-is-≤-monotone c a y a≤y
c·y≤x : c · y ≤ x
c·y≤x = div-spec x c <₁
c·a≤x : c · a ≤ x
c·a≤x = ≤-trans c·a≤c·y c·y≤x
·-is-mul : is-mul _·_
·-is-mul = case-zero , case-suc , case-lim
where
case-zero : ∀ a c → is-zero a → c · a ≡ a
case-zero a c a-is-zero =
c · a
≡⟨ cong (c ·_) (is-zero→≡𝟎 a-is-zero) ⟩
c · 𝟎
≡⟨ ·𝟎-is-𝟎 c ⟩
𝟎
≡⟨ sym (is-zero→≡𝟎 a-is-zero) ⟩
a ∎
case-suc : ∀ a b c → a is-suc-of b → c · a ≡ c · b + c
case-suc a b c a-is-suc-of-b =
c · a
≡⟨ cong (c ·_) (sym (suc→+𝟏 a-is-suc-of-b)) ⟩
c · (b + 𝟏)
≡⟨ ·+𝟏-spec c b ⟩
c · b + c ∎
case-lim : ∀ a b c f f↑ → a is-lim-of (f , f↑) → b is-sup-of (λ i → c · f i) → c · a ≡ b
case-lim a b c f f↑ a-is-sup-of-f b-is-sup-of-c·f = c·a≡b
where
c·a-is-sup-of-c·f : (c · a) is-sup-of (λ i → c · f i)
c·a-is-sup-of-c·f = ·r-preserves-sup c a-is-sup-of-f
c·a≡b : c · a ≡ b
c·a≡b = sup-unique c·a-is-sup-of-c·f b-is-sup-of-c·f
mul-is-unique : (_·'_ : Cnf → Cnf → Cnf) → is-mul _·'_ → _·_ ≡ _·'_
mul-is-unique _·'_ (·'-is-mul-zero , ·'-is-mul-suc , ·'-is-mul-lim) = funExt (funExt ∘ goal)
where
goal : ∀ c a → c · a ≡ c ·' a
goal c = cf-ind (λ _ → Cnf-is-set _ _) case-zero case-suc case-lim
where
case-zero : c · 𝟎 ≡ c ·' 𝟎
case-zero =
c · 𝟎
≡⟨ ·𝟎-is-𝟎 c ⟩
𝟎
≡⟨ sym (·'-is-mul-zero 𝟎 c 𝟎-is-zero) ⟩
c ·' 𝟎 ∎
case-suc : ∀ a → c · a ≡ c ·' a → c · (a + 𝟏) ≡ c ·' (a + 𝟏)
case-suc a ih =
c · (a + 𝟏)
≡⟨ ·+𝟏-spec c a ⟩
c · a + c
≡⟨ cong (_+ c) ih ⟩
(c ·' a) + c
≡⟨ sym (·'-is-mul-suc (a + 𝟏) a c (+𝟏-calc-suc a)) ⟩
c ·' (a + 𝟏) ∎
case-lim : ∀ a f f↑ → a is-lim-of (f , f↑)
→ (∀ i → c · f i ≡ c ·' f i)
→ c · a ≡ c ·' a
case-lim a f f↑ a-is-sup-of-f ih =
c · a
≡⟨ sym (·'-is-mul-lim a (c · a) c f f↑ a-is-sup-of-f c·a-is-sup-of-c·'f) ⟩
c ·' a ∎
where
c·a-is-sup-of-c·f : (c · a) is-sup-of (λ i → c · f i)
c·a-is-sup-of-c·f = ·r-preserves-sup c a-is-sup-of-f
c·'f≤c·a : ∀ i → (c ·' f i) ≤ c · a
c·'f≤c·a i = ≤-trans (inr (ih i)) (fst c·a-is-sup-of-c·f i)
c·a-min-over-c·'f : ∀ x → (∀ i → (c ·' f i) ≤ x) → c · a ≤ x
c·a-min-over-c·'f x c·'f≤x = snd c·a-is-sup-of-c·f x c·f≤x
where
c·f≤x : ∀ i → c · f i ≤ x
c·f≤x i = subst (_≤ x) (sym (ih i)) (c·'f≤x i)
c·a-is-sup-of-c·'f : (c · a) is-sup-of (λ i → c ·' f i)
c·a-is-sup-of-c·'f = c·'f≤c·a , c·a-min-over-c·'f
Cnf-has-unique-mul : has-unique-mul
Cnf-has-unique-mul = (_·_ , ·-is-mul) ,
(λ (f , p) → Σ≡Prop (isProp⟨is-mul⟩ Cnf-is-set) (mul-is-unique f p))
open Exponentiation
(_+_ , +-is-add)
(_·_ , ·-is-mul)
hiding (_·_)
public
ω^⟨⟩-is-exp-with-base-ω : ω^⟨_⟩ is-exp-with-base ω
ω^⟨⟩-is-exp-with-base-ω = case-zero , case-suc , case-lim , (λ _ _ _ _ ωz → ⊥-rec (ω^≰𝟎 (ωz 𝟎)))
where
case-zero : ∀ a b → is-zero a → b is-suc-of a → ω^⟨ a ⟩ ≡ b
case-zero a b a-is-zero b-is-suc-of-a =
ω^⟨ a ⟩
≡⟨ cong ω^⟨_⟩ (is-zero→≡𝟎 a-is-zero) ⟩
ω^⟨ 𝟎 ⟩
≡⟨ cong (_+ 𝟏) (sym (is-zero→≡𝟎 a-is-zero)) ⟩
a + 𝟏
≡⟨ suc→+𝟏 b-is-suc-of-a ⟩
b ∎
case-suc : ∀ a b → a is-suc-of b → ω^⟨ a ⟩ ≡ ω^⟨ b ⟩ · ω
case-suc a b a-is-suc-of-b =
ω^⟨ a ⟩
≡⟨ cong ω^⟨_⟩ (sym (suc→+𝟏 a-is-suc-of-b)) ⟩
ω^⟨ b + 𝟏 ⟩
≡⟨ refl ⟩
ω^⟨ b ⟩ · ω ∎
case-lim : ∀ a b f f↑ → a is-lim-of (f , f↑) → _ → b is-sup-of (λ i → ω^⟨ f i ⟩) → ω^⟨ a ⟩ ≡ b
case-lim a 𝟎 f f↑ a-is-sup-of-f _ 𝟎-is-sup-of-ω^f = ⊥-rec (ω^≰𝟎 (fst 𝟎-is-sup-of-ω^f 0))
case-lim a b@(ω^ u + v [ r ]) f f↑ a-is-sup-of-f _ b-is-sup-of-ω^f = goal
where
f≤u : ∀ i → f i ≤ u
f≤u i = ≮→≥ (λ u<fi → ≤→≯ (fst b-is-sup-of-ω^f i) (<₂ u<fi))
a≤u : a ≤ u
a≤u = snd a-is-sup-of-f u f≤u
ω^a≤b : ω^⟨ a ⟩ ≤ b
ω^a≤b = ≤-trans (≤₂ {a} {u} {𝟎} {𝟎≤} {𝟎≤} a≤u) (≤₃ refl 𝟎≤)
ω^f<ω^a : ∀ i → ω^⟨ f i ⟩ ≤ ω^⟨ a ⟩
ω^f<ω^a i = ≤₂ (fst a-is-sup-of-f i)
b≤ω^a : b ≤ ω^⟨ a ⟩
b≤ω^a = snd b-is-sup-of-ω^f ω^⟨ a ⟩ ω^f<ω^a
goal : ω^⟨ a ⟩ ≡ b
goal = ≤-antisym ω^a≤b b≤ω^a
exp-is-unique : (exp : Cnf → Cnf) → exp is-exp-with-base ω → ω^⟨_⟩ ≡ exp
exp-is-unique exp exp-is-exp = funExt goal
where
goal : ∀ a → ω^⟨ a ⟩ ≡ exp a
goal = cf-ind (λ _ → Cnf-is-set _ _) case-zero case-suc case-lim
where
case-zero : ω^⟨ 𝟎 ⟩ ≡ exp 𝟎
case-zero = sym (fst exp-is-exp 𝟎 𝟏 𝟎-is-zero (+𝟏-calc-suc 𝟎))
case-suc : ∀ a → ω^⟨ a ⟩ ≡ exp a → ω^⟨ a + 𝟏 ⟩ ≡ exp (a + 𝟏)
case-suc a ih =
ω^⟨ a + 𝟏 ⟩
≡⟨ refl ⟩
ω^⟨ a ⟩ · ω
≡⟨ cong (_· ω) ih ⟩
exp a · ω
≡⟨ sym (fst (snd exp-is-exp) (a + 𝟏) a (+𝟏-calc-suc a)) ⟩
exp (a + 𝟏) ∎
case-lim : ∀ a f f↑ → a is-lim-of (f , f↑) → (∀ i → ω^⟨ f i ⟩ ≡ exp (f i)) → ω^⟨ a ⟩ ≡ exp a
case-lim a f f↑ a-is-sup-of-f ih = ω^a≡expa
where
expf≤ω^a : ∀ i → exp (f i) ≤ ω^⟨ a ⟩
expf≤ω^a i = ≤-trans (inr (ih i)) (≤₂ (fst a-is-sup-of-f i))
ω^a-min-over-expf : ∀ x → (∀ i → exp (f i) ≤ x) → ω^⟨ a ⟩ ≤ x
ω^a-min-over-expf 𝟎 h = ⊥-rec (ω^≰𝟎 (subst (_≤ 𝟎) (sym (ih 0)) (h 0)))
ω^a-min-over-expf x@(ω^ u + v [ r ]) h = ω^a≤x
where
f≤u : ∀ i → f i ≤ u
f≤u i = ≮→≥ (λ u<fi → ≤→≯ (subst (_≤ _) (sym (ih i)) (h i)) (<₂ u<fi))
a≤u : a ≤ u
a≤u = snd a-is-sup-of-f u f≤u
ω^a≤x : ω^⟨ a ⟩ ≤ x
ω^a≤x = ≤-trans (≤₂ {a} {u} {𝟎} {𝟎≤} {𝟎≤} a≤u) (≤₃ refl 𝟎≤)
ω^a-is-sup-of-expf : ω^⟨ a ⟩ is-sup-of (λ i → exp (f i))
ω^a-is-sup-of-expf = expf≤ω^a , ω^a-min-over-expf
ω^a≡expa : ω^⟨ a ⟩ ≡ exp a
ω^a≡expa = sym (fst (snd (snd exp-is-exp)) a (ω^⟨ a ⟩) f f↑ a-is-sup-of-f
(λ ωz → ω^≰𝟎 (ωz 𝟎)) ω^a-is-sup-of-expf)
Cnf-has-unique-exp-with-base-ω : has-unique-exp-with-base ω
Cnf-has-unique-exp-with-base-ω =
(ω^⟨_⟩ , ω^⟨⟩-is-exp-with-base-ω) ,
(λ (f , p) → Σ≡Prop (λ _ → isProp⟨is-exp⟩ Cnf-is-set _ _) (exp-is-unique f p))