\subsection{Stream-entry Selection and the Substream Relation}
\label{sec:appl:substream}

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

We come now to the definition of the substream relation and the proof that it is
transitive.
As in \secRef{trans-substream}, first define the substream relation in terms of
selection from streams, which we call here $\leq'$.
Also we repeat, for the sake of completeness, in Agda code the proof that
selecting distributes over composition of selectors, from which we derived
that $\leq'$ is transitive in \secRef{trans-substream}.
In \exRef{cat-substream}, we showed how the substream relation can be directly
defined as an inductive-coinductive relation.
The second part of this section is concerned with restating this definition in
Agda and proving that it is equivalent to the definition in terms of selecting.
We end by deriving transitivity of the directly defined substream relation from
the distribution of selecting over selector composition.

\begin{code}
module Substream (A : Set) where
\end{code}

In this section, it suffices to instantiate bisimilarity for streams over $A$
so that we compare heads by propositional equality.
Recall that we introduced in \exRef{prop-eq-type} for terms $s$ and $t$ a type
$\Eq_A(s,t)$ with one constructor: $\refl : \pTerm[(x : A)]{\Eq_A(x,x)}$.
This types is meant to model propositional equality, that it, the notion of
equality on $A$ internal to the type theory.
In Agda, propositional equality is a binary relation \AgdaFunction{\_≡\_},
which we import from the module \AgdaModule{Relation.Binary}.
Since propositional equality is an equivalence relation, $(A, \equiv)$ is a
setoid.
Thus, we can instantiate \AgdaModule{Bisim} that setoid to obtain that
streams over $A$ form a setoid with bisimilarity.
\begin{code}
open import Relation.Binary
open import Relation.Binary.PropositionalEquality renaming (setoid to ≡-setoid)
open import PropsAsTypes
open import Stream

open Bisim (≡-setoid A)
\end{code}

\AgdaHide{
\begin{code}
open ~-Reasoning
\end{code}
}

Recall that we defined in \exRef{filter} the type of stream selectors $\Sel$ to
be the inductive-coinductive type $\gfp{\lfp[Y]{X + Y}}$, and that the first
unfolding $\Selm$ to the finitary steps was given by $\lfp[Y]{\Sel + Y}$.
In Agda, we declare these types mutually as follows, where we directly give
readable names to the corresponding destructors and constructors.
\begin{code}
mutual
  record Sel : Set where
    coinductive
    field out : Selμ

  data Selμ : Set where
    pres  : Sel → Selμ
    drop  : Selμ → Selμ
\end{code}

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

Given this definition of selectors, we can define selection from streams exactly
as in \exRef{filter} by the following equational specification.
\begin{code}
selectμ  : Selμ → Stream A → Stream A
select   : Sel → Stream A → Stream A

select x = selectμ (x .out)

selectμ (pres x) s .hd  = s .hd
selectμ (pres x) s .tl  = select x (s .tl)
selectμ (drop u) s      = selectμ u (s .tl)
\end{code}

Stream selecting allows us now to define the first version of the substream
relation.\endnote{%
  \textcite{Bertot:FiltersStreams} defines a different notion of stream
  selection that allows one to select from streams by productive predicates.
  This way of selecting from streams is essentially equivalent to our notion of
  selecting by positions, see.\todo{Provide reference to code}
}
Since it will turn out to be useful to be explicit about the $x$ selector that
witnesses that $s$ is a substream of $t$, we first define a ternary relation.
This relation should be read as saying that if
\AgdaBound{s} \AgdaFunction{≤μ[}\AgdaBound{x}\AgdaFunction{]} \AgdaBound{t},
then $s$ is a substream of $t$ witnessed by the selector $x$.
In the later proofs, we also need to be able to witness the substream relation
by elements of $\Selm$, hence we also introduce the corresponding version of
the substream relation.
\begin{code}
_≤[_]_ : Stream A → Sel → Stream A → Prop
s ≤[ x ] t = s ~ select x t

_≤μ[_]_ : Stream A → Selμ → Stream A → Prop
s ≤μ[ u ] t = s ~ selectμ u t
\end{code}

From the ternary substream relation we can recover the definition that we used
in \exRef{substream}.
\begin{code}
_≤'_ : Stream A → Stream A → Prop
s ≤' t = ∃[ x ∈ Sel ] (s ≤[ x ] t)
\end{code}

To prove transitivity of $\leq'$, we defined in \secRef{trans-substream} also
composition of stream selectors, the definition of which we repeat here now in
Agda syntax.
\begin{code}
_•_   : Sel → Sel → Sel
_•μ_  : Selμ → Selμ → Selμ

(x • y) .out = (x .out) •μ (y .out)

(pres x')  •μ (pres y')  = pres (x' • y')
(drop u')  •μ (pres y')  = drop (u' •μ (y' .out))
u          •μ (drop v')  = drop (u •μ v')
\end{code}

The main result of \secRef{trans-substream}, \propRef{filter-comp-hom}, was that
selecting from streams by a composition of selectors is equally given by
composition of select functions.
We went in that section through great pain to prove this result.
This was caused by the fact that we had to separate the induction principle
for $\Selm$ from the coinduction principle of $\Sel$.
Using recursive equational specifications, we can merge these two and thereby
give now a very compact proof.
Note that we use bisimilarity in the following propositions to compare streams,
rather than the weaker notion of propositional equality.
\begin{code}
select-hom   : ∀ x y s → select (y • x) s ~ select y (select x s)
selectμ-hom  : ∀ u v s → selectμ (v •μ u) s ~ selectμ v (selectμ u s)

select-hom x y s = selectμ-hom (x .out) (y .out) s

selectμ-hom (pres x) (pres y)  s .hd≈  = refl
selectμ-hom (pres x) (pres y)  s .tl~  = select-hom x y (s .tl)
selectμ-hom (pres x) (drop v)  s       = selectμ-hom (x .out) v (s .tl)
selectμ-hom (drop u) (pres x)  s       = selectμ-hom u (pres x) (s .tl)
selectμ-hom (drop u) (drop v)  s       = selectμ-hom u (drop v) (s .tl)
\end{code}
This is our first proof that proceeds by mixing induction and coinduction, so
let us briefly explain what is going on here.
First of all, we are simultaneously proving two propositions, namely
\AgdaFunction{select-hom} and \AgdaFunction{selectμ-hom}.
The first is the statement we are after and constitutes the coinductive
part of the proof, whereas the second proposition encapsulates the induction.
\AgdaFunction{select-hom} is fairly simple and is only used in the case when we
have to prove that the tails of of both outputs are bisimilar (second case of
\AgdaFunction{selectμ-hom}).
In the proof of the second proposition \AgdaFunction{selectμ-hom}, we proceed by
induction on the two $\Selm$ arguments.
The cases that appear here are essentially those that appear in the definition
of selector composition.
Note, however, that in the last two cases of \AgdaFunction{selectμ-hom} we do
the same.
At the time of writing, they both need to be there for Agda to be able to
reduce the definition of \AgdaFunction{•μ} while checking the correctness of
the proof.
This is a slight nuisance, which might be improved in the future though.

To use that selecting preserves composition for proving transitivity of $\leq'$,
we will need the following lemma.
This lemma states that selecting respects bisimilarity, that is, bisimilar
streams are mapped to bisimilar streams by \AgdaFunction{select}.
\begin{code}
select-resp~   : ∀{s t} (x : Sel)  → s ~ t → select x s ~ select x t
selectμ-resp~  : ∀{s t} (u : Selμ) → s ~ t → selectμ u s ~ selectμ u t

select-resp~ x p = selectμ-resp~ (x .out) p

selectμ-resp~ (pres x)  p .hd≈  = p .hd≈
selectμ-resp~ (pres x)  p .tl~  = select-resp~ x (p .tl~)
selectμ-resp~ (drop u)  p       = selectμ-resp~ u (p .tl~)
\end{code}

% We prove transitivity of the witnessed substream relation by
% \begin{align*}
%   r & \sim \AgdaFunction{select} \> \AgdaBound{x} \> \AgdaBound{s} \\
%   & \sim \AgdaFunction{select} \> \AgdaBound{x} \>
%   (\AgdaFunction{select} \> \AgdaBound{y} \> \AgdaBound{t}) \\
%   & \sim \AgdaFunction{select} \>
%   (\AgdaFunction{comp} \> \AgdaBound{x} \> \AgdaBound{y}) \> \AgdaBound{t}
% \end{align*}

We are now in the position to show that the relation $\leq'$ is transitive.
To do so, we first show transitivity for the substream relation with explicit
witnesses.
This proof proceeds by chaining together bisimilarity proofs that are given
in the \AgdaFunction{begin} \dots \ \AgdaFunction{\blacksquare} block.
Since the technicalities of how such blocks can be defined in Agda would lead us
of track, we will skip these details and just explain the intuition of the
proof.
By definition of $r \mathrel{{\leq}[x]} s$, $p$ is a proof of
$r \sim \fil \> (x \filComp y) \> t$.
Inside the block, we write this as
$r \mathrel{{\sim}\langle p \rangle} \fil \> (x \filComp y) \> t$.
Next, we use that selecting respects bisimilarity to replace $s$ by
$\fil \> y \> t$.
Finally, we turn the composition of selecting into composition of the witnessing
selectors.
This proves $r \sim \fil \> (x \filComp y) \> t$, which is by definition
$r \mathrel{{\leq}[x \filComp y]} t$.
The proof term \AgdaFunction{≤-select-trans} could be given by using
transitivity of bisimilarity (\AgdaFunction{S.trans}) twice, but the presented
version is certainly preferable in terms of readability.
\begin{code}
≤-select-trans : ∀{r s t} {x y} → r ≤[ x ] s → s ≤[ y ] t → r ≤[ x • y ] t
≤-select-trans {r} {s} {t} {x} {y} p q =
  begin
    r
  ~⟨ p ⟩
    select x s
  ~⟨ select-resp~ x q ⟩
    select x (select y t)
  ~⟨ S.sym (select-hom y x t) ⟩
    select (x • y) t
  ∎
  where
    module S = Setoid stream-setoid
\end{code}

Now that we have proved transitivity with explicit witnesses, transitivity of
$\leq'$ follows by an easy manipulation of existential quantifiers:
\begin{code}
≤'-trans : ∀{r s t} → r ≤' s → s ≤' t → r ≤' t
≤'-trans = ∃₂-elim  (λ x y p q →
                    ∃-intro (x • y) (≤-select-trans {x = x} {y} p q))
\end{code}

This concludes the recasting of the proof of transitivity relation based of
stream selecting in Agda.
We come now to the direct definition of the substream relation as mixed
inductive-coinductive relation.
The intuition for this definition was explained in \exRef{cat-substream},
we merely repeat the definition here in Agda syntax.
\begin{code}
mutual
  record _≤_ (s t : Stream A) : Prop where
    coinductive
    field out≤ : s ≤μ t

  data _≤μ_ (s t : Stream A) : Prop where
    match : (s .hd ≡ t .hd) → (s .tl ≤ t .tl) → s ≤μ t
    skip  : (s ≤μ t .tl) → s ≤μ t
\end{code}

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

In the remainder of the section we show that this direct definition is
equivalent to the selecting-based one and derive transitivity of $\leq$
from there.
The first step towards this is to extract from a proof of $\leq$ a selector
witness.
\begin{code}
witness   : {s t : Stream A} → s ≤ t → Sel
witnessμ  : {s t : Stream A} → s ≤μ t → Selμ

witness p .out = witnessμ (p .out≤)

witnessμ (match _ t≤)  = pres (witness t≤)
witnessμ (skip u)      = drop (witnessμ u)
\end{code}

We can now use the extracted witness to show that the substream relation
is included in the witness-based substream relation and hence in the
select-based substream relation.
\begin{code}
≤-implies-select≤    : ∀{s t} → (p : s ≤ t) → s ≤[ witness p ] t
≤μ-implies-selectμ≤  : ∀{s t} → (p : s ≤μ t) → s ≤μ[ witnessμ p ] t

≤-implies-select≤ {s} {t} p = ≤μ-implies-selectμ≤ (p .out≤)

≤μ-implies-selectμ≤ (match h≡ t≤) .hd≈  = h≡
≤μ-implies-selectμ≤ (match h≡ t≤) .tl~  = ≤-implies-select≤ t≤
≤μ-implies-selectμ≤ (skip q)            = ≤μ-implies-selectμ≤ q

≤-implies-≤' : ∀{s t} → s ≤ t → s ≤' t
≤-implies-≤' p = ∃-intro (witness p) (≤-implies-select≤ p)
\end{code}

Conversely, we can construct from a selector witness a proof for the
substream relation.
This allows us then to show that the select-based substream relation is
in included in the substream relation.
\begin{code}
select≤-implies-≤    : ∀{s t} (x : Sel) → s ≤[ x ] t → s ≤ t
selectμ≤⇒≤μ  : ∀{s t} (u : Selμ) → s ≤μ[ u ] t → s ≤μ t

select≤-implies-≤ x p .out≤ = selectμ≤⇒≤μ (x .out) p

selectμ≤⇒≤μ (pres x) p  = match (p .hd≈) (select≤-implies-≤ x (p .tl~))
selectμ≤⇒≤μ (drop u) p  = skip (selectμ≤⇒≤μ u p)

≤'-implies-≤ : ∀{s t} → s ≤' t → s ≤ t
≤'-implies-≤ = ∃-elim select≤-implies-≤
\end{code}

Putting these to results together, we obtain a proof that the two
definitions for the substream relation are equivalent.
\begin{code}
≤-and-≤'-equiv : ∀ s t → s ≤ t ⇔ s ≤' t
≤-and-≤'-equiv s t = equivalence ≤-implies-≤' ≤'-implies-≤
\end{code}

Finally, using this equivalence, we can derive from the fact that
$\leq'$ is transitive that also $\leq$ is transitive.
\begin{code}
≤-trans : ∀{r s t} → r ≤ s → s ≤ t → r ≤ t
≤-trans p q = ≤'-implies-≤ (≤'-trans (≤-implies-≤' p) (≤-implies-≤' q))
\end{code}

%%% Local Variables:
%%% ispell-local-dictionary: "british"
%%% End: