----------------------------------------------------------------------------------------------------
-- 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↑} ≤∎))))))