{-# OPTIONS --cubical-compatible #-}
module CantorNormalForm.WithPropositionalEquality.Addition where
open import Data.Product renaming (proj₁ to fst; proj₂ to snd)
open import Data.Sum renaming (inj₁ to inl; inj₂ to inr)
open import Data.Empty
renaming (⊥-elim to ⊥-rec)
open import Agda.Builtin.Nat
renaming (Nat to ℕ) using (zero ; suc)
open import CantorNormalForm.WithPropositionalEquality.Base
infixl 35 _+_
mutual
_+_ : Cnf → Cnf → Cnf
𝟎 + b = b
a + 𝟎 = a
(ω^ a + c [ r ]) + (ω^ b + d [ s ]) with <-tri a b
... | inl a<b = ω^ b + d [ s ]
... | inr a≥b = ω^ a + (c + ω^ b + d [ s ]) [ ≥left+ c _ r a≥b ]
≥left+ : {a : Cnf} (b c : Cnf)
→ a ≥ left b → a ≥ left c → a ≥ left (b + c)
≥left+ 𝟎 _ r s = s
≥left+ (ω^ _ + _ [ _ ]) 𝟎 r s = r
≥left+ (ω^ b + _ [ _ ]) (ω^ c + _ [ _ ]) r s with <-tri b c
... | inl b<c = s
... | inr b≥c = r
+𝟎-is-identity : {a : Cnf} → a + 𝟎 ≡ a
+𝟎-is-identity {𝟎} = refl
+𝟎-is-identity {ω^ a + b [ r ]} = refl
+-is-assoc : ∀ a b c → a + (b + c) ≡ (a + b) + c
+-is-assoc 𝟎 b c = refl
+-is-assoc (ω^ a + a' [ r ]) 𝟎 c = refl
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) 𝟎 = sym +𝟎-is-identity
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
with <-tri a b with <-tri b c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inl a<b | inl b<c with <-tri b c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inl a<b | inl b<c | inl _ with <-tri a c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inl a<b | inl b<c | inl _ | inl a<c = refl
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inl a<b | inl b<c | inl _ | inr a≥c = ⊥-rec (≤→≯ a≥c (<-trans a<b b<c))
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inl a<b | inl b<c | inr b≥c = ⊥-rec (≤→≯ b≥c b<c)
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inl a<b | inr b≥c with <-tri a b
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inl a<b | inr b≥c | inl _ with <-tri b c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inl a<b | inr b≥c | inl _ | inl b<c = ⊥-rec (≤→≯ b≥c b<c)
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inl a<b | inr b≥c | inl _ | inr _ = Cnf⁼ refl refl
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inl a<b | inr b≥c | inr a≥b = ⊥-rec (≤→≯ a≥b a<b)
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inr a≥b | inl b<c with <-tri a c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inr a≥b | inl b<c | inl a<c = refl
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inr a≥b | inl b<c | inr a≥c = Cnf⁼ refl (claim₁ ∙ IH)
where
IH : a' + (ω^ b + b' [ s ] + ω^ c + c' [ t ]) ≡ (a' + ω^ b + b' [ s ]) + ω^ c + c' [ t ]
IH = +-is-assoc a' (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
claim₀ : ω^ c + c' [ t ] ≡ ω^ b + b' [ s ] + ω^ c + c' [ t ]
claim₀ with <-tri b c
claim₀ | inl _ = refl
claim₀ | inr b≥c = ⊥-rec (≤→≯ b≥c b<c)
claim₁ : a' + ω^ c + c' [ t ] ≡ a' + (ω^ b + b' [ s ] + ω^ c + c' [ t ])
claim₁ = cong (a' +_) claim₀
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inr a≥b | inr b≥c with <-tri a c
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inr a≥b | inr b≥c | inl a<c = ⊥-rec (≤→≯ (≤-trans b≥c a≥b) a<c)
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inr a≥b | inr b≥c | inr a≥c with <-tri a b
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inr a≥b | inr b≥c | inr a≥c | inl a<b = ⊥-rec (≤→≯ a≥b a<b)
+-is-assoc (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
| inr a≥b | inr b≥c | inr a≥c | inr _ = Cnf⁼ refl (claim₁ ∙ IH)
where
IH : a' + (ω^ b + b' [ s ] + ω^ c + c' [ t ]) ≡ (a' + ω^ b + b' [ s ]) + ω^ c + c' [ t ]
IH = +-is-assoc a' (ω^ b + b' [ s ]) (ω^ c + c' [ t ])
claim₀ : ω^ b + (b' + ω^ c + c' [ t ]) [ _ ] ≡ ω^ b + b' [ s ] + ω^ c + c' [ t ]
claim₀ with <-tri b c
claim₀ | inl b<c = ⊥-rec (≤→≯ b≥c b<c)
claim₀ | inr _ = Cnf⁼ refl refl
claim₁ : a' + (ω^ b + (b' + ω^ c + c' [ t ]) [ _ ]) ≡ a' + (ω^ b + b' [ s ] + ω^ c + c' [ t ])
claim₁ = cong (a' +_) claim₀
≤+r : ∀ a b → a ≤ a + b
≤+r 𝟎 b = 𝟎≤
≤+r (ω^ a + c [ r ]) 𝟎 = inr refl
≤+r (ω^ a + c [ r ]) (ω^ b + d [ s ]) with <-tri a b
... | inl a<b = inl (<₂ a<b)
... | inr a≥b = ≤₃ refl (≤+r c _)
<+r : ∀ a b → b > 𝟎 → a < a + b
<+r 𝟎 (ω^ b + d [ s ]) <₁ = <₁
<+r (ω^ a + c [ r ]) (ω^ b + d [ s ]) <₁ with <-tri a b
... | inl a<b = <₂ a<b
... | inr a≥b = <₃ refl (<+r c (ω^ b + d [ s ]) <₁ )
+r-is-<-monotone : ∀ a b c → b < c → a + b < a + c
+r-is-<-monotone 𝟎 b c b<c = b<c
+r-is-<-monotone (ω^ a + a' [ r ]) 𝟎 c <₁ = <+r _ c <₁
+r-is-<-monotone (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ]) (<₂ b<c)
with <-tri a b with <-tri a c
... | inl a<b | inl a<c = <₂ b<c
... | inl a<b | inr a≥c = ⊥-rec (≤→≯ a≥c (<-trans a<b b<c))
... | inr a≥b | inl a<c = <₂ a<c
... | inr a≥b | inr a≥c = <₃ refl (+r-is-<-monotone a' _ _ (<₂ b<c))
+r-is-<-monotone (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) (ω^ c + c' [ t ]) (<₃ b≡c b'<c')
with <-tri a b with <-tri a c
... | inl a<b | inl a<c = <₃ b≡c b'<c'
... | inl a<b | inr a≥c = ⊥-rec (≤→≯ (≤-trans (inr (sym b≡c)) a≥c) a<b)
... | inr a≥b | inl a<c = ⊥-rec (≤→≯ (≤-trans (inr b≡c) a≥b) a<c)
... | inr a≥b | inr a≥c = <₃ refl (+r-is-<-monotone a' _ _ (<₃ b≡c b'<c'))
+r-is-≤-monotone : ∀ a b c → b ≤ c → a + b ≤ a + c
+r-is-≤-monotone a b c (inl b<c) = inl (+r-is-<-monotone a b c b<c)
+r-is-≤-monotone a b c (inr c≡b) = inr (cong (a +_) c≡b)
≤l+ : ∀ a b → a ≤ b + a
≤l+ 𝟎 b = 𝟎≤
≤l+ (ω^ _ + _ [ _ ]) 𝟎 = ≤-refl
≤l+ (ω^ a + x [ r ]) (ω^ b + y [ _ ]) with <-tri b a
... | inl b<a = ≤-refl
... | inr (inl b>a) = inl (<₂ b>a)
... | inr (inr b≡a) = inl (<₃ (sym b≡a) (<∘≤-in-< (right< a x r) (≤l+ (ω^ a + x [ r ]) y)))
<l+ : ∀ a b → b > 𝟎 → left a ≤ left b → a < b + a
<l+ 𝟎 b@(ω^ a₁ + a' [ _ ]) <₁ _ = <₁
<l+ a@(ω^ a₁ + a' [ _ ]) b@(ω^ b₁ + b' [ _ ]) <₁ (inl a₁<b₁) with <-tri b₁ a₁
... | inl b₁<a₁ = ⊥-rec (<→≯ a₁<b₁ b₁<a₁)
... | inr _ = <₂ a₁<b₁
<l+ a@(ω^ a₁ + a' [ r ]) b@(ω^ b₁ + b' [ _ ]) <₁ (inr b₁≡a₁) with <-tri b₁ a₁
... | inl b₁<a₁ = ⊥-rec (<-irreflexive b₁≡a₁ b₁<a₁)
... | inr _ = <₃ (sym b₁≡a₁) (<∘≤-in-< (right< a₁ a' r) (≤l+ a b'))
l+-is-≤-monotone : ∀ a b c → a ≤ b → a + c ≤ b + c
l+-is-≤-monotone 𝟎 b c a≤b = ≤l+ c b
l+-is-≤-monotone (ω^ u + x [ r ]) 𝟎 c a≤b = ⊥-rec (ω^≰𝟎 a≤b)
l+-is-≤-monotone (ω^ u + x [ r ]) (ω^ v + y [ s ]) 𝟎 a≤b = a≤b
l+-is-≤-monotone (ω^ u + x [ r ]) (ω^ v + y [ s ]) c@(ω^ w + z [ t ]) (inr a≡b) =
inr (cong (_+ c) a≡b)
l+-is-≤-monotone (ω^ u + x [ r ]) (ω^ v + y [ s ]) c@(ω^ w + z [ t ]) (inl a<b)
with (<-tri u w) with (<-tri v w) with a<b
... | inl u<w | inl v<w | _ = ≤-refl
... | inl u<w | inr (inl v>w) | _ = inl (<₂ v>w)
... | inl u<w | inr (inr v≡w) | _ = inl (<₃ (sym v≡w) (<∘≤-in-< (right< w z t) (≤l+ c y)))
... | inr u≥w | inl v<w | _ = ⊥-rec (≤→≯ (inl a<b) (<₂ (<∘≤-in-< v<w u≥w)))
... | inr u≥w | inr v≥w | <₂ u<v = inl (<₂ u<v)
... | inr u≥w | inr v≥w | <₃ u≡v x<y = ≤₃ u≡v (l+-is-≤-monotone x y c (inl x<y))
+-is-≤-monotone : ∀ a b c d → a ≤ b → c ≤ d → a + c ≤ b + d
+-is-≤-monotone a b c d a≤b c≤d = ≤-trans a+c≤b+c b+c≤b+d
where
a+c≤b+c : a + c ≤ b + c
a+c≤b+c = l+-is-≤-monotone a b c a≤b
b+c≤b+d : b + c ≤ b + d
b+c≤b+d = +r-is-≤-monotone b c d c≤d
ω^+≡ω^⟨⟩+ : ∀ {a} b r → ω^ a + b [ r ] ≡ ω^⟨ a ⟩ + b
ω^+≡ω^⟨⟩+ {a} 𝟎 _ = Cnf⁼ refl refl
ω^+≡ω^⟨⟩+ {a} (ω^ b + c [ r ]) a≥b with <-tri a b
... | inl a<b = ⊥-rec (≤→≯ a≥b a<b)
... | inr _ = Cnf⁼ refl refl
+-left-cancel : ∀ a b → left a < left b → a + b ≡ b
+-left-cancel 𝟎 b _ = refl
+-left-cancel (ω^ a + c [ r ]) (ω^ b + d [ s ]) a<b with <-tri a b
... | inl _ = refl
... | inr a≥b = ⊥-rec (≤→≯ a≥b a<b)
left⟨+⟩ : ∀ a b → left a ≥ left b → left a ≡ left (a + b)
left⟨+⟩ 𝟎 b lb≤𝟎 = sym (≤𝟎→≡𝟎 lb≤𝟎)
left⟨+⟩ (ω^ a + c [ r ]) 𝟎 _ = refl
left⟨+⟩ (ω^ a + c [ r ]) (ω^ b + d [ s ]) a≥b with <-tri a b
... | inl a<b = ⊥-rec (≤→≯ a≥b a<b)
... | inr _ = refl
left⟨+⟩≤⁻¹ : ∀ a b c → left (a + b) ≤ c → (left a ≤ c) × (left b ≤ c)
left⟨+⟩≤⁻¹ 𝟎 b c t = 𝟎≤ , t
left⟨+⟩≤⁻¹ (ω^ a + a' [ r ]) 𝟎 c t = t , 𝟎≤
left⟨+⟩≤⁻¹ (ω^ a + a' [ r ]) (ω^ b + b' [ s ]) c t with <-tri a b
... | inl a<b = ≤-trans (inl a<b) t , t
... | inr a≥b = t , ≤-trans a≥b t
ω^-is-add-indecomposable : ∀ a b {c} →
a < ω^⟨ c ⟩ → b < ω^⟨ c ⟩ → a + b < ω^⟨ c ⟩
ω^-is-add-indecomposable 𝟎 b a< b< = b<
ω^-is-add-indecomposable a@(ω^ _ + _ [ _ ]) 𝟎 a< b< = a<
ω^-is-add-indecomposable a@(ω^ a₁ + x [ _ ])
b@(ω^ b₁ + y [ _ ])
{c} a< b< with <-tri a₁ b₁ with a<
... | inl a₁<b₁ | _ = b<
... | inr a₁≥b₁ | <₂ a₁<c = <₂ a₁<c
<+𝟏 : ∀ {x} → x < x + 𝟏
<+𝟏 {𝟎} = <₁
<+𝟏 {ω^ a + b [ c ]} with <-tri a 𝟎
... | inr _ = <₃ refl <+𝟏
<→+𝟏≤ : ∀ {x y} → x < y → x + 𝟏 ≤ y
<→+𝟏≤ {𝟎} {ω^ c + d [ s ]} <₁ = 𝟏≤ω^
<→+𝟏≤ {ω^ a + b [ r ]} {ω^ c + d [ s ]} (<₂ a<c) with <-tri a 𝟎
... | inr _ = inl (<₂ a<c)
<→+𝟏≤ {ω^ a + b [ r ]} {ω^ c + d [ s ]} (<₃ a≡c b<d) with <-tri a 𝟎
... | inr _ = ≤₃ a≡c (<→+𝟏≤ b<d)
<+𝟏→≤ : ∀ {x y} → x < y + 𝟏 → x ≤ y
<+𝟏→≤ {𝟎} {y} _ = 𝟎≤
<+𝟏→≤ {ω^ a + b [ r ]} {𝟎} t = ⊥-rec (ω^≮𝟏 t)
<+𝟏→≤ {ω^ a + b [ r ]} {ω^ c + d [ s ]} t with <-tri c 𝟎
... | inr _ with ω^<-cases t
... | inl a<c = inl (<₂ a<c)
... | inr (a≡c , b<d+1) = ≤₃ a≡c (<+𝟏→≤ b<d+1)
ω^𝟎+-is-+𝟏 : (a : Cnf) (r : 𝟎 ≥ left a) → a + 𝟏 ≡ ω^ 𝟎 + a [ r ]
ω^𝟎+-is-+𝟏 𝟎 _ = Cnf⁼ refl refl
ω^𝟎+-is-+𝟏 ω^ a + b [ r ] (inr 𝟎≡a) with <-tri a 𝟎
... | inr _ = goal
where
𝟎≥lb : 𝟎 ≥ left b
𝟎≥lb = subst (_≥ left b) (sym 𝟎≡a) r
IH : b + 𝟏 ≡ ω^ 𝟎 + b [ 𝟎≥lb ]
IH = ω^𝟎+-is-+𝟏 b 𝟎≥lb
goal : ω^ a + (b + 𝟏) [ _ ] ≡ ω^ 𝟎 + (ω^ a + b [ r ]) [ inr 𝟎≡a ]
goal = Cnf⁼ (sym 𝟎≡a) (IH ∙ Cnf⁼ 𝟎≡a refl)
NtoC⟨suc⟩≡NtoC+𝟏 : ∀ n → NtoC (suc n) ≡ NtoC n + 𝟏
NtoC⟨suc⟩≡NtoC+𝟏 n = sym (ω^𝟎+-is-+𝟏 (NtoC n) _)