------------------------------------------------------------------------
-- Colists
------------------------------------------------------------------------

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

module Colist where

open import Conat using (Conat; zero; suc; force; infinity)
open import Equality.Propositional as E using (_≡_; refl)
open import Logical-equivalence using (_⇔_)
open import Prelude

open import Function-universe E.equality-with-J hiding (id; _∘_)
import Nat E.equality-with-J as Nat

------------------------------------------------------------------------
-- The type

-- Colists.

mutual

  infixr  _∷_

  data Colist {a} (A : Set a) (i : Size) : Set a where
    []  : Colist A i
    _∷_ : A → Colist′ A i → Colist A i

  record Colist′ {a} (A : Set a) (i : Size) : Set a where
    coinductive
    field
      force : {j : Size< i} → Colist A j

open Colist′ public

------------------------------------------------------------------------
-- Some operations

-- A variant of cons.

infixr  _∷′_

_∷′_ : ∀ {i a} {A : Set a} → A → Colist A i → Colist A i
x ∷′ xs = x ∷ λ { .force → xs }

-- The colist's tail, if any.

tail : ∀ {a} {A : Set a} {i} → Colist A i → Colist′ A i
tail xs@[]    = λ { .force → xs }
tail (x ∷ xs) = xs

-- A map function.

map : ∀ {a b i} {A : Set a} {B : Set b} →
      (A → B) → Colist A i → Colist B i
map f []       = []
map f (x ∷ xs) = f x ∷ λ { .force → map f (force xs) }

-- The length of a colist.

length : ∀ {a i} {A : Set a} → Colist A i → Conat i
length []       = zero
length (n ∷ ns) = suc λ { .force → length (force ns) }

-- The colist replicate n x contains exactly n copies of x (and
-- nothing else).

replicate : ∀ {a i} {A : Set a} → Conat i → A → Colist A i
replicate zero    x = []
replicate (suc n) x = x ∷ λ { .force → replicate (force n) x }

-- Repeats the given element indefinitely.

repeat : ∀ {a i} {A : Set a} → A → Colist A i
repeat = replicate infinity

-- Appends one colist to another.

infixr  _++_

_++_ : ∀ {a i} {A : Set a} → Colist A i → Colist A i → Colist A i
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ λ { .force → force xs ++ ys }

-- The colist cycle x xs is an endless cycle of repetitions of the
-- colist x ∷ xs.

cycle : ∀ {a i} {A : Set a} → A → Colist′ A i → Colist A i
cycle x xs = x ∷ λ { .force → force xs ++ cycle x xs }

-- "Scan left".

scanl : ∀ {a b i} {A : Set a} {B : Set b} →
        (A → B → A) → A → Colist B i → Colist A i
scanl c n []       = n ∷ λ { .force → [] }
scanl c n (x ∷ xs) = n ∷ λ { .force → scanl c (c n x) (force xs) }

-- The natural numbers in strictly increasing order.

nats : ∀ {i} → Colist ℕ i
nats =  ∷ λ { .force → map suc nats }

-- The colist nats-from n is the natural numbers greater than or equal
-- to n, in strictly increasing order.

nats-from : ∀ {i} → ℕ → Colist ℕ i
nats-from n = n ∷ λ { .force → nats-from (suc n) }

-- The list take n xs is the longest possible prefix of xs that
-- contains at most n elements.

take : ∀ {a} {A : Set a} → ℕ → Colist A ∞ → List A
take zero    _        = []
take _       []       = []
take (suc n) (x ∷ xs) = x ∷ take n (force xs)

------------------------------------------------------------------------
-- Bisimilarity

module _ {a} {A : Set a} where

  -- [ ∞ ] xs ∼ ys means that xs and ys are "equal".

  mutual

    infix  [_]_∼_ [_]_∼′_

    data [_]_∼_ (i : Size) : Colist A ∞ → Colist A ∞ → Set a where
      []  : [ i ] [] ∼ []
      _∷_ : ∀ {x y xs ys} →
            x ≡ y → [ i ] force xs ∼′ force ys → [ i ] x ∷ xs ∼ y ∷ ys

    record [_]_∼′_ (i : Size) (xs ys : Colist A ∞) : Set a where
      coinductive
      field
        force : {j : Size< i} → [ j ] xs ∼ ys

  open [_]_∼′_ public

  -- Bisimilarity is an equivalence relation.

  reflexive-∼ : ∀ {i} xs → [ i ] xs ∼ xs
  reflexive-∼ []       = []
  reflexive-∼ (x ∷ xs) = refl ∷ λ { .force → reflexive-∼ (force xs) }

  symmetric-∼ : ∀ {i xs ys} →
                [ i ] xs ∼ ys → [ i ] ys ∼ xs
  symmetric-∼ []        = []
  symmetric-∼ (p₁ ∷ p₂) =
    E.sym p₁ ∷ λ { .force → symmetric-∼ (force p₂) }

  transitive-∼ : ∀ {i xs ys zs} →
                 [ i ] xs ∼ ys → [ i ] ys ∼ zs → [ i ] xs ∼ zs
  transitive-∼ []        []        = []
  transitive-∼ (p₁ ∷ p₂) (q₁ ∷ q₂) =
    E.trans p₁ q₁ ∷ λ { .force → transitive-∼ (force p₂) (force q₂) }

  -- Equational reasoning combinators.

  infix  -1 _∎
  infixr -2 step-∼ step-≡ _∼⟨⟩_

  _∎ : ∀ {i} xs → [ i ] xs ∼ xs
  _∎ = reflexive-∼

  step-∼ : ∀ {i} xs {ys zs} →
           [ i ] ys ∼ zs → [ i ] xs ∼ ys → [ i ] xs ∼ zs
  step-∼ _ ys∼zs xs∼ys = transitive-∼ xs∼ys ys∼zs

  syntax step-∼ xs ys∼zs xs∼ys = xs ∼⟨ xs∼ys ⟩ ys∼zs

  step-≡ : ∀ {i} xs {ys zs} → [ i ] ys ∼ zs → xs ≡ ys → [ i ] xs ∼ zs
  step-≡ _ ys∼zs refl = ys∼zs

  syntax step-≡ xs ys∼zs xs≡ys = xs ≡⟨ xs≡ys ⟩ ys∼zs

  _∼⟨⟩_ : ∀ {i} xs {ys} → [ i ] xs ∼ ys → [ i ] xs ∼ ys
  _ ∼⟨⟩ xs∼ys = xs∼ys

  -- A property relating Colist._∷_ and _∷′_.

  ∷∼∷′ : ∀ {i} {x : A} {xs} →
         [ i ] x ∷ xs ∼ x ∷′ force xs
  ∷∼∷′ = refl ∷ λ { .force → reflexive-∼ _ }

-- Functor laws.

map-id :
  ∀ {a i} {A : Set a} (xs : Colist A ∞) →
  [ i ] map id xs ∼ xs
map-id []       = []
map-id (_ ∷ xs) = refl ∷ λ { .force → map-id (force xs) }

map-∘ :
  ∀ {a b c i} {A : Set a} {B : Set b} {C : Set c}
    {f : B → C} {g : A → B}
  (xs : Colist A ∞) →
  [ i ] map (f ∘ g) xs ∼ map f (map g xs)
map-∘ []       = []
map-∘ (_ ∷ xs) = refl ∷ λ { .force → map-∘ (force xs) }

-- If two non-empty colists are bisimilar, then their heads are
-- bisimilar.

head-cong : ∀ {a i} {A : Set a} {x y : A} {xs ys} →
            [ i ] x ∷ xs ∼ y ∷ ys → x ≡ y
head-cong (p ∷ _) = p

-- Some preservation lemmas.

tail-cong :
  ∀ {a i} {A : Set a} {xs ys : Colist A ∞} →
  [ i ] xs ∼ ys → [ i ] force (tail xs) ∼′ force (tail ys)
tail-cong []       = λ { .force → [] }
tail-cong (_ ∷ ps) = ps

map-cong :
  ∀ {a b i} {A : Set a} {B : Set b} {f g : A → B} {xs ys} →
  (∀ x → f x ≡ g x) → [ i ] xs ∼ ys → [ i ] map f xs ∼ map g ys
map-cong f≡g []          = []
map-cong f≡g (refl ∷ ps) =
  f≡g _ ∷ λ { .force → map-cong f≡g (force ps) }

length-cong :
  ∀ {a i} {A : Set a} {xs ys : Colist A ∞} →
  [ i ] xs ∼ ys → Conat.[ i ] length xs ∼ length ys
length-cong []       = zero
length-cong (_ ∷ ps) = suc λ { .force → length-cong (force ps) }

replicate-cong :
  ∀ {a i} {A : Set a} {m n} {x : A} →
  Conat.[ i ] m ∼ n → [ i ] replicate m x ∼ replicate n x
replicate-cong zero    = []
replicate-cong (suc p) = refl ∷ λ { .force → replicate-cong (force p) }

infixr  _++-cong_

_++-cong_ :
  ∀ {a i} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : Colist A ∞} →
  [ i ] xs₁ ∼ ys₁ → [ i ] xs₂ ∼ ys₂ → [ i ] xs₁ ++ xs₂ ∼ ys₁ ++ ys₂
[]       ++-cong qs = qs
(p ∷ ps) ++-cong qs = p ∷ λ { .force → force ps ++-cong qs }

cycle-cong :
  ∀ {a i} {A : Set a} {x : A} {xs ys} →
  [ i ] force xs ∼′ force ys → [ i ] cycle x xs ∼ cycle x ys
cycle-cong p = refl ∷ λ { .force → force p ++-cong cycle-cong p }

scanl-cong :
  ∀ {a b i} {A : Set a} {B : Set b} {c : A → B → A} {n : A} {xs ys} →
  [ i ] xs ∼ ys → [ i ] scanl c n xs ∼ scanl c n ys
scanl-cong []          = refl ∷ λ { .force → [] }
scanl-cong (refl ∷ ps) = refl ∷ λ { .force → scanl-cong (force ps) }

take-cong :
  ∀ {a} {A : Set a} n {xs ys : Colist A ∞} →
  [ ∞ ] xs ∼ ys → take n xs ≡ take n ys
take-cong n       []       = refl
take-cong zero    (p ∷ ps) = refl
take-cong (suc n) (p ∷ ps) = E.cong₂ _∷_ p (take-cong n (force ps))

-- The length of replicate n x is bisimilar to n.

length-replicate :
  ∀ {a i} {A : Set a} {x : A} n →
  Conat.[ i ] length (replicate n x) ∼ n
length-replicate zero    = zero
length-replicate (suc n) =
  suc λ { .force → length-replicate (force n) }

-- A lemma relating nats and nats-from n.

map-+-nats∼nats-from :
  ∀ {i} n → [ i ] map (n +_) nats ∼ nats-from n
map-+-nats∼nats-from n = Nat.+-right-identity ∷ λ { .force →
  map (n +_) (map suc nats)  ∼⟨ symmetric-∼ (map-∘ _) ⟩
  map ((n +_) ∘ suc) nats    ∼⟨ map-cong (λ _ → E.sym (Nat.suc+≡+suc _)) (_ ∎) ⟩
  map (suc n +_) nats        ∼⟨ map-+-nats∼nats-from (suc n) ⟩
  nats-from (suc n)          ∎ }

-- The colist nats is bisimilar to nats-from 0.

nats∼nats-from-0 : ∀ {i} → [ i ] nats ∼ nats-from 
nats∼nats-from-0 =
  nats             ∼⟨ symmetric-∼ (map-id _) ⟩
  map id nats      ∼⟨⟩
  map ( +_) nats  ∼⟨ map-+-nats∼nats-from _ ⟩
  nats-from       ∎

------------------------------------------------------------------------
-- The ◇ predicate

-- ◇ ∞ P xs means that P holds for some element in xs.

data ◇ {a p} {A : Set a} (i : Size)
       (P : A → Set p) : Colist A ∞ → Set (a ⊔ p) where
  here  : ∀ {x xs} → P x → ◇ i P (x ∷ xs)
  there : ∀ {x xs} {j : Size< i} → ◇ j P (force xs) → ◇ i P (x ∷ xs)

-- ◇ respects bisimilarity.

◇-∼ :
  ∀ {a p i} {A : Set a} {P : A → Set p} {xs ys} →
  [ ∞ ] xs ∼ ys → ◇ i P xs → ◇ i P ys
◇-∼ (refl ∷ _) (here p)  = here p
◇-∼ (_    ∷ b) (there p) = there (◇-∼ (force b) p)

-- A map function for ◇.

◇-map : ∀ {a p q i} {A : Set a} {P : A → Set p} {Q : A → Set q} →
        (∀ {x} → P x → Q x) →
        (∀ {xs} → ◇ i P xs → ◇ i Q xs)
◇-map f (here p)  = here (f p)
◇-map f (there p) = there (◇-map f p)

-- A variant of ◇-map.

◇-map′ : ∀ {a b c p q i} {A : Set a} {B : Set b} {C : Set c}
           {P : B → Set p} {Q : C → Set q}
           {f : A → B} {g : A → C} →
         (∀ {x} → P (f x) → Q (g x)) →
         (∀ {xs} → ◇ i P (map f xs) → ◇ i Q (map g xs))
◇-map′ g {_ ∷ _} (here p)  = here (g p)
◇-map′ g {_ ∷ _} (there p) = there (◇-map′ g p)
◇-map′ g {[]}    ()

-- If a predicate holds for some element in a colist, then it holds
-- for some value.

◇-witness : ∀ {a p i} {A : Set a} {P : A → Set p} {xs} →
            ◇ i P xs → ∃ P
◇-witness (here p)  = _ , p
◇-witness (there p) = ◇-witness p

-- If const P holds for some element, then P holds.

◇-const : ∀ {a p i} {A : Set a} {P : Set p} {xs : Colist A ∞} →
          ◇ i (const P) xs → P
◇-const = proj₂ ∘ ◇-witness

-- Colist membership.

infix  [_]_∈_

[_]_∈_ : ∀ {a} {A : Set a} → Size → A → Colist A ∞ → Set a
[ i ] x ∈ xs = ◇ i (x ≡_) xs

-- A generalisation of "◇ ∞ P xs holds iff P holds for some element in
-- xs".

◇⇔∈× : ∀ {a p i} {A : Set a} {P : A → Set p} {xs} →
       ◇ i P xs ⇔ ∃ λ x → [ i ] x ∈ xs × P x
◇⇔∈× {P = P} = record { to = to; from = from }
  where
  to : ∀ {i xs} → ◇ i P xs → ∃ λ x → [ i ] x ∈ xs × P x
  to (here p)  = _ , here refl , p
  to (there p) = Σ-map id (Σ-map there id) (to p)

  from : ∀ {i xs} → (∃ λ x → [ i ] x ∈ xs × P x) → ◇ i P xs
  from (x , here refl  , p) = here p
  from (x , there x∈xs , p) = there (from (x , x∈xs , p))

-- If P holds for some element in replicate (suc n) x, then it also
-- holds for x, and vice versa.

◇-replicate-suc⇔ :
  ∀ {a p i} {A : Set a} {P : A → Set p} {x : A} {n} →
  ◇ i P (replicate (suc n) x) ⇔ P x
◇-replicate-suc⇔ {P = P} {x} = record
  { to   = to _
  ; from = here
  }
  where
  to : ∀ {i} n → ◇ i P (replicate n x) → P x
  to zero    ()
  to (suc n) (here p)  = p
  to (suc n) (there p) = to (force n) p

-- If P holds for some element in cycle x xs, then it also holds for
-- some element in x ∷ xs, and vice versa.

◇-cycle⇔ :
  ∀ {a p i} {A : Set a} {P : A → Set p} {x : A} {xs} →
  ◇ i P (cycle x xs) ⇔ ◇ i P (x ∷ xs)
◇-cycle⇔ {i = i} {P = P} {x} {xs} = record
  { to   = ◇ i P (cycle x xs)               ↝⟨ ◇-∼ (transitive-∼ ∷∼∷′ (symmetric-∼ ∷∼∷′)) ⟩
           ◇ i P ((x ∷ xs) ++ cycle x xs)   ↝⟨ to _ ⟩
           ◇ i P (x ∷ xs) ⊎ ◇ i P (x ∷ xs)  ↝⟨ [ id , id ] ⟩□
           ◇ i P (x ∷ xs)                   □
  ; from = ◇ i P (x ∷ xs)                  ↝⟨ from ⟩
           ◇ i P ((x ∷ xs) ++ cycle x xs)  ↝⟨ ◇-∼ (transitive-∼ ∷∼∷′ (symmetric-∼ ∷∼∷′)) ⟩□
           ◇ i P (cycle x xs)              □
  }
  where
  to : ∀ {i} ys → ◇ i P (ys ++ cycle x xs) → ◇ i P ys ⊎ ◇ i P (x ∷ xs)
  to []       (here p)  = inj₂ (here p)
  to []       (there p) = case to (force xs) p of
                            [ inj₂ ∘ there , inj₂ ]
  to (y ∷ ys) (here p)  = inj₁ (here p)
  to (y ∷ ys) (there p) = ⊎-map there id (to (force ys) p)

  from : ∀ {i ys} → ◇ i P ys → ◇ i P (ys ++ cycle x xs)
  from (here p)   = here p
  from (there ps) = there (from ps)

------------------------------------------------------------------------
-- The □ predicate

-- □ ∞ P xs means that P holds for every element in xs.

mutual

  data □ {a p} {A : Set a} (i : Size)
         (P : A → Set p) : Colist A ∞ → Set (a ⊔ p) where
    []  : □ i P []
    _∷_ : ∀ {x xs} → P x → □′ i P (force xs) → □ i P (x ∷ xs)

  record □′ {a p} {A : Set a} (i : Size)
            (P : A → Set p) (xs : Colist A ∞) : Set (a ⊔ p) where
    coinductive
    field
      force : {j : Size< i} → □ j P xs

open □′ public

-- Some projections.

□-head : ∀ {a p i} {A : Set a} {P : A → Set p} {x xs} →
         □ i P (x ∷ xs) → P x
□-head (p ∷ _) = p

□-tail : ∀ {a p i} {j : Size< i} {A : Set a} {P : A → Set p} {x xs} →
         □ i P (x ∷ xs) → □ j P (force xs)
□-tail (_ ∷ ps) = force ps

-- □ respects bisimilarity.

□-∼ :
  ∀ {i a p} {A : Set a} {P : A → Set p} {xs ys} →
  [ i ] xs ∼ ys → □ i P xs → □ i P ys
□-∼ []         _        = []
□-∼ (refl ∷ b) (p ∷ ps) = p ∷ λ { .force → □-∼ (force b) (force ps) }

-- A generalisation of "□ ∞ P xs holds iff P is true for every element
-- in xs".

□⇔∈→ : ∀ {a p i} {A : Set a} {P : A → Set p} {xs} →
       □ i P xs ⇔ (∀ x → [ i ] x ∈ xs → P x)
□⇔∈→ {P = P} = record { to = to; from = from _ }
  where
  to : ∀ {i xs} → □ i P xs → (∀ x → [ i ] x ∈ xs → P x)
  to (p ∷ ps) x (here refl)  = p
  to (p ∷ ps) x (there x∈xs) = to (force ps) x x∈xs

  from : ∀ {i} xs → (∀ x → [ i ] x ∈ xs → P x) → □ i P xs
  from []       f = []
  from (x ∷ xs) f =
    f x (here refl) ∷ λ { .force → from (force xs) (λ x → f x ∘ there) }

-- If P is universally true, then □ i P is also universally true.

□-replicate : ∀ {a p i} {A : Set a} {P : A → Set p} →
              (∀ x → P x) →
              (∀ xs → □ i P xs)
□-replicate f _ = _⇔_.from □⇔∈→ (λ x _ → f x)

-- Something resembling applicative functor application for □.

infixl  _□-⊛_

_□-⊛_ : ∀ {i a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {xs} →
        □ i (λ x → P x → Q x) xs → □ i P xs → □ i Q xs
[]       □-⊛ _        = []
(f ∷ fs) □-⊛ (p ∷ ps) = f p ∷ λ { .force → force fs □-⊛ force ps }

-- A map function for □.

□-map : ∀ {a p q i} {A : Set a} {P : A → Set p} {Q : A → Set q} →
        (∀ {x} → P x → Q x) →
        (∀ {xs} → □ i P xs → □ i Q xs)
□-map f ps = □-replicate (λ _ → f) _ □-⊛ ps

-- A variant of □-map.

□-map′ : ∀ {a b c p q i} {A : Set a} {B : Set b} {C : Set c}
           {P : B → Set p} {Q : C → Set q}
           {f : A → B} {g : A → C} →
         (∀ {x} → P (f x) → Q (g x)) →
         (∀ {xs} → □ i P (map f xs) → □ i Q (map g xs))
□-map′ g {[]}    []       = []
□-map′ g {_ ∷ _} (p ∷ ps) = g p ∷ λ { .force → □-map′ g (force ps) }

-- Something resembling applicative functor application for □ and ◇.

infixl  _□◇-⊛_

_□◇-⊛_ : ∀ {a p q i} {A : Set a} {P : A → Set p} {Q : A → Set q} {xs} →
         □ i (λ x → P x → Q x) xs → ◇ i P xs → ◇ i Q xs
(f ∷ _)  □◇-⊛ (here p)  = here (f p)
(_ ∷ fs) □◇-⊛ (there p) = there (force fs □◇-⊛ p)

-- A combination of some of the combinators above.

□◇-witness :
  ∀ {a p q i} {A : Set a} {P : A → Set p} {Q : A → Set q} {xs} →
  □ i P xs → ◇ i Q xs → ∃ λ x → P x × Q x
□◇-witness p q = ◇-witness (□-map _,_ p □◇-⊛ q)

-- If P holds for every element in replicate (suc n) x, then it also holds
-- for x, and vice versa.

□-replicate-suc⇔ :
  ∀ {a p i} {A : Set a} {P : A → Set p} {x : A} {n} →
  □ i P (replicate (suc n) x) ⇔ P x
□-replicate-suc⇔ {P = P} {x} = record
  { to   = □-head
  ; from = from _
  }
  where
  from : ∀ {i} n → P x → □ i P (replicate n x)
  from zero    p = []
  from (suc n) p = p ∷ λ { .force → from (force n) p }

-- If P holds for every element in cycle x xs, then it also holds for
-- every element in x ∷ xs, and vice versa.

□-cycle⇔ :
  ∀ {a p i} {A : Set a} {P : A → Set p} {x : A} {xs} →
  □ i P (cycle x xs) ⇔ □ i P (x ∷ xs)
□-cycle⇔ {i = i} {P = P} {x} {xs} = record
  { to   = □ i P (cycle x xs)              ↝⟨ (λ { (p ∷ ps) → p ∷ ps }) ⟩
           □ i P ((x ∷ xs) ++ cycle x xs)  ↝⟨ to _ ⟩□
           □ i P (x ∷ xs)                  □
  ; from = □ i P (x ∷ xs)                  ↝⟨ (λ hyp → from hyp hyp) ⟩
           □ i P ((x ∷ xs) ++ cycle x xs)  ↝⟨ (λ { (p ∷ ps) → p ∷ ps }) ⟩□
           □ i P (cycle x xs)              □
  }
  where
  to : ∀ {i} ys → □ i P (ys ++ cycle x xs) → □ i P ys
  to []       _        = []
  to (y ∷ ys) (p ∷ ps) = p ∷ λ { .force → to (force ys) (force ps) }

  from : ∀ {i ys} →
         □ i P (x ∷ xs) → □ i P ys → □ i P (ys ++ cycle x xs)
  from ps       (q ∷ qs) = q ∷ λ { .force → from ps (force qs) }
  from (p ∷ ps) []       = p ∷ λ { .force → from (p ∷ ps) (force ps) }

------------------------------------------------------------------------
-- A variant of ◇ with a sized predicate

-- ◇ˢ ∞ P xs means that (some instance of) P holds for some element in
-- xs.

data ◇ˢ {a p} {A : Set a} (i : Size)
        (P : Size → A → Set p) : Colist A ∞ → Set (a ⊔ p) where
  here  : ∀ {x xs} → P i x → ◇ˢ i P (x ∷ xs)
  there : ∀ {x xs} {j : Size< i} → ◇ˢ j P (force xs) → ◇ˢ i P (x ∷ xs)

-- ◇ˢ respects bisimilarity.

◇ˢ-∼ :
  ∀ {a p i} {A : Set a} {P : Size → A → Set p} {xs ys} →
  [ ∞ ] xs ∼ ys → ◇ˢ i P xs → ◇ˢ i P ys
◇ˢ-∼ (refl ∷ _) (here p)  = here p
◇ˢ-∼ (_    ∷ b) (there p) = there (◇ˢ-∼ (force b) p)

-- If P is upwards closed, then flip ◇ˢ P is upwards closed.

◇ˢ-upwards-closed :
  ∀ {a p} {A : Set a} {P : Size → A → Set p} →
  (∀ {i} {j : Size< i} {x} → P j x → P i x) →
  (∀ {i} {j : Size< i} {xs} → ◇ˢ j P xs → ◇ˢ i P xs)
◇ˢ-upwards-closed P-closed (here p)  = here (P-closed p)
◇ˢ-upwards-closed P-closed (there p) =
  there (◇ˢ-upwards-closed P-closed p)

-- A variant of the previous lemma.

◇ˢ-upwards-closed-∞ :
  ∀ {a p} {A : Set a} {P : Size → A → Set p} →
  (∀ {i x} → P i x → P ∞ x) →
  (∀ {i xs} → ◇ˢ i P xs → ◇ˢ ∞ P xs)
◇ˢ-upwards-closed-∞ P-closed-∞ (here p)  = here (P-closed-∞ p)
◇ˢ-upwards-closed-∞ P-closed-∞ (there p) =
  there (◇ˢ-upwards-closed-∞ P-closed-∞ p)

-- A map function for ◇ˢ.

◇ˢ-map : ∀ {a p q i}
           {A : Set a} {P : Size → A → Set p} {Q : Size → A → Set q} →
         (∀ {i x} → P i x → Q i x) →
         (∀ {xs} → ◇ˢ i P xs → ◇ˢ i Q xs)
◇ˢ-map f (here p)  = here (f p)
◇ˢ-map f (there p) = there (◇ˢ-map f p)

-- A variant of ◇ˢ-map.

◇ˢ-map′ : ∀ {a b c p q i} {A : Set a} {B : Set b} {C : Set c}
            {P : Size → B → Set p} {Q : Size → C → Set q}
            {f : A → B} {g : A → C} →
          (∀ {i x} → P i (f x) → Q i (g x)) →
          (∀ {xs} → ◇ˢ i P (map f xs) → ◇ˢ i Q (map g xs))
◇ˢ-map′ g {_ ∷ _} (here p)  = here (g p)
◇ˢ-map′ g {_ ∷ _} (there p) = there (◇ˢ-map′ g p)
◇ˢ-map′ g {[]}    ()

-- If a predicate holds for some element in a colist, then it holds
-- for some value (assuming that P is upwards closed).

◇ˢ-witness : ∀ {a p i} {A : Set a} {P : Size → A → Set p} {xs} →
             (∀ {i} {j : Size< i} {x} → P j x → P i x) →
             ◇ˢ i P xs → ∃ (P i)
◇ˢ-witness closed (here p)  = _ , p
◇ˢ-witness closed (there p) = Σ-map id closed (◇ˢ-witness closed p)

-- If P ∞ holds for some element in xs, then ◇ˢ ∞ P xs holds.

∈×∞→◇ˢ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {x xs} →
         [ ∞ ] x ∈ xs → P ∞ x → ◇ˢ ∞ P xs
∈×∞→◇ˢ (here refl)  p = here p
∈×∞→◇ˢ (there x∈xs) p = there (∈×∞→◇ˢ x∈xs p)

-- If P i x implies P ∞ x for any i and x, then ◇ˢ ∞ P xs holds iff
-- P ∞ holds for some element in xs.

◇ˢ⇔∈× : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
        (∀ {i x} → P i x → P ∞ x) →
        ◇ˢ ∞ P xs ⇔ (∃ λ x → [ ∞ ] x ∈ xs × P ∞ x)
◇ˢ⇔∈× {P = P} →∞ = record
  { to   = to
  ; from = λ { (_ , x∈xs , p) → ∈×∞→◇ˢ x∈xs p }
  }
  where
  to : ∀ {i xs} → ◇ˢ i P xs → ∃ λ x → [ ∞ ] x ∈ xs × P ∞ x
  to (here p)  = _ , here refl , →∞ p
  to (there p) = Σ-map id (Σ-map there id) (to p)

-- Sized variants of the previous lemma.

◇ˢ→∈× : ∀ {a p} {A : Set a} {P : Size → A → Set p} →
        (∀ {i} {j : Size< i} {x} → P j x → P i x) →
        ∀ {i xs} → ◇ˢ i P xs → ∃ λ x → [ i ] x ∈ xs × P i x
◇ˢ→∈× closed (here p)  = _ , here refl , p
◇ˢ→∈× closed (there p) = Σ-map id (Σ-map there closed) (◇ˢ→∈× closed p)

∈×→◇ˢ : ∀ {a p} {A : Set a} {P : Size → A → Set p} →
        (∀ {i} {j : Size< i} {x} → P i x → P j x) →
        ∀ {i x xs} → [ i ] x ∈ xs → P i x → ◇ˢ i P xs
∈×→◇ˢ closed (here refl)  p = here p
∈×→◇ˢ closed (there x∈xs) p = there (∈×→◇ˢ closed x∈xs (closed p))

-- ◇ ∞ (P ∞) is "contained in" ◇ˢ ∞ P.

◇∞→◇ˢ∞ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
         ◇ ∞ (P ∞) xs → ◇ˢ ∞ P xs
◇∞→◇ˢ∞ {P = P} {xs} =
  ◇ ∞ (P ∞) xs                    ↝⟨ _⇔_.to ◇⇔∈× ⟩
  (∃ λ x → [ ∞ ] x ∈ xs × P ∞ x)  ↝⟨ (λ { (_ , x∈xs , p) → ∈×∞→◇ˢ x∈xs p }) ⟩□
  ◇ˢ ∞ P xs                       □

-- If P i x implies P ∞ x for any i and x, then ◇ˢ ∞ P is pointwise
-- logically equivalent to ◇ ∞ (P ∞).

◇ˢ∞⇔◇∞ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
         (∀ {i x} → P i x → P ∞ x) →
         ◇ˢ ∞ P xs ⇔ ◇ ∞ (P ∞) xs
◇ˢ∞⇔◇∞ {P = P} {xs} →∞ =
  ◇ˢ ∞ P xs                       ↝⟨ ◇ˢ⇔∈× →∞ ⟩
  (∃ λ x → [ ∞ ] x ∈ xs × P ∞ x)  ↝⟨ inverse ◇⇔∈× ⟩□
  ◇ ∞ (P ∞) xs                    □

-- ◇ˢ i (const P) is pointwise logically equivalent to ◇ i P.

◇ˢ⇔◇ : ∀ {a p i} {A : Set a} {P : A → Set p} {xs} →
       ◇ˢ i (const P) xs ⇔ ◇ i P xs
◇ˢ⇔◇ {P = P} {xs} = record { to = to; from = from }
  where
  to : ∀ {i xs} → ◇ˢ i (const P) xs → ◇ i P xs
  to (here p)  = here p
  to (there p) = there (to p)

  from : ∀ {i xs} → ◇ i P xs → ◇ˢ i (const P) xs
  from (here p)  = here p
  from (there p) = there (from p)

-- If ◇ˢ i P (x ∷ xs) holds, then ◇ˢ i P (cycle x xs) also holds.

◇ˢ-cycle← :
  ∀ {a p i} {A : Set a} {P : Size → A → Set p} {x : A} {xs} →
  ◇ˢ i P (x ∷ xs) → ◇ˢ i P (cycle x xs)
◇ˢ-cycle← {i = i} {P = P} {x} {xs} =
  ◇ˢ i P (x ∷ xs)                  ↝⟨ from ⟩
  ◇ˢ i P ((x ∷ xs) ++ cycle x xs)  ↝⟨ ◇ˢ-∼ (transitive-∼ ∷∼∷′ (symmetric-∼ ∷∼∷′)) ⟩□
  ◇ˢ i P (cycle x xs)              □
  where
  from : ∀ {i ys} → ◇ˢ i P ys → ◇ˢ i P (ys ++ cycle x xs)
  from (here p)   = here p
  from (there ps) = there (from ps)

-- If P i x implies P ∞ x for any i and x, then ◇ˢ ∞ P (cycle x xs) is
-- logically equivalent to ◇ˢ ∞ P (x ∷ xs).

◇ˢ-cycle⇔ :
  ∀ {a p} {A : Set a} {P : Size → A → Set p} {x : A} {xs} →
  (∀ {i x} → P i x → P ∞ x) →
  ◇ˢ ∞ P (cycle x xs) ⇔ ◇ˢ ∞ P (x ∷ xs)
◇ˢ-cycle⇔ {P = P} {x} {xs} →∞ = record
  { to   = ◇ˢ ∞ P (cycle x xs)                ↝⟨ ◇ˢ-∼ (transitive-∼ ∷∼∷′ (symmetric-∼ ∷∼∷′)) ⟩
           ◇ˢ ∞ P ((x ∷ xs) ++ cycle x xs)    ↝⟨ to _ ⟩
           ◇ˢ ∞ P (x ∷ xs) ⊎ ◇ˢ ∞ P (x ∷ xs)  ↝⟨ [ id , id ] ⟩□
           ◇ˢ ∞ P (x ∷ xs)                    □
  ; from = ◇ˢ-cycle←
  }
  where
  to :
    ∀ {i} ys → ◇ˢ i P (ys ++ cycle x xs) → ◇ˢ ∞ P ys ⊎ ◇ˢ ∞ P (x ∷ xs)
  to []       (here p)  = inj₂ (here (→∞ p))
  to []       (there p) = case to (force xs) p of
                            [ inj₂ ∘ there , inj₂ ]
  to (y ∷ ys) (here p)  = inj₁ (here (→∞ p))
  to (y ∷ ys) (there p) = ⊎-map there id (to (force ys) p)

------------------------------------------------------------------------
-- A variant of □ with a sized predicate

-- □ˢ ∞ P xs means that (some instance of) P holds for every element
-- in xs.

mutual

  data □ˢ {a p} {A : Set a} (i : Size)
          (P : Size → A → Set p) : Colist A ∞ → Set (a ⊔ p) where
    []  : □ˢ i P []
    _∷_ : ∀ {x xs} → P i x → □ˢ′ i P (force xs) → □ˢ i P (x ∷ xs)

  record □ˢ′ {a p} {A : Set a} (i : Size)
             (P : Size → A → Set p) (xs : Colist A ∞) : Set (a ⊔ p) where
    coinductive
    field
      force : {j : Size< i} → □ˢ j P xs

open □ˢ′ public

-- Some projections.

□ˢ-head : ∀ {a p i} {A : Set a} {P : Size → A → Set p} {x xs} →
          □ˢ i P (x ∷ xs) → P i x
□ˢ-head (p ∷ _) = p

□ˢ-tail : ∀ {a p i} {j : Size< i}
            {A : Set a} {P : Size → A → Set p} {x xs} →
          □ˢ i P (x ∷ xs) → □ˢ j P (force xs)
□ˢ-tail (_ ∷ ps) = force ps

-- □ˢ respects bisimilarity.

□ˢ-∼ :
  ∀ {i a p} {A : Set a} {P : Size → A → Set p} {xs ys} →
  [ i ] xs ∼ ys → □ˢ i P xs → □ˢ i P ys
□ˢ-∼ []         _        = []
□ˢ-∼ (refl ∷ b) (p ∷ ps) = p ∷ λ { .force → □ˢ-∼ (force b) (force ps) }

-- If P is downwards closed, then flip □ˢ P is downwards closed.

□ˢ-downwards-closed :
  ∀ {a p} {A : Set a} {P : Size → A → Set p} →
  (∀ {i} {j : Size< i} {x} → P i x → P j x) →
  (∀ {i} {j : Size< i} {xs} → □ˢ i P xs → □ˢ j P xs)
□ˢ-downwards-closed P-closed []       = []
□ˢ-downwards-closed P-closed (p ∷ ps) =
  P-closed p ∷ λ { .force → □ˢ-downwards-closed P-closed (force ps) }

-- A variant of the previous lemma.

□ˢ-downwards-closed-∞ :
  ∀ {a p} {A : Set a} {P : Size → A → Set p} →
  (∀ {i x} → P ∞ x → P i x) →
  (∀ {i xs} → □ˢ ∞ P xs → □ˢ i P xs)
□ˢ-downwards-closed-∞ P-closed-∞ []       = []
□ˢ-downwards-closed-∞ P-closed-∞ (p ∷ ps) =
  P-closed-∞ p ∷ λ { .force →
  □ˢ-downwards-closed-∞ P-closed-∞ (force ps) }

-- If □ˢ ∞ P xs holds, then P ∞ holds for every element in xs.

□ˢ∞∈→ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs x} →
        □ˢ ∞ P xs → [ ∞ ] x ∈ xs → P ∞ x
□ˢ∞∈→ (p ∷ ps) (here refl)  = p
□ˢ∞∈→ (p ∷ ps) (there x∈xs) = □ˢ∞∈→ (force ps) x∈xs

-- If P ∞ x implies P i x for any i and x, then □ˢ ∞ P xs holds iff P ∞
-- holds for every element in xs.

□ˢ⇔∈→ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
        (∀ {i x} → P ∞ x → P i x) →
        □ˢ ∞ P xs ⇔ (∀ x → [ ∞ ] x ∈ xs → P ∞ x)
□ˢ⇔∈→ {P = P} ∞→ = record { to = λ p _ → □ˢ∞∈→ p; from = from _ }
  where
  from : ∀ {i} xs → (∀ x → [ ∞ ] x ∈ xs → P ∞ x) → □ˢ i P xs
  from []       f = []
  from (x ∷ xs) f =
    ∞→ (f x (here refl)) ∷ λ { .force →
    from (force xs) (λ x → f x ∘ there) }

-- Sized variants of the previous lemma.

□ˢ∈→ : ∀ {a p} {A : Set a} {P : Size → A → Set p} →
       (∀ {i} {j : Size< i} {x} → P j x → P i x) →
       ∀ {i x xs} → □ˢ i P xs → [ i ] x ∈ xs → P i x
□ˢ∈→ closed (p ∷ ps) (here refl)  = p
□ˢ∈→ closed (p ∷ ps) (there x∈xs) = closed (□ˢ∈→ closed (force ps) x∈xs)

∈→→□ˢ : ∀ {a p} {A : Set a} {P : Size → A → Set p} →
        (∀ {i} {j : Size< i} {x} → P i x → P j x) →
        ∀ {i} xs → (∀ x → [ i ] x ∈ xs → P i x) → □ˢ i P xs
∈→→□ˢ closed []       f = []
∈→→□ˢ closed (x ∷ xs) f =
  f x (here refl) ∷ λ { .force →
  ∈→→□ˢ closed (force xs) (λ x → closed ∘ f x ∘ there) }

-- □ˢ ∞ P is "contained in" □ ∞ (P ∞).

□ˢ∞→□∞ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
         □ˢ ∞ P xs → □ ∞ (P ∞) xs
□ˢ∞→□∞ {P = P} {xs} =
  □ˢ ∞ P xs                     ↝⟨ (λ p _ → □ˢ∞∈→ p) ⟩
  (∀ x → [ ∞ ] x ∈ xs → P ∞ x)  ↝⟨ _⇔_.from □⇔∈→ ⟩□
  □ ∞ (P ∞) xs                  □

-- If P ∞ x implies P i x for any i and x, then □ˢ ∞ P is pointwise
-- logically equivalent to □ ∞ (P ∞).

□ˢ∞⇔□∞ : ∀ {a p} {A : Set a} {P : Size → A → Set p} {xs} →
         (∀ {i x} → P ∞ x → P i x) →
         □ˢ ∞ P xs ⇔ □ ∞ (P ∞) xs
□ˢ∞⇔□∞ {P = P} {xs} ∞→ =
  □ˢ ∞ P xs                     ↝⟨ □ˢ⇔∈→ ∞→ ⟩
  (∀ x → [ ∞ ] x ∈ xs → P ∞ x)  ↝⟨ inverse □⇔∈→ ⟩□
  □ ∞ (P ∞) xs                  □

-- □ˢ i (const P) is pointwise logically equivalent to □ i P.

□ˢ⇔□ : ∀ {a p i} {A : Set a} {P : A → Set p} {xs} →
       □ˢ i (const P) xs ⇔ □ i P xs
□ˢ⇔□ {P = P} {xs} = record { to = to; from = from }
  where
  to : ∀ {i xs} → □ˢ i (const P) xs → □ i P xs
  to []       = []
  to (p ∷ ps) = p ∷ λ { .force → to (force ps) }

  from : ∀ {i xs} → □ i P xs → □ˢ i (const P) xs
  from []       = []
  from (p ∷ ps) = p ∷ λ { .force → from (force ps) }

-- If P is universally true, then □ˢ i P is also universally true.

□ˢ-replicate : ∀ {a p i} {A : Set a} {P : Size → A → Set p} →
               (∀ {i} x → P i x) →
               (∀ xs → □ˢ i P xs)
□ˢ-replicate f []       = []
□ˢ-replicate f (x ∷ xs) = f x ∷ λ { .force → □ˢ-replicate f (force xs) }

-- Something resembling applicative functor application for □ˢ.

infixl  _□ˢ-⊛_

_□ˢ-⊛_ : ∀ {i a p q} {A : Set a}
           {P : Size → A → Set p} {Q : Size → A → Set q} {xs} →
         □ˢ i (λ j x → P j x → Q j x) xs → □ˢ i P xs → □ˢ i Q xs
[]       □ˢ-⊛ _        = []
(f ∷ fs) □ˢ-⊛ (p ∷ ps) = f p ∷ λ { .force → force fs □ˢ-⊛ force ps }

-- A map function for □ˢ.

□ˢ-map : ∀ {a p q i}
           {A : Set a} {P : Size → A → Set p} {Q : Size → A → Set q} →
         (∀ {i x} → P i x → Q i x) →
         (∀ {xs} → □ˢ i P xs → □ˢ i Q xs)
□ˢ-map f ps = □ˢ-replicate (λ _ → f) _ □ˢ-⊛ ps

-- A variant of □ˢ-map.

□ˢ-map′ : ∀ {a b c p q i} {A : Set a} {B : Set b} {C : Set c}
            {P : Size → B → Set p} {Q : Size → C → Set q}
            {f : A → B} {g : A → C} →
          (∀ {i x} → P i (f x) → Q i (g x)) →
          (∀ {xs} → □ˢ i P (map f xs) → □ˢ i Q (map g xs))
□ˢ-map′ g {[]}    []       = []
□ˢ-map′ g {_ ∷ _} (p ∷ ps) = g p ∷ λ { .force → □ˢ-map′ g (force ps) }

-- Something resembling applicative functor application for □ˢ and ◇ˢ.

infixl  _□ˢ◇ˢ-⊛_

_□ˢ◇ˢ-⊛_ : ∀ {a p q i} {A : Set a}
             {P : Size → A → Set p} {Q : Size → A → Set q} {xs} →
           □ˢ i (λ j x → P j x → Q j x) xs → ◇ˢ i P xs → ◇ˢ i Q xs
(f ∷ _)  □ˢ◇ˢ-⊛ (here p)  = here (f p)
(_ ∷ fs) □ˢ◇ˢ-⊛ (there p) = there (force fs □ˢ◇ˢ-⊛ p)

-- A combination of some of the combinators above.

□ˢ◇ˢ-witness :
  ∀ {a p q i}
    {A : Set a} {P : Size → A → Set p} {Q : Size → A → Set q} {xs} →
  (∀ {i} {j : Size< i} {x} → P j x → P i x) →
  (∀ {i} {j : Size< i} {x} → Q j x → Q i x) →
  □ˢ i P xs → ◇ˢ i Q xs → ∃ λ x → P i x × Q i x
□ˢ◇ˢ-witness P-closed Q-closed p q =
  ◇ˢ-witness (λ { {_} {_} → Σ-map P-closed Q-closed })
             (□ˢ-map _,_ p □ˢ◇ˢ-⊛ q)

-- If □ˢ i P (cycle x xs) holds, then □ˢ i P (x ∷ xs) also holds.

□ˢ-cycle→ :
  ∀ {a p i} {A : Set a} {P : Size → A → Set p} {x : A} {xs} →
  □ˢ i P (cycle x xs) → □ˢ i P (x ∷ xs)
□ˢ-cycle→ {i = i} {P = P} {x} {xs} =
  □ˢ i P (cycle x xs)              ↝⟨ (λ { (p ∷ ps) → p ∷ ps }) ⟩
  □ˢ i P ((x ∷ xs) ++ cycle x xs)  ↝⟨ to _ ⟩□
  □ˢ i P (x ∷ xs)                  □
  where
  to : ∀ {i} ys → □ˢ i P (ys ++ cycle x xs) → □ˢ i P ys
  to []       _        = []
  to (y ∷ ys) (p ∷ ps) = p ∷ λ { .force → to (force ys) (force ps) }

-- If P ∞ x implies P i x for any i and x, then □ˢ ∞ P (cycle x xs) is
-- logically equivalent to □ˢ ∞ P (x ∷ xs).

□ˢ-cycle⇔ :
  ∀ {a p} {A : Set a} {P : Size → A → Set p} {x : A} {xs} →
  (∀ {i x} → P ∞ x → P i x) →
  □ˢ ∞ P (cycle x xs) ⇔ □ˢ ∞ P (x ∷ xs)
□ˢ-cycle⇔ {P = P} {x} {xs} ∞→ = record
  { to   = □ˢ-cycle→
  ; from = □ˢ ∞ P (x ∷ xs)                  ↝⟨ (λ hyp → from hyp hyp) ⟩
           □ˢ ∞ P ((x ∷ xs) ++ cycle x xs)  ↝⟨ (λ { (p ∷ ps) → p ∷ ps }) ⟩□
           □ˢ ∞ P (cycle x xs)              □
  }
  where
  from : ∀ {i ys} →
         □ˢ ∞ P (x ∷ xs) → □ˢ i P ys → □ˢ i P (ys ++ cycle x xs)
  from ps       (q ∷ qs) = q ∷ λ { .force → from ps (force qs) }
  from (p ∷ ps) []       = ∞→ p ∷ λ { .force →
                           from (p ∷ ps) (force ps) }