{-# OPTIONS --cubical --safe #-}
module CantorNormalForm.Subtraction where
open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat using (ℕ; suc)
open import Cubical.Data.Sum
open import Cubical.Data.Empty
renaming (rec to ⊥-rec)
open import CantorNormalForm.Base
open import CantorNormalForm.Addition
infixl 35 _-_
_-_ : Cnf → Cnf → Cnf
𝟎 - b = 𝟎
a - 𝟎 = a
ω^ a + c [ r ] - ω^ b + d [ s ] with <-tri a b
... | inl a<b = 𝟎
... | inr (inl a>b) = ω^ a + c [ r ]
... | inr (inr a≡b) = c - d
sub-spec₀ : ∀ a b → a ≤ b → a + (b - a) ≡ b
sub-spec₀ 𝟎 𝟎 _ = refl
sub-spec₀ 𝟎 (ω^ b + d [ s ]) _ = refl
sub-spec₀ (ω^ a + c [ r ]) 𝟎 t = ≤𝟎→≡𝟎 t
sub-spec₀ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t with <-tri b a
sub-spec₀ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t | inl b<a = ⊥-rec (≤→≯ t (<₂ b<a))
sub-spec₀ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t | inr (inl b>a) with <-tri a b
sub-spec₀ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t | inr (inl b>a) | inl a<b = refl
sub-spec₀ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t | inr (inl b>a) | inr a≥b = ⊥-rec (≤→≯ a≥b b>a)
sub-spec₀ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t | inr (inr b≡a) = goal
where
IH : c + (d - c) ≡ d
IH = sub-spec₀ c d (≤₃⁻¹ (sym b≡a) t)
claim₀ : ω^ a + c [ r ] + (d - c) ≡ (ω^⟨ a ⟩ + c) + (d - c)
claim₀ = cong (_+ (d - c)) (ω^+≡ω^⟨⟩+ c r)
claim₁ : (ω^⟨ a ⟩ + c) + (d - c) ≡ ω^⟨ a ⟩ + (c + (d - c))
claim₁ = sym (+-is-assoc ω^⟨ a ⟩ c (d - c))
claim₂ : ω^⟨ a ⟩ + (c + (d - c)) ≡ ω^⟨ a ⟩ + d
claim₂ = cong (ω^⟨ a ⟩ +_) IH
claim₃ : ω^⟨ a ⟩ + d ≡ ω^⟨ b ⟩ + d
claim₃ = cong (λ x → ω^⟨ x ⟩ + d) (sym b≡a)
claim₄ : ω^⟨ b ⟩ + d ≡ ω^ b + d [ s ]
claim₄ = sym (ω^+≡ω^⟨⟩+ d s)
goal : ω^ a + c [ r ] + (d - c) ≡ ω^ b + d [ s ]
goal = claim₀ ∙ claim₁ ∙ claim₂ ∙ claim₃ ∙ claim₄
Thm[sub] : ∀ a b → a ≤ b → Σ[ c ∈ Cnf ] a + c ≡ b
Thm[sub] a b a≤b = b - a , sub-spec₀ a b a≤b
sub-spec₁ : ∀ a b → a ≤ b → a - b ≡ 𝟎
sub-spec₁ 𝟎 b t = refl
sub-spec₁ (ω^ a + c [ r ]) 𝟎 t = ⊥-rec (ω^≰𝟎 t)
sub-spec₁ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t with <-tri a b
sub-spec₁ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t | inl a<b = refl
sub-spec₁ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t | inr (inl a>b) = ⊥-rec (≤→≯ t (<₂ a>b))
sub-spec₁ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t | inr (inr a≡b) = sub-spec₁ c d (≤₃⁻¹ a≡b t)
sub-spec₂ : ∀ a b → a > b → a - b > 𝟎
sub-spec₂ (ω^ a + c [ r ]) 𝟎 <₁ = <₁
sub-spec₂ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t with <-tri a b
sub-spec₂ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t | inl a<b = ⊥-rec (<→≯ t (<₂ a<b))
sub-spec₂ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t | inr (inl a>b) = <₁
sub-spec₂ (ω^ a + c [ r ]) (ω^ b + d [ s ]) t | inr (inr a≡b) = sub-spec₂ c d (<₃⁻¹ (sym a≡b) t)
sub-spec₂' : ∀ a b → a - b > 𝟎 → a > b
sub-spec₂' a b a-b>0 with <-tri b a
... | inl a>b = a>b
... | inr a≤b = ⊥-rec (<-irreflexive (sym (sub-spec₁ a b a≤b)) a-b>0)
sub-spec₃ : ∀ a b → a - b ≤ a
sub-spec₃ 𝟎 b = 𝟎≤
sub-spec₃ (ω^ a + c [ r ]) 𝟎 = ≤-refl
sub-spec₃ (ω^ a + c [ r ]) (ω^ b + d [ s ]) with <-tri a b
... | inl a<b = 𝟎≤
... | inr (inl a>b) = ≤-refl
... | inr (inr a≡b) = ≤-trans (sub-spec₃ c d) (inl (right< a c r))
-𝟎-is-identity : {a : Cnf} → a - 𝟎 ≡ a
-𝟎-is-identity {𝟎} = refl
-𝟎-is-identity {ω^ a + b [ r ]} = refl
-𝟏-is-<-monotone : ∀ a b → a > 𝟎 → a < b → a - 𝟏 < b - 𝟏
-𝟏-is-<-monotone a@(ω^ a₁ + x [ r ]) b@(ω^ b₁ + y [ _ ]) <₁ (<₂ a₁<b₁)
with <-tri a₁ 𝟎 with <-tri b₁ 𝟎
... | inr (inl a₁>𝟎) | inr (inl b₁>𝟎) = <₂ a₁<b₁
... | inr (inl a₁>𝟎) | inr (inr b₁≡𝟎) = ⊥-rec (<→≯ a₁<b₁ (subst (a₁ >_) (sym b₁≡𝟎) a₁>𝟎))
... | inr (inr a₁≡𝟎) | inr (inl b₁>𝟎) = subst (_< b) (sym -𝟎-is-identity)
(<-trans (right< a₁ x r) (<₂ a₁<b₁))
... | inr (inr a₁≡𝟎) | inr (inr b₁≡𝟎) = ⊥-rec (<-irreflexive (a₁≡𝟎 ∙ sym b₁≡𝟎) a₁<b₁)
-𝟏-is-<-monotone (ω^ a₁ + x [ _ ]) (ω^ b₁ + y [ _ ]) <₁ (<₃ a₁≡b₁ x<y)
with <-tri a₁ 𝟎 with <-tri b₁ 𝟎
... | inr (inl a₁>𝟎) | inr (inl b₁>𝟎) = <₃ a₁≡b₁ x<y
... | inr (inl a₁>𝟎) | inr (inr b₁≡𝟎) = ⊥-rec (<-irreflexive (sym (a₁≡b₁ ∙ b₁≡𝟎)) a₁>𝟎)
... | inr (inr a₁≡𝟎) | inr (inl b₁>𝟎) = ⊥-rec (<-irreflexive (sym a₁≡𝟎 ∙ a₁≡b₁) b₁>𝟎)
... | inr (inr a₁≡𝟎) | inr (inr b₁≡𝟎) = subst2 _<_ (sym -𝟎-is-identity) (sym -𝟎-is-identity) x<y
left⟨-⟩< : ∀ a b c → left a < b → left (a - c) < b
left⟨-⟩< 𝟎 b c 𝟎<b = 𝟎<b
left⟨-⟩< (ω^ a + a' [ r ]) b 𝟎 a<b = a<b
left⟨-⟩< (ω^ a + a' [ r ]) b@(ω^ _ + _ [ _ ]) (ω^ c + c' [ t ]) a<b with <-tri a c
... | inl a<c = <₁
... | inr (inl a>c) = a<b
... | inr (inr a≡c) = left⟨-⟩< a' b c' (≤∘<-in-< r a<b)
left⟨-⟩≤ : ∀ a b c → left a ≤ b → left (a - c) ≤ b
left⟨-⟩≤ 𝟎 b c 𝟎≤b = 𝟎≤b
left⟨-⟩≤ (ω^ a + a' [ r ]) b 𝟎 a≤b = a≤b
left⟨-⟩≤ (ω^ a + a' [ r ]) b (ω^ c + c' [ t ]) a≤b with <-tri a c
... | inl a<c = 𝟎≤
... | inr (inl a>c) = a≤b
... | inr (inr a≡c) = left⟨-⟩≤ a' b c' (≤-trans r a≤b)
+<→<- : ∀ a b c → a + b < c → b < c - a
+<→<- 𝟎 b c b<𝟎 = subst (b <_) (sym -𝟎-is-identity) b<𝟎
+<→<- (ω^ a + a' [ r ]) 𝟎 c u = sub-spec₂ _ _ u
+<→<- (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ]) u with <-tri a b with <-tri c a
... | inl a<b | inl c<a = ⊥-rec (<→≯ u (<₂ (<-trans c<a a<b)))
... | inl a<b | inr (inl c>a) = u
... | inl a<b | inr (inr c≡a) = ⊥-rec (<→≯ u (<₂ (subst (_< b) (sym c≡a) a<b)))
... | inr a≥b | inl c<a = ⊥-rec (<→≯ u (<₂ c<a))
... | inr a≥b | inr (inl c>a) = <₂ (≤∘<-in-< a≥b c>a)
... | inr a≥b | inr (inr c≡a) = +<→<- a' (ω^ b + b' [ s ]) c' (<₃⁻¹ (sym c≡a) u)
+≡→≡- : ∀ a b c → a + b ≡ c → b ≡ c - a
+≡→≡- 𝟎 b c b≡c = b≡c ∙ sym -𝟎-is-identity
+≡→≡- (ω^ a + a' [ r ]) 𝟎 c e = sym (sub-spec₁ c _ (inr e))
+≡→≡- (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) 𝟎 e with <-tri a b
+≡→≡- (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) 𝟎 e | inl a<b = ⊥-rec (ω≢𝟎 e)
+≡→≡- (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) 𝟎 e | inr a≥b = ⊥-rec (ω≢𝟎 e)
+≡→≡- (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ]) e with <-tri a b with <-tri c a
... | inl a<b | inl c<a = ⊥-rec (<-irreflexive (sym e) (<₂ (<-trans c<a a<b)))
... | inl a<b | inr (inl c>a) = e
... | inl a<b | inr (inr c≡a) = ⊥-rec (<-irreflexive (sym e) (<₂ (subst (_< b) (sym c≡a) a<b)))
... | inr a≥b | inl c<a = ⊥-rec (<-irreflexive (sym e) (<₂ c<a))
... | inr a≥b | inr (inl c>a) = ⊥-rec (<-irreflexive e (<₂ c>a))
... | inr a≥b | inr (inr c≡a) = +≡→≡- a' (ω^ b + b' [ s ]) c' (cong right e)
+≤→≤- : ∀ a b c → a + b ≤ c → b ≤ c - a
+≤→≤- a b c (inl u) = inl (+<→<- a b c u)
+≤→≤- a b c (inr e) = inr (sym (+≡→≡- a b c (sym e)))
sub-monotone : ∀ {a b c} → a < b → b > c → a - c < b - c
sub-monotone {a} {b} {c} a<b b>c with <-tri a c
sub-monotone {a} {b} {c} a<b b>c | inl a<c = subst (_< b - c) (sym (sub-spec₁ a c (inl a<c))) (sub-spec₂ b c b>c)
sub-monotone {a} {b} {c} a<b b>c | inr c≤a = +<→<- c (a - c) b (subst (_< b) (sym (sub-spec₀ c a c≤a)) a<b)
x<ω-finite : (x : Cnf) → x < ω → Σ[ n ∈ ℕ ] (x ≡ NtoC n)
x<ω-finite 𝟎 x<ω = 0 , refl
x<ω-finite ω^ 𝟎 + b [ r ] x<ω = let (n , p) = x<ω-finite b (fin<ω b (≤𝟎→≡𝟎 r)) in suc n , Cnf⁼ refl p
x<ω-finite ω^ (ω^ a + a' [ r ]) + b [ q ] x<ω = ⊥-rec (ω≢𝟎 (<ω→fin x<ω))
x<ω+ω-finite : (x : Cnf) → x ≥ ω → x < ω + ω → Σ[ n ∈ ℕ ] (x ≡ ω + NtoC n)
x<ω+ω-finite x x≥ω x<ω+ω =
let (n , p) = x<ω-finite (x - ω) (sub-monotone {c = ω} x<ω+ω (<₃ refl <₁))
in n , sym (sub-spec₀ ω x x≥ω) ∙ cong (ω +_) p
x<ω+ω→x≤ω+n : (x : Cnf) → x < ω + ω → Σ[ n ∈ ℕ ] (x ≤ ω + NtoC n)
x<ω+ω→x≤ω+n 𝟎 _ = 0 , 𝟎≤
x<ω+ω→x≤ω+n (ω^ .𝟎 + _ [ _ ]) (<₂ <₁) = 0 , inl (<₂ <₁)
x<ω+ω→x≤ω+n (ω^ a + b [ _ ]) (<₃ a≡𝟏 b<ω) = n , inr goal
where
n : ℕ
n = fst (x<ω-finite b b<ω)
b≡n : b ≡ NtoC n
b≡n = snd (x<ω-finite b b<ω)
goal : ω + NtoC n ≡ ω^ a + b [ _ ]
goal = ω + NtoC n
≡⟨ cong (λ x → ω^⟨ x ⟩ + NtoC n) (sym a≡𝟏) ⟩
ω^⟨ a ⟩ + NtoC n
≡⟨ cong (ω^⟨ a ⟩ +_) (sym b≡n) ⟩
ω^⟨ a ⟩ + b
≡⟨ sym (ω^+≡ω^⟨⟩+ b _) ⟩
ω^ a + b [ _ ] ∎
+-left-cancellation-< : (a b c : Cnf) → a + b < a + c → b < c
+-left-cancellation-< 𝟎 b c p = p
+-left-cancellation-< ω^ a + a' [ r ] 𝟎 𝟎 p = ⊥-rec (<-irrefl p)
+-left-cancellation-< ω^ a + a' [ r ] 𝟎 ω^ c + c₁ [ x ] p = <₁
+-left-cancellation-< (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) 𝟎 p = ⊥-rec (<-irrefl (≤∘<-in-< (≤+r _ ω^ b + b' [ s ]) p))
+-left-cancellation-< x@(ω^ a + a' [ r ]) y@(ω^ b + b' [ s ]) z@(ω^ c + c' [ t ]) p with <-tri a b | <-tri a c
... | inl _ | inl _ = p
+-left-cancellation-< ω^ a + a' [ r ] ω^ b + b' [ s ] ω^ c + c' [ t ] (<₂ p) | inl q | inr _ = ⊥-rec (<-irrefl (<-trans p q))
+-left-cancellation-< ω^ a + a' [ r ] ω^ b + b' [ s ] ω^ c + c' [ t ] (<₃ x p) | inl q | inr _ = ⊥-rec (<-irreflexive (sym x) q)
+-left-cancellation-< ω^ a + a' [ r ] ω^ b + b' [ s ] ω^ c + c' [ t ] (<₂ p) | inr q | inl qq = <₂ (≤∘<-in-< q p )
+-left-cancellation-< ω^ a + a' [ r ] ω^ b + b' [ s ] ω^ c + c' [ t ] (<₃ e p) | inr q | inl qq = <₂ (≤∘<-in-< q qq )
+-left-cancellation-< ω^ a + a' [ r ] ω^ b + b' [ s ] ω^ c + c' [ t ] (<₂ p) | inr q | inr qq = ⊥-rec (<-irrefl p)
+-left-cancellation-< ω^ a + a' [ r ] ω^ b + b' [ s ] ω^ c + c' [ t ] (<₃ x p) | inr q | inr qq = +-left-cancellation-< a' (ω^ b + b' [ s ]) (ω^ c + c' [ t ]) p