{-# OPTIONS --cubical-compatible #-}
module CantorNormalForm.WithPropositionalEquality.Classifiability where
open import Data.Sum
renaming (inj₁ to inl; inj₂ to inr)
open import Data.Product
renaming (proj₁ to fst; proj₂ to snd)
open import Data.Empty
renaming (⊥-elim to ⊥-rec)
open import Agda.Builtin.Nat
renaming (Nat to ℕ) using (zero; suc)
open import Agda.Builtin.Equality
open import Relation.Nullary
open import CantorNormalForm.WithPropositionalEquality.Base
open import CantorNormalForm.WithPropositionalEquality.Wellfoundedness
is-zero : Cnf → Set _
is-zero a = (b : Cnf) → a ≤ b
𝟎-is-zero : is-zero 𝟎
𝟎-is-zero _ = 𝟎≤
_is-strong-suc-of_ : Cnf → Cnf → Set _
a is-strong-suc-of b = ((b < a) × (∀ x → b < x → a ≤ x)) × ∀ x → x < a → x ≤ b
is-strong-suc : Cnf → Set _
is-strong-suc a = Σ[ b ∈ Cnf ] a is-strong-suc-of b
mutual
succ : Cnf → Cnf
succ 𝟎 = 𝟏
succ (ω^ a + b [ r ]) = ω^ a + succ b [ ≥left-succ b r ]
≥left-succ : ∀ {a} b → a ≥ left b → a ≥ left (succ b)
≥left-succ 𝟎 r = r
≥left-succ (ω^ _ + _ [ _ ]) r = r
<succ : {a : Cnf} → a < succ a
<succ {𝟎} = <₁
<succ {ω^ _ + _ [ _ ]} = <₃ refl <succ
<→succ≤ : {a b : Cnf} → a < b → succ a ≤ b
<→succ≤ {𝟎} {ω^ 𝟎 + _ [ _ ]} <₁ = ≤₃ refl 𝟎≤
<→succ≤ {𝟎} {ω^ ω^ _ + _ [ _ ] + _ [ _ ]} <₁ = inl (<₂ <₁)
<→succ≤ (<₂ r) = inl (<₂ r)
<→succ≤ (<₃ e r) = ≤₃ e (<→succ≤ r)
<succ→≤ : {a b : Cnf} → a < succ b → a ≤ b
<succ→≤ {.𝟎} {𝟎} <₁ = inr refl
<succ→≤ {.𝟎} {ω^ _ + _ [ _ ]} <₁ = inl <₁
<succ→≤ {ω^ _ + _ [ _ ]} {ω^ _ + _ [ _ ]} (<₂ r) = inl (<₂ r)
<succ→≤ {ω^ _ + _ [ _ ]} {ω^ _ + _ [ _ ]} (<₃ e r) = ≤₃ e (<succ→≤ r)
succ-calc-strong-suc : (a : Cnf) → succ a is-strong-suc-of a
succ-calc-strong-suc a = (<succ , λ _ → <→succ≤) , (λ _ → <succ→≤)
ω^𝟎+-is-succ : (a : Cnf) (r : 𝟎 ≥ left a) → succ a ≡ ω^ 𝟎 + a [ r ]
ω^𝟎+-is-succ 𝟎 r = Cnf⁼ refl refl
ω^𝟎+-is-succ (ω^ 𝟎 + y [ s ]) (inr refl) = Cnf⁼ refl (ω^𝟎+-is-succ y s)
ω^𝟎+-is-strong-suc : (a : Cnf) (r : 𝟎 ≥ left a) → is-strong-suc (ω^ 𝟎 + a [ r ])
ω^𝟎+-is-strong-suc a r = subst is-strong-suc (ω^𝟎+-is-succ a r) (a , succ-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 + succ d [ _ ]
claim₀ = p (ω^ b + succ d [ ≥left-succ d s ]) (<₃ refl <succ)
claim₁ : ω^ a + 𝟎 [ _ ] > ω^ b + succ 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))
_is-sup-of_ : Cnf → (ℕ → Cnf) → Set _
a is-sup-of f = (∀ i → f i ≤ a) × (∀ x → ((∀ i → f i ≤ x) → a ≤ x))
IncrSeq : Set _
IncrSeq = Σ[ f ∈ (ℕ → Cnf) ] ∀ k → f k < f (suc k)
IncrBoundedSeq : Set _
IncrBoundedSeq = Σ[ f ∈ (ℕ → Cnf) ] ((∀ k → f k < f (suc k)) × (Σ[ b ∈ Cnf ] (∀ k → f k < b)))
_is-lim-of_ : Cnf → IncrSeq → Set _
a is-lim-of (f , _) = a is-sup-of f
is-Σlim : Cnf → Set _
is-Σlim a = Σ[ f ∈ IncrSeq ] a is-lim-of f
NtoC↑ : ∀ k → NtoC k < NtoC (suc k)
NtoC↑ 0 = <₁
NtoC↑ (suc i) = <₃ refl (NtoC↑ i)
private
P : Cnf → Set
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
mutual
g : ℕ → Cnf
g 0 = 𝟎
g (suc i) = ω^ x + g i [ ≥left i ]
≥left : ∀ i → x ≥ left (g i)
≥left 0 = 𝟎≤
≥left (suc i) = inr refl
g↑ : ∀ k → g k < g (suc k)
g↑ 0 = <₁
g↑ (suc i) = <₃ refl (g↑ i)
pp : ∀ i → g i ≤ ω^ a + 𝟎 [ r ]
pp 0 = inl <₁
pp (suc i) = inl (<₂ 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
lemma-g : ∀ z → x ≥ left z → Σ ℕ (λ n → z < g (suc n))
lemma-g 𝟎 _ = 0 , <₁
lemma-g (ω^ a' + b' [ r' ]) (inl a'<x) = 0 , <₂ a'<x
lemma-g (ω^ .x + b' [ r' ]) (inr refl) = suc n , claim
where
IH : Σ ℕ (λ n → b' < g (suc n))
IH = lemma-g b' r'
n : ℕ
n = fst IH
claim : ω^ x + b' [ r' ] < g (suc (suc n))
claim = <₃ refl (snd IH)
claim₀ : Σ ℕ (λ n → ω^ u + v [ w ] < g (suc n))
claim₀ = lemma-g _ (inr x≡u)
n : ℕ
n = suc (fst claim₀)
claim₁ : ω^ u + v [ w ] < g n
claim₁ = snd claim₀
claim₂ : g 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
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↑ : ∀ k → g k < g (suc k)
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
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↑ : ∀ k → g k < g (suc k)
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
Cnf-is-Σclassifiable : (a : Cnf) → is-zero a ⊎ (is-strong-suc a ⊎ is-Σlim 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
transfinite-rec : ∀ {ℓ} {A : Set ℓ}
→ A
→ (A → A)
→ ((ℕ → A) → A)
→ Cnf → A
transfinite-rec {ℓ} {A} a s f = wf-ind step
where
step : ∀ x → (∀ y → y < x → A) → A
step x h with Cnf-is-Σclassifiable x
... | inl x-is-zero = a
... | inr (inl (y , x-is-suc-y)) = s (h y (fst (fst x-is-suc-y)))
... | inr (inr ((g , g↑) , q)) = f (λ n → h (g n) (g<x n))
where
g<x : ∀ i → g i < x
g<x i = <∘≤-in-< (g↑ i) (fst q (suc i))