------------------------------------------------------------------------
-- Upper bounds of colists containing natural numbers
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Upper-bounds where

open import Colist
open import Conat hiding (pred) renaming (_+_ to _⊕_; _∸_ to _⊖_)
open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Omniscience
open import Prelude

open import Equality.Decision-procedures equality-with-J
open import Function-universe equality-with-J as F hiding (id; _∘_)
open import Nat equality-with-J as Nat using (_≤_; _<_; pred)

------------------------------------------------------------------------
-- Upper bounds

-- [ ∞ ] ms ⊑ n means that n is an upper bound of every number in ms.

infix  [_]_⊑_ [_]_⊑′_

[_]_⊑_ : Size → Colist ℕ ∞ → Conat ∞ → Set
[ i ] ms ⊑ n = □ i (λ m → [ ∞ ] ⌜ m ⌝ ≤ n) ms

[_]_⊑′_ : Size → Colist ℕ ∞ → Conat ∞ → Set
[ i ] ms ⊑′ n = □′ i (λ m → [ ∞ ] ⌜ m ⌝ ≤ n) ms

-- The conatural number infinity is always an upper bound.

infix  _⊑infinity

_⊑infinity : ∀ {i} ns → [ i ] ns ⊑ infinity
_⊑infinity = □-replicate (_≤infinity ∘ ⌜_⌝)

-- A form of transitivity.

transitive-⊑≤ :
  ∀ {i ms n o} → [ i ] ms ⊑ n → [ ∞ ] n ≤ o → [ i ] ms ⊑ o
transitive-⊑≤ p q = □-map (flip transitive-≤ q) p

-- Another form of transitivity.

transitive-◇≤⊑ :
  ∀ {m ns o i} → ◇ i (m ≤_) ns → [ i ] ns ⊑ o → [ i ] ⌜ m ⌝ ≤ o
transitive-◇≤⊑ {m} {ns} {o} {i} = curry (
  ◇ i (m ≤_) ns × [ i ] ns ⊑ o       ↝⟨ Σ-map id swap ∘ uncurry □◇-witness ∘ swap ⟩
  (∃ λ n → m ≤ n × [ i ] ⌜ n ⌝ ≤ o)  ↝⟨ (λ { (_ , m≤n , n≤o) → transitive-≤ (⌜⌝-mono m≤n) n≤o }) ⟩□
  [ i ] ⌜ m ⌝ ≤ o                    □)

-- If m is an upper bound of ms, and no natural number is an upper
-- bound, then m is bisimilar to infinity.

no-finite→infinite :
  ∀ {m ms} →
  (∀ n → ¬ [ ∞ ] ms ⊑ ⌜ n ⌝) →
  [ ∞ ] ms ⊑ m →
  Conat.[ ∞ ] m ∼ infinity
no-finite→infinite {m} {ms} no-finite =
  [ ∞ ] ms ⊑ m               ↝⟨ (λ ms⊑n → uncurry λ n →

      Conat.[ ∞ ] m ∼ ⌜ n ⌝        ↝⟨ ∼→≤ ⟩
      [ ∞ ] m ≤ ⌜ n ⌝              ↝⟨ transitive-⊑≤ ms⊑n ⟩
      [ ∞ ] ms ⊑ ⌜ n ⌝             ↝⟨ no-finite n ⟩□
      ⊥                            □) ⟩

  Infinite m                 ↝⟨ Infinite→∼infinity ⟩□
  Conat.[ ∞ ] m ∼ infinity   □

-- No natural number is an upper bound of nats.

nats⋢ : ∀ n → ¬ [ ∞ ] nats ⊑ ⌜ n ⌝
nats⋢ zero =
  [ ∞ ] nats ⊑ ⌜  ⌝         ↝⟨ □-head ∘ □-tail ⟩
  Conat.[ ∞ ] ⌜  ⌝ ≤ ⌜  ⌝  ↝⟨ ≮0 ⟩□
  ⊥                          □
nats⋢ (suc n) =
  [ ∞ ] nats ⊑ ⌜ suc n ⌝          ↝⟨ □-tail ⟩
  [ ∞ ] map suc nats ⊑ ⌜ suc n ⌝  ↝⟨ □-map′ (⌜⌝-mono ∘ Nat.suc≤suc⁻¹ ∘ ⌜⌝-mono⁻¹) ⟩
  [ ∞ ] map id nats ⊑ ⌜ id n ⌝    ↝⟨ □-∼ (map-id _) ⟩
  [ ∞ ] nats ⊑ ⌜ n ⌝              ↝⟨ nats⋢ n ⟩□
  ⊥                               □

-- The number ⌜ n ⌝ is an upper bound of replicate m n.

replicate⊑ : ∀ {i} m {n} → [ i ] replicate m n ⊑ ⌜ n ⌝
replicate⊑ {i} zero    {n} = []
replicate⊑ {i} (suc m) {n} =                                      $⟨ (λ { _ refl → reflexive-≤ _ }) ⟩
  (∀ o → o ≡ n → [ ∞ ] ⌜ o ⌝ ≤ ⌜ n ⌝)                             ↝⟨ (λ hyp _ → hyp _ ∘ _⇔_.to ◇-replicate-suc⇔) ⟩
  (∀ o → ◇ i (o ≡_) (replicate (suc m) n) → [ ∞ ] ⌜ o ⌝ ≤ ⌜ n ⌝)  ↔⟨⟩
  (∀ o → [ i ] o ∈ replicate (suc m) n → [ ∞ ] ⌜ o ⌝ ≤ ⌜ n ⌝)     ↝⟨ _⇔_.from □⇔∈→ ⟩
  □ i (λ o → [ ∞ ] ⌜ o ⌝ ≤ ⌜ n ⌝) (replicate (suc m) n)           ↝⟨ id ⟩□
  [ i ] replicate (suc m) n ⊑ ⌜ n ⌝                               □

------------------------------------------------------------------------
-- Least upper bounds

-- The least upper bound of a colist of natural numbers.

LUB : Colist ℕ ∞ → Conat ∞ → Set
LUB ns n =
  [ ∞ ] ns ⊑ n
    ×
  (∀ n′ → [ ∞ ] ns ⊑ n′ → [ ∞ ] n ≤ n′)

-- Least upper bounds are unique.

lub-unique :
  ∀ {ns n₁ n₂ i} →
  LUB ns n₁ → LUB ns n₂ → Conat.[ i ] n₁ ∼ n₂
lub-unique (lub₁₁ , lub₁₂) (lub₂₁ , lub₂₂) =
  antisymmetric-≤ (lub₁₂ _ lub₂₁) (lub₂₂ _ lub₁₁)

-- LUB respects bisimilarity.

LUB-∼ :
  ∀ {ms ns m n} →
  Colist.[ ∞ ] ms ∼ ns → Conat.[ ∞ ] m ∼ n →
  LUB ms m → LUB ns n
LUB-∼ {ms} {ns} {m} {n} p q = Σ-map
  ([ ∞ ] ms ⊑ m  ↝⟨ □-∼ p ⟩
   [ ∞ ] ns ⊑ m  ↝⟨ □-map (flip transitive-≤ (∼→≤ q)) ⟩□
   [ ∞ ] ns ⊑ n  □)
  (λ hyp n′ →
     [ ∞ ] ns ⊑ n′  ↝⟨ □-∼ (Colist.symmetric-∼ p) ⟩
     [ ∞ ] ms ⊑ n′  ↝⟨ hyp n′ ⟩
     [ ∞ ] m ≤ n′   ↝⟨ transitive-≤ (∼→≤ (Conat.symmetric-∼ q)) ⟩□
     [ ∞ ] n ≤ n′   □)

-- The least upper bound of the empty colist is 0.

lub-[] : LUB [] ⌜  ⌝
lub-[] = [] , λ _ _ → zero

-- Some lemmas that can be used to establish the least upper bound of
-- a non-empty colist.

lub-∷ˡ :
  ∀ {m ms n} →
  [ ∞ ] n ≤ ⌜ m ⌝ →
  LUB (ms .force) n →
  LUB (m ∷ ms) ⌜ m ⌝
lub-∷ˡ {m} {ms} {n} n≤m = Σ-map
  ([ ∞ ] ms .force ⊑ n      ↝⟨ (λ hyp → reflexive-≤ _ ∷ λ { .force → □-map (flip transitive-≤ n≤m) hyp }) ⟩□
   [ ∞ ] m ∷ ms    ⊑ ⌜ m ⌝  □)
  ((∀ n′ → [ ∞ ] ms .force ⊑ n′ → [ ∞ ] n     ≤ n′)  ↝⟨ (λ _ _ → □-head) ⟩□
   (∀ n′ → [ ∞ ] m ∷ ms    ⊑ n′ → [ ∞ ] ⌜ m ⌝ ≤ n′)  □)

lub-∷ʳ :
  ∀ {m ms n} →
  [ ∞ ] ⌜ m ⌝ ≤ n →
  LUB (ms .force) n →
  LUB (m ∷ ms) n
lub-∷ʳ {m} {ms} {n} m≤n = Σ-map
  ([ ∞ ] ms .force ⊑ n  ↝⟨ (λ hyp → m≤n ∷ λ { .force → hyp }) ⟩□
   [ ∞ ] m ∷ ms    ⊑ n  □)
  ((∀ n′ → [ ∞ ] ms .force ⊑ n′ → [ ∞ ] n ≤ n′)  ↝⟨ (λ hyp n′ → hyp n′ ∘ □-tail) ⟩□
   (∀ n′ → [ ∞ ] m ∷ ms    ⊑ n′ → [ ∞ ] n ≤ n′)  □)

-- If m ∷ ms has a least upper bound, then cycle m ms has the same
-- least upper bound.

lub-cycle :
  ∀ {m ms n} →
  LUB (m ∷ ms) n →
  LUB (cycle m ms) n
lub-cycle {m} {ms} {n} = Σ-map
  ([ ∞ ] m ∷ ms     ⊑ n  ↝⟨ _⇔_.from □-cycle⇔ ⟩□
   [ ∞ ] cycle m ms ⊑ n  □)
  ((∀ n′ → [ ∞ ] m ∷ ms     ⊑ n′ → [ ∞ ] n ≤ n′)  ↝⟨ (∀-cong _ λ _ → →-cong-→ (_⇔_.to □-cycle⇔) id) ⟩□
   (∀ n′ → [ ∞ ] cycle m ms ⊑ n′ → [ ∞ ] n ≤ n′)  □)

-- The least upper bound of nats is infinity.

lub-nats-infinity : LUB nats Conat.infinity
lub-nats-infinity =
    (nats ⊑infinity)
  , λ n →
      [ ∞ ] nats ⊑ n                                             ↝⟨ flip no-finite→infinite ⟩
      ((∀ n → ¬ [ ∞ ] nats ⊑ ⌜ n ⌝) → Conat.[ ∞ ] n ∼ infinity)  ↝⟨ _$ nats⋢ ⟩
      Conat.[ ∞ ] n ∼ infinity                                   ↝⟨ Conat.symmetric-∼ ⟩
      Conat.[ ∞ ] infinity ∼ n                                   ↝⟨ ∼→≤ ⟩□
      [ ∞ ] infinity ≤ n                                         □

-- If WLPO holds, then the least upper bound of a colist of natural
-- numbers can be determined.
--
-- (In fact, WLPO is logically equivalent to the codomain of this
-- lemma, see Unbounded-space.wlpo⇔lub.)
--
-- I received help with this proof from Andreas Abel and Ulf Norell: I
-- had presented a proof that used LPO. Andreas Abel came up with the
-- idea for the following, less complicated proof, and Ulf Norell
-- suggested that one could get away with WLPO instead of LPO.

wlpo→lub : WLPO → (∀ ms → ∃ λ n → LUB ms n)
wlpo→lub wlpo = λ ms → lub ms , □ˢ∞→□∞ (upper-bound ms) , least ms
  where
  -- The boolean >0 ms n is true if the n-th number (counting from
  -- zero) of ms is positive.

  >0 : Colist ℕ ∞ → ℕ → Bool
  >0 []           _       = false
  >0 (m     ∷ ms) (suc n) = >0 (ms .force) n
  >0 (zero  ∷ ms) zero    = false
  >0 (suc m ∷ ms) zero    = true

  -- The number lub ms is the least upper bound of ms.

  lub : ∀ {i} → Colist ℕ ∞ → Conat i
  lub ms with wlpo (>0 ms)
  ... | inj₁ _ = zero
  ... | inj₂ _ = suc λ { .force → lub (map pred ms) }

  -- Zero is an upper bound of ms iff >0 ms is universally false.

  ⊑0⇔≡false : ∀ ms → [ ∞ ] ms ⊑ zero ⇔ (∀ n → >0 ms n ≡ false)
  ⊑0⇔≡false = λ ms → record { to = to ms; from = from ms }
    where
    to : ∀ ms → [ ∞ ] ms ⊑ zero → (∀ n → >0 ms n ≡ false)
    to _            []         _       = refl
    to (zero  ∷ ms) _          zero    = refl
    to (suc _ ∷ _)  (() ∷ _)   _
    to (m     ∷ ms) (_ ∷ ms⊑0) (suc n) = to (ms .force) (ms⊑0 .force) n

    from : ∀ {i} ms → (∀ n → >0 ms n ≡ false) → [ i ] ms ⊑ zero
    from []           _      = []
    from (suc m ∷ ms) ≡false = ⊥-elim (Bool.true≢false (≡false zero))
    from (zero  ∷ ms) ≡false =
      zero ∷ λ { .force → from (ms .force) (≡false ∘ suc) }

  -- If n .force is an upper bound of map pred ms, then suc n is an
  -- upper bound of ms. Note that the lemma is size-preserving and
  -- takes □ˢ′ to □ˢ.

  pred-lemma₁ :
    ∀ {i n} ms →
    □ˢ′ i (λ i m → [ i ] ⌜ m ⌝ ≤ n .force) (map pred ms) →
    □ˢ i (λ i m → [ i ] ⌜ m ⌝ ≤ suc n) ms
  pred-lemma₁ []       hyp = []
  pred-lemma₁ (m ∷ ms) hyp =
    helper m hyp
      ∷ λ { .force →
    pred-lemma₁ (ms .force) λ { .force → □ˢ-tail (hyp .force) }}
    where
    helper :
      ∀ {i n} m →
      □ˢ′ i (λ i m → [ i ] ⌜ m ⌝ ≤ n .force) (map pred (m ∷ ms)) →
      [ i ] ⌜ m ⌝ ≤ suc n
    helper zero    hyp = zero
    helper (suc m) hyp = suc λ { .force → □ˢ-head (hyp .force) }

  -- If suc n is an upper bound of ms, then n .force is an upper bound
  -- of map pred ms.

  pred-lemma₂ :
    ∀ {n ms i} →
    [ i ] ms ⊑ suc n →
    [ i ] map pred ms ⊑ n .force
  pred-lemma₂     []                         = []
  pred-lemma₂ {n} (_∷_ {x = m} m≤1+n ms⊑1+n) =
    (⌜ pred m ⌝        ∼⟨ ⌜⌝-pred m ⟩≤
     Conat.pred ⌜ m ⌝  ≤⟨ pred-mono m≤1+n ⟩∎
     n .force          ∎≤)
      ∷ λ { .force →
    pred-lemma₂ (ms⊑1+n .force) }

  -- The number lub ms is an upper bound of ms.

  upper-bound : ∀ {i} ms → □ˢ i (λ i m → [ i ] ⌜ m ⌝ ≤ lub ms) ms
  upper-bound {i} ms with wlpo (>0 ms)
  ... | inj₂ _ =
    pred-lemma₁ _ (λ { .force → upper-bound (map pred ms) })

  ... | inj₁ ≡false =                     $⟨ ≡false ⟩
    (∀ n → >0 ms n ≡ false)               ↝⟨ _⇔_.from (⊑0⇔≡false ms) ⟩
    [ ∞ ] ms ⊑ zero                       ↝⟨ id ⟩
    [ i ] ms ⊑ zero                       ↝⟨ _⇔_.from □ˢ⇔□ ⟩
    □ˢ i (λ _ m → [ ∞ ] ⌜ m ⌝ ≤ zero) ms  ↝⟨ id ⟩□
    □ˢ i (λ i m → [ i ] ⌜ m ⌝ ≤ zero) ms  □

  -- The number lub ms is less than or equal to every number that is
  -- an upper bound of ms.

  least :
    ∀ {i} ms ub →
    [ ∞ ] ms ⊑ ub →
    [ i ] lub ms ≤ ub
  least ms ub ms⊑ub with wlpo (>0 ms)
  least ms ub ms⊑ub | inj₁ _ = zero

  least ms (suc ub) ms⊑1+ub | inj₂ _ =
    suc λ { .force →
      least (map pred ms) (ub .force) (pred-lemma₂ ms⊑1+ub) }

  least ms zero ms⊑0 | inj₂ ¬≡false =
                             $⟨ ms⊑0 ⟩
    [ ∞ ] ms ⊑ zero          ↝⟨ _⇔_.to (⊑0⇔≡false _) ⟩
    (∀ n → >0 ms n ≡ false)  ↝⟨ ¬≡false ⟩
    ⊥                        ↝⟨ ⊥-elim ⟩□
    _                        □

------------------------------------------------------------------------
-- A relation that can be used to relate the least upper bounds of two
-- colists

-- [ ∞ ] ms ≲ ns means that every upper bound of ns is also an upper
-- bound of ms.

infix  [_]_≲_ [_]_≲′_

[_]_≲_ : Size → Colist ℕ ∞ → Colist ℕ ∞ → Set
[ i ] ms ≲ ns = ∀ {n} → [ ∞ ] ns ⊑ n → [ i ] ms ⊑ n

[_]_≲′_ : Size → Colist ℕ ∞ → Colist ℕ ∞ → Set
[ i ] ms ≲′ ns = ∀ {n} → [ ∞ ] ns ⊑ n → [ i ] ms ⊑′ n

-- Bounded m ns means that m is smaller than or equal to some element
-- in ns, or equal to zero.

Bounded : ℕ → Colist ℕ ∞ → Set
Bounded m ns = ◇ ∞ (m ≤_) ns ⊎ m ≡ zero

-- If Bounded m ns holds, then m is less than or equal to every upper
-- bound of ns.

bounded-lemma :
  ∀ {m ns n} →
  Bounded m ns → [ ∞ ] ns ⊑ n → [ ∞ ] ⌜ m ⌝ ≤ n
bounded-lemma (inj₁ ◇m≤ns) = transitive-◇≤⊑ ◇m≤ns
bounded-lemma (inj₂ refl)  = const zero

-- The empty colist is bounded by any other.

[]≲ : ∀ {ns i} → [ i ] [] ≲ ns
[]≲ = λ _ → []

-- Some derived cons-like operations.

consʳ-≲ :
  ∀ {ms ns n i} →
  [ i ] ms ≲ ns .force →
  [ i ] ms ≲ n ∷ ns
consʳ-≲ = _∘ □-tail

consˡ-≲ :
  ∀ {i m ms ns} →
  Bounded m ns →
  [ i ] ms .force ≲′ ns →
  [ i ] m ∷ ms ≲ ns
consˡ-≲ ◇m≤ns ms≲′ns ns⊑n =
  bounded-lemma ◇m≤ns ns⊑n ∷ λ { .force →
  ms≲′ns ns⊑n .force }

cons-≲ :
  ∀ {i m ms n ns} →
  Bounded m (n ∷ ns) →
  [ i ] ms .force ≲′ ns .force →
  [ i ] m ∷ ms ≲ n ∷ ns
cons-≲ {i} {m} {ms} {n} {ns} ◇m≤n∷ns =
  [ i ] ms .force ≲′ ns .force  ↝⟨ (λ { ms≲′ns hyp .force → consʳ-≲ (λ hyp → ms≲′ns hyp .force) hyp }) ⟩
  [ i ] ms .force ≲′ n ∷ ns     ↝⟨ consˡ-≲ ◇m≤n∷ns ⟩□
  [ i ] m ∷ ms ≲ n ∷ ns         □

cons′-≲ :
  ∀ {i m ms ns} →
  [ i ] ms .force ≲′ ns .force →
  [ i ] m ∷ ms ≲ m ∷ ns
cons′-≲ = cons-≲ (inj₁ (here Nat.≤-refl))

-- If the combinator consʳ-≲ had taken the primed variant of the
-- relation as an argument instead of the unprimed variant, then any
-- colist would have been bounded by any infinite colist.

consʳ-≲′→≲-infinite :
  (∀ {i ms ns n} → [ i ] ms ≲′ ns .force → [ i ] ms ≲ n ∷ ns) →
  (∀ {i ms ns} → Conat.[ ∞ ] length ns ∼ infinity → [ i ] ms ≲ ns)
consʳ-≲′→≲-infinite consʳ-≲′ {ns = []}    ()
consʳ-≲′→≲-infinite consʳ-≲′ {ns = _ ∷ _} (suc p) =
  consʳ-≲′ λ { hyp .force →
    consʳ-≲′→≲-infinite consʳ-≲′ (p .force) hyp }

-- Thus one cannot make this argument's type primed.

¬-consʳ-≲′ :
  ¬ (∀ {i ms ns n} → [ i ] ms ≲′ ns .force → [ i ] ms ≲ n ∷ ns)
¬-consʳ-≲′ =
  (∀ {i ms ns n} → [ i ] ms ≲′ ns .force → [ i ] ms ≲ n ∷ ns)       ↝⟨ consʳ-≲′→≲-infinite ⟩
  (∀ {i ms ns} → Conat.[ ∞ ] length ns ∼ infinity → [ i ] ms ≲ ns)  ↝⟨ (λ hyp → hyp (length-replicate _)) ⟩
  [ ∞ ] repeat  ≲ repeat                                          ↝⟨ _$ replicate⊑ _ ⟩
  [ ∞ ] repeat  ⊑ zero                                             ↝⟨ □-head ⟩
  [ ∞ ] ⌜  ⌝ ≤ ⌜  ⌝                                               ↝⟨ ≮0 ⟩□
  ⊥                                                                 □

-- Bisimilarity is contained in the relation.

∼→≲ : ∀ {i ms ns} → Colist.[ i ] ms ∼ ns → [ i ] ms ≲ ns
∼→≲ []          = []≲
∼→≲ (refl ∷ ps) = cons′-≲ λ { hyp .force → ∼→≲ (ps .force) hyp }

-- "Equational" reasoning combinators.

infix  -1 _□≲ finally-≲ finally-≲∼
infixr -2 step-≲ step-≡≲ _≡⟨⟩≲_ step-∼≲

step-≲ : ∀ {i} ms {ns os} →
         [ ∞ ] ns ≲ os → [ i ] ms ≲ ns → [ i ] ms ≲ os
step-≲ {i} ms {ns} {os} ns≲os ms≲ns {n = n} =
  [ ∞ ] os ⊑ n  ↝⟨ ns≲os ⟩
  [ ∞ ] ns ⊑ n  ↝⟨ ms≲ns ⟩□
  [ i ] ms ⊑ n  □

syntax step-≲ ms ns≲os ms≲ns = ms ≲⟨ ms≲ns ⟩ ns≲os

step-≡≲ : ∀ {i} ms {ns os} → [ i ] ns ≲ os → ms ≡ ns → [ i ] ms ≲ os
step-≡≲ _ ns≲os refl = ns≲os

syntax step-≡≲ ms ns≲os ms≡ns = ms ≡⟨ ms≡ns ⟩≲ ns≲os

_≡⟨⟩≲_ : ∀ {i} ms {ns} → [ i ] ms ≲ ns → [ i ] ms ≲ ns
_ ≡⟨⟩≲ ms≲ns = ms≲ns

step-∼≲ : ∀ {i} ms {ns os} →
          [ i ] ns ≲ os → Colist.[ i ] ms ∼ ns → [ i ] ms ≲ os
step-∼≲ {i} ms {ns} {os} ns≲os ms∼ns {n} =
  [ ∞ ] os ⊑ n  ↝⟨ ns≲os ⟩
  [ i ] ns ⊑ n  ↝⟨ □-∼ (Colist.symmetric-∼ ms∼ns) ⟩□
  [ i ] ms ⊑ n  □

syntax step-∼≲ ms ns≲os ms∼ns = ms ∼⟨ ms∼ns ⟩≲ ns≲os

finally-≲ : ∀ {i} ms ns → [ i ] ms ≲ ns → [ i ] ms ≲ ns
finally-≲ _ _ = id

syntax finally-≲ ms ns ms≲ns = ms ≲⟨ ms≲ns ⟩□ ns

finally-≲∼ : ∀ {i} ms ns → Colist.[ i ] ms ∼ ns → [ i ] ms ≲ ns
finally-≲∼ _ _ = ∼→≲

syntax finally-≲∼ ms ns ms∼ns = ms ∼⟨ ms∼ns ⟩□≲ ns

_□≲ : ∀ {i} ns → [ i ] ns ≲ ns
_□≲ {i} ns {n} =
  [ ∞ ] ns ⊑ n  ↝⟨ id ⟩□
  [ i ] ns ⊑ n  □

-- The transitivity proof can not be made size-preserving in the other
-- argument.

¬-transitivity-size-preservingʳ :
  ¬ (∀ {i ms ns os} → [ ∞ ] ms ≲ ns → [ i ] ns ≲ os → [ i ] ms ≲ os)
¬-transitivity-size-preservingʳ trans = contradiction
  where
  ones : ∀ {i} → Colist′ ℕ i
  ones .force = repeat 

  bad : ∀ {i} → [ i ]  ∷ ones ≲ repeat 
  bad {n = n} hyp = zero ∷ λ { .force {j} →  $⟨ (λ {_} → consʳ-≲ (repeat  □≲)) ⟩
    [ ∞ ] repeat  ≲  ∷ ones                ↝⟨ flip trans bad ⟩
    [ j ] repeat  ≲ repeat                 ↝⟨ (λ f → f hyp) ⟩□
    [ j ] repeat  ⊑ n                       □ }

  contradiction =              $⟨ (λ {_} → bad) ⟩
    [ ∞ ]  ∷ ones ≲ repeat   ↝⟨ _$ replicate⊑ _ ⟩
    [ ∞ ]  ∷ ones ⊑ zero      ↝⟨ □-head ∘ □-tail ⟩
    [ ∞ ] ⌜  ⌝ ≤ ⌜  ⌝        ↝⟨ ≮0 ⟩□
    ⊥                          □

-- The transitivity proof can not be made size-preserving in both
-- arguments.

¬-transitivity-size-preserving :
  ¬ (∀ {i ms ns os} → [ i ] ms ≲ ns → [ i ] ns ≲ os → [ i ] ms ≲ os)
¬-transitivity-size-preserving = ¬-transitivity-size-preservingʳ

-- If the least upper bound of ms is m and the least upper bound of ns
-- is n, then [ ∞ ] ms ≲ ns holds if and only if [ ∞ ] m ≤ n holds.

≲⇔least-upper-bounds-≤ :
  ∀ {m n ms ns} →
  LUB ms m → LUB ns n →
  [ ∞ ] ms ≲ ns ⇔ [ ∞ ] m ≤ n
≲⇔least-upper-bounds-≤ {⨆ms} {⨆ns} {ms} {ns} ⨆ms-lub ⨆ns-lub = record
  { to   = λ ms≲ns →          $⟨ proj₁ ⨆ns-lub ⟩
             [ ∞ ] ns ⊑ ⨆ns   ↝⟨ ms≲ns ⟩
             [ ∞ ] ms ⊑ ⨆ns   ↝⟨ proj₂ ⨆ms-lub _ ⟩□
             [ ∞ ] ⨆ms ≤ ⨆ns  □
  ; from = λ ⨆ms≤⨆ns {n} →
             [ ∞ ] ns ⊑ n   ↝⟨ proj₂ ⨆ns-lub n ⟩
             [ ∞ ] ⨆ns ≤ n  ↝⟨ transitive-≤ ⨆ms≤⨆ns ⟩
             [ ∞ ] ⨆ms ≤ n  ↝⟨ transitive-⊑≤ (proj₁ ⨆ms-lub) ⟩□
             [ ∞ ] ms ⊑ n   □
  }

------------------------------------------------------------------------
-- Another relation that can be used to relate the least upper bounds
-- of two colists

-- [ ∞ ] ms ≂ ns means that every upper bound of ns is also an upper
-- bound of ms, and vice versa.

infix  [_]_≂_ [_]_≂′_

[_]_≂_ : Size → Colist ℕ ∞ → Colist ℕ ∞ → Set
[ i ] ms ≂ ns = [ i ] ms ≲ ns × [ i ] ns ≲ ms

[_]_≂′_ : Size → Colist ℕ ∞ → Colist ℕ ∞ → Set
[ i ] ms ≂′ ns = [ i ] ms ≲′ ns × [ i ] ns ≲′ ms

-- The relation is symmetric.

symmetric-≂ : ∀ {i ms ns} → [ i ] ms ≂ ns → [ i ] ns ≂ ms
symmetric-≂ = swap

-- Some derived cons-like operations.

consʳ-≂ :
  ∀ {i ms n ns} →
  Bounded n ms →
  [ i ] ms ≂ ns .force →
  [ i ] ms ≂ n ∷ ns
consʳ-≂ ◇n≤ms = Σ-map
  consʳ-≲
  (λ ns≲ms → consˡ-≲ ◇n≤ms λ hyp → λ { .force → ns≲ms hyp })

consˡ-≂ :
  ∀ {i m ms ns} →
  Bounded m ns →
  [ i ] ms .force ≂ ns →
  [ i ] m ∷ ms ≂ ns
consˡ-≂ ◇m≤ns = symmetric-≂ ∘ consʳ-≂ ◇m≤ns ∘ symmetric-≂

cons-≂ :
  ∀ {i m ms n ns} →
  Bounded m (n ∷ ns) →
  Bounded n (m ∷ ms) →
  [ i ] ms .force ≂′ ns .force →
  [ i ] m ∷ ms ≂ n ∷ ns
cons-≂ ◇m≤n∷ns ◇n≤m∷ms = Σ-map (cons-≲ ◇m≤n∷ns) (cons-≲ ◇n≤m∷ms)

cons′-≂ :
  ∀ {i m ms ns} →
  [ i ] ms .force ≂′ ns .force →
  [ i ] m ∷ ms ≂ m ∷ ns
cons′-≂ = Σ-map cons′-≲ cons′-≲

cons″-≂ :
  ∀ {i m ms ns} →
  [ i ] ms .force ≂ ns .force →
  [ i ] m ∷ ms ≂ m ∷ ns
cons″-≂ = cons′-≂ ∘ Σ-map (λ { ms≲ns hyp .force → ms≲ns hyp })
                          (λ { ns≲ms hyp .force → ns≲ms hyp })

-- Bisimilarity is contained in the relation.

∼→≂ : ∀ {i ms ns} → Colist.[ i ] ms ∼ ns → [ i ] ms ≂ ns
∼→≂ ms∼ns = ∼→≲ ms∼ns , ∼→≲ (Colist.symmetric-∼ ms∼ns)

-- "Equational" reasoning combinators.

infix  -1 _□≂ finally-≂ finally-≂∼
infixr -2 step-≂ step-≡≂ _≡⟨⟩≂_ step-∼≂ step-≂∼

step-≂ : ∀ {i} ms {ns os} →
         [ ∞ ] ns ≂ os → [ ∞ ] ms ≂ ns → [ i ] ms ≂ os
step-≂ _ = Σ-zip (step-≲ _) (flip (step-≲ _))

syntax step-≂ ms ns≂os ms≂ns = ms ≂⟨ ms≂ns ⟩ ns≂os

step-≡≂ : ∀ {i} ms {ns os} → [ i ] ns ≂ os → ms ≡ ns → [ i ] ms ≂ os
step-≡≂ _ ns≂os refl = ns≂os

syntax step-≡≂ ms ns≂os ms≡ns = ms ≡⟨ ms≡ns ⟩≂ ns≂os

_≡⟨⟩≂_ : ∀ {i} ms {ns} → [ i ] ms ≂ ns → [ i ] ms ≂ ns
_ ≡⟨⟩≂ ms≂ns = ms≂ns

step-∼≂ : ∀ {i} ms {ns os} →
          [ i ] ns ≂ os → Colist.[ ∞ ] ms ∼ ns → [ i ] ms ≂ os
step-∼≂ {i} ms {ns} {os} (ns≲os , os≲ns) ms∼ns =
    step-∼≲ ms ns≲os ms∼ns
  , λ {n} →
      [ ∞ ] ms ⊑ n  ↝⟨ □-∼ ms∼ns ⟩
      [ ∞ ] ns ⊑ n  ↝⟨ os≲ns ⟩□
      [ i ] os ⊑ n  □

syntax step-∼≂ ms ns≂os ms∼ns = ms ∼⟨ ms∼ns ⟩≂ ns≂os

step-≂∼ : ∀ {i} ms {ns os} →
          Colist.[ ∞ ] ns ∼ os → [ i ] ms ≂ ns → [ i ] ms ≂ os
step-≂∼ _ ns∼os ms≂ns =
  symmetric-≂
    (step-∼≂ _ (symmetric-≂ ms≂ns) (Colist.symmetric-∼ ns∼os))

syntax step-≂∼ ms ns∼os ms≂ns = ms ≂⟨ ms≂ns ⟩∼ ns∼os

finally-≂ : ∀ {i} ms ns → [ i ] ms ≂ ns → [ i ] ms ≂ ns
finally-≂ _ _ = id

syntax finally-≂ ms ns ms≂ns = ms ≂⟨ ms≂ns ⟩□ ns

finally-≂∼ : ∀ {i} ms ns → Colist.[ i ] ms ∼ ns → [ i ] ms ≂ ns
finally-≂∼ _ _ = ∼→≂

syntax finally-≂∼ ms ns ms∼ns = ms ∼⟨ ms∼ns ⟩□≂ ns

_□≂ : ∀ {i} ns → [ i ] ns ≂ ns
ns □≂ = (ns □≲) , (ns □≲)

-- If the least upper bound of ms is m and the least upper bound of ns
-- is n, then [ ∞ ] ms ≂ ns holds if and only if m and n are
-- bisimilar.

≂⇔least-upper-bounds-∼ :
  ∀ {m n ms ns} →
  LUB ms m → LUB ns n →
  [ ∞ ] ms ≂ ns ⇔ Conat.[ ∞ ] m ∼ n
≂⇔least-upper-bounds-∼ {⨆ms} {⨆ns} {ms} {ns} ⨆ms-lub ⨆ns-lub =
  [ ∞ ] ms ≂ ns                      ↝⟨ ≲⇔least-upper-bounds-≤ ⨆ms-lub ⨆ns-lub
                                          ×-cong
                                        ≲⇔least-upper-bounds-≤ ⨆ns-lub ⨆ms-lub ⟩
  [ ∞ ] ⨆ms ≤ ⨆ns × [ ∞ ] ⨆ns ≤ ⨆ms  ↝⟨ record { to   = uncurry antisymmetric-≤
                                               ; from = λ hyp → ∼→≤ hyp , ∼→≤ (Conat.symmetric-∼ hyp)
                                               } ⟩□
  Conat.[ ∞ ] ⨆ms ∼ ⨆ns              □

-- The predicate flip LUB n respects [ ∞ ]_≂_.

LUB-≂ : ∀ {ms ns n} → [ ∞ ] ms ≂ ns → LUB ms n → LUB ns n
LUB-≂ {ms} {ns} {n} (ms≲ns , ns≲ms) = Σ-map
  ([ ∞ ] ms ⊑ n  ↝⟨ ns≲ms ⟩□
   [ ∞ ] ns ⊑ n  □)
  ((∀ n′ → [ ∞ ] ms ⊑ n′ → [ ∞ ] n ≤ n′)  ↝⟨ (λ hyp n′ → hyp n′ ∘ ms≲ns) ⟩□
   (∀ n′ → [ ∞ ] ns ⊑ n′ → [ ∞ ] n ≤ n′)  □)

-- If [ ∞ ] ms ≂ ns holds, then ms and ns have the same least upper
-- bounds.

LUB-cong : ∀ {ms ns n} → [ ∞ ] ms ≂ ns → LUB ms n ⇔ LUB ns n
LUB-cong ms≂ns = record
  { to   = LUB-≂              ms≂ns
  ; from = LUB-≂ (symmetric-≂ ms≂ns)
  }

------------------------------------------------------------------------
-- Variants of [_]_≲_ and [_]_≂_ that are intended to make certain
-- proofs easier to write

-- Using consˡ-≲/cons-≲/cons′-≲ in recursive proofs can be awkward.
-- [_]_≲D_ is intended to make it a little easier.

mutual

  infix  [_]_≲D_ [_]_≲D′_

  data [_]_≲D_ (i : Size) : Colist ℕ ∞ → Colist ℕ ∞ → Set where
    ⌈_⌉      : ∀ {ms ns} →
               [ i ] ms ≲ ns →
               [ i ] ms ≲D ns
    consˡ-≲D : ∀ {m ms ns} →
               Bounded m ns →
               [ i ] ms .force ≲D′ ns →
               [ i ] m ∷ ms ≲D ns
    cons-≲D  : ∀ {m ms n ns} →
               Bounded m (n ∷ ns) →
               [ i ] ms .force ≲D′ ns .force →
               [ i ] m ∷ ms ≲D n ∷ ns

  record [_]_≲D′_ (i : Size) (ms ns : Colist ℕ ∞) : Set where
    coinductive
    field
      force : {j : Size< i} → [ j ] ms ≲D ns

open [_]_≲D′_ public

-- Interprets [_]_≲D_.

⌊_⌋≲ : ∀ {i ms ns} → [ i ] ms ≲D ns → [ i ] ms ≲ ns
⌊ ⌈ p ⌉ ⌋≲        = p
⌊ consˡ-≲D b p ⌋≲ = consˡ-≲ b λ { hyp .force → ⌊ p .force ⌋≲ hyp }
⌊ cons-≲D b p ⌋≲  = cons-≲  b λ { hyp .force → ⌊ p .force ⌋≲ hyp }

-- Some abbreviations.

consʳ-≲D :
  ∀ {i ms n ns} →
  [ i ] ms ≲D ns .force →
  [ i ] ms ≲D n ∷ ns
consʳ-≲D = ⌈_⌉ ∘ consʳ-≲ ∘ ⌊_⌋≲

cons′-≲D :
  ∀ {i m ms ns} →
  [ i ] ms .force ≲D′ ns .force →
  [ i ] m ∷ ms ≲D m ∷ ns
cons′-≲D p = ⌈ cons′-≲ (λ { hyp .force → ⌊ p .force ⌋≲ hyp }) ⌉

-- Using cons-≂/cons′-≂ in recursive proofs can be awkward. [_]_≂D_ is
-- intended to make it a little easier.

mutual

  infix  [_]_≂D_ [_]_≂D′_

  data [_]_≂D_ (i : Size) : Colist ℕ ∞ → Colist ℕ ∞ → Set where
    ⌈_⌉      : ∀ {ms ns} →
               [ i ] ms ≂ ns →
               [ i ] ms ≂D ns
    consʳ-≂D : ∀ {ms n ns} →
               Bounded n ms →
               [ i ] ms ≂D ns .force →
               [ i ] ms ≂D n ∷ ns
    consˡ-≂D : ∀ {m ms ns} →
               Bounded m ns →
               [ i ] ms .force ≂D ns →
               [ i ] m ∷ ms ≂D ns
    cons-≂D  : ∀ {m ms n ns} →
               Bounded m (n ∷ ns) →
               Bounded n (m ∷ ms) →
               [ i ] ms .force ≂D′ ns .force →
               [ i ] m ∷ ms ≂D n ∷ ns

  record [_]_≂D′_ (i : Size) (ms ns : Colist ℕ ∞) : Set where
    coinductive
    field
      force : {j : Size< i} → [ j ] ms ≂D ns

open [_]_≂D′_ public

-- Interprets [_]_≂D_.

⌊_⌋≂ : ∀ {i ms ns} → [ i ] ms ≂D ns → [ i ] ms ≂ ns
⌊ ⌈ p ⌉ ⌋≂           = p
⌊ consʳ-≂D b p ⌋≂    = consʳ-≂ b ⌊ p ⌋≂
⌊ consˡ-≂D b p ⌋≂    = consˡ-≂ b ⌊ p ⌋≂
⌊ cons-≂D b₁ b₂ p ⌋≂ =
  cons-≂ b₁ b₂ ( (λ { hyp .force {j} → proj₁ ⌊ p .force {j} ⌋≂ hyp  })
               , (λ { hyp .force     → proj₂ ⌊ p .force     ⌋≂ hyp  })
               )

-- An abbreviation.

cons′-≂D :
  ∀ {i m ms ns} →
  [ i ] ms .force ≂D′ ns .force →
  [ i ] m ∷ ms ≂D m ∷ ns
cons′-≂D = cons-≂D (inj₁ (here Nat.≤-refl)) (inj₁ (here Nat.≤-refl))

-- A workaround for what might be an Agda bug.

cast-≂ :
  ∀ {i} {j : Size< i} {ms ns} →
  [ i ] ms ≂ ns → [ j ] ms ≂ ns
cast-≂ {i} p = ⌊ [_]_≂D_.⌈_⌉ {i = i} p ⌋≂