\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: