Adds schema-based inductive type encoding to the engine, supporting both
plain inductives (Nat, List, Bool) and HITs (S¹, propositional truncation,
suspensions) via a single CTypeSchema/CtorSpec/CTypeArg structure.
New CType constructor:
- .ind (S : CTypeSchema) (params : List CType)
New CTerm constructors:
- .dimExpr (r : DimExpr)
- .ctor (S, ctorName, params, args)
- .indElim (S, params, motive, branches, target)
New CVal constructors:
- .vctor (S, ctorName, params, evaluatedArgs)
- .vdimExpr (DimExpr)
New CNeu constructor:
- .nIndElim (S, params, motive, branches, neuTarget)
Five-way mutual block in Syntax.lean (CType, CTerm, CTypeArg, CtorSpec,
CTypeSchema) with Repr derivation post-hoc. Tag layout per
docs/INDUCTIVE_TYPES.md §6: old tags preserved (no shifting). Existing
62/62 smoke + property tests pass unchanged through Rust.
Substitution / dim-absent / endpoint handling:
Subst.lean — substDim, substDimExpr, equation lemmas,
substDim_eq_substDimExpr (mutual with .params helpers).
DimLine.lean — CTerm.dimAbsent + CType.dimAbsent (mutual w/ helpers
for list / branches / params). Plus all five
auxiliary mutual blocks: substDim_absent_aux,
substDimExpr_absent_aux, dimAbsent_after_substDim_aux,
substDim_comm_aux — for both CTerm and CType.
Eval.lean: ctor → vctor (eval'd args); indElim β-reduces on canonical
vctor target via vApp chain over branch body, otherwise stuck via
.nIndElim; dimExpr → vdimExpr. Path-ctor boundary firing and
recursive-arg IH wiring marked TODO REL1.1 (β-reduction works for
non-recursive ctors today).
Readback.lean: vctor → .ctor, vdimExpr → .dimExpr, nIndElim → .indElim.
FFITest.lean: cvalSummary / ctermSummary extended with new constructor
arms.
Topolei (sibling repo) has not yet been migrated — see
docs/INDUCTIVE_TYPES.md §9.1 for the per-file impact map.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Restructure to engine-only contents. Application code (Topolei.*
namespace, canvas-rs / render Rust crates, Main / ProbeTest, naga IR
pipeline, Selection / Subobject / Trace / Obs.Ctx hypothesis stack,
cells-spec / HYPOTHESES / STATUS / NAGA_IR_PLAN docs) moves to the
sibling repo max/topolei.
What moved:
- `Topolei/Cubical/*.lean` (22 files) → `CubicalTransport/*.lean`
with namespace `Topolei.Cubical.*` renamed to `CubicalTransport.*`.
Fully-qualified test types `TopoleiCubical{FFI,Property}Test` →
`CubicalTransport{FFI,Property}Test` for consistency.
- New root file `CubicalTransport.lean` re-exporting all 22 modules.
- Lakefile: package `cubicalTransport`; lib `CubicalTransport`; only
`cubical-test` and `cubical-bench` exes (no GPU link path).
The split criterion: anything an AI shortcut could break that would
cascade-corrupt downstream proofs lives here. Anything that would
only break the application stays in the topolei interface repo.
cubical-test passes 62/62 (smoke + properties) on the renamed engine.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2026-04-27 21:35:01 -06:00
Renamed from Topolei/Cubical/Subst.lean (Browse further)
