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

{-# OPTIONS --cubical-compatible #-}

module CantorNormalForm.WithPropositionalEquality.Wellfoundedness where

open import Induction.WellFounded
  renaming (WellFounded to isWellFounded;
            Acc to isAcc)

open import Agda.Builtin.Equality

open import CantorNormalForm.WithPropositionalEquality.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ᡃ refl {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ᡃ refl IH b<a t
    where
     IH : isAcc _<_ d
     IH = goal d (<-trans (right< b d t) (<β‚‚ b<a))
   goal (Ο‰^ b + d [ t ]) (<₃ refl d<y) = Lm[snd-acc] acᡃ refl (ξᢜ 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


wf-ind : βˆ€ {β„“''} {P : Cnf β†’ Set β„“''} β†’
         ((x : Cnf) β†’ ((y : Cnf) β†’ y < x β†’ P y) β†’ P x) β†’ (x : Cnf) β†’ P x
wf-ind = All.wfRec <-is-wellfounded _ _