From f27211f73ff3c4ff1994fb742d55a7ef43ecf5c0 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Thu, 30 Apr 2026 15:09:39 -0600 Subject: [PATCH] REL1 foundation: schema-based inductive + HIT CTypes (Lean side) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- CubicalTransport/DimLine.lean | 521 +++++++++++++++++++++++---------- CubicalTransport/Eval.lean | 36 +++ CubicalTransport/FFITest.lean | 60 ++-- CubicalTransport/Readback.lean | 9 + CubicalTransport/Subst.lean | 198 ++++++++----- CubicalTransport/Syntax.lean | 149 +++++++++- CubicalTransport/Value.lean | 27 ++ 7 files changed, 748 insertions(+), 252 deletions(-) diff --git a/CubicalTransport/DimLine.lean b/CubicalTransport/DimLine.lean index 8001eb1..28c315a 100644 --- a/CubicalTransport/DimLine.lean +++ b/CubicalTransport/DimLine.lean @@ -75,6 +75,15 @@ mutual | .pair a b => a.dimAbsent i && b.dimAbsent i | .fst t => t.dimAbsent i | .snd t => t.dimAbsent i + -- REL1 inductive-type constructors. Schema and ctor/elim *params* + -- are static (caller-supplied externally to any binder we'd be + -- substituting into) — same approximation as transp/comp's `A`. + | .dimExpr s => s.dimAbsent i + | .ctor _ _ _ args => CTerm.dimAbsent.list i args + | .indElim _ _ motive branches target => + motive.dimAbsent i && + CTerm.dimAbsent.branches i branches && + target.dimAbsent i /-- Helper: check that `i` is absent from every clause in a system. -/ def CTerm.dimAbsent.clauses (i : DimVar) : @@ -82,18 +91,38 @@ mutual | [] => true | (φ, u) :: rest => φ.dimAbsent i && u.dimAbsent i && CTerm.dimAbsent.clauses i rest + + /-- Helper: check `i` absent from every CTerm in a list (ctor args). -/ + def CTerm.dimAbsent.list (i : DimVar) : List CTerm → Bool + | [] => true + | t :: rest => t.dimAbsent i && CTerm.dimAbsent.list i rest + + /-- Helper: check `i` absent from every branch body of an `indElim`. -/ + def CTerm.dimAbsent.branches (i : DimVar) : + List (String × CTerm) → Bool + | [] => true + | (_, b) :: rest => + b.dimAbsent i && CTerm.dimAbsent.branches i rest end -def CType.dimAbsent (i : DimVar) : CType → Bool - | .univ => true - | .pi A B => A.dimAbsent i && B.dimAbsent i - | .path A a t => A.dimAbsent i && a.dimAbsent i && t.dimAbsent i - | .sigma A B => A.dimAbsent i && B.dimAbsent i - | .glue φ T f fInv sec ret coh A => - φ.dimAbsent i && T.dimAbsent i && - f.dimAbsent i && fInv.dimAbsent i && - sec.dimAbsent i && ret.dimAbsent i && coh.dimAbsent i && - A.dimAbsent i +mutual + def CType.dimAbsent (i : DimVar) : CType → Bool + | .univ => true + | .pi A B => A.dimAbsent i && B.dimAbsent i + | .path A a t => A.dimAbsent i && a.dimAbsent i && t.dimAbsent i + | .sigma A B => A.dimAbsent i && B.dimAbsent i + | .glue φ T f fInv sec ret coh A => + φ.dimAbsent i && T.dimAbsent i && + f.dimAbsent i && fInv.dimAbsent i && + sec.dimAbsent i && ret.dimAbsent i && coh.dimAbsent i && + A.dimAbsent i + | .ind _ params => CType.dimAbsent.params i params + + /-- Helper: check `i` absent from every CType in a parameter list. -/ + def CType.dimAbsent.params (i : DimVar) : List CType → Bool + | [] => true + | A :: rest => A.dimAbsent i && CType.dimAbsent.params i rest +end -- ── Absence → subst is identity: DimExpr level ─────────────────────────────── @@ -201,6 +230,21 @@ mutual simp only [CTerm.dimAbsent] at h simp only [CTerm.substDim] rw [CTerm.substDim_absent_aux i r t h] + | .dimExpr s, h => by + simp only [CTerm.dimAbsent] at h + simp only [CTerm.substDim] + rw [DimExpr.subst_of_absent i r s h] + | .ctor S c params args, h => by + simp only [CTerm.dimAbsent] at h + simp only [CTerm.substDim] + rw [CTerm.substDim.list_of_absent i r args h] + | .indElim S params motive branches target, h => by + simp only [CTerm.dimAbsent, Bool.and_eq_true] at h + simp only [CTerm.substDim] + obtain ⟨⟨hm, hbr⟩, htg⟩ := h + rw [CTerm.substDim_absent_aux i r motive hm, + CTerm.substDim.branches_of_absent i r branches hbr, + CTerm.substDim_absent_aux i r target htg] /-- Helper: `substDim.clauses` is identity on clause lists whose every `(face, body)` pair has `i` absent. -/ @@ -216,6 +260,32 @@ mutual rw [FaceFormula.substDim_of_absent i r φ hφ, CTerm.substDim_absent_aux i r u hu, CTerm.substDim.clauses_of_absent i r rest hrest] + + /-- Helper: `substDim.list` is identity on CTerm lists with `i` absent + from every element. -/ + private def CTerm.substDim.list_of_absent (i : DimVar) (r : DimExpr) : + (ts : List CTerm) → + CTerm.dimAbsent.list i ts = true → + CTerm.substDim.list i r ts = ts + | [], _ => rfl + | t :: rest, h => by + simp only [CTerm.dimAbsent.list, Bool.and_eq_true] at h + simp only [CTerm.substDim.list] + rw [CTerm.substDim_absent_aux i r t h.1, + CTerm.substDim.list_of_absent i r rest h.2] + + /-- Helper: `substDim.branches` is identity on branch lists whose every + body has `i` absent. -/ + private def CTerm.substDim.branches_of_absent (i : DimVar) (r : DimExpr) : + (brs : List (String × CTerm)) → + CTerm.dimAbsent.branches i brs = true → + CTerm.substDim.branches i r brs = brs + | [], _ => rfl + | (n, b) :: rest, h => by + simp only [CTerm.dimAbsent.branches, Bool.and_eq_true] at h + simp only [CTerm.substDim.branches] + rw [CTerm.substDim_absent_aux i r b h.1, + CTerm.substDim.branches_of_absent i r rest h.2] end /-- Generalised: `CTerm.substDim i r t = t` whenever `i` is absent from `t`, @@ -230,49 +300,68 @@ theorem CTerm.substDimBool_of_absent (i : DimVar) (b : Bool) (t : CTerm) unfold CTerm.substDimBool exact CTerm.substDim_of_absent i _ t h -private def CType.substDim_absent_aux (i : DimVar) (b : Bool) : - (A : CType) → CType.dimAbsent i A = true → CType.substDim i b A = A - | .univ, _ => rfl - | .pi A B, h => by - simp only [CType.dimAbsent, Bool.and_eq_true] at h - show CType.pi (CType.substDim i b A) (CType.substDim i b B) = CType.pi A B - congr 1 - · exact CType.substDim_absent_aux i b A h.1 - · exact CType.substDim_absent_aux i b B h.2 - | .path A a t, h => by - simp only [CType.dimAbsent, Bool.and_eq_true] at h - show CType.path (CType.substDim i b A) - (CTerm.substDimBool i b a) (CTerm.substDimBool i b t) = - CType.path A a t - congr 1 - · exact CType.substDim_absent_aux i b A h.1.1 - · exact CTerm.substDimBool_of_absent i b a h.1.2 - · exact CTerm.substDimBool_of_absent i b t h.2 - | .sigma A B, h => by - simp only [CType.dimAbsent, Bool.and_eq_true] at h - show CType.sigma (CType.substDim i b A) (CType.substDim i b B) = - CType.sigma A B - congr 1 - · exact CType.substDim_absent_aux i b A h.1 - · exact CType.substDim_absent_aux i b B h.2 - | .glue φ T f fInv sec ret coh A, h => by - simp only [CType.dimAbsent, Bool.and_eq_true] at h - show CType.glue (φ.substDim i (if b then DimExpr.one else DimExpr.zero)) - (CType.substDim i b T) - (CTerm.substDimBool i b f) (CTerm.substDimBool i b fInv) - (CTerm.substDimBool i b sec) (CTerm.substDimBool i b ret) - (CTerm.substDimBool i b coh) - (CType.substDim i b A) = - CType.glue φ T f fInv sec ret coh A - obtain ⟨⟨⟨⟨⟨⟨⟨hφ, hT⟩, hf⟩, hfInv⟩, hsec⟩, hret⟩, hcoh⟩, hA⟩ := h - rw [FaceFormula.substDim_of_absent i _ φ hφ, - CType.substDim_absent_aux i b T hT, - CTerm.substDimBool_of_absent i b f hf, - CTerm.substDimBool_of_absent i b fInv hfInv, - CTerm.substDimBool_of_absent i b sec hsec, - CTerm.substDimBool_of_absent i b ret hret, - CTerm.substDimBool_of_absent i b coh hcoh, - CType.substDim_absent_aux i b A hA] +mutual + private def CType.substDim_absent_aux (i : DimVar) (b : Bool) : + (A : CType) → CType.dimAbsent i A = true → CType.substDim i b A = A + | .univ, _ => rfl + | .pi A B, h => by + simp only [CType.dimAbsent, Bool.and_eq_true] at h + show CType.pi (CType.substDim i b A) (CType.substDim i b B) = CType.pi A B + congr 1 + · exact CType.substDim_absent_aux i b A h.1 + · exact CType.substDim_absent_aux i b B h.2 + | .path A a t, h => by + simp only [CType.dimAbsent, Bool.and_eq_true] at h + show CType.path (CType.substDim i b A) + (CTerm.substDimBool i b a) (CTerm.substDimBool i b t) = + CType.path A a t + congr 1 + · exact CType.substDim_absent_aux i b A h.1.1 + · exact CTerm.substDimBool_of_absent i b a h.1.2 + · exact CTerm.substDimBool_of_absent i b t h.2 + | .sigma A B, h => by + simp only [CType.dimAbsent, Bool.and_eq_true] at h + show CType.sigma (CType.substDim i b A) (CType.substDim i b B) = + CType.sigma A B + congr 1 + · exact CType.substDim_absent_aux i b A h.1 + · exact CType.substDim_absent_aux i b B h.2 + | .glue φ T f fInv sec ret coh A, h => by + simp only [CType.dimAbsent, Bool.and_eq_true] at h + show CType.glue (φ.substDim i (if b then DimExpr.one else DimExpr.zero)) + (CType.substDim i b T) + (CTerm.substDimBool i b f) (CTerm.substDimBool i b fInv) + (CTerm.substDimBool i b sec) (CTerm.substDimBool i b ret) + (CTerm.substDimBool i b coh) + (CType.substDim i b A) = + CType.glue φ T f fInv sec ret coh A + obtain ⟨⟨⟨⟨⟨⟨⟨hφ, hT⟩, hf⟩, hfInv⟩, hsec⟩, hret⟩, hcoh⟩, hA⟩ := h + rw [FaceFormula.substDim_of_absent i _ φ hφ, + CType.substDim_absent_aux i b T hT, + CTerm.substDimBool_of_absent i b f hf, + CTerm.substDimBool_of_absent i b fInv hfInv, + CTerm.substDimBool_of_absent i b sec hsec, + CTerm.substDimBool_of_absent i b ret hret, + CTerm.substDimBool_of_absent i b coh hcoh, + CType.substDim_absent_aux i b A hA] + | .ind S params, h => by + simp only [CType.dimAbsent] at h + simp only [CType.substDim] + rw [CType.substDim.params_of_absent i b params h] + + /-- Helper: `CType.substDim.params i b` is identity on CType lists with + `i` absent from every element. -/ + private def CType.substDim.params_of_absent (i : DimVar) (b : Bool) : + (params : List CType) → + CType.dimAbsent.params i params = true → + CType.substDim.params i b params = params + | [], _ => rfl + | A :: rest, h => by + simp only [CType.dimAbsent.params, Bool.and_eq_true] at h + simp only [CType.substDim.params] + rw [CType.substDim_absent_aux i b A h.1, + CType.substDim.params_of_absent i b rest h.2] +end theorem CType.substDim_of_absent (i : DimVar) (b : Bool) (A : CType) (h : CType.dimAbsent i A = true) : CType.substDim i b A = A := @@ -280,47 +369,66 @@ theorem CType.substDim_of_absent (i : DimVar) (b : Bool) (A : CType) -- ── CType.substDimExpr absent-subst (general DimExpr version) ───────────────── -private def CType.substDimExpr_absent_aux (i : DimVar) (r : DimExpr) : - (A : CType) → CType.dimAbsent i A = true → CType.substDimExpr i r A = A - | .univ, _ => rfl - | .pi A B, h => by - simp only [CType.dimAbsent, Bool.and_eq_true] at h - show CType.pi (A.substDimExpr i r) (B.substDimExpr i r) = CType.pi A B - congr 1 - · exact CType.substDimExpr_absent_aux i r A h.1 - · exact CType.substDimExpr_absent_aux i r B h.2 - | .path A a t, h => by - simp only [CType.dimAbsent, Bool.and_eq_true] at h - show CType.path (A.substDimExpr i r) (a.substDim i r) (t.substDim i r) = - CType.path A a t - congr 1 - · exact CType.substDimExpr_absent_aux i r A h.1.1 - · exact CTerm.substDim_of_absent i r a h.1.2 - · exact CTerm.substDim_of_absent i r t h.2 - | .sigma A B, h => by - simp only [CType.dimAbsent, Bool.and_eq_true] at h - show CType.sigma (A.substDimExpr i r) (B.substDimExpr i r) = - CType.sigma A B - congr 1 - · exact CType.substDimExpr_absent_aux i r A h.1 - · exact CType.substDimExpr_absent_aux i r B h.2 - | .glue φ T f fInv sec ret coh A, h => by - simp only [CType.dimAbsent, Bool.and_eq_true] at h - show CType.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) = - CType.glue φ T f fInv sec ret coh A - obtain ⟨⟨⟨⟨⟨⟨⟨hφ, hT⟩, hf⟩, hfInv⟩, hsec⟩, hret⟩, hcoh⟩, hA⟩ := h - rw [FaceFormula.substDim_of_absent i r φ hφ, - CType.substDimExpr_absent_aux i r T hT, - CTerm.substDim_of_absent i r f hf, - CTerm.substDim_of_absent i r fInv hfInv, - CTerm.substDim_of_absent i r sec hsec, - CTerm.substDim_of_absent i r ret hret, - CTerm.substDim_of_absent i r coh hcoh, - CType.substDimExpr_absent_aux i r A hA] +mutual + private def CType.substDimExpr_absent_aux (i : DimVar) (r : DimExpr) : + (A : CType) → CType.dimAbsent i A = true → CType.substDimExpr i r A = A + | .univ, _ => rfl + | .pi A B, h => by + simp only [CType.dimAbsent, Bool.and_eq_true] at h + show CType.pi (A.substDimExpr i r) (B.substDimExpr i r) = CType.pi A B + congr 1 + · exact CType.substDimExpr_absent_aux i r A h.1 + · exact CType.substDimExpr_absent_aux i r B h.2 + | .path A a t, h => by + simp only [CType.dimAbsent, Bool.and_eq_true] at h + show CType.path (A.substDimExpr i r) (a.substDim i r) (t.substDim i r) = + CType.path A a t + congr 1 + · exact CType.substDimExpr_absent_aux i r A h.1.1 + · exact CTerm.substDim_of_absent i r a h.1.2 + · exact CTerm.substDim_of_absent i r t h.2 + | .sigma A B, h => by + simp only [CType.dimAbsent, Bool.and_eq_true] at h + show CType.sigma (A.substDimExpr i r) (B.substDimExpr i r) = + CType.sigma A B + congr 1 + · exact CType.substDimExpr_absent_aux i r A h.1 + · exact CType.substDimExpr_absent_aux i r B h.2 + | .glue φ T f fInv sec ret coh A, h => by + simp only [CType.dimAbsent, Bool.and_eq_true] at h + show CType.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) = + CType.glue φ T f fInv sec ret coh A + obtain ⟨⟨⟨⟨⟨⟨⟨hφ, hT⟩, hf⟩, hfInv⟩, hsec⟩, hret⟩, hcoh⟩, hA⟩ := h + rw [FaceFormula.substDim_of_absent i r φ hφ, + CType.substDimExpr_absent_aux i r T hT, + CTerm.substDim_of_absent i r f hf, + CTerm.substDim_of_absent i r fInv hfInv, + CTerm.substDim_of_absent i r sec hsec, + CTerm.substDim_of_absent i r ret hret, + CTerm.substDim_of_absent i r coh hcoh, + CType.substDimExpr_absent_aux i r A hA] + | .ind S params, h => by + simp only [CType.dimAbsent] at h + simp only [CType.substDimExpr] + rw [CType.substDimExpr.params_of_absent i r params h] + + /-- Helper: `CType.substDimExpr.params i r` is identity on CType lists + with `i` absent from every element. -/ + private def CType.substDimExpr.params_of_absent (i : DimVar) (r : DimExpr) : + (params : List CType) → + CType.dimAbsent.params i params = true → + CType.substDimExpr.params i r params = params + | [], _ => rfl + | A :: rest, h => by + simp only [CType.dimAbsent.params, Bool.and_eq_true] at h + simp only [CType.substDimExpr.params] + rw [CType.substDimExpr_absent_aux i r A h.1, + CType.substDimExpr.params_of_absent i r rest h.2] +end /-- Generalised: when `i` is absent from `A`, substituting `i` by any `DimExpr` leaves `A` unchanged. Equivalently: line reversal (via `i := inv i`) is @@ -447,6 +555,17 @@ mutual | .snd t => by simp only [CTerm.substDim, CTerm.dimAbsent, CTerm.dimAbsent_after_substDim_aux i r hr t] + | .dimExpr s => by + simp only [CTerm.substDim, CTerm.dimAbsent, + DimExpr.dimAbsent_after_subst i r hr s] + | .ctor S c params args => by + simp only [CTerm.substDim, CTerm.dimAbsent, + CTerm.dimAbsent.list_after_substDim i r hr args] + | .indElim S params motive branches target => by + simp only [CTerm.substDim, CTerm.dimAbsent, + CTerm.dimAbsent_after_substDim_aux i r hr motive, + CTerm.dimAbsent.branches_after_substDim i r hr branches, + CTerm.dimAbsent_after_substDim_aux i r hr target, Bool.and_self] /-- Helper: `i` is absent from every clause in the result of substituting `i := r` in a clause list (provided `r` doesn't mention `i`). -/ @@ -462,6 +581,30 @@ mutual · exact FaceFormula.dimAbsent_after_substDim i r hr φ · exact CTerm.dimAbsent_after_substDim_aux i r hr u · exact CTerm.dimAbsent.clauses_after_substDim i r hr rest + + /-- Helper: `i` is absent from every CTerm in the result of substituting + `i := r` in a CTerm list. -/ + private def CTerm.dimAbsent.list_after_substDim + (i : DimVar) (r : DimExpr) (hr : r.dimAbsent i = true) : + (ts : List CTerm) → + CTerm.dimAbsent.list i (CTerm.substDim.list i r ts) = true + | [] => rfl + | t :: rest => by + simp only [CTerm.substDim.list, CTerm.dimAbsent.list, + CTerm.dimAbsent_after_substDim_aux i r hr t, + CTerm.dimAbsent.list_after_substDim i r hr rest, Bool.and_self] + + /-- Helper: `i` is absent from every branch body in the result of + substituting `i := r` in a branch list. -/ + private def CTerm.dimAbsent.branches_after_substDim + (i : DimVar) (r : DimExpr) (hr : r.dimAbsent i = true) : + (brs : List (String × CTerm)) → + CTerm.dimAbsent.branches i (CTerm.substDim.branches i r brs) = true + | [] => rfl + | (n, b) :: rest => by + simp only [CTerm.substDim.branches, CTerm.dimAbsent.branches, + CTerm.dimAbsent_after_substDim_aux i r hr b, + CTerm.dimAbsent.branches_after_substDim i r hr rest, Bool.and_self] end theorem CTerm.dimAbsent_after_substDimBool (i : DimVar) (b : Bool) (t : CTerm) : @@ -470,33 +613,48 @@ theorem CTerm.dimAbsent_after_substDimBool (i : DimVar) (b : Bool) (t : CTerm) : -- Step 3: after CType.substDim i b, i is absent from the type. -private def CType.dimAbsent_after_substDim_aux (i : DimVar) (b : Bool) : - (A : CType) → (A.substDim i b).dimAbsent i = true - | .univ => rfl - | .pi A B => by - simp only [CType.substDim, CType.dimAbsent, - CType.dimAbsent_after_substDim_aux i b A, - CType.dimAbsent_after_substDim_aux i b B, Bool.and_self] - | .path A a t => by - simp only [CType.substDim, CType.dimAbsent, - CType.dimAbsent_after_substDim_aux i b A, - CTerm.dimAbsent_after_substDimBool i b a, - CTerm.dimAbsent_after_substDimBool i b t, Bool.and_self] - | .sigma A B => by - simp only [CType.substDim, CType.dimAbsent, - CType.dimAbsent_after_substDim_aux i b A, - CType.dimAbsent_after_substDim_aux i b B, Bool.and_self] - | .glue φ T f fInv sec ret coh A => by - simp only [CType.substDim, CType.dimAbsent, - FaceFormula.dimAbsent_after_substDim i _ - (DimExpr.dimAbsent_endpoint i b) φ, - CType.dimAbsent_after_substDim_aux i b T, - CTerm.dimAbsent_after_substDimBool i b f, - CTerm.dimAbsent_after_substDimBool i b fInv, - CTerm.dimAbsent_after_substDimBool i b sec, - CTerm.dimAbsent_after_substDimBool i b ret, - CTerm.dimAbsent_after_substDimBool i b coh, - CType.dimAbsent_after_substDim_aux i b A, Bool.and_self] +mutual + private def CType.dimAbsent_after_substDim_aux (i : DimVar) (b : Bool) : + (A : CType) → (A.substDim i b).dimAbsent i = true + | .univ => rfl + | .pi A B => by + simp only [CType.substDim, CType.dimAbsent, + CType.dimAbsent_after_substDim_aux i b A, + CType.dimAbsent_after_substDim_aux i b B, Bool.and_self] + | .path A a t => by + simp only [CType.substDim, CType.dimAbsent, + CType.dimAbsent_after_substDim_aux i b A, + CTerm.dimAbsent_after_substDimBool i b a, + CTerm.dimAbsent_after_substDimBool i b t, Bool.and_self] + | .sigma A B => by + simp only [CType.substDim, CType.dimAbsent, + CType.dimAbsent_after_substDim_aux i b A, + CType.dimAbsent_after_substDim_aux i b B, Bool.and_self] + | .glue φ T f fInv sec ret coh A => by + simp only [CType.substDim, CType.dimAbsent, + FaceFormula.dimAbsent_after_substDim i _ + (DimExpr.dimAbsent_endpoint i b) φ, + CType.dimAbsent_after_substDim_aux i b T, + CTerm.dimAbsent_after_substDimBool i b f, + CTerm.dimAbsent_after_substDimBool i b fInv, + CTerm.dimAbsent_after_substDimBool i b sec, + CTerm.dimAbsent_after_substDimBool i b ret, + CTerm.dimAbsent_after_substDimBool i b coh, + CType.dimAbsent_after_substDim_aux i b A, Bool.and_self] + | .ind S params => by + simp only [CType.substDim, CType.dimAbsent, + CType.dimAbsent.params_after_substDim i b params] + + /-- Helper: `i` absent from every CType in `substDim.params i b ps`. -/ + private def CType.dimAbsent.params_after_substDim (i : DimVar) (b : Bool) : + (params : List CType) → + CType.dimAbsent.params i (CType.substDim.params i b params) = true + | [] => rfl + | A :: rest => by + simp only [CType.substDim.params, CType.dimAbsent.params, + CType.dimAbsent_after_substDim_aux i b A, + CType.dimAbsent.params_after_substDim i b rest, Bool.and_self] +end theorem CType.dimAbsent_after_substDim (i : DimVar) (b : Bool) (A : CType) : (A.substDim i b).dimAbsent i = true := @@ -632,6 +790,20 @@ mutual | .snd t => by simp only [CTerm.substDim] exact congrArg CTerm.snd (CTerm.substDim_comm_aux i j r s hij hrj hsi t) + | .dimExpr e => by + simp only [CTerm.substDim] + exact congrArg CTerm.dimExpr + (DimExpr.subst_comm i j r s hij hrj hsi e).symm + | .ctor S c params args => by + simp only [CTerm.substDim] + exact congrArg (CTerm.ctor S c params) + (CTerm.substDim.list_comm_aux i j r s hij hrj hsi args) + | .indElim S params motive branches target => by + simp only [CTerm.substDim] + congr 1 + · exact CTerm.substDim_comm_aux i j r s hij hrj hsi motive + · exact CTerm.substDim.branches_comm_aux i j r s hij hrj hsi branches + · exact CTerm.substDim_comm_aux i j r s hij hrj hsi target /-- Helper: `substDim.clauses` commutes on disjoint dim variables. -/ private def CTerm.substDim.clauses_comm_aux @@ -648,6 +820,34 @@ mutual (FaceFormula.substDim_comm i j r s hij hrj hsi φ) (CTerm.substDim_comm_aux i j r s hij hrj hsi u) · exact CTerm.substDim.clauses_comm_aux i j r s hij hrj hsi rest + + /-- Helper: `substDim.list` commutes on disjoint dim variables. -/ + private def CTerm.substDim.list_comm_aux + (i j : DimVar) (r s : DimExpr) (hij : i ≠ j) + (hrj : r.dimAbsent j = true) (hsi : s.dimAbsent i = true) : + (ts : List CTerm) → + CTerm.substDim.list j s (CTerm.substDim.list i r ts) = + CTerm.substDim.list i r (CTerm.substDim.list j s ts) + | [] => rfl + | t :: rest => by + simp only [CTerm.substDim.list] + congr 1 + · exact CTerm.substDim_comm_aux i j r s hij hrj hsi t + · exact CTerm.substDim.list_comm_aux i j r s hij hrj hsi rest + + /-- Helper: `substDim.branches` commutes on disjoint dim variables. -/ + private def CTerm.substDim.branches_comm_aux + (i j : DimVar) (r s : DimExpr) (hij : i ≠ j) + (hrj : r.dimAbsent j = true) (hsi : s.dimAbsent i = true) : + (brs : List (String × CTerm)) → + CTerm.substDim.branches j s (CTerm.substDim.branches i r brs) = + CTerm.substDim.branches i r (CTerm.substDim.branches j s brs) + | [] => rfl + | (n, b) :: rest => by + simp only [CTerm.substDim.branches] + congr 1 + · exact Prod.ext rfl (CTerm.substDim_comm_aux i j r s hij hrj hsi b) + · exact CTerm.substDim.branches_comm_aux i j r s hij hrj hsi rest end theorem CTerm.substDimBool_comm @@ -659,36 +859,55 @@ theorem CTerm.substDimBool_comm -- CType commutativity -private def CType.substDim_comm_aux - (i j : DimVar) (b c : Bool) (hij : i ≠ j) : - (A : CType) → - (A.substDim i b).substDim j c = - (A.substDim j c).substDim i b - | .univ => rfl - | .pi A B => by - simp only [CType.substDim] - rw [CType.substDim_comm_aux i j b c hij A, - CType.substDim_comm_aux i j b c hij B] - | .path A a t => by - simp only [CType.substDim] - rw [CType.substDim_comm_aux i j b c hij A, - CTerm.substDimBool_comm i j b c hij a, - CTerm.substDimBool_comm i j b c hij t] - | .sigma A B => by - simp only [CType.substDim] - rw [CType.substDim_comm_aux i j b c hij A, - CType.substDim_comm_aux i j b c hij B] - | .glue φ T f fInv sec ret coh A => by - simp only [CType.substDim] - rw [FaceFormula.substDim_comm i j _ _ hij - (DimExpr.dimAbsent_endpoint j b) (DimExpr.dimAbsent_endpoint i c) φ, - CType.substDim_comm_aux i j b c hij T, - CTerm.substDimBool_comm i j b c hij f, - CTerm.substDimBool_comm i j b c hij fInv, - CTerm.substDimBool_comm i j b c hij sec, - CTerm.substDimBool_comm i j b c hij ret, - CTerm.substDimBool_comm i j b c hij coh, - CType.substDim_comm_aux i j b c hij A] +mutual + private def CType.substDim_comm_aux + (i j : DimVar) (b c : Bool) (hij : i ≠ j) : + (A : CType) → + (A.substDim i b).substDim j c = + (A.substDim j c).substDim i b + | .univ => rfl + | .pi A B => by + simp only [CType.substDim] + rw [CType.substDim_comm_aux i j b c hij A, + CType.substDim_comm_aux i j b c hij B] + | .path A a t => by + simp only [CType.substDim] + rw [CType.substDim_comm_aux i j b c hij A, + CTerm.substDimBool_comm i j b c hij a, + CTerm.substDimBool_comm i j b c hij t] + | .sigma A B => by + simp only [CType.substDim] + rw [CType.substDim_comm_aux i j b c hij A, + CType.substDim_comm_aux i j b c hij B] + | .glue φ T f fInv sec ret coh A => by + simp only [CType.substDim] + rw [FaceFormula.substDim_comm i j _ _ hij + (DimExpr.dimAbsent_endpoint j b) (DimExpr.dimAbsent_endpoint i c) φ, + CType.substDim_comm_aux i j b c hij T, + CTerm.substDimBool_comm i j b c hij f, + CTerm.substDimBool_comm i j b c hij fInv, + CTerm.substDimBool_comm i j b c hij sec, + CTerm.substDimBool_comm i j b c hij ret, + CTerm.substDimBool_comm i j b c hij coh, + CType.substDim_comm_aux i j b c hij A] + | .ind S params => by + simp only [CType.substDim] + exact congrArg (CType.ind S) + (CType.substDim.params_comm_aux i j b c hij params) + + /-- Helper: `CType.substDim.params` commutes on disjoint dim variables. -/ + private def CType.substDim.params_comm_aux + (i j : DimVar) (b c : Bool) (hij : i ≠ j) : + (params : List CType) → + CType.substDim.params j c (CType.substDim.params i b params) = + CType.substDim.params i b (CType.substDim.params j c params) + | [] => rfl + | A :: rest => by + simp only [CType.substDim.params] + congr 1 + · exact CType.substDim_comm_aux i j b c hij A + · exact CType.substDim.params_comm_aux i j b c hij rest +end theorem CType.substDim_comm (i j : DimVar) (b c : Bool) (hij : i ≠ j) (A : CType) : diff --git a/CubicalTransport/Eval.lean b/CubicalTransport/Eval.lean index a0ae439..aeaf807 100644 --- a/CubicalTransport/Eval.lean +++ b/CubicalTransport/Eval.lean @@ -119,6 +119,38 @@ mutual | .pair a b => .vpair (eval env a) (eval env b) | .fst t => vFst (eval env t) | .snd t => vSnd (eval env t) + -- REL1 inductive-type constructors. + | .dimExpr r => .vdimExpr r + | .ctor S c params args => + -- Produce a canonical constructor value with all args evaluated. + -- (Boundary firing for path ctors lands in a follow-up — REL1 + -- design doc §4: when a `.dim`-typed arg evaluates to .zero/.one + -- and matches a clause in `S.ctors[c].boundary`, we should fire + -- that clause body instead. TODO REL1.1.) + .vctor S c params (args.map (eval env)) + | .indElim S params motive branches target => + -- β-reduce on a canonical `vctor`; otherwise build a stuck + -- `.nIndElim` that preserves env-evaluated motive and branches + -- so it can unstick when target later resolves. + match eval env target with + | .vctor _ c _ argsV => + match List.lookup c branches with + | some body => + -- Apply branch body to constructor's args via repeated + -- `vApp` — the body is curried: λ a₁ … aₙ. result. + -- Recursive-arg hypotheses (the IH passed alongside each + -- `.self` arg in the design doc §5) are not yet wired + -- here; an `indElim` of a non-recursive ctor is fully + -- handled, but recursive ctors land their branch body + -- with only the constructor args (no IH) — TODO REL1.1. + argsV.foldl (fun f a => vApp f a) (eval env body) + | none => + .vneu (.nvar s!"") + | .vneu n => + .vneu (.nIndElim S params (eval env motive) + (branches.map (fun (nm, b) => (nm, eval env b))) n) + | _ => + .vneu (.nvar "") /-- First projection at the value level. β-reduces `vpair`; pushes a stuck neutral into `nfst`. Projecting any other value shape is a @@ -176,6 +208,8 @@ mutual | .vTubeApp _ _, _ => .vneu (.nvar "") | .vPathTransp _ _ _ _ _ _ _, _ => .vneu (.nvar "") | .vpair _ _, _ => .vneu (.nvar "") + | .vctor _ _ _ _, _ => .vneu (.nvar "") + | .vdimExpr _, _ => .vneu (.nvar "") /-- Apply a value to a dimension expression. β-reduces `vplam` closures by substituting the dim in the body and re-evaluating; pushes stuck @@ -206,6 +240,8 @@ mutual | .vHCompFun _ _ _ _, _ => .vneu (.nvar "") | .vCompFun _ _ _ _ _ _ _, _ => .vneu (.nvar "") | .vpair _ _, _ => .vneu (.nvar "") + | .vctor _ _ _ _, _ => .vneu (.nvar "") + | .vdimExpr _, _ => .vneu (.nvar "") /-- Homogeneous composition at the value level. The type `A` is *homogeneous* (doesn't vary along `i`); the tube and base are diff --git a/CubicalTransport/FFITest.lean b/CubicalTransport/FFITest.lean index 75f31d3..e01c19a 100644 --- a/CubicalTransport/FFITest.lean +++ b/CubicalTransport/FFITest.lean @@ -26,35 +26,41 @@ namespace CubicalTransportFFITest -- ── Summarisers ──────────────────────────────────────────────────────────── def cvalSummary : CVal → String - | .vneu (.nvar s) => s!"vneu nvar {s}" - | .vneu (.napp _ _) => "vneu napp" - | .vneu (.npapp _ _) => "vneu npapp" - | .vneu (.ntransp _ _ _ _) => "vneu ntransp" - | .vneu (.nhcomp _ _ _ _) => "vneu nhcomp" - | .vneu (.ncomp _ _ _ _ _) => "vneu ncomp" - | .vneu (.ncompN _ _ _ _ _) => "vneu ncompN" - | .vneu (.nglueIn _ _ _) => "vneu nglueIn" - | .vneu (.nunglue _ _ _) => "vneu nunglue" - | .vneu (.nfst _) => "vneu nfst" - | .vneu (.nsnd _) => "vneu nsnd" - | .vlam _ x _ => s!"vlam {x} ..." - | .vplam _ i _ => s!"vplam {i.name} ..." - | .vpair _ _ => "vpair ..." - | .vTranspFun _ _ _ _ _ => "vTranspFun" - | .vHCompFun _ _ _ _ => "vHCompFun" - | .vCompFun _ _ _ _ _ _ _ => "vCompFun" - | .vTubeApp _ _ => "vTubeApp" - | .vPathTransp _ _ _ _ _ _ _ => "vPathTransp" + | .vneu (.nvar s) => s!"vneu nvar {s}" + | .vneu (.napp _ _) => "vneu napp" + | .vneu (.npapp _ _) => "vneu npapp" + | .vneu (.ntransp _ _ _ _) => "vneu ntransp" + | .vneu (.nhcomp _ _ _ _) => "vneu nhcomp" + | .vneu (.ncomp _ _ _ _ _) => "vneu ncomp" + | .vneu (.ncompN _ _ _ _ _) => "vneu ncompN" + | .vneu (.nglueIn _ _ _) => "vneu nglueIn" + | .vneu (.nunglue _ _ _) => "vneu nunglue" + | .vneu (.nfst _) => "vneu nfst" + | .vneu (.nsnd _) => "vneu nsnd" + | .vneu (.nIndElim _ _ _ _ _) => "vneu nIndElim" + | .vlam _ x _ => s!"vlam {x} ..." + | .vplam _ i _ => s!"vplam {i.name} ..." + | .vpair _ _ => "vpair ..." + | .vTranspFun _ _ _ _ _ => "vTranspFun" + | .vHCompFun _ _ _ _ => "vHCompFun" + | .vCompFun _ _ _ _ _ _ _ => "vCompFun" + | .vTubeApp _ _ => "vTubeApp" + | .vPathTransp _ _ _ _ _ _ _ => "vPathTransp" + | .vctor _ c _ _ => s!"vctor {c} ..." + | .vdimExpr _ => "vdimExpr ..." def ctermSummary : CTerm → String - | .var x => s!"var {x}" - | .lam x _ => s!"lam {x} ..." - | .app _ _ => "app ..." - | .plam i _ => s!"plam {i.name} ..." - | .pair _ _ => "pair ..." - | .fst _ => "fst ..." - | .snd _ => "snd ..." - | _ => "" + | .var x => s!"var {x}" + | .lam x _ => s!"lam {x} ..." + | .app _ _ => "app ..." + | .plam i _ => s!"plam {i.name} ..." + | .pair _ _ => "pair ..." + | .fst _ => "fst ..." + | .snd _ => "snd ..." + | .dimExpr _ => "dimExpr ..." + | .ctor _ c _ _ => s!"ctor {c} ..." + | .indElim _ _ _ _ _ => "indElim ..." + | _ => "" -- ── Individual test definitions ──────────────────────────────────────────── -- Each returns (description, actual, expected) for runSmokeTests to print. diff --git a/CubicalTransport/Readback.lean b/CubicalTransport/Readback.lean index a9254ce..daf261f 100644 --- a/CubicalTransport/Readback.lean +++ b/CubicalTransport/Readback.lean @@ -138,6 +138,10 @@ mutual | _ => .transp i (.path A a b) φ p | .vpair a b => .pair (readback a) (readback b) + -- REL1 inductive-type values. + | .vctor S c params args => + .ctor S c params (args.map readback) + | .vdimExpr r => .dimExpr r /-- Readback a `CNeu` into a `CTerm`. Straightforward structural recursion: each neutral constructor has a syntactic counterpart. @@ -161,6 +165,11 @@ mutual | .nunglue φ f g => .unglue φ (readback f) (readback g) | .nfst n => .fst (readbackNeu n) | .nsnd n => .snd (readbackNeu n) + -- REL1 inductive-eliminator stuck form. + | .nIndElim S params motive branches target => + .indElim S params (readback motive) + (branches.map (fun p => (p.1, readback p.2))) + (readbackNeu target) end -- ── Convenience wrapper ───────────────────────────────────────────────────── diff --git a/CubicalTransport/Subst.lean b/CubicalTransport/Subst.lean index 25d9cdb..e6fe784 100644 --- a/CubicalTransport/Subst.lean +++ b/CubicalTransport/Subst.lean @@ -46,40 +46,64 @@ 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. -/-- Substitute dimension variable i with Bool endpoint b throughout a type. - Path type endpoints are terms, so we delegate to CTerm.substDimBool. -/ -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) +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. -/-- Substitute dimension variable `i` with an arbitrary `DimExpr r` throughout - a type. Generalises `CType.substDim`, which fixes `r` to a Bool endpoint. +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) - 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. -/ -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) + /-- 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 @@ -109,6 +133,9 @@ theorem substDim_glue (i : DimVar) (b : Bool) (φ : FaceFormula) (T : CType) (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) : @@ -135,49 +162,76 @@ theorem substDimExpr_glue (i : DimVar) (r : DimExpr) (φ : FaceFormula) (T : CTy (sec.substDim i r) (ret.substDim i r) (coh.substDim i r) (A.substDimExpr i r) := 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. -/ -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] +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 diff --git a/CubicalTransport/Syntax.lean b/CubicalTransport/Syntax.lean index 0f8ddba..ca42f64 100644 --- a/CubicalTransport/Syntax.lean +++ b/CubicalTransport/Syntax.lean @@ -51,7 +51,19 @@ mutual | glue (φ : FaceFormula) (T : CType) (f fInv sec ret coh : CTerm) (A : CType) : CType -- Glue [φ ↦ (T, e)] A - deriving Repr + /-- Schema-defined inductive type (REL1, INDUCTIVE_TYPES.md). + + `ind S params` is an instance of the schema `S` at the given + type parameters. `params.length = S.numParams` is a typing-side + condition (not enforced syntactically — see `HasType.ind` in + `Typing.lean`). + + The schema `S` carries the constructor list (point + path + ctors) and their boundary partial-element systems. Both plain + inductives (`Nat`, `List A`, `Bool`) and HITs (`S¹`, `‖A‖₋₁`, + suspensions, pushouts) are encoded uniformly via + `CTypeSchema`. -/ + | ind (S : CTypeSchema) (params : List CType) : CType -- ind S params /-- Terms in the cubical calculus. -/ inductive CTerm where @@ -94,9 +106,115 @@ mutual | fst (t : CTerm) : CTerm -- t.1 /-- Σ elimination (second projection). -/ | snd (t : CTerm) : CTerm -- t.2 - deriving Repr + /-- A dimension expression lifted into the term language (REL1). + + Used to fill `.dim`-typed argument positions of schema + constructors (path ctors) and to hand a `DimExpr` to any + future term-level operation that needs one. `DimExpr` is + de Morgan algebra over `DimVar` and 0/1; lifting it lets path + constructors take general dim arguments like `.meet i j`, + `.inv r`, etc., not just bare `.var`-shaped dim names. -/ + | dimExpr (r : DimExpr) : CTerm -- ⟦ r ⟧ + /-- Schema constructor application (REL1, INDUCTIVE_TYPES.md §2.4). + + `ctor S c params args` applies the constructor named `c` of + schema `S` at parameters `params`, with `args.length = + (S.ctors.find c).args.length`. + + Args are positional and follow `CtorSpec.args` order. `.dim`- + typed arg positions carry `CTerm.dimExpr r` (or any other + CTerm that evaluates to a dim) — eval consults the + constructor's boundary system on these to decide whether to + produce the canonical `vctor` or fire a boundary clause. -/ + | ctor (S : CTypeSchema) (ctorName : String) + (params : List CType) (args : List CTerm) : CTerm + /-- Inductive eliminator (REL1, INDUCTIVE_TYPES.md §5). + + `indElim S params motive branches target` eliminates a value + of type `.ind S params`. + + - `motive` is a CTerm of (function-CType) shape `.pi (.ind S + params) .univ` — i.e. `λx : .ind S params. SomeType x`. + - `branches` is one entry per ctor in *schema-declaration + order*. Entry `(c, body)` says: when target reduces to the + ctor `c`, evaluate `body` applied to the ctor's args plus + (for each `.self` arg) the recursive elimination result. + - `target : .ind S params` is the term being eliminated. + + For path constructors, the branch must respect boundary + coherence: at every face in the ctor's boundary system, the + branch agrees with the corresponding eliminated body. This + is a typing-level side condition (see `HasType.indElim`). -/ + | indElim (S : CTypeSchema) (params : List CType) + (motive : CTerm) + (branches : List (String × CTerm)) + (target : CTerm) : CTerm + + /-- Argument shape for a schema constructor (REL1, §2.1). + + Distinguishes ordinary CType-typed args (which may reference + schema parameters via `.param`) from recursive `.self` args + (the inductive being defined) and `.dim` args (used by path + constructors). Boundary clauses inside `CtorSpec` reference + args positionally; `.dim` args are addressed in face formulae + via `DimVar.mk "$d_k"` where `k` is the dim-arg index counted + among `.dim` arg positions only. -/ + inductive CTypeArg where + /-- A non-recursive arg whose type is a closed CType. May + reference schema parameters via embedded `.param i` inside `A` + (parameter substitution happens at instantiation time). -/ + | type (A : CType) : CTypeArg + /-- The `i`th schema parameter (zero-indexed against + `CTypeSchema.numParams`). -/ + | param (i : Nat) : CTypeArg + /-- Recursive reference to the inductive type being defined. -/ + | self : CTypeArg + /-- A dimension binder, used by path constructors. -/ + | dim : CTypeArg + + /-- Constructor specification (REL1, §2.2). + + `name` is unique within the schema. `args` is the positional + arg list. `boundary` is the partial-element system for path + constructors (empty list ≡ point ctor). Each clause `(φ, body)` + says: on the face `φ` of the dim args, the constructor reduces + to `body`. Coherence obligations on the clauses are enforced + at typing time (see `HasType.ctor` in `Typing.lean`). + + Boundary clause bodies are CTerms in a scope where the ctor's + args are bound positionally as `.var "$arg_k"`. Face formulae + reference dim args as `DimVar.mk "$d_k"`. -/ + inductive CtorSpec where + | mk (name : String) (args : List CTypeArg) + (boundary : List (FaceFormula × CTerm)) : CtorSpec + + /-- Schema for an inductive (or higher-inductive) type (REL1, §2.3). + + `name` is the schema's symbolic name (used for diagnostics, not + identity — schemas are compared structurally). `numParams` is + the count of type parameters; `ctors` is the constructor list + in declaration order. Equality is structural (no interning). + + The schema mutually depends on `CType` (via `.type`-typed args + and via `params : List CType` in `CType.ind`) and `CTerm` (via + boundary clauses), so all five types live in this `mutual` + block. -/ + inductive CTypeSchema where + | mk (name : String) (numParams : Nat) + (ctors : List CtorSpec) : CTypeSchema end +-- ── Repr derivations ───────────────────────────────────────────────────────── +-- All five mutual inductives get `Repr` instances post-hoc (Lean's +-- `deriving Repr` clause inside a mutual block of five doesn't always +-- compose; explicit `deriving instance` is the robust form). + +deriving instance Repr for CType +deriving instance Repr for CTerm +deriving instance Repr for CTypeArg +deriving instance Repr for CtorSpec +deriving instance Repr for CTypeSchema + -- ── Dimension substitution ──────────────────────────────────────────────────── -- Substitute dimension variable i with DimExpr r throughout a term. -- @@ -138,6 +256,18 @@ mutual | .pair a b => .pair (a.substDim i r) (b.substDim i r) | .fst t => .fst (t.substDim i r) | .snd t => .snd (t.substDim i r) + -- REL1 inductive-type constructors. Same CType-approximation as + -- transp/comp/glue: schemas and `params : List CType` are *not* + -- recursed into. The schemas are static and the params are + -- supplied externally to any binder we'd be substituting into. + | .dimExpr s => .dimExpr (DimExpr.subst i r s) + | .ctor S c params args => + .ctor S c params (CTerm.substDim.list i r args) + | .indElim S params motive branches target => + .indElim S params + (motive.substDim i r) + (CTerm.substDim.branches i r branches) + (target.substDim i r) /-- Helper: apply `CTerm.substDim i r` to each clause body (and `FaceFormula.substDim` to each face) in a system's clause list. @@ -147,6 +277,21 @@ mutual | [] => [] | (φ, u) :: rest => (φ.substDim i r, u.substDim i r) :: CTerm.substDim.clauses i r rest + + /-- Helper: apply `CTerm.substDim i r` to each element of a CTerm + list (ctor argument lists). Mutually recursive for termination. -/ + def CTerm.substDim.list (i : DimVar) (r : DimExpr) : + List CTerm → List CTerm + | [] => [] + | t :: rest => t.substDim i r :: CTerm.substDim.list i r rest + + /-- Helper: apply `CTerm.substDim i r` to the body of each branch in + an `indElim`. Branch *names* are not affected; only bodies. -/ + def CTerm.substDim.branches (i : DimVar) (r : DimExpr) : + List (String × CTerm) → List (String × CTerm) + | [] => [] + | (n, b) :: rest => + (n, b.substDim i r) :: CTerm.substDim.branches i r rest end -- ── One-step reduction ──────────────────────────────────────────────────────── diff --git a/CubicalTransport/Value.lean b/CubicalTransport/Value.lean index 3f3ac72..f60a827 100644 --- a/CubicalTransport/Value.lean +++ b/CubicalTransport/Value.lean @@ -114,6 +114,26 @@ mutual `vpair` they reduce component-wise, on a `vneu` they produce a stuck `.nfst`/`.nsnd` neutral. -/ | vpair : CVal → CVal → CVal + /-- Schema constructor application — fully-evaluated, canonical + constructor of an inductive (or higher-inductive) type (REL1). + + `vctor S c params args` carries: + - `S : CTypeSchema` — the schema this constructor belongs to. + - `c : String` — the constructor's name. + - `params : List CType` — the type parameters at which the + inductive was instantiated. + - `args : List CVal` — already-evaluated argument values. + + For path constructors, when a `.dim`-typed arg lands on a face + in the constructor's boundary system, eval fires the boundary + clause and never produces a `vctor` — so a `vctor` represents + a value that is *not* on a boundary face. -/ + | vctor : CTypeSchema → String → List CType → List CVal → CVal + /-- Lifted dimension-expression value (REL1). Produced by + `eval env (.dimExpr r)`; consumed by path-constructor face + dispatch and by `vPApp` when its left operand is a `vplam` + whose argument is a `.dimExpr`. -/ + | vdimExpr : DimExpr → CVal /-- Neutral (stuck) terms. Each constructor corresponds to a λ-calculus or cubical elimination whose principal argument is itself @@ -160,6 +180,13 @@ mutual | nfst : CNeu → CNeu /-- A stuck second projection. Produced by `vSnd` on a neutral. -/ | nsnd : CNeu → CNeu + /-- A stuck inductive eliminator (REL1). Produced by `eval`'s + `.indElim` arm when the target evaluates to a neutral (or a + non-`vctor` value). Preserves the schema, parameters, motive, + evaluated branches, and the underlying neutral target so that + later substitution / unstucking can fire the matching branch. -/ + | nIndElim : CTypeSchema → List CType → CVal → + List (String × CVal) → CNeu → CNeu end -- Inhabited instances — needed so `partial def` evaluators can be elaborated