----------------------------------------------------------------------------------------------------
-- Some properties of Brouwer trees
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical  #-}

module BrouwerTree.Properties where

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

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

open import Cubical.Relation.Nullary
open import Cubical.Relation.Binary

open import BrouwerTree.Base


Brw-is-set : isSet Brw
Brw-is-set = trunc

isProp⟨<⟩ :  {x y}  isProp (x < y)
isProp⟨<⟩ = ≤-trunc

isProp⟨≤⟩ :  {x y}  isProp (x  y)
isProp⟨≤⟩ = ≤-trunc

{- ≤ is reflexive -}

≤-refl :  {x}  x  x
≤-refl {x} =
  Brw-ind  x  x  x)
           x  ≤-trunc)
          ≤-zero
          ≤-succ-mono
           {f f↑} fk≤fk  ≤-limiting f {f↑ = f↑} {x = limit f {f↑}} λ k 
             ≤-cocone f {f↑} {k} (fk≤fk k))
          x

≤-refl-≡ :  {x y}  x  y  x  y
≤-refl-≡ {x} {y} x≡y = subst  z  z  y) (sym x≡y) ≤-refl

{- simplified cocone formulation -}

≤-cocone-simple :  f {f↑} {k}  f k  limit f {f↑}
≤-cocone-simple f {f↑} {k} = ≤-cocone f {f↑} {k} ≤-refl

{- Agda's standard notational trick -}

_≤⟨_⟩_ :  {y z}  (x : Brw)  (x  y)  (y  z)  (x  z)
x ≤⟨ x≤y  y≤z = ≤-trans x≤y y≤z

_≤∎ : (x : Brw)  x  x
_ ≤∎ = ≤-refl

infixr  0 _≤⟨_⟩_
infix   1 _≤∎

{- simple lemmas about succ and ≤ -}

<-succ-incr-simple :  {x}  x < succ x
<-succ-incr-simple = ≤-refl

≤-succ-incr-simple :  {x}  x  succ x
≤-succ-incr-simple {x} =
  Brw-ind  x  x  succ x)
           _  ≤-trunc)
          ≤-zero
          ≤-succ-mono
           {f} {f↑} f≤sf  ≤-limiting f {f↑} λ k 
             f k            ≤⟨ f≤sf k 
             succ (f k)     ≤⟨ ≤-succ-mono (≤-cocone-simple f) 
             succ (limit f) ≤∎)
          x

≤-succ-incr :  {x y}  x  y  x  succ y
≤-succ-incr {x} {y} x≤y = ≤-trans x≤y ≤-succ-incr-simple

limit-pointwise-equal :  f {f↑} g {g↑}  ((n : )  f n  g n)  limit f {f↑}  limit g {g↑}
limit-pointwise-equal f g f≡g = bisim f g ((λ k   k , ≤-refl-≡ (f≡g k) ) ,
                                            k   k , ≤-refl-≡ (sym (f≡g k)) ))

{- Some simple properties -}

simulation→≤ :  {f f↑ g g↑}  (∀ k -> Σ[ n   ] f k  g n) -> limit f {f↑}   limit g {g↑}
simulation→≤ {f} {f↑} {g} {g↑} f≤g = ≤-limiting f λ k  ≤-cocone g (snd (f≤g k))

<-trunc :  {x y} -> isProp (x < y)
<-trunc = ≤-trunc

<-in-≤ :  {x y}  x < y  x  y
<-in-≤ {x} x<y = ≤-trans (≤-succ-incr-simple {x}) x<y

<∘≤-in-< :  {x y z}  x < y  y  z  x < z
<∘≤-in-< x<y y≤z = ≤-trans x<y y≤z

≤∘<-in-< :  {x y z}  x  y  y < z  x < z
≤∘<-in-< {x} {y} {z} x≤y y<z = succ x ≤⟨ ≤-succ-mono x≤y  succ y ≤⟨ y<z  z ≤∎

<-trans : BinaryRelation.isTrans _<_
<-trans x y z x<y y<z = ≤-trans x<y (<-in-≤ y<z)

{- Predecessor -}

module predecessor where

  pred : Brw  Brw
  pred zero = zero
  pred (succ x) = x
  pred (limit f {f↑}) = limit f {f↑}
  pred (bisim f {f↑} g {g↑} f∼g i) = bisim f {f↑} g {g↑} f∼g i
  pred (trunc x y p q i j) = trunc (pred x) (pred y) (cong pred p) (cong pred q) i j

  pred-decr-simple :  x  pred x  x
  pred-decr-simple =
    Brw-ind  x  pred x  x)
             _  ≤-trunc)
            ≤-zero
             _  ≤-succ-incr-simple)
            λ _  ≤-refl

  succ-is-inj :  {x y}  succ x  succ y  x  y
  succ-is-inj = cong pred

  pred-≤ : {x y : Brw}  y  x  pred y  pred x
  pred-≤ =
    ≤-ind  {y} {x} y≤x  pred y  pred x)
           _  ≤-trunc)
          ≤-zero
          ≤-trans
           y≤x _  y≤x)
           {y} f {f↑} {k} y≤fk py≤pfk 
             ≤-cocone {pred y} f {f↑} {k} (≤-trans (pred-decr-simple y) y≤fk))
           f {f↑} {x} f≤x pf≤px f≤psx  ≤-limiting f {f↑} {pred x} λ k 
             f k              ≤⟨ f≤psx k 
             pred (f (suc k)) ≤⟨ pf≤px (suc k) 
             pred x           ≤∎)

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

{- Distinguishing the constructors -}

isZero' : Brw  hProp ℓ-zero
isZero' zero = Unit , isPropUnit
isZero' (succ x) =  , isProp⊥
isZero' (limit f) =  , isProp⊥
isZero' (bisim f g x i) =  , isProp⊥
isZero' (trunc x y p q i j) =
  isSet→SquareP {A = λ i j  hProp ℓ-zero}
                 i j  isSetHProp)
                 j  isZero' (p j))
                 j  isZero' (q j))
                refl
                refl
                i j

isZero : Brw  Type
isZero x = typ (isZero' x)

isProp⟨isZero⟩ : {x : Brw}  isProp (isZero x)
isProp⟨isZero⟩ {x} = str (isZero' x)

zero≠succ :  {x}  zero  succ x  
zero≠succ {x} z≡sx = subst isZero z≡sx tt

zero≠lim :  {f f↑}  zero  limit f {f↑}  
zero≠lim {f} {f↑} zero≡⊔f = subst isZero zero≡⊔f tt

isZero-correct :  {x}  isZero x  x  zero
isZero-correct {x} iZ⟨x⟩ =
  Brw-ind  x  isZero x  x  zero)
           x  isPropΠ  _  trunc x zero))
           _  refl)
           _ ())
           _ ())
          x iZ⟨x⟩

isDec⟨isZero⟩ : (x : Brw)  Dec (isZero x)
isDec⟨isZero⟩ = Brw-ind  x  Dec (isZero x))  x  isPropDec (isProp⟨isZero⟩ {x}))
                  (yes tt)
                   _  no λ ())
                   _  no λ ())


decZero : (x : Brw)  Dec (x  zero)
decZero x = mapDec isZero-correct  ¬isZ x≡zero  subst  z  isZero z  ) x≡zero ¬isZ tt)
                   (isDec⟨isZero⟩ x)

isSucc' : Brw  hProp ℓ-zero
isSucc' zero =  , isProp⊥
isSucc' (succ x) = Unit , isPropUnit
isSucc' (limit f) =  , isProp⊥
isSucc' (bisim f g x i) =  , isProp⊥
isSucc' (trunc x y p q i j) =
  isSet→SquareP {A = λ i j  hProp ℓ-zero}
                 i j  isSetHProp)
                 j  isSucc' (p j))
                 j  isSucc' (q j))
                refl
                refl
                i j

isSucc : Brw  Type ℓ-zero
isSucc x = typ (isSucc' x)

succ≠lim :  {x f f↑}  succ x  limit f {f↑}  
succ≠lim sx≡⊔f = subst isSucc sx≡⊔f tt

{- Successors and limits are not smaller or equal to zero. -}

≤-isZero-function :  {x y}  x  y  isZero y  isZero x
≤-isZero-function {x} {y} = ≤-ind  {x} {y} x≤y  isZero y  isZero x)
                                   {x} x≤y  isProp→ (isProp⟨isZero⟩ {x}))
                                   _  tt)
                                   ih₁ ih₂  ih₁  ih₂)
                                   _ _ ())
                                   {x} f {f↑} x≤fk ih ())
                                  λ f {f↑} {y} f≤y ih ih↑ iZ⟨y⟩  ih↑ 0 (ih 1 iZ⟨y⟩)

succ≰zero-aux :  {x y z}  y  z  y  succ x  isZero z  
succ≰zero-aux {x} {.zero} {z} ≤-zero y≡sx iZ⟨z⟩ = zero≠succ y≡sx
succ≰zero-aux {x} {y} {z} (≤-trans {y} {y₁} {z} y≤y₁ y₁≤z) y≡sx iZ⟨z⟩ =
    succ≰zero-aux y≤y₁ y≡sx (≤-isZero-function y₁≤z iZ⟨z⟩)
succ≰zero-aux {x} {.(limit f)} {z} (≤-limiting f x₁) y≡sx iZ⟨z⟩ = succ≠lim (sym y≡sx)
succ≰zero-aux {x} {y} {z} (≤-trunc y≤z y≤z₁ i) y≡sx iZ⟨z⟩ =
    isProp⊥ (succ≰zero-aux y≤z y≡sx iZ⟨z⟩) (succ≰zero-aux y≤z₁ y≡sx iZ⟨z⟩) i

succ≰zero :  {x}  succ x  zero  
succ≰zero {x} sx≤z = succ≰zero-aux sx≤z refl tt

x≮zero :  {x}  x < zero  
x≮zero = succ≰zero

x≤zero→x≡zero :  {x}  x  zero  x  zero
x≤zero→x≡zero x≤zero = isZero-correct (≤-isZero-function x≤zero tt)

lim≰zero :  {f f↑}  limit f {f↑}  zero  
lim≰zero {f} {f↑} ⊔f≤zero = succ≰zero (succ (f 0) ≤⟨ f↑ 0 
                                       f 1        ≤⟨ ≤-cocone-simple f {f↑} 
                                       limit f    ≤⟨ ⊔f≤zero 
                                       zero       ≤∎)

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

zero<lim :  {f f↑}  zero < limit f {f↑}
zero<lim {f} {f↑} = ≤-trans (≤-succ-mono (≤-zero {f 0})) (≤-trans (f↑ 0) (≤-cocone-simple f))

{- Embedding natural numbers into Brouwer trees -}

ι :   Brw
ι zero = zero
ι (suc x) = succ (ι x)

ι-increasing : increasing ι
ι-increasing zero = zero<succ
ι-increasing (suc k) = ≤-succ-mono (ι-increasing k)

ι-pointwise-smaller :   f (f↑ : increasing f)  (k : )  ι k  f k
ι-pointwise-smaller f f↑ zero = ≤-zero
ι-pointwise-smaller f f↑ (suc k) = ≤-trans (≤-succ-mono (ι-pointwise-smaller f f↑ k)) (f↑ k)

ι_<lim :  {f f↑}  (k : )  ι k < limit f {f↑}
ι_<lim {f} {f↑} k = ≤∘<-in-< (ι-pointwise-smaller f f↑ k) (<∘≤-in-< (f↑ k) (≤-cocone-simple f))

zero≠x→zero<x :  x  ¬ (zero  x)  zero < x
zero≠x→zero<x = Brw-ind  x  ¬ (zero  x)  zero < x)  x  isProp→ ≤-trunc)
                   z≢z  ⊥.rec (z≢z refl))
                   _ _  zero<succ)
                   _ _  zero<lim)

one<x→x≢zero :  {x}  one < x  ¬ x  zero
one<x→x≢zero {x} one<x x≡zero = x≮zero (subst  z  one < z) x≡zero one<x)

one<lim :  {f f↑}  one < limit f {f↑}
one<lim {f} {f↑} = ι 1 <lim

limit-skip-first :  f {f↑}  limit f {f↑}  limit (f  suc) {f↑  suc}
limit-skip-first f {f↑} = bisim f (f  suc)
                                ((λ k   k , <-in-≤ (f↑ k) ) , λ k   suc k , ≤-refl )

decZeroOneMany : (x : Brw)  (x  zero)  ((x  one)  (one < x))
decZeroOneMany zero = inl refl
decZeroOneMany (succ x) with decZeroOneMany x
... | inl x≡zero = inr (inl (cong succ x≡zero))
... | inr (inl x≡one) = inr (inr (≤-succ-mono (≤-refl-≡ (sym x≡one))))
... | inr (inr one<x) = inr (inr (≤-succ-incr one<x))
decZeroOneMany (limit f) = inr (inr one<lim)
decZeroOneMany (bisim f {f↑} g {g↑} p i) = inr (inr (isProp→PathP {B = λ i  one < bisim f g p i}
                                                                   i  <-trunc)
                                                                  one<lim one<lim i))
decZeroOneMany (trunc x y p q i j) =
    isSet→SquareP {A = λ i j  (trunc x y p q i j  zero)
                              ((trunc x y p q i j  one)
                              (one < trunc x y p q i j))}
                   i j  isSet⊎ (isProp→isSet (Brw-is-set _ _))
                                    (isSet⊎ (isProp→isSet (Brw-is-set _ _))
                                              (isProp→isSet <-trunc)))
                   j  decZeroOneMany (p j))  j  decZeroOneMany (q j)) refl refl i j