Coinductive types: a ν-scheme over polynomial codes, with dischargeable coinduction

[Russoul]

Coinductive types for Nova, specified and implemented end to end: a ν-scheme over one-hole polynomial codes — the smallest useful dual of the QIIT scheme — with observation, corecursion, one-step β, and a dischargeable coinduction principle.

Theory (docs/NovaFoundation.txt)

• Polynomials 𝔽 ::= 𝕏 | K a | 𝔽 ⨯ 𝔽 | 𝔽 ⊎ 𝔽 | El a ⨯ 𝔽 | El a → 𝔽 — one-hole strictly positive codes, checked by poly-* rules; positivity is grammatical. Every polynomial is small, so ν 𝔽 always has a code.
• Formers: ν 𝔽 (carried polynomial, structural identity — iso-recursive, like a QIIT's 𝒮), out as the eliminator, corec 𝔽 a f x as the introduction (the polynomial and carrier are carried: β consumes map_𝔽, so the redex is self-contained). Canonical forms are corec-headed; out forces lazily — Π's polarity, not ℕ's.
• Laws: el-nu-beta (one observation step through the ≜-defined functorial action map_𝔽) and el-nu-eta (uniqueness of the corecursor — the coinduction principle, judgemental under the extensional discipline, with bisimulation-implies-equality as corollary).
• el-nu-coind — the admissible relational form of el-nu-eta (the el-squash-e-eq precedent), via a fourth ≜-meta-operation, the relator lift_𝔽(R): relation lifting per former, sums by dependent ⊎-elim at motive Ω (definitional collapse on the diagonal), dependent pairs with no transport (the instance equation reflects from its own binder). The subset-carrier derivation from el-nu-eta is sketched in place.
• SEMANTICS and SUBSUMPTION notes: the setoid model interprets ν 𝔽 by the ℕ-indexed limit with the largest bisimulation as the relation; every ν 𝔽 is definable by that limit internally, so the scheme is conservative — retained for structural identity, one-step β, and the uniform η, exactly the status of ℕ, ⊎ and (/).

Kernel and elaborator

• docs/NovaKernel.txt / docs/NovaElaboration.txt updated rule for rule; Poly in the core syntax with reflectPoly / mapPoly / liftPoly as meta-operations; β in all three normalizers; formation, inference, checking, typed descent, path replay, and structural ν-conversion (nuCong-style decomposition of carried polynomials).
• Coinduction discharges: el-nu-coind rides ⋆ as a skeleton payload (invariant, endpoint proof, one-step closure — three checked terms; the closure's type is kernel-computed from 𝔽 and R, never elaborator-supplied). Surface form coind (x y. R) p (x y h. q).
• Two discharge-engine extensions make closure proofs ergonomic: ground hypotheses shaped as (dependent) Σ-trees of equations license one rewrite candidate per component (the shape squash-elim binds for conjunction and existential invariants), and variable-definition hypotheses (☐ₙ ≡ t, ☐ₙ ∉ t) are admitted as rewrite rules despite growing — each application strictly removes an occurrence.

Corpus

• stream.nova — streams and conaturals: hd/tl/cons/iterate/mapS, β-driven observation lemmas, tlCons by graph-invariant coinduction, and conat's ∞ ≡ ∞ + 1 (the relator's sum clause, collapsing definitionally on the inj₂ diagonal).
• streamEq.nova — observational equality in Ω (obsEq, squash of a Π over ℕ of equations), with map-id and map-fusion proved by induction on observation depth.
• streamBisim.nova — bisimilarity as the impredicative gfp in Ω (union of post-fixed points), unfold laws, equivalence with obsEq in both directions, and bisimReflect: bisimilarity implies equality, upgrading map-id and map-fusion to judgemental equations.

Tests

127/127 golden tests, 26/26 corpus elaborations. New coverage: parser goldens for the ν formers, evaluation goldens for el-nu-beta (including take N of a finite colist with padding and of the infinite naturals), elaboration goldens for acceptance, for coinduction at every polynomial class (sum, exponent, dependent pair), and a negative test showing a non-closing invariant surfaces as an ordinary obligation rather than an error.