----------------------------------------------------------------------------------------------------
-- Subtraction of Cantor Normal Forms
----------------------------------------------------------------------------------------------------

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

module CantorNormalForm.Subtraction where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sum
open import Cubical.Data.Empty
  renaming (rec to ⊥-rec)

open import CantorNormalForm.Base
open import CantorNormalForm.Addition


{- Subtraction -}

infixl  _-_

_-_ : 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

{- Some properties of subtraction -}

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₄

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

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)))