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>
251 lines
11 KiB
Text
251 lines
11 KiB
Text
/-
|
||
Topolei.Cubical.Typing
|
||
======================
|
||
The typing judgment Γ ⊢ t : A for the cubical term language.
|
||
|
||
Rules:
|
||
var : membership in context
|
||
lam : introduce Π
|
||
app : eliminate Π
|
||
plam : introduce Path — Γ, i:I ⊢ t : A ⟹ Γ ⊢ ⟨i⟩t : Path A t[i:=0] t[i:=1]
|
||
papp : eliminate Path — t : Path A a b ⟹ t @ r : A
|
||
|
||
Face connection:
|
||
The face lattice tells us *when* a boundary holds (eq0 i / eq1 i).
|
||
`FaceFormula.eq0_iff_env_false` / `eq1_iff_env_true` (below) classify
|
||
which environments put us on the corresponding endpoint. The
|
||
boundary reduction itself is now an NbE theorem in `Readback.lean`
|
||
(`readback_papp_plam`); the previous step-level path β `PathWitness`
|
||
encoding has been removed alongside its underlying axiom.
|
||
|
||
Note: Π types are non-dependent here (B is a CType, not CTerm → CType).
|
||
Dependent Π is deferred until we have a term evaluator.
|
||
-/
|
||
|
||
import CubicalTransport.DimLine
|
||
|
||
-- ── Context ───────────────────────────────────────────────────────────────────
|
||
|
||
/-- Typing context: ordered list of term-variable bindings. -/
|
||
abbrev Ctx := List (String × CType)
|
||
|
||
-- ── Typing judgment ───────────────────────────────────────────────────────────
|
||
|
||
/-- The typing judgment Γ ⊢ t : A. -/
|
||
inductive HasType : Ctx → CTerm → CType → Prop where
|
||
| var : (x, A) ∈ Γ →
|
||
HasType Γ (.var x) A
|
||
|
||
| lam : HasType ((x, A) :: Γ) t B →
|
||
HasType Γ (.lam x t) (.pi A B)
|
||
|
||
| app : HasType Γ f (.pi A B) →
|
||
HasType Γ a A →
|
||
HasType Γ (.app f a) B
|
||
|
||
/-- Path introduction: ⟨i⟩t has type Path A t[i:=0] t[i:=1].
|
||
The boundaries are computed directly from substDim. -/
|
||
| plam : HasType Γ t A →
|
||
HasType Γ (.plam i t) (.path A (t.substDim i .zero) (t.substDim i .one))
|
||
|
||
/-- Path elimination: applying a path to any DimExpr gives the fibration type. -/
|
||
| papp : HasType Γ t (.path A a b) →
|
||
HasType Γ (.papp t r) A
|
||
|
||
/-- Transport: if t has the type at the 0-end of line L,
|
||
then transpⁱ (λi.A) φ t has the type at the 1-end.
|
||
L packages the binder and body; we unpack to CTerm.transp's raw form. -/
|
||
| transp : (L : DimLine) →
|
||
HasType Γ t L.at0 →
|
||
HasType Γ (.transp L.binder L.body φ t) L.at1
|
||
|
||
/-- Composition: compⁱ (λi.A) φ u t has type L.at1, given:
|
||
· t : L.at0 (base term)
|
||
· u : L.at1 (system body typed at output end)
|
||
· on (φ ∩ i=0), u[i:=0] = t (compatibility side-condition)
|
||
|
||
The compat condition has the universally-quantified shape
|
||
∀ env, φ.eval env = true → env i = false → u[i:=0] = t
|
||
which is logically equivalent to
|
||
(∃ env, φ ∧ i=0) → u[i:=0] = t
|
||
— i.e. *if the face (φ ∩ i=0) is actually inhabited, the equation holds*.
|
||
This makes `.bot`-faced systems (unsatisfiable) vacuously compatible while
|
||
still forcing the equation wherever the face can actually be met.
|
||
|
||
The face formula φ and system body u are stored raw (no System wrapper)
|
||
to avoid a circular import; System.lean wraps these for ergonomics. -/
|
||
| comp : (L : DimLine) →
|
||
HasType Γ t L.at0 →
|
||
HasType Γ u L.at1 →
|
||
(∀ env : DimVar → Bool,
|
||
φ.eval env = true → env L.binder = false →
|
||
CTerm.substDimBool L.binder false u = t) →
|
||
HasType Γ (.comp L.binder L.body φ u t) L.at1
|
||
|
||
/-- Σ introduction: pairing. Non-dependent form — `B` does not depend
|
||
on the first component's value. -/
|
||
| pair : HasType Γ a A →
|
||
HasType Γ b B →
|
||
HasType Γ (.pair a b) (.sigma A B)
|
||
|
||
/-- Σ elimination (first projection). -/
|
||
| fst : HasType Γ t (.sigma A B) →
|
||
HasType Γ (.fst t) A
|
||
|
||
/-- Σ elimination (second projection). -/
|
||
| 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 Γ₂.
|
||
We take `Γ` as a free variable and carry `Γ = Γ₁ ++ Γ₂` as a hypothesis
|
||
so that `induction h` works (the index must be a variable). -/
|
||
private theorem HasType.weaken_core
|
||
(x : String) (B : CType) (Γ₂ : Ctx)
|
||
{Γ : Ctx} {t : CTerm} {A : CType}
|
||
(h : HasType Γ t A) :
|
||
∀ (Γ₁ : Ctx), Γ = Γ₁ ++ Γ₂ → HasType (Γ₁ ++ (x, B) :: Γ₂) t A := by
|
||
induction h with
|
||
| var mem =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
apply HasType.var
|
||
rw [List.mem_append] at mem ⊢
|
||
rcases mem with h | h
|
||
· exact Or.inl h
|
||
· exact Or.inr (List.mem_cons.mpr (Or.inr h))
|
||
| lam ht ih =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.lam (ih ((_, _) :: Γ₁) rfl)
|
||
| app hf ha ihf iha =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.app (ihf Γ₁ rfl) (iha Γ₁ rfl)
|
||
| plam ht ih =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.plam (ih Γ₁ rfl)
|
||
| papp ht ih =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.papp (ih Γ₁ rfl)
|
||
| transp L ht ih =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.transp L (ih Γ₁ rfl)
|
||
| comp L ht hu hc iht ihu =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.comp L (iht Γ₁ rfl) (ihu Γ₁ rfl) hc
|
||
| pair ha hb iha ihb =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.pair (iha Γ₁ rfl) (ihb Γ₁ rfl)
|
||
| fst ht ih =>
|
||
intro Γ₁ hΓ; subst hΓ
|
||
exact HasType.fst (ih Γ₁ rfl)
|
||
| 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 :=
|
||
HasType.weaken_core x B Γ h [] rfl
|
||
|
||
-- ── Face lattice connection ───────────────────────────────────────────────────
|
||
-- These lemmas tie the Bool-valued face semantics to the dimensional endpoints.
|
||
|
||
namespace FaceFormula
|
||
|
||
/-- The face (i=0) holds precisely when env i = false. -/
|
||
theorem eq0_iff_env_false (i : DimVar) (env : DimVar → Bool) :
|
||
(eq0 i).eval env = true ↔ env i = false := by
|
||
simp [eval]
|
||
|
||
/-- The face (i=1) holds precisely when env i = true. -/
|
||
theorem eq1_iff_env_true (i : DimVar) (env : DimVar → Bool) :
|
||
(eq1 i).eval env = true ↔ env i = true := by
|
||
simp [eval]
|
||
|
||
end FaceFormula
|
||
|
||
-- ── Typing inversion ─────────────────────────────────────────────────────────
|
||
|
||
/-- Inversion for plam: if ⟨i⟩t : Path A a b, then t : A and
|
||
the boundaries are exactly the substDim images. -/
|
||
theorem HasType.plam_inv
|
||
(Γ : Ctx) (i : DimVar) (t : CTerm) (A : CType) (a b : CTerm)
|
||
(h : HasType Γ (.plam i t) (.path A a b)) :
|
||
HasType Γ t A ∧
|
||
a = t.substDim i .zero ∧
|
||
b = t.substDim i .one := by
|
||
cases h with
|
||
| plam ht => exact ⟨ht, rfl, rfl⟩
|
||
|
||
/-- Inversion for papp: if t @ r : A, then t : Path A a b for some a b. -/
|
||
theorem HasType.papp_inv
|
||
(Γ : Ctx) (t : CTerm) (r : DimExpr) (A : CType)
|
||
(h : HasType Γ (.papp t r) A) :
|
||
∃ a b, HasType Γ t (.path A a b) := by
|
||
cases h with
|
||
| papp ht => exact ⟨_, _, ht⟩
|
||
|
||
/-- Inversion for comp: reading off all components of a composition judgment.
|
||
We return an existential DimLine to avoid the naming clash between the
|
||
outer parameter and the constructor's internal binder. -/
|
||
theorem HasType.comp_inv
|
||
(Γ : Ctx) (i : DimVar) (bodyA : CType) (φ : FaceFormula) (u t : CTerm) (A : CType)
|
||
(h : HasType Γ (.comp i bodyA φ u t) A) :
|
||
∃ L : DimLine, L.binder = i ∧ L.body = bodyA ∧
|
||
A = L.at1 ∧
|
||
HasType Γ t L.at0 ∧
|
||
HasType Γ u L.at1 ∧
|
||
(∀ env : DimVar → Bool,
|
||
φ.eval env = true → env L.binder = false →
|
||
CTerm.substDimBool L.binder false u = t) := by
|
||
cases h with
|
||
| comp L ht hu hc => exact ⟨L, rfl, rfl, rfl, ht, hu, hc⟩
|
||
|
||
/-- Inversion for transp: the output type is exactly L.at1. -/
|
||
theorem HasType.transp_inv
|
||
(Γ : Ctx) (i : DimVar) (bodyA : CType) (φ : FaceFormula) (t : CTerm) (A : CType)
|
||
(h : HasType Γ (.transp i bodyA φ t) A) :
|
||
∃ L : DimLine, L.binder = i ∧ L.body = bodyA ∧
|
||
A = L.at1 ∧ HasType Γ t L.at0 := by
|
||
cases h with
|
||
| transp L ht => exact ⟨L, rfl, rfl, rfl, ht⟩
|