\subsection{Streams and Bisimilarity}
\label{sec:appl:streams}

\AgdaHide{
\begin{code}
{-# OPTIONS --without-K #-}
\end{code}
}

To define the substream relation, we first need to introduce streams.
We have done this already in the simple type system in \exRef{basic-types}
but to have a complete example, we recast the definition of streams here
again in Agda.
This allows us to also explain the syntax of Agda's coinductive types.
Moreover, we will introduce bisimilarity on streams as a coinductively
defined relation and prove that it is an equivalence relation.
\begin{code}
module Stream where
\end{code}

\AgdaHide{
\begin{code}
open import Level as Level using (zero)
import Relation.Binary as BinRel
open import Relation.Binary as BinRel hiding (Setoid; Rel)

Setoid = BinRel.Setoid Level.zero Level.zero
Rel : Set → Set₁
Rel A = BinRel.Rel A Level.zero
\end{code}
}

Before we come to the actual definitions, we import a few modules
that we use throughout this section.
The module \AgdaModule{Relation.Binary} contains definitions surrounding binary
relations.
In particular, we can write R : \AgdaFunction{Rel} \AgdaBound{A} to express
that R is a type with two parameters of type A, that is, if
R is of type A \AgdaSymbol{→} A \AgdaSymbol{→} \AgdaPrimitiveType{Set}.
We will later show that bisimilarity of streams implies point-wise equality.
Since point-wise equality is defined in terms of indexing into streams by
natural numbers, we also need to import the module \AgdaModule{Data.Nat}.
Finally, the module \AgdaModule{PropsAsTypes} was given in
\secRef{appl:agda-preliminaries} above.
\begin{code}
import Relation.Binary as BinRel

open import Data.Nat using (ℕ; zero; suc)
open import PropsAsTypes
\end{code}

Let us now come to the definition of streams and their corresponding coiteration
principle.
The following coinductive record type corresponds to what we have called
so far codata types.
Thus, instead of
\begin{lstlisting}
codata Stream (A : Set) : Set where
  hd : A
  tl : Stream A
\end{lstlisting}
the type of streams is given in Agda by the following record type.
\begin{code}
record Stream (A : Set) : Set where
  coinductive
  field
    hd  : A
    tl  : Stream A
\end{code}

A record type in Agda is a type that is defined by its destructors, which
are called fields in Agda.
If a record is recursive, that is, it uses itself in its own definition,
then we need to specify whether it this recursion is to be interpreted
inductively or coinductively.
Since we never encounter inductive record types here, we stick to the
codata terminology.
The reader should thus just replace the verbose coinductive record syntax
in her head by the simpler codata syntax.

\AgdaHide{
\begin{code}
open Stream public
\end{code}
}

The coiteration principle for streams is given in Agda by the following
equational specification.
\begin{code}
coiter : {X A : Set} → (X → A × X) → (X → Stream A)
coiter c x .hd  = π₁ (c x)
coiter c x .tl  = coiter c (π₂ (c x))
\end{code}

Note that we define the coiteration principle in terms of copattern
equations, which are the same as in the calculus $\CopatCalc$.
Agda ensures that this definition is well-formed by performing covering and
guardedness checks.\endnote{%
  Agda also supports more sophisticated
  termination checks by using sized types.
  We will not discuss these further here though.
}
These checks intuitively work for coinductive types as follows.
First, if we specify an element of a coinductive type, like for example a
stream, then we are required to specify the outcome of each destructor.
In the case of streams, we need to give both head and tail of a stream.
Second, the guardedness condition requires that the element we are specifying
does not occur in another term on the right-hand side of an equation.
This ensures that the result of a destructor application does not depend
on this very result itself, an instance of which we have seen in
\exRef{non-productive-term}.
Note that \AgdaFunction{coiter}, as given above, is thus well-defined because
it appears directly and in another term on the right-hand side of the equation
that specifies the tail.

It is possible, though very tedious, to translate all the following
equational specification into instances of iteration and coiteration schemes.
But this translation largely obscures the proof idea and so we refrain from
carrying it out.
However, we should also make clear that this translation from such Agda
specifications into the given calculus has the status of a conjecture for the
time being.
Some evidence that such a translation should be possible is given
by~\cite{Gimenez-RecursiveSchemes} and~\cite{Goguen06:EliminatingDepPattern}.

The following two functions are straightforward definitions of higher
derivatives of streams, that is, repeated applications of the tail destructor,
and indexing of stream positions by natural numbers.
Since we have seen such definitions before, we will not explain these
further here.
\begin{code}
δ : ∀{A} → ℕ → Stream A → Stream A
δ         s = s
δ (suc n)  s = δ n (s .tl)

_at_ : ∀{A} → Stream A → ℕ → A
s at n = (δ n s) .hd
\end{code}

We now come to the definition of bisimilarity for streams.
In \exRef{stream-bisimilarity}, we defined stream bisimilarity as a coinductive
relation in the category theoretical setup of recursive type closed categories.
The idea of that definition was that stream bisimilarity is given by two
destructors: one that extracts from a proof of bisimilarity a proof that the
heads of related streams are equivalent, and one that extracts a bisimilarity
proof for their tails.
To facilitate reuse, we define bisimilarity in terms of a so called
\term{setoid}, which is a set $A$ together with an equivalence relation
$\approx$ on it.
Such a pair is given by the term $S$ of type \AgdaDatatype{Setoid}.
To avoid further complications, we directly introduce names for the
carrier $A$ of the setoid, the relation $\approx$ and for the proof that
that $\approx$ is an equivalence relation.
\begin{code}
module Bisim (S : Setoid) where
  open BinRel.Setoid S
    renaming (Carrier to A; _≈_ to _≈_; isEquivalence to S-equiv)
\end{code}

\AgdaHide{
\begin{code}
  infix  _~_
\end{code}
}

Given such a setoid, let us now define bisimilarity for streams over $A$.
We define it as a binary relations that can be written in infix
notation.
This is signalled by the following declaration, which says that $\sim$ is
a relation with two positions (marked by the underscores).
The relation itself is then defined as a coinductive type in the expected way.
\begin{code}
  record _~_ (s t : Stream A) : Prop where
    coinductive
    field
      hd≈  : s .hd  ≈  t .hd
      tl~  : s .tl  ~  t .tl
\end{code}

\AgdaHide{
\begin{code}
  open _~_ public
\end{code}
}

Since bisimilarity is a coinductive type, it comes with a coiteration
principle.
This principle is, as we have explained in \exRef{stream-bisimilarity},
by the usual bisimulation proof (or coinduction) principle.
We briefly show how this principle can be derived from equational
specifications.
First, we define what it means for a relation $R$ to be a bisimulation on
streams.
This is witnessed by the following predicate on relations, which should
be intuitively clear: A relation $R$ is a bisimulation if for all streams
$s$ and $t$ that are related by $R$, their heads must be equivalent (in the
setoid A) and their tails must again be related by $R$.
\begin{code}
  isBisim : Rel (Stream A) → Prop
  isBisim _R_ = ∀ s t → s R t → (s .hd ≈ t .hd) ∧ (s .tl R t .tl)
\end{code}

Given this notion of bisimulation relation we can now derive the usual
proof principle:
\begin{code}
  ∃-bisim→~ :  ∀ {_R_} → isBisim _R_ →
               ∀ (s t : Stream A) → s R t → s ~ t
  ∃-bisim→~ R-isBisim s t q .hd≈  = ∧-elim₁ (R-isBisim s t q)
  ∃-bisim→~ R-isBisim s t q .tl~  =
    ∃-bisim→~ R-isBisim (s .tl) (t .tl) (∧-elim₂ (R-isBisim s t q))
\end{code}
Note the striking similarity to the coiteration principle for streams,
only that in this case we construct a bisimilarity proof rather than a
stream.
Let us briefly go through the types that appear in the definition
of \AgdaFunction{∃-bisim→~}.
First, we are given a binary relation $R$ and the following arguments.
\begin{align*}
  & \RisBisim : \AgdaFunction{isBisim} \> R \\
  & s, t : \AgdaFunction{Stream} \> \AgdaField{A} \\
  & q : s \mathrel{R} t
\end{align*}
To show that $s$ and $t$ are bisimilar, we need to provide now proofs that
their heads are equivalent and that the tails are related.
These are the two copattern cases of \AgdaFunction{∃-bisim→~}.
By the definition of \AgdaFunction{isBisim}, we have
\begin{equation*}
  \RisBisim \> s \> t :
    (s \phead \approx t \phead) \conj (s \ptail \mathrel{R} t \ptail).
\end{equation*}
Thus, the first conjunction elimination gives us the sought after proof
for the head case.
The tail case is given by recursively constructing a bisimilarity proof
for the tails from the second part of the above conjunction.
This should intuitively clarify how proofs of coinductive predicates
are given in Agda, and it should also highlight the similarity to the
definition of the coiteration principle for streams.

As a sanity check for the correctness of the definition of bisimilarity, we
prove that bisimilar streams are point-wise equivalent.

\begin{code}
  bisim→ext-≈ : ∀ {s t} → s ~ t → (∀ n → s at n ≈ t at n)
  bisim→ext-≈ p zero     = p .hd≈
  bisim→ext-≈ p (suc n)  = bisim→ext-≈ (p .tl~) n
\end{code}

We finish this section by showing that bisimilarity is an equivalence relation,
where we appeal to the fact that $\approx$ is an equivalence relation.
This allows us to show that streams form a setoid with bisimilarity as
equivalence relation on them.
These proofs should speak for themselves, thus we will not go through them
in detail.
\begin{code}
  module SE = IsEquivalence S-equiv

  s-bisim-refl : ∀ {s : Stream A} → s ~ s
  s-bisim-refl      .hd≈  = SE.refl
  s-bisim-refl {s}  .tl~  = s-bisim-refl {s .tl}

  s-bisim-sym : ∀ {s t : Stream A} → s ~ t → t ~ s
  s-bisim-sym p .hd≈  = SE.sym       (p .hd≈)
  s-bisim-sym p .tl~  = s-bisim-sym  (p .tl~)

  s-bisim-trans : ∀ {r s t : Stream A} → r ~ s → s ~ t → r ~ t
  s-bisim-trans p q .hd≈  = SE.trans       (p .hd≈)  (q .hd≈)
  s-bisim-trans p q .tl~  = s-bisim-trans  (p .tl~)  (q .tl~)

  stream-setoid : Setoid
  stream-setoid = record
    { Carrier = Stream A
    ; _≈_ = _~_
    ; isEquivalence = record
      { refl   = s-bisim-refl
      ; sym    = s-bisim-sym
      ; trans  = s-bisim-trans
      }
    }

\end{code}

\AgdaHide{
\begin{code}
  import Relation.Binary.EqReasoning as EqR

  module ~-Reasoning where
    module _ where
      open EqR (stream-setoid) public
        hiding (_≡⟨_⟩_) renaming (_≈⟨_⟩_ to _~⟨_⟩_; begin_ to begin_; _∎ to _∎)
\end{code}
}

This concludes the definition of streams and bisimilarity as their canonical
notion of equivalence.