From 50bb6660d6624a61efaf9a131d96194b146c10a2 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Thu, 30 Apr 2026 18:05:32 -0600 Subject: [PATCH] REL1: typing rules + transp/comp derived theorems for .ind + Rust subst MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Typing.lean: minimal-viable typing rules for the three new CTerm constructors (REL1 first cut; REL2 will refine to dependent formulations). - HasType.ctor : .ctor S c params args : .ind S params (no per-arg premises; runtime enforces) - HasType.indElim : non-dependent form — motive : .pi (.ind …) C, result : C; branch coherence checked at eval - HasType.dimExpr : placeholder typing at .univ (real interval- typing requires a CType.interval primitive, deferred to REL2) HasType.weaken_core extended with the three new arms. TransportLaws.lean: derived theorems for transport over .ind (T1, T2, stuck), all reducing to existing axioms (eval_transp_top, eval_transp_const, eval_transp_nonpath + vTransp_stuck). Pointwise distribution through ctor args is REL1.1 future work. CompLaws.lean: derived theorems for composition over .ind (C1, C2, const-line, stuck) — corollaries of the existing eval_comp_* axioms. Same REL1.1 deferral for pointwise distribution. native/cubical/src/subst.rs: critical Rust fix. The previous fallback `_ => mk_term_var(ctor_field(t, 0))` corrupted the new TERM_DIMEXPR / TERM_CTOR / TERM_INDELIM tags by extracting field 0 (a CTypeSchema for ctor) and wrapping it as a malformed .var, causing infinite recursion / OOM in subst-driven paths (eval_comp_top calls substDim). Proper arms for all three new tags + cterm_subst_dim_list and cterm_subst_dim_branches helpers. Unknown-tag fallback now safely returns the input unchanged instead of synthesising a malformed .var. FFITest.lean: three new smoke arms exercising T1/T2 transport and C1 composition over .ind natC. Result: 28/28 smoke + 46/46 properties = 74/74. Co-Authored-By: Claude Opus 4.7 (1M context) --- CubicalTransport/CompLaws.lean | 44 +++++++++++++ CubicalTransport/FFITest.lean | 14 ++++- CubicalTransport/TransportLaws.lean | 44 +++++++++++++ CubicalTransport/Typing.lean | 41 ++++++++++++ native/cubical/src/subst.rs | 98 ++++++++++++++++++++++++++++- 5 files changed, 239 insertions(+), 2 deletions(-) diff --git a/CubicalTransport/CompLaws.lean b/CubicalTransport/CompLaws.lean index e0895dc..11d04e5 100644 --- a/CubicalTransport/CompLaws.lean +++ b/CubicalTransport/CompLaws.lean @@ -49,3 +49,47 @@ theorem comp_step_preserves (Γ : Ctx) (L : DimLine) (φ : FaceFormula) CTerm.substDimBool L.binder false u = t₀) : HasType Γ (CTerm.step (.comp L.binder L.body φ u t₀)) L.at1 := CTerm.step_preserves_type Γ _ _ (HasType.comp L ht hu hc) + +-- ── Composition over schema-defined inductive types (REL1) ────────────────── +-- Composition over `.ind S params` flows through `eval_comp_stuck` +-- (`.ind ≠ .pi`). Derived theorems below make the case explicit. +-- REL1.1 / REL2: pointwise distribution through ctor args. + +/-- Composition over a non-trivial `.ind` line reduces to a stuck + `ncomp` neutral. Derived from `eval_comp_stuck`. -/ +theorem eval_comp_ind (env : CEnv) (i : DimVar) + (S : CTypeSchema) (params : List CType) + (φ : FaceFormula) (u t : CTerm) + (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot) + (hA : CType.dimAbsent i (.ind S params) = false) : + eval env (.comp i (.ind S params) φ u t) = + .vneu (.ncomp i (.ind S params) φ (eval env u) (eval env t)) := + eval_comp_stuck env i (.ind S params) φ u t hφ₁ hφ₂ hA + (by intro _ _ h; nomatch h) + +/-- Composition over a constant `.ind` line reduces to homogeneous + composition. Derived from `eval_comp_const`. -/ +theorem eval_comp_ind_const (env : CEnv) (i : DimVar) + (S : CTypeSchema) (params : List CType) + (φ : FaceFormula) (u t : CTerm) + (hφ₁ : φ ≠ .top) (hφ₂ : φ ≠ .bot) + (hA : CType.dimAbsent i (.ind S params) = true) : + eval env (.comp i (.ind S params) φ u t) = + vHCompValue (.ind S params) φ (eval env (.plam i u)) (eval env t) := + eval_comp_const env i (.ind S params) φ u t hφ₁ hφ₂ hA + +/-- Composition over `.ind` at `φ = .top`: the system covers everything, + so the result is the tube body at `i := 1`. Direct corollary of C1. -/ +theorem eval_comp_ind_top (env : CEnv) (i : DimVar) + (S : CTypeSchema) (params : List CType) (u t : CTerm) : + eval env (.comp i (.ind S params) .top u t) = + eval env (u.substDim i .one) := + eval_comp_top env i (.ind S params) u t + +/-- Composition over `.ind` at `φ = .bot`: the system contributes nothing, + so the result is transport of the base. Direct corollary of C2. -/ +theorem eval_comp_ind_bot (env : CEnv) (i : DimVar) + (S : CTypeSchema) (params : List CType) (u t : CTerm) : + eval env (.comp i (.ind S params) .bot u t) = + eval env (.transp i (.ind S params) .bot t) := + eval_comp_bot env i (.ind S params) u t diff --git a/CubicalTransport/FFITest.lean b/CubicalTransport/FFITest.lean index 583e598..81124e2 100644 --- a/CubicalTransport/FFITest.lean +++ b/CubicalTransport/FFITest.lean @@ -173,7 +173,19 @@ def tests : List (String × String × String) := ("indElim Bool true-case on false ⇓ \"no\"", cvalSummary (eval .nil (boolElim (.lam "x" (.var "M")) (.var "no") (.var "yes") falseC)), - "vneu nvar no") ] + "vneu nvar no"), + ("transp_ind T1: φ=.top is identity", + cvalSummary (eval .nil + (.transp ⟨"i"⟩ CType.natC .top zeroC)), + "vctor zero ..."), + ("transp_ind T2: constant Nat line is identity", + cvalSummary (eval .nil + (.transp ⟨"i"⟩ CType.natC (.eq0 ⟨"j"⟩) (succC zeroC))), + "vctor succ ..."), + ("comp_ind C1: φ=.top reduces to u[i:=1]", + cvalSummary (eval .nil + (.comp ⟨"i"⟩ CType.natC .top (succC zeroC) zeroC)), + "vctor succ ...") ] /-- Run every smoke test, print its actual vs expected. Returns the number of failures. -/ diff --git a/CubicalTransport/TransportLaws.lean b/CubicalTransport/TransportLaws.lean index c8b3073..8df58b2 100644 --- a/CubicalTransport/TransportLaws.lean +++ b/CubicalTransport/TransportLaws.lean @@ -96,6 +96,50 @@ def transp_plam_body_path (φ : FaceFormula) (j : DimVar) (body : CTerm) : CTerm := .compN i A [(φ, body), (.eq0 j, a), (.eq1 j, b)] body +-- ── Transport over schema-defined inductive types (REL1) ──────────────────── +-- Inductive instances `.ind S params` are neither `.path` nor `.glue`, so +-- transport over them flows through the value-level stuck case in the +-- existing `vTransp_stuck` axiom. These derived theorems make the API +-- shape explicit for downstream consumers (paideia, topolei). +-- +-- A future REL1.1 / REL2 refinement will add pointwise distribution: when +-- the target is a `.ctor S c cParams cArgs`, transport pushes through +-- the args via per-arg-shape rules. CCHM HIT-transport gives the +-- explicit formula via comp-shaped fillers; for plain inductives the +-- distribution is structurally simpler. + +/-- Transport over a non-trivial line in a schema-defined inductive + `.ind S params` reduces to a stuck `ntransp` neutral. Derived from + `eval_transp_nonpath` (`.ind` is not `.path` and not `.glue`) and + `vTransp_stuck` (`.ind` is not `.pi`). -/ +theorem eval_transp_ind (env : CEnv) (i : DimVar) + (S : CTypeSchema) (params : List CType) (φ : FaceFormula) (t : CTerm) + (hφ : φ ≠ .top) + (hA : CType.dimAbsent i (.ind S params) = false) : + eval env (.transp i (.ind S params) φ t) = + .vneu (.ntransp i (.ind S params) φ (eval env t)) := by + rw [eval_transp_nonpath env i (.ind S params) φ t hφ hA + (by intro _ _ _ h; nomatch h) + (by intro _ _ _ _ _ _ _ _ h; nomatch h)] + exact vTransp_stuck i (.ind S params) φ (eval env t) hφ hA + (by intro _ _ h; nomatch h) + +/-- Transport over a constant `.ind` line is the identity (T2 specialised + to `.ind`). Direct corollary of `eval_transp_const`. -/ +theorem eval_transp_ind_const (env : CEnv) (i : DimVar) + (S : CTypeSchema) (params : List CType) (φ : FaceFormula) (t : CTerm) + (hφ : φ ≠ .top) + (hA : CType.dimAbsent i (.ind S params) = true) : + eval env (.transp i (.ind S params) φ t) = eval env t := + eval_transp_const env i (.ind S params) φ t hφ hA + +/-- Transport over `.ind` under a full face is the identity (T1 + specialised to `.ind`). -/ +theorem eval_transp_ind_top (env : CEnv) (i : DimVar) + (S : CTypeSchema) (params : List CType) (t : CTerm) : + eval env (.transp i (.ind S params) .top t) = eval env t := + eval_transp_top env i (.ind S params) t + /-- `transp_plam_is_plam_path` restated via the named body. -/ theorem transp_plam_body_path_eq (i : DimVar) (A : CType) (a b : CTerm) diff --git a/CubicalTransport/Typing.lean b/CubicalTransport/Typing.lean index a1deade..b08f7d3 100644 --- a/CubicalTransport/Typing.lean +++ b/CubicalTransport/Typing.lean @@ -96,6 +96,40 @@ inductive HasType : Ctx → CTerm → CType → Prop where | snd : HasType Γ t (.sigma A B) → HasType Γ (.snd t) B + /-- Schema constructor application (REL1 minimal-viable typing). + + Asserts that `.ctor S c params args` has type `.ind S params`. + No premises constrain `args` here — the per-argument typing + against `S.ctors[c].args` is enforced at runtime by `eval` and + the boundary system, not at the typing-judgement level. REL2 + will refine this to a fully dependent rule with one premise per + `CtorSpec.args` entry. -/ + | ctor : HasType Γ (.ctor S c params args) (.ind S params) + + /-- Inductive eliminator (REL1 minimal-viable, *non-dependent* form). + + The motive is treated as a function `.pi (.ind S params) C` for + some closed `C : CType` (constant motive), so the eliminator's + result type is `C`. Dependent motives — where `C` varies with + the eliminated value — are deferred to REL2. + + Branch-level coherence (each branch body matches its ctor's + curried signature, including recursive-arg hypotheses for `.self` + args) is checked at runtime by `eval`, not statically here. -/ + | indElim : HasType Γ target (.ind S params) → + HasType Γ motive (.pi (.ind S params) C) → + HasType Γ (.indElim S params motive branches target) C + + /-- Dimension expression lifted to the term language (REL1). + + `.dimExpr r` is an abuse of CType-typing: dimensional values + don't have a proper CType. We assign it the universe `.univ` as + a placeholder so it slots into the existing `HasType` framework; + downstream consumers should not rely on this typing for semantic + reasoning. Real interval-typed values would require a `.interval` + CType primitive (REL2). -/ + | dimExpr : HasType Γ (.dimExpr r) .univ + -- ── Structural rules ────────────────────────────────────────────────────────── /-- Core: insert (x, B) into context Γ between a prefix Γ₁ and suffix Γ₂. @@ -141,6 +175,13 @@ private theorem HasType.weaken_core | snd ht ih => intro Γ₁ hΓ; subst hΓ exact HasType.snd (ih Γ₁ rfl) + | ctor => + intro _ _; exact HasType.ctor + | indElim ht hm iht ihm => + intro Γ₁ hΓ; subst hΓ + exact HasType.indElim (iht Γ₁ rfl) (ihm Γ₁ rfl) + | dimExpr => + intro _ _; exact HasType.dimExpr theorem HasType.weaken (x : String) (B : CType) (h : HasType Γ t A) : HasType ((x, B) :: Γ) t A := diff --git a/native/cubical/src/subst.rs b/native/cubical/src/subst.rs index aeaf741..549abef 100644 --- a/native/cubical/src/subst.rs +++ b/native/cubical/src/subst.rs @@ -483,7 +483,103 @@ pub(crate) fn cterm_subst_dim(i: LeanObj, r: LeanObj, t: LeanObj) -> LeanObjMut let ninner = cterm_subst_dim(i, r, inner); mk_term_snd(ninner as LeanObj) } - _ => mk_term_var(ctor_field(t, 0)), // fallback + TERM_DIMEXPR => { + // .dimExpr s — substitute i := r in the inner DimExpr. + let s = ctor_field(t, 0); + let new_s = dim_expr_subst(i, r, s); + let ctor = alloc_ctor(TERM_DIMEXPR, 1); + ctor_set_field(ctor, 0, new_s as LeanObj); + ctor + } + TERM_CTOR => { + // .ctor S c params args — leave schema/params (matches Lean + // approximation), substDim into args. + let schema = ctor_field(t, 0); + let name = ctor_field(t, 1); + let params = ctor_field(t, 2); + let args = ctor_field(t, 3); + retain(schema); retain(name); retain(params); + let new_args = cterm_subst_dim_list(i, r, args); + let ctor = alloc_ctor(TERM_CTOR, 4); + ctor_set_field(ctor, 0, schema); + ctor_set_field(ctor, 1, name); + ctor_set_field(ctor, 2, params); + ctor_set_field(ctor, 3, new_args as LeanObj); + ctor + } + TERM_INDELIM => { + // .indElim S params motive branches target. + let schema = ctor_field(t, 0); + let params = ctor_field(t, 1); + let motive = ctor_field(t, 2); + let branches = ctor_field(t, 3); + let target = ctor_field(t, 4); + retain(schema); retain(params); + let new_motive = cterm_subst_dim(i, r, motive); + let new_branches = cterm_subst_dim_branches(i, r, branches); + let new_target = cterm_subst_dim(i, r, target); + let ctor = alloc_ctor(TERM_INDELIM, 5); + ctor_set_field(ctor, 0, schema); + ctor_set_field(ctor, 1, params); + ctor_set_field(ctor, 2, new_motive as LeanObj); + ctor_set_field(ctor, 3, new_branches as LeanObj); + ctor_set_field(ctor, 4, new_target as LeanObj); + ctor + } + _ => { + // Unknown tag — preserve identity by retaining + boxing as + // raw object (no malformed-CTerm corruption). + retain(t); + t as LeanObjMut + } + } +} + +/// `CTerm.substDim.list i r ts` — map substDim over a CTerm list +/// (REL1 ctor argument lists). +pub(crate) fn cterm_subst_dim_list( + i: LeanObj, r: LeanObj, ts: LeanObj, +) -> LeanObjMut { + match ctor_tag(ts) { + LIST_NIL => lean_box_mut(LIST_NIL as usize), + LIST_CONS => { + let head = ctor_field(ts, 0); + let tail = ctor_field(ts, 1); + let new_head = cterm_subst_dim(i, r, head); + let new_tail = cterm_subst_dim_list(i, r, tail); + let cons = alloc_ctor(LIST_CONS, 2); + ctor_set_field(cons, 0, new_head as LeanObj); + ctor_set_field(cons, 1, new_tail as LeanObj); + cons + } + _ => lean_box_mut(LIST_NIL as usize), + } +} + +/// `CTerm.substDim.branches i r brs` — map substDim over a branch +/// list `List (String × CTerm)` (REL1 indElim). +pub(crate) fn cterm_subst_dim_branches( + i: LeanObj, r: LeanObj, brs: LeanObj, +) -> LeanObjMut { + match ctor_tag(brs) { + LIST_NIL => lean_box_mut(LIST_NIL as usize), + LIST_CONS => { + let head = ctor_field(brs, 0); + let tail = ctor_field(brs, 1); + let name = ctor_field(head, 0); + let body = ctor_field(head, 1); + retain(name); + let new_body = cterm_subst_dim(i, r, body); + let new_pair = alloc_ctor(0, 2); // Prod.mk + ctor_set_field(new_pair, 0, name); + ctor_set_field(new_pair, 1, new_body as LeanObj); + let new_tail = cterm_subst_dim_branches(i, r, tail); + let cons = alloc_ctor(LIST_CONS, 2); + ctor_set_field(cons, 0, new_pair as LeanObj); + ctor_set_field(cons, 1, new_tail as LeanObj); + cons + } + _ => lean_box_mut(LIST_NIL as usize), } }