----------------------------------------------------------------------------------------------------
-- Wellfoundedness of Cantor Normal Forms
----------------------------------------------------------------------------------------------------

{- We recall the wellfoundedness proof of CNF's from

     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.Wellfoundedness where

open import Cubical.Foundations.Prelude
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.Relation.Binary
open BinaryRelation
open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded;
            Acc to isAcc)

open import CantorNormalForm.Base


𝟎IsAcc : isAcc _<_ 𝟎
𝟎IsAcc = acc (λ _ ())

mutual

 Lm[fst-acc] : βˆ€ {a a'} β†’ isAcc _<_ a' β†’ a ≑ a'
   β†’ βˆ€ {b x} β†’ isAcc _<_ b β†’ x < a' β†’ (r : x β‰₯ left b)
   β†’ isAcc _<_ (Ο‰^ x + b [ r ])
 Lm[fst-acc] {a} {a'} (acc ΞΎ) a=a' {b} {x} acᡇ x<a' r = acc goal
   where
    goal : βˆ€ z β†’ z < Ο‰^ x + b [ r ] β†’ isAcc _<_ z
    goal  𝟎 <₁ = 𝟎IsAcc
    goal (Ο‰^ c + d [ s ]) (<β‚‚ c<y) = Lm[fst-acc] (ΞΎ x x<a') refl IH c<y s
     where
      IH : isAcc _<_ d
      IH = goal d (<-trans (right< c d s) (<β‚‚ c<y))
    goal (Ο‰^ c + d [ s ]) (<₃ c=y d<b) = Lm[snd-acc] (ΞΎ x x<a') c=y acᡇ d<b s

 Lm[snd-acc] : βˆ€ {a a'} β†’ isAcc _<_ a' β†’ a ≑ a'
   β†’ βˆ€ {c y} β†’ isAcc _<_ c β†’ y < c β†’ (r : a β‰₯ left y)
   β†’ isAcc _<_ (Ο‰^ a + y [ r ])
 Lm[snd-acc] {a} {a'} acᡃ a=a' {c} {y} (acc ξᢜ) y<c r = acc goal
  where
   goal : βˆ€ z β†’ z < Ο‰^ a + y [ r ] β†’ isAcc _<_ z
   goal 𝟎 <₁ = 𝟎IsAcc
   goal (Ο‰^ b + d [ t ]) (<β‚‚ b<a) = Lm[fst-acc] acᡃ a=a' IH (subst (b <_) a=a' b<a) t
    where
     IH : isAcc _<_ d
     IH = goal d (<-trans (right< b d t) (<β‚‚ b<a))
   goal (Ο‰^ b + d [ t ]) (<₃ b=a d<y) = Lm[snd-acc] acᡃ (b=a βˆ™ a=a') (ξᢜ y y<c) d<y t


<-is-wellfounded : isWellFounded _<_
<-is-wellfounded 𝟎 = 𝟎IsAcc
<-is-wellfounded (Ο‰^ a + b [ r ]) = acc goal
 where
  goal : βˆ€ z β†’ z < Ο‰^ a + b [ r ] β†’ isAcc _<_ z
  goal 𝟎 <₁ = 𝟎IsAcc
  goal (Ο‰^ c + d [ s ]) (<β‚‚ c<a) =
    Lm[fst-acc] (<-is-wellfounded a) refl IH c<a s
   where
    IH : isAcc _<_ d
    IH = goal d (<-trans (right< c d s) (<β‚‚ c<a))
  goal (Ο‰^ c + d [ s ]) (<₃ c=a d<b) =
    Lm[snd-acc] (<-is-wellfounded a) c=a (<-is-wellfounded b) d<b s


open WFI <-is-wellfounded
  renaming (induction to wf-ind)
  public