----------------------------------------------------------------------------------------------------
-- 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↑  0      = <₁
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≤ω  0      = inl <₁
  NtoC≤ω (suc i) = inl (<₂ <₁)
  ω-min-over-NtoC-lem :  x  (∀ i  NtoC i  x)  ¬ (x < ω)
  ω-min-over-NtoC-lem 𝟎 h <₁ = ω^≰𝟎 (h 1)
  ω-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 1))
  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 1)
    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 0))
  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 0))
  q (ω^ u + v [ _ ]) h with <-tri a u
  ... | inl a<u = inl (<₂ a<u)
  ... | inr (inl a>u) = ⊥-rec (≤→≯ (h 0) (<₂ 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↑ 0) (f≤𝟎 1))))
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)