50bb6660d6
Some checks are pending
Lean Action CI / build (push) Waiting to run
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) <noreply@anthropic.com>
95 lines
4.6 KiB
Text
95 lines
4.6 KiB
Text
/-
|
|
Topolei.Cubical.CompLaws
|
|
========================
|
|
Residual step-level axiom for composition: subject reduction (C4).
|
|
|
|
C1 (`comp_full`) and C2 (`comp_empty`), formerly stated here as
|
|
step-level axioms, are now NbE theorems in `Cubical/Readback.lean`
|
|
(`readback_comp_full` / `readback_comp_empty`). The Rust backend's
|
|
discharge obligations for composition reduce to: the eval-level
|
|
axioms in `Eval.lean`, the readback-level axioms in `Readback.lean`,
|
|
and the C4 residual below.
|
|
|
|
Note on CCHM C3 (`transp = comp_{[φ↦t₀]} t₀`):
|
|
CCHM expresses transport as a specialised composition. That
|
|
specialisation is only *typed* when the system body coincides with
|
|
the base (u = t₀) and the compatibility `t₀[i:=0] = t₀` holds —
|
|
i.e. `L.binder` is absent from `t₀`. Stating it would duplicate
|
|
the constant-line transport identity (`readback_transp_const_id`).
|
|
The real CCHM reduction (`transp = hcomp + fill`) lives at the
|
|
eval level; see `vCompFun` / `vApp_vCompFun` in `Eval.lean`.
|
|
|
|
Why C4 stays step-level: same reason as T3 — needs a typing-
|
|
preservation lemma on `eval`/`readback` (Stream B #2a).
|
|
-/
|
|
|
|
import CubicalTransport.System
|
|
import CubicalTransport.TransportLaws
|
|
import CubicalTransport.ValueTyping
|
|
|
|
-- ── Subject reduction for composition ────────────────────────────────────────
|
|
|
|
/-- **C4 (composition subject reduction)** — stepping a well-typed
|
|
composition preserves the output type.
|
|
|
|
**Now a theorem, not an axiom.** Stage 2.3 consolidation: follows
|
|
from `HasType.comp` and `CTerm.step_preserves_type` (ValueTyping.lean).
|
|
Parallel to `transp_step_preserves` (T3).
|
|
|
|
The `HasType.comp` constructor requires a compatibility side-condition
|
|
on the system body (`u[i:=0] = t₀` wherever `φ ∩ (i=0)` is inhabited).
|
|
Callers that cannot produce this side-condition should fall through
|
|
to a per-callsite argument rather than using this theorem. -/
|
|
theorem comp_step_preserves (Γ : Ctx) (L : DimLine) (φ : FaceFormula)
|
|
(u t₀ : CTerm)
|
|
(ht : HasType Γ t₀ L.at0)
|
|
(hu : HasType Γ u L.at1)
|
|
(hc : ∀ env : DimVar → Bool,
|
|
φ.eval env = true → env L.binder = false →
|
|
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
|