----------------------------------------------------------------------------------------------------
-- Cantor Normal Forms as subset of unlabeled binary trees
----------------------------------------------------------------------------------------------------

{- We work with the mutual definition of Cantor Normal Forms and its
   ordering, which has been developed in

     Fredrik Nordvall Forsberg, Chuangjie Xu, and Neil Ghani.
     Threee quivalent ordinal notation systems in cubical agda.
     In Proceedings of the 9th ACM SIGPLAN International Conference
     on Certified Programs and Proofs, CPP 2020, page 172–185.
     Association for Computing Machinery, 2020.
-}

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

module CantorNormalForm.Base where

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

open import General-Properties


{- Cantor Normal Forms -}

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


{- Basic properties of CNF -}

<₂' : ∀ {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 : Type ℓ} (x y : A) → Cnf → A
caseCnf x y  𝟎               = x
caseCnf x y (ω^ _ + _ [ _ ]) = y

𝟎≢ω : ∀ {a b} {r : a ≥ left b} → ¬ (𝟎 ≡ ω^ a + b [ r ])
𝟎≢ω e = subst (caseCnf Cnf ⊥) e 𝟎

ω≢𝟎 : ∀ {a b} {r : a ≥ left b} → ¬ (ω^ a + b [ r ] ≡ 𝟎)
ω≢𝟎 e = subst (caseCnf ⊥ Cnf) e 𝟎

≢𝟎→>𝟎 : ∀ a → ¬ (a ≡ 𝟎) → a > 𝟎
≢𝟎→>𝟎 𝟎 f = ⊥-rec (f refl)
≢𝟎→>𝟎 (ω^ _ + _ [ _ ]) f = <₁

𝟎≤ : {a : Cnf} → 𝟎 ≤ a
𝟎≤ {𝟎} = inr (refl)
𝟎≤ {ω^ a + b [ r ]} = inl <₁

≮𝟎 : ∀ {a} → ¬ (a < 𝟎)
≮𝟎 ()

ω^≰𝟎 : ∀ {a b r} → ¬ (ω^ a + b [ r ] ≤ 𝟎)
ω^≰𝟎 (inr e) = 𝟎≢ω e

≤𝟎→≡𝟎 : ∀ {a} → a ≤ 𝟎 → a ≡ 𝟎
≤𝟎→≡𝟎 (inr e) = sym e

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 (<₃ e r)) = inr (sym e)
left-is-≤-monotone (inr e) = inr (cong left e)

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 e = subst (λ x → ¬ _ < x) e <-irrefl

<-trans : ∀ {a b c} → a < b → b < c → a < c
<-trans  <₁      (<₂ _)   = <₁
<-trans  <₁      (<₃ _ _) = <₁
<-trans (<₂ r)   (<₂ s)   = <₂ (<-trans r s)
<-trans (<₂ r)   (<₃ p _) = <₂ (subst (λ x → _ < x) p r)
<-trans (<₃ p _) (<₂ s)   = <₂ (subst (λ x → x < _) (sym p) s)
<-trans (<₃ p r) (<₃ q s) = <₃ (p ∙ q) (<-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 (ω^ b + c [ s ]) (inr e) = <₃ (sym e) (right< b 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)
≤→≯ (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

≤-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

≤-splits : {a b : Cnf} → a ≤ b → (a < b) ⊎ (a ≡ b)
≤-splits (inl a<b) = inl a<b
≤-splits (inr b≡a) = inr (sym b≡a)

{- Convert paths to propositional equality to help Agda's termination checker. -}
import Agda.Builtin.Equality as P

PropEqfromPath : ∀ {ℓ} {A : Set ℓ} {x y : A} → x ≡ y → x P.≡ y
PropEqfromPath {x = x} p = subst (x P.≡_) p P.refl

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
 {---- Pattern match on c, to please Agda's termination checker ----}
 Cnf-is-discrete (ω^ a + 𝟎 [ r ]) (ω^ b + d [ s ]) | yes a≡b | yes 𝟎≡d
     with PropEqfromPath a≡b | PropEqfromPath 𝟎≡d
 Cnf-is-discrete (ω^ a + 𝟎 [ r ]) (ω^ b + d [ s ]) | yes a≡b | yes 𝟎≡d
     | P.refl | P.refl = yes (cong (ω^ a + 𝟎 [_]) (isProp⟨≤⟩ r s))
 Cnf-is-discrete (ω^ a + c@(ω^ _ + _ [ _ ]) [ r ]) (ω^ b + d [ s ]) | yes a≡b | yes c≡d
     with PropEqfromPath a≡b | PropEqfromPath c≡d
 Cnf-is-discrete (ω^ a + c@(ω^ _ + _ [ _ ]) [ r ]) (ω^ b + d [ s ]) | yes a≡b | yes c≡d
     | P.refl | P.refl = yes (cong (ω^ a + c [_]) (isProp⟨≤⟩ r s))
 {---------------- End of the pattern matching on c ----------------}
 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))

 {----- Inlining the proof of "Discrete→isSet Cnf-is-discrete" -----}
 ≡-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
 {---------  Cnf-is-set = Discrete→isSet Cnf-is-discrete  ----------}
 {---------------------- End of the inlining -----------------------}

 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} {c} {d} {r} {s} a≡c b≡d = claim₁ r r' ∙ claim₃ r' s
 where
  r' : c ≥ left b
  r' = subst _ a≡c r
  claim₀ : ∀ r r' → ω^ a + b [ r ] ≡ ω^ a + b [ r' ]
  claim₀ r r' = cong (ω^ a + b [_]) (isProp⟨≤⟩ r r')
  claim₁ : (r : a ≥ left b) (r' : c ≥ left b) → ω^ a + b [ r ] ≡ ω^ c + b [ r' ]
  claim₁ = subst _ a≡c claim₀
  claim₂ : ∀ r' s → ω^ c + d [ r' ] ≡ ω^ c + d [ s ]
  claim₂ r' s = cong (ω^ c + d [_]) (isProp⟨≤⟩ r' s)
  claim₃ : (r' : c ≥ left b) (s : c ≥ left d) → ω^ c + b [ r' ] ≡ ω^ c + d [ s ]
  claim₃ = subst _ (sym b≡d) claim₂

<-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))

<-dec : (a b : Cnf) → Dec (a < b)
<-dec a b with <-tri a b
... | inl a<b = yes a<b
... | inr a≥b = no (≤→≯ a≥b)

≤-dec : (a b : Cnf) → Dec (a ≤ b)
≤-dec a b with <-tri b a
... | inl a>b = no (λ a≤b → ≤→≯ a≤b a>b)
... | inr a≤b = yes a≤b

≤-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

<-extensional : isExtensional _<_
<-extensional a b h with <-tri a b
... | inl      a<b  = ⊥-rec (<-irrefl (snd (h a) a<b))
... | inr (inl a>b) = ⊥-rec (<-irrefl (fst (h b) a>b))
... | inr (inr a≡b) = a≡b

≤-extensional : isExtensional _≤_
≤-extensional a b h = ≤-antisym (fst (h a) ≤-refl) (snd (h b) ≤-refl)

≤₂ : ∀ {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 + c [ r ] ≤ ω^ b + d [ s ] → a ≤ b
≤₂⁻¹ (inl (<₂ a<b))     = inl a<b
≤₂⁻¹ (inl (<₃ a≡b c<d)) = inr (sym a≡b)
≤₂⁻¹ (inr e)            = inr (cong left e)

≤₃ : ∀ {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 c d r s} → a ≤ b → c ≤ d → ω^ a + c [ r ] ≤ ω^ b + d [ s ]
≤₂' (inl a<b) c≤d = inl (<₂ a<b)
≤₂' (inr b≡a) c≤d = ≤₃ (sym b≡a) c≤d

≮→≥ : {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)


{- Exponentiation with base ω -}

ω^⟨_⟩ : 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


{- a is finite iff left a ≡ 𝟎 -}

fin<ω : ∀ a → left a ≡ 𝟎 → a < ω
fin<ω 𝟎 p = <₁
fin<ω (ω^ u + x [ _ ]) u≡𝟎 = <₂ (subst (_< 𝟏) (sym u≡𝟎) <₁)

<ω→fin : ∀ {a} → a < ω → left a ≡ 𝟎
<ω→fin  <₁    = refl
<ω→fin (<₂ r) = <𝟏→≡𝟎 r


{- Embedding natural numbers into CNF -}
mutual

 NtoC : ℕ → Cnf
 NtoC        = 𝟎
 NtoC (suc n) = ω^ 𝟎 + NtoC n [ inr (sym (left-NtoC-is-𝟎 n)) ]

 left-NtoC-is-𝟎 : ∀ n → left (NtoC n) ≡ 𝟎
 left-NtoC-is-𝟎        = refl
 left-NtoC-is-𝟎 (suc n) = refl

left≡𝟎-is-nat : ∀ a → left a ≡ 𝟎 → Σ[ n ∈ ℕ ] a ≡ NtoC n
left≡𝟎-is-nat 𝟎 e =  , 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)