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

.claude/skills/nova/SKILL.md

@@ -120,7 +120,10 @@ Types: `𝟘 𝟙 ℕ 𝕌 Ω`, `(x : T) → U` and `T → U`, `(x : T) ⨯ U`,
 `T ⊎ U` (non-dependent disjoint union; binds TIGHTER than → ⨯, so
 `A ⊎ B → C` is `(A ⊎ B) → C`),
 `l ≡ r ∈ T` (SUGAR for `Prf (l ≡ r ∈ T)` — equality is an Ω-valued
-PROPOSITION), `El t`, `T / (x y. r)` (r is Ω-valued), `Prf p`.
+PROPOSITION), `El t`, `T / (x y. r)` (r is Ω-valued), `Prf p`,
+`ν F` (coinductive type at a one-hole polynomial `F ::= 𝕏 | K t |
+F ⨯ F | F ⊎ F | (x:t) ⨯ F | (x:t) → F` — external pieces are codes;
+e.g. `ν (K a ⨯ 𝕏)` is streams of `a`).
 `∥T∥` squashes any type to a proposition; `∥Prf p∥ ≜ p`.
 
 Elements: `λx. t`; application by juxtaposition; `(t : T)` ascription
@@ -132,6 +135,19 @@ the ∈-slot takes a TYPE, so write `∈ El a` for a code `a`);
 `⊎-elim (w. T) (a. l) (b. r) t` (motive, left case, right case,
 scrutinee — β on both injections);
 `class t` (quotient intro); `quot-elim (x. T) (a. f) q`;
+`out t` (the coinductive observation — infers, like the projections)
+and `corec (x : a. f) u` (corecursor: carrier code `a`, coalgebra
+body `f` over `x : El a`, seed `u` — checking-only, the polynomial
+comes from the expected ν-type; β: `out (corec …)` runs one step);
+`coind (x y. R) p (x y h. q)` (COINDUCTION, el-nu-coind, checked at
+`Prf (l ≡ r ∈ El (ν F))`: invariant `R` at Ω over the two sides,
+`p : Prf (R l r)`, and `q` the one-step closure — under generic
+`x y` and `h : Prf (R x y)`, prove the observations RELATOR-related.
+Idioms: conjunction/existential invariants are squashed Σs —
+`squash-elim h (w. ⋆ (…))` unpacks them, and the engine harvests
+`w`'s projected equations automatically; `u ≡ ⟨machine⟩`-shaped
+components act as unfold-once rewrite rules. See stream.nova's
+tlCons and streamBisim.nova's bisimReflect);
 `⋆` (canonical proof; `⋆ e` with explicit witness);
 `squash-elim e (x. body)`. Universe codes are written like their types
 (`𝟘 𝟙 ℕ`, `(x : t) → u`, `l ≡ r ∈ t`).
@@ -210,6 +226,11 @@ data [a : 𝕌] [r : El a → El a → Ω]
 - `src/nova/` — the corpus, one topic per file: `nat` (arithmetic),
   `sum` (the disjoint union ⊎: inj₁/inj₂, ⊎-elim, β/η, derived
   injectivity and disjointness),
+  `stream` (coinductive streams and conaturals: ν, out, corec,
+  β-driven observation lemmas, tlCons by graph-invariant coind),
+  `streamEq`/`streamBisim` (observational equality in Ω, bisimilarity
+  as the impredicative gfp, bisimReflect — bisimilarity implies
+  equality — and the map-id/map-fusion equalities),
   `equality`/`prop` (≡ and Ω), `quotient`/`quottyuniv` (quotients),
   `vect`/`vectAppend` (𝕌-indexed families), `qiitNat`/`qiitBag`/
   `qiitQuot`/`qiitVec` (QIIT basics), `id` (the identity family —

docs/NovaElaboration.txt

@@ -111,7 +111,7 @@ fixity ::= infixl d op | infixr d op          # d a digit 0-9
 # Types. Elaboration needs no rule keywords and no context prefixes —
 # the context is always implicit in where a subterm sits.
 T{4} ::= 𝟘 | 𝟙 | ℕ | 𝕌 | Ω | x | (T{≥0})
-T{2} ::= El t{≥4} | Prf t{≥4}
+T{2} ::= El t{≥4} | Prf t{≥4} | ν F{≥2}
 T{1} ::= ((x:T{≥0}))+ → T{≥0} | ((x:T{≥0}))+ ⨯ T{≥0}
        | T{≥1½} / (x y. t{≥1})
 T{1½} ::= T{≥2} ⊎ T{≥1½}
@@ -139,6 +139,9 @@ T{0} ::= t{≥2} ≡ t{≥2} ∈ T{≥1}
 #   2. ℕ-elim and quot-elim take their motives inline, motive-first.
 #      Motives are not inferable without higher-order unification, so
 #      they are mandatory syntax here.
+#   3. corec takes its state CARRIER inline, as a binder annotation —
+#      corec (x : a. f) u — the carrier code is not recoverable from
+#      the expected ν-type, so it is mandatory syntax, like a motive.
 t{5} ::= x | () | Z | ⋆ | ∥T{≥0}∥ | 𝟘 | 𝟙 | ℕ | (t{≥0}) | (t{≥0} : T{≥0})
 t{3} ::= t{≥3} t{≥4} | t{≥3} .π₁ | t{≥3} .π₂                 (left-assoc)
 t{2} ::= λx. t{≥1½}
@@ -151,6 +154,13 @@ t{2} ::= λx. t{≥1½}
                                                               #   right case, scrutinee
        | class t{≥4}
        | quot-elim (z. T{≥0}) (a. t{≥0}) t{≥4}                # motive, case fn, scrutinee
+       | ν F{≥2}                                              # the ν CODE (⇒ 𝕌)
+       | out t{≥4}
+       | corec (x : t{≥0}. t{≥0}) t{≥4}                       # carrier code + coalgebra
+                                                              #   body (one binder), seed
+       | coind (x y. t{≥0}) t{≥4} (x y h. t{≥0})              # invariant, endpoint proof,
+                                                              #   one-step closure — see
+                                                              #   e-coind
        | squash-elim t{≥4} (x. t{≥0})               # el-squash-e-prf: eliminate a
                                                      #   proof of a squash into a
                                                      #   further proposition
@@ -173,6 +183,15 @@ t{1¼} ::= t{≥1½} ⊎ t{≥1¼}            # the ⊎ code — tighter than th
 t{1½} ::= t{≥2} (op t{≥2})*     # declared infix operators, by fixity
 t{0} ::= t{≥1} , t{≥0}                                        (right-assoc)
 
+# Polynomials (the one-hole codes of Foundation's coinductive
+# section). The hole is 𝕏; external pieces are element-level CODES.
+# ⊎ binds tighter than ⨯, as everywhere; the binder forms mirror the
+# type-level binder groups (a left-hand (x:t) BINDS x in the body):
+F{2} ::= 𝕏 | K t{≥4} | (F{≥0})
+F{1½} ::= F{≥2} ⊎ F{≥1½}
+F{1} ::= F{≥1½} ⨯ F{≥1} | ((x:t{≥0}))+ ⨯ F{≥1} | ((x:t{≥0}))+ → F{≥1}
+F{0} ::= F{≥1}
+
 # Name-dropping sugar: `A → B` for `(_:A) → B`, `A / R` for
 # `A / (_ _. R)`, `_` in any binder.
 
@@ -289,13 +308,14 @@ instead an error asking the user for an ascription or annotation.
 whnf(–) is weak-head normalization by Foundation's ≜ rules:
 el-pi-beta, el-sigma-beta₁, el-sigma-beta₂, el-nat-beta-z,
 el-nat-beta-s, el-sum-beta₁, el-sum-beta₂, el-quot-beta,
-el-qiit-beta (the eliminator at a
+el-nu-beta (out at a corec head — map_𝔽 and hᵉˡ expanding by
+Foundation's ≜-clauses), el-qiit-beta (the eliminator at a
 saturated constructor of the nf-identical signature),
 el-sig-beta/ty-sig-beta (signature
 unfolding — for DEFINITION entries; a declaration reference is stuck
 by design, el-sig-decl/ty-sig-decl, and constraint entries are
 nameless and never referenced), and the El-decoding family (ty-el-zero, ty-el-one,
-ty-el-nat, ty-el-pi, ty-el-sigma, ty-el-sum, ty-el-eq, ty-el-quot — the last
+ty-el-nat, ty-el-pi, ty-el-sigma, ty-el-sum, ty-el-nu, ty-el-eq, ty-el-quot — the last
 decoding El (A / r) ≜ El A / r, the Ω-valued relation passing through
 undecoded — and ty-el-qiit, El (𝒮.𝕤 ē) ≜ 𝒮.𝕤 ē; Prf ∥A∥ has no
 decoding rule). Per
@@ -339,6 +359,21 @@ never an unsound acceptance.
 ------------------------------ (e-ty-quot)                    # (A / r)
 Γ ⊢ T / (x y. r) ⇝ A / r̂ type
 
+Γ ⊢ F ⇝ 𝔽 poly
+-------------------------- (e-ty-nu)                          # (ν 𝔽)
+Γ ⊢ ν F ⇝ ν 𝔽 type
+
+# Polynomial elaboration Γ ⊢ F ⇝ 𝔽 poly — structural, each external
+# piece a code, the context growing under the binder forms
+# (Foundation's poly-* rules):
+
+Γ ⊢ 𝕏 ⇝ 𝕏 poly                                    (e-poly-hole)
+Γ ⊢ t ⇐ 𝕌 ⇝ a   ⟹   Γ ⊢ K t ⇝ K a poly           (e-poly-const)
+componentwise at F ⨯ G and F ⊎ G                  (e-poly-prod, e-poly-sum)
+Γ ⊢ t ⇐ 𝕌 ⇝ a   Γ ▷ x:El a ⊢ F ⇝ 𝔽 poly
+   ⟹   Γ ⊢ (x:t) ⨯ F ⇝ El a ⨯ 𝔽 poly             (e-poly-sigma)
+   ⟹   Γ ⊢ (x:t) → F ⇝ El a → 𝔽 poly             (e-poly-pi)
+
 Γ ⊢ p ⇐ Ω ⇝ p̂
 ------------------- (e-ty-prf)                                # (Prf p)
 Γ ⊢ Prf p ⇝ Prf p̂ type
@@ -411,6 +446,12 @@ never an unsound acceptance.
 # no side condition beyond the branches themselves — β covers both
 # injections, so unlike quot-elim there is no well-definedness premise
 
+Γ ⊢ t ⇒ C ⇝ t̂        whnf(C) = ν 𝔽
+------------------------------------------ (e-out)
+Γ ⊢ out t ⇒ El ⌊𝔽⌋(ν 𝔽) ⇝ out t̂           # (out t)
+# fully inference-driven, like the projections: no motive, the
+# polynomial read off the scrutinee's whnf type
+
 Γ ⊢ q ⇒ C ⇝ q̂        whnf(C) = A / r
 Γ ▷ z:(A / r) ⊢ T ⇝ B type
 Γ ▷ a:A ⊢ f ⇐ B[↑, class ☐₀] ⇝ f̂
@@ -445,6 +486,10 @@ never an unsound acceptance.
 Γ ⊢ t / (x y. r) ⇒ 𝕌 ⇝ a / r̂                                  # (A / r : 𝕌)
    # the relation is checked at Ω, not 𝕌
 
+Γ ⊢ F ⇝ 𝔽 poly
+------------------------ (e-code-nu)                          # (ν 𝔽 : 𝕌)
+Γ ⊢ ν F ⇒ 𝕌 ⇝ ν 𝔽
+
 Γ ⊢ T ⇝ A type        Γ ⊢ t₀ ⇐ A ⇝ a₀        Γ ⊢ t₁ ⇐ A ⇝ a₁
 --------------------------------------------------------------- (e-eq)
 Γ ⊢ t₀ ≡ t₁ ∈ T ⇒ Ω ⇝ (a₀ ≡ a₁ ∈ A)                # (a₀ ≡ a₁ ∈ A : Ω)
@@ -483,6 +528,35 @@ whnf(C) = A / r        Γ ⊢ a ⇐ A ⇝ â
 -------------------------------------- (e-class)              # (class a)
 Γ ⊢ class a ⇐ C ⇝ class â
 
+whnf(C) = ν 𝔽        Γ ⊢ t ⇐ 𝕌 ⇝ a
+Γ ▷ x:El a ⊢ f ⇐ El ⌊𝔽⌋(a)[↑] ⇝ f̂        Γ ⊢ u ⇐ El a ⇝ û
+------------------------------------------------------------ (e-corec)
+Γ ⊢ corec (x : t. f) u ⇐ C ⇝ corec 𝔽 a f̂ û    # (corec 𝔽 a f x)
+# checking-only, like λ and class: the polynomial comes from the
+# expected type. In ⇒ position, ascribe.
+
+whnf(C) = Prf p    whnf(p) = (l ≡ r ∈ E)    whnf(E) = ν 𝔽
+Γ ▷ x:ν 𝔽 ▷ y:(ν 𝔽)[↑] ⊢ R ⇐ Ω ⇝ R̂
+Γ ⊢ p ⇐ Prf R̂[id, l, r] ⇝ p̂
+Γ ▷ x:ν 𝔽 ▷ y:(ν 𝔽)[↑] ▷ h:Prf R̂ ⊢ q ⇐ Prf (lift_𝔽(R̂) (out ☐₂) (out ☐₁)) ⇝ q̂
+------------------------------------------------------------ (e-coind)
+Γ ⊢ coind (x y. R) p (x y h. q) ⇐ C ⇝ ⋆
+# el-nu-coind's surface form: the core term is ⋆; the invariant,
+# endpoint proof and closure ship in the skeleton payload
+# (docs/NovaKernel.txt §8). The closure's expected type is the
+# RELATOR at the generic observations — its sub-goals surface as
+# ordinary obligations, dischargeable by the usual loop. Two engine
+# facts make the closure proofs ergonomic: (1) a GROUND hypothesis
+# whose type is a (possibly dependent) Σ-tree of Prf-equalities
+# licenses one rewrite candidate per component, the proof element
+# being the projection chain (el-reflect takes any Prf-typed term) —
+# the shape squash-elim binds for conjunction/existential
+# invariants; (2) a VARIABLE-DEFINITION hypothesis — ☐ₙ ≡ t with ☐ₙ
+# not in t — is admitted as a rewrite rule even when size-increasing
+# (each application strictly removes an occurrence, so it
+# terminates): the "this variable is that machine" pattern every
+# graph invariant produces.
+
 whnf(C) = Prf p        p evident: whnf(p) = ∥A∥ with whnf(A) = 𝟙
                         (witness ()), or whnf(p) = (l ≡ r ∈ A) with
                         Γ ⊢ l ≐ r : A ↓ (el-eq-i)