----------------------------------------------------------------------------------------------------
-- Some results of using the Code family of ≤ on Brouwer trees
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

module BrouwerTree.Code.Results where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function

open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.Empty as 

open import Cubical.Relation.Nullary

open import Cubical.Induction.WellFounded
  renaming (WellFounded to isWellFounded)

open import Cubical.HITs.PropositionalTruncation.Properties
  renaming (rec to ∥-∥rec)

open import BrouwerTree.Base
open import BrouwerTree.Properties
open import BrouwerTree.Code

open import Iff
open import General-Properties


{- Inequality between limits is equivalent to weak simulation -}

lim≤lim→weakly-bisimilar :  f {f↑} g {g↑}  (limit f {f↑}  limit g {g↑})  f  g
lim≤lim→weakly-bisimilar f {f↑} g {g↑} ⊔f≤⊔g = λ k 
  ∥-∥rec {A = Σ[ n   ] Code (f k) (g n)}
         {P =   λ n  f k  g n}
         propTruncIsProp
          {(n , c-fk≤gn)   (n , Code→≤ c-fk≤gn) })
         (≤→Code ⊔f≤⊔g k)

weakly-bisimilar→lim≤lim :  f {f↑} g {g↑}  f  g  (limit f {f↑}  limit g {g↑})
weakly-bisimilar→lim≤lim f {f↑} g {g↑} f≤g =
    ≤-limiting f  k  ∥-∥rec ≤-trunc  (n , fk≤gn)  ≤-cocone g fk≤gn) (f≤g k))

≤-succ-mono⁻¹ :  {x y}  succ y  succ x  y  x
≤-succ-mono⁻¹ {x} {y} sy≤sx = Code→≤ (≤→Code sy≤sx)

<-succ-mono :  {x y}  y < x  succ y < succ x
<-succ-mono = ≤-succ-mono

<-succ-mono⁻¹ :  {x y}  succ y < succ x  y < x
<-succ-mono⁻¹ = ≤-succ-mono⁻¹

<-cocone-simple :  f {f↑} {k}  f k < limit f {f↑}
<-cocone-simple f {f↑} {k} = <∘≤-in-< (f↑ k) (≤-cocone-simple f {f↑} {suc k})

-- If a limit is below `succ x`, then it is already below `x`
lim≤sx→lim≤x :  f x {f↑}  limit f {f↑}  succ x  limit f {f↑}  x
lim≤sx→lim≤x f x {f↑} ⊔f≤sx =
    ≤-limiting f {f↑}  k  ≤-succ-mono⁻¹ {x} {f k}
                                           (succ (f k) ≤⟨ f↑ k 
                                            f (suc k)  ≤⟨ ≤-cocone-simple f 
                                            limit f    ≤⟨ ⊔f≤sx 
                                            succ x     ≤∎))

-- similarly for being strictly below
lim<sx→lim≤x :  f x {f↑}  limit f {f↑} < succ x  limit f {f↑}  x
lim<sx→lim≤x f x {f↑} ⊔f<sx = ≤-succ-mono⁻¹ (⊔f<sx)

-- If something is strictly below the limit of f, then it is strictly
-- below some f n. This corresponds to the succ-limit case.
below-limit-lemma :  x f {f↑}  x < limit f {f↑}    λ n  x < f n
below-limit-lemma x f {f↑} x<⊔f =
  ∥-∥rec {A = Σ[ n   ] Code (succ x) (f n)}
         {P =    n  x < f n)}
         propTruncIsProp
          {(n , c-sx≤fn)   n , Code→≤ c-sx≤fn })
         (≤→Code {succ x} {limit f} x<⊔f )

{- Wellfoundedness -}

smaller-accessible : (x : Brw)  Acc _<_ x   y  y  x  Acc _<_ y
smaller-accessible x is-acc⟨x⟩ y y≤x = acc  y' y'<y  access is-acc⟨x⟩ y' (<∘≤-in-< y'<y y≤x))

<-is-wellfounded : isWellFounded _<_
<-is-wellfounded =
  Brw-ind  x  Acc _<_ x)
           x  isPropAcc x)
          (acc  y y<zero  ⊥.rec (succ≰zero y<zero)))
           {x} x-acc  acc  y y<sx  smaller-accessible x x-acc y (≤-succ-mono⁻¹ y<sx)))
           {f} {f↑} f-acc  acc  y y<⊔f 
             ∥-∥rec {A = Σ[ n   ] y < f n}
                    {P = Acc _<_ y}
                    (isPropAcc y)
                     {(n , y<fn)  smaller-accessible (f n) (f-acc n) y (<-in-≤ y<fn)})
                    (below-limit-lemma y f {f↑} y<⊔f)))

<-irreflexive :  x  ¬ x < x
<-irreflexive = wellfounded→irreflexive <-is-wellfounded

{- Antisymmetry -}

antisym :  {x y} -> x  y -> y  x -> x  y
antisym {x} {y} =
  Brw-ind  x   y  x  y -> y  x -> x  y)
           x  isPropΠ  y  isProp→ (isProp→ (isSetBrw _ _))))
          (Brw-ind  y  zero  y -> y  zero -> zero  y)
                    y  isProp→ (isProp→ (isSetBrw _ _)))
           _ _  refl)
           _ x≤y y≤x  ⊥.rec (succ≰zero y≤x))
           _ x≤y y≤x  ⊥.rec (lim≰zero y≤x)))
           {x} ih 
             Brw-ind  y  succ x  y -> y  succ x -> succ x  y)
                      y  isProp→ (isProp→ (isSetBrw _ _)))
                      x≤y y≤x  ⊥.rec (succ≰zero x≤y))
                      {y} _ sx≤sy sy≤sx 
                        cong succ (ih y (≤-succ-mono⁻¹ sx≤sy) (≤-succ-mono⁻¹ sy≤sx)))
                      {g} {g↑} _ x≤y y≤x 
                        ⊥.rec (<-irreflexive _ (≤-trans x≤y (lim≤sx→lim≤x g x {g↑} y≤x)))))
           {f} {f↑} _ 
             Brw-ind  y  limit f {f↑}  y -> y  limit f {f↑} -> limit f {f↑}  y)
                      y  isProp→ (isProp→ (isSetBrw _ _)))
                      x≤y y≤x  ⊥.rec (lim≰zero x≤y))
                      {y} _ x≤y y≤x 
                        ⊥.rec (<-irreflexive _ (≤-trans y≤x (lim≤sx→lim≤x f y {f↑} x≤y))))
                      {g} {g↑} _ lf≤lg lg≤lf 
                        bisim f {f↑} g {g↑} (lim≤lim→weakly-bisimilar f g lf≤lg ,
                                             lim≤lim→weakly-bisimilar g f lg≤lf)))
          x y

{- Extensionality -}

extensional : (a b : Brw)  (∀ c  (c < a)  (c < b))  a  b
extensional =
  Brw-ind  a  (b : Brw)  (∀ c  (c < a)  (c < b))  a  b)
           a  isPropΠ  b  isProp→ (isSetBrw a b)))
          (Brw-ind  b  (∀ c  (c < zero)  (c < b))  zero  b)
                    b  isProp→ (isSetBrw _ _))
                    _  refl)
                    {b} _ ext  ⊥.rec (<-irreflexive _ (snd (ext zero) zero<succ)))
                    {f} {f↑} _ ext  ⊥.rec (<-irreflexive _ (snd (ext zero) zero<lim))))
           {a} ih 
             Brw-ind  b  (∀ c  (c < succ a)  (c < b))  succ a  b)
                      b  isProp→ (isSetBrw _ _))
                      ext  ⊥.rec (<-irreflexive _ (fst (ext zero) zero<succ)))
                      {b} _ ext 
                        cong succ (ih b  c   c<a  <-succ-mono⁻¹ (fst (ext (succ c))
                                                                      (<-succ-mono c<a))) ,
                                                c<b  <-succ-mono⁻¹ (snd (ext (succ c))
                                                                      (<-succ-mono c<b))))))
                      {f} {f↑} _ ext 
                        let lf≤a = ≤-limiting f {f↑} {a}  k  ≤-succ-mono⁻¹ (snd (ext (f k))
                                                                              (<-cocone-simple f)))
                        in ⊥.rec (<-irreflexive _ (fst (ext (limit f {f↑}))
                                                (≤∘<-in-< lf≤a <-succ-incr-simple)))))
           {f} {f↑} ih 
             Brw-ind  b  (∀ c  (c < limit f {f↑})  (c < b))  limit f {f↑}  b)
                      b  isProp→ (isSetBrw _ _))
                      ext  ⊥.rec (<-irreflexive _ (fst (ext zero) zero<lim)))
                      {b} _ ext 
                        let lf≤b = ≤-limiting f {f↑} {b}  k  ≤-succ-mono⁻¹ (fst (ext (f k))
                                                                              (<-cocone-simple f)))
                        in ⊥.rec (<-irreflexive _ (snd (ext (limit f {f↑}))
                                                (≤∘<-in-< lf≤b <-succ-incr-simple))))
                      {g} {g↑} ih' ext 
                        antisym {limit f} {limit g}
                                (≤-limiting f {f↑} {limit g}
                                             k  <-in-≤ (fst (ext (f k))
                                                          (succ (f k)   ≤⟨ f↑ k 
                                                           f (suc k)    ≤⟨ ≤-cocone-simple f 
                                                           limit f {f↑} ≤∎))))
                                (≤-limiting g {g↑} {limit f}
                                             k  <-in-≤ (snd (ext (g k))
                                                          (succ (g k)   ≤⟨ g↑ k 
                                                           g (suc k)    ≤⟨ ≤-cocone-simple g 
                                                           limit g {g↑} ≤∎))))))