ch:coinduction: ch:coinduction

Take state $\mathbf{2}$, output the state itself, transition Boolean negation, and initial state $\mathsf{tt}$: $$\mathsf{alternate}:={\mathsf{corec}}_{\mathbf{2}}(\mathbf{2},\lambda x.x,\mathsf{not},\mathsf{tt}).$$ The state iterates at depths $0$ through $4$ are $\mathsf{tt},\mathsf{ff},\mathsf{tt},\mathsf{ff},\mathsf{tt}$, respectively. Applying the output function, which is the identity, gives the same five observations.

The complete clauses are Compile them with state $\mathsf{Stream}(A)\times \mathsf{Stream}(B)$ and maps The corecursor’s head and tail equations reduce judgmentally to the two clauses. Deleting the tail clause leaves $\mathsf{tail}(\mathsf{zipWith}(f,s,t))$ uncovered, so the copattern definition is incomplete.

Use the proof-relevant relation Eliminate the two identities carried by a witness $(r,t,-,-)$. The head obligation is exactly $c(\mathsf{head}(r))(\mathsf{head}(t))$. The tails reduce to $$\mathsf{zipWith}(f,\mathsf{tail}(r),\mathsf{tail}(t)),\mathsf{zipWith}(f,\mathsf{tail}(t),\mathsf{tail}(r)),$$ which belong to $B$ with witnesses $\mathsf{tail}(r),\mathsf{tail}(t)$. Thus $B$ is a bisimulation, and stream coinduction gives the required observational equality.

Let $s$ be the constant-zero stream. Let $t$ be generated from Boolean state with output $0$ at $\mathsf{ff}$, output $1$ at $\mathsf{tt}$, negating transition, and initial state $\mathsf{ff}$. Then both heads are $0$, so $B(s,t)$ holds, but their depth-one observations are $0$ and $1$. The proposed relation has no closure witness $B(\mathsf{tail}(s),\mathsf{tail}(t))$; this is precisely the second premise of definition 85.12.

Use the proof-relevant relation $$B(u,v):=\sum _{r:\mathsf{Stream}(A)}({\mathsf{Id}}_{\mathsf{Stream}(A)}(u,\mathsf{map}(\lambda x.x,r))\times {\mathsf{Id}}_{\mathsf{Stream}(A)}(v,r)).$$ After eliminating the two identities carried by a witness $(r,-,-)$, the heads calculate as $$\mathsf{head}(\mathsf{map}(\lambda x.x,r))\equiv (\lambda x.x)(\mathsf{head}(r))\equiv \mathsf{head}(r).$$ The tails are related with witness $\mathsf{tail}(r)$ because $\mathsf{tail}(\mathsf{map}(\lambda x.x,r))\equiv \mathsf{map}(\lambda x.x,\mathsf{tail}(r))$. Coinduction yields $\mathsf{map}(\lambda x.x,s){\approx }_{A}s$.

Use state $(n,a):\mathbb{N}\times \mathbb{N}$, output $a$, transition $(n,a)\mapsto (\mathsf{suc}(n),a+\mathsf{suc}(n))$, and initial state $(0,0)$. The equivalent copattern clauses are $$\mathsf{head}(T(n,a))=a,\mathsf{tail}(T(n,a))=T(\mathsf{suc}(n),a+\mathsf{suc}(n)).$$ Their compilation is exactly that pair-state corecursor. Starting from $(0,0)$, the states have second components $0,1,3,6,10,15$, so these are the first six observations. To compare a separately named copattern definition with the compiled corecursor, relate the two results at every state $(n,a)$. Their heads are both $a$ and their tails are related at $(\mathsf{suc}(n),a+\mathsf{suc}(n))$; coinduction proves observational equality.

The zero clauses compile with state $\mathbf{1}$, constant output $0$, and the identity transition, so both are accepted instances of definition 85.9. Put $s:=\mathsf{nats}:=\mathsf{iterate}(\mathsf{suc},0)$. Its head equation is judgmental, while its tail relation is observational: $$\mathsf{head}(s)\equiv 0,\mathsf{tail}(s){\approx }_{\mathbb{N}}\mathsf{map}(\mathsf{suc},s).$$ For the second equation, relate, for every $n$, $$\mathsf{iterate}(\mathsf{suc},\mathsf{suc}(n))\text{and}\mathsf{map}(\mathsf{suc},\mathsf{iterate}(\mathsf{suc},n)).$$ Their heads both compute to $\mathsf{suc}(n)$; their tails have the same relation at $\mathsf{suc}(n)$ by the iterate-tail and map-tail rules. Coinduction proves the displayed observational equality at $n=0$. Written as a recursive clause, its recursive occurrence is nested under $\mathsf{map}$ rather than being the complete result of the matched tail clause, so the selected syntactic guard rejects it.

For the finite observations, first prove by induction on $n$ that $$\mathsf{nth}(n,\mathsf{map}(f,r))=f(\mathsf{nth}(n,r)).$$ The zero case is Map-head. The successor case uses Map-tail and the induction hypothesis at $\mathsf{tail}(r)$. More directly, induction on $n$ with the iterate computation rules gives Thus $s$ has observations $0,1,2,\dots$. The observational tail equation and these calculations prove productivity of the example without turning stream observational equality into identity or claiming completeness of the guard checker.