diff --git a/.claude/skills/nova/SKILL.md b/.claude/skills/nova/SKILL.md index f42c1c2..47c0821 100644 --- a/.claude/skills/nova/SKILL.md +++ b/.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 — diff --git a/docs/NovaElaboration.txt b/docs/NovaElaboration.txt index 398fb60..4951a32 100644 --- a/docs/NovaElaboration.txt +++ b/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) diff --git a/docs/NovaFoundation.txt b/docs/NovaFoundation.txt index d6dbb51..806a8ab 100644 --- a/docs/NovaFoundation.txt +++ b/docs/NovaFoundation.txt @@ -1,7 +1,7 @@ ////////// Preface ////////// -#! highlight keywords: ⊦ : ; , · [ ] ‖ .π₁ .π₂ ∈ ∋ ≐ ≜ ≔ ⇒ ⇐ = ⬡ ⬦ ▷ ◁ ⇛ ⇑ 𝕚𝕕 El U ☐ ε ↑ ∘ ⁺ id λ → ⨯ ⊎ ≡ ∥ / Ω 𝕌 ℕ 𝟘 𝟙 Z S ⋆ Prf class inj₁ inj₂ ⌊ ⌋ ⟦ ⟧ ⋈ ⋉ ᴰ 𝟘-elim ℕ-elim quot-elim squash-elim ⊎-elim -elim qctx qty qsig ctx type tel mot dalg eprob sect norm small sig nf qpath -#! highlight tos: 𝔄 𝔅 𝕥 𝕦 𝕧 𝕤 𝕔 𝕜 𝕘 𝕒 𝕓 𝕞 Φ 𝒮 ς 𝔎 +#! highlight keywords: ⊦ : ; , · [ ] ‖ .π₁ .π₂ ∈ ∋ ≐ ≜ ≔ ⇒ ⇐ = ⬡ ⬦ ▷ ◁ ⇛ ⇑ 𝕚𝕕 El U ☐ ε ↑ ∘ ⁺ id λ → ⨯ ⊎ ≡ ∥ / Ω 𝕌 ℕ 𝟘 𝟙 Z S ⋆ Prf class inj₁ inj₂ ⌊ ⌋ ⟦ ⟧ ⋈ ⋉ ᴰ 𝟘-elim ℕ-elim quot-elim squash-elim ⊎-elim -elim qctx qty qsig ctx type tel mot dalg eprob sect norm small sig nf qpath ν 𝕏 K out corec poly map +#! highlight tos: 𝔄 𝔅 𝕥 𝕦 𝕧 𝕤 𝕔 𝕜 𝕘 𝕒 𝕓 𝕞 Φ 𝒮 ς 𝔎 𝔽 𝔾 #! highlight nova: Γ Δ Ξ Σ σ τ δ θ latin #! highlight meta: 𝑤 ρ υ π 𝒞 ℰ #! highlight indexed: ☐ ⬡ ‖ @@ -75,6 +75,14 @@ # constructors are INDUCTIVE (they may relate constructor terms across # indices and participate in the induction). ℕ, (⊎) and (/) are # retained for now. +# * Coinductive types: a second SCHEME, dual to QIITs in its smallest +# useful form — for each POLYNOMIAL 𝔽 (a one-hole strictly positive +# code), the type ν 𝔽, its observation out (the eliminator), its +# corecursor corec (the introduction), β running one observation +# step, and a uniqueness law that is the coinduction principle +# (bisimulation implies equality). Every ν 𝔽 is DERIVABLE (an +# ℕ-indexed limit — see SUBSUMPTION in the coinductive notes); +# the scheme is kept for structural identity and one-step β. ///////////// Syntax /////////////// @@ -129,6 +137,9 @@ T ::= x [e˲] # type in the signature context | 𝒮.𝕤 ē # sort 𝕤 of a QIIT signature 𝒮 at index spine ē # (see "Quotient inductive-inductive types"); 𝒮 is # carried in the type, so QIIT equality is structural + | ν 𝔽 # coinductive type at polynomial 𝔽 (see "Coinductive + # types"); 𝔽 is carried in the type, so ν-equality + # is structural # element t ::= x [e˲] # element in the signature context @@ -169,6 +180,13 @@ t ::= x [e˲] # element in the signature context # content is a judgement — see el-qiit-path) | 𝒮.𝕤-elim ℰ ē t # QIIT eliminator (elimination problem ℰ, indices ē, # eliminee t) — see the QIIT section + | ν 𝔽 # universe code for the coinductive type at 𝔽 + # (every polynomial is small — see "Coinductive types") + | out t # coinductive observation (the ELIMINATOR) + | corec 𝔽 t t t # corecursor (the INTRODUCTION: polynomial, carrier + # code, coalgebra body, seed — 𝔽 and the carrier are + # CARRIED, like ℰ at 𝒮.𝕤-elim: el-nu-beta consumes + # map_𝔽, so the redex must be self-contained) # (type) telescope Δ ::= ε | T ◁ Δ @@ -239,7 +257,7 @@ t ::= x [e˲] # element in the signature context # * NAMES. Every rule carries a canonical name on its inference line, # following one homogeneous scheme — -- — where -# the class is the judgement class (ctx, sub, sub-norm, ty, el, code, +# the class is the judgement class (ctx, sub, sub-norm, ty, el, code, poly, # tel, sp), the former names the connective or constructor, and the # kind distinguishes introduction (i), elimination (e), computation # (beta), uniqueness (eta), congruence (cong), injectivity (inj), @@ -275,9 +293,13 @@ t ::= x [e˲] # element in the signature context Γ ⊦ ℰ : 𝒮 dalg Γ ⊦ 𝒮 qsig (displayed algebra, ℰ = C̄ ; m̄) Γ ⊦ ℰ : 𝒮 eprob Γ ⊦ ℰ : 𝒮 dalg (elimination problem) Γ ⊦ φ : C̄ sect Γ ⊦ C̄ : 𝒮 mot (section candidate) + Γ ⊦ 𝔽 poly Γ ctx (polynomial — see "Coinductive types") # the theory-of-signatures judgements (dual zone Γ ; Φ — Nova zone, # then ToS zone) are defined in the QIIT section; a signature is - # nothing but a well-formed qiit-context. + # nothing but a well-formed qiit-context. Like signatures, + # polynomials are inert syntax with no equality judgement of their + # own: they are compared structurally, per IDENTITY in each scheme's + # section. # A context extension Γ ▷ A presupposes Γ ctx and Γ ⊦ A type, so a # premise stated under Γ ▷ A carries A's well-formedness with it (and @@ -2358,6 +2380,271 @@ e˲ : Γ₁ ⇒ Γ norm --------------------------- (code-squash-cong) # admissible via code-prop-eq + el-ty-coe Γ ⊦ ∥A₀∥ ≐ ∥A₁∥ : Ω +///////// Coinductive types (polynomial codes) ///////// +# +# The dual scheme to QIITs, in its smallest useful form: for each +# POLYNOMIAL 𝔽 — a one-hole strictly positive code, no binders over +# the hole, no internal fixpoints — the rules below license the +# coinductive type ν 𝔽, its observation out (the ELIMINATOR), its +# corecursor corec (the INTRODUCTION), a β-law running one +# observation step, and a uniqueness law (η) that IS the coinduction +# principle. The polarity is Π's, not ℕ's: canonical forms are +# corec-headed, out forces lazily, and elements are compared by +# observation. Like a QIIT signature, 𝔽 is not a Σ-entry and mints +# no names — it is carried by the formers and compared structurally. +# +# THE EXTENSIONAL PAYOFF, dual to the QIIT section's: uniqueness of +# the corecursor is a plain judgemental rule. In intensional +# theories judgemental finality is rejected as undecidable, and +# coinductive equality degenerates into hand-rolled bisimulation +# setoids; here ≐ is already reflection-strong, so el-nu-eta is +# homogeneous with el-qiit-eta — and BISIMULATION IMPLIES EQUALITY +# becomes a corollary rather than a discipline. + +# POLYNOMIALS — grammar. External pieces are CODES, so every +# polynomial is small and ν 𝔽 always has a code (no smallness side +# condition — the grammar enforces it). A left-hand `El a` BINDS a +# Nova variable in its body, exactly as code-sigma/code-pi bind; the +# two product forms are distinguished by their left-hand side (K a +# ⨯ … is the non-binding instance of the same shape). The hole 𝕏 +# never occurs left of a → — strict positivity is GRAMMATICAL, with +# nothing to check (the same decidable-proxy commitment as +# RELAXATION in the QIIT notes: here the semantic condition is that +# 𝔽's operator be monotone on the setoid lattice). + +# polynomial + 𝔽, 𝔾 ::= 𝕏 # the hole + | K a # constant at a code + | 𝔽 ⨯ 𝔾 # product + | 𝔽 ⊎ 𝔾 # sum — onto the native ⊎ + | El a ⨯ 𝔽 # dependent pair over external data + # (binds a NOVA variable) + | El a → 𝔽 # exponent with external domain + # (binds a NOVA variable) + +Γ ctx +--------------- (poly-hole) +Γ ⊦ 𝕏 poly + +Γ ⊦ a : 𝕌 +---------------- (poly-const) +Γ ⊦ K a poly + +Γ ⊦ 𝔽 poly Γ ⊦ 𝔾 poly +---------------------------- (poly-prod) +Γ ⊦ 𝔽 ⨯ 𝔾 poly + +Γ ⊦ 𝔽 poly Γ ⊦ 𝔾 poly +---------------------------- (poly-sum) +Γ ⊦ 𝔽 ⊎ 𝔾 poly + +Γ ⊦ a : 𝕌 Γ ▷ El a ⊦ 𝔽 poly +---------------------------------- (poly-sigma) +Γ ⊦ El a ⨯ 𝔽 poly + +Γ ⊦ a : 𝕌 Γ ▷ El a ⊦ 𝔽 poly +---------------------------------- (poly-pi) +Γ ⊦ El a → 𝔽 poly + +# REFLECTION ⌊𝔽⌋(c) — the code with the hole filled by Γ ⊦ c : 𝕌 +# (≜-defined by meta-level induction on 𝔽, like the QIIT ⌊·⌋; c +# weakens under the binders): + + ⌊𝕏⌋(c) ≜ c + ⌊K a⌋(c) ≜ a + ⌊𝔽 ⨯ 𝔾⌋(c) ≜ ⌊𝔽⌋(c) ⨯ ⌊𝔾⌋(c)[↑] # code-sigma, non-dependent + ⌊𝔽 ⊎ 𝔾⌋(c) ≜ ⌊𝔽⌋(c) ⊎ ⌊𝔾⌋(c) # code-sum, direct + ⌊El a ⨯ 𝔽⌋(c) ≜ a ⨯ ⌊𝔽⌋(c[↑]) + ⌊El a → 𝔽⌋(c) ≜ a → ⌊𝔽⌋(c[↑]) + +# FUNCTORIAL ACTION map_𝔽 — for Γ ⊦ g : El c₀ → El c₁, a function +# term Γ ⊦ map_𝔽 g : El ⌊𝔽⌋(c₀) → El ⌊𝔽⌋(c₁), ≜-defined by +# meta-level induction on 𝔽 (clauses written applied; at the binding +# formers the recursion proceeds at the instantiated body and g +# weakens under the binder; the sum clause is ⊎-elim at constant +# motive): + + map_𝕏 g x ≜ g x + map_{K a} g x ≜ x + map_{𝔽 ⨯ 𝔾} g p ≜ (map_𝔽 g (p .π₁) , map_𝔾 g (p .π₂)) + map_{𝔽 ⊎ 𝔾} g s ≜ ⊎-elim (inj₁ (map_𝔽 g[↑] ☐₀)) (inj₂ (map_𝔾 g[↑] ☐₀)) s + map_{El a ⨯ 𝔽} g p ≜ (p .π₁ , map_𝔽 g (p .π₂)) + map_{El a → 𝔽} g f ≜ λ (map_𝔽 g[↑] (f[↑] ☐₀)) + +# The FUNCTOR LAWS — map_𝔽 (λ ☐₀) ≐ λ ☐₀ and +# map_𝔽 (g₁ ∘ g₀-composite) ≐ map_𝔽 g₁ ∘ map_𝔽 g₀ pointwise — are +# derivable per polynomial by meta-level induction on 𝔽, each +# instance an ordinary internal equation (β, η and ⊎-eta per +# former). + +# IDENTITY (structural). ν 𝔽 carries its polynomial; two ν-types +# are equal exactly when their polynomials are — nameless indexed +# syntax, compared componentwise (embedded Nova pieces by the +# existing congruence/injectivity rules), iso-recursive: the +# comparison never unfolds the fixpoint into its body. ν 𝔽 and +# El ⌊𝔽⌋(ν 𝔽) are ISOMORPHIC (out one way; the derivable in below +# the other) and deliberately never ≐ — same commitment as the QIIT +# IDENTITY paragraph. Congruence and injectivity are structural, by +# that meta-recursion (code-nu-cong/-inj are the componentwise +# instances, not stated per former). + +# FORMATION. Every polynomial names a small type: + +Γ ⊦ 𝔽 poly +--------------- (ty-nu) +Γ ⊦ ν 𝔽 type + +Γ ⊦ 𝔽 poly +--------------- (code-nu) +Γ ⊦ ν 𝔽 : 𝕌 + +Γ ⊦ 𝔽 poly +--------------------------- (ty-el-nu) +Γ ⊦ El (ν 𝔽) ≜ ν 𝔽 type + +# ELIMINATION — the observation. A sort of this scheme has no +# constructor canonical forms; out is the only way to consume it, +# and the only computation is β below (out of a neutral is +# neutral): + +Γ ⊦ 𝔽 poly Γ ⊦ t : ν 𝔽 +------------------------------ (el-nu-e) +Γ ⊦ out t : El ⌊𝔽⌋(ν 𝔽) + +# INTRODUCTION — the corecursor: any coalgebra maps in. The +# polynomial 𝔽 and the carrier code a are CARRIED by the term (like +# ℰ at 𝒮.𝕤-elim — β consumes map_𝔽, so the redex is +# self-contained); f is the coalgebra body, x the seed. Write +# hᵉˡ ≜ λ (corec 𝔽 a f[↑] ☐₀) for the corecursor as a function term +# (cf. φᵉˡ at el-qiit-beta): + +Γ ⊦ 𝔽 poly Γ ⊦ a : 𝕌 +Γ ▷ El a ⊦ f : El ⌊𝔽⌋(a)[↑] +Γ ⊦ x : El a +------------------------------ (el-nu-i) +Γ ⊦ corec 𝔽 a f x : ν 𝔽 + +# COMPUTATION (β) — observing a corecursive value runs the +# coalgebra one step and re-wraps the recursive positions: + +Γ ⊦ 𝔽 poly Γ ⊦ a : 𝕌 +Γ ▷ El a ⊦ f : El ⌊𝔽⌋(a)[↑] +Γ ⊦ x : El a +------------------------------------------------------------- (el-nu-beta) +Γ ⊦ out (corec 𝔽 a f x) ≜ map_𝔽 hᵉˡ (f[id, x]) : El ⌊𝔽⌋(ν 𝔽) + +# UNIQUENESS (η) — the coinduction principle, el-quot-eta's shape: +# any candidate commuting with the observation IS the corecursor. + +Γ ⊦ 𝔽 poly Γ ⊦ a : 𝕌 +Γ ▷ El a ⊦ f : El ⌊𝔽⌋(a)[↑] +Γ ▷ El a ⊦ h : (ν 𝔽)[↑] +Γ ▷ El a ⊦ out h ≐ map_𝔽 ((λ h)[↑]) f : El ⌊𝔽⌋(ν 𝔽)[↑] +Γ ⊦ x : El a +------------------------------------------------------------- (el-nu-eta) +Γ ⊦ h[id, x] ≐ corec 𝔽 a f x : ν 𝔽 + +# Corollary (two-candidate form, as at ℕ and ⊎): two maps into ν 𝔽 +# commuting with out through the same coalgebra are equal — chain +# el-nu-eta through the corecursor they both equal. This is the +# internal BISIMULATION-IMPLIES-EQUALITY principle: a bisimulation +# is a coalgebra on its own carrier, and its two projections +# commute. + +# COINDUCTION, RELATIONAL FORM — el-nu-eta's corollary adopted as a +# rule for the kernel's convenience (the el-squash-e-eq precedent: +# ADMISSIBLE, kept because the kernel replays it directly). It needs +# one more ≜-meta-operation, the RELATOR lift_𝔽(R) — the relation +# lifting of a polynomial: for Γ ▷ ν 𝔽 ▷ (ν 𝔽)[↑] ⊦ R : Ω and +# elements u, v of ⌊𝔽⌋(ν 𝔽)'s decoding (R's base weakens under every +# binder the clauses cross; its own two binders lift over it): +# +# lift_𝕏(R) u v ≜ R[id, u, v] +# lift_{K a}(R) u v ≜ u ≡ v ∈ El a +# lift_{𝔽 ⨯ 𝔾}(R) u v ≜ ∥Prf (lift_𝔽(R) (u .π₁) (v .π₁)) +# ⨯ Prf (lift_𝔾(R) (u .π₂) (v .π₂))∥ +# lift_{𝔽 ⊎ 𝔾}(R) u v ≜ ⊎-elim at motive Ω, on u then v: +# the diagonal branches lift the +# payloads, the off-diagonal ones are ⊥ +# — definitional collapse at canonical +# forms, the tag mismatch judgementally +# visible +# lift_{El a ⨯ 𝔽}(R) u v ≜ ∥(h : Prf (u .π₁ ≡ v .π₁ ∈ El a)) +# ⨯ Prf (lift_{𝔽[u .π₁]}(R) (u .π₂) (v .π₂))∥ +# # the two instances are ≐ under h by +# # el-reflect — no transport, the same +# # extensional degeneration as the +# # QIIT ᴰ-clauses +# lift_{El a → 𝔽}(R) u v ≜ ∥(x : El a) → Prf (lift_𝔽(R) (u x) (v x))∥ + +Γ ⊦ 𝔽 poly +Γ ▷ ν 𝔽 ▷ (ν 𝔽)[↑] ⊦ R : Ω +Γ ⊦ p : Prf R[id, t₀, t₁] +Γ ▷ ν 𝔽 ▷ (ν 𝔽)[↑] ▷ Prf R ⊦ q : Prf (lift_𝔽(R) (out ☐₂) (out ☐₁)) +Γ ⊦ t₀ : ν 𝔽 Γ ⊦ t₁ : ν 𝔽 +------------------------------------------------------------------- (el-nu-coind) +Γ ⊦ t₀ ≐ t₁ : ν 𝔽 + +# DERIVATION (why admissible). From R build the subset carrier +# b ≜ (νᶜ ⨯ νᶜ) ⨯ prf R — νᶜ the ν-code, prf the derivable prf-code +# of the Ω block's impredicativity note — with the coalgebra +# observing the FIRST component, the closure q transporting the +# invariant to the tails; both projections commute with out (the +# second by q's head equations, reflected), so el-nu-eta equates +# them through the corecursor, and instantiating at (t₀, t₁, p) +# gives the conclusion. The kernel replays the rule as stated +# instead (a ⋆-payload — docs/NovaKernel.txt §8): the subset-carrier +# construction is the JUSTIFICATION, not the implementation. + +# SUBSTITUTION ACTION. Substitution acts through the carried +# polynomial (𝔽[σ] the evident meta-operation: σ on the embedded +# Nova pieces, lifted under the binders; the hole is inert): +# (ν 𝔽)[σ] ≜ ν 𝔽[σ] (type and code) +# (out t)[σ] ≜ out t[σ] +# (corec 𝔽 a f x)[σ] ≜ corec 𝔽[σ] a[σ] f[σ⁺] x[σ] + +# NOTES. +# * LAMBEK. in ≜ λ (corec 𝔽 ⌊𝔽⌋(ν 𝔽) (map_𝔽 (λ (out ☐₀)) ☐₀) ☐₀) +# inverts out +# up to ≐ — out ∘ in by el-nu-beta plus the functor laws, +# in ∘ out by el-nu-eta — so ν 𝔽 ≅ El ⌊𝔽⌋(ν 𝔽) elementwise, +# while the TYPES stay structurally distinct (IDENTITY above). +# * SUBSUMPTION (conservativity). Every ν 𝔽 is definable: with +# F̂ⁿ(𝟙) : 𝕌 by ℕ-elim at motive 𝕌, the ℕ-indexed limit +# (g : ℕ → El (F̂ⁿ 𝟙)-family) ⨯ Prf (restriction coherence) +# is a final 𝔽-coalgebra — containers preserve this limit — with +# out, corec and both laws provable (β up to lemmas, η by +# ℕ-induction and funext-via-reflection). The scheme is retained +# for structural identity, one-step β, and the uniform η; the +# encoding is its justification, exactly as the QIIT SEMANTICS +# note is for that scheme. +# * SEMANTICS. In the setoid model the carrier of ν 𝔽 is the +# meta-level limit above (the descending chain of the monotone +# operator, converging at ω), and the relation is the LARGEST +# BISIMULATION — el-nu-eta is finality, validated on the nose. +# Models that fail finality are hereby excluded, as models +# failing initiality are by the QIIT notes. +# * DELIBERATE OMISSIONS, each with a known upgrade path: no +# internal fixpoints in the grammar (interleaved nesting like +# ν of X ↦ A ⨯ List X needs the inner functor reified to +# shape-and-positions form by hand; non-interleaved nesting is +# free through K-constants at previously formed ν/QIIT codes); +# no indexed or mutual coinductive sorts and no coequations +# (those want the full dual theory of cosignatures); no ν under +# a QIIT constructor domain (an inner ν forces infinitary +# branching, which the finitary ToS grammar excludes). +# +# EXAMPLES. +# Stream a ≜ ν (K a ⨯ 𝕏) +# Conat ≜ ν (K 𝟙 ⊎ 𝕏) +# Colist a ≜ ν (K 𝟙 ⊎ (K a ⨯ 𝕏)) +# Cotree a ≜ ν (K 𝟙 ⊎ (K a ⨯ (𝕏 ⨯ 𝕏))) # leaf/node infinite trees +# Moore a b ≜ ν (K b ⨯ (El a → 𝕏)) +# head, tail, and friends are out followed by projections and +# ⊎-elim; constructors (cons, and Cotree's leaf/node) are in +# instances. Surface codata declarations elaborate to +# ν-polynomials — docs/NovaElaboration.txt's business. + ///////// Rules (elem list) ///////// Γ ctx @@ -2421,5 +2708,7 @@ e˲ : Γ₁ ⇒ Γ norm # Names follow -- uniformly (see Conventions). # The equivalence schema instances are ctx-refl/-sym/-trans, sub-…, -# sub-norm-…, ty-…, el-…, tel-…, sp-…. All other names appear verbatim -# on their rules; there are no synonyms. +# sub-norm-…, ty-…, el-…, tel-…, sp-…. The poly class has +# well-formedness rules only (polynomials are inert syntax, no +# equality judgement). All other names appear verbatim on their +# rules; there are no synonyms. diff --git a/docs/NovaKernel.txt b/docs/NovaKernel.txt index ebc7907..d6d7411 100644 --- a/docs/NovaKernel.txt +++ b/docs/NovaKernel.txt @@ -31,6 +31,8 @@ kernel-only judgement forms added: Σ; Γ ⊦ t ⇒ T ⟨sk⟩ item-level inference Σ; Γ ⊦ T type ⟨sk⟩ item-level formation Σ; Γ ⊦ 𝒮 qsig ⟨sk⟩ item-level QIIT signature checking (§8) + Σ; Γ ⊦ 𝔽 poly ⟨sk⟩ item-level polynomial checking (inside + ν formation — Foundation's poly-* rules) Every kernel judgement is decided inside a FUEL MONAD: a computation either returns, fails with a reason, or exhausts its fuel — and fuel @@ -54,6 +56,11 @@ of fuel, are exactly: ⊎-elim l r (inj₁ a) ≜ l[id, a] # el-sum-beta₁ ⊎-elim l r (inj₂ b) ≜ r[id, b] # el-sum-beta₂ quot-elim f (class a) ≜ f[id, a] # el-quot-beta + out (corec 𝔽 a f x) ≜ map_𝔽 hᵉˡ f[id, x] # el-nu-beta; map_𝔽 and + # hᵉˡ = λ (corec 𝔽 a f[↑] ☐₀) + # expand by Foundation's + # ≜-clauses at contraction + # time (one fuel unit) 𝒮.𝕤-elim ℰ ē (𝒮′.𝕔 θ) ≜ m_𝕔 θ⟨φᵉˡ⟩ # el-qiit-beta; fires # only when 𝒮 and 𝒮′ are # IDENTICAL after nf @@ -68,6 +75,7 @@ of fuel, are exactly: El (a ⊎ b) ≜ El a ⊎ El b El (a / r) ≜ El a / r # the Ω-valued relation is NOT decoded El (𝒮.𝕤 ē) ≜ 𝒮.𝕤 ē # ty-el-qiit + El (ν 𝔽) ≜ ν 𝔽 # ty-el-nu Ω adds exactly ONE contraction clause: @@ -167,6 +175,7 @@ implementation's names): | sigmaCong 𝒞 𝒞 (FSigmaCong) | sumCong 𝒞 𝒞 (FSumCong) | qiitCong 𝒞̄ 𝒞̄ (FQiitCong) + | nuCong 𝒞̄ (FNuCong) The three Ω finals: propext is code-prop-eq — the sides are prop codes and s, t are the two hypothetical implications, CHECKED as typings @@ -203,10 +212,12 @@ Child indexing, shared by paths, the typed descent (§6) and skeletons 𝒮.𝕤 ē (code) → 0.. (the index spine) 𝒮.𝕔 θ → 0.. (the argument spine) 𝒮.𝕤-elim ℰ ē w → 0..n-1 (the index spine), n (the eliminee) + out t → 0 corec 𝔽 a f x → 0, 1(1), 2 + ν 𝔽 (code) → (none) types: A → B → 0, 1(1) A ⨯ B → 0, 1(1) A ⊎ B → 0, 1 El e → 0ᵉ Prf e → 0ᵉ A / r → 0, 1ᵉ(2) x[e˲] → 0..ᵉ - 𝒮.𝕤 ē → 0..ᵉ + 𝒮.𝕤 ē → 0..ᵉ ν 𝔽 → (none) (ᶜ marks universe codes; ᵉ marks descent into an element child, ᵗ into a type child. The quotient relation is an Ω-valued element child. A carried signature 𝒮 and eliminator problem ℰ have NO child indices — @@ -240,7 +251,9 @@ a generic lemma's 𝕌-parameter materialized at a concrete code is a legitimate spine argument — and so does a small signature's sort code, its index spine checked positionally against the reflected arity: - Σ; Γ ⊦ ℕc ⇒ᵖ 𝕌 (likewise 𝟘c, 𝟙c; Π/Σ/⊎/quot/≡ codes componentwise) + Σ; Γ ⊦ ℕc ⇒ᵖ 𝕌 (likewise 𝟘c, 𝟙c; Π/Σ/⊎/quot/≡ codes componentwise; + a ν code checks its polynomial's embedded pieces at 𝕌 + in binder order, the context growing under El-binders) 𝒮 small 𝒮(𝕜) = 𝔄 ending in U Σ; Γ ⊦ ē ⇐ᵖ ⌊𝔄⌋ᵗ (entrywise) -------------------------------------------------------------- @@ -274,6 +287,15 @@ introduction forms structurally and falls back to infer-and-compare: # A1, see §9): the instance of # el-sum-e with motive T[↑] + Σ; Γ ⊦ t ⇒ᵖ Tt nf(Tt) ⇓ ν 𝔽 + -------------------------------------- # el-nu-e: fully + Σ; Γ ⊦ out t ⇒ᵖ El ⌊𝔽⌋(ν 𝔽) # inference-driven + + nf(T) ⇓ ν 𝔽 (the term's carried 𝔽 nf-identical to nf(T)'s) + Σ; Γ ⊦ a ⇐ᵖ 𝕌 Σ; Γ ▷ El a ⊦ f ⇐ᵖ El ⌊𝔽⌋(a)[↑] Σ; Γ ⊦ x ⇐ᵖ El a + -------------------------------------------------------------------- + Σ; Γ ⊦ corec 𝔽 a f x ⇐ᵖ T # el-nu-i + nf(T) ⇓ 𝒮.𝕤 ē 𝒮(𝕔) = 𝔄 ending in El (𝕤 ī) Σ; Γ ⊦ θ ⇐ᵖ ⌊𝔄⌋ᵗ (entrywise) nf(⌊ī⌋[θ]) = nf(ē) -------------------------------------------------- # el-qiit-intro: @@ -430,6 +452,9 @@ type E; — means undetermined): x[e˲] child i : Δᵢ[e˲ prefix] # the telescope entry's type class a child 0 : A when nf(E) ⇓ A / r quot-elim f q child 0 : —, child 1 : ⇒ᴺ(q) + out t child 0 : ⇒ᴺ(t) + corec 𝔽 a f x child 0 : 𝕌, child 1 : — # carrier-dependent (like + child 2 : El a # quot-elim's case function) 𝒮.𝕤 ē (code) child i : entry i of ⌊𝔎⌋ᵗ, instantiated by the preceding children (𝒮(𝕤) = 𝔎) 𝒮.𝕔 θ child i : entry i of ⌊𝔄⌋ᵗ, likewise (𝒮(𝕔) = 𝔄) @@ -505,7 +530,14 @@ componentwise: domain certificate, then codomain certificate under the RIGHT domain — needed exactly when a component's equality is itself extensional, e.g. a Prf codomain equal only by propext), sumCong 𝒞 𝒞 (ty-sum-cong, componentwise — both components over Γ, -no binder to cross), and +no binder to cross), +nuCong 𝒞̄ (both sides ν types/codes ν 𝔽₀ / ν 𝔽₁: the polynomials must +be identical one-hole syntax up to their embedded Nova pieces — former +shapes and binder structure compared syntactically — with each aligned +pair of embedded pieces replayed by its certificate, in the Nova-zone +context accumulated from the binders passed. Foundation's structural ν +congruence, stated there by meta-recursion; the same final closes a +CODE equation ν 𝔽₀ ≐ ν 𝔽₁ : 𝕌 in element replay), and qiitCong 𝒞̄p 𝒞̄i (both sides sort applications 𝒮₀.𝕤 ē₀ / 𝒮₁.𝕤 ē₁ AT THE SAME SORT POSITION: 𝒮₀ and 𝒮₁ must be identical nameless ToS syntax up to their embedded Nova pieces — positions, entry shapes, binder @@ -577,6 +609,23 @@ Checking Σ; Γ ⊦ t ⇐ T ⟨sk⟩ : Σ; Γ ⊦ ⋆ ⇐ T ⟨sk⟩ # el-eq-i over replay # disambiguated from the squash rules below by nf(T)'s prop head + el-nu-coind rides ⋆ too — COINDUCTION at an equality prop over a + ν-type, the payload carrying the invariant, the endpoint proof and + the one-step closure, each with its skeleton (all three are checked + terms, not replay certificates — the premises are prop + inhabitations, exactly the item-level checker's job): + + nf(T) ⇓ Prf p nf(p) ⇓ (l ≡ r ∈ E) nf(E) ⇓ ν 𝔽 + sk carries coind R ⟨skR⟩, p̂ ⟨skp⟩, q̂ ⟨skq⟩ + Σ; Γ ▷ ν 𝔽 ▷ (ν 𝔽)[↑] ⊦ R ⇐ Ω ⟨skR⟩ + Σ; Γ ⊦ p̂ ⇐ Prf R[id, l, r] ⟨skp⟩ + Σ; Γ ▷ ν 𝔽 ▷ (ν 𝔽)[↑] ▷ Prf R ⊦ q̂ ⇐ Prf (lift_𝔽(R) (out ☐₂) (out ☐₁)) ⟨skq⟩ + ------------------------------------------------------------------- + Σ; Γ ⊦ ⋆ ⇐ T ⟨sk⟩ # el-nu-coind + # lift_𝔽 is the RELATOR (Foundation, coinductive section) — + # KERNEL-computed from 𝔽 and R, like out's result type; the + # closure's type is the rule's shape, never elaborator-supplied + nf(T) ⇓ A ⊎ B Σ; Γ ⊦ a ⇐ A ⟨sk.0⟩ ------------------------------------- # el-sum-i₁ Σ; Γ ⊦ inj₁ a ⇐ T ⟨sk⟩ (inj₂ analogously at B) @@ -585,6 +634,12 @@ Checking Σ; Γ ⊦ t ⇐ T ⟨sk⟩ : ------------------------------------- # el-quot-i Σ; Γ ⊦ class a ⇐ T ⟨sk⟩ + nf(T) ⇓ ν 𝔽 (the term's carried 𝔽 nf-identical to nf(T)'s) + Σ; Γ ⊦ a ⇐ 𝕌 ⟨sk.0⟩ Σ; Γ ▷ El a ⊦ f ⇐ El ⌊𝔽⌋(a)[↑] ⟨sk.1⟩ + Σ; Γ ⊦ x ⇐ El a ⟨sk.2⟩ + ------------------------------------------------------------ + Σ; Γ ⊦ corec 𝔽 a f x ⇐ T ⟨sk⟩ # el-nu-i + nf(T) ⇓ 𝒮.𝕤 ē 𝒮(𝕔) = 𝔄 ending in El (𝕤 ī) Σ; Γ ⊦ θᵢ ⇐ (entry i of ⌊𝔄⌋ᵗ)[θ prefix] ⟨sk.i⟩ (entrywise) nf(⌊ī⌋[θ]) = nf(ē) @@ -660,6 +715,13 @@ Inference Σ; Γ ⊦ t ⇒ T ⟨sk⟩ : Σ; Γ ⊦ quot-elim f q ⇒ M[id, q] # el-quot-e (the well-definedness hypothesis is Prf r — the DECODED relation) + out is fully inference-driven — no motive, no skeleton payload + beyond the scrutinee's: + + Σ; Γ ⊦ t ⇒ Tt ⟨sk.0⟩ nf(Tt) ⇓ ν 𝔽 + ------------------------------------------------------------ + Σ; Γ ⊦ out t ⇒ El ⌊𝔽⌋(ν 𝔽) # el-nu-e + The QIIT eliminator carries its own motives and methods (ℰ = C̄ ; m̄ in the TERM, Foundation's design), so no motive payload is needed — only the coherences, which are equations, arrive as certificates: @@ -695,7 +757,10 @@ Inference Σ; Γ ⊦ t ⇒ T ⟨sk⟩ : ascription payload) is rejected. Formation Σ; Γ ⊦ T type ⟨sk⟩ : structural over the type formers -(ty-pi/sigma/sum/el/prf/quot/ty-prop/ty-sig-var), El's code checked at 𝕌, +(ty-pi/sigma/sum/el/prf/quot/nu/ty-prop/ty-sig-var), El's code checked at 𝕌, +a ν type's polynomial checked structurally (poly-hole/-const/-prod/ +-sum/-sigma/-pi: each embedded code at 𝕌, the context growing under +the El-binders, skeleton children along in binder order), Prf's code and the quotient's relation checked at Ω, signature-type arguments checked against their telescope — all with skeleton children along. A sort @@ -770,7 +835,11 @@ EQUATION REPLAY (A1, A2), and three added by the QIIT extension (coherences as PQCoh certificates, §8). A5 NO η CERTIFICATE FOR QIITs. el-qiit-eta (like el-nat-eta, - el-sum-eta and el-quot-eta before it) has no replay final; + el-sum-eta and el-quot-eta before it) has no replay final; for + ν the gap is CLOSED, by el-nu-coind as a ⋆-payload (§8) — the + admissible relational form, not el-nu-eta itself (whose + candidate h would be a carried higher-order payload; the + relational form subsumes it via graph invariants); uniqueness arguments live in the elaborator as lemmas, not in kernel certificates (an el-sum-eta instance is proven as an ordinary ⊎-elim lemma at an equality motive, β closing both diff --git a/src/idris/Nova/Compute.idr b/src/idris/Nova/Compute.idr index 338aca2..c5d34e0 100644 --- a/src/idris/Nova/Compute.idr +++ b/src/idris/Nova/Compute.idr @@ -170,6 +170,12 @@ mutual Prf p => whnfElem sig p -- code-squash-prf: ∥Prf p∥ ≜ p t' => Squash t' whnfElem sig Star = Star + whnfElem sig (Elem.NuTy f) = Elem.NuTy f + whnfElem sig (Corec p a f x) = Corec p a f x -- co-data: a corec head is canonical + whnfElem sig (Out t) = + case whnfElem sig t of + Corec p a f x => whnfElem sig (mapPoly p (corecFun p a f) (substElem f (Ext Id x))) + _ => assert_total $ idris_crash "whnfElem: out scrutinee is not a corec head (impossible for a closed, well-typed term)" whnfElem sig (QSortC sg k es) = QSortC sg k es whnfElem sig (QCtor sg k es) = QCtor sg k es whnfElem sig (QElim sg k ms fs es w) = @@ -190,6 +196,7 @@ mutual whnfTy sig (Ty.PiTy a b) = Ty.PiTy a b -- co-data whnfTy sig (Ty.SigmaTy a b) = Ty.SigmaTy a b whnfTy sig (Ty.SumTy a b) = Ty.SumTy a b + whnfTy sig (Ty.NuTy f) = Ty.NuTy f whnfTy sig (El e) = case whnfElem sig e of Elem.ZeroTy => Ty.ZeroTy @@ -200,6 +207,7 @@ mutual Elem.SumTy a b => Ty.SumTy (El a) (El b) QuotTy a r => Quotient (El a) r QSortC sg k es => QSort sg k es -- ty-el-qiit + Elem.NuTy f => Ty.NuTy f -- ty-el-nu _ => assert_total $ idris_crash "whnfTy: El argument is not a universe code (impossible for a closed, well-typed term)" whnfTy sig PropTy = PropTy whnfTy sig (Prf e) = Prf e @@ -257,6 +265,9 @@ mutual go (QSortC sg k es) = QSortC sg k (nfSubNorm sig es) -- sg: a bundle of binder telescopes, left alone go (QCtor sg k es) = QCtor sg k (nfSubNorm sig es) go (QElim sg k ms fs es w) = QElim sg k ms fs (nfSubNorm sig es) (nfElem sig w) + go (Elem.NuTy f) = Elem.NuTy f -- 𝔽: embedded pieces partly under binders, left alone + go (Out t) = Out (nfElem sig t) + go (Corec p a f x) = Corec p (nfElem sig a) f (nfElem sig x) -- f: under a binder, left alone ||| T's normal form: whnf, then nf on every immediate subterm that ||| stays in the SAME context (see nfElem). @@ -278,6 +289,7 @@ mutual go (Quotient a r) = Quotient (nfTy sig a) r -- r: under a binder, left alone go (Ty.SigVar x es) = Ty.SigVar x es -- unreachable: whnf always unfolds x[e˲] go (QSort sg k es) = QSort sg k (nfSubNorm sig es) -- sg: a bundle of binder telescopes, left alone + go (Ty.NuTy f) = Ty.NuTy f -- 𝔽 carried, left alone export nfSubNorm : Sig -> SubNorm -> SubNorm diff --git a/src/idris/Nova/Elaboration.idr b/src/idris/Nova/Elaboration.idr index 0932b80..13ce2fa 100644 --- a/src/idris/Nova/Elaboration.idr +++ b/src/idris/Nova/Elaboration.idr @@ -237,6 +237,7 @@ mapRefsSub : (String -> SubNorm -> Maybe Elem) -> SubNorm -> SubNorm mapRefsQTm : (String -> SubNorm -> Maybe Elem) -> QTm -> QTm mapRefsQTy : (String -> SubNorm -> Maybe Elem) -> QTy -> QTy mapRefsQSig : (String -> SubNorm -> Maybe Elem) -> QSig -> QSig +mapRefsPoly : (String -> SubNorm -> Maybe Elem) -> Poly -> Poly mapRefsE : (String -> SubNorm -> Maybe Elem) -> Elem -> Elem mapRefsE f (SigVar x es) = @@ -273,6 +274,9 @@ mapRefsE f (QCtor sg k es) = QCtor (mapRefsQSig f sg) k (mapRefsSub f es) mapRefsE f (QElim sg k ms fs es w) = QElim (mapRefsQSig f sg) k (map (mapRefsT f) ms) (map (mapRefsE f) fs) (mapRefsSub f es) (mapRefsE f w) +mapRefsE f (Elem.NuTy p) = Elem.NuTy (mapRefsPoly f p) +mapRefsE f (Out t) = Out (mapRefsE f t) +mapRefsE f (Corec p a g x) = Corec (mapRefsPoly f p) (mapRefsE f a) (mapRefsE f g) (mapRefsE f x) mapRefsT f Ty.ZeroTy = Ty.ZeroTy mapRefsT f Ty.OneTy = Ty.OneTy @@ -287,6 +291,7 @@ mapRefsT f (Prf e) = Prf (mapRefsE f e) mapRefsT f (Quotient a r) = Quotient (mapRefsT f a) (mapRefsE f r) mapRefsT f (Ty.SigVar x es) = Ty.SigVar x (mapRefsSub f es) mapRefsT f (QSort sg k es) = QSort (mapRefsQSig f sg) k (mapRefsSub f es) +mapRefsT f (Ty.NuTy p) = Ty.NuTy (mapRefsPoly f p) mapRefsSub f [<] = [<] mapRefsSub f (es :< e) = mapRefsSub f es :< mapRefsE f e @@ -303,6 +308,13 @@ mapRefsQTy f (QPiInd u b) = QPiInd (mapRefsQTm f u) (mapRefsQTy f b) mapRefsQSig f = map (mapRefsQTy f) +mapRefsPoly f PHole = PHole +mapRefsPoly f (PConst a) = PConst (mapRefsE f a) +mapRefsPoly f (PProd g h) = PProd (mapRefsPoly f g) (mapRefsPoly f h) +mapRefsPoly f (PSum g h) = PSum (mapRefsPoly f g) (mapRefsPoly f h) +mapRefsPoly f (PSigma a g) = PSigma (mapRefsE f a) (mapRefsPoly f g) +mapRefsPoly f (PPi a g) = PPi (mapRefsE f a) (mapRefsPoly f g) + ||| Every signature name an element references (with duplicates). collectRefsE : Elem -> List String collectRefsE e = go e @@ -310,6 +322,7 @@ collectRefsE e = go e goT : Ty -> List String goQTm : QTm -> List String goQTy : QTy -> List String + goP : Poly -> List String go : Elem -> List String go (SigVar x es) = x :: concatMap go (toList es) go (CtxVar _) = [] @@ -343,6 +356,16 @@ collectRefsE e = go e go (QElim sg k ms fs es w) = concatMap goQTy sg ++ concatMap goT ms ++ concatMap go fs ++ concatMap go (toList es) ++ go w + go (Elem.NuTy p) = goP p + go (Out t) = go t + go (Corec p a f x) = goP p ++ go a ++ go f ++ go x + + goP PHole = [] + goP (PConst a) = go a + goP (PProd f g) = goP f ++ goP g + goP (PSum f g) = goP f ++ goP g + goP (PSigma a f) = go a ++ goP f + goP (PPi a f) = go a ++ goP f goQTm (QVar _) = [] goQTm (QAppE f e) = goQTm f ++ go e @@ -367,6 +390,7 @@ collectRefsE e = go e goT (Quotient a r) = goT a ++ go r goT (Ty.SigVar x es) = x :: concatMap go (toList es) goT (QSort sg k es) = concatMap goQTy sg ++ concatMap go (toList es) + goT (Ty.NuTy p) = goP p ||| ONE δ-step at the head: a definition reference unfolds to its ||| definiens under the spine; anything else is left alone. Used to @@ -425,6 +449,29 @@ qsigDom0Pieces sg0 sg1 = goTy d (QPiInd u b) (QPiInd u' b') = do ignore (goTm u u'); goTy (S d) b b' goTy _ _ _ = Nothing +||| ν identity is STRUCTURAL on the carried polynomial: same shape, the +||| embedded codes compared pairwise. Depth-0 pieces (not under a +||| polynomial binder) come back for decomposition, strengthened; +||| deeper mismatches make the whole comparison conservative (Nothing). +polyDom0Pieces : Poly -> Poly -> Maybe (List (Elem, Elem)) +polyDom0Pieces = goP 0 + where + piece0 : Nat -> Elem -> Elem -> Maybe (List (Elem, Elem)) + piece0 d a a' = + if a == a' then Just [] + else if d == 0 then Just [(a, a')] + else case (strengthenElem d a, strengthenElem d a') of + (Just s0, Just s1) => Just [(s0, s1)] + _ => Nothing + goP : Nat -> Poly -> Poly -> Maybe (List (Elem, Elem)) + goP d PHole PHole = Just [] + goP d (PConst a) (PConst a') = piece0 d a a' + goP d (PProd f g) (PProd f' g') = [| goP d f f' ++ goP d g g' |] + goP d (PSum f g) (PSum f' g') = [| goP d f f' ++ goP d g g' |] + goP d (PSigma a f) (PSigma a' f') = [| piece0 d a a' ++ goP (S d) f f' |] + goP d (PPi a f) (PPi a' f') = [| piece0 d a a' ++ goP (S d) f f' |] + goP _ _ _ = Nothing + ||| Position of the entry binding a name (leftmost/oldest first). sigIndexOf : String -> List SigEntry -> Maybe Nat sigIndexOf q = go 0 @@ -474,6 +521,7 @@ codeOf (Ty.SumTy a b) = Elem.SumTy <$> codeOf a <*> codeOf b -- the relation is an Ω-element in BOTH the type former and the code: -- El (A / R) ≜ El A / R, so it passes through unchanged codeOf (Quotient a r) = QuotTy <$> codeOf a <*> Just r +codeOf (Ty.NuTy f) = Just (Elem.NuTy f) codeOf (El e) = Just e -- code-qiit: a sort's code is the sort former itself (smallness is -- enforced wherever the code is USED — inferP rejects large ones) @@ -678,6 +726,8 @@ condSub k p bs = ||| below). tySize : Ty -> Nat +polySize : Poly -> Nat + elemSize : Elem -> Nat elemSize (CtxVar _) = 1 elemSize (ZeroElim t) = S (elemSize t) @@ -714,6 +764,9 @@ elemSize (QElim _ _ ms fs es w) = S (foldl (\acc, m => acc + tySize m) 0 ms + foldl (\acc, f => acc + elemSize f) 0 fs + foldl (\acc, e => acc + elemSize e) 0 es + elemSize w) +elemSize (Elem.NuTy p) = S (polySize p) +elemSize (Out t) = S (elemSize t) +elemSize (Corec p a f x) = S (polySize p + elemSize a + elemSize f + elemSize x) tySize Ty.ZeroTy = 1 tySize Ty.OneTy = 1 @@ -728,6 +781,14 @@ tySize (Prf e) = S (elemSize e) tySize (Quotient a r) = S (tySize a + elemSize r) tySize (Ty.SigVar _ es) = S (foldl (\acc, e => acc + elemSize e) 0 es) tySize (QSort _ _ es) = S (foldl (\acc, e => acc + elemSize e) 0 es) +tySize (Ty.NuTy p) = S (polySize p) + +polySize PHole = 1 +polySize (PConst a) = S (elemSize a) +polySize (PProd f g) = S (polySize f + polySize g) +polySize (PSum f g) = S (polySize f + polySize g) +polySize (PSigma a f) = S (elemSize a + polySize f) +polySize (PPi a f) = S (elemSize a + polySize f) ||| Equal up to a bijective renaming of the parametric variables ||| (commutativity-shaped) — such equations loop as rewrite rules. @@ -820,10 +881,22 @@ permutative c = isJust (go 0 c.lhs c.rhs []) ||| permutative and growing equations never rewrite). ordered : List Cand -> List Cand ordered cs = - let usable = filter (\c => elemSize c.rhs <= elemSize c.lhs && not (permutative c)) cs + let usable = filter (\c => (elemSize c.rhs <= elemSize c.lhs || varDef c) && not (permutative c)) cs shrinking = filter (\c => elemSize c.rhs < elemSize c.lhs) usable rest = filter (\c => not (elemSize c.rhs < elemSize c.lhs)) usable in shrinking ++ rest + where + -- a VARIABLE-DEFINITION rule — ground, ☐ₙ ⇝ t with ☐ₙ not in t — + -- terminates regardless of size (each application strictly removes + -- an occurrence), so it is usable as a rewrite rule even when + -- growing: the "the hypothesis defines this variable" pattern that + -- coinduction invariants produce + varDef : Cand -> Bool + varDef c = + c.params == 0 && + (case c.lhs of + CtxVar n => isJust (strengthenElem n c.rhs) + _ => False) -- ===== Step materialization ===== -- @@ -958,6 +1031,13 @@ rewriteElemS side c pi d t = descend (QElim sg k ms fs es w) = spineAt es (\es' => QElim sg k ms fs es' w) <|> at (length (toList es)) 0 w (\w' => QElim sg k ms fs es w') + -- ν formers: out's scrutinee and corec's carrier/body/seed are + -- addressable; the carried polynomial is OPAQUE, like a signature + descend (Out t) = at 0 0 t Out + descend (Corec p a f x) = + at 0 0 a (\a' => Corec p a' f x) + <|> at 1 1 f (\f' => Corec p a f' x) + <|> at 2 0 x (\x' => Corec p a f x') descend _ = Nothing rewriteTyS side c pi d Ty.ZeroTy = Nothing @@ -981,6 +1061,9 @@ rewriteTyS side c pi d (El e) = rewriteTyS side c pi d (Quotient a r) = ((\(a', st) => (Quotient a' r, st)) <$> rewriteTyS side c (0 :: pi) d a) <|> ((\(r', st) => (Quotient a r', st)) <$> rewriteElemS side c (1 :: pi) (2 + d) r) +-- a ν type has no child indices: the carried polynomial is OPAQUE to +-- paths, like a carried signature (NovaKernel.txt, child indexing) +rewriteTyS side c pi d (Ty.NuTy f) = Nothing -- QIIT sort application: rewriting reaches the INDEX SPINE; the carried -- signature is OPAQUE to paths (NovaKernel.txt, A3) rewriteTyS side c pi d (QSort sg k es) = @@ -1103,7 +1186,7 @@ closeCand c = ||| against the lemma store, RECORDING the normalization so the kernel ||| can bridge from the raw reflected equation. hypCands : ElabSt -> Ctx -> List Cand -hypCands st ctx = concatMap closeCand (mapMaybe candAt [0 .. minus (length ctx) 1]) +hypCands st ctx = concatMap closeCand (concatMap candsAt [0 .. minus (length ctx) 1]) where lemmaRw : List Cand lemmaRw = ordered st.lemmas @@ -1141,6 +1224,46 @@ hypCands st ctx = concatMap closeCand (mapMaybe candAt [0 .. minus (length ctx) (betaElem st.sig l) (betaElem st.sig r) mk [] []) Nothing => Nothing + -- a GROUND hypothesis whose type is a (nested, non-dependent) Σ of + -- Prf-equalities licenses one candidate per component, the proof + -- element being the projection chain (el-reflect takes any + -- Prf-typed term, so a projection is a legitimate witness). This is + -- the shape squash-elim binds when an invariant is a conjunction. + groundEqCand : Elem -> (Elem, Elem, Ty) -> Cand + groundEqCand prf (l, r, t) = + let (l1, lSteps) = rwNfElemS st.sig lemmaRw True (betaElem st.sig l) + (r1, rSteps) = rwNfElemS st.sig lemmaRw True (betaElem st.sig r) + in MkCand "hypothesis" 0 [] l1 r1 (\_ => Just (prf, [])) (toPSteps lSteps) (toPSteps rSteps) + + pairEqs : Nat -> (proj : Elem) -> Ty -> List (Elem, (Elem, Elem, Ty)) + pairEqs fuel proj ty = + case fuel of + Z => [] + S fuel' => + case betaTy st.sig ty of + Prf p => + case betaElem st.sig p of + Elem.EqTy l r t => [(proj, (l, r, t))] + _ => [] + Ty.SigmaTy a b => + -- dependent Σs instantiate the body at the projection — + -- existential invariants (Σ of data and equations) land here + pairEqs fuel' (SigmaElim1 proj) a ++ + pairEqs fuel' (SigmaElim2 proj) (substTy b (Ext Id (SigmaElim1 proj))) + _ => [] + + candsAt : Nat -> List Cand + candsAt i = + case candAt i of + Just c => [c] + Nothing => + case ctxLookup ctx i of + Just tyI => + case betaTy st.sig tyI of + tyB@(Ty.SigmaTy _ _) => map (uncurry groundEqCand) (pairEqs 8 (CtxVar i) tyB) + _ => [] + Nothing => [] + record CandSet where constructor MkCandSet all : List Cand @@ -1745,6 +1868,14 @@ mutual Left _ => zonkElimStuck st sg k ms fs es (QCtor sgW c theta) else zonkElimStuck st sg k ms fs es (QCtor sgW c theta) w2 => zonkElimStuck st sg k ms fs es w2 + zonkElem st (Elem.NuTy p) = Elem.NuTy (zonkPoly st p) + zonkElem st (Out t) = + case zonkElem st t of + -- el-nu-beta at a corec head + Corec p a f x => zonkElem st (mapPoly p (corecFun p a f) (substElem f (Ext Id x))) + t2 => Out t2 + zonkElem st (Corec p a f x) = + Corec (zonkPoly st p) (zonkElem st a) (zonkElem st f) (zonkElem st x) zonkTy : ElabSt -> Ty -> Ty zonkTy st (Ty.SigVar x es) = @@ -1780,6 +1911,7 @@ mutual case resugarQ st (QSortC zsg k zes) of Just code => El code Nothing => QSort zsg k zes + zonkTy st (Ty.NuTy p) = Ty.NuTy (zonkPoly st p) zonkElimStuck : ElabSt -> QSig -> Nat -> List Ty -> List Elem -> SubNorm -> Elem -> Elem zonkElimStuck st sg k ms fs es w2 = @@ -1806,6 +1938,14 @@ mutual zonkQSig : ElabSt -> QSig -> QSig zonkQSig st = map (zonkQTy st) + zonkPoly : ElabSt -> Poly -> Poly + zonkPoly st PHole = PHole + zonkPoly st (PConst a) = PConst (zonkElem st a) + zonkPoly st (PProd f g) = PProd (zonkPoly st f) (zonkPoly st g) + zonkPoly st (PSum f g) = PSum (zonkPoly st f) (zonkPoly st g) + zonkPoly st (PSigma a f) = PSigma (zonkElem st a) (zonkPoly st f) + zonkPoly st (PPi a f) = PPi (zonkElem st a) (zonkPoly st f) + zonkCtx : ElabSt -> Ctx -> Ctx zonkCtx st [<] = [<] zonkCtx st (rest :< ty) = zonkCtx st rest :< zonkTy st ty @@ -2606,6 +2746,12 @@ mutual Just pieces => traverse_ (\(t0, t1) => ignore $ convTy ctx env site comp' t0 t1) pieces Nothing => assume cur site comp else assume cur site comp + -- ν identity is STRUCTURAL (Foundation, coinductive IDENTITY): + -- same polynomial shape, embedded codes decomposed pairwise + (Ty.NuTy f0, Ty.NuTy f1) => + case polyDom0Pieces f0 f1 of + Just pieces => traverse_ (\(e0, e1) => ignore $ convElem ctx env site comp' e0 e1 Ty.UniverseTy) pieces + Nothing => assume cur site comp (El x, El y) => ignore $ convElem ctx env site comp' x y Ty.UniverseTy (Prf x, Prf y) => ignore $ convElem ctx env site comp' x y Ty.PropTy (El x, rigid) => case codeOf rigid of @@ -2660,6 +2806,24 @@ preferSum st ctx ty = case rwNfTy st ctx ty of tyX@(Ty.SumTy a b) => (\e => (a, b, Just e)) <$> exposeCert st ctx ty tyX _ => Nothing +||| A prop stuck only up to hypothesis rewriting (e.g. the relator's +||| ⊎-elim at neutral observations, unstuck by a variable-definition +||| hypothesis): rewrite it and bridge with an exposure certificate +||| from the ORIGINAL expected type. +exposeProp : ElabSt -> Ctx -> Ty -> Elem -> (Elem, Maybe (Ty, ECert)) +exposeProp st ctx ty p = + let pR = rwNfElem st ctx p in + if pR == p then (p, Nothing) + else case exposeCert st ctx ty (Prf pR) of + Just e2 => (pR, Just e2) + Nothing => (p, Nothing) + +preferNu : ElabSt -> Ctx -> Ty -> Maybe (Poly, Maybe (Ty, ECert)) +preferNu st ctx (Ty.NuTy f) = Just (f, Nothing) +preferNu st ctx ty = case rwNfTy st ctx ty of + tyX@(Ty.NuTy f) => (\e => (f, Just e)) <$> exposeCert st ctx ty tyX + _ => Nothing + preferQuot : ElabSt -> Ctx -> Ty -> Maybe (Ty, Elem, Maybe (Ty, ECert)) preferQuot st ctx (Ty.Quotient a r) = Just (a, r, Nothing) preferQuot st ctx ty = case rwNfTy st ctx ty of @@ -2679,6 +2843,33 @@ withExpose (Just (tyX, c)) sk = addPayload (PExpose tyX c) sk mutual export + ||| Γ ⊢ F ⇝ 𝔽 poly (e-poly-*): each embedded piece a code at 𝕌, the + ||| context growing under the binder forms; skeleton children + ||| accumulate in binder order (the kernel's kCheckPolyK order). + elabPoly : Ctx -> NameEnv -> String -> SPoly -> ElabM (Poly, List Skel) + elabPoly ctx env site SPHole = pure (PHole, []) + elabPoly ctx env site (SPConst a) = do + (a', aSk) <- checkElem ctx env site a Ty.UniverseTy + pure (PConst a', [aSk]) + elabPoly ctx env site (SPProd f g) = do + (f', fSks) <- elabPoly ctx env site f + (g', gSks) <- elabPoly ctx env site g + pure (PProd f' g', fSks ++ gSks) + elabPoly ctx env site (SPSum f g) = do + (f', fSks) <- elabPoly ctx env site f + (g', gSks) <- elabPoly ctx env site g + pure (PSum f' g', fSks ++ gSks) + elabPoly ctx env site (SPSigma (xn, xr) a f) = do + (a', aSk) <- checkElem ctx env site a Ty.UniverseTy + recordBinder xr ctx env xn (El a') + (f', fSks) <- elabPoly (ctx :< El a') (env :< xn) site f + pure (PSigma a' f', aSk :: fSks) + elabPoly ctx env site (SPPi (xn, xr) a f) = do + (a', aSk) <- checkElem ctx env site a Ty.UniverseTy + recordBinder xr ctx env xn (El a') + (f', fSks) <- elabPoly (ctx :< El a') (env :< xn) site f + pure (PPi a' f', aSk :: fSks) + elabTy : Ctx -> NameEnv -> String -> STy -> ElabM (Ty, Skel) elabTy ctx env site STyZero = pure (Ty.ZeroTy, Nd [] []) elabTy ctx env site STyOne = pure (Ty.OneTy, Nd [] []) @@ -2713,6 +2904,10 @@ mutual recordBinder nyr (ctx :< a') (env :< nx) ny (substTy a' Wk) (r', rSk) <- checkElem (ctx :< a' :< substTy a' Wk) (env :< nx :< ny) site r Ty.PropTy pure (Ty.Quotient a' r', Nd [] [aSk, rSk]) + elabTy ctx env site (STyNu f) = do + -- e-ty-nu + (f', fSks) <- elabPoly ctx env site f + pure (Ty.NuTy f', Nd [] fSks) elabTy ctx env site (STyEq l r t) = do -- e-ty-eq: the surface ≡-TYPE elaborates to Prf of the equality -- prop (equality is Ω-valued) @@ -2898,6 +3093,22 @@ mutual (l', lSk) <- checkElem ctx env site l t' (r', rSk) <- checkElem ctx env site r t' pure (Elem.EqTy l' r' t', Ty.PropTy, Nd [] [lSk, rSk, tSk]) + inferElem ctx env site (SNuC f) = do + -- e-code-nu + (f', fSks) <- elabPoly ctx env site f + pure (Elem.NuTy f', Ty.UniverseTy, Nd [] fSks) + inferElem ctx env site (SOut t) = do + -- e-out: fully inference-driven, the polynomial read off the + -- scrutinee's type + (t', tTy, tSk) <- inferElem ctx env site t + st <- getSt + case preferNu st ctx tTy of + Just (p, _) => pure (Out t', El (reflectPoly p (Elem.NuTy p)), Nd [] [tSk]) + Nothing => throw "\{site}: out scrutinee has non-ν type\{structuralHint}" + inferElem ctx env site (SCorec _ _ _ _) = + throw "\{site}: cannot infer the type of corec (the polynomial comes from the expected ν-type)\{structuralHint}" + inferElem ctx env site (SCoind _ _ _ _ _ _ _ _) = + throw "\{site}: cannot infer the type of coind (the equation comes from the expected Prf type)\{structuralHint}" inferElem ctx env site (SInj1 _) = throw "\{site}: cannot infer the type of inj₁ (the other summand is undetermined)\{structuralHint}" inferElem ctx env site (SInj2 _) = @@ -2943,6 +3154,54 @@ mutual (b', bSk) <- checkElem ctx env site b cod pure (Inj2 b', withExpose exp (Nd [] [bSk])) Nothing => throw "\{site}: inj₂ checked against a non-⊎ type\{structuralHint}" + checkElem ctx env site (SCorec (xn, xr) a f u) ty = do + -- e-corec: checking-only, like λ and class + st <- getSt + case preferNu st ctx ty of + Just (p, exp) => do + (a', aSk) <- checkElem ctx env site a Ty.UniverseTy + recordBinder xr ctx env xn (El a') + (f', fSk) <- checkElem (ctx :< El a') (env :< xn) site f + (substTy (El (reflectPoly p a')) Wk) + (u', uSk) <- checkElem ctx env site u (El a') + pure (Corec p a' f' u', withExpose exp (Nd [] [aSk, fSk, uSk])) + Nothing => throw "\{site}: corec checked against a non-ν type\{structuralHint}" + checkElem ctx env site (SCoind (xn, xr) (yn, yr) rS pS (mxn, mxr) (myn, myr) (mhn, mhr) qS) ty = do + -- e-coind: el-nu-coind's surface form, at Prf (l ≡ r ∈ El (ν F)) — + -- invariant, endpoint proof, one-step closure at the relator + st <- getSt + case preferPrf st ctx ty of + Nothing => throw "\{site}: coind checked against a non-Prf type\{structuralHint}" + Just (pc, exp) => do + let pcUse = case pc of + Elem.EqTy _ _ _ => pc + _ => betaElem st.sig pc + case pcUse of + Elem.EqTy l rhs ety => do + let fM = case whnfT st.sig ety of + Ty.NuTy f => Just f + _ => case rwNfTy st ctx ety of + Ty.NuTy f => Just f + _ => Nothing + case fM of + Nothing => throw "\{site}: coind at an equation over a non-ν type\{structuralHint}" + Just f => do + let nuT = Ty.NuTy f + recordBinder xr ctx env xn nuT + recordBinder yr (ctx :< nuT) (env :< xn) yn (substTy nuT Wk) + (r', skR) <- checkElem (ctx :< nuT :< substTy nuT Wk) (env :< xn :< yn) site rS Ty.PropTy + (p', skp) <- checkElem ctx env site pS (Prf (substElem r' (Ext (Ext Id l) rhs))) + let ctx3 = ctx :< nuT :< substTy nuT Wk :< Prf r' + let wk3 = Chain Wk (Chain Wk Wk) + let f3 = substPoly f wk3 + let r3 = substElem r' (under (under wk3)) + recordBinder mxr ctx env mxn nuT + recordBinder myr (ctx :< nuT) (env :< mxn) myn (substTy nuT Wk) + recordBinder mhr (ctx :< nuT :< substTy nuT Wk) (env :< mxn :< myn) mhn (Prf r') + (q', skq) <- checkElem ctx3 (env :< mxn :< myn :< mhn) site qS + (Prf (liftPoly f3 r3 (Out (CtxVar 2)) (Out (CtxVar 1)))) + pure (Star, withExpose exp (Nd [PNuCoind r' skR p' skp q' skq] [])) + _ => throw "\{site}: coind checked against a non-equality proposition\{structuralHint}" checkElem ctx env site (SClass a) ty = do st <- getSt case preferQuot st ctx ty of @@ -2973,9 +3232,15 @@ mutual -- witnessed outright. Prefer the prop as written for readable -- obligation statements; fall back to its normal form. let pN = betaElem st.sig p - let pUse = case p of - Elem.EqTy _ _ _ => p - _ => pN + let pUse0 = case p of + Elem.EqTy _ _ _ => p + _ => pN + (pUse, exp) <- pure $ case pUse0 of + Elem.EqTy _ _ _ => (pUse0, exp) + Squash _ => (pUse0, exp) + _ => case exposeProp st ctx ty pUse0 of + (pR, Just e2) => (pR, Just e2) + (pR, Nothing) => (pR, exp) case pUse of Elem.EqTy l r t => do c <- convElem ctx env "\{site}: checking ⋆" Nothing l r t @@ -3011,7 +3276,14 @@ mutual -- el-squash-i, general form: w proves the squashee directly, -- whatever its shape. At an equality prop, any proof will do -- (el-prf-prop): w becomes a proof license for the equation. - case betaElem st.sig p of + let pB = betaElem st.sig p in + let (pUse, exp) = the (Elem, Maybe (Ty, ECert)) $ case pB of + Squash _ => (pB, exp) + Elem.EqTy _ _ _ => (pB, exp) + _ => case exposeProp st ctx ty pB of + (pR, Just e2) => (pR, Just e2) + (pR, Nothing) => (pR, exp) + in case pUse of Squash sq => do (w', wSk) <- checkElem ctx env site w sq pure (Star, withExpose exp (Nd [PSquashWit w' wSk] [])) diff --git a/src/idris/Nova/Elaboration/Named.idr b/src/idris/Nova/Elaboration/Named.idr index 797f864..9b32da1 100644 --- a/src/idris/Nova/Elaboration/Named.idr +++ b/src/idris/Nova/Elaboration/Named.idr @@ -207,6 +207,7 @@ mutual usesIndexTy k (Quotient a r) = usesIndexTy k a || usesIndexElem (S (S k)) r usesIndexTy k (Ty.SigVar x es) = usesIndexSubNorm k es usesIndexTy k (QSort sg j es) = usesIndexQSig k sg || usesIndexSubNorm k es + usesIndexTy k (Ty.NuTy f) = usesIndexPoly k f usesIndexQSig : Nat -> QSig -> Bool usesIndexQSig k = any (usesIndexQTy k) @@ -223,6 +224,14 @@ mutual usesIndexQTm k (QAppI f a) = usesIndexQTm k f || usesIndexQTm k a usesIndexQTm k (QEqC l r u) = usesIndexQTm k l || usesIndexQTm k r || usesIndexQTm k u + usesIndexPoly : Nat -> Poly -> Bool + usesIndexPoly k PHole = False + usesIndexPoly k (PConst a) = usesIndexElem k a + usesIndexPoly k (PProd f g) = usesIndexPoly k f || usesIndexPoly k g + usesIndexPoly k (PSum f g) = usesIndexPoly k f || usesIndexPoly k g + usesIndexPoly k (PSigma a f) = usesIndexElem k a || usesIndexPoly (S k) f + usesIndexPoly k (PPi a f) = usesIndexElem k a || usesIndexPoly (S k) f + usesIndexElem : Nat -> Elem -> Bool usesIndexElem k (CtxVar n) = n == k usesIndexElem k (ZeroElim e) = usesIndexElem k e @@ -259,6 +268,10 @@ mutual where usesIndexMotive : (Nat, Ty) -> Bool usesIndexMotive (sj, m) = usesIndexTy (k + S (qArityLen sg sj)) m + usesIndexElem k (Elem.NuTy f) = usesIndexPoly k f + usesIndexElem k (Out t) = usesIndexElem k t + usesIndexElem k (Corec p a f x) = + usesIndexPoly k p || usesIndexElem k a || usesIndexElem (S k) f || usesIndexElem k x usesIndexSubNorm : Nat -> SubNorm -> Bool usesIndexSubNorm k [<] = False @@ -367,6 +380,14 @@ mutual ++ b ++ ". " ++ prettyElemN tbl (env :< b) r ++ ") " ++ prettyElemAtomN tbl env t prettyElemPrefixN tbl env (Class a) = "class " ++ prettyElemAtomN tbl env a + prettyElemPrefixN tbl env (Elem.NuTy f) = "ν " ++ prettyPolyAtomN tbl env f + prettyElemPrefixN tbl env (Out t) = "out " ++ prettyElemAtomN tbl env t + prettyElemPrefixN tbl env (Corec p a f x) = + -- surface-faithful: the carried 𝔽 is not printed (it is the + -- expected ν-type's, recovered at checking) + let v = if usesIndexElem 0 f then freshGeneric env else wildcard + in "corec (" ++ v ++ " : " ++ prettyElemNoCommaN tbl env a ++ ". " + ++ prettyElemN tbl (env :< v) f ++ ") " ++ prettyElemAtomN tbl env x prettyElemPrefixN tbl env (QuotElim f q) = let a = if usesIndexElem 0 f then freshGeneric env else wildcard in "quot-elim (" ++ a ++ ". " ++ prettyElemN tbl (env :< a) f ++ ") " ++ prettyElemAtomN tbl env q @@ -479,8 +500,32 @@ mutual prettyTyElN : FixTable -> NameEnv -> Ty -> String prettyTyElN tbl env (El e) = "El " ++ prettyElemAtomN tbl env e prettyTyElN tbl env (Prf e) = "Prf " ++ prettyElemAtomN tbl env e + prettyTyElN tbl env (Ty.NuTy f) = "ν " ++ prettyPolyAtomN tbl env f prettyTyElN tbl env ty = prettyTyAtomN tbl env ty + -- Polynomials, by the surface grammar's levels: binders and products + -- at the top, sums tighter, atoms (𝕏, K t, parens) innermost. + prettyPolyN : FixTable -> NameEnv -> Poly -> String + prettyPolyN tbl env (PProd f g) = + prettyPolySumN tbl env f ++ " ⨯ " ++ prettyPolyN tbl env g + prettyPolyN tbl env (PSigma a f) = + let x = if usesIndexPoly 0 f then freshGeneric env else wildcard + in "(" ++ x ++ ":" ++ prettyElemNoCommaN tbl env a ++ ") ⨯ " ++ prettyPolyN tbl (env :< x) f + prettyPolyN tbl env (PPi a f) = + let x = if usesIndexPoly 0 f then freshGeneric env else wildcard + in "(" ++ x ++ ":" ++ prettyElemNoCommaN tbl env a ++ ") → " ++ prettyPolyN tbl (env :< x) f + prettyPolyN tbl env f = prettyPolySumN tbl env f + + prettyPolySumN : FixTable -> NameEnv -> Poly -> String + prettyPolySumN tbl env (PSum f g) = + prettyPolyAtomN tbl env f ++ " ⊎ " ++ prettyPolySumN tbl env g + prettyPolySumN tbl env f = prettyPolyAtomN tbl env f + + prettyPolyAtomN : FixTable -> NameEnv -> Poly -> String + prettyPolyAtomN tbl env PHole = "𝕏" + prettyPolyAtomN tbl env (PConst a) = "K " ++ prettyElemAtomN tbl env a + prettyPolyAtomN tbl env f = "(" ++ prettyPolyN tbl env f ++ ")" + prettyTyAtomN : FixTable -> NameEnv -> Ty -> String prettyTyAtomN tbl env Ty.ZeroTy = "𝟘" prettyTyAtomN tbl env Ty.OneTy = "𝟙" diff --git a/src/idris/Nova/Elaboration/Parser.idr b/src/idris/Nova/Elaboration/Parser.idr index 9647195..cef1ecb 100644 --- a/src/idris/Nova/Elaboration/Parser.idr +++ b/src/idris/Nova/Elaboration/Parser.idr @@ -221,8 +221,35 @@ mutual parseSTyEl tbl env = (do kw "El"; space; e <- parseSElemAtom tbl env; pure (STyEl e)) <|> (do kw "Prf"; space; e <- parseSElemAtom tbl env; pure (STyPrf e)) + <|> (do kw "ν"; space; f <- parseSPolyAtom tbl env; pure (STyNu f)) <|> parseSTyAtom tbl env + -- Polynomials (NovaElaboration.txt, F{·} grammar): binders and + -- products at the top, sums tighter, atoms innermost. + parseSPoly : FixTable -> NameEnv -> Rule SPoly + parseSPoly tbl env = + (do kwc '('; sp; x <- parseNameR; sp; kwc ':'; sp + a <- parseSElemNoComma tbl env; sp; kwc ')'; sp + (do kw "⨯"; sp; f <- parseSPoly tbl (env :< fst x); pure (SPSigma x a f)) + <|> (do kw "→"; sp; f <- parseSPoly tbl (env :< fst x); pure (SPPi x a f))) + <|> (do f <- parseSPolySum tbl env + (do sp; kw "⨯"; sp; g <- parseSPoly tbl env; pure (SPProd f g)) + <|> pure f) + + -- F{1½}: ⊎, right-assoc, tighter than ⨯ (as everywhere) + parseSPolySum : FixTable -> NameEnv -> Rule SPoly + parseSPolySum tbl env = do + f <- parseSPolyAtom tbl env + (do sp; kw "⊎"; sp; g <- parseSPolySum tbl env; pure (SPSum f g)) + <|> pure f + + -- F{2}: atoms — the hole, constants, parens + parseSPolyAtom : FixTable -> NameEnv -> Rule SPoly + parseSPolyAtom tbl env = + (kw "𝕏" $> SPHole) + <|> (do kw "K"; space; a <- parseSElemAtom tbl env; pure (SPConst a)) + <|> (do kwc '('; sp; f <- parseSPoly tbl env; sp; kwc ')'; pure f) + -- T{4}: atoms parseSTyAtom : FixTable -> NameEnv -> Rule STy parseSTyAtom tbl env = @@ -341,6 +368,22 @@ mutual t <- parseSElemAtom tbl env pure (SSumElim z mot a l b r t)) <|> (do kw "class"; space; e <- parseSElemAtom tbl env; pure (SClass e)) + <|> (do kw "ν"; space; f <- parseSPolyAtom tbl env; pure (SNuC f)) + <|> (do kw "out"; space; e <- parseSElemAtom tbl env; pure (SOut e)) + <|> (do kw "corec"; space + kwc '('; sp; x <- parseNameR; sp; kwc ':'; sp + a <- parseSElemNoComma tbl env; sp; kwc '.'; sp + f <- parseSElem tbl (env :< fst x); sp; kwc ')'; sp + u <- parseSElemAtom tbl env + pure (SCorec x a f u)) + <|> (do kw "coind"; space + kwc '('; sp; x <- parseNameR; space; y <- parseNameR; sp; kwc '.'; sp + r <- parseSElem tbl (env :< fst x :< fst y); sp; kwc ')'; sp + pw <- parseSElemAtom tbl env; sp + kwc '('; sp; mx <- parseNameR; space; my <- parseNameR; space; mh <- parseNameR + sp; kwc '.'; sp + q <- parseSElem tbl (env :< fst mx :< fst my :< fst mh); sp; kwc ')' + pure (SCoind x y r pw mx my mh q)) <|> (do kw "quot-elim"; space kwc '('; sp; z <- parseNameR; sp; kwc '.'; sp mot <- parseSTy tbl (env :< fst z); sp; kwc ')'; sp diff --git a/src/idris/Nova/Elaboration/Surface.idr b/src/idris/Nova/Elaboration/Surface.idr index f1eb8a3..a487c5f 100644 --- a/src/idris/Nova/Elaboration/Surface.idr +++ b/src/idris/Nova/Elaboration/Surface.idr @@ -48,12 +48,32 @@ mutual STyProp : STy ||| Prf t STyPrf : SElem -> STy + ||| ν F — the coinductive type at a surface polynomial + STyNu : SPoly -> STy ||| ?x (rigid) or _x/_ (solvable) — a hole in type position: a ||| type declaration in Σ, stuck until (if solvable) instantiated; ||| blocks acceptance while it remains a declaration. The range is ||| the token's source span (display metadata, for the LSP). STyHole : Maybe Range -> (solvable : Bool) -> String -> STy + ||| Surface polynomials — the one-hole codes of Foundation's + ||| coinductive section. External pieces are element-level CODES; a + ||| left-hand (x:t) binds x in the body. + public export + data SPoly : Type where + ||| 𝕏 — the hole + SPHole : SPoly + ||| K t — constant at a code + SPConst : SElem -> SPoly + ||| F ⨯ G — product (non-binding) + SPProd : SPoly -> SPoly -> SPoly + ||| F ⊎ G — sum + SPSum : SPoly -> SPoly -> SPoly + ||| (x:t) ⨯ F — dependent pair over external data (binds) + SPSigma : (x : SName) -> SElem -> SPoly -> SPoly + ||| (x:t) → F — exponent with external domain (binds) + SPPi : (x : SName) -> SElem -> SPoly -> SPoly + public export data SElem : Type where ||| ☐ᵢ — a resolved local variable (the parser resolved the name) @@ -97,6 +117,22 @@ mutual SClass : SElem -> SElem ||| quot-elim (z. T) (a. f) q — motive-first SQuotElim : (z : SName) -> STy -> (a : SName) -> SElem -> SElem -> SElem + ||| ν F — the ν CODE (infers at 𝕌) + SNuC : SPoly -> SElem + ||| out t — the coinductive observation (infers, like the + ||| projections) + SOut : SElem -> SElem + ||| corec (x : a. f) u — carrier code inline as a binder + ||| annotation; checking-only (the polynomial comes from the + ||| expected ν-type) + SCorec : (x : SName) -> SElem -> SElem -> SElem -> SElem + ||| coind (x y. R) p (x y h. q) — COINDUCTION (el-nu-coind), + ||| checked at Prf (l ≡ r ∈ El (ν F)): invariant R (Ω-valued, + ||| over the two sides), p a proof of R l r, q the one-step + ||| closure — under generic x y and h : Prf (R x y), a proof + ||| that the observations are lift_𝔽(R)-related + SCoind : (nx, ny : SName) -> SElem -> SElem -> + (mx, my, mh : SName) -> SElem -> SElem ||| ∥T∥ — squash: proposition from an arbitrary type SSquash : STy -> SElem ||| ⋆ — the canonical proof of a true proposition (evident 𝟙-/ @@ -242,6 +278,7 @@ mutual show (STyQuot a x y r) = "Quot (\{show a}) \{fst x} \{fst y} (\{show r})" show (STyEq l r t) = "Eq (\{show l}) (\{show r}) (\{show t})" show (STyEl e) = "El (\{show e})" + show (STyNu f) = "Nu (\{show f})" show STyProp = "Ω" show (STyPrf e) = "Prf (\{show e})" show (STyHole _ solvable x) = if solvable then "_\{x}" else "?\{x}" @@ -276,6 +313,12 @@ mutual show (SClass t) = "Class (\{show t})" show (SQuotElim z mot a f q) = "QuotElim \{fst z} (\{show mot}) \{fst a} (\{show f}) (\{show q})" + show (SNuC f) = "NuC (\{show f})" + show (SOut e) = "Out (\{show e})" + show (SCorec x a f u) = + "Corec \{fst x} (\{show a}) (\{show f}) (\{show u})" + show (SCoind nx ny r pw mx my mh q) = + "Coind \{fst nx} \{fst ny} (\{show r}) (\{show pw}) \{fst mx} \{fst my} \{fst mh} (\{show q})" show (SSquash t) = "Squash (\{show t})" show SStar = "⋆" show (SStarWit e) = "⋆ (\{show e})" @@ -283,6 +326,16 @@ mutual show (SAnn t ty) = "Ann (\{show t}) (\{show ty})" show (SHole _ solvable x) = if solvable then "_\{x}" else "?\{x}" + public export + covering + Show SPoly where + show SPHole = "𝕏" + show (SPConst a) = "K (\{show a})" + show (SPProd f g) = "PProd (\{show f}) (\{show g})" + show (SPSum f g) = "PSum (\{show f}) (\{show g})" + show (SPSigma x a f) = "PSigma \{fst x} (\{show a}) (\{show f})" + show (SPPi x a f) = "PPi \{fst x} (\{show a}) (\{show f})" + export Show SImport where show (MkSImport m []) = "import \{m}" diff --git a/src/idris/Nova/Kernel.idr b/src/idris/Nova/Kernel.idr index e806a12..d95a893 100644 --- a/src/idris/Nova/Kernel.idr +++ b/src/idris/Nova/Kernel.idr @@ -102,6 +102,12 @@ mutual ||| of the carried signature, replayed in the entry's ᴰ-context ||| (the QIIT generalization of quot-elim's wd) PQCoh : List ECert -> Payload + ||| coinduction behind a ⋆ checked at an equality prop over a + ||| ν-type (el-nu-coind): the invariant R (Ω-valued, two bound + ||| variables), the proof that R holds at the equation's + ||| endpoints, and the one-step closure — R implies the RELATOR + ||| lift_𝔽(R) after one observation — each with its skeleton + PNuCoind : Elem -> Skel -> Elem -> Skel -> Elem -> Skel -> Payload public export data Skel : Type where @@ -300,6 +306,25 @@ mutual Left err => kerr "kernel: \{err}" else pure (QElim sg' k ms' fs' es' w') _ => pure (QElim sg' k ms' fs' es' w') + kElem sig (Elem.NuTy f) = [| Elem.NuTy (kPoly sig f) |] + kElem sig (Out t) = do + t' <- kElem sig t + case t' of + -- el-nu-beta: run the coalgebra one step, re-wrap the recursive + -- positions (map_𝔽 hᵉˡ f[id, x]) + Corec p a f x => do burn + kElem sig (mapPoly p (corecFun p a f) (substElem f (Ext Id x))) + _ => pure (Out t') + kElem sig (Corec p a f x) = + [| Corec (kPoly sig p) (kElem sig a) (kElem sig f) (kElem sig x) |] + + kPoly : Sig -> Poly -> KM Poly + kPoly sig PHole = pure PHole + kPoly sig (PConst a) = [| PConst (kElem sig a) |] + kPoly sig (PProd f g) = [| PProd (kPoly sig f) (kPoly sig g) |] + kPoly sig (PSum f g) = [| PSum (kPoly sig f) (kPoly sig g) |] + kPoly sig (PSigma a f) = [| PSigma (kElem sig a) (kPoly sig f) |] + kPoly sig (PPi a f) = [| PPi (kElem sig a) (kPoly sig f) |] kQTm : Sig -> QTm -> KM QTm kQTm sig (QVar i) = pure (QVar i) @@ -337,6 +362,7 @@ mutual Elem.SumTy a b => do burn; kTy sig (Ty.SumTy (El a) (El b)) QuotTy a r => do burn; kTy sig (Quotient (El a) r) QSortC sg k es => do burn; pure (QSort sg k es) -- ty-el-qiit + Elem.NuTy f => do burn; pure (Ty.NuTy f) -- ty-el-nu _ => pure (El e') kTy sig PropTy = pure PropTy kTy sig (Prf p) = Prf <$> kElem sig p @@ -350,6 +376,7 @@ mutual Just _ => kerr "kernel: signature name '\{x}' is not a type entry" Nothing => kerr "kernel: unknown signature name '\{x}'" kTy sig (QSort sg k es) = [| QSort (kQSig sig sg) (pure k) (kSubNorm sig es) |] + kTy sig (Ty.NuTy f) = [| Ty.NuTy (kPoly sig f) |] -- ===== Path rewriting ===== -- @@ -536,6 +563,12 @@ mutual case tTy of Ty.SigmaTy _ b => pure (substTy b (Ext Id (SigmaElim1 t))) _ => kerr "kernel: proof projects a non-pair" + -- el-nu-e: fully inference-driven, like the projections + inferP sig ctx (Out t) = do + tTy <- inferP sig ctx t >>= kTy sig + case tTy of + Ty.NuTy f => pure (El (reflectPoly f (Elem.NuTy f))) + _ => kerr "kernel: proof observes a non-ν element" inferP sig ctx OneIntro = pure Ty.OneTy inferP sig ctx NatIntro0 = pure Ty.NatTy inferP sig ctx (NatIntro1 t) = do checkP sig ctx t Ty.NatTy; pure Ty.NatTy @@ -698,6 +731,19 @@ mutual checkP sig (ctx :< a) l (substTy ty Wk) checkP sig (ctx :< b) r (substTy ty Wk) _ => kerr "kernel: ⊎-elim proof scrutinee at non-⊎ type" + -- el-nu-i as a proof argument: the carried 𝔽 must be nf-identical to + -- the expected ν-type's + checkP sig ctx (Corec p a f x) ty = do + ty' <- kTy sig ty + case ty' of + Ty.NuTy pT => do + p' <- kPoly sig p + pT' <- kPoly sig pT + if p' == pT' then pure () else kerr "kernel: corec proof carries a different polynomial than its ν-type" + checkP sig ctx a Ty.UniverseTy + checkP sig (ctx :< El a) f (substTy (El (reflectPoly p a)) Wk) + checkP sig ctx x (El a) + _ => kerr "kernel: corec proof at non-ν type" -- el-qiit-intro as a proof argument (spec §3): the saturated -- constructor at its sort, the term's signature nf-identical to the -- type's, spine checked entrywise, indices compared @@ -797,6 +843,16 @@ mutual Nothing => kerr "kernel: sort index spine out of range" goIdx (S i) rest tel + ||| Γ ⊦ 𝔽 poly, tiny-checker side (Foundation's poly-* rules): each + ||| embedded code at 𝕌, the context growing under the binding formers. + checkPolyP : Sig -> Ctx -> Poly -> KM () + checkPolyP sig ctx PHole = pure () + checkPolyP sig ctx (PConst a) = checkP sig ctx a Ty.UniverseTy + checkPolyP sig ctx (PProd f g) = do checkPolyP sig ctx f; checkPolyP sig ctx g + checkPolyP sig ctx (PSum f g) = do checkPolyP sig ctx f; checkPolyP sig ctx g + checkPolyP sig ctx (PSigma a f) = do checkP sig ctx a Ty.UniverseTy; checkPolyP sig (ctx :< El a) f + checkPolyP sig ctx (PPi a f) = do checkP sig ctx a Ty.UniverseTy; checkPolyP sig (ctx :< El a) f + ||| Γ ⊢ A type, tiny-checker side (needed for eliminator motives that ||| arrive inside proof spines). checkTyP : Sig -> Ctx -> Ty -> KM () @@ -822,6 +878,7 @@ mutual checkTyP sig ctx (QSort sg k es) = do sg' <- kQSig sig sg checkQSpineP sig ctx sg' k es + checkTyP sig ctx (Ty.NuTy f) = checkPolyP sig ctx f checkTyP sig ctx (Ty.SigVar x es) = case sigLookup x sig of Just (SigTyDef delta _ _) => checkSubstP sig ctx (toList es) (toList delta) @@ -1069,6 +1126,12 @@ mutual Ty.Quotient dom _ => pure (Just dom) _ => pure Nothing childTyE sig ctx pexp (QuotElim _ q) 1 = inferNeK sig ctx q + -- ν formers: out's scrutinee is neutrally inferable; corec's carrier + -- is a code, its seed at the carrier's decoding (the body, child 1, + -- is carrier-dependent — undetermined, like ⊎-elim's cases) + childTyE sig ctx pexp (Out t) 0 = inferNeK sig ctx t + childTyE sig ctx pexp (Corec _ _ _ _) 0 = pure (Just Ty.UniverseTy) + childTyE sig ctx pexp (Corec _ a _ _) 2 = pure (Just (El a)) -- QIIT formers: spine child i's type is the reflected telescope's -- entry i, instantiated by the earlier children — always determined childTyE sig ctx pexp (QSortC sg k es) i = qSpineChildTy sg k es i @@ -1111,6 +1174,15 @@ mutual Ty.SigmaTy a _ => pure (Just a) _ => pure Nothing Nothing => pure Nothing + inferNeK sig ctx (Out t) = do + mt <- inferNeK sig ctx t + case mt of + Just tTy => do + t' <- kTy sig tTy + case t' of + Ty.NuTy f => pure (Just (El (reflectPoly f (Elem.NuTy f)))) + _ => pure Nothing + Nothing => pure Nothing inferNeK sig ctx (SigVar x es) = case sigLookup x sig of Just (SigDef _ _ _ ty) => pure (Just (substTy ty (embed es))) @@ -1187,6 +1259,10 @@ goE sig ctx lic (i :: p) b mexp u = do Nothing => kerr "kernel: bad path" Nothing => kerr "kernel: bad path" (Class a, 0) => Class <$> goE sig ctx lic p b childTy a + (Out t', 0) => Out <$> goE sig ctx lic p b childTy t' + (Corec pf a f x, 0) => (\a' => Corec pf a' f x) <$> goE sig ctx lic p b childTy a + (Corec pf a f x, 1) => (\f' => Corec pf a f' x) <$> goE sig ctx lic p (1 + b) childTy f + (Corec pf a f x, 2) => Corec pf a f <$> goE sig ctx lic p b childTy x (QuotElim f q, 0) => (\f' => QuotElim f' q) <$> goE sig ctx lic p (1 + b) childTy f (QuotElim f q, 1) => QuotElim f <$> goE sig ctx lic p b childTy q (Squash t, 0) => Squash <$> goTy sig ctx lic p b t @@ -1325,6 +1401,10 @@ pSquashWit : Payload -> Maybe (Elem, Skel) pSquashWit (PSquashWit e sk) = Just (e, sk) pSquashWit _ = Nothing +pNuCoind : Payload -> Maybe (Elem, Skel, Elem, Skel, Elem, Skel) +pNuCoind (PNuCoind r skR pw skp qw skq) = Just (r, skR, pw, skp, qw, skq) +pNuCoind _ = Nothing + pSquashElim : Payload -> Maybe (Elem, Skel, Elem, Skel) pSquashElim (PSquashElim e esk b bsk) = Just (e, esk, b, bsk) pSquashElim _ = Nothing @@ -1528,9 +1608,40 @@ mutual _ => kerr "kernel: refl-eq payload at a non-equality prop" _ => kerr "kernel: ⋆ checked at a non-Prf type" Nothing => + -- el-nu-coind: ⋆ at an equality prop over a ν-type, + -- by COINDUCTION — invariant, endpoint proof, and + -- one-step closure at the relator (the admissible + -- rule; Foundation, coinductive NOTES) + case takeP pNuCoind sk of + Just ((r, skR, pw, skp, qw, skq), _) => do + ty' <- kTy sig ty + case ty' of + Prf pc => do + pc' <- kElem sig pc + case pc' of + Elem.EqTy l rhs ety => do + ety' <- kTy sig ety + case ety' of + Ty.NuTy f => do + let nuT = Ty.NuTy f + -- the invariant is an Ω-relation + kCheckE sig (ctx :< nuT :< substTy nuT Wk) r Ty.PropTy skR + -- it holds at the endpoints + kCheckE sig ctx pw (Prf (substElem r (Ext (Ext Id l) rhs))) skp + -- one-step closure under the generic hypotheses + let ctx3 = ctx :< nuT :< substTy nuT Wk :< Prf r + let wk3 = Chain Wk (Chain Wk Wk) + let f3 = substPoly f wk3 + let r3 = substElem r (under (under wk3)) + kCheckE sig ctx3 qw + (Prf (liftPoly f3 r3 (Out (CtxVar 2)) (Out (CtxVar 1)))) skq + _ => kerr "kernel: coinduction payload at an equation over a non-ν type" + _ => kerr "kernel: coinduction payload at a non-equality prop" + _ => kerr "kernel: ⋆ checked at a non-Prf type" + Nothing => -- el-squash-i: ⋆ : Prf ∥A∥ carries its witness (an -- inhabitant of the squashee) as a payload - case takeP pSquashWit sk of + case takeP pSquashWit sk of Just ((wit, witSk), _) => do ty' <- kTy sig ty case ty' of @@ -1574,6 +1685,22 @@ mutual case ty' of Ty.Quotient dom _ => kCheckE sig ctx a dom (skelChild 0 sk) _ => kerr "kernel: class checked at a non-quotient type" + -- el-nu-i: the carried 𝔽 must be nf-identical to the + -- expected ν-type's; carrier at 𝕌, coalgebra body over the + -- carrier at the reflected observation type, seed at the + -- carrier + Corec p aC f x => do + ty' <- kTy sig ty + case ty' of + Ty.NuTy pT => do + p' <- kPoly sig p + pT' <- kPoly sig pT + if p' == pT' then pure () + else kerr "kernel: corec carries a different polynomial than its ν-type" + kCheckE sig ctx aC Ty.UniverseTy (skelChild 0 sk) + kCheckE sig (ctx :< El aC) f (substTy (El (reflectPoly p aC)) Wk) (skelChild 1 sk) + kCheckE sig ctx x (El aC) (skelChild 2 sk) + _ => kerr "kernel: corec checked at a non-ν type" ZeroElim t => kCheckE sig ctx t Ty.ZeroTy (skelChild 0 sk) QCtor sgC c theta => do -- el-qiit-intro, SATURATED. The signature is nf(T)'s own — @@ -1668,6 +1795,12 @@ mutual case tTy of Ty.SigmaTy _ b => pure (substTy b (Ext Id (SigmaElim1 t))) _ => kerr "kernel: projecting a non-pair" + -- el-nu-e: fully inference-driven, no motive payload + Out t => do + tTy <- kInferE sig ctx t (skelChild 0 sk) >>= kTy sig + case tTy of + Ty.NuTy f => pure (El (reflectPoly f (Elem.NuTy f))) + _ => kerr "kernel: observing a non-ν element" NatElim z st t => case takeP pMotive sk of Just ((mot, motSk), _) => do @@ -1794,6 +1927,11 @@ mutual kCheckE sig ctx a Ty.UniverseTy (skelChild 0 sk) kCheckE sig ctx b Ty.UniverseTy (skelChild 1 sk) pure Ty.UniverseTy + -- code-nu: the polynomial's pieces, skeleton children in + -- binder order (every polynomial is small) + Elem.NuTy f => do + _ <- kCheckPolyK sig ctx f 0 sk + pure Ty.UniverseTy QuotTy a r => do kCheckE sig ctx a Ty.UniverseTy (skelChild 0 sk) kCheckE sig (ctx :< El a :< substTy (El a) Wk) r Ty.PropTy (skelChild 1 sk) @@ -1813,6 +1951,28 @@ mutual childSkels : Skel -> List Skel childSkels (Nd _ cs) = cs + ||| Γ ⊦ 𝔽 poly, kernel-side (Foundation's poly-* rules): each + ||| embedded code at 𝕌 with its skeleton child, children indexed in + ||| binder order across the whole polynomial; returns the next child + ||| index. + kCheckPolyK : Sig -> Ctx -> Poly -> (i : Nat) -> Skel -> KM Nat + kCheckPolyK sig ctx PHole i sk = pure i + kCheckPolyK sig ctx (PConst a) i sk = do + kCheckE sig ctx a Ty.UniverseTy (skelChild i sk) + pure (S i) + kCheckPolyK sig ctx (PProd f g) i sk = do + i' <- kCheckPolyK sig ctx f i sk + kCheckPolyK sig ctx g i' sk + kCheckPolyK sig ctx (PSum f g) i sk = do + i' <- kCheckPolyK sig ctx f i sk + kCheckPolyK sig ctx g i' sk + kCheckPolyK sig ctx (PSigma a f) i sk = do + kCheckE sig ctx a Ty.UniverseTy (skelChild i sk) + kCheckPolyK sig (ctx :< El a) f (S i) sk + kCheckPolyK sig ctx (PPi a f) i sk = do + kCheckE sig ctx a Ty.UniverseTy (skelChild i sk) + kCheckPolyK sig (ctx :< El a) f (S i) sk + ||| Γ ⊢ A type, kernel-side. export kCheckTyK : Sig -> Ctx -> Ty -> Skel -> KM () @@ -1839,6 +1999,10 @@ mutual -- ty-qiit: the signature and the index spine against its arity kQSigCheck sig ctx sg kQSortSpine sig ctx sg k es sk + kCheckTyK sig ctx (Ty.NuTy f) sk = do + -- ty-nu: the polynomial's pieces, skeleton children in binder order + _ <- kCheckPolyK sig ctx f 0 sk + pure () kCheckTyK sig ctx (Ty.SigVar x es) sk = case sigLookup x sig of Just (SigTyDef delta _ _) => diff --git a/src/idris/Nova/Kernel/Beta.idr b/src/idris/Nova/Kernel/Beta.idr index 02592e2..fd83037 100644 --- a/src/idris/Nova/Kernel/Beta.idr +++ b/src/idris/Nova/Kernel/Beta.idr @@ -115,6 +115,25 @@ mutual Left err => assert_total $ idris_crash "betaElem: el-qiit-beta on an ill-formed eliminator: \{err}" else QElim sg' k ms' fs' es' (QCtor sgW c theta) w' => QElim sg' k ms' fs' es' w' + betaElem sig (Elem.NuTy f) = Elem.NuTy (betaPoly sig f) + betaElem sig (Out t) = + case betaElem sig t of + -- el-nu-beta: out at a corec head runs the coalgebra one step + -- and re-wraps the recursive positions (map_𝔽 hᵉˡ f[id, x]) + Corec p a f x => betaElem sig (mapPoly p (corecFun p a f) (substElem f (Ext Id x))) + t' => Out t' + betaElem sig (Corec p a f x) = + Corec (betaPoly sig p) (betaElem sig a) (betaElem sig f) (betaElem sig x) + + ||| The carried polynomial, with every embedded Nova piece normalized. + export + betaPoly : Sig -> Poly -> Poly + betaPoly sig PHole = PHole + betaPoly sig (PConst a) = PConst (betaElem sig a) + betaPoly sig (PProd f g) = PProd (betaPoly sig f) (betaPoly sig g) + betaPoly sig (PSum f g) = PSum (betaPoly sig f) (betaPoly sig g) + betaPoly sig (PSigma a f) = PSigma (betaElem sig a) (betaPoly sig f) + betaPoly sig (PPi a f) = PPi (betaElem sig a) (betaPoly sig f) ||| The carried signature, with every embedded Nova piece normalized. export @@ -163,6 +182,7 @@ mutual Elem.SumTy a b => betaTy sig (Ty.SumTy (El a) (El b)) QuotTy a r => betaTy sig (Quotient (El a) r) QSortC sg k es => QSort sg k es -- ty-el-qiit + Elem.NuTy f => Ty.NuTy (betaPoly sig f) -- ty-el-nu e' => El e' betaTy sig PropTy = PropTy betaTy sig (Prf e) = Prf (betaElem sig e) @@ -176,6 +196,7 @@ mutual Just _ => assert_total $ idris_crash "betaTy: signature identifier '\{x}' is not a type entry" Nothing => assert_total $ idris_crash "betaTy: signature identifier '\{x}' not found" betaTy sig (QSort sg k es) = QSort (betaQSig sig sg) k (betaSubNorm sig es) + betaTy sig (Ty.NuTy f) = Ty.NuTy (betaPoly sig f) ||| σ, with every element's own beta-redexes rewritten. export @@ -249,6 +270,10 @@ mutual Left _ => QElim sg k ms fs es (QCtor sgW c theta) else QElim sg k ms fs es (QCtor sgW c theta) w' => QElim sg k ms fs es w' + whnfE sig (Out t) = + case whnfE sig t of + Corec p a f x => whnfE sig (mapPoly p (corecFun p a f) (substElem f (Ext Id x))) + t' => Out t' whnfE sig e = e export @@ -263,6 +288,7 @@ mutual Elem.SumTy a b => Ty.SumTy (El a) (El b) QuotTy a r => Quotient (El a) r QSortC sg k es => QSort sg k es -- ty-el-qiit + Elem.NuTy f => Ty.NuTy f -- ty-el-nu e' => El e' whnfT sig (Ty.SigVar x es) = case sigLookup x sig of diff --git a/src/idris/Nova/Kernel/Parser.idr b/src/idris/Nova/Kernel/Parser.idr index bb51cf7..7181881 100644 --- a/src/idris/Nova/Kernel/Parser.idr +++ b/src/idris/Nova/Kernel/Parser.idr @@ -142,6 +142,14 @@ mutual t <- parseElemAtom pure (SumElim l r t)) <|> (do str_ "class"; space; e <- parseElemAtom; pure (Class e)) + <|> (do str_ "ν"; space; f <- parsePolyAtom; pure (Elem.NuTy f)) + <|> (do str_ "out"; space; e <- parseElemAtom; pure (Out e)) + <|> (do str_ "corec"; space + f <- parsePolyAtom; space + a <- parseElemAtom; space + g <- parseElemAtom; space + x <- parseElemAtom + pure (Corec f a g x)) <|> (do str_ "quot-elim"; space f <- parseElemAtom; space q <- parseElemAtom @@ -274,8 +282,35 @@ mutual parseTyEl = (do str_ "El"; space; e <- parseElemAtom; pure (El e)) <|> (do str_ "Prf"; space; e <- parseElemAtom; pure (Prf e)) + <|> (do str_ "ν"; space; f <- parsePolyAtom; pure (Ty.NuTy f)) <|> parseTyAtom + -- Polynomials (one-hole codes): binders and products at the top, + -- sums tighter, atoms innermost — the surface grammar's levels. + covering + parsePoly : Rule Poly + parsePoly = + (do str_ "El"; space; a <- parseElemAtom; sp + (do str_ "⨯"; sp; f <- parsePoly; pure (PSigma a f)) + <|> (do str_ "→"; sp; f <- parsePoly; pure (PPi a f))) + <|> (do f <- parsePolySum + (do sp; str_ "⨯"; sp; g <- parsePoly; pure (PProd f g)) + <|> pure f) + + covering + parsePolySum : Rule Poly + parsePolySum = do + f <- parsePolyAtom + (do sp; str_ "⊎"; sp; g <- parsePolySum; pure (PSum f g)) + <|> pure f + + covering + parsePolyAtom : Rule Poly + parsePolyAtom = + (str_ "𝕏" $> PHole) + <|> (do str_ "K"; space; a <- parseElemAtom; pure (PConst a)) + <|> (do char_ '('; sp; f <- parsePoly; sp; char_ ')'; pure f) + -- Constant types, signature type variable, and parenthesised type covering parseTyAtom : Rule Ty diff --git a/src/idris/Nova/Kernel/Subst.idr b/src/idris/Nova/Kernel/Subst.idr index 3389a7e..83e4bd3 100644 --- a/src/idris/Nova/Kernel/Subst.idr +++ b/src/idris/Nova/Kernel/Subst.idr @@ -83,6 +83,10 @@ mutual QElim (substQSig sg sigma) k (substMotives sg ms sigma) (map (\f => substElem f sigma) fs) (substSubNorm es sigma) (substElem w sigma) + substElem (Elem.NuTy f) sigma = Elem.NuTy (substPoly f sigma) + substElem (Out t) sigma = Out (substElem t sigma) + substElem (Corec p a f x) sigma = + Corec (substPoly p sigma) (substElem a sigma) (substElem f (under sigma)) (substElem x sigma) ||| Motive i lives over Γ·⌊𝔎ᵢ⌋ᵗ ▷ 𝒮.kᵢ δ — lift σ once per index ||| binder plus once for the eliminee. @@ -119,6 +123,17 @@ mutual substQSig : QSig -> Sub -> QSig substQSig sg sigma = map (\t => substQTy t sigma) sg + ||| 𝔽[σ] — σ on the embedded Nova pieces, lifted under the binding + ||| formers; the hole is inert. + export + substPoly : Poly -> Sub -> Poly + substPoly PHole sigma = PHole + substPoly (PConst a) sigma = PConst (substElem a sigma) + substPoly (PProd f g) sigma = PProd (substPoly f sigma) (substPoly g sigma) + substPoly (PSum f g) sigma = PSum (substPoly f sigma) (substPoly g sigma) + substPoly (PSigma a f) sigma = PSigma (substElem a sigma) (substPoly f (under sigma)) + substPoly (PPi a f) sigma = PPi (substElem a sigma) (substPoly f (under sigma)) + ||| T[σ] export substTy : Ty -> Sub -> Ty @@ -135,6 +150,7 @@ mutual substTy (Quotient a r) sigma = Quotient (substTy a sigma) (substElem r (under (under sigma))) substTy (Ty.SigVar x es) sigma = Ty.SigVar x (substSubNorm es sigma) substTy (QSort sg k es) sigma = QSort (substQSig sg sigma) k (substSubNorm es sigma) + substTy (Ty.NuTy f) sigma = Ty.NuTy (substPoly f sigma) @@ -205,6 +221,11 @@ mutual goMs [] (m :: rest) = Nothing goMs (kk :: ks) (m :: rest) = [| strengthenTy (d + S (qArityLen sg kk)) m :: goMs ks rest |] + strengthenElem d (Elem.NuTy f) = Elem.NuTy <$> strengthenPoly d f + strengthenElem d (Out t) = Out <$> strengthenElem d t + strengthenElem d (Corec p a f x) = + Corec <$> strengthenPoly d p <*> strengthenElem d a + <*> strengthenElem (1 + d) f <*> strengthenElem d x export strengthenQTm : (depth : Nat) -> QTm -> Maybe QTm @@ -224,6 +245,15 @@ mutual strengthenQSig : (depth : Nat) -> QSig -> Maybe QSig strengthenQSig d = traverse (strengthenQTy d) + export + strengthenPoly : (depth : Nat) -> Poly -> Maybe Poly + strengthenPoly d PHole = Just PHole + strengthenPoly d (PConst a) = PConst <$> strengthenElem d a + strengthenPoly d (PProd f g) = PProd <$> strengthenPoly d f <*> strengthenPoly d g + strengthenPoly d (PSum f g) = PSum <$> strengthenPoly d f <*> strengthenPoly d g + strengthenPoly d (PSigma a f) = PSigma <$> strengthenElem d a <*> strengthenPoly (1 + d) f + strengthenPoly d (PPi a f) = PPi <$> strengthenElem d a <*> strengthenPoly (1 + d) f + export strengthenSubNorm : (depth : Nat) -> SubNorm -> Maybe SubNorm strengthenSubNorm d [<] = Just [<] @@ -244,6 +274,7 @@ mutual strengthenTy d (Quotient a r) = Quotient <$> strengthenTy d a <*> strengthenElem (2 + d) r strengthenTy d (Ty.SigVar x es) = Ty.SigVar x <$> strengthenSubNorm d es strengthenTy d (QSort sg k es) = QSort <$> strengthenQSig d sg <*> Just k <*> strengthenSubNorm d es + strengthenTy d (Ty.NuTy f) = Ty.NuTy <$> strengthenPoly d f ||| Only surface-shaped substitutions (flat Ext/Terminal element lists) ||| strengthen; Id/Wk/Chain are index-sensitive and never appear in @@ -266,3 +297,93 @@ weakenSub : Sub -> Sub weakenSub Terminal = Terminal weakenSub (Ext s e) = Ext (weakenSub s) (substElem e Wk) weakenSub s = assert_total $ idris_crash "weakenSub: non-surface substitution" + + +-- ===== Coinductive meta-operations (Foundation, coinductive section) ===== + +||| ⌊𝔽⌋(c) — the code with the hole filled by c (a code over the same +||| context as 𝔽). c weakens under the binding formers; the non-binding +||| product's second component crosses code-sigma's binder, so it +||| weakens too. +export covering +reflectPoly : Poly -> Elem -> Elem +reflectPoly PHole c = c +reflectPoly (PConst a) c = a +reflectPoly (PProd f g) c = + Elem.SigmaTy (reflectPoly f c) (substElem (reflectPoly g c) Wk) +reflectPoly (PSum f g) c = Elem.SumTy (reflectPoly f c) (reflectPoly g c) +reflectPoly (PSigma a f) c = Elem.SigmaTy a (reflectPoly f (substElem c Wk)) +reflectPoly (PPi a f) c = Elem.PiTy a (reflectPoly f (substElem c Wk)) + +||| map_𝔽 g x — the functorial action, applied: an element of +||| El ⌊𝔽⌋(c₀) rebuilt with g : El c₀ → El c₁ at the hole positions. +||| g and x weaken under the binders the clauses cross; at the binding +||| formers the body polynomial is INSTANTIATED (PSigma: at the first +||| component; PPi: at the freshly bound argument). +export covering +mapPoly : Poly -> (g : Elem) -> (x : Elem) -> Elem +mapPoly PHole g x = PiApp g x +mapPoly (PConst a) g x = x +mapPoly (PProd f h) g x = + SigmaIntro (mapPoly f g (SigmaElim1 x)) (mapPoly h g (SigmaElim2 x)) +mapPoly (PSum f h) g x = + SumElim (Inj1 (mapPoly (substPoly f Wk) (substElem g Wk) (CtxVar 0))) + (Inj2 (mapPoly (substPoly h Wk) (substElem g Wk) (CtxVar 0))) + x +mapPoly (PSigma a f) g x = + SigmaIntro (SigmaElim1 x) + (mapPoly (substPoly f (Ext Id (SigmaElim1 x))) g (SigmaElim2 x)) +mapPoly (PPi a f) g x = + PiIntro (mapPoly f (substElem g Wk) (PiApp (substElem x Wk) (CtxVar 0))) + +||| hᵉˡ ≜ λ (corec 𝔽 a f[↑] ☐₀) — the corecursor as a function term +||| (el-nu-beta's re-wrapper). +export covering +corecFun : Poly -> (a : Elem) -> (f : Elem) -> Elem +corecFun p a f = + PiIntro (Corec (substPoly p Wk) (substElem a Wk) (substElem f (under Wk)) (CtxVar 0)) + +||| lift_𝔽(R) u v — the RELATOR: the relation lifting of a polynomial +||| (Foundation, el-nu-coind). R is an Ω-valued OPEN term with two +||| bound variables (Γ ▷ ν𝔽 ▷ (ν𝔽)[↑], ☐₁ the left side, ☐₀ the +||| right); u and v are elements of El ⌊𝔽⌋(c)'s decoding in the +||| ambient context; the result is an Ω-element there. One clause per +||| former: the hole instantiates R, constants compare by ≡, products +||| are Ω-conjunctions (squashed Σ of Prfs), sums match tags by a +||| dependent ⊎-elim at motive Ω (⊥ off the diagonal, definitional +||| collapse on it), the dependent pair binds the first-component +||| equation so the instances are ≐ by reflection (no transport), and +||| exponents lift pointwise. R's BASE weakens under every binder the +||| clauses cross (its own two binders lift over it). +export covering +liftPoly : Poly -> (r : Elem) -> (u : Elem) -> (v : Elem) -> Elem +liftPoly PHole r u v = substElem r (Ext (Ext Id u) v) +liftPoly (PConst a) r u v = Elem.EqTy u v (El a) +liftPoly (PProd f g) r u v = + Squash (Ty.SigmaTy (Prf (liftPoly f r (SigmaElim1 u) (SigmaElim1 v))) + (substTy (Prf (liftPoly g r (SigmaElim2 u) (SigmaElim2 v))) Wk)) +liftPoly (PSum f g) r u v = + SumElim + (SumElim (liftPoly f (wk2base r) (CtxVar 1) (CtxVar 0)) + (Squash Ty.ZeroTy) + (substElem v Wk)) + (SumElim (Squash Ty.ZeroTy) + (liftPoly g (wk2base r) (CtxVar 1) (CtxVar 0)) + (substElem v Wk)) + u + where + wk2base : Elem -> Elem + wk2base e = substElem (substElem e (under (under Wk))) (under (under Wk)) +liftPoly (PSigma a f) r u v = + Squash (Ty.SigmaTy + (Prf (Elem.EqTy (SigmaElim1 u) (SigmaElim1 v) (El a))) + (Prf (liftPoly (substPoly (substPoly f (Ext Id (SigmaElim1 u))) Wk) + (substElem r (under (under Wk))) + (substElem (SigmaElim2 u) Wk) + (substElem (SigmaElim2 v) Wk)))) +liftPoly (PPi a f) r u v = + Squash (Ty.PiTy (El a) + (Prf (liftPoly f + (substElem r (under (under Wk))) + (PiApp (substElem u Wk) (CtxVar 0)) + (PiApp (substElem v Wk) (CtxVar 0))))) diff --git a/src/idris/Nova/Kernel/Syntax.idr b/src/idris/Nova/Kernel/Syntax.idr index 1dd021f..49cd92e 100644 --- a/src/idris/Nova/Kernel/Syntax.idr +++ b/src/idris/Nova/Kernel/Syntax.idr @@ -55,6 +55,9 @@ mutual ||| 𝒮.k ē (the sort at entry position k of the carried QIIT ||| signature, at index spine ē — ty-qiit) QSort : QSig -> Nat -> SubNorm -> Ty + ||| ν 𝔽 (the coinductive type at the carried polynomial — ty-nu; + ||| 𝔽 is carried, so ν-equality is structural, like a QIIT's 𝒮) + NuTy : Poly -> Ty namespace Elem public export @@ -139,6 +142,18 @@ mutual ||| in entry order, terms over Γ; then the index spine and the ||| eliminee. Coherences are CHECKED (kernel PQCoh), not stored.) QElim : QSig -> Nat -> List Ty -> List Elem -> SubNorm -> Elem -> Elem + ||| ν 𝔽 (universe code for the coinductive type — code-nu; every + ||| polynomial is small, the grammar enforces it) + NuTy : Poly -> Elem + ||| out t (the coinductive observation — el-nu-e, the ELIMINATOR; + ||| lazy: computes only at a corec head, el-nu-beta) + Out : Elem -> Elem + ||| corec 𝔽 a f x (the corecursor — el-nu-i, the INTRODUCTION: + ||| carried polynomial, carrier code, coalgebra body — one bound + ||| variable over El a — and seed. 𝔽 and a are CARRIED, like ℰ at + ||| QElim: el-nu-beta consumes map_𝔽, so the redex is + ||| self-contained) + Corec : Poly -> Elem -> Elem -> Elem -> Elem namespace QTm ||| Theory-of-signatures terms (docs/NovaFoundation.txt, QIIT @@ -173,6 +188,27 @@ mutual ||| El 𝕥 ⇛ 𝔄 — INDUCTIVE Π (𝕥 a sort code; binds a ToS variable) QPiInd : QTm -> QTy -> QTy + namespace Poly + ||| One-hole polynomial codes (docs/NovaFoundation.txt, coinductive + ||| section): the hole 𝕏, external CODE pieces, products, sums, and + ||| the two binding formers (a left-hand El a binds a Nova variable + ||| in the body's embedded pieces). Strict positivity is + ||| grammatical: the hole never sits left of an exponent. + public export + data Poly : Type where + ||| 𝕏 — the hole + PHole : Poly + ||| K a — constant at a code + PConst : Elem -> Poly + ||| 𝔽 ⨯ 𝔾 — product (non-binding) + PProd : Poly -> Poly -> Poly + ||| 𝔽 ⊎ 𝔾 — sum + PSum : Poly -> Poly -> Poly + ||| El a ⨯ 𝔽 — dependent pair over external data (binds) + PSigma : Elem -> Poly -> Poly + ||| El a → 𝔽 — exponent with external domain (binds) + PPi : Elem -> Poly -> Poly + ||| A QIIT signature IS a closed qiit-context: entries in declaration ||| order (position 0 first), ANONYMOUS — a signature mints no names. public export @@ -374,6 +410,7 @@ mutual Quotient a r == Quotient a' r' = a == a' && r == r' Ty.SigVar x s == Ty.SigVar x' s' = x == x' && s == s' QSort s k es == QSort s' k' es' = s == s' && k == k' && es == es' + NuTy f == NuTy f' = f == f' _ == _ = False public export @@ -410,6 +447,9 @@ mutual QCtor s k es == QCtor s' k' es' = s == s' && k == k' && es == es' QElim s k ms fs es w == QElim s' k' ms' fs' es' w' = s == s' && k == k' && ms == ms' && fs == fs' && es == es' && w == w' + Elem.NuTy f == Elem.NuTy f' = f == f' + Out t == Out t' = t == t' + Corec p a f x == Corec p' a' f' x' = p == p' && a == a' && f == f' && x == x' _ == _ = False public export @@ -430,6 +470,17 @@ mutual QPiInd u b == QPiInd u' b' = u == u' && b == b' _ == _ = False + public export + covering + Eq Poly where + PHole == PHole = True + PConst a == PConst a' = a == a' + PProd f g == PProd f' g' = f == f' && g == g' + PSum f g == PSum f' g' = f == f' && g == g' + PSigma a f == PSigma a' f' = a == a' && f == f' + PPi a f == PPi a' f' = a == a' && f == f' + _ == _ = False + mutual public export covering @@ -488,6 +539,9 @@ mutual compare (Ty.SigVar _ _) _ = LT compare _ (Ty.SigVar _ _) = GT compare (QSort s k es) (QSort s' k' es') = compare s s' <+> compare k k' <+> compare es es' + compare (QSort _ _ _) _ = LT + compare _ (QSort _ _ _) = GT + compare (NuTy f) (NuTy f') = compare f f' public export covering @@ -581,6 +635,16 @@ mutual compare _ (QCtor _ _ _) = GT compare (QElim s k ms fs es w) (QElim s' k' ms' fs' es' w') = compare s s' <+> compare k k' <+> compare ms ms' <+> compare fs fs' <+> compare es es' <+> compare w w' + compare (QElim _ _ _ _ _ _) _ = LT + compare _ (QElim _ _ _ _ _ _) = GT + compare (Elem.NuTy f) (Elem.NuTy f') = compare f f' + compare (Elem.NuTy _) _ = LT + compare _ (Elem.NuTy _) = GT + compare (Out t) (Out t') = compare t t' + compare (Out _) _ = LT + compare _ (Out _) = GT + compare (Corec p a f x) (Corec p' a' f' x') = + compare p p' <+> compare a a' <+> compare f f' <+> compare x x' public export covering @@ -610,6 +674,26 @@ mutual compare _ (QPiExt _ _) = GT compare (QPiInd u b) (QPiInd u' b') = compare u u' <+> compare b b' + public export + covering + Ord Poly where + compare PHole PHole = EQ + compare PHole _ = LT + compare _ PHole = GT + compare (PConst a) (PConst a') = compare a a' + compare (PConst _) _ = LT + compare _ (PConst _) = GT + compare (PProd f g) (PProd f' g') = compare f f' <+> compare g g' + compare (PProd _ _) _ = LT + compare _ (PProd _ _) = GT + compare (PSum f g) (PSum f' g') = compare f f' <+> compare g g' + compare (PSum _ _) _ = LT + compare _ (PSum _ _) = GT + compare (PSigma a f) (PSigma a' f') = compare a a' <+> compare f f' + compare (PSigma _ _) _ = LT + compare _ (PSigma _ _) = GT + compare (PPi a f) (PPi a' f') = compare a a' <+> compare f f' + mutual public export covering @@ -636,6 +720,7 @@ mutual show (Quotient a r) = "Quotient (\{show a}) (\{show r})" show (Ty.SigVar x s) = "SigVar \{show x} (\{show s})" show (QSort s k es) = "QSort (\{show s}) \{show k} (\{show es})" + show (NuTy f) = "NuTy (\{show f})" public export covering @@ -671,6 +756,9 @@ mutual show (QCtor s k es) = "QCtor (\{show s}) \{show k} (\{show es})" show (QElim s k ms fs es w) = "QElim (\{show s}) \{show k} (\{show ms}) (\{show fs}) (\{show es}) (\{show w})" + show (Elem.NuTy f) = "NuTy (\{show f})" + show (Out t) = "Out (\{show t})" + show (Corec p a f x) = "Corec (\{show p}) (\{show a}) (\{show f}) (\{show x})" public export covering @@ -687,3 +775,13 @@ mutual show (QEl t) = "QEl (\{show t})" show (QPiExt a b) = "QPiExt (\{show a}) (\{show b})" show (QPiInd u b) = "QPiInd (\{show u}) (\{show b})" + + public export + covering + Show Poly where + show PHole = "PHole" + show (PConst a) = "PConst (\{show a})" + show (PProd f g) = "PProd (\{show f}) (\{show g})" + show (PSum f g) = "PSum (\{show f}) (\{show g})" + show (PSigma a f) = "PSigma (\{show a}) (\{show f})" + show (PPi a f) = "PPi (\{show a}) (\{show f})" diff --git a/src/nova/stream.nova b/src/nova/stream.nova new file mode 100644 index 0000000..d33cf26 --- /dev/null +++ b/src/nova/stream.nova @@ -0,0 +1,102 @@ +-- Coinductive streams and conaturals — the ν-scheme at its two +-- simplest polynomials (NovaFoundation.txt, "Coinductive types"). +-- Stream a ≔ ν (K a ⨯ 𝕏): one observation, out, splitting into head +-- and tail; corec builds a stream from any coalgebra. Every lemma +-- below closes by COMPUTATION (el-nu-beta plus projections/⊎-elim): +-- the uniqueness law el-nu-eta is judgemental in the theory but has +-- no kernel certificate (NovaKernel.txt, A5 — same status as +-- el-qiit-eta), so bisimulation-shaped equations are out of scope +-- here; see the deliberate obligation in the test suite. + +def stream : 𝕌 → 𝕌 ≔ λa. ν (K a ⨯ 𝕏) + +def hd : (a : 𝕌) → El (stream a) → El a ≔ + λa. λt. (out t) .π₁ + +def tl : (a : 𝕌) → El (stream a) → El (stream a) ≔ + λa. λt. (out t) .π₂ + +-- cons, by corecursion at the one-step carrier a ⨯ stream a: emit the +-- stored head, then continue by OBSERVING the stored tail — Lambek's +-- in, specialized +def cons : (a : 𝕌) → El a → El (stream a) → El (stream a) ≔ + λa. λx. λs. corec (p : a ⨯ stream a. ((p .π₁) , out (p .π₂))) (x , s) + +-- iterate f x: the stream x, f x, f (f x), … +def iterate : (a : 𝕌) → (El a → El a) → El a → El (stream a) ≔ + λa. λf. λx. corec (s : a. (s , f s)) x + +-- β-lemmas: one el-nu-beta step each (plus pairing/projections) +def hdCons : (a : 𝕌) (x : El a) (s : El (stream a)) → hd _ (cons _ x s) ≡ x ∈ El a ≔ + λa. λx. λs. ⋆ +def hdIterate : (a : 𝕌) (f : El a → El a) (x : El a) → hd _ (iterate _ f x) ≡ x ∈ El a ≔ + λa. λf. λx. ⋆ + +-- two observation steps: the tail of an iterate is the iterate of the +-- image — hd ∘ tl commutes with one application of f +def hdTlIterate : (a : 𝕌) (f : El a → El a) (x : El a) → + hd _ (tl _ (iterate _ f x)) ≡ f x ∈ El a ≔ + λa. λf. λx. ⋆ + +-- the head under one cons-then-tail: reaches the stored tail's head +def hdTlCons : (a : 𝕌) (x : El a) (s : El (stream a)) → + hd _ (tl _ (cons _ x s)) ≡ hd _ s ∈ El a ≔ + λa. λx. λs. ⋆ + +-- Conaturals: ν (K 𝟙 ⊎ 𝕏) — zero observes as inj₁, a successor as +-- inj₂ of its predecessor; ∞ is its own predecessor +def conat : 𝕌 ≔ ν (K 𝟙 ⊎ 𝕏) + +def czero : El conat ≔ corec (s : 𝟙. inj₁ s) () +def cinf : El conat ≔ corec (s : 𝟙. inj₂ s) () + +-- observation shapes, by computation (el-nu-beta + el-sum-beta) +def outZero : out czero ≡ inj₁ () ∈ 𝟙 ⊎ El conat ≔ ⋆ +def outInf : out cinf ≡ inj₂ cinf ∈ 𝟙 ⊎ El conat ≔ ⋆ + +-- csucc: emit inj₂ of the stored conat, continuing by observation +def csucc : El conat → El conat ≔ + λn. corec (p : 𝟙 ⊎ conat. inj₂ (⊎-elim (w. 𝟙 ⊎ El conat) (u. inj₁ u) (m. out m) p)) (out n) + +-- a successor always observes as inj₂ — one β step, the payload +-- irrelevant to the shape (⊎-elim at an equality motive would refute +-- inj₁; here the equation is between the injections themselves) +def outSuccInf : out (csucc cinf) ≡ inj₂ (csucc cinf) ∈ 𝟙 ⊎ El conat ≔ ⋆ + +-- map over streams: relabel every element, by corecursion on the +-- source stream itself +def mapS : (a : 𝕌) (b : 𝕌) → (El a → El b) → El (stream a) → El (stream b) ≔ + λa. λb. λf. λt. corec (s : stream a. (f (hd _ s) , tl _ s)) t + +-- map commutes with the observations — the finite-depth shadow of +-- the (η-needing) map-fusion laws, closed by pure computation +def hdMap : (a : 𝕌) (b : 𝕌) (f : El a → El b) (t : El (stream a)) → + hd _ (mapS _ _ f t) ≡ f (hd _ t) ∈ El b ≔ + λa. λb. λf. λt. ⋆ +def hdTlMap : (a : 𝕌) (b : 𝕌) (f : El a → El b) (t : El (stream a)) → + hd _ (tl _ (mapS _ _ f t)) ≡ f (hd _ (tl _ t)) ∈ El b ≔ + λa. λb. λf. λt. ⋆ + +-- With coinduction dischargeable (el-nu-coind; `coind`), the +-- η-needing laws close. tlCons: the tail of a cons is the consed +-- stream — by coinduction with a GRAPH invariant: u is v's image +-- under the one-step machine, for SOME v. +def tlCons : (a : 𝕌) (x : El a) (s : El (stream a)) → + tl _ (cons _ x s) ≡ s ∈ El (stream a) ≔ + λa. λx. λs. + coind (u v. ∥(w : El (stream a)) ⨯ + ((u ≡ corec (p : a ⨯ stream a. ((p .π₁) , out (p .π₂))) (out w) ∈ El (stream a)) ⨯ + (v ≡ w ∈ El (stream a)))∥) + (⋆ ((s , (⋆ , ⋆)))) + (u v h. squash-elim h (w. + ⋆ ((⋆ , ⋆ (((out (w .π₁)) .π₂ , (⋆ , ⋆))))))) + +-- conat's classic coinductive theorem: ∞ is its own successor. The +-- closure exercises the relator's SUM clause: the ⊎-elim at motive Ω +-- is stuck at the generic observations, un-stuck by the invariant's +-- variable-definition equations, and collapses definitionally on the +-- inj₂/inj₂ diagonal. +def infSucc : cinf ≡ csucc cinf ∈ El conat ≔ + coind (x y. ∥(x ≡ cinf ∈ El conat) ⨯ (y ≡ csucc cinf ∈ El conat)∥) + (⋆ ((⋆ , ⋆))) + (x y h. squash-elim h (w. ⋆ ((⋆ , ⋆)))) diff --git a/src/nova/streamBisim.nova b/src/nova/streamBisim.nova new file mode 100644 index 0000000..d9e0e81 --- /dev/null +++ b/src/nova/streamBisim.nova @@ -0,0 +1,95 @@ +import equality (cong) +import stream (stream, hd, tl, mapS) +import streamEq (tlN, nth, obsEq, obsEqRefl, nthMap, mapIdObsEq, mapFuseObsEq) + +-- Observational equality, restated CORECURSIVELY: two streams are +-- bisimilar iff SOME relation relates them, agrees on heads, and is +-- preserved by tails — the union of all post-fixed points of the +-- one-observation-step operator, i.e. the greatest fixed point by +-- Knaster–Tarski, landed in Ω by impredicative squash (the dual of +-- Foundation's least-relations-by-intersection note). The +-- coinduction principle is DEFINITIONAL here: to prove bisim s t, +-- exhibit an invariant and its one-step closure — no ℕ index +-- anywhere. Below: intro/unfold laws, a direct corecursive proof +-- (reflexivity via the equality invariant), and equivalence with the +-- ℕ-indexed obsEq. + +def bisim : (a : 𝕌) → El (stream a) → El (stream a) → Ω ≔ + λa. λs. λt. + ∥(r : El (stream a) → El (stream a) → Ω) ⨯ + ((x : El (stream a)) (y : El (stream a)) → Prf (r x y) → + Prf (hd _ x ≡ hd _ y ∈ El a) ⨯ Prf (r (tl _ x) (tl _ y))) ⨯ + Prf (r s t)∥ + +-- UNFOLD, head half: bisimilar streams agree at the head +def bisimHd : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) → + Prf (bisim _ s t) → Prf (hd _ s ≡ hd _ t ∈ El a) ≔ + λa. λs. λt. λh. squash-elim h (w. ((w .π₂ .π₁) s t (w .π₂ .π₂)) .π₁) + +-- UNFOLD, tail half: bisimilarity is preserved by observation — +-- the SAME invariant relates the tails +def bisimTl : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) → + Prf (bisim _ s t) → Prf (bisim _ (tl _ s) (tl _ t)) ≔ + λa. λs. λt. λh. + squash-elim h (w. + ⋆ ((w .π₁ , ((w .π₂ .π₁) , ((w .π₂ .π₁) s t (w .π₂ .π₂)) .π₂)))) + +-- a DIRECT corecursive proof: reflexivity, with judgemental equality +-- itself as the invariant — heads by cong at hd, tails by cong at tl +def bisimRefl : (a : 𝕌) (s : El (stream a)) → Prf (bisim _ s s) ≔ + λa. λs. + ⋆ (((λx. λy. (x ≡ y ∈ El (stream a))) , + ((λx. λy. λp. (cong _ (λv. a) (λv. hd _ v) x y p , + cong _ (λv. stream a) (λv. tl _ v) x y p)) , + ⋆))) + +-- obsEq ⊃ bisim: the ℕ-indexed relation is ITSELF a bisimulation — +-- heads are observation 0, and shifting the index moves under one +-- tail (nth n (tl x) ≐ nth (S n) x, judgementally) +def obsEqBisim : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) → + Prf (obsEq _ s t) → Prf (bisim _ s t) ≔ + λa. λs. λt. λh. + ⋆ (((λx. λy. obsEq _ x y) , + ((λx. λy. λp. (squash-elim p (w. w Z) , + squash-elim p (w. ⋆ (λn. w (S n))))) , + h))) + +-- bisim ⊃ obsEq: unfold n times, by ℕ-induction over the depth +def bisimObsEq : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) → + Prf (bisim _ s t) → Prf (obsEq _ s t) ≔ + λa. λs. λt. λh. + ⋆ (λn. (ℕ-elim (m. (x : El (stream a)) → (y : El (stream a)) → + Prf (bisim _ x y) → Prf (nth _ m x ≡ nth _ m y ∈ El a)) + (λx. λy. λg. bisimHd _ x y g) + (m ih. λx. λy. λg. ih (tl _ x) (tl _ y) (bisimTl _ x y g)) + n) s t h) + +-- interop corollary: map-identity, now in the corecursive spelling +def mapIdBisim : (a : 𝕌) (s : El (stream a)) → + Prf (bisim _ (mapS _ _ (λx. x) s) s) ≔ + λa. λs. obsEqBisim _ _ _ (mapIdObsEq _ s) + +-- THE REFLECTION: bisimilarity implies equality — el-nu-coind's +-- surface form, with bisim ITSELF as the invariant and the unfold +-- laws as the one-step closure. This is the theorem that upgrades +-- every observational result below it to a judgemental equation. +def bisimReflect : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) → + Prf (bisim _ s t) → Prf (s ≡ t ∈ El (stream a)) ≔ + λa. λs. λt. λh. + coind (x y. bisim _ x y) h + (x y hb. ⋆ ((bisimHd _ x y hb , bisimTl _ x y hb))) + +def obsEqReflect : (a : 𝕌) (s : El (stream a)) (t : El (stream a)) → + Prf (obsEq _ s t) → Prf (s ≡ t ∈ El (stream a)) ≔ + λa. λs. λt. λh. bisimReflect _ s t (obsEqBisim _ s t h) + +-- the η-needing equalities, now judgemental theorems +def mapIdEq : (a : 𝕌) (s : El (stream a)) → + mapS _ _ (λx. x) s ≡ s ∈ El (stream a) ≔ + λa. λs. bisimReflect _ _ _ (mapIdBisim _ s) + +def mapFuseEq : (a : 𝕌) (b : 𝕌) (c : 𝕌) (f : El a → El b) (g : El b → El c) + (s : El (stream a)) → + mapS _ _ g (mapS _ _ f s) ≡ mapS _ _ (λx. g (f x)) s ∈ El (stream c) ≔ + λa. λb. λc. λf. λg. λs. + obsEqReflect _ _ _ (mapFuseObsEq _ _ _ f g s) diff --git a/src/nova/streamEq.nova b/src/nova/streamEq.nova new file mode 100644 index 0000000..ac10da0 --- /dev/null +++ b/src/nova/streamEq.nova @@ -0,0 +1,59 @@ +import stream (stream, hd, tl, mapS, iterate) + +-- Observational equality of streams: two streams are related iff +-- every finite observation agrees — the ℕ-indexed spelling of +-- bisimilarity, definable TODAY as an Ω-proposition (squash of a Π +-- over ℕ of equations). Its theory below runs on ℕ-INDUCTION where a +-- bisimulation proof would use coinduction: el-nu-eta is judgemental +-- in the theory but has no kernel certificate (NovaKernel.txt, A5), +-- so the REFLECTION of obsEq into ≡ is the one statement that stays +-- out of reach here — everything observational is provable now. + +-- n-fold tail, unfolding head-first: tlN (S n) s ≐ tlN n (tl s) +def tlN : (a : 𝕌) → ℕ → El (stream a) → El (stream a) ≔ + λa. λn. ℕ-elim (m. El (stream a) → El (stream a)) (λs. s) (m ih. λs. ih (tl _ s)) n + +-- the n-th observation +def nth : (a : 𝕌) → ℕ → El (stream a) → El a ≔ + λa. λn. λs. hd _ (tlN _ n s) + +-- observational equality, in Ω +def obsEq : (a : 𝕌) → El (stream a) → El (stream a) → Ω ≔ + λa. λs. λt. ∥(n : ℕ) → Prf (nth _ n s ≡ nth _ n t ∈ El a)∥ + +-- reflexivity: every observation is ≐-reflexive +def obsEqRefl : (a : 𝕌) (s : El (stream a)) → Prf (obsEq _ s s) ≔ + λa. λs. ⋆ (λn. ⋆) + +-- map commutes with EVERY observation, by ℕ-induction — the step is +-- judgemental: tl (mapS f s) ≐ mapS f (tl s) is one el-nu-beta +def nthMap : (a : 𝕌) (b : 𝕌) (f : El a → El b) (n : ℕ) (s : El (stream a)) → + nth _ n (mapS _ _ f s) ≡ f (nth _ n s) ∈ El b ≔ + λa. λb. λf. λn. + ℕ-elim (m. (s : El (stream a)) → nth _ m (mapS _ _ f s) ≡ f (nth _ m s) ∈ El b) + (λs. ⋆) + (m ih. λs. ih (tl _ s)) + n + +-- mapping the identity is observationally the identity — the +-- η-needing `mapS id s ≡ s` weakened to its observational shadow, +-- where it is PROVABLE +def mapIdObsEq : (a : 𝕌) (s : El (stream a)) → Prf (obsEq _ (mapS _ _ (λx. x) s) s) ≔ + λa. λs. ⋆ (λn. nthMap _ _ (λx. x) n s) + +-- likewise map fusion, observationally: composing maps is mapping +-- the composite +def mapFuseObsEq : (a : 𝕌) (b : 𝕌) (c : 𝕌) (f : El a → El b) (g : El b → El c) + (s : El (stream a)) → + Prf (obsEq _ (mapS _ _ g (mapS _ _ f s)) (mapS _ _ (λx. g (f x)) s)) ≔ + λa. λb. λc. λf. λg. λs. + ⋆ (λn. (ℕ-elim (m. (t : El (stream a)) → + nth _ m (mapS _ _ g (mapS _ _ f t)) ≡ nth _ m (mapS _ _ (λx. g (f x)) t) ∈ El c) + (λt. ⋆) + (m ih. λt. ih (tl _ t)) + n) s) + +-- the tail of an iterate is the iterate of the image, observationally +def iterShiftObsEq : (a : 𝕌) (f : El a → El a) (x : El a) → + Prf (obsEq _ (tl _ (iterate _ f x)) (iterate _ f (f x))) ≔ + λa. λf. λx. ⋆ (λn. ⋆) diff --git a/tests/nova/elaboration/elab-nu-coind-general/expected b/tests/nova/elaboration/elab-nu-coind-general/expected new file mode 100644 index 0000000..55dbce6 --- /dev/null +++ b/tests/nova/elaboration/elab-nu-coind-general/expected @@ -0,0 +1,13 @@ +defined conat +defined cinf +defined csucc +defined infSucc +defined moore +defined m1 +defined m2 +defined mEq +defined dep +defined d1 +defined d2 +defined dEq +Accepted. diff --git a/tests/nova/elaboration/elab-nu-coind-general/input.nova b/tests/nova/elaboration/elab-nu-coind-general/input.nova new file mode 100644 index 0000000..7a916a8 --- /dev/null +++ b/tests/nova/elaboration/elab-nu-coind-general/input.nova @@ -0,0 +1,27 @@ +-- sum clause: conat, the classic ∞ = ∞ + 1 +def conat : 𝕌 ≔ ν (K 𝟙 ⊎ 𝕏) +def cinf : El conat ≔ corec (s : 𝟙. inj₂ s) () +def csucc : El conat → El conat ≔ + λn. corec (p : 𝟙 ⊎ conat. inj₂ (⊎-elim (w. 𝟙 ⊎ El conat) (u. inj₁ u) (m. out m) p)) (out n) +def infSucc : cinf ≡ csucc cinf ∈ El conat ≔ + coind (x y. ∥(x ≡ cinf ∈ El conat) ⨯ (y ≡ csucc cinf ∈ El conat)∥) + (⋆ ((⋆ , ⋆))) + (x y h. squash-elim h (w. ⋆ ((⋆ , ⋆)))) + +-- exponent clause: Moore machines, constant machines over two carriers +def moore : 𝕌 ≔ ν (K ℕ ⨯ ((i : ℕ) → 𝕏)) +def m1 : El moore ≔ corec (s : 𝟙. (Z , λi. s)) () +def m2 : El moore ≔ corec (s : ℕ. (Z , λi. s)) Z +def mEq : m1 ≡ m2 ∈ El moore ≔ + coind (x y. ∥(x ≡ m1 ∈ El moore) ⨯ (y ≡ m2 ∈ El moore)∥) + (⋆ ((⋆ , ⋆))) + (x y h. squash-elim h (w. ⋆ ((⋆ , ⋆ (λi. ⋆ ((⋆ , ⋆))))))) + +-- dependent-pair clause: a binder polynomial +def dep : 𝕌 ≔ ν ((n : ℕ) ⨯ 𝕏) +def d1 : El dep ≔ corec (s : 𝟙. (Z , s)) () +def d2 : El dep ≔ corec (s : ℕ. (Z , s)) Z +def dEq : d1 ≡ d2 ∈ El dep ≔ + coind (x y. ∥(x ≡ d1 ∈ El dep) ⨯ (y ≡ d2 ∈ El dep)∥) + (⋆ ((⋆ , ⋆))) + (x y h. squash-elim h (w. ⋆ ((⋆ , ⋆ ((⋆ , ⋆)))))) diff --git a/tests/nova/elaboration/elab-nu-coind-general/run b/tests/nova/elaboration/elab-nu-coind-general/run new file mode 100755 index 0000000..505e6e2 --- /dev/null +++ b/tests/nova/elaboration/elab-nu-coind-general/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" elab input.nova diff --git a/tests/nova/elaboration/elab-nu-coind/expected b/tests/nova/elaboration/elab-nu-coind/expected new file mode 100644 index 0000000..b5e0a98 --- /dev/null +++ b/tests/nova/elaboration/elab-nu-coind/expected @@ -0,0 +1,6 @@ +defined stream +defined zerosA +defined zerosB +defined triv +defined zerosEq +Accepted. diff --git a/tests/nova/elaboration/elab-nu-coind/input.nova b/tests/nova/elaboration/elab-nu-coind/input.nova new file mode 100644 index 0000000..e7091ac --- /dev/null +++ b/tests/nova/elaboration/elab-nu-coind/input.nova @@ -0,0 +1,13 @@ +def stream : 𝕌 → 𝕌 ≔ λa. ν (K a ⨯ 𝕏) +def zerosA : El (stream ℕ) ≔ corec (s : 𝟙. (Z , s)) () +def zerosB : El (stream ℕ) ≔ corec (s : ℕ. (Z , s)) Z + +-- pipeline smoke: coinduction with equality itself as the invariant +def triv : zerosB ≡ zerosB ∈ El (stream ℕ) ≔ + coind (x y. x ≡ y ∈ El (stream ℕ)) ⋆ (x y h. ⋆ ((⋆ , ⋆))) + +-- the real thing: two different carriers, same behavior +def zerosEq : zerosA ≡ zerosB ∈ El (stream ℕ) ≔ + coind (x y. ∥(x ≡ zerosA ∈ El (stream ℕ)) ⨯ (y ≡ zerosB ∈ El (stream ℕ))∥) + (⋆ ((⋆ , ⋆))) + (x y h. squash-elim h (w. ⋆ ((⋆ , ⋆ ((⋆ , ⋆)))))) diff --git a/tests/nova/elaboration/elab-nu-coind/run b/tests/nova/elaboration/elab-nu-coind/run new file mode 100755 index 0000000..505e6e2 --- /dev/null +++ b/tests/nova/elaboration/elab-nu-coind/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" elab input.nova diff --git a/tests/nova/elaboration/elab-nu-obligation/expected b/tests/nova/elaboration/elab-nu-obligation/expected new file mode 100644 index 0000000..cc45fdc --- /dev/null +++ b/tests/nova/elaboration/elab-nu-obligation/expected @@ -0,0 +1,7 @@ +defined stream +defined zeros +defined ones +defined bad [+1 obligation] +open obligations (1): + [1] (x : ν (K ℕ ⨯ 𝕏)) (y : ν (K ℕ ⨯ 𝕏)) (h : Prf ∥Prf (x ≡ zeros ∈ El (stream ℕ)) ⨯ Prf (y ≡ ones ∈ El (stream ℕ))∥) (w : Prf (x ≡ corec (z : 𝟙. Z, z) () ∈ ν (K ℕ ⨯ 𝕏)) ⨯ Prf (y ≡ corec (z : 𝟙. S Z, z) () ∈ ν (K ℕ ⨯ 𝕏))) ⊢ (out x) .π₁ ≐ (out y) .π₁ : ℕ + at: def bad: checking ⋆ diff --git a/tests/nova/elaboration/elab-nu-obligation/input.nova b/tests/nova/elaboration/elab-nu-obligation/input.nova new file mode 100644 index 0000000..f3b27d1 --- /dev/null +++ b/tests/nova/elaboration/elab-nu-obligation/input.nova @@ -0,0 +1,10 @@ +-- coinduction with a NON-closing invariant: the closure's head +-- component is Z ≐ S Z, which stays an OBLIGATION (not an error) — +-- the coind payload composes with the ordinary obligation loop +def stream : 𝕌 → 𝕌 ≔ λa. ν (K a ⨯ 𝕏) +def zeros : El (stream ℕ) ≔ corec (s : 𝟙. (Z , s)) () +def ones : El (stream ℕ) ≔ corec (s : 𝟙. (S Z , s)) () +def bad : zeros ≡ ones ∈ El (stream ℕ) ≔ + coind (x y. ∥(x ≡ zeros ∈ El (stream ℕ)) ⨯ (y ≡ ones ∈ El (stream ℕ))∥) + (⋆ ((⋆ , ⋆))) + (x y h. squash-elim h (w. ⋆ ((⋆ , ⋆ ((⋆ , ⋆)))))) diff --git a/tests/nova/elaboration/elab-nu-obligation/run b/tests/nova/elaboration/elab-nu-obligation/run new file mode 100755 index 0000000..505e6e2 --- /dev/null +++ b/tests/nova/elaboration/elab-nu-obligation/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" elab input.nova diff --git a/tests/nova/elaboration/elab-nu/expected b/tests/nova/elaboration/elab-nu/expected new file mode 100644 index 0000000..44a6f55 --- /dev/null +++ b/tests/nova/elaboration/elab-nu/expected @@ -0,0 +1,7 @@ +defined stream +defined iterate +defined hd +defined tl +defined hdIter +defined hdTlIter +Accepted. diff --git a/tests/nova/elaboration/elab-nu/input.nova b/tests/nova/elaboration/elab-nu/input.nova new file mode 100644 index 0000000..36aad23 --- /dev/null +++ b/tests/nova/elaboration/elab-nu/input.nova @@ -0,0 +1,11 @@ +-- ν formation, corec introduction, out observation; both β-lemmas +-- close by computation (el-nu-beta) +def stream : 𝕌 → 𝕌 ≔ λa. ν (K a ⨯ 𝕏) +def iterate : (a : 𝕌) → (El a → El a) → El a → El (stream a) ≔ + λa. λf. λx. corec (s : a. (s , f s)) x +def hd : (a : 𝕌) → El (stream a) → El a ≔ λa. λt. (out t) .π₁ +def tl : (a : 𝕌) → El (stream a) → El (stream a) ≔ λa. λt. (out t) .π₂ +def hdIter : (a : 𝕌) (f : El a → El a) (x : El a) → hd _ (iterate _ f x) ≡ x ∈ El a ≔ + λa. λf. λx. ⋆ +def hdTlIter : (a : 𝕌) (f : El a → El a) (x : El a) → hd _ (tl _ (iterate _ f x)) ≡ f x ∈ El a ≔ + λa. λf. λx. ⋆ diff --git a/tests/nova/elaboration/elab-nu/run b/tests/nova/elaboration/elab-nu/run new file mode 100755 index 0000000..505e6e2 --- /dev/null +++ b/tests/nova/elaboration/elab-nu/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" elab input.nova diff --git a/tests/nova/evaluation/eval-nu-take-inf/expected b/tests/nova/evaluation/eval-nu-take-inf/expected new file mode 100644 index 0000000..e2f7334 --- /dev/null +++ b/tests/nova/evaluation/eval-nu-take-inf/expected @@ -0,0 +1 @@ +SigmaIntro (NatIntro0) (SigmaIntro (NatIntro1 (NatIntro0)) (SigmaIntro (NatIntro1 (NatIntro1 (NatIntro0))) (OneIntro))) diff --git a/tests/nova/evaluation/eval-nu-take-inf/input.nova b/tests/nova/evaluation/eval-nu-take-inf/input.nova new file mode 100644 index 0000000..f9122f3 --- /dev/null +++ b/tests/nova/evaluation/eval-nu-take-inf/input.nova @@ -0,0 +1,11 @@ +-- take from an INFINITE colist: the naturals as an always-cons +-- colist; three observations, no padding path taken +def clist : 𝕌 ≔ ν (K 𝟙 ⊎ (K ℕ ⨯ 𝕏)) +def cnil : El clist ≔ corec (s : 𝟙. inj₁ s) () +def cnats : El clist ≔ corec (s : ℕ. inj₂ (s , S s)) Z +def vecc : ℕ → 𝕌 ≔ λn. ℕ-elim (m. 𝕌) 𝟙 (m ih. ℕ ⨯ ih) n +def take : (n : ℕ) → El clist → El (vecc n) ≔ + λn. ℕ-elim (m. El clist → El (vecc m)) (λt. ()) + (m ih. λt. ⊎-elim (w. El (vecc (S m))) (u. (Z , ih cnil)) (q. ((q .π₁) , ih (q .π₂))) (out t)) + n +def val : El (vecc (S (S (S Z)))) ≔ take (S (S (S Z))) cnats diff --git a/tests/nova/evaluation/eval-nu-take-inf/run b/tests/nova/evaluation/eval-nu-take-inf/run new file mode 100755 index 0000000..dccbffc --- /dev/null +++ b/tests/nova/evaluation/eval-nu-take-inf/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" eval input.nova val diff --git a/tests/nova/evaluation/eval-nu-take/expected b/tests/nova/evaluation/eval-nu-take/expected new file mode 100644 index 0000000..078c133 --- /dev/null +++ b/tests/nova/evaluation/eval-nu-take/expected @@ -0,0 +1 @@ +SigmaIntro (NatIntro1 (NatIntro0)) (SigmaIntro (NatIntro1 (NatIntro1 (NatIntro0))) (SigmaIntro (NatIntro0) (SigmaIntro (NatIntro0) (OneIntro)))) diff --git a/tests/nova/evaluation/eval-nu-take/input.nova b/tests/nova/evaluation/eval-nu-take/input.nova new file mode 100644 index 0000000..40fb892 --- /dev/null +++ b/tests/nova/evaluation/eval-nu-take/input.nova @@ -0,0 +1,18 @@ +-- take the first N elements of a COLIST, padding with Z past its +-- end: ℕ-elim drives N observations (one el-nu-beta each, through +-- ⊎-elim on the colist's step), the result a nested pair at an +-- ℕ-elim-defined vector code +def clist : 𝕌 ≔ ν (K 𝟙 ⊎ (K ℕ ⨯ 𝕏)) +def step : 𝕌 ≔ 𝟙 ⊎ (ℕ ⨯ clist) +def cnil : El clist ≔ corec (s : 𝟙. inj₁ s) () +def ccons : El ℕ → El clist → El clist ≔ + λx. λt. corec (p : step. ⊎-elim (w. El (𝟙 ⊎ (ℕ ⨯ step))) (u. inj₁ u) (q. inj₂ ((q .π₁) , out (q .π₂))) p) + (inj₂ (x , t)) +def vecc : ℕ → 𝕌 ≔ λn. ℕ-elim (m. 𝕌) 𝟙 (m ih. ℕ ⨯ ih) n +def take : (n : ℕ) → El clist → El (vecc n) ≔ + λn. ℕ-elim (m. El clist → El (vecc m)) (λt. ()) + (m ih. λt. ⊎-elim (w. El (vecc (S m))) (u. (Z , ih cnil)) (q. ((q .π₁) , ih (q .π₂))) (out t)) + n +-- [1, 2] taken to depth 4: two elements, then two Z-pads +def val : El (vecc (S (S (S (S Z))))) ≔ + take (S (S (S (S Z)))) (ccons (S Z) (ccons (S (S Z)) cnil)) diff --git a/tests/nova/evaluation/eval-nu-take/run b/tests/nova/evaluation/eval-nu-take/run new file mode 100755 index 0000000..dccbffc --- /dev/null +++ b/tests/nova/evaluation/eval-nu-take/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" eval input.nova val diff --git a/tests/nova/evaluation/eval-nu/expected b/tests/nova/evaluation/eval-nu/expected new file mode 100644 index 0000000..66707ee --- /dev/null +++ b/tests/nova/evaluation/eval-nu/expected @@ -0,0 +1 @@ +NatIntro1 (NatIntro0) diff --git a/tests/nova/evaluation/eval-nu/input.nova b/tests/nova/evaluation/eval-nu/input.nova new file mode 100644 index 0000000..16bb9fb --- /dev/null +++ b/tests/nova/evaluation/eval-nu/input.nova @@ -0,0 +1,3 @@ +-- out at a corec head runs one coalgebra step (el-nu-beta) +def nats : El (ν (K ℕ ⨯ 𝕏)) ≔ corec (s : ℕ. (s , S s)) Z +def val : ℕ ≔ (out ((out nats) .π₂)) .π₁ diff --git a/tests/nova/evaluation/eval-nu/run b/tests/nova/evaluation/eval-nu/run new file mode 100755 index 0000000..dccbffc --- /dev/null +++ b/tests/nova/evaluation/eval-nu/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" eval input.nova val diff --git a/tests/nova/parser/elem-corec/expected b/tests/nova/parser/elem-corec/expected new file mode 100644 index 0000000..8b9d3ec --- /dev/null +++ b/tests/nova/parser/elem-corec/expected @@ -0,0 +1 @@ +Corec (PProd (PConst (NatTy)) (PHole)) (NatTy) (SigmaIntro (NatIntro0) (CtxVar 0)) (NatIntro0) diff --git a/tests/nova/parser/elem-corec/run b/tests/nova/parser/elem-corec/run new file mode 100755 index 0000000..b87c944 --- /dev/null +++ b/tests/nova/parser/elem-corec/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" run elem "corec (K ℕ ⨯ 𝕏) ℕ (Z , ☐₀) Z" diff --git a/tests/nova/parser/elem-nu/expected b/tests/nova/parser/elem-nu/expected new file mode 100644 index 0000000..5508440 --- /dev/null +++ b/tests/nova/parser/elem-nu/expected @@ -0,0 +1 @@ +NuTy (PSum (PConst (OneTy)) (PHole)) diff --git a/tests/nova/parser/elem-nu/run b/tests/nova/parser/elem-nu/run new file mode 100755 index 0000000..2bd5c95 --- /dev/null +++ b/tests/nova/parser/elem-nu/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" run elem "ν (K 𝟙 ⊎ 𝕏)" diff --git a/tests/nova/parser/elem-out/expected b/tests/nova/parser/elem-out/expected new file mode 100644 index 0000000..89e208b --- /dev/null +++ b/tests/nova/parser/elem-out/expected @@ -0,0 +1 @@ +Out (CtxVar 0) diff --git a/tests/nova/parser/elem-out/run b/tests/nova/parser/elem-out/run new file mode 100755 index 0000000..7580d57 --- /dev/null +++ b/tests/nova/parser/elem-out/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" run elem "out ☐₀" diff --git a/tests/nova/parser/ty-nu-pi/expected b/tests/nova/parser/ty-nu-pi/expected new file mode 100644 index 0000000..098343e --- /dev/null +++ b/tests/nova/parser/ty-nu-pi/expected @@ -0,0 +1 @@ +NuTy (PPi (NatTy) (PSum (PConst (NatTy)) (PHole))) diff --git a/tests/nova/parser/ty-nu-pi/run b/tests/nova/parser/ty-nu-pi/run new file mode 100755 index 0000000..6e7a7c8 --- /dev/null +++ b/tests/nova/parser/ty-nu-pi/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" run ty "ν (El ℕ → K ℕ ⊎ 𝕏)" diff --git a/tests/nova/parser/ty-nu/expected b/tests/nova/parser/ty-nu/expected new file mode 100644 index 0000000..5548ed8 --- /dev/null +++ b/tests/nova/parser/ty-nu/expected @@ -0,0 +1 @@ +NuTy (PProd (PConst (NatTy)) (PHole)) diff --git a/tests/nova/parser/ty-nu/run b/tests/nova/parser/ty-nu/run new file mode 100755 index 0000000..c9b6d3d --- /dev/null +++ b/tests/nova/parser/ty-nu/run @@ -0,0 +1,2 @@ +#!/bin/sh +"$1" run ty "ν (K ℕ ⨯ 𝕏)"