Corecursive Definitions, Copatterns, and Productivity

Proof. Induct on the declaration order of $\mathrm{\Sigma }$. The empty extension is theorem 111.76, lemma 111.77. For one nonrecursive Timpl-data block, extend the semantic domain by disjoint constructor tags carrying the semantic interpretations of their already interpreted fields. Evaluation of an introduction returns that tag. Evaluation of its eliminator inspects the tag and applies the corresponding generated method; this is exactly Block-comp. A neutral scrutinee is reflected as a stuck eliminator, and readback reconstructs it. Structural induction on the finite constructor telescope proves that evaluation and readback are functional. The proof of the fundamental lemma gains precisely the introduction, neutral-elimination, and Block-comp cases just described; none recurses through the new family. The escape argument therefore gives typing and soundness, the semantic equality argument gives completeness, and induction on normal forms gives stability, exactly as in theorem 111.76, lemma 111.77. The same declaration-order induction proves definedness of the new semantic operations: every Block-comp clause consumes a constructor tag from the block being interpreted and invokes methods over previously interpreted field types, so no semantic call returns to the new family.

For item 5, ordinary substitution gives $e[\theta ]\equiv e[{\theta }^{\prime }]$ from the component equations, after the displayed classifier conversion. Completeness from item 3 makes their normal forms identical.

The definition of ${\Downarrow }_{\mathsf{T}}$ makes existence and uniqueness immediate from item 1. Soundness gives the forward implication of the displayed characterization. Conversely, completeness and stability show that any normal $n$ judgmentally equal to $e$ is the normalizer output.

For the implementation claims, first prove determinism by induction on the first ${\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}$ derivation and inversion of a second derivation. Disjoint value constructors select the same rule; the induction hypotheses identify each runtime premise and then the selected branch. In T-Nat-S and T-Vec-Cons, apply the hypotheses first to the scrutinee, then to the strictly smaller recursive-eliminator premise, and finally to the branch body. These are the only rules with a recursive evaluation premise.

Finally, induct on a ${\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}$ derivation, retaining its typing derivation, to prove $e\equiv v$. Rule T-Val uses reflexivity. For T-App-R, inversion gives $f:\prod _{x:A_0}^{ϵ,\mathsf{runtime}}B$ and $a:A_0$. The induction hypotheses and the application computation rule give $$fa\stackrel{congruence}{\equiv }(\lambda x.b)v_a\stackrel{\mathrm{\Pi }-\beta }{\equiv }b[v_a/x]\stackrel{IH}{\equiv }v.$$ Substitution congruence for $a\equiv v_a$ converts the chain from $B[v_a/x]$ to $B[a/x]$. Rule T-App-E uses the same chain with the unchanged checked argument $a$. Rule T-Pair uses dependent pair congruence, converting the second induction hypothesis along the first one. Rules T-Fst and T-Snd compose scrutinee congruence with the corresponding $\mathrm{\Sigma }$-computation equation; the second projection result is converted along congruence of first projection.

Rule T-Con uses constructor congruence on each runtime field and reflexivity on each static field. For T-Case, scrutinee congruence reaches the selected constructor, Block-comp exposes the selected branch, and simultaneous substitution congruence followed by the branch induction hypothesis reaches $v$. Motive conversion follows the scrutinee equality. Rules T-Bool-T and T-Bool-F are the two primitive instances.

For T-Nat-Z, combine scrutinee congruence, Nat-comp${}_1$, and the base induction hypothesis. For T-Nat-S, scrutinee congruence and Nat-comp${}_2$ expose the step body. The predecessor and recursive-result induction hypotheses justify simultaneous substitution, and the branch induction hypothesis reaches $v$; conversion along $m\equiv \mathsf{suc}(v_n)$ restores the original motive. In T-J, proof soundness gives $e_q\equiv {\mathsf{refl}}_{v_q}$. Identity-value inversion gives $v_q\equiv a\equiv b$; after those conversions, Id-comp exposes $e_r[a/z]$, and its induction hypothesis reaches $v$.

Rule T-Vec-Nil uses the index and vector induction hypotheses, Vec-comp${}_1$, and conversion along $m\equiv 0$ and $ys\equiv \mathsf{vnil}$. Rule T-Vec-Cons uses Vec-comp${}_2$; simultaneous congruence substitutes the equal predecessor, head, tail, and recursive result, while conversion along $m\equiv \mathsf{suc}(v_n)$ and $ys\equiv \mathsf{vcons}(v_n,v_a,v_{xs})$ restores the declared indexed motive. These cases exhaust the implementation rule card. Normalizer completeness gives $\mathrm{nf}(e)=\mathrm{nf}(v)$, and the definition of ${\Downarrow }_{\mathsf{T}}$ gives $e{\Downarrow }_{\mathsf{T}}\mathrm{nf}(v)$. For example, $\lambda x.((\lambda y.y)x){\Downarrow }_{\mathsf{T}\mathsf{,}\mathsf{cbv}}\lambda x.((\lambda y.y)x)$ by T-Val, after which the required second stage returns the NbE normal form $\lambda x.x$. ◻

Proof. Induct on $\mathrm{\Delta }$. The empty tuple has the unique empty result. For a runtime extension, apply the induction hypothesis to the prefix, substitute its result into the last component, and use lemma 124.3 to obtain its unique typed normal form. For an erased extension, the induction hypothesis fixes the prefix and totality and uniqueness of the same typed normalizer fix the canonical static component. These are exactly the two recursive clauses of $\mathsf{prep}$. ◻

Proof. The checker traverses each finite right side once, emitting a finite graph. It deletes positive edges and performs depth-first cycle detection on the remaining finite graph. If no back edge is found, reverse finishing order is a topological ranking. Every zero edge points to a vertex with smaller rank by construction. All traversals therefore terminate and the returned rank has the stated property. ◻

Proof. Inspect the selected copattern equation. A head right side is in the nonrecursive terminating Timpl fragment except for recorded zero-weight calls. By lemma 124.4, the preparation function first produces ${\mathsf{prep}}_{{\mathrm{\Delta }}_f}(\overrightarrow{a})={\overrightarrow{a}}_v$. Substitution of ${\overrightarrow{a}}_v$ leaves every alias argument closed and group-free, and its componentwise evaluation produces the closed tuple required by Co-Head-Alias. Each alias call decreases rank by lemma 124.8; finite induction on $r(f)$ reaches a right side with no zero call and returns its normal form by the extended NbE subevaluation. A tail equation discharges the demanded tail and Co-Tail-Unfold returns its root mutual call after componentwise evaluation; the system-card side condition makes its arguments closed and group-free. These are the two coprojection forms of the system card. ◻

Proof. Generalize over the declared function $f$ and every closed group-free input tuple $\overrightarrow{a}$, then fix an observation word $o$. Induct lexicographically on the number of tail symbols in $o$ and the stored rank of $f$. For a head word, lemma 124.9 either returns a value or follows a zero edge and decreases the second component. For $\mathsf{tail}\cdot o^{\prime }$, the same lemma computes the tail to a closed call $g\overrightarrow{b}$. The recursive demand $o^{\prime }$ has one fewer tail symbol, so the generalized outer induction hypothesis applies to the arbitrary closed tuple $\overrightarrow{b}$ and gives its value. The two clauses construct a finite derivation $s{\Downarrow }_{o}v$ for every $o$. ◻

Proof. Induct on $\mathrm{\Delta }$. The empty suffix gives the first equation immediately. At a runtime binder, substitution composition identifies the term prepared by the recursive clause with the corresponding component of $\theta [{\eta }_v]$; totality and determinism in lemma 124.3 supply the component of ${\theta }_v$. At an erased binder, substitution composition identifies the same typed input to the normalizer, whose uniqueness supplies the component of ${\theta }_v$. This proves the concatenation equation.

For the second claim, compare the two simultaneous substitutions component by component. At a runtime position, the defining premise of preparation and soundness in lemma 124.3 give judgmental equality between the unprepared component and its normal form. At an erased position, normalizer soundness gives the same judgmental equality. Dependent substitution congruence, in telescope order, therefore gives $$e[\theta [{\eta }_v]/\mathrm{\Delta }]\equiv e[{\theta }_v/\mathrm{\Delta }]$$ at the common converted result type. Completeness in lemma 124.3 identifies their normal forms. By the definition of ${\Downarrow }_{\mathsf{T}}$, either displayed subevaluation judgment holds exactly when that common normal form is $w$, which proves both implications. ◻

Proof. Induct on $\mathrm{\Delta }$. Both extensions use stability of closed typed normal forms; the relevance mark determines only which preparation clause records the normalizer call. In both cases the induction hypothesis fixes the prefix, so the dependent substitution into the final component is unchanged. ◻

Proof. First, soundness of normalization and congruence give $$h({\mathsf{st}}_i({\overrightarrow{a}}_v))\equiv h({\mathsf{in}}_i({\overrightarrow{a}}_v)),t({\mathsf{st}}_i({\overrightarrow{a}}_v))\equiv t({\mathsf{in}}_i({\overrightarrow{a}}_v)).$$ Completeness therefore lets either map be calculated at the constructor and then normalized.

For the head equivalence, induct on the stored rank of $f_i$. A producer rule normalizes ${\hat{e}}_i[{\overrightarrow{a}}_v/\overrightarrow{x}]$, which is the branch selected by $h({\mathsf{in}}_i({\overrightarrow{a}}_v))$. For an alias to $f_j\overrightarrow{u}$, Co-Head-Alias first derives $${\mathsf{prep}}_{{\mathrm{\Delta }}_j}(\overrightarrow{u}[{\overrightarrow{a}}_v/\overrightarrow{x}])=\overrightarrow{b}$$ and then evaluates $\mathsf{head}(f_j\overrightarrow{b})$. Static alias resolution defines ${\hat{e}}_i$ as ${\hat{e}}_j$ under the same simultaneous substitution. By lemma 124.12, the resolved expression receives the same prepared tuple $\overrightarrow{b}$; the induction hypothesis for $f_j$, whose rank is smaller, gives both implications. This treats the producer and alias rule families.

For the tail equivalence, invert Co-Tail-Unfold. It fixes $j=\tau (i)$ and derives ${\mathsf{prep}}_{{\mathrm{\Delta }}_j}({\overrightarrow{u}}_i[{\overrightarrow{a}}_v/\overrightarrow{x}])=\overrightarrow{b}$. The generated branch for $t$ first contracts to ${\mathsf{in}}_{\tau (i)}({\overrightarrow{u}}_i[{\overrightarrow{a}}_v/\overrightarrow{x}])$. For every runtime component, preparation soundness identifies that component judgmentally with the corresponding component of $\overrightarrow{b}$. For every erased component, preparation replaces the checked substitution term by its typed NbE normal form; normalizer soundness makes those two terms judgmentally equal. Constructor congruence and completeness therefore identify the branch normal form with ${\mathsf{st}}_{\tau (i)}(\overrightarrow{b})$. Conversely, injectivity of the generated constructor tag identifies the prepared components, and normalizer uniqueness identifies each erased canonical component with the one fixed by preparation. Hence the same prepared tuple is recovered and Co-Tail-Unfold applies. The declaration index fixes $j=\tau (i)$. ◻

Proof. Write $s=f_i\overrightarrow{a}$. Generalize over $f_i$ and every closed group-free tuple $\overrightarrow{a}:{\mathrm{\Delta }}_i$, then induct on $o$. Normalizer-defined preparation gives a unique tuple ${\overrightarrow{a}}_v$ with ${\mathsf{prep}}_{{\mathrm{\Delta }}_i}(\overrightarrow{a})={\overrightarrow{a}}_v$. Preparation soundness and constructor congruence identify the normal forms, so $${\mathsf{in}}_i(\overrightarrow{a}){\Downarrow }_{\mathsf{T}}{\mathsf{st}}_i({\overrightarrow{a}}_v).$$

For $\mathsf{head}$, invert the source observation rule and apply the head equivalence of lemma 124.14. Its right side together with the displayed constructor evaluation is precisely Coiter-Head, so the elaborated call has the same head observation. Inverting Coiter-Head and using the converse implication of the lemma proves the reverse direction.

For $\mathsf{tail}\cdot o^{\prime }$, source inversion gives a uniquely determined closed call $f_j\overrightarrow{b}$, together with $$\mathsf{tail}(f_i\overrightarrow{a})\Downarrow f_j\overrightarrow{b},f_j\overrightarrow{b}{\Downarrow }_{o^{\prime }}v.$$ The tail equivalence of lemma 124.14 and Coiter-Tail derive $$\mathsf{tail}(\mathsf{coiter}(h,t,{\mathsf{in}}_i(\overrightarrow{a})))\Downarrow \mathsf{coiter}(h,t,{\mathsf{st}}_j(\overrightarrow{b})).$$ By lemma 124.13, the tuple $\overrightarrow{b}$ is fixed by preparation. The raw elaborated state ${\mathsf{in}}_j(\overrightarrow{b})$ and the state ${\mathsf{st}}_j(\overrightarrow{b})$ both subevaluate to the latter by definition and stability. Hence every first Coiter-Head or Coiter-Tail premise is identical for the two target streams. Apply the generalized induction hypothesis to the closed call $f_j\overrightarrow{b}$ and the shorter word $o^{\prime }$. Conversely, inversion of Coiter-Tail, the converse tail equivalence, and the same induction hypothesis reconstruct the two source premises. These are the two forms of observation word. ◻