Copatterns: defining observations, over primitive corecursion

[Russoul]

What

Basic copattern matching for Nova — a def into a ν-type states its one observation and the elaborator synthesizes everything else — built on two coordinated strengthenings of the coinductive scheme in Foundation.

1. Primitive corecursion + coinduction up to equality (theory)

• el-nu-i/-beta/-eta: the corecursor is now the apomorphism — the coalgebra fills each hole with ν 𝔽 ⊎ a, where inj₁ stops at an existing element and inj₂ continues from a seed. β mediates through the stop-or-continue copair [𝕚𝕕 ‖ hᵉˡ], so a stopped element is released bare, judgementally (the inductive side already ships full dependent elimination; this restores parity — the old scheme was dual to mere iteration).
• el-nu-coind's relator hole clause is now up to equality: lift_𝕏(R) u v ≜ ∥R ⊎ (u ≡ v ∈ ν 𝔽)∥.
• Both are admissible, with derivation/subsumption notes extended in NovaFoundation.txt; the setoid model validates them on the nose (equality ⊆ the largest bisimulation).
• Payoff visible before copatterns even land: cons/csucc become one-stop machines, and tlCons — previously the deliberately η-needing example proven by hand-rolled coinduction — demotes to a β-lemma.

2. The copattern item (docs/NovaElaboration.txt, "Defining observations")

def cons : {a : 𝕌} → a → stream a → stream a using (stream.stream.unfold)
  | out (cons x s) ≔ x, s

An item macro, the clausal def's dual: it asserts the observation determines the definiendum and expands into the batch naming that assertion's pieces — existence (a synthesized primitive corecursor, the body read against the polynomial's shape: literal constructors down to the holes, calls continuing at the varying-columns seed, f-free elements stopping), the Π-closed observation lemma consOut (λ…. ⋆, β in every case), and pointwise uniqueness consEta (coind at the pure graph invariant; stops close in the relator's up-to-equality leg). Tiers degrade exactly as at the clausal def — witness-supplied existence keeps the lemma ⋆ an ordinary obligation, non-fragment bodies demote to declarations, never a wall. No new Foundation rule or kernel capability beyond layer 1.

3. Implicit columns — both macros

LHS and calls follow the ordinary term syntax — implicits elided or {x}-spelled, never spelled as explicit arguments. Placement is resolved by the macro from the item's own type; the values of elided call arguments are verified against the insertion-resolved body by a snapshot-rolled-back probe (conversion to the corecursor happens after implicit placement is resolved), degrading with a spell-it remedy if an elided argument varies. Generated spines apply the item through {…} overrides and a candidate variable fully and plainly; generated lemma binders mirror the item's implicitness.

The pattern-clause macro takes the same conventions (second commit): clause LHSs align against the item's columns with {x}-spelled or elided implicits, recursive calls elide likewise (elided arguments read as the ambient columns, verified by the clause lemmas' β-discharge), and the item-level using-clause rides along on every generated item — so def hd : {a : 𝕌} → stream a → a using (…) | hd t ≔ (out t) .π₁ works, ℕ-splits over implicit-parameterized items included (nth). The bespoke structural-recursion rewriter is replaced by a generic spine-rewriting traversal shared with the copattern respell.

Reviewer notes

• Three latent engine gaps surfaced and fixed while making the discharges silent: matchElemP had no coinductive-former clauses (an out-headed rewrite candidate could never fire); observation equations are growing rewrites, now admitted as observation-shaped candidates (the el-nu-beta counterpart of the clause-shaped admission, SearchlessElaboration.md §12); and the certificate-bearing rewriter (rewriteElemS) emitted kernel-untypable steps under branch binders — it now stays at kernel-determinable positions, scrutinee-first.
• One subtle invariant worth knowing: the Σ-entry name index (sigEntryIx) caches positively, sound because Σ only extends within a run. The macro's probe therefore pre-declares the item under a machine name — a probe declaration cached under the real name would shadow the later definition and silently disable its unfolds. Recorded in SearchlessElaboration.md.
• Also fixes a latent weakening bug in liftPoly's sum clause (sub-polynomials' embedded codes weren't weakened under the two ⊎-elim binders; never fired because no corpus polynomial had ambient-referencing codes under a ⊎).
• Corpus: conat.nova (czero/cinf/csucc) and stream.nova (cons/iterate/map) are copattern items, hd/tl clausal ones, all in canonical distill form; streamEq/streamBisim needed zero changes. The migrated ν goldens have byte-identical expected outputs (evaluation through stops included).
• Gates: 163/163 tests, 94/94 corpus elaborations, distill round-trip and canonical-form verified.

Deferred (future-work list updated): observation splitting / defined observations (wants the codata item macro), the probe verification of elided call arguments for the pattern macro (copattern-only today), course-of-values ↔ futumorphism.