{-# OPTIONS --cubical-compatible #-}
module CantorNormalForm.WithPropositionalEquality.Base 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 Relation.Nullary
using (Dec ; yes ; no ; ¬_)
open import Data.Nat
using (ℕ ; zero ; suc)
open import PropositionalEquality public
mutual
data Cnf : Set where
𝟎 : Cnf
ω^_+_[_] : (a b : Cnf) → (a ≥ left b) → Cnf
data _<_ : Cnf → Cnf → Set where
<₁ : ∀ {a b r} → 𝟎 < ω^ a + b [ r ]
<₂ : ∀ {a b c d r s} → a < b → ω^ a + c [ r ] < ω^ b + d [ s ]
<₃ : ∀ {a b c d r s} → a ≡ b → c < d → ω^ a + c [ r ] < ω^ b + d [ s ]
left : Cnf → Cnf
left 𝟎 = 𝟎
left (ω^ a + _ [ _ ]) = a
_>_ _≥_ _≤_ : Cnf → Cnf → Set
a > b = b < a
a ≥ b = (a > b) ⊎ (a ≡ b)
a ≤ b = b ≥ a
<₂' : ∀ {a b} → left a < left b → a < b
<₂' {𝟎} {ω^ _ + _ [ x ]} _ = <₁
<₂' {ω^ _ + _ [ _ ]} {ω^ _ + _ [ _ ]} a<b = <₂ a<b
<₂'' : ∀ {a b d s} → left a < b → a < ω^ b + d [ s ]
<₂'' {𝟎} _ = <₁
<₂'' {ω^ _ + _ [ _ ]} a<b = <₂ a<b
right : Cnf → Cnf
right 𝟎 = 𝟎
right (ω^ _ + b [ _ ]) = b
caseCnf : ∀ {ℓ} {A : Set ℓ} (x y : A) → Cnf → A
caseCnf x y 𝟎 = x
caseCnf x y (ω^ _ + _ [ _ ]) = y
𝟎≢ω : ∀ {a b} {r : a ≥ left b} → ¬ (𝟎 ≡ ω^ a + b [ r ])
𝟎≢ω ()
ω≢𝟎 : ∀ {a b} {r : a ≥ left b} → ¬ (ω^ a + b [ r ] ≡ 𝟎)
ω≢𝟎 ()
𝟎≤ : {a : Cnf} → 𝟎 ≤ a
𝟎≤ {𝟎} = inr (refl)
𝟎≤ {ω^ a + b [ r ]} = inl <₁
≮𝟎 : ∀ {a} → ¬ (a < 𝟎)
≮𝟎 ()
ω^≰𝟎 : ∀ {a b r} → ¬ (ω^ a + b [ r ] ≤ 𝟎)
ω^≰𝟎 (inr e) = 𝟎≢ω e
≤𝟎→≡𝟎 : ∀ {a} → a ≤ 𝟎 → a ≡ 𝟎
≤𝟎→≡𝟎 (inr refl) = refl
left-is-≤-monotone : {a b : Cnf} → a ≤ b → left a ≤ left b
left-is-≤-monotone (inl <₁) = 𝟎≤
left-is-≤-monotone (inl (<₂ r)) = inl r
left-is-≤-monotone (inl (<₃ refl r)) = inr refl
left-is-≤-monotone (inr refl) = inr refl
left-is-<-≤-monotone : {a b : Cnf} → a < b → left a ≤ left b
left-is-<-≤-monotone r = left-is-≤-monotone (inl r)
<-irrefl : ∀ {a} → ¬ a < a
<-irrefl (<₂ r) = <-irrefl r
<-irrefl (<₃ a=a r) = <-irrefl r
<-irreflexive : ∀ {a b} → a ≡ b → ¬ a < b
<-irreflexive refl = <-irrefl
<-trans : ∀ {a b c} → a < b → b < c → a < c
<-trans <₁ (<₂ _) = <₁
<-trans <₁ (<₃ _ _) = <₁
<-trans (<₂ r) (<₂ s) = <₂ (<-trans r s)
<-trans (<₂ r) (<₃ refl _) = <₂ r
<-trans (<₃ refl _) (<₂ s) = <₂ s
<-trans (<₃ refl r) (<₃ refl s) = <₃ refl (<-trans r s)
left< : {a b : Cnf} {r : a ≥ left b} → a < ω^ a + b [ r ]
left< {𝟎} = <₁
left< {ω^ a + c [ s ]} = <₂ left<
left≤ : {a : Cnf} → left a ≤ a
left≤ {𝟎} = inr refl
left≤ {ω^ a + b [ r ]} = inl left<
right< : (a b : Cnf) (r : a ≥ left b) → b < ω^ a + b [ r ]
right< a 𝟎 _ = <₁
right< a (ω^ b + c [ s ]) (inl r) = <₂ r
right< a (ω^ _ + c [ s ]) (inr refl) = <₃ refl (right< a c s)
right≤ : (a : Cnf) → right a ≤ a
right≤ 𝟎 = inr refl
right≤ (ω^ a + b [ r ]) = inl (right< a b r)
ω^<-cases : ∀ {a b c d r s}
→ ω^ a + c [ r ] < ω^ b + d [ s ]
→ (a < b) ⊎ ((a ≡ b) × (c < d))
ω^<-cases (<₂ a<b) = inl a<b
ω^<-cases (<₃ a≡b c<d) = inr (a≡b , c<d)
<→≯ : {a b : Cnf} → a < b → ¬ (a > b)
<→≯ (<₂ r) (<₂ s) = <→≯ r s
<→≯ (<₂ r) (<₃ e s) = <-irreflexive (sym e) r
<→≯ (<₃ e r) (<₂ s) = <-irreflexive (sym e) s
<→≯ (<₃ e r) (<₃ _ s) = <→≯ r s
<→≱ : {a b : Cnf} → a < b → ¬ (a ≥ b)
<→≱ a<b (inl a>b) = <→≯ a<b a>b
<→≱ a<b (inr a≡b) = <-irreflexive a≡b a<b
≤→≯ : {a b : Cnf} → a ≤ b → ¬ (a > b)
≤→≯ (inl a<b) = <→≯ a<b
≤→≯ (inr b≡a) = <-irreflexive b≡a
≤∧≮→≡ : {a b : Cnf} → a ≤ b → ¬ (a < b) → a ≡ b
≤∧≮→≡ (inl a<b) a≮b = ⊥-rec (a≮b a<b)
≤∧≮→≡ (inr b≡a) _ = sym b≡a
≤∧≥→≡ : {a b : Cnf} → a ≤ b → a ≥ b → a ≡ b
≤∧≥→≡ a≤b a≥b = ≤∧≮→≡ a≤b (≤→≯ a≥b)
≤-refl : ∀ {a} → a ≤ a
≤-refl = inr refl
≤-trans : {a b c : Cnf} → a ≤ b → b ≤ c → a ≤ c
≤-trans (inl a<b) (inl b<c) = inl (<-trans a<b b<c)
≤-trans (inl a<b) (inr c≡b) = inl (subst (_ <_) (sym c≡b) a<b)
≤-trans (inr b≡a) (inl b<c) = inl (subst (_< _) b≡a b<c)
≤-trans (inr b≡a) (inr c≡b) = inr (c≡b ∙ b≡a)
≤-antisym : {a b : Cnf} → a ≤ b → b ≤ a → a ≡ b
≤-antisym (inl a<b) (inl a>b) = ⊥-rec (<→≯ a<b a>b)
≤-antisym (inl a<b) (inr a≡b) = ⊥-rec (<-irreflexive a≡b a<b)
≤-antisym (inr b≡a) (inl a>b) = ⊥-rec (<-irreflexive b≡a a>b)
≤-antisym (inr b≡a) (inr a≡b) = a≡b
<-in-≤ : {a b : Cnf} → a < b → a ≤ b
<-in-≤ = inl
<∘≤-in-< : {a b c : Cnf} → a < b → b ≤ c → a < c
<∘≤-in-< a<b (inl b<c) = <-trans a<b b<c
<∘≤-in-< a<b (inr c≡b) = subst (_ <_) (sym c≡b) a<b
≤∘<-in-< : {a b c : Cnf} → a ≤ b → b < c → a < c
≤∘<-in-< (inl a<b) b<c = <-trans a<b b<c
≤∘<-in-< (inr b≡a) b<c = subst (_< _) b≡a b<c
mutual
Cnf-is-discrete : Discrete Cnf
Cnf-is-discrete 𝟎 𝟎 = yes refl
Cnf-is-discrete 𝟎 (ω^ b + d [ s ]) = no 𝟎≢ω
Cnf-is-discrete (ω^ a + c [ r ]) 𝟎 = no ω≢𝟎
Cnf-is-discrete (ω^ a + c [ r ]) (ω^ b + d [ s ])
with Cnf-is-discrete a b with Cnf-is-discrete c d
Cnf-is-discrete (ω^ a + 𝟎 [ r ]) (ω^ b + d [ s ]) | yes refl | yes refl =
yes (cong (ω^ a + 𝟎 [_]) (isProp⟨≤⟩ r s))
Cnf-is-discrete (ω^ a + c@(ω^ _ + _ [ _ ]) [ r ]) (ω^ b + d [ s ]) | yes refl | yes refl =
yes (cong (ω^ a + c [_]) (isProp⟨≤⟩ r s))
Cnf-is-discrete (ω^ a + c [ r ]) (ω^ b + d [ s ]) | yes a≡b | no c≢d =
no (λ e → c≢d (cong right e))
Cnf-is-discrete (ω^ a + c [ r ]) (ω^ b + d [ s ]) | no a≢b | v =
no (λ e → a≢b (cong left e))
≡-normalise : ∀ {a b} → a ≡ b → a ≡ b
≡-normalise {a} {b} a≡b with Cnf-is-discrete a b
... | yes p = p
... | no ¬p = ⊥-rec (¬p a≡b)
≡-normalise-constant : ∀ {a b} (p q : a ≡ b) → ≡-normalise p ≡ ≡-normalise q
≡-normalise-constant {a} {b} p q with Cnf-is-discrete a b
... | yes _ = refl
... | no ¬p = ⊥-rec (¬p p)
≡-canonical : ∀ {a b} (p : a ≡ b)
→ (sym (≡-normalise refl)) ∙ (≡-normalise p) ≡ p
≡-canonical = J (λ y p → sym (≡-normalise refl) ∙ (≡-normalise p) ≡ p)
(lCancel (≡-normalise refl))
Cnf-is-set : isSet Cnf
Cnf-is-set _ _ p q = (sym (≡-canonical p)) ∙
cong (sym (≡-normalise refl) ∙_) (≡-normalise-constant p q) ∙
≡-canonical q
isProp⟨<⟩ : ∀ {a b} → isProp (a < b)
isProp⟨<⟩ <₁ <₁ = refl
isProp⟨<⟩ (<₂ r) (<₂ s) = cong <₂ (isProp⟨<⟩ r s)
isProp⟨<⟩ (<₂ r) (<₃ q s) = ⊥-rec (<-irreflexive q r)
isProp⟨<⟩ (<₃ p r) (<₂ s) = ⊥-rec (<-irreflexive p s)
isProp⟨<⟩ (<₃ p r) (<₃ q s) = cong₂ <₃ (Cnf-is-set _ _ p q) (isProp⟨<⟩ r s)
isProp⟨≤⟩ : ∀ {a b} → isProp (a ≤ b)
isProp⟨≤⟩ (inl r) (inl s) = cong inl (isProp⟨<⟩ r s)
isProp⟨≤⟩ (inl r) (inr q) = ⊥-rec (<-irreflexive (sym q) r)
isProp⟨≤⟩ (inr p) (inl s) = ⊥-rec (<-irreflexive (sym p) s)
isProp⟨≤⟩ (inr p) (inr q) = cong inr (Cnf-is-set _ _ p q)
Cnf⁼ : ∀ {a b c d r s} → a ≡ c → b ≡ d → ω^ a + b [ r ] ≡ ω^ c + d [ s ]
Cnf⁼ {a} {b} refl refl = cong (ω^ a + b [_]) (isProp⟨≤⟩ _ _)
<-tri : (a b : Cnf) → (a < b) ⊎ (a ≥ b)
<-tri 𝟎 𝟎 = inr (inr refl)
<-tri 𝟎 (ω^ b + d [ _ ]) = inl <₁
<-tri (ω^ a + c [ _ ]) 𝟎 = inr (inl <₁)
<-tri (ω^ a + c [ _ ]) (ω^ b + d [ _ ]) with <-tri a b with <-tri c d
... | inl a<b | _ = inl (<₂ a<b)
... | inr (inl a>b) | _ = inr (inl (<₂ a>b))
... | inr (inr a≡b) | inl c<d = inl (<₃ a≡b c<d)
... | inr (inr a≡b) | inr (inl c>d) = inr (inl (<₃ (sym a≡b) c>d))
... | inr (inr a≡b) | inr (inr c≡d) = inr (inr (Cnf⁼ a≡b c≡d))
≤-connex : (a b : Cnf) → (a ≤ b) ⊎ (a ≥ b)
≤-connex a b with <-tri a b
... | inl a<b = inl (inl a<b)
... | inr a≥b = inr a≥b
≤₂ : ∀ {a b c r s} → a ≤ b → ω^ a + c [ r ] ≤ ω^ b + c [ s ]
≤₂ (inl a<b) = inl (<₂ a<b)
≤₂ (inr b≡a) = inr (Cnf⁼ b≡a refl)
≤₃ : ∀ {a b c d r s} → a ≡ b → c ≤ d → ω^ a + c [ r ] ≤ ω^ b + d [ s ]
≤₃ a≡b (inl c<d) = inl (<₃ a≡b c<d)
≤₃ a≡b (inr d≡c) = inr (Cnf⁼ (sym a≡b) d≡c)
<₃⁻¹ : ∀ {a b c d r s} → a ≡ b → ω^ a + c [ r ] < ω^ b + d [ s ] → c < d
<₃⁻¹ a≡b (<₂ a<b) = ⊥-rec (<-irreflexive a≡b a<b)
<₃⁻¹ a≡b (<₃ _ c<d) = c<d
≤₃⁻¹ : ∀ {a b c d r s} → a ≡ b → ω^ a + c [ r ] ≤ ω^ b + d [ s ] → c ≤ d
≤₃⁻¹ a≡b (inl r) = inl (<₃⁻¹ a≡b r)
≤₃⁻¹ a≡b (inr e) = inr (cong right e)
≮→≥ : {a b : Cnf} → ¬ (a < b) → a ≥ b
≮→≥ {a} {b} ¬a<b with <-tri a b
... | inl a<b = ⊥-rec (¬a<b a<b)
... | inr a≥b = a≥b
≰→> : {a b : Cnf} → ¬ (a ≤ b) → a > b
≰→> {a} {b} ¬a≤b with <-tri b a
... | inl a>b = a>b
... | inr a≤b = ⊥-rec (¬a≤b a≤b)
ω^⟨_⟩ : Cnf → Cnf
ω^⟨ a ⟩ = ω^ a + 𝟎 [ 𝟎≤ ]
𝟏 : Cnf
𝟏 = ω^⟨ 𝟎 ⟩
ω : Cnf
ω = ω^⟨ 𝟏 ⟩
𝟏≤ω^ : ∀ {a b r} → 𝟏 ≤ ω^ a + b [ r ]
𝟏≤ω^ {𝟎} = ≤₃ refl 𝟎≤
𝟏≤ω^ {ω^ a + c [ s ]} = inl (<₂ <₁)
ω^≮𝟏 : ∀ {a b r} → ¬ (ω^ a + b [ r ] < 𝟏)
ω^≮𝟏 = ≤→≯ 𝟏≤ω^
<𝟏→≡𝟎 : ∀ {a} → a < 𝟏 → a ≡ 𝟎
<𝟏→≡𝟎 <₁ = refl
mutual
NtoC : ℕ → Cnf
NtoC 0 = 𝟎
NtoC (suc n) = ω^ 𝟎 + NtoC n [ inr (sym (left-NtoC-is-𝟎 n)) ]
left-NtoC-is-𝟎 : ∀ n → left (NtoC n) ≡ 𝟎
left-NtoC-is-𝟎 0 = refl
left-NtoC-is-𝟎 (suc n) = refl
left≡𝟎-is-nat : ∀ a → left a ≡ 𝟎 → Σ ℕ (λ n → a ≡ NtoC n)
left≡𝟎-is-nat 𝟎 e = 0 , refl
left≡𝟎-is-nat (ω^ a + b [ r ]) a≡𝟎 = suc n , claim
where
lb≡𝟎 : left b ≡ 𝟎
lb≡𝟎 = ≤𝟎→≡𝟎 (subst (left b ≤_) a≡𝟎 r)
IH : Σ ℕ (λ n → b ≡ NtoC n)
IH = left≡𝟎-is-nat b lb≡𝟎
n : ℕ
n = fst IH
claim : ω^ a + b [ r ] ≡ NtoC (suc n)
claim = Cnf⁼ a≡𝟎 (snd IH)