f27211f73f
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>
278 lines
13 KiB
Text
278 lines
13 KiB
Text
/-
|
|
Topolei.Cubical.Subst
|
|
=====================
|
|
Dimension substitution for CType (Step 1 of the transport plan).
|
|
|
|
CTerm already has substDim : DimVar → DimExpr → CTerm → CTerm (Syntax.lean).
|
|
Here we add:
|
|
|
|
CTerm.substDimBool : DimVar → Bool → CTerm → CTerm
|
|
— specialises substDim to the two canonical endpoints (false = 0, true = 1).
|
|
— Defined as a thin wrapper; no new recursion.
|
|
|
|
CType.substDim : DimVar → Bool → CType → CType
|
|
— Substitutes a dimension variable with a Bool endpoint throughout a type.
|
|
— CType.path recurses into its CTerm endpoints via substDimBool.
|
|
|
|
Key theorems:
|
|
· Reduction lemmas (univ, pi, path) — proved by rfl.
|
|
· substDimBool_eq_substDim — the wrapper unfolds correctly.
|
|
· substDim_false_of_env / substDim_true_of_env — face connection:
|
|
the Bool environment value at i selects which endpoint substitution applies.
|
|
· substDim_idem — substituting twice at the same Bool is idempotent.
|
|
|
|
Note: substDim_comm (disjoint dimensions commute) is deferred;
|
|
it requires DimExpr.subst commutativity, which needs its own treatment.
|
|
-/
|
|
|
|
import CubicalTransport.Syntax
|
|
|
|
-- ── CTerm.substDimBool ────────────────────────────────────────────────────────
|
|
|
|
/-- Specialise CTerm.substDim to a Bool endpoint.
|
|
false → substitute i with DimExpr.zero (the i=0 face)
|
|
true → substitute i with DimExpr.one (the i=1 face) -/
|
|
def CTerm.substDimBool (i : DimVar) (b : Bool) (t : CTerm) : CTerm :=
|
|
t.substDim i (if b then .one else .zero)
|
|
|
|
-- Unfolds to substDim by definition.
|
|
theorem CTerm.substDimBool_eq_substDim (i : DimVar) (b : Bool) (t : CTerm) :
|
|
t.substDimBool i b = t.substDim i (if b then .one else .zero) := rfl
|
|
|
|
theorem CTerm.substDimBool_false (i : DimVar) (t : CTerm) :
|
|
t.substDimBool i false = t.substDim i .zero := rfl
|
|
|
|
theorem CTerm.substDimBool_true (i : DimVar) (t : CTerm) :
|
|
t.substDimBool i true = t.substDim i .one := rfl
|
|
|
|
-- ── CType.substDim ────────────────────────────────────────────────────────────
|
|
-- Substitute dimension variable i with Bool endpoint b throughout a type.
|
|
-- Path type endpoints are terms, so we delegate to CTerm.substDimBool.
|
|
--
|
|
-- `.ind S params` recurses pointwise through the parameter list via an
|
|
-- explicit mutually-recursive helper (`CType.substDim.params`); this
|
|
-- is the standard way to thread structural recursion through a
|
|
-- `List CType` field of a CType constructor.
|
|
|
|
mutual
|
|
def CType.substDim (i : DimVar) (b : Bool) : CType → CType
|
|
| .univ => .univ
|
|
| .pi A B => .pi (A.substDim i b) (B.substDim i b)
|
|
| .path A a t => .path (A.substDim i b) (a.substDimBool i b) (t.substDimBool i b)
|
|
| .sigma A B => .sigma (A.substDim i b) (B.substDim i b)
|
|
| .glue φ T f fInv sec ret coh A =>
|
|
.glue (φ.substDim i (if b then .one else .zero))
|
|
(T.substDim i b)
|
|
(f.substDimBool i b) (fInv.substDimBool i b)
|
|
(sec.substDimBool i b) (ret.substDimBool i b) (coh.substDimBool i b)
|
|
(A.substDim i b)
|
|
-- REL1: schema-defined inductive. Recurse into params; the schema
|
|
-- itself is static (its boundary CTerms are the schema's data, not
|
|
-- caller-substituted dim-bound terms).
|
|
| .ind S params => .ind S (CType.substDim.params i b params)
|
|
|
|
/-- Pointwise `substDim` through a list of CType parameters. -/
|
|
def CType.substDim.params (i : DimVar) (b : Bool) : List CType → List CType
|
|
| [] => []
|
|
| A :: rest => A.substDim i b :: CType.substDim.params i b rest
|
|
end
|
|
|
|
-- ── CType.substDimExpr ────────────────────────────────────────────────────────
|
|
-- Substitute dimension variable `i` with an arbitrary `DimExpr r` throughout
|
|
-- a type. Generalises `CType.substDim`, which fixes `r` to a Bool endpoint.
|
|
--
|
|
-- Used for *line reversal* in transport: the reversed line is
|
|
-- `A[i := inv i]`, which cannot be expressed as a Bool-endpoint
|
|
-- substitution because `inv i` is an open DimExpr.
|
|
|
|
mutual
|
|
def CType.substDimExpr (i : DimVar) (r : DimExpr) : CType → CType
|
|
| .univ => .univ
|
|
| .pi A B => .pi (A.substDimExpr i r) (B.substDimExpr i r)
|
|
| .path A a t => .path (A.substDimExpr i r) (a.substDim i r) (t.substDim i r)
|
|
| .sigma A B => .sigma (A.substDimExpr i r) (B.substDimExpr i r)
|
|
| .glue φ T f fInv sec ret coh A =>
|
|
.glue (φ.substDim i r)
|
|
(T.substDimExpr i r)
|
|
(f.substDim i r) (fInv.substDim i r)
|
|
(sec.substDim i r) (ret.substDim i r) (coh.substDim i r)
|
|
(A.substDimExpr i r)
|
|
| .ind S params => .ind S (CType.substDimExpr.params i r params)
|
|
|
|
/-- Pointwise `substDimExpr` through a list of CType parameters. -/
|
|
def CType.substDimExpr.params (i : DimVar) (r : DimExpr) : List CType → List CType
|
|
| [] => []
|
|
| A :: rest => A.substDimExpr i r :: CType.substDimExpr.params i r rest
|
|
end
|
|
|
|
-- ── Reduction lemmas ──────────────────────────────────────────────────────────
|
|
-- All proved by rfl: substDim is defined by pattern matching, so these
|
|
-- hold definitionally.
|
|
|
|
namespace CType
|
|
|
|
theorem substDim_univ (i : DimVar) (b : Bool) :
|
|
(univ).substDim i b = .univ := rfl
|
|
|
|
theorem substDim_pi (i : DimVar) (b : Bool) (A B : CType) :
|
|
(pi A B).substDim i b = .pi (A.substDim i b) (B.substDim i b) := rfl
|
|
|
|
theorem substDim_path (i : DimVar) (b : Bool) (A : CType) (a t : CTerm) :
|
|
(path A a t).substDim i b =
|
|
.path (A.substDim i b) (a.substDimBool i b) (t.substDimBool i b) := rfl
|
|
|
|
theorem substDim_sigma (i : DimVar) (b : Bool) (A B : CType) :
|
|
(sigma A B).substDim i b = .sigma (A.substDim i b) (B.substDim i b) := rfl
|
|
|
|
theorem substDim_glue (i : DimVar) (b : Bool) (φ : FaceFormula) (T : CType)
|
|
(f fInv sec ret coh : CTerm) (A : CType) :
|
|
(glue φ T f fInv sec ret coh A).substDim i b =
|
|
.glue (φ.substDim i (if b then .one else .zero))
|
|
(T.substDim i b)
|
|
(f.substDimBool i b) (fInv.substDimBool i b)
|
|
(sec.substDimBool i b) (ret.substDimBool i b) (coh.substDimBool i b)
|
|
(A.substDim i b) := rfl
|
|
|
|
theorem substDim_ind (i : DimVar) (b : Bool) (S : CTypeSchema) (params : List CType) :
|
|
(ind S params).substDim i b = .ind S (CType.substDim.params i b params) := rfl
|
|
|
|
-- ── substDimExpr reduction lemmas ─────────────────────────────────────────────
|
|
|
|
theorem substDimExpr_univ (i : DimVar) (r : DimExpr) :
|
|
(univ).substDimExpr i r = .univ := rfl
|
|
|
|
theorem substDimExpr_pi (i : DimVar) (r : DimExpr) (A B : CType) :
|
|
(pi A B).substDimExpr i r =
|
|
.pi (A.substDimExpr i r) (B.substDimExpr i r) := rfl
|
|
|
|
theorem substDimExpr_path (i : DimVar) (r : DimExpr) (A : CType) (a t : CTerm) :
|
|
(path A a t).substDimExpr i r =
|
|
.path (A.substDimExpr i r) (a.substDim i r) (t.substDim i r) := rfl
|
|
|
|
theorem substDimExpr_sigma (i : DimVar) (r : DimExpr) (A B : CType) :
|
|
(sigma A B).substDimExpr i r =
|
|
.sigma (A.substDimExpr i r) (B.substDimExpr i r) := rfl
|
|
|
|
theorem substDimExpr_glue (i : DimVar) (r : DimExpr) (φ : FaceFormula) (T : CType)
|
|
(f fInv sec ret coh : CTerm) (A : CType) :
|
|
(glue φ T f fInv sec ret coh A).substDimExpr i r =
|
|
.glue (φ.substDim i r)
|
|
(T.substDimExpr i r)
|
|
(f.substDim i r) (fInv.substDim i r)
|
|
(sec.substDim i r) (ret.substDim i r) (coh.substDim i r)
|
|
(A.substDimExpr i r) := rfl
|
|
|
|
theorem substDimExpr_ind (i : DimVar) (r : DimExpr) (S : CTypeSchema) (params : List CType) :
|
|
(ind S params).substDimExpr i r = .ind S (CType.substDimExpr.params i r params) := rfl
|
|
|
|
-- The Bool-endpoint `substDim` is exactly `substDimExpr` at the canonical
|
|
-- endpoint `DimExpr`. Proof is by pattern-matching `def` (rather than the
|
|
-- `induction` tactic) because `CType` is mutually inductive with `CTerm`.
|
|
-- `CTerm.substDimBool` is defined as `CTerm.substDim` at the same DimExpr,
|
|
-- so the path case closes by unfolding both.
|
|
--
|
|
-- `.ind` recurses into params via `substDim_eq_substDimExpr.params`,
|
|
-- a structurally-recursive helper that establishes pointwise equality
|
|
-- on the parameter list.
|
|
|
|
mutual
|
|
def substDim_eq_substDimExpr (i : DimVar) (b : Bool) :
|
|
(A : CType) →
|
|
A.substDim i b = A.substDimExpr i (if b then DimExpr.one else DimExpr.zero)
|
|
| .univ => rfl
|
|
| .pi A B => by
|
|
show CType.pi (A.substDim i b) (B.substDim i b) =
|
|
CType.pi (A.substDimExpr i _) (B.substDimExpr i _)
|
|
rw [substDim_eq_substDimExpr i b A, substDim_eq_substDimExpr i b B]
|
|
| .path A a t => by
|
|
show CType.path (A.substDim i b) (a.substDimBool i b) (t.substDimBool i b) =
|
|
CType.path (A.substDimExpr i _) (a.substDim i _) (t.substDim i _)
|
|
rw [substDim_eq_substDimExpr i b A,
|
|
CTerm.substDimBool_eq_substDim,
|
|
CTerm.substDimBool_eq_substDim]
|
|
| .sigma A B => by
|
|
show CType.sigma (A.substDim i b) (B.substDim i b) =
|
|
CType.sigma (A.substDimExpr i _) (B.substDimExpr i _)
|
|
rw [substDim_eq_substDimExpr i b A, substDim_eq_substDimExpr i b B]
|
|
| .glue φ T f fInv sec ret coh A => by
|
|
show CType.glue
|
|
(φ.substDim i (if b then DimExpr.one else DimExpr.zero))
|
|
(T.substDim i b)
|
|
(f.substDimBool i b) (fInv.substDimBool i b)
|
|
(sec.substDimBool i b) (ret.substDimBool i b) (coh.substDimBool i b)
|
|
(A.substDim i b)
|
|
= CType.glue
|
|
(φ.substDim i _)
|
|
(T.substDimExpr i _)
|
|
(f.substDim i _) (fInv.substDim i _)
|
|
(sec.substDim i _) (ret.substDim i _) (coh.substDim i _)
|
|
(A.substDimExpr i _)
|
|
rw [substDim_eq_substDimExpr i b T,
|
|
substDim_eq_substDimExpr i b A,
|
|
CTerm.substDimBool_eq_substDim,
|
|
CTerm.substDimBool_eq_substDim,
|
|
CTerm.substDimBool_eq_substDim,
|
|
CTerm.substDimBool_eq_substDim,
|
|
CTerm.substDimBool_eq_substDim]
|
|
| .ind S params => by
|
|
show CType.ind S (CType.substDim.params i b params)
|
|
= CType.ind S (CType.substDimExpr.params i _ params)
|
|
rw [substDim_eq_substDimExpr.params i b params]
|
|
|
|
/-- Helper: pointwise equality between `substDim.params` and
|
|
`substDimExpr.params` at the canonical endpoint DimExpr. -/
|
|
def substDim_eq_substDimExpr.params (i : DimVar) (b : Bool) :
|
|
(params : List CType) →
|
|
CType.substDim.params i b params =
|
|
CType.substDimExpr.params i (if b then DimExpr.one else DimExpr.zero) params
|
|
| [] => rfl
|
|
| A :: rest => by
|
|
show A.substDim i b :: CType.substDim.params i b rest
|
|
= A.substDimExpr i _ :: CType.substDimExpr.params i _ rest
|
|
rw [substDim_eq_substDimExpr i b A,
|
|
substDim_eq_substDimExpr.params i b rest]
|
|
end
|
|
|
|
-- ── Face connection ───────────────────────────────────────────────────────────
|
|
-- These lemmas state the relationship between the Bool dimension environment
|
|
-- and which endpoint substitution applies.
|
|
--
|
|
-- Semantics: env i = false means we are at the i=0 face (eq0 i holds).
|
|
-- env i = true means we are at the i=1 face (eq1 i holds).
|
|
-- The correct substitution to apply is therefore substDim i (env i).
|
|
|
|
/-- At the i=0 face (env i = false), substDim i (env i) is substDim i false. -/
|
|
theorem substDim_at_false (i : DimVar) (A : CType) (env : DimVar → Bool)
|
|
(h : env i = false) :
|
|
A.substDim i (env i) = A.substDim i false := by
|
|
rw [h]
|
|
|
|
/-- At the i=1 face (env i = true), substDim i (env i) is substDim i true. -/
|
|
theorem substDim_at_true (i : DimVar) (A : CType) (env : DimVar → Bool)
|
|
(h : env i = true) :
|
|
A.substDim i (env i) = A.substDim i true := by
|
|
rw [h]
|
|
|
|
-- ── Deferred: idempotence and commutativity ───────────────────────────────────
|
|
-- substDim_idem : (A.substDim i b).substDim i b = A.substDim i b
|
|
-- substDim_comm : for i ≠ j, (A.substDim i b).substDim j c = (A.substDim j c).substDim i b
|
|
--
|
|
-- Both require simultaneous induction over the CType/CTerm mutual inductive,
|
|
-- which needs a `mutual` proof block or a size-indexed recursor.
|
|
-- Deferred to a later pass after the DimLine and transport layers are in place.
|
|
--
|
|
-- Correctness argument (informal):
|
|
-- · After substDim i b, every DimExpr referencing i becomes zero or one
|
|
-- (neither of which contains free variables), so a second substDim i b
|
|
-- finds nothing left to substitute. Idempotence follows.
|
|
-- · Substituting disjoint dimensions i ≠ j affects non-overlapping parts
|
|
-- of every DimExpr (DimExpr.subst is capture-avoiding), so order is irrelevant.
|
|
|
|
theorem substDim_comm_univ (i j : DimVar) (b c : Bool) :
|
|
((univ : CType).substDim i b).substDim j c =
|
|
((univ : CType).substDim j c).substDim i b := rfl
|
|
|
|
end CType
|
|
|
|
-- Note: dimAbsent, substDimBool_idem, and substDim_idem are proved in DimLine.lean,
|
|
-- which is downstream in the import chain and has access to dimAbsent predicates.
|