----------------------------------------------------------------------------------------------------
-- Classifiability of Cantor Normal Forms
----------------------------------------------------------------------------------------------------

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

module CantorNormalForm.Classifiability where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Data.Empty
  renaming (rec to ⊥-rec)
open import Cubical.Data.Nat
  using (ℕ ; zero ; suc)
open import Cubical.Relation.Nullary
open import Cubical.HITs.PropositionalTruncation.Properties
  renaming (rec to ∥-∥rec)

open import CantorNormalForm.Base
open import CantorNormalForm.Addition
open import CantorNormalForm.Multiplication
open import CantorNormalForm.Wellfoundedness
open import Abstract.ZerSucLim _<_ _≤_ public

open Properties
 Cnf-is-set
 (λ _ _ → isProp⟨<⟩)
 (λ _ _ → isProp⟨≤⟩)
 (λ _ → <-irrefl)
 (λ _ → ≤-refl)
 (λ _ _ _ → ≤-trans)
 ≤-antisym
 <∘≤-in-<
 public


{- Zero -}

𝟎-is-zero : is-zero 𝟎
𝟎-is-zero _ = 𝟎≤

is-zero→≡𝟎 : {a : Cnf} → is-zero a → a ≡ 𝟎
is-zero→≡𝟎 {𝟎} _ = refl
is-zero→≡𝟎 {ω^ a + b [ r ]} h = ⊥-rec (ω^≰𝟎 (h 𝟎))

ω^-is-not-zero : ∀ {a b r} → ¬ (is-zero (ω^ a + b [ r ]))
ω^-is-not-zero p = ω^≰𝟎 (p 𝟎)


{- Successor -}

+𝟏-calc-strong-suc : (a : Cnf) → (a + 𝟏) is-strong-suc-of a
+𝟏-calc-strong-suc a = (<+𝟏 , λ _ → <→+𝟏≤) , (λ _ → <+𝟏→≤)

+𝟏-calc-suc : (a : Cnf) → (a + 𝟏) is-suc-of a
+𝟏-calc-suc a = fst (+𝟏-calc-strong-suc a)

suc→+𝟏 : ∀ {a b} → a is-suc-of b → b + 𝟏 ≡ a
suc→+𝟏 {a} {b} u = cong fst (suc-unique b (b + 𝟏 , +𝟏-calc-suc b) (a , u))

is-suc→is-strong-suc : ∀ {a b} → a is-suc-of b → a is-strong-suc-of b
is-suc→is-strong-suc {a} {b} u = subst (_is-strong-suc-of b) (suc→+𝟏 u) (+𝟏-calc-strong-suc b)

ω^𝟎+-is-strong-suc : (a : Cnf) (r : 𝟎 ≥ left a) → is-strong-suc (ω^ 𝟎 + a [ r ])
ω^𝟎+-is-strong-suc a r = subst is-strong-suc (ω^𝟎+-is-+𝟏 a r) (a , +𝟏-calc-strong-suc a)

right-is-strong-suc₀ : ∀ {x} → is-strong-suc (right x) → is-strong-suc x
right-is-strong-suc₀ {𝟎} ()
right-is-strong-suc₀ {ω^ a + b [ r ]} (c , (c<b , p) , q) = (ω^ a + c [ s ]) , (t , p') , q'
 where
  s : left c ≤ a
  s = ≤-trans (left-is-<-≤-monotone c<b) r
  t : ω^ a + c [ s ] < ω^ a + b [ r ]
  t = <₃ refl c<b
  p' : ∀ x → ω^ a + c [ s ] < x → ω^ a + b [ r ] ≤ x
  p' (ω^ d + e [ u ]) (<₂ a<d) = inl (<₂ a<d)
  p' (ω^ d + e [ u ]) (<₃ a≡d c<e) = ≤₃ a≡d (p e c<e)
  q' : ∀ x → x < ω^ a + b [ r ] → x ≤ ω^ a + c [ s ]
  q' 𝟎 <₁ = inl <₁
  q' (ω^ d + e [ u ]) (<₂ d<a) = inl (<₂ d<a)
  q' (ω^ d + e [ u ]) (<₃ d≡a e<b) = ≤₃ d≡a (q e e<b)

is-strong-suc-impossible : ∀ {a b c d r s} → a > b →
    ¬ ((ω^ a + c [ r ]) is-strong-suc-of (ω^ b + d [ s ]))
is-strong-suc-impossible {a} {b} {𝟎} {d} {r} {s} a>b ((t , p) , q) = ≤→≯ claim₀ claim₁
 where
  claim₀ : ω^ a + 𝟎 [ _ ] ≤ ω^ b + (d + 𝟏) [ _ ]
  claim₀ = p (ω^ b + (d + 𝟏) [ ≥left+ d 𝟏 s 𝟎≤ ]) (<₃ refl <+𝟏)
  claim₁ : ω^ a + 𝟎 [ _ ] > ω^ b + (d + 𝟏) [ _ ]
  claim₁ = <₂ a>b
is-strong-suc-impossible {a} {b} {ω^ _ + _ [ _ ]} {d} {r} {s} a>b ((t , p) , q) = ≤→≯ claim₀ claim₁
 where
  claim₀ : ω^ a + 𝟎 [ _ ] ≤ ω^ b + d [ _ ]
  claim₀ = q ω^⟨ a ⟩ (<₃ refl <₁)
  claim₁ : ω^ a + 𝟎 [ _ ] > ω^ b + d [ _ ]
  claim₁ = <₂ a>b

right-is-strong-suc₁ : ∀ {x} → left x > 𝟎 → is-strong-suc x → is-strong-suc (right x)
right-is-strong-suc₁ <₁ (𝟎 , (<₁ , p) , q) = ⊥-rec (ω^≰𝟎 (q 𝟏 (<₂ <₁)))
right-is-strong-suc₁ <₁ (_ , (<₂ t , p) , q) = ⊥-rec (is-strong-suc-impossible t ((<₂ t , p) , q))
right-is-strong-suc₁ {ω^ (ω^ a + b [ r ]) + c [ s ]} <₁ (ω^ d + e [ t ] , (<₃ d≡ e<c , p) , q) =
    e , (e<c , p') , q'
 where
  p' : ∀ x → e < x → c ≤ x
  p' x e<x with <-tri d (left x)
  ... | inl d<lx = ≤-trans (inl (right< _ _ _)) fact
   where
    fact : ω^ ω^ a + b [ r ] + c [ s ] ≤ x
    fact = p x (<₂' d<lx)
  ... | inr d≥lx = ≤₃⁻¹ (sym d≡) fact
   where
    fact : ω^ ω^ a + b [ r ] + c [ s ] ≤ ω^ d + x [ d≥lx ]
    fact = p (ω^ d + x [ d≥lx ]) (<₃ refl e<x)
  q' : ∀ x → x < c → x ≤ e
  q' x x<c with <-tri d (left x)
  ... | inl d<lx = ⊥-rec (≤→≯ fact (<₂' d<lx))
   where
    fact : x ≤ ω^ d + e [ t ]
    fact = q x (<-trans x<c (right< _ _ _))
  ... | inr d≥lx = ≤₃⁻¹ refl fact
   where
    fact : ω^ d + x [ d≥lx ] ≤ ω^ d + e [ t ]
    fact = q (ω^ d + x [ d≥lx ]) (<₃ d≡ x<c)

is-strong-suc-dec : (a : Cnf) → (is-strong-suc a) ⊎ (¬ (is-strong-suc a))
is-strong-suc-dec 𝟎 = inr (λ ())
is-strong-suc-dec ω^ 𝟎 + c [ r ] = inl (ω^𝟎+-is-strong-suc c r)
is-strong-suc-dec ω^ (ω^ a + b [ s ]) + c [ r ] with is-strong-suc-dec c
... | inl u = inl (right-is-strong-suc₀ u)
... | inr f = inr (λ u → f (right-is-strong-suc₁ <₁ u))

right-is-not-strong-suc : {a : Cnf} → ¬ (is-strong-suc a) → ¬ (is-strong-suc (right a))
right-is-not-strong-suc {𝟎} f = f
right-is-not-strong-suc {ω^ a + b [ r ]} f (c , (c<b , p) , q) = f (x , (s , p') , q')
 where
  x : Cnf
  x = ω^ a + c [ ≤-trans (left-is-<-≤-monotone c<b) r ]
  s : x < ω^ a + b [ r ]
  s = <₃ refl c<b
  p' : ∀ y → x < y → ω^ a + b [ r ] ≤ y
  p' (ω^ y + z [ _ ]) (<₂ a<y) = inl (<₂ a<y)
  p' (ω^ y + z [ _ ]) (<₃ a≡y c<z) = ≤₃ a≡y (p z c<z)
  q' : ∀ y → y < ω^ a + b [ r ] → y ≤ x
  q' 𝟎 <₁ = 𝟎≤
  q' (ω^ y + z [ _ ]) (<₂ y<a) = inl (<₂ y<a)
  q' (ω^ y + z [ _ ]) (<₃ y≡a z<b) = ≤₃ y≡a (q z z<b)


{- Limit -}

{- Example: ω is the limit of NtoC -}

NtoC↑ : is-<-increasing NtoC
NtoC↑        = <₁
NtoC↑ (suc i) = <₃ refl (NtoC↑ i)

ω-is-lim-of-NtoC : ω is-lim-of (NtoC , NtoC↑)
ω-is-lim-of-NtoC = NtoC≤ω , ω-min-over-NtoC
 where
  NtoC≤ω : ∀ i → NtoC i ≤ ω
  NtoC≤ω        = inl <₁
  NtoC≤ω (suc i) = inl (<₂ <₁)
  ω-min-over-NtoC-lem : ∀ x → (∀ i → NtoC i ≤ x) → ¬ (x < ω)
  ω-min-over-NtoC-lem 𝟎 h <₁ = ω^≰𝟎 (h )
  ω-min-over-NtoC-lem x@(ω^ a + b [ r ]) h (<₂ a<𝟏) = ≤→≯ sn≤x x<sn
   where
    a≡𝟎 : a ≡ 𝟎
    a≡𝟎 = <𝟏→≡𝟎 a<𝟏
    n : ℕ
    n = fst (left≡𝟎-is-nat x a≡𝟎)
    x≡n : x ≡ NtoC n
    x≡n = snd (left≡𝟎-is-nat x a≡𝟎)
    x<sn : x < NtoC (suc n)
    x<sn = subst (_< NtoC (suc n)) (sym x≡n) (NtoC↑ n)
    sn≤x : NtoC (suc n) ≤ x
    sn≤x = h (suc n)
  ω-min-over-NtoC : ∀ x → (∀ i → NtoC i ≤ x) → ω ≤ x
  ω-min-over-NtoC x h = ≮→≥ (ω-min-over-NtoC-lem x h)


{- Fundamental sequences -}

private
 P : Cnf → Type
 P a = a > 𝟎 → ¬ (is-strong-suc a) → is-Σlim a

fundamental-sequence-step : ∀ a → (∀ b → b < a → P b) → P a
fundamental-sequence-step (ω^ 𝟎 + b [ r ]) H <₁ not-suc = ⊥-rec (not-suc (ω^𝟎+-is-strong-suc b r))
fundamental-sequence-step (ω^ a@(ω^ _ + _ [ _ ]) + 𝟎 [ r ]) H <₁ not-suc with is-strong-suc-dec a
fundamental-sequence-step (ω^ a@(ω^ _ + _ [ _ ]) + 𝟎 [ r ]) H <₁ not-suc | inl (x , (x<a , p) , q) =
    (g , g↑) , pp , qq
 where -- ω^a = ω^{x+1} = ω^x·ω = lim(λi.ω^x·i)
  g : ℕ → Cnf
  g i = ω^⟨ x ⟩ • i
  g↑ : is-<-increasing g
  g↑ = ω^•-is-<-increasing ω^⟨ x ⟩ <₁
  pp : ∀ i → g i ≤ ω^ a + 𝟎 [ r ]
  pp i = inl (<₂' (≤∘<-in-< (left•≤ ω^⟨ x ⟩ i) x<a))
  qq : ∀ z → (∀ i → g i ≤ z) → ω^ a + 𝟎 [ r ] ≤ z
  qq 𝟎 h = ⊥-rec (ω^≰𝟎 (h ))
  qq (ω^ u + v [ _ ]) h with <-tri a u
  qq (ω^ u + v [ _ ]) h | inl a<u = inl (<₂ a<u)
  qq (ω^ u + v [ w ]) h | inr (inl a>u) = ⊥-rec (≤→≯ claim₂ claim₁)
   where
    u≤x : u ≤ x
    u≤x = q u a>u
    x≤u : x ≤ u
    x≤u = left-is-≤-monotone (h )
    x≡u : x ≡ u
    x≡u = ≤-antisym x≤u u≤x
    claim₀ : Σ[ n ∈ ℕ ] (ω^ u + v [ w ] < ω^⟨ x ⟩ • suc n)
    claim₀ = Σn<•sn _ (inr x≡u)
    n : ℕ
    n = suc (fst claim₀)
    claim₁ : ω^ u + v [ w ] < ω^⟨ x ⟩ • n
    claim₁ = snd claim₀
    claim₂ : ω^⟨ x ⟩ • n ≤ ω^ u + v [ w ]
    claim₂ = h n
  qq (ω^ u + v [ _ ]) h | inr (inr x≡u) = ≤₃ x≡u 𝟎≤
fundamental-sequence-step (ω^ a@(ω^ _ + _ [ _ ]) + 𝟎 [ r ]) H <₁ not-suc | inr a-is-not-suc =
    (g , g↑) , p , q
 where  -- ω^a = ω^(lim(f)) = lim(λi.ω^(fi))
  IH : is-Σlim a
  IH = H a left< <₁ a-is-not-suc
  f : ℕ → Cnf
  f = fst (fst IH)
  g : ℕ → Cnf
  g i = ω^⟨ f i ⟩
  g↑ : is-<-increasing g
  g↑ i = <₂ (snd (fst IH) i)
  p : ∀ i → g i ≤ ω^ a + 𝟎 [ r ]
  p i = ≤₂ (fst (snd IH) i)
  q : ∀ z → (∀ i → g i ≤ z) → ω^ a + 𝟎 [ r ] ≤ z
  q 𝟎 h = ⊥-rec (ω^≰𝟎 (h ))
  q (ω^ u + v [ _ ]) h = ≤-trans claim₀ claim₁
   where
    f≤u : ∀ i → f i ≤ u
    f≤u i = left-is-≤-monotone (h i)
    a≤u : a ≤ u
    a≤u = snd (snd IH) u f≤u
    claim₀ : ω^ a + 𝟎 [ r ] ≤ ω^ u + 𝟎 [ 𝟎≤ ]
    claim₀ = ≤₂ a≤u
    claim₁ : ω^ u + 𝟎 [ _ ] ≤ ω^ u + v [ _ ]
    claim₁ = ≤₃ refl 𝟎≤
fundamental-sequence-step (ω^ a@(ω^ _ + _ [ _ ]) + b@(ω^ _ + _ [ _ ]) [ r ]) H <₁ not-suc
    with is-strong-suc-dec b
fundamental-sequence-step (ω^ a@(ω^ _ + _ [ _ ]) + b@(ω^ _ + _ [ _ ]) [ r ]) H <₁ not-suc
    | inl b-is-suc = ⊥-rec (not-suc (right-is-strong-suc₀ b-is-suc))
fundamental-sequence-step (ω^ a@(ω^ _ + _ [ _ ]) + b@(ω^ _ + _ [ _ ]) [ r ]) H <₁ not-suc
    | inr b-is-not-suc = (g , g↑) , p , q
 where  -- ω^a+b = ω^a+lim(f) = lim(λi.ω^a+fi)
  IH : is-Σlim b
  IH = H b (right< _ _ _) <₁ b-is-not-suc
  f : ℕ → Cnf
  f = fst (fst IH)
  a≥lf : ∀ i → a ≥ left (f i)
  a≥lf i = ≤-trans (left-is-≤-monotone (fst (snd IH) i)) r
  g : ℕ → Cnf
  g i = ω^ a + f i [ a≥lf i ]
  g↑ : is-<-increasing g
  g↑ i = <₃ refl (snd (fst IH) i)
  p : ∀ i → g i ≤ ω^ a + b [ r ]
  p i = ≤₃ refl (fst (snd IH) i)
  q : ∀ z → (∀ i → g i ≤ z) → ω^ a + b [ r ] ≤ z
  q 𝟎 h = ⊥-rec (ω^≰𝟎 (h ))
  q (ω^ u + v [ _ ]) h with <-tri a u
  ... | inl a<u = inl (<₂ a<u)
  ... | inr (inl a>u) = ⊥-rec (≤→≯ (h ) (<₂ a>u))
  ... | inr (inr a≡u) = ≤₃ a≡u (snd (snd IH) v (λ i → ≤₃⁻¹ a≡u (h i)))


fundamental-sequence : (a : Cnf) → a > 𝟎 → ¬ (is-strong-suc a) → is-Σlim a
fundamental-sequence = wf-ind fundamental-sequence-step

lim>𝟎 : ∀ {a} → is-lim a → a > 𝟎
lim>𝟎 {𝟎} = ∥-∥rec isProp⟨<⟩ (λ ((_ , f↑) , f≤𝟎 , _) → ⊥-rec (≮𝟎 (<∘≤-in-< (f↑ ) (f≤𝟎 ))))
lim>𝟎 {ω^ _ + _ [ _ ]} _ = <₁

lim-is-not-suc : ∀ {a} → is-lim a → ¬ (is-strong-suc a)
lim-is-not-suc la sa = unique.not-s-and-l _ sa la

FS : ∀ a → is-lim a → ℕ → Cnf
FS a la = fst (fst (fundamental-sequence a (lim>𝟎 la) (lim-is-not-suc la)))

FS↑ : ∀ a → (la : is-lim a) → is-<-increasing (FS a la)
FS↑ a la = snd (fst (fundamental-sequence a (lim>𝟎 la) (lim-is-not-suc la)))

FS≤lim : ∀ a → (la : is-lim a) → ∀ i → FS a la i ≤ a
FS≤lim a la = fst (snd (fundamental-sequence a (lim>𝟎 la) (lim-is-not-suc la)))

lim-is-min-over-FS : ∀ a → (la : is-lim a) → ∀ x → (∀ i → FS a la i ≤ x) → a ≤ x
lim-is-min-over-FS a la = snd (snd (fundamental-sequence a (lim>𝟎 la) (lim-is-not-suc la)))


{- Cnf is classifiable, i.e., every CNF is either zero, successor or limit. -}

Cnf-is-Σclassifiable : (a : Cnf) → is-Σclassifiable a
Cnf-is-Σclassifiable 𝟎 = inl 𝟎-is-zero
Cnf-is-Σclassifiable a@(ω^ _ + _ [ _ ]) with is-strong-suc-dec a
... | inl a-is-suc     = inr (inl a-is-suc)
... | inr a-is-not-suc = inr (inr a-is-lim)
 where
  a-is-lim : is-Σlim a
  a-is-lim = fundamental-sequence a <₁ a-is-not-suc

Cnf-is-classifiable : (a : Cnf) → is-classifiable a
Cnf-is-classifiable a = to-is-classifiable (Cnf-is-Σclassifiable a)

{- Classifiability induction -}

open ClassifiabilityInduction Cnf-is-classifiable <IsWellFounded

cf-ind : ∀ {ℓ} {P : Cnf → Type ℓ}
      → (∀ a → isProp (P a))
      → P 𝟎
      → (∀ a → P a → P (a + 𝟏))
      → (∀ a f f↑ → a is-lim-of (f , f↑) → (∀ i → P (f i)) → P a)
      → ∀ a → P a
cf-ind {_} {P} pP p0 ps = ind pP p0' ps'
 where
  p0' : ∀ a → is-zero a → P a
  p0' a a-is-zero = subst P (sym (≤𝟎→≡𝟎 (a-is-zero 𝟎))) p0
  ps' : ∀ a b → a is-strong-suc-of b → P b → P a
  ps' a b a-is-suc-of-b pb = subst P (suc→+𝟏 (fst a-is-suc-of-b)) (ps b pb)