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

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

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 Size

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 4 [_]_⊑_ [_]_⊑′_

[_]_⊑_ : 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 4 _⊑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   0          ↝⟨ □-head  □-tail 
  Conat.[  ]  1    0   ↝⟨ ≮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 []  0 
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 4 [_]_≲_ [_]_≲′_

[_]_≲_ : 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 1  repeat 0                                         ↝⟨ _$ replicate⊑ _ 
  [  ] repeat 1  zero                                             ↝⟨ □-head 
  [  ]  1    0                                                ↝⟨ ≮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 1

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

  contradiction =              $⟨  {_}  bad) 
    [  ] 0  ones  repeat 0  ↝⟨ _$ replicate⊑ _ 
    [  ] 0  ones  zero      ↝⟨ □-head  □-tail 
    [  ]  1    0         ↝⟨ ≮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 4 [_]_≂_ [_]_≂′_

[_]_≂_ : 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)
  }

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

cast-≂ :
   {i} {j : Size< i} {ms ns} 
  [ i ] ms  ns  [ j ] ms  ns
cast-≂ p = proj₁ p , proj₂ p

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

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

infix 4 [_]_≲″_

record [_]_≲″_ (i : Size) (ms ns : Colist  ) : Set where
  coinductive
  field
    force : {j : Size< i}  [ j ] ms  ns

open [_]_≲″_ public

-- Interprets [_]_≲″_.

⌊_⌋≲″ :  {i ms ns}  [ i ] ms ≲″ ns  [ i ] ms ≲′ ns
 p ⌋≲″ hyp .force = p .force hyp

-- [_]_≲′_ and [_]_≲″_ are pointwise logically equivalent.

≲′⇔≲″ :  {i ms ns}  [ i ] ms ≲′ ns  [ i ] ms ≲″ ns
≲′⇔≲″ = record
  { to   = λ { p .force hyp  p hyp .force }
  ; from = λ { p hyp .force  p .force hyp }
  }

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

infix 4 [_]_≂″_

record [_]_≂″_ (i : Size) (ms ns : Colist  ) : Set where
  coinductive
  field
    force : {j : Size< i}  [ j ] ms  ns

open [_]_≂″_ public

-- [_]_≂′_ and [_]_≂″_ are pointwise logically equivalent.

≂′⇔≂″ :  {i ms ns}  [ i ] ms ≂′ ns  [ i ] ms ≂″ ns
≂′⇔≂″ = record
  { to   = λ { p .force   hyp  proj₁ p hyp .force)
                        ,  hyp  proj₂ p hyp .force)
             }
  ; from = λ p   { hyp .force  proj₁ (p .force) hyp })
               ,  { hyp .force  proj₂ (p .force) hyp })
  }