streamBisim

import equality (cong)
import stream (stream, hd, tl, mapS)
import streamEq (tlN, nth, obsEq, obsEqRefl, nthMap, mapIdObsEq, mapFuseObsEq)

-- 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.

def bisim : (a : 𝕌) → El (stream a) → El (stream a) → Ω ≔
  λa. λs. λt.
    ∥(r : El (stream a) → El (stream a) → Ω) ⨯
      ((x : El (stream a)) (y : El (stream a)) → Prf (r x y) →
         Prf (hd _ x ≡ hd _ y ∈ El a) ⨯ Prf (r (tl _ x) (tl _ y))) ⨯
      Prf (r s t)∥

-- UNFOLD, head half: bisimilar streams agree at the head
def bisimHd : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) →
    Prf (bisim _ s t) → Prf (hd _ s ≡ hd _ t ∈ El a) ≔
  λ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
def bisimTl : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) →
    Prf (bisim _ s t) → Prf (bisim _ (tl _ s) (tl _ t)) ≔
  λ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
def bisimRefl : (a : 𝕌) (s : El (stream a)) → Prf (bisim _ s s) ≔
  λa. λs.
    ⋆ (((λx. λy. (x ≡ y ∈ El (stream a))) ,
       ((λx. λy. λp. (cong _ (λv. a) (λv. hd _ v) x y p ,
                      cong _ (λv. stream a) (λv. tl _ v) x y 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)
def obsEqBisim : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) →
    Prf (obsEq _ s t) → Prf (bisim _ s t) ≔
  λ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
def bisimObsEq : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) →
    Prf (bisim _ s t) → Prf (obsEq _ s t) ≔
  λa. λs. λt. λh.
    ⋆ (λn. (ℕ-elim (m. (x : El (stream a)) → (y : El (stream a)) →
                Prf (bisim _ x y) → Prf (nth _ m x ≡ nth _ m y ∈ El a))
          (λx. λy. λg. bisimHd _ x y g)
          (m ih. λx. λy. λg. ih (tl _ x) (tl _ y) (bisimTl _ x y g))
          n) s t h)

-- interop corollary: map-identity, now in the corecursive spelling
def mapIdBisim : (a : 𝕌) (s : El (stream a)) →
    Prf (bisim _ (mapS _ _ (λx. x) s) s) ≔
  λ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.
def bisimReflect : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) →
    Prf (bisim _ s t) → Prf (s ≡ t ∈ El (stream a)) ≔
  λa. λs. λt. λh.
    coind (x y. bisim _ x y) h
          (x y hb. ⋆ ((bisimHd _ x y hb , bisimTl _ x y hb)))

def obsEqReflect : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) →
    Prf (obsEq _ s t) → Prf (s ≡ t ∈ El (stream a)) ≔
  λa. λs. λt. λh. bisimReflect _ s t (obsEqBisim _ s t h)

-- the η-needing equalities, now judgemental theorems
def mapIdEq : (a : 𝕌) (s : El (stream a)) →
    mapS _ _ (λx. x) s ≡ s ∈ El (stream a) ≔
  λa. λs. bisimReflect _ _ _ (mapIdBisim _ s)

def mapFuseEq : (a : 𝕌) (b : 𝕌) (c : 𝕌) (f : El a → El b) (g : El b → El c)
    (s : El (stream a)) →
    mapS _ _ g (mapS _ _ f s) ≡ mapS _ _ (λx. g (f x)) s ∈ El (stream c) ≔
  λa. λb. λc. λf. λg. λs.
    obsEqReflect _ _ _ (mapFuseObsEq _ _ _ f g s)