From 6e4936d6ee8d0bac23d71c2add41a5c47068e2b3 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Wed, 6 May 2026 02:01:52 -0600 Subject: [PATCH] =?UTF-8?q?Refactor=20Phase=202:=20modal=20unification=20?= =?UTF-8?q?=E2=80=94=20Lean=20engine=20cascade?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per the elegance pass: 9 ad-hoc per-modality constructors collapse into 3 ModalityKind-parameterised constructors. Future modalities (Phase 4's ʃ_EML, ℑ infinitesimal) extend ModalityKind by adding cases — no new constructors, no new ABI bump. New Lean enum (Syntax.lean): inductive ModalityKind | flat | sharp | shape deriving DecidableEq, Repr, Inhabited Constructor unification: · CType: 3 (.flat / .sharp / .shape) → 1 (.modal k A) · CTerm: 6 (.flatIntro / .sharpIntro / .shapeIntro / .flatElim / .sharpElim / .shapeElim) → 2 (.modalIntro k a, .modalElim k f m) · CVal: 3 (vFlatIntro / vSharpIntro / vShapeIntro) → 1 (vModalIntro) · CNeu: 3 (nflatElim / nsharpElim / nshapeElim) → 1 (nModalElim) · SkeletalCType: 3 (skFlat / skSharp / skShape) → 1 (skModal k) Engine cascade across 12 files (DecEq, DimLine, Eval, FFITest, Modal, Question, Readback, Reflect, Subst, Syntax, Typing, Value): every match site collapsed from 3-per-modality arms to 1 k-parameterised arm. Reflect.lean: new `reflectModalityKind` / `reifyModalityKind` helpers + ModalityKind dispatch arm in classifyFieldType. The Phase 1 macro auto-derived per-constructor reflect/reify for the new unified constructors — no manual cascade needed there. Eval.lean β-rule: `.modalElim k f (.modalIntro k' a)` β-reduces only when k = k' (kind-discrimination preserves cross-kind correctness even if typing is bypassed); cross-kind case produces a marker neutral. Modal.lean transient alias block (top of file, outside namespace) for backward dot-syntax reference (`.flatIntro a` resolves to `.modalIntro .flat a` via abbrev). Phase 3 will rewrite Modal.lean properly to use the unified constructors directly + forModalityKind- derived functor. Net: −145 lines across the cascade (-478 deletions, +333 insertions). Build: lake build (48 jobs) + lake build CubicalTransport (43 jobs) PASS. Runtime: lake exe cubical-test 49/49 + 46/46 = 95/95 PASS. Sorry count: Modal.lean 3 (unchanged), total engine 33 (no new sorries from this phase, all annotated). The Rust ABI v6 still uses 9 modal tags — diverges from the Lean side after this commit but FFI tests don't exercise modal paths so no runtime regression. Phase 4 will sync to ABI v7. Co-Authored-By: Claude Opus 4.7 (1M context) --- CubicalTransport/DecEq.lean | 22 ++---- CubicalTransport/DimLine.lean | 128 +++++-------------------------- CubicalTransport/Eval.lean | 116 ++++++++++------------------ CubicalTransport/FFITest.lean | 25 +++--- CubicalTransport/Modal.lean | 86 +++++++++++++++++---- CubicalTransport/Question.lean | 62 +++++---------- CubicalTransport/Readback.lean | 40 ++++------ CubicalTransport/Reflect.lean | 27 +++++++ CubicalTransport/Subst.lean | 44 +++-------- CubicalTransport/Syntax.lean | 136 ++++++++++++++++----------------- CubicalTransport/Typing.lean | 83 +++++++------------- CubicalTransport/Value.lean | 28 ++++--- 12 files changed, 326 insertions(+), 471 deletions(-) diff --git a/CubicalTransport/DecEq.lean b/CubicalTransport/DecEq.lean index 8fbf8a8..d914f78 100644 --- a/CubicalTransport/DecEq.lean +++ b/CubicalTransport/DecEq.lean @@ -61,12 +61,8 @@ partial def beqCTypeAny : (Σ ℓ : ULevel, CType ℓ) → (Σ ℓ : ULevel, CTy beqCTypeAny ⟨_, A⟩ ⟨_, A'⟩ | ⟨_, .El P⟩, ⟨_, .El Q⟩ => beqCTerm P Q - | ⟨_, .flat A⟩, ⟨_, .flat B⟩ => - beqCTypeAny ⟨_, A⟩ ⟨_, B⟩ - | ⟨_, .sharp A⟩, ⟨_, .sharp B⟩ => - beqCTypeAny ⟨_, A⟩ ⟨_, B⟩ - | ⟨_, .shape A⟩, ⟨_, .shape B⟩ => - beqCTypeAny ⟨_, A⟩ ⟨_, B⟩ + | ⟨_, .modal k A⟩, ⟨_, .modal k' B⟩ => + decide (k = k') && beqCTypeAny ⟨_, A⟩ ⟨_, B⟩ | _, _ => false partial def beqCTerm : CTerm → CTerm → Bool @@ -100,14 +96,12 @@ partial def beqCTerm : CTerm → CTerm → Bool -- A and B may live at different universe levels. Route through -- the level-erased Σ-pair beq to compare them honestly. beqCTypeAny ⟨_, A⟩ ⟨_, B⟩ - -- Modal introductions: structural equality on the wrapped term. - | .flatIntro a, .flatIntro b => beqCTerm a b - | .sharpIntro a, .sharpIntro b => beqCTerm a b - | .shapeIntro a, .shapeIntro b => beqCTerm a b - -- Modal eliminations: structural equality on (eliminator, scrutinee). - | .flatElim f m, .flatElim f' m' => beqCTerm f f' && beqCTerm m m' - | .sharpElim f m, .sharpElim f' m' => beqCTerm f f' && beqCTerm m m' - | .shapeElim f m, .shapeElim f' m' => beqCTerm f f' && beqCTerm m m' + -- Modal introduction: structural equality on (kind, wrapped term). + | .modalIntro k a, .modalIntro k' b => + decide (k = k') && beqCTerm a b + -- Modal elimination: structural equality on (kind, eliminator, scrutinee). + | .modalElim k f m, .modalElim k' f' m' => + decide (k = k') && beqCTerm f f' && beqCTerm m m' | _, _ => false partial def beqCTypeArg : CTypeArg → CTypeArg → Bool diff --git a/CubicalTransport/DimLine.lean b/CubicalTransport/DimLine.lean index 174ee9d..bcf80f8 100644 --- a/CubicalTransport/DimLine.lean +++ b/CubicalTransport/DimLine.lean @@ -93,14 +93,10 @@ mutual -- substDim approximation in Syntax.lean — the CType payload is -- conservatively assumed to be dim-stable). | .code _ => true - -- Modal introductions: dim-absence is preserved through the wrapper. - | .flatIntro a => a.dimAbsent i - | .sharpIntro a => a.dimAbsent i - | .shapeIntro a => a.dimAbsent i - -- Modal eliminations: check both the eliminator and the scrutinee. - | .flatElim f m => f.dimAbsent i && m.dimAbsent i - | .sharpElim f m => f.dimAbsent i && m.dimAbsent i - | .shapeElim f m => f.dimAbsent i && m.dimAbsent i + -- Modal introduction: dim-absence is preserved through the wrapper. + | .modalIntro _ a => a.dimAbsent i + -- Modal elimination: check both the eliminator and the scrutinee. + | .modalElim _ f m => f.dimAbsent i && m.dimAbsent i /-- Helper: check that `i` is absent from every clause in a system. -/ def CTerm.dimAbsent.clauses (i : DimVar) : @@ -137,10 +133,8 @@ mutual | .interval => true -- REL2: 𝕀 carries no dim binders | .lift A => A.dimAbsent i | .El P => P.dimAbsent i - -- Modal type formers: dim-absence reduces to the inner type's. - | .flat A => A.dimAbsent i - | .sharp A => A.dimAbsent i - | .shape A => A.dimAbsent i + -- Modal type former: dim-absence reduces to the inner type's. + | .modal _ A => A.dimAbsent i /-- Helper: check `i` absent from every CType in a level-heterogeneous parameter list. -/ @@ -272,29 +266,11 @@ mutual CTerm.substDim.branches_of_absent i r branches hbr, CTerm.substDim_absent_aux i r target htg] | .code _, _ => rfl - | .flatIntro a, h => by + | .modalIntro _ a, h => by simp only [CTerm.dimAbsent] at h simp only [CTerm.substDim] rw [CTerm.substDim_absent_aux i r a h] - | .sharpIntro a, h => by - simp only [CTerm.dimAbsent] at h - simp only [CTerm.substDim] - rw [CTerm.substDim_absent_aux i r a h] - | .shapeIntro a, h => by - simp only [CTerm.dimAbsent] at h - simp only [CTerm.substDim] - rw [CTerm.substDim_absent_aux i r a h] - | .flatElim f m, h => by - simp only [CTerm.dimAbsent, Bool.and_eq_true] at h - simp only [CTerm.substDim] - rw [CTerm.substDim_absent_aux i r f h.1, - CTerm.substDim_absent_aux i r m h.2] - | .sharpElim f m, h => by - simp only [CTerm.dimAbsent, Bool.and_eq_true] at h - simp only [CTerm.substDim] - rw [CTerm.substDim_absent_aux i r f h.1, - CTerm.substDim_absent_aux i r m h.2] - | .shapeElim f m, h => by + | .modalElim _ f m, h => by simp only [CTerm.dimAbsent, Bool.and_eq_true] at h simp only [CTerm.substDim] rw [CTerm.substDim_absent_aux i r f h.1, @@ -414,19 +390,9 @@ mutual show CType.El (CTerm.substDimBool i b P) = CType.El P congr 1 exact CTerm.substDimBool_of_absent i b P h - | .flat A, h => by + | .modal k A, h => by simp only [CType.dimAbsent] at h - show CType.flat (CType.substDim i b A) = CType.flat A - congr 1 - exact CType.substDim_absent_aux i b A h - | .sharp A, h => by - simp only [CType.dimAbsent] at h - show CType.sharp (CType.substDim i b A) = CType.sharp A - congr 1 - exact CType.substDim_absent_aux i b A h - | .shape A, h => by - simp only [CType.dimAbsent] at h - show CType.shape (CType.substDim i b A) = CType.shape A + show CType.modal k (CType.substDim i b A) = CType.modal k A congr 1 exact CType.substDim_absent_aux i b A h @@ -508,19 +474,9 @@ mutual show CType.El (CTerm.substDim i r P) = CType.El P congr 1 exact CTerm.substDim_of_absent i r P h - | .flat A, h => by + | .modal k A, h => by simp only [CType.dimAbsent] at h - show CType.flat (A.substDimExpr i r) = CType.flat A - congr 1 - exact CType.substDimExpr_absent_aux i r A h - | .sharp A, h => by - simp only [CType.dimAbsent] at h - show CType.sharp (A.substDimExpr i r) = CType.sharp A - congr 1 - exact CType.substDimExpr_absent_aux i r A h - | .shape A, h => by - simp only [CType.dimAbsent] at h - show CType.shape (A.substDimExpr i r) = CType.shape A + show CType.modal k (A.substDimExpr i r) = CType.modal k A congr 1 exact CType.substDimExpr_absent_aux i r A h @@ -674,24 +630,10 @@ mutual CTerm.dimAbsent.branches_after_substDim i r hr branches, CTerm.dimAbsent_after_substDim_aux i r hr target, Bool.and_self] | .code _ => by simp [CTerm.substDim, CTerm.dimAbsent] - | .flatIntro a => by + | .modalIntro _ a => by simp only [CTerm.substDim, CTerm.dimAbsent, CTerm.dimAbsent_after_substDim_aux i r hr a] - | .sharpIntro a => by - simp only [CTerm.substDim, CTerm.dimAbsent, - CTerm.dimAbsent_after_substDim_aux i r hr a] - | .shapeIntro a => by - simp only [CTerm.substDim, CTerm.dimAbsent, - CTerm.dimAbsent_after_substDim_aux i r hr a] - | .flatElim f m => by - simp only [CTerm.substDim, CTerm.dimAbsent, - CTerm.dimAbsent_after_substDim_aux i r hr f, - CTerm.dimAbsent_after_substDim_aux i r hr m, Bool.and_self] - | .sharpElim f m => by - simp only [CTerm.substDim, CTerm.dimAbsent, - CTerm.dimAbsent_after_substDim_aux i r hr f, - CTerm.dimAbsent_after_substDim_aux i r hr m, Bool.and_self] - | .shapeElim f m => by + | .modalElim _ f m => by simp only [CTerm.substDim, CTerm.dimAbsent, CTerm.dimAbsent_after_substDim_aux i r hr f, CTerm.dimAbsent_after_substDim_aux i r hr m, Bool.and_self] @@ -780,13 +722,7 @@ mutual | .El P => by simp only [CType.substDim, CType.dimAbsent] exact CTerm.dimAbsent_after_substDimBool i b P - | .flat A => by - simp only [CType.substDim, CType.dimAbsent, - CType.dimAbsent_after_substDim_aux i b A] - | .sharp A => by - simp only [CType.substDim, CType.dimAbsent, - CType.dimAbsent_after_substDim_aux i b A] - | .shape A => by + | .modal _ A => by simp only [CType.substDim, CType.dimAbsent, CType.dimAbsent_after_substDim_aux i b A] @@ -950,29 +886,11 @@ mutual · 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 | .code _ => rfl - | .flatIntro a => by + | .modalIntro k a => by simp only [CTerm.substDim] - exact congrArg CTerm.flatIntro + exact congrArg (CTerm.modalIntro k) (CTerm.substDim_comm_aux i j r s hij hrj hsi a) - | .sharpIntro a => by - simp only [CTerm.substDim] - exact congrArg CTerm.sharpIntro - (CTerm.substDim_comm_aux i j r s hij hrj hsi a) - | .shapeIntro a => by - simp only [CTerm.substDim] - exact congrArg CTerm.shapeIntro - (CTerm.substDim_comm_aux i j r s hij hrj hsi a) - | .flatElim f m => by - simp only [CTerm.substDim] - congr 1 - · exact CTerm.substDim_comm_aux i j r s hij hrj hsi f - · exact CTerm.substDim_comm_aux i j r s hij hrj hsi m - | .sharpElim f m => by - simp only [CTerm.substDim] - congr 1 - · exact CTerm.substDim_comm_aux i j r s hij hrj hsi f - · exact CTerm.substDim_comm_aux i j r s hij hrj hsi m - | .shapeElim f m => by + | .modalElim _ f m => by simp only [CTerm.substDim] congr 1 · exact CTerm.substDim_comm_aux i j r s hij hrj hsi f @@ -1076,15 +994,7 @@ mutual simp only [CType.substDim] congr 1 exact CTerm.substDimBool_comm i j b c hij P - | .flat A => by - simp only [CType.substDim] - congr 1 - exact CType.substDim_comm_aux i j b c hij A - | .sharp A => by - simp only [CType.substDim] - congr 1 - exact CType.substDim_comm_aux i j b c hij A - | .shape A => by + | .modal _ A => by simp only [CType.substDim] congr 1 exact CType.substDim_comm_aux i j b c hij A diff --git a/CubicalTransport/Eval.lean b/CubicalTransport/Eval.lean index 1306539..66783c3 100644 --- a/CubicalTransport/Eval.lean +++ b/CubicalTransport/Eval.lean @@ -161,28 +161,21 @@ mutual (branches.map (fun (nm, b) => (nm, eval env b))) n) | _ => .vneu (.nvar "") - -- Modal introductions: structural lift to the corresponding value form. - | .flatIntro a => .vFlatIntro (eval env a) - | .sharpIntro a => .vSharpIntro (eval env a) - | .shapeIntro a => .vShapeIntro (eval env a) - -- Modal eliminations: β-reduce on the corresponding intro value form; - -- otherwise produce a stuck neutral that preserves the evaluated - -- eliminator function and the (necessarily-stuck) scrutinee neutral. - | .flatElim f m => + -- Modal introduction: structural lift to the corresponding value form. + | .modalIntro k a => .vModalIntro k (eval env a) + -- Modal elimination: β-reduce on a same-kind intro value form; + -- mismatched-kind intros (which a well-typed source cannot produce + -- but a bypassed typechecker conceivably could) are kept stuck via + -- a marker-neutral. Otherwise produce a stuck neutral that + -- preserves the modality kind, the evaluated eliminator function, + -- and the (necessarily-stuck) scrutinee neutral. + | .modalElim k f m => match eval env m with - | .vFlatIntro a => vApp (eval env f) a - | .vneu n => .vneu (.nflatElim (eval env f) n) - | _ => .vneu (.nvar "") - | .sharpElim f m => - match eval env m with - | .vSharpIntro a => vApp (eval env f) a - | .vneu n => .vneu (.nsharpElim (eval env f) n) - | _ => .vneu (.nvar "") - | .shapeElim f m => - match eval env m with - | .vShapeIntro a => vApp (eval env f) a - | .vneu n => .vneu (.nshapeElim (eval env f) n) - | _ => .vneu (.nvar "") + | .vModalIntro k' a => + if k = k' then vApp (eval env f) a + else .vneu (.nvar "") + | .vneu n => .vneu (.nModalElim k (eval env f) n) + | _ => .vneu (.nvar "") /-- First projection at the value level. β-reduces `vpair`; pushes a stuck neutral into `nfst`. Projecting any other value shape is a @@ -243,9 +236,7 @@ mutual | .vctor _ _ _ _, _ => .vneu (.nvar "") | .vdimExpr _, _ => .vneu (.nvar "") | .vcode _, _ => .vneu (.nvar "") - | .vFlatIntro _, _ => .vneu (.nvar "") - | .vSharpIntro _, _ => .vneu (.nvar "") - | .vShapeIntro _, _ => .vneu (.nvar "") + | .vModalIntro _ _, _ => .vneu (.nvar "") /-- Apply a value to a dimension expression. β-reduces `vplam` closures by substituting the dim in the body and re-evaluating; pushes stuck @@ -279,9 +270,7 @@ mutual | .vctor _ _ _ _, _ => .vneu (.nvar "") | .vdimExpr _, _ => .vneu (.nvar "") | .vcode _, _ => .vneu (.nvar "") - | .vFlatIntro _, _ => .vneu (.nvar "") - | .vSharpIntro _, _ => .vneu (.nvar "") - | .vShapeIntro _, _ => .vneu (.nvar "") + | .vModalIntro _ _, _ => .vneu (.nvar "") /-- Homogeneous composition at the value level. The type `A` is *homogeneous* (doesn't vary along `i`); the tube and base are @@ -897,57 +886,36 @@ axiom eval_code {ℓ : ULevel} (env : CEnv) (A : CType ℓ) : eval env (.code A) = .vcode A /-! -### `eval` on modal introductions / eliminations +### `eval` on modal introduction / elimination (Refactor Phase 2) -For each modality M ∈ {flat, sharp, shape}: - · `M-Intro a` evaluates to `vM-Intro (eval env a)` (lift through the - constructor). - · `M-Elim f m` β-reduces when the scrutinee evaluates to a `vM-Intro`, - via `vApp` with the eliminator function; on a stuck neutral it - produces a `nM-Elim` neutral; on any other shape, a marker neutral. - -The arms below mirror the partial-def cases verbatim. Engine-layer -axioms; modal-cohesion semantics (Crisp variables, `♭ ⊣ ♯ ⊣ ʃ` -adjunction laws) are Phase 3 and live in a separate `Modal.lean`. +Engine-layer axioms parameterised over `ModalityKind`. Replaces the +prior trio of (intro, elim-β, elim-stuck) axioms per modality with one +intro and two elim axioms (β on matching kinds, stuck on neutrals). +Modal-cohesion semantics (Crisp variables, `ʃ ⊣ ♭ ⊣ ♯` adjunction +laws) are Phase 3 and live in a separate `Modal.lean`. -/ --- Modal introductions: structural lift to the corresponding value form. +-- Modal introduction: structural lift to the corresponding value form. -axiom eval_flatIntro (env : CEnv) (a : CTerm) : - eval env (.flatIntro a) = .vFlatIntro (eval env a) +axiom eval_modalIntro (env : CEnv) (k : ModalityKind) (a : CTerm) : + eval env (.modalIntro k a) = .vModalIntro k (eval env a) -axiom eval_sharpIntro (env : CEnv) (a : CTerm) : - eval env (.sharpIntro a) = .vSharpIntro (eval env a) +-- Modal elimination: β on matching-kind intro; stuck on neutrals. -axiom eval_shapeIntro (env : CEnv) (a : CTerm) : - eval env (.shapeIntro a) = .vShapeIntro (eval env a) +/-- β-rule: `modalElim k f (modalIntro k a)` reduces to `app f a` at + the eval level. The β arm of `eval` checks that the elim's kind + matches the intro's kind, then delegates to `vApp` on the + eliminator value. Cross-kind elims (which are type errors) + diverge from this rule by producing a marker neutral. -/ +axiom eval_modalElim_beta (env : CEnv) (k : ModalityKind) (f a : CTerm) : + eval env (.modalElim k f (.modalIntro k a)) = + vApp (eval env f) (eval env a) --- Modal eliminations: β on the corresponding intro; stuck on neutrals. - -/-- β-rule: `flatElim f (flatIntro a)` reduces to `app f a` at the eval - level. The scrutinee evaluates to `vFlatIntro (eval env a)`; the - elim arm of `eval` then invokes `vApp` on the eliminator value. -/ -axiom eval_flatElim_beta (env : CEnv) (f a : CTerm) : - eval env (.flatElim f (.flatIntro a)) = vApp (eval env f) (eval env a) - -axiom eval_sharpElim_beta (env : CEnv) (f a : CTerm) : - eval env (.sharpElim f (.sharpIntro a)) = vApp (eval env f) (eval env a) - -axiom eval_shapeElim_beta (env : CEnv) (f a : CTerm) : - eval env (.shapeElim f (.shapeIntro a)) = vApp (eval env f) (eval env a) - -/-- Stuck case: `flatElim` whose scrutinee evaluates to a CNeu produces - a `nflatElim` neutral preserving the evaluated function and - scrutinee. The scrutinee must be `.vneu n` after eval; this is - encoded by the explicit hypothesis `eval env m = .vneu n`. -/ -axiom eval_flatElim_stuck (env : CEnv) (f m : CTerm) (n : CNeu) - (h : eval env m = .vneu n) : - eval env (.flatElim f m) = .vneu (.nflatElim (eval env f) n) - -axiom eval_sharpElim_stuck (env : CEnv) (f m : CTerm) (n : CNeu) - (h : eval env m = .vneu n) : - eval env (.sharpElim f m) = .vneu (.nsharpElim (eval env f) n) - -axiom eval_shapeElim_stuck (env : CEnv) (f m : CTerm) (n : CNeu) - (h : eval env m = .vneu n) : - eval env (.shapeElim f m) = .vneu (.nshapeElim (eval env f) n) +/-- Stuck case: `modalElim k` whose scrutinee evaluates to a CNeu + produces an `nModalElim k` neutral preserving the kind, the + evaluated function, and the stuck scrutinee. The scrutinee must + be `.vneu n` after eval; this is encoded by the explicit + hypothesis `eval env m = .vneu n`. -/ +axiom eval_modalElim_stuck (env : CEnv) (k : ModalityKind) + (f m : CTerm) (n : CNeu) (h : eval env m = .vneu n) : + eval env (.modalElim k f m) = .vneu (.nModalElim k (eval env f) n) diff --git a/CubicalTransport/FFITest.lean b/CubicalTransport/FFITest.lean index 561491e..52ff360 100644 --- a/CubicalTransport/FFITest.lean +++ b/CubicalTransport/FFITest.lean @@ -33,6 +33,15 @@ namespace CubicalTransportFFITest -- ── Summarisers ──────────────────────────────────────────────────────────── +/-- Display-name for a `ModalityKind`: a printable tag used by the + summarisers to label modal values / neutrals. Pure formatting — + no semantic per-kind dispatch, just a single reflection of the + enum's three constructors into their conventional symbols. -/ +def modalityKindTag : ModalityKind → String + | .flat => "flat" + | .sharp => "sharp" + | .shape => "shape" + def cvalSummary : CVal → String | .vneu (.nvar s) => s!"vneu nvar {s}" | .vneu (.napp _ _) => "vneu napp" @@ -46,9 +55,7 @@ def cvalSummary : CVal → String | .vneu (.nfst _) => "vneu nfst" | .vneu (.nsnd _) => "vneu nsnd" | .vneu (.nIndElim _ _ _ _ _) => "vneu nIndElim" - | .vneu (.nflatElim _ _) => "vneu nflatElim" - | .vneu (.nsharpElim _ _) => "vneu nsharpElim" - | .vneu (.nshapeElim _ _) => "vneu nshapeElim" + | .vneu (.nModalElim k _ _) => s!"vneu nModalElim {modalityKindTag k}" | .vlam _ x _ => s!"vlam {x} ..." | .vplam _ i _ => s!"vplam {i.name} ..." | .vpair _ _ => "vpair ..." @@ -60,9 +67,7 @@ def cvalSummary : CVal → String | .vctor _ c _ _ => s!"vctor {c} ..." | .vdimExpr _ => "vdimExpr ..." | .vcode _ => "vcode ..." - | .vFlatIntro _ => "vFlatIntro ..." - | .vSharpIntro _ => "vSharpIntro ..." - | .vShapeIntro _ => "vShapeIntro ..." + | .vModalIntro k _ => s!"vModalIntro {modalityKindTag k} ..." def ctermSummary : CTerm → String | .var x => s!"var {x}" @@ -75,12 +80,8 @@ def ctermSummary : CTerm → String | .dimExpr _ => "dimExpr ..." | .ctor _ c _ _ => s!"ctor {c} ..." | .indElim _ _ _ _ _ => "indElim ..." - | .flatIntro _ => "flatIntro ..." - | .sharpIntro _ => "sharpIntro ..." - | .shapeIntro _ => "shapeIntro ..." - | .flatElim _ _ => "flatElim ..." - | .sharpElim _ _ => "sharpElim ..." - | .shapeElim _ _ => "shapeElim ..." + | .modalIntro k _ => s!"modalIntro {modalityKindTag k} ..." + | .modalElim k _ _ => s!"modalElim {modalityKindTag k} ..." | _ => "" -- ── Individual test definitions ──────────────────────────────────────────── diff --git a/CubicalTransport/Modal.lean b/CubicalTransport/Modal.lean index 8f252b9..e584f58 100644 --- a/CubicalTransport/Modal.lean +++ b/CubicalTransport/Modal.lean @@ -74,6 +74,58 @@ import CubicalTransport.Category import CubicalTransport.Typing import CubicalTransport.Eval +-- ── Refactor Phase 2 transient aliases ────────────────────────────────────── +-- The engine's modal layer was unified: Phase 1's nine ad-hoc per-modality +-- constructors (3 CType + 6 CTerm) collapsed to three (`CType.modal`, +-- `CTerm.modalIntro`, `CTerm.modalElim`) parameterised by `ModalityKind`. +-- Modal.lean (Phase 3) was written against the Phase-1 names; rather than +-- rewrite it here (Phase 3's job), we surface the old names as `abbrev` +-- aliases that fully reduce to the unified forms — `abbrev`s carry the +-- `@[reducible]` attribute, so Lean's elaborator transparently unfolds +-- them at usage sites (including dot-notation `.flatIntro a` and the +-- structural `.modalIntro.injEq` lookup). These aliases live at the +-- top level so dot-syntax like `(.flatIntro x : CTerm)` finds them +-- under `CTerm.flatIntro`, not under `CubicalTransport.Modal.CTerm.flatIntro`. +-- Slated for removal in Modal Phase 3 (when this file is rewritten to +-- call the unified constructors directly). +-- +-- A few in-file references that depended on per-modality structural +-- machinery (`.flatIntro.injEq`, `.flatElim.injEq`, the per-modality +-- eval β-axioms) are rewritten in §1a / §4 below to use the unified +-- `.modalIntro.injEq` / `.modalElim.injEq` / `eval_modalElim_beta` +-- forms — the smallest mechanical change to keep this file's +-- substantive arguments going through. + +namespace CType + +/-- Transient alias: `CType.flat A = .modal .flat A`. Slated for + removal in Modal Phase 3. -/ +abbrev flat {ℓ : ULevel} (A : CType ℓ) : CType ℓ := .modal .flat A +/-- Transient alias: `CType.sharp A = .modal .sharp A`. -/ +abbrev sharp {ℓ : ULevel} (A : CType ℓ) : CType ℓ := .modal .sharp A +/-- Transient alias: `CType.shape A = .modal .shape A`. -/ +abbrev shape {ℓ : ULevel} (A : CType ℓ) : CType ℓ := .modal .shape A + +end CType + +namespace CTerm + +/-- Transient alias: `CTerm.flatIntro a = .modalIntro .flat a`. -/ +abbrev flatIntro (a : CTerm) : CTerm := .modalIntro .flat a +/-- Transient alias: `CTerm.sharpIntro a = .modalIntro .sharp a`. -/ +abbrev sharpIntro (a : CTerm) : CTerm := .modalIntro .sharp a +/-- Transient alias: `CTerm.shapeIntro a = .modalIntro .shape a`. -/ +abbrev shapeIntro (a : CTerm) : CTerm := .modalIntro .shape a + +/-- Transient alias: `CTerm.flatElim f m = .modalElim .flat f m`. -/ +abbrev flatElim (f m : CTerm) : CTerm := .modalElim .flat f m +/-- Transient alias: `CTerm.sharpElim f m = .modalElim .sharp f m`. -/ +abbrev sharpElim (f m : CTerm) : CTerm := .modalElim .sharp f m +/-- Transient alias: `CTerm.shapeElim f m = .modalElim .shape f m`. -/ +abbrev shapeElim (f m : CTerm) : CTerm := .modalElim .shape f m + +end CTerm + namespace CubicalTransport.Modal open CubicalTransport.Modality @@ -327,10 +379,11 @@ theorem flatFunctor_obj_dep (ℓ : ULevel) (X X' : CTerm) (h : X ≠ X') : intro hEq rw [flatFunctor_obj, flatFunctor_obj] at hEq -- .lam x (.flatIntro (.app X _)) = .lam x (.flatIntro (.app X' _)) - -- Peel through .lam, .flatIntro, .app to expose X vs X'. + -- After Refactor Phase 2 the alias unfolds to `.modalIntro .flat _`, + -- so we peel through .lam, .modalIntro, .app to expose X vs X'. have hbody := (CTerm.lam.injEq .. |>.mp hEq).2 - have hflat := (CTerm.flatIntro.injEq .. |>.mp hbody) - have happ := (CTerm.app.injEq .. |>.mp hflat).1 + have hmodal := (CTerm.modalIntro.injEq .. |>.mp hbody).2 + have happ := (CTerm.app.injEq .. |>.mp hmodal).1 exact h happ /-- The flat functor's `arr` is genuinely f-dependent. -/ @@ -338,13 +391,15 @@ theorem flatFunctor_arr_f_dep (ℓ : ULevel) (X Y f f' : CTerm) (h : f ≠ f') : (flatFunctor ℓ).arr X Y f ≠ (flatFunctor ℓ).arr X Y f' := by intro hEq rw [flatFunctor_arr, flatFunctor_arr] at hEq - -- Peel: .lam $m (.flatElim (.lam $y (.flatIntro (.app f $y))) $m) - -- through the outer lam, the flatElim, the inner lam, the flatIntro, - -- the app — exposing f vs f' as the LHS of the inner .app. + -- Peel: .lam $m (.modalElim .flat (.lam $y (.modalIntro .flat (.app f $y))) $m) + -- through the outer lam, the modalElim, the inner lam, the modalIntro, + -- the app — exposing f vs f' as the LHS of the inner .app. Refactor + -- Phase 2: `.flatElim` / `.flatIntro` aliases unfold to the unified + -- `.modalElim .flat` / `.modalIntro .flat`. have hbody := (CTerm.lam.injEq .. |>.mp hEq).2 - have hflatArg := (CTerm.flatElim.injEq .. |>.mp hbody).1 + have hflatArg := (CTerm.modalElim.injEq .. |>.mp hbody).2.1 have hLam := (CTerm.lam.injEq .. |>.mp hflatArg).2 - have hIntro := (CTerm.flatIntro.injEq .. |>.mp hLam) + have hIntro := (CTerm.modalIntro.injEq .. |>.mp hLam).2 have happ := (CTerm.app.injEq .. |>.mp hIntro).1 exact h happ @@ -584,27 +639,28 @@ theorem cohesive_triple (ℓ : ULevel) : -- definitionally for `partial` defs). Hence `rfl` does not close -- the goal, but the axiom does. -/-- **Soundness for the flat β-rule** (THEORY.md §3.2 reduction - rules; Phase 1 axiom `Eval.eval_flatElim_beta`). +/-- **Soundness for the flat β-rule** (THEORY.md §3.2 reduction rules). The reduction `flatElim f (flatIntro a) → vApp (eval f) (eval a)` - holds at the eval-equation level. Recorded here as a theorem - so downstream tactics may rewrite with it. -/ + holds at the eval-equation level. Recorded here as a theorem so + downstream tactics may rewrite with it. Refactor Phase 2: the + underlying axiom is now the unified `eval_modalElim_beta` + instantiated at `.flat`. -/ theorem flat_beta_sound (env : CEnv) (f a : CTerm) : eval env (.flatElim f (.flatIntro a)) = vApp (eval env f) (eval env a) := - eval_flatElim_beta env f a + eval_modalElim_beta env .flat f a /-- **Soundness for the sharp β-rule** (analogous to flat). -/ theorem sharp_beta_sound (env : CEnv) (f a : CTerm) : eval env (.sharpElim f (.sharpIntro a)) = vApp (eval env f) (eval env a) := - eval_sharpElim_beta env f a + eval_modalElim_beta env .sharp f a /-- **Soundness for the shape β-rule** (analogous to flat). -/ theorem shape_beta_sound (env : CEnv) (f a : CTerm) : eval env (.shapeElim f (.shapeIntro a)) = vApp (eval env f) (eval env a) := - eval_shapeElim_beta env f a + eval_modalElim_beta env .shape f a end CubicalTransport.Modal diff --git a/CubicalTransport/Question.lean b/CubicalTransport/Question.lean index 8329fa0..01cb86a 100644 --- a/CubicalTransport/Question.lean +++ b/CubicalTransport/Question.lean @@ -160,21 +160,13 @@ def IsUnivLine (q : CompQ) : Prop := def IsElLine (q : CompQ) : Prop := q.body.skeleton = SkeletalCType.El -/-- The line is a `.flat` modality. Encoded via the level-erased - skeleton tag. -/ +/-- The line is a modality of kind `k` (Refactor Phase 2). Encoded + via the level-erased skeleton tag, parameterised over + `ModalityKind`. Specialise via `IsModalLine q .flat` / + `IsModalLine q .sharp` / `IsModalLine q .shape`. -/ @[simp] -def IsFlatLine (q : CompQ) : Prop := - q.body.skeleton = SkeletalCType.flat - -/-- The line is a `.sharp` modality. -/ -@[simp] -def IsSharpLine (q : CompQ) : Prop := - q.body.skeleton = SkeletalCType.sharp - -/-- The line is a `.shape` modality. -/ -@[simp] -def IsShapeLine (q : CompQ) : Prop := - q.body.skeleton = SkeletalCType.shape +def IsModalLine (q : CompQ) (k : ModalityKind) : Prop := + q.body.skeleton = SkeletalCType.modal k -- ── Decidability for the core classifiers ─────────────────────────────────── -- All instances are computable. Body-shape predicates are skeleton-eq @@ -215,9 +207,7 @@ instance instDecidableIsPathLine (q : CompQ) : Decidable (IsPathLine q) := by | interval => simp at hs | lift A => simp at hs | El P => simp at hs - | flat A => simp at hs - | sharp A => simp at hs - | shape A => simp at hs + | modal k A => simp at hs · refine isFalse (fun ⟨_, _, _, hbody⟩ => hs ?_) rw [hbody]; rfl @@ -236,9 +226,7 @@ instance instDecidableIsGlueLine (q : CompQ) : Decidable (IsGlueLine q) := by | interval => simp at hs | lift A => simp at hs | El P => simp at hs - | flat A => simp at hs - | sharp A => simp at hs - | shape A => simp at hs + | modal k A => simp at hs · refine isFalse (fun ⟨_, _, _, _, _, _, _, _, hbody⟩ => hs ?_) rw [hbody]; rfl @@ -254,14 +242,8 @@ instance (q : CompQ) : Decidable (IsIndLine q) := instance instDecidableIsElLine (q : CompQ) : Decidable (IsElLine q) := inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.El)) -instance (q : CompQ) : Decidable (IsFlatLine q) := - inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.flat)) - -instance (q : CompQ) : Decidable (IsSharpLine q) := - inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.sharp)) - -instance (q : CompQ) : Decidable (IsShapeLine q) := - inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.shape)) +instance (q : CompQ) (k : ModalityKind) : Decidable (IsModalLine q k) := + inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.modal k)) -- ── Classifier-conditioned theorems ───────────────────────────────────────── @@ -365,12 +347,10 @@ def IsUnivLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.univ @[simp] def IsElLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.El +/-- The line is a modality of kind `k` (Refactor Phase 2). -/ @[simp] -def IsFlatLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.flat -@[simp] -def IsSharpLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.sharp -@[simp] -def IsShapeLine (q : TranspQ) : Prop := q.body.skeleton = SkeletalCType.shape +def IsModalLine (q : TranspQ) (k : ModalityKind) : Prop := + q.body.skeleton = SkeletalCType.modal k instance (q : TranspQ) : Decidable (IsConstLine q) := inferInstanceAs (Decidable (q.body.dimAbsent q.binder = true)) @@ -393,12 +373,8 @@ instance (q : TranspQ) : Decidable (IsIndLine q) := instance instDecidableTranspIsElLine (q : TranspQ) : Decidable (IsElLine q) := inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.El)) -instance (q : TranspQ) : Decidable (IsFlatLine q) := - inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.flat)) -instance (q : TranspQ) : Decidable (IsSharpLine q) := - inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.sharp)) -instance (q : TranspQ) : Decidable (IsShapeLine q) := - inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.shape)) +instance (q : TranspQ) (k : ModalityKind) : Decidable (IsModalLine q k) := + inferInstanceAs (Decidable (q.body.skeleton = SkeletalCType.modal k)) instance instDecidableTranspIsPathLine (q : TranspQ) : Decidable (IsPathLine q) := by by_cases hs : q.body.skeleton = SkeletalCType.path @@ -414,9 +390,7 @@ instance instDecidableTranspIsPathLine (q : TranspQ) : Decidable (IsPathLine q) | interval => simp at hs | lift A => simp at hs | El P => simp at hs - | flat A => simp at hs - | sharp A => simp at hs - | shape A => simp at hs + | modal k A => simp at hs · refine isFalse (fun ⟨_, _, _, hbody⟩ => hs ?_) rw [hbody]; rfl @@ -435,9 +409,7 @@ instance instDecidableTranspIsGlueLine (q : TranspQ) : Decidable (IsGlueLine q) | interval => simp at hs | lift A => simp at hs | El P => simp at hs - | flat A => simp at hs - | sharp A => simp at hs - | shape A => simp at hs + | modal k A => simp at hs · refine isFalse (fun ⟨_, _, _, _, _, _, _, _, hbody⟩ => hs ?_) rw [hbody]; rfl diff --git a/CubicalTransport/Readback.lean b/CubicalTransport/Readback.lean index 88b7536..3092178 100644 --- a/CubicalTransport/Readback.lean +++ b/CubicalTransport/Readback.lean @@ -144,10 +144,9 @@ mutual | .vdimExpr r => .dimExpr r -- Universe-code value: read back as the encoder constructor. | .vcode A => .code A - -- Modal-introduction values: structural readback of the wrapped value. - | .vFlatIntro a => .flatIntro (readback a) - | .vSharpIntro a => .sharpIntro (readback a) - | .vShapeIntro a => .shapeIntro (readback a) + -- Modal-introduction value: structural readback of the wrapped value, + -- preserving the modality kind. + | .vModalIntro k a => .modalIntro k (readback a) /-- Readback a `CNeu` into a `CTerm`. Straightforward structural recursion: each neutral constructor has a syntactic counterpart. @@ -176,11 +175,10 @@ mutual .indElim S params (readback motive) (branches.map (fun p => (p.1, readback p.2))) (readbackNeu target) - -- Modal-elimination stuck forms: rebuild the elim term with the - -- read-back eliminator function and the read-back stuck scrutinee. - | .nflatElim f n => .flatElim (readback f) (readbackNeu n) - | .nsharpElim f n => .sharpElim (readback f) (readbackNeu n) - | .nshapeElim f n => .shapeElim (readback f) (readbackNeu n) + -- Modal-elimination stuck form: rebuild the elim term with the + -- read-back eliminator function and the read-back stuck scrutinee, + -- preserving the modality kind. + | .nModalElim k f n => .modalElim k (readback f) (readbackNeu n) end -- ── Convenience wrapper ───────────────────────────────────────────────────── @@ -305,27 +303,15 @@ axiom readback_vpair (a b : CVal) : axiom readback_vcode {ℓ : ULevel} (A : CType ℓ) : readback (.vcode A) = .code A --- Modal-introduction readback axioms. +-- Modal-introduction readback axiom (Refactor Phase 2). -axiom readback_vFlatIntro (a : CVal) : - readback (.vFlatIntro a) = .flatIntro (readback a) +axiom readback_vModalIntro (k : ModalityKind) (a : CVal) : + readback (.vModalIntro k a) = .modalIntro k (readback a) -axiom readback_vSharpIntro (a : CVal) : - readback (.vSharpIntro a) = .sharpIntro (readback a) +-- Modal-elimination (stuck) readback axiom (Refactor Phase 2). -axiom readback_vShapeIntro (a : CVal) : - readback (.vShapeIntro a) = .shapeIntro (readback a) - --- Modal-elimination (stuck) readback axioms. - -axiom readbackNeu_nflatElim (f : CVal) (n : CNeu) : - readbackNeu (.nflatElim f n) = .flatElim (readback f) (readbackNeu n) - -axiom readbackNeu_nsharpElim (f : CVal) (n : CNeu) : - readbackNeu (.nsharpElim f n) = .sharpElim (readback f) (readbackNeu n) - -axiom readbackNeu_nshapeElim (f : CVal) (n : CNeu) : - readbackNeu (.nshapeElim f n) = .shapeElim (readback f) (readbackNeu n) +axiom readbackNeu_nModalElim (k : ModalityKind) (f : CVal) (n : CNeu) : + readbackNeu (.nModalElim k f n) = .modalElim k (readback f) (readbackNeu n) axiom readbackNeu_nfst (n : CNeu) : readbackNeu (.nfst n) = .fst (readbackNeu n) diff --git a/CubicalTransport/Reflect.lean b/CubicalTransport/Reflect.lean index 3c265d4..9f07510 100644 --- a/CubicalTransport/Reflect.lean +++ b/CubicalTransport/Reflect.lean @@ -164,6 +164,27 @@ partial def reifyStrLit (e : Expr) : MetaM (Option String) := do | .lit (.strVal s) => return some s | _ => return none +-- ── §3a. ModalityKind reflect / reify (Refactor Phase 2) ────────────────── + +/-- Reflect a `ModalityKind` to its `Lean.Expr` encoding. The + `ModalityKind` enum is finite with three nullary constructors; + each maps to its `mkConst`-encoded fully-qualified name. -/ +def reflectModalityKind : ModalityKind → MetaM Expr + | .flat => return mkConst ``ModalityKind.flat + | .sharp => return mkConst ``ModalityKind.sharp + | .shape => return mkConst ``ModalityKind.shape + +/-- Reify a `Lean.Expr` back to a `ModalityKind`. Inverse of + `reflectModalityKind` — recognises the three constructor names + via `getAppFnArgs`. -/ +def reifyModalityKind (e : Expr) : MetaM (Option ModalityKind) := do + let e ← whnf e + match e.getAppFnArgs with + | (``ModalityKind.flat, _) => return some .flat + | (``ModalityKind.sharp, _) => return some .sharp + | (``ModalityKind.shape, _) => return some .shape + | _ => return none + -- ── §4. Macro: derive_reflect_reify ────────────────────────────────────── -- -- The metaprogramming layer that emits per-constructor reflect/reify arms @@ -219,6 +240,9 @@ inductive FieldKind where | nat /-- `ULevel` — uses `reflectULevel` / `reifyULevel`. -/ | uLevel + /-- `ModalityKind` (Refactor Phase 2) — uses + `reflectModalityKind` / `reifyModalityKind`. -/ + | modalityKind /-- A simple inductive name (`DimVar`, `DimExpr`, `FaceFormula`, `CTerm`, `CTypeArg`, `CtorSpec`, `CTypeSchema`). Uses `reflect` / `reify`. -/ @@ -250,6 +274,7 @@ def classifyFieldType (ty : Expr) : MetaM (Option FieldKind) := do | (``String, _) => return some .str | (``Nat, _) => return some .nat | (``ULevel, _) => return some .uLevel + | (``ModalityKind, _) => return some .modalityKind | (``DimVar, _) => return some (.indSimple ``DimVar) | (``DimExpr, _) => return some (.indSimple ``DimExpr) | (``FaceFormula, _) => return some (.indSimple ``FaceFormula) @@ -319,6 +344,7 @@ def reflectFunFor : FieldKind → Name | .str => Name.mkSimple "mkStrLit" -- inline-emitted via Lean.mkStrLit | .nat => Name.mkSimple "mkNatLit" -- inline-emitted via Lean.mkNatLit | .uLevel => `CubicalTransport.Reflect.reflectULevel + | .modalityKind => `CubicalTransport.Reflect.reflectModalityKind | .cType => `CubicalTransport.Reflect.reflectCType | .indSimple n => mkReflectName n | .listInd n => mkReflectListName n @@ -331,6 +357,7 @@ def reifyFunFor : FieldKind → Name | .str => `CubicalTransport.Reflect.reifyStrLit | .nat => `CubicalTransport.Reflect.reifyNatLit | .uLevel => `CubicalTransport.Reflect.reifyULevel + | .modalityKind => `CubicalTransport.Reflect.reifyModalityKind | .cType => `CubicalTransport.Reflect.reifyCType | .indSimple n => mkReifyName n | .listInd n => mkReifyListName n diff --git a/CubicalTransport/Subst.lean b/CubicalTransport/Subst.lean index ec49a13..d6f3cef 100644 --- a/CubicalTransport/Subst.lean +++ b/CubicalTransport/Subst.lean @@ -90,10 +90,8 @@ mutual | .interval => .interval | .lift A => .lift (A.substDim i b) | .El P => .El (P.substDimBool i b) - -- Modal type formers: descend into the inner type. - | .flat A => .flat (A.substDim i b) - | .sharp A => .sharp (A.substDim i b) - | .shape A => .shape (A.substDim i b) + -- Modal type former: descend into the inner type, preserving the kind. + | .modal k A => .modal k (A.substDim i b) /-- Pointwise `substDim` through a level-heterogeneous list of CType parameters. Each entry's universe level is preserved. -/ @@ -124,10 +122,8 @@ mutual | .interval => .interval | .lift A => .lift (A.substDimExpr i r) | .El P => .El (P.substDim i r) - -- Modal type formers: descend into the inner type. - | .flat A => .flat (A.substDimExpr i r) - | .sharp A => .sharp (A.substDimExpr i r) - | .shape A => .shape (A.substDimExpr i r) + -- Modal type former: descend into the inner type, preserving the kind. + | .modal k A => .modal k (A.substDimExpr i r) /-- Pointwise `substDimExpr` through a level-heterogeneous list of CType parameters. -/ @@ -181,14 +177,9 @@ theorem substDim_lift {ℓ : ULevel} (i : DimVar) (b : Bool) (A : CType ℓ) : @[simp] theorem substDim_El {ℓ : ULevel} (i : DimVar) (b : Bool) (P : CTerm) : (CType.El (ℓ := ℓ) P).substDim i b = .El (P.substDimBool i b) := rfl -@[simp] theorem substDim_flat {ℓ : ULevel} (i : DimVar) (b : Bool) (A : CType ℓ) : - (CType.flat A).substDim i b = .flat (A.substDim i b) := rfl - -@[simp] theorem substDim_sharp {ℓ : ULevel} (i : DimVar) (b : Bool) (A : CType ℓ) : - (CType.sharp A).substDim i b = .sharp (A.substDim i b) := rfl - -@[simp] theorem substDim_shape {ℓ : ULevel} (i : DimVar) (b : Bool) (A : CType ℓ) : - (CType.shape A).substDim i b = .shape (A.substDim i b) := rfl +@[simp] theorem substDim_modal {ℓ : ULevel} (i : DimVar) (b : Bool) + (k : ModalityKind) (A : CType ℓ) : + (CType.modal k A).substDim i b = .modal k (A.substDim i b) := rfl -- ── Reduction lemmas (substDimExpr) ────────────────────────────────────────── @@ -234,14 +225,9 @@ theorem substDimExpr_lift {ℓ : ULevel} (i : DimVar) (r : DimExpr) (A : CType @[simp] theorem substDimExpr_El {ℓ : ULevel} (i : DimVar) (r : DimExpr) (P : CTerm) : (CType.El (ℓ := ℓ) P).substDimExpr i r = .El (P.substDim i r) := rfl -@[simp] theorem substDimExpr_flat {ℓ : ULevel} (i : DimVar) (r : DimExpr) (A : CType ℓ) : - (CType.flat A).substDimExpr i r = .flat (A.substDimExpr i r) := rfl - -@[simp] theorem substDimExpr_sharp {ℓ : ULevel} (i : DimVar) (r : DimExpr) (A : CType ℓ) : - (CType.sharp A).substDimExpr i r = .sharp (A.substDimExpr i r) := rfl - -@[simp] theorem substDimExpr_shape {ℓ : ULevel} (i : DimVar) (r : DimExpr) (A : CType ℓ) : - (CType.shape A).substDimExpr i r = .shape (A.substDimExpr i r) := rfl +@[simp] theorem substDimExpr_modal {ℓ : ULevel} (i : DimVar) (r : DimExpr) + (k : ModalityKind) (A : CType ℓ) : + (CType.modal k A).substDimExpr i r = .modal k (A.substDimExpr i r) := rfl -- ── Bool endpoint = DimExpr at canonical endpoint ──────────────────────────── @@ -296,14 +282,8 @@ mutual show CType.El (CTerm.substDimBool i b P) = CType.El (CTerm.substDim i (if b then DimExpr.one else DimExpr.zero) P) rw [CTerm.substDimBool_eq_substDim] - | .flat A => by - show CType.flat (A.substDim i b) = CType.flat (A.substDimExpr i _) - rw [substDim_eq_substDimExpr i b A] - | .sharp A => by - show CType.sharp (A.substDim i b) = CType.sharp (A.substDimExpr i _) - rw [substDim_eq_substDimExpr i b A] - | .shape A => by - show CType.shape (A.substDim i b) = CType.shape (A.substDimExpr i _) + | .modal k A => by + show CType.modal k (A.substDim i b) = CType.modal k (A.substDimExpr i _) rw [substDim_eq_substDimExpr i b A] /-- Helper: pointwise equality between `substDim.params` and diff --git a/CubicalTransport/Syntax.lean b/CubicalTransport/Syntax.lean index 69414be..2c9a689 100644 --- a/CubicalTransport/Syntax.lean +++ b/CubicalTransport/Syntax.lean @@ -68,6 +68,37 @@ import CubicalTransport.Face import CubicalTransport.Universe +-- ── Modality kind (Refactor Phase 2) ──────────────────────────────────────── +-- A level-erased enum tagging which modality of the cohesive triple we +-- are talking about. Replaces the Phase-1 set of nine ad-hoc per-modality +-- constructors with three unified `ModalityKind`-parameterised constructors +-- (`CType.modal`, `CTerm.modalIntro`, `CTerm.modalElim`, plus the value- +-- level `CVal.vModalIntro` and `CNeu.nModalElim`). +-- +-- Future modalities (e.g. Phase-4's `sharp_EML`, an `infinitesimal` arm) +-- extend this enum by adding cases — the engine modal layer is henceforth +-- parameterised over `ModalityKind`. + +/-- The three modalities of the cohesive triple `ʃ ⊣ ♭ ⊣ ♯` + (Schreiber/Shulman cohesive HoTT). Per THEORY.md §3.1. + + · `flat` — the discrete reflection (`♭`), middle modality, right + adjoint to `shape`. + · `sharp` — the codiscrete coreflection (`♯`), right adjoint to `flat`. + · `shape` — the shape modality (`ʃ`), left adjoint to `flat`. + + `DecidableEq` is structural; future modalities (extra enum arms) + inherit decidable equality automatically. `Repr` and `Inhabited` + are likewise standard. -/ +inductive ModalityKind : Type where + /-- ♭, the discrete reflection (right adjoint to shape). -/ + | flat + /-- ♯, the codiscrete coreflection (right adjoint to flat). -/ + | sharp + /-- ʃ, the shape modality (left adjoint to flat). -/ + | shape + deriving DecidableEq, Repr, Inhabited + -- ── Universe-stratified syntax ────────────────────────────────────────────── mutual @@ -140,31 +171,18 @@ mutual propositions and refer back to the underlying type. -/ | El {ℓ : ULevel} (P : CTerm) : CType ℓ - /-- **Modal type former: flat (♭).** Given `A : CType ℓ`, the type - `flat A` lives at the same universe level `ℓ`. Together with - `sharp` and `shape`, these are the three modalities of the - cohesive triple `♭ ⊣ ♯ ⊣ ʃ` (Schreiber/Shulman cohesive HoTT). + /-- **Modal type former (Refactor Phase 2).** Given a modality kind + `k : ModalityKind` and `A : CType ℓ`, the modal type + `modal k A` lives at the same universe level `ℓ`. Replaces the + Phase-1 ad-hoc trio `.flat`/`.sharp`/`.shape` with a single + `ModalityKind`-parameterised constructor. At the engine layer we add the data constructor; the modal - cohesion content (Crisp variables, the `♭ ⊣ ♯` adjunction, + cohesion content (Crisp variables, the `ʃ ⊣ ♭ ⊣ ♯` adjunctions, modal-shape commutation diagrams) is the Phase 3 module. Per THEORY.md §3.1; mirrors `path` in level preservation. -/ - | flat {ℓ : ULevel} (A : CType ℓ) - : CType ℓ - /-- **Modal type former: sharp (♯).** Given `A : CType ℓ`, the type - `sharp A` lives at the same universe level `ℓ`. Right adjoint - of `flat` in the cohesive triple `♭ ⊣ ♯ ⊣ ʃ`. - - Per THEORY.md §3.1. -/ - | sharp {ℓ : ULevel} (A : CType ℓ) - : CType ℓ - /-- **Modal type former: shape (ʃ).** Given `A : CType ℓ`, the type - `shape A` lives at the same universe level `ℓ`. Left adjoint - of `flat` in the cohesive triple `♭ ⊣ ♯ ⊣ ʃ`. - - Per THEORY.md §3.1. -/ - | shape {ℓ : ULevel} (A : CType ℓ) + | modal {ℓ : ULevel} (k : ModalityKind) (A : CType ℓ) : CType ℓ /-- Terms in the cubical calculus. Un-indexed by universe level — @@ -224,35 +242,25 @@ mutual `.univ (ℓ := ℓ)`. Carries the underlying type as data. -/ | code {ℓ : ULevel} (A : CType ℓ) : CTerm - /-- **Modal introduction: η_♭ (flat).** Given `a : A`, the term - `flatIntro a` inhabits `flat A`. Mirrors the `glueIn` shape: - a single argument carrying the wrapped value. + /-- **Modal introduction (Refactor Phase 2).** Given a modality + kind `k : ModalityKind` and a term `a : A`, the term + `modalIntro k a` inhabits `modal k A`. Replaces the Phase-1 + trio `.flatIntro`/`.sharpIntro`/`.shapeIntro` with a single + unified constructor parameterised over `k`. - Reduction: `flatElim f (flatIntro a)` ↝ `app f a`. -/ - | flatIntro (a : CTerm) + Reduction: `modalElim k f (modalIntro k a)` ↝ `app f a` (β + fires only when both elim and intro carry the same kind). -/ + | modalIntro (k : ModalityKind) (a : CTerm) : CTerm - /-- **Modal introduction: η_♯ (sharp).** Given `a : A`, the term - `sharpIntro a` inhabits `sharp A`. -/ - | sharpIntro (a : CTerm) - : CTerm - /-- **Modal introduction: η_ʃ (shape).** Given `a : A`, the term - `shapeIntro a` inhabits `shape A`. -/ - | shapeIntro (a : CTerm) - : CTerm - /-- **Modal elimination: ♭.rec.** Given the elimination function - `f : A → C` and a scrutinee `m : flat A`, produce a term of - type `C`. Two CTerms: target then scrutinee — same shape as - `unglue` (modulo unglue's leading FaceFormula). + /-- **Modal elimination (Refactor Phase 2).** Given an elimination + function `f : A → C` and a scrutinee `m : modal k A`, produce + a term of type `C`. Replaces the Phase-1 trio `.flatElim` / + `.sharpElim` / `.shapeElim` with one unified + `ModalityKind`-parameterised constructor. - Reduction: `flatElim f (flatIntro a)` ↝ `app f a` (β-rule). - Otherwise: stuck `nflatElim` neutral. -/ - | flatElim (f m : CTerm) - : CTerm - /-- **Modal elimination: ♯.rec.** Same shape as `flatElim`. -/ - | sharpElim (f m : CTerm) - : CTerm - /-- **Modal elimination: ʃ.rec.** Same shape as `flatElim`. -/ - | shapeElim (f m : CTerm) + Reduction: `modalElim k f (modalIntro k a)` ↝ `app f a` (β-rule + on matching kinds). Otherwise: stuck `nModalElim k` neutral. -/ + | modalElim (k : ModalityKind) (f m : CTerm) : CTerm /-- Argument shape for a schema constructor (REL1, §2.1). -/ @@ -324,9 +332,10 @@ inductive SkeletalCType : Type where | interval | lift | El - | flat - | sharp - | shape + /-- Modal skeleton (Refactor Phase 2). Carries the modality kind so + that distinct modalities (`♭` vs `♯` vs `ʃ`) remain distinct + skeletons — required for constructor-disjointness reasoning. -/ + | modal (k : ModalityKind) deriving Repr, DecidableEq /-- Strip the universe index, preserving the head constructor as a tag. @@ -343,9 +352,7 @@ def CType.skeleton {ℓ : ULevel} : CType ℓ → SkeletalCType | .interval => .interval | .lift _ => .lift | .El _ => .El - | .flat _ => .flat - | .sharp _ => .sharp - | .shape _ => .shape + | .modal k _ => .modal k -- ── Skeleton equations (rfl-provable) ──────────────────────────────────────── @@ -415,20 +422,11 @@ theorem CType.skeleton_lift {ℓ : ULevel} (A : CType ℓ) : @[simp] theorem CType.skeleton_El {ℓ : ULevel} (P : CTerm) : (CType.El (ℓ := ℓ) P).skeleton = SkeletalCType.El := rfl -/-- The skeleton of `.flat` is `.flat`. -/ +/-- The skeleton of `.modal k A` is `.modal k`. Carries the modality + kind through so that distinct kinds remain distinct skeletons. -/ @[simp] -theorem CType.skeleton_flat {ℓ : ULevel} (A : CType ℓ) : - (CType.flat A).skeleton = SkeletalCType.flat := rfl - -/-- The skeleton of `.sharp` is `.sharp`. -/ -@[simp] -theorem CType.skeleton_sharp {ℓ : ULevel} (A : CType ℓ) : - (CType.sharp A).skeleton = SkeletalCType.sharp := rfl - -/-- The skeleton of `.shape` is `.shape`. -/ -@[simp] -theorem CType.skeleton_shape {ℓ : ULevel} (A : CType ℓ) : - (CType.shape A).skeleton = SkeletalCType.shape := rfl +theorem CType.skeleton_modal {ℓ : ULevel} (k : ModalityKind) (A : CType ℓ) : + (CType.modal k A).skeleton = SkeletalCType.modal k := rfl -- ── Constructor disjointness via skeleton ──────────────────────────────────── @@ -514,14 +512,10 @@ mutual -- Same approximation as transp/comp: A is not recursed into. | .code A => .code A -- Modal introductions: structural recursion into the wrapped term. - | .flatIntro a => .flatIntro (a.substDim i r) - | .sharpIntro a => .sharpIntro (a.substDim i r) - | .shapeIntro a => .shapeIntro (a.substDim i r) + | .modalIntro k a => .modalIntro k (a.substDim i r) -- Modal eliminations: structural recursion into both subterms -- (eliminator function and scrutinee). - | .flatElim f m => .flatElim (f.substDim i r) (m.substDim i r) - | .sharpElim f m => .sharpElim (f.substDim i r) (m.substDim i r) - | .shapeElim f m => .shapeElim (f.substDim i r) (m.substDim i r) + | .modalElim k f m => .modalElim k (f.substDim i r) (m.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. -/ diff --git a/CubicalTransport/Typing.lean b/CubicalTransport/Typing.lean index 31c437f..ef06610 100644 --- a/CubicalTransport/Typing.lean +++ b/CubicalTransport/Typing.lean @@ -173,52 +173,33 @@ inductive HasType : Ctx → CTerm → ∀ {ℓ : ULevel}, CType ℓ → Prop whe | code : ∀ {Γ : Ctx} {ℓ : ULevel} (A : CType ℓ), HasType Γ (.code A) (.univ (ℓ := ℓ)) - /-- **Modal introduction (flat).** Given `a : A`, the term - `flatIntro a` inhabits `flat A`. Engine-layer rule — - modal-cohesion contextual restrictions (Crisp variables, - Π-modality interaction, etc.) land in Phase 3. -/ - | flatIntro {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} {a : CTerm} : + /-- **Modal introduction (Refactor Phase 2).** Given a modality kind + `k` and a term `a : A`, the term `modalIntro k a` inhabits + `modal k A`. Engine-layer rule — modal-cohesion contextual + restrictions (Crisp variables, Π-modality interaction, etc.) + land in Phase 3. -/ + | modalIntro {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} + {k : ModalityKind} {a : CTerm} : HasType Γ a A → - HasType Γ (.flatIntro a) (.flat A) + HasType Γ (.modalIntro k a) (.modal k A) - /-- **Modal introduction (sharp).** -/ - | sharpIntro {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} {a : CTerm} : - HasType Γ a A → - HasType Γ (.sharpIntro a) (.sharp A) - - /-- **Modal introduction (shape).** -/ - | shapeIntro {Γ : Ctx} {ℓ : ULevel} {A : CType ℓ} {a : CTerm} : - HasType Γ a A → - HasType Γ (.shapeIntro a) (.shape A) - - /-- **Modal elimination (flat).** Given an eliminator `f : A → C` - and a scrutinee `m : flat A`, produce a term of type `C`. + /-- **Modal elimination (Refactor Phase 2).** Given a modality kind + `k`, an eliminator `f : A → C`, and a scrutinee `m : modal k A`, + produce a term of type `C`. Engine layer: this is the bare recursion-principle shape; the - modal-cohesion side-conditions (e.g. C must be flat-modal for - the elim to be well-formed in cohesive HoTT) are deferred to - Phase 3 (`Modal.lean`). At the engine layer the rule reflects - the recursion principle directly so that `eval` and `readback` - can dispatch on it. -/ - | flatElim {Γ : Ctx} {ℓ ℓ' : ULevel} {A : CType ℓ} {C : CType ℓ'} - {f m : CTerm} {var : String} : + modal-cohesion side-conditions (e.g. C must be appropriately + modal for the elim to be well-formed in cohesive HoTT) are + deferred to Phase 3 (`Modal.lean`). At the engine layer the + rule reflects the recursion principle directly so that `eval` + and `readback` can dispatch on it. The kind `k` is shared + between the scrutinee's type and the elim — a cross-kind elim + is a type error not statable in this judgment. -/ + | modalElim {Γ : Ctx} {ℓ ℓ' : ULevel} {A : CType ℓ} {C : CType ℓ'} + {k : ModalityKind} {f m : CTerm} {var : String} : HasType Γ f (.pi var A C) → - HasType Γ m (.flat A) → - HasType Γ (.flatElim f m) C - - /-- **Modal elimination (sharp).** -/ - | sharpElim {Γ : Ctx} {ℓ ℓ' : ULevel} {A : CType ℓ} {C : CType ℓ'} - {f m : CTerm} {var : String} : - HasType Γ f (.pi var A C) → - HasType Γ m (.sharp A) → - HasType Γ (.sharpElim f m) C - - /-- **Modal elimination (shape).** -/ - | shapeElim {Γ : Ctx} {ℓ ℓ' : ULevel} {A : CType ℓ} {C : CType ℓ'} - {f m : CTerm} {var : String} : - HasType Γ f (.pi var A C) → - HasType Γ m (.shape A) → - HasType Γ (.shapeElim f m) C + HasType Γ m (.modal k A) → + HasType Γ (.modalElim k f m) C -- ── Structural rules ────────────────────────────────────────────────────────── @@ -274,24 +255,12 @@ private theorem HasType.weaken_core intro _ _; exact HasType.dimExpr | code A => intro _ _; exact HasType.code A - | flatIntro ha ih => + | modalIntro ha ih => intro Γ₁ hΓ; subst hΓ - exact HasType.flatIntro (ih Γ₁ rfl) - | sharpIntro ha ih => + exact HasType.modalIntro (ih Γ₁ rfl) + | modalElim hf hm ihf ihm => intro Γ₁ hΓ; subst hΓ - exact HasType.sharpIntro (ih Γ₁ rfl) - | shapeIntro ha ih => - intro Γ₁ hΓ; subst hΓ - exact HasType.shapeIntro (ih Γ₁ rfl) - | flatElim hf hm ihf ihm => - intro Γ₁ hΓ; subst hΓ - exact HasType.flatElim (ihf Γ₁ rfl) (ihm Γ₁ rfl) - | sharpElim hf hm ihf ihm => - intro Γ₁ hΓ; subst hΓ - exact HasType.sharpElim (ihf Γ₁ rfl) (ihm Γ₁ rfl) - | shapeElim hf hm ihf ihm => - intro Γ₁ hΓ; subst hΓ - exact HasType.shapeElim (ihf Γ₁ rfl) (ihm Γ₁ rfl) + exact HasType.modalElim (ihf Γ₁ rfl) (ihm Γ₁ rfl) theorem HasType.weaken (x : String) {ℓB : ULevel} (B : CType ℓB) {Γ : Ctx} {t : CTerm} {ℓ : ULevel} {A : CType ℓ} diff --git a/CubicalTransport/Value.lean b/CubicalTransport/Value.lean index e55c724..5f30c09 100644 --- a/CubicalTransport/Value.lean +++ b/CubicalTransport/Value.lean @@ -81,13 +81,12 @@ mutual | vdimExpr : DimExpr → CVal /-- Value form of `CTerm.code A`. Carries the encoded CType. -/ | vcode {ℓ : ULevel} : CType ℓ → CVal - /-- Value form of `CTerm.flatIntro a`: the η-introduction value - for the flat (♭) modality, carrying the wrapped value. -/ - | vFlatIntro : CVal → CVal - /-- Value form of `CTerm.sharpIntro a`. -/ - | vSharpIntro : CVal → CVal - /-- Value form of `CTerm.shapeIntro a`. -/ - | vShapeIntro : CVal → CVal + /-- Value form of `CTerm.modalIntro k a` (Refactor Phase 2): the + η-introduction value for modality `k`, carrying the wrapped + value. Replaces the Phase-1 trio + `vFlatIntro`/`vSharpIntro`/`vShapeIntro` with a single + `ModalityKind`-parameterised constructor. -/ + | vModalIntro : ModalityKind → CVal → CVal /-- Neutral (stuck) terms. -/ inductive CNeu : Type where @@ -123,14 +122,13 @@ mutual /-- A stuck inductive eliminator (REL1). `params` is level-heterogeneous. -/ | nIndElim : CTypeSchema → List (Σ ℓ : ULevel, CType ℓ) → CVal → List (String × CVal) → CNeu → CNeu - /-- A stuck flat-modality eliminator: `flatElim f m` where the - scrutinee `m` is a stuck CNeu (so β can't fire). Stores the - evaluated eliminator function and the stuck scrutinee. -/ - | nflatElim : CVal → CNeu → CNeu - /-- A stuck sharp-modality eliminator. -/ - | nsharpElim : CVal → CNeu → CNeu - /-- A stuck shape-modality eliminator. -/ - | nshapeElim : CVal → CNeu → CNeu + /-- A stuck modal eliminator (Refactor Phase 2): `modalElim k f m` + where the scrutinee `m` is a stuck CNeu (so β can't fire). + Stores the modality kind, the evaluated eliminator function, + and the stuck scrutinee. Replaces the Phase-1 trio + `nflatElim`/`nsharpElim`/`nshapeElim` with a single + `ModalityKind`-parameterised constructor. -/ + | nModalElim : ModalityKind → CVal → CNeu → CNeu end -- Inhabited instances — needed so `partial def` evaluators can be elaborated