Bisimulation proof in Agda with copatterns

Bisim.agda

-- Inspired by http://www.cse.chalmers.se/research/group/logic/AIM/AIM6/SetzerCoInduction.pdf
{-# OPTIONS --copatterns #-}
module Bisim where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : ∀ {n} → A → Vec A n → Vec A (succ n) 

data _≡_ {A : Set} (a : A) : A → Set where 
  reflexive : a ≡ a

record Stream (A : Set) : Set where
  coinductive
  constructor _∷_ 
  field
    head : A
    tail : Stream A

open Stream

take : ∀ {n A} → Stream A → Vec A n
take {zero} s = []
take {succ n} s = head s ∷ take {n} (tail s)

ones : Stream ℕ
head ones = 1
tail ones = ones

ssucc : Stream ℕ → Stream ℕ
head (ssucc s) = succ (head s)
tail (ssucc s) = ssucc (tail s)

twos : Stream ℕ
head twos = 2
tail twos = twos

record Bisim {A : Set} (s s' : Stream A) : Set where
  coinductive
  constructor _∷_
  field
    phead : head s ≡ head s'
    ptail : Bisim (tail s) (tail s')
open Bisim

Bisim-ssucc⋆ones-twos : Bisim (ssucc ones) twos
phead Bisim-ssucc⋆ones-twos = reflexive
ptail Bisim-ssucc⋆ones-twos = Bisim-ssucc⋆ones-twos

postulate bisim-eq : ∀ {A} {s s' : Stream A} → Bisim s s' → s ≡ s'

succ⋆ones≡twos : ssucc ones ≡ twos 
succ⋆ones≡twos = bisim-eq Bisim-ssucc⋆ones-twos