Codata.streamBisim

-- Observational equality, restated CORECURSIVELY: two streams are
-- bisimilar iff SOME relation relates them, agrees on heads, and is
-- preserved by tails — the union of all post-fixed points of the
-- one-observation-step operator, i.e. the greatest fixed point by
-- Knaster–Tarski, landed in Ω by impredicative squash (the dual of
-- Foundation's least-relations-by-intersection note). The
-- coinduction principle is DEFINITIONAL here: to prove bisim s t,
-- exhibit an invariant and its one-step closure — no ℕ index
-- anywhere. Below: intro/unfold laws, a direct corecursive proof
-- (reflexivity via the equality invariant), and equivalence with the
-- ℕ-indexed obsEq.

import Core.prelude (id, ∘)
import Core.equality (cong)
import Codata.stream (stream, hd, tl, map)
import Codata.streamEq (tlN, nth, obsEq, obsEqRefl, nthMap, mapIdObsEq, mapFuseObsEq)

bisim : {a : 𝕌} → stream a → stream a → Ω
bisim =
  λa s t. ∥(r : stream a → stream a → Ω)
    × ((x y : stream a) → r x y → (hd x ≡ hd y) × r (tl x) (tl y)) × r s t∥

-- UNFOLD, head half: bisimilar streams agree at the head
bisimHd : {a : 𝕌} {s t : stream a} → bisim s t → hd s ≡ hd t using (Codata.streamBisim.bisim.unfold)
bisimHd = λa s t h. squash-elim h (w. w .π₂ .π₁ s t (w .π₂ .π₂) .π₁)

-- UNFOLD, tail half: bisimilarity is preserved by observation —
-- the SAME invariant relates the tails
bisimTl : {a : 𝕌} {s t : stream a} → bisim s t → bisim (tl s) (tl t)
  using (Codata.streamBisim.bisim.unfold)
bisimTl = λa s t h. squash-elim h (w. ⋆ (w .π₁, w .π₂ .π₁, w .π₂ .π₁ s t (w .π₂ .π₂) .π₂))

-- a DIRECT corecursive proof: reflexivity, with judgemental equality
-- itself as the invariant — heads by cong at hd, tails by cong at tl
bisimRefl : {a : 𝕌} (s : stream a) → bisim s s using (Codata.streamBisim.bisim.unfold)
bisimRefl =
  λa s. ⋆
    (λx y. x ≡ y), (λx y p. cong (λv. a) (λv. hd {} a v) p, cong (λv. stream a) (λv. tl v) p), ⋆

-- obsEq ⊃ bisim: the ℕ-indexed relation is ITSELF a bisimulation —
-- heads are observation 0, and shifting the index moves under one
-- tail (nth n (tl x) ≐ nth (S n) x, judgementally)
obsEqBisim : {a : 𝕌} {s t : stream a} → obsEq s t → bisim s t
  using (Codata.stream.hd.eq,
    Codata.stream.stream.unfold,
    Codata.stream.tl.eq,
    Codata.streamBisim.bisim.unfold,
    Codata.streamEq.nth.eq,
    Codata.streamEq.obsEq.unfold,
    Codata.streamEq.tlN.eq)
obsEqBisim =
  λa s t h. ⋆
    (λx y. obsEq x y), (λx y p. squash-elim p (w. w Z), squash-elim p (w. ⋆ (λn. w (S n)))), h

-- bisim ⊃ obsEq: unfold n times, by ℕ-induction over the depth
bisimObsEq : {a : 𝕌} {s t : stream a} → bisim s t → obsEq s t
  using (Codata.stream.hd.eq,
    Codata.stream.stream.unfold,
    Codata.stream.tl.eq,
    Codata.streamBisim.bisim.unfold,
    Codata.streamEq.nth.eq,
    Codata.streamEq.obsEq.unfold,
    Codata.streamEq.tlN.eq)
bisimObsEq =
  λa s t h. ⋆
    λn. ℕ-elim
      m. (x y : stream a) → bisim x y → nth m x ≡ nth m y
      λx y g. bisimHd g
      m ih. λx y g. ih (tl x) (tl y) (bisimTl g)
      n
      s
      t
      h

-- interop corollary: map-identity, now in the corecursive spelling
mapIdBisim : {a : 𝕌} (s : stream a) → bisim (map (id {a}) s) s
  using (Codata.streamBisim.bisim.unfold, Core.prelude.id.eq)
mapIdBisim = λa s. obsEqBisim (mapIdObsEq s)

-- THE REFLECTION: bisimilarity implies equality — el-nu-coind's
-- surface form, with bisim ITSELF as the invariant and the unfold
-- laws as the one-step closure. This is the theorem that upgrades
-- every observational result below it to a judgemental equation.
bisimReflect : {a : 𝕌} {s t : stream a} → bisim s t → s ≡ t
  using (bisim.eq,
    hyp.rw,
    Codata.stream.hd.eq,
    Codata.stream.stream.eq,
    Codata.stream.stream.unfold,
    Codata.stream.tl.eq,
    Codata.streamBisim.bisim.unfold)
bisimReflect = λa s t h. coind (x y. bisim x y) h (x y hb. ⋆ (bisimHd hb, bisimTl hb))

obsEqReflect : {a : 𝕌} {s t : stream a} → obsEq s t → s ≡ t
obsEqReflect = λa s t h. bisimReflect (obsEqBisim h)

-- the η-needing equalities, now judgemental theorems
mapIdEq : (a : 𝕌) (s : stream a) → map (id {a}) s ≡ s using (Core.prelude.id.eq)
mapIdEq = λa s. bisimReflect (mapIdBisim s)

mapFuseEq : (a b c : 𝕌) (f : a → b) (g : b → c) (s : stream a) → map g (map f s) ≡ map (g ∘ f) s
mapFuseEq = λa b c f g s. obsEqReflect (mapFuseObsEq f g s)