----------------------------------------------------------------------------------------------------
-- Decidability results for binary joins of Brouwer trees
----------------------------------------------------------------------------------------------------

{-# OPTIONS --cubical #-}

module BrouwerTree.Decidability.Joins where

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

open import Cubical.Data.Empty as 
open import Cubical.Data.Unit
open import Cubical.Data.Sum
open import Cubical.Data.Nat as N using (; zero; suc)
open import Cubical.Data.Nat.Order as N using ()
open import Cubical.Data.Sigma
open import Cubical.Relation.Nullary
  using (¬_; Dec; yes; no; isPropDec; mapDec; Dec→Stable)

open import PropTrunc

open import General-Properties
open import Iff

open import BrouwerTree.Base
open import BrouwerTree.Properties
open import BrouwerTree.Classifiability
open import BrouwerTree.Arithmetic
open import BrouwerTree.Code.Results
open import BrouwerTree.Decidability
open import BrouwerTree.Decidability.Finite


module with-ω where

  _⊔ω : Brw  Brw
  x ⊔ω with decIsFinite x
  ... | yes x-finite = ω
  ... | no x-infinite = x

  is-join :  x  (x ⊔ω) is-join-of x and ω
  is-join x with decIsFinite x
  ... | yes x-finite = (∥-∥rec isProp⟨≤⟩  { (n , ιn=x)  subst (_≤ ω) ιn=x (≤-cocone-simple ι)  }) (fst (isFinite-correct x) x-finite) , ≤-refl) , λ y p q  q
  ... | no x-infinite = (≤-refl , notFinite→ω≤ x x-infinite) , λ y p q  p

module with-finite where

  _⊔_ : Brw    Brw
  x  zero = x
  zero  suc n = ι (suc n)
  succ x  suc n = succ (x  n)
  limit f {f↑}  suc n = limit f {f↑}
  bisim f {f↑} g {g↑} f∼g i  suc n = bisim f {f↑} g {g↑} f∼g i
  trunc x y p q i j  suc n = trunc (x  suc n) (y  suc n)  j  p j  suc n)  j  q j  suc n) i j

  is-join :  x n  (x  n) is-join-of x and (ι n)
  is-join x zero = (≤-refl , ≤-zero) ,  y x≤y _  x≤y)
  is-join zero (suc n) = (≤-zero , ≤-refl) ,  y _ p  p)
  is-join (succ x) (suc n) = ((≤-succ-mono (fst (fst (is-join x n)))) , ≤-succ-mono (snd (fst (is-join x n)))) , succCase
    where
      succCase :  {n x}  (y : Brw)  succ x  y  succ (ι n)  y  succ (x  n)  y
      succCase zero p q = ⊥.rec (succ≰zero p)
      succCase {n} {x} (succ y) p q = ≤-succ-mono (snd (is-join x n) y (≤-succ-mono⁻¹ p) (≤-succ-mono⁻¹ q))
      succCase {n} {x} (limit f {f↑}) p q =
        ∥-∥rec isProp⟨<⟩  { (m , x<fm)  ∥-∥rec isProp⟨<⟩  { (k , ιn<fk) 
           ≤∘<-in-< (snd (is-join x n) (f (N.max m k)) (<-in-≤ (<∘≤-in-< x<fm (increasing-monotone f↑ N.left-≤-max)))
                                                     (<-in-≤ (<∘≤-in-< ιn<fk (increasing-monotone f↑ N.right-≤-max)))) (<-cocone-simple f) })
                                    (below-limit-lemma _ f q)  })
                        (below-limit-lemma x f p)
      succCase {n} {x} (bisim f {f↑} g {g↑} f~g i) p q = isProp→PathP {B = λ i  (p : succ x  bisim f g f~g i)  (q : succ (ι n)  bisim f g f~g i)  succ (x  n)  bisim f g f~g i}  i  isProp→ (isProp→ isProp⟨≤⟩))  p q  ∥-∥rec isProp⟨<⟩  { (m , x<fm)  ∥-∥rec isProp⟨<⟩  { (k , ιn<fk)  ≤∘<-in-< (snd (is-join x n) (f (N.max m k)) (<-in-≤ (<∘≤-in-< x<fm (increasing-monotone f↑ N.left-≤-max))) (<-in-≤ (<∘≤-in-< ιn<fk (increasing-monotone f↑ N.right-≤-max)))) (<-cocone-simple f) }) (below-limit-lemma _ f q)  }) (below-limit-lemma x f p))  p q  ∥-∥rec isProp⟨<⟩  { (m , x<gm)  ∥-∥rec isProp⟨<⟩  { (k , ιn<gk)  ≤∘<-in-< (snd (is-join x n) (g (N.max m k)) (<-in-≤ (<∘≤-in-< x<gm (increasing-monotone g↑ N.left-≤-max))) (<-in-≤ (<∘≤-in-< ιn<gk (increasing-monotone g↑ N.right-≤-max)))) (<-cocone-simple g) }) (below-limit-lemma _ g q)  }) (below-limit-lemma x g p)) i p q
      succCase {n} {z} (trunc x y p q i j) r w = isProp→SquareP' {B = λ i j  (r : succ z  trunc x y p q i j)  (w : succ (ι n)  trunc x y p q i j)  succ (z  n)  trunc x y p q i j}  i j  isProp→ (isProp→ isProp⟨≤⟩))  j r w  succCase x r w)  j r w  succCase y r w)  j r w  succCase (p j) r w)  j r w  succCase (q j) r w) i j r w
  is-join (limit f) (suc n) = (≤-refl , ι n <lim) , λ y p q  p
  is-join (bisim f g x i) (suc n) = isProp→PathP {B = λ i  bisim f g x i is-join-of bisim f g x i and succ (ι n)}  i  isProp⟨is-join-of⟩ isProp⟨≤⟩) ((≤-refl , ι n <lim) , λ y p q  p) ((≤-refl , ι n <lim) , λ y p q  p) i
  is-join (trunc x y p q i j) (suc n) = isProp→SquareP' {B = λ i j  (trunc x y p q i j  suc n) is-join-of trunc x y p q i j and ι (suc n)}  i j  isProp⟨is-join-of⟩ isProp⟨≤⟩)
                                           j  is-join x (suc n))
                                           j  is-join y (suc n))
                                           j  is-join (p j) (suc n))
                                          ((λ j  is-join (q j) (suc n))) i j

  -- additional properties (not needed above)

  zero⊔n≡n :  n  zero  n  ι n
  zero⊔n≡n zero = refl
  zero⊔n≡n (suc n) = refl

  ⊔-mono-right :  x n m  ι n  ι m  (x  n)  (x  m)
  ⊔-mono-right x zero zero _ = ≤-refl
  ⊔-mono-right zero zero (suc m) p = p
  ⊔-mono-right (succ x) zero (suc m) _
    = ≤-succ-mono (⊔-mono-right x zero m ≤-zero)
  ⊔-mono-right (limit f) zero (suc m) p = ≤-refl
  ⊔-mono-right (bisim f g x i) zero (suc m) p = ≤-refl
  ⊔-mono-right (trunc x y p q i j) zero (suc m) r =
    isProp→SquareP' {B = λ i j  (trunc x y p q i j)  trunc (x  suc m) (y  suc m)  j₁  p j₁  suc m)  j₁  q j₁  suc m) i j }
       i j  ≤-trunc)
       j  ⊔-mono-right x zero (suc m) r)
      ((λ j  ⊔-mono-right y zero (suc m) r))
      ((λ j  ⊔-mono-right (p j) zero (suc m) r))
      ((λ j  ⊔-mono-right (q j) zero (suc m) r)) i j
  ⊔-mono-right x (suc n) zero p = ⊥.rec (succ≰zero p)
  ⊔-mono-right zero (suc n) (suc m) p = p
  ⊔-mono-right (succ x) (suc n) (suc m) p
    = ≤-succ-mono (⊔-mono-right x n m (≤-succ-mono⁻¹ p))
  ⊔-mono-right (limit f) (suc n) (suc m) p = ≤-refl
  ⊔-mono-right (bisim f g x i) (suc n) (suc m) p = ≤-refl
  ⊔-mono-right (trunc x y p q i j) (suc n) (suc m) r =
    isProp→SquareP' {B = λ i j  (trunc (x  suc n) (y  suc n)  j₁  p j₁  suc n)  j₁  q j₁  suc n) i j)  trunc (x  suc m) (y  suc m)  j₁  p j₁  suc m)  j₁  q j₁  suc m) i j }
       i j  ≤-trunc)
       j  ⊔-mono-right x (suc n) (suc m) r)
      ((λ j  ⊔-mono-right y (suc n) (suc m) r))
      ((λ j  ⊔-mono-right (p j) (suc n) (suc m) r))
      ((λ j  ⊔-mono-right (q j) (suc n) (suc m) r)) i j


module with-ω+1 where

  ⊔ω+1 : LPO  Brw  Brw
  ⊔ω+1 lpo x with Dec≤→Dec< (LPO→Dec≤ lpo) ω x
  ... | yes ω<x = x
  ... | no ¬ω<x = succ ω

  LPO→⊔ω+1 : (lpo : LPO)  (x : Brw)  (⊔ω+1 lpo x) is-join-of x and (succ ω)
  LPO→⊔ω+1 lpo x with Dec≤→Dec< (LPO→Dec≤ lpo) ω x
  ... | yes ω<x = (≤-refl , ω<x) ,  y p q  p)
  ... | no ¬ω<x = (lemma x ¬ω<x , ≤-refl) , λ y p q  q where
    succ-finite : (x : Brw)  ¬ (ω < succ x)  isFinite x
    succ-finite = Brw-ind  x  ¬ (ω < succ x)  isFinite x)  x  isProp→ (isProp⟨isFinite⟩ x))
                           _  tt)
                           {x} ih p  ih  q  p (<-trans _ _ _ q <-succ-incr-simple)))
                          λ {f} ih p  ⊥.rec (p (≤-succ-mono (ω-smallest f)))

    lemma : (x : Brw)  ¬ (ω < x)  x  succ ω
    lemma = Brw-ind  x  ¬ (ω < x)  x  succ ω)  x  isProp→ isProp⟨≤⟩)
                     _  ≤-zero)
                     {x} ih p  ∥-∥rec isProp⟨≤⟩  { (n , ιn=x)  subst (_< succ ω) ιn=x (≤-succ-mono (≤-cocone-simple ι)) }) (fst (isFinite-correct x) (succ-finite x p)))
                    λ {f} ih p  ≤-limiting f  k  ih k  q  p ((<-trans _ _ _ q (<-cocone-simple f)))))


  ⊔ω+1→Dec≡ω : (⊔ω+1 : Brw  Brw)  ((x : Brw)  (⊔ω+1 x) is-join-of x and (succ ω))  (y : Brw)  Dec (y  ω)
  ⊔ω+1→Dec≡ω ⊔ω+1 is-join = Brw-ind  y  Dec (y  ω))  x  isPropDec (Brw-is-set _ _))
                                    (no zero≠lim)
                                     {x} _  no succ≠lim)
                                    λ {f} {f↑} ih  limitCase f f↑ where
   limitCase :  f f↑  Dec (limit f {f↑}  ω)
   limitCase f f↑ with Brw-has-classification (⊔ω+1 (limit f {f↑})) | is-join ((limit f {f↑}))
   ... | inl is-zero | ((p , _) , _) = ⊥.rec (lim≰zero (≤-trans p (is-zero zero)))
   ... | inr (inl (x , ((x<lf⊔ω+1 , p) , q))) | ((jl , jr) , ju)
     = yes (≤-antisym (≤-limiting f λ k  <-in-≤ (Dec→Stable (mapDec  p  ∥-∥rec isProp⟨≤⟩  { (n , ιn≡fk)  subst (_< ω) ιn≡fk (<-cocone-simple ι) }) (fst (isFinite-correct (f k)) p))
                                                                      p q  <-irreflexive _ (≤∘<-in-< (notFinite→ω≤ (f k) p) q))
                                                                     (decIsFinite (f k)))
                                                            λ ¬fk<ω  succ≠lim (sym lf⊔ω+1≡sx  ≤-antisym (ju (limit f) ≤-refl (<-in-≤ (lf-greatest k (notFinite→ω≤ (f k) λ fin  ∥-∥rec isProp⊥  { (n , ιn≡fk)  ¬fk<ω (subst (_< ω) ιn≡fk (<-cocone-simple ι)) }) (fst (isFinite-correct (f k)) fin))))) jl)))
                      (ω-smallest f))
     where
       lf⊔ω+1≡sx : ⊔ω+1 (limit f {f↑})  succ x
       lf⊔ω+1≡sx = ≤-antisym (p (succ x) ≤-refl) x<lf⊔ω+1
       lf-greatest : (k : )  ω  f k  succ ω < limit f {f↑}
       lf-greatest k p = ≤-cocone f {k = suc (suc (suc k))} (≤-trans (≤-succ-mono (≤-succ-mono p)) (≤∘<-in-< (<-trans _ _ _ (f↑ k) (f↑ (suc k))) (f↑ (suc (suc k)))))

   ... | inr (inr is-lim) | _
     = ∥-∥rec (isPropDec (Brw-is-set _ _))
              { ((g , g↑) , (cone , lim))  no λ lg≡ω  ⊥.rec (succ≠lim {f↑ = g↑}
                                                                          (sym ( ≤-antisym (≤-limiting g cone) (lim (limit g) λ k  ≤-cocone-simple g)  cong ⊔ω+1 lg≡ω  ω⊔ω+1≡ω+1))) }) is-lim
     where
       ω⊔ω+1≡ω+1 : ⊔ω+1 ω  succ ω
       ω⊔ω+1≡ω+1 = ≤-antisym (snd (is-join ω) (succ ω) ≤-succ-incr-simple ≤-refl) (snd (fst (is-join ω)))