From 48b732652338820917165bd4820f01a6cbadbf67 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Fri, 1 May 2026 02:57:48 -0600 Subject: [PATCH] =?UTF-8?q?Abstract=20the=20four=20=E2=9A=A0=EF=B8=8F=20to?= =?UTF-8?q?ols=20into=20well-defined=20primitives?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per feedback "tooling possible, not tools — highly selective". Each former opinionated wrapper either reduces to a Lean-standard mechanism or splits into stated-contract primitives. CubicalTransport/Question.lean: - Drop the `cubical_simp` and `cubical_simp [..]` macros. They baked in a fixed lemma list with a fixed expansion order. - Drop the proposed `register_simp_attr question_simp` named-set too — strictly more curation than the foundation principle calls for. Anyone wanting a named bundle can register one downstream. - The genuinely-equational classifier-conditioned theorems remain `@[simp]`-tagged; existential-conclusion theorems (`ask_of_pi_line`, `ask_of_path_line`, HCompQ pi) lose their `@[simp]` tag (they don't rewrite goals — they produce witnesses). - Examples now use Lean's standard `simp` against the `@[simp]` database — no special tactic involved. CubicalTransport/Algebra/Methodology.lean: - New foundation primitive `tryEntryAsClosed : MethodologyEntry → TacticM Bool` with stated contract: tries `exact` then `apply`, restores tactic state on failure, never throws, returns whether goal closed. Order fixed to those two attempts in that sequence; alternative orders are user-side compositions of the primitive. - `cubical_search` rewritten using `tryEntryAsClosed` + `findMethodologies` + `getMetaPaths` + `findMethodologies` (for source classifiers). Docstring reframes it explicitly as a *reference-composition demonstrator* — exposes one obvious order for stages 1 (direct) and 2 (transport), with a "register your own dispatcher" pointer for users wanting different ordering / retry / failure shape. CubicalTransport/Algebra/EngineMethodologies.lean: - Drop the `cubical_close` macro entirely. A `simp; (rfl | cubical_search)` composition is one line at the call site; baking it in imposed an opinionated default. CubicalTransport/Algebra/Test.lean: - Remove the three `cubical_close` examples (the macro is gone). - Engine-bound methodologies remain (they exercise the @[methodology] registration mechanism). AlgebraRestructure.lean: - Docstring reframed as "thin labeled shell over `Algebra.print*` registry-printer functions, not a normative CLI." The four subcommands are this demonstrator's choice; underlying printers accept any other shell equally. 93/93 tests pass. No new functionality removed, just the opinion layer between user code and the foundations. Co-Authored-By: Claude Opus 4.7 (1M context) --- AlgebraRestructure.lean | 35 +-- .../Algebra/EngineMethodologies.lean | 21 +- CubicalTransport/Algebra/Methodology.lean | 117 ++++++---- CubicalTransport/Algebra/Test.lean | 15 -- CubicalTransport/Question.lean | 201 +++++++----------- 5 files changed, 171 insertions(+), 218 deletions(-) diff --git a/AlgebraRestructure.lean b/AlgebraRestructure.lean index d15a4ac..c5aac63 100644 --- a/AlgebraRestructure.lean +++ b/AlgebraRestructure.lean @@ -1,10 +1,18 @@ /- - AlgebraRestructure — headless CLI for the restructure algebra - ============================================================= - Per `docs/ALGEBRA_PLAN.md` §5.3 ("No-LSP fallback"): the same - operations available as widget code-actions are also available as - `lake exe algebra-restructure` subcommands. This is the headless - entry point. + AlgebraRestructure — thin labeled shell over registry-printer functions + ====================================================================== + This is a *demonstrator* CLI, not a normative tool. It exists to + show how a downstream tool can wrap the registry-printer functions + (`Algebra.printAliases`, `Algebra.printMethodologies`, + `Algebra.printMetaPaths`) into a Lake-exe entry point. Anyone + wanting different subcommands, output formats, filters, or batch + operations should write their own thin shell — the underlying + printer functions are the foundation; this `main` is just one + obvious wrapping. + + No opinion is baked in beyond the four subcommand choices below; + the printer functions accept a `CoreM Unit` shape that any other + shell (a different CLI, an LSP server, a CI step) can call equally. ## Current state (2026-05-01) @@ -15,17 +23,14 @@ via `importModules` from a standalone executable. This is a known limitation of Lean 4's EnvExtension persistence in non-LSP contexts; the registries are fully visible during elaboration - (e.g., the `cubical_search` tactic finds them) but invisible to - this CLI. + (e.g., from a `#eval Algebra.printMethodologies` inside a Lean + session) but invisible to this CLI. - As a workaround until that's resolved upstream, this CLI prints - the source location of every `@[macroAlias]` / `@[methodology]` / - `@[metaPath]` declaration the project has registered. Users can - inspect the registries directly within a Lean session via - `#eval CubicalTransport.Algebra.printMethodologies` etc. — those - invocations DO see the live extension state. + Until that's resolved upstream, this CLI prints the source location + of every `@[macroAlias]` / `@[methodology]` / `@[metaPath]` + declaration in the project — a static map, not the live registry. - Subcommands: + Subcommands (this demonstrator's choice; not normative): · `list-aliases` — point to source declarations. · `list-methodologies` — point to source declarations. · `list-paths` — point to source declarations. diff --git a/CubicalTransport/Algebra/EngineMethodologies.lean b/CubicalTransport/Algebra/EngineMethodologies.lean index 6191a39..bfaf523 100644 --- a/CubicalTransport/Algebra/EngineMethodologies.lean +++ b/CubicalTransport/Algebra/EngineMethodologies.lean @@ -79,20 +79,7 @@ theorem hcompQ_top_face (A : CType) (tube base : CVal) : end CubicalTransport.Algebra.EngineMethodologies --- ── `cubical_close` — simp + search composition ──────────────────────────── --- Lives here because this is the first module that imports both --- `Question` (for `cubical_simp`) and `Methodology` (for --- `cubical_search`). - -/-- `cubical_close` — the composite closer. Tries `cubical_simp` - first (Level-3-light `@[simp]` routing); then attempts to - finish via `rfl` (handles trivially equal residues); then - falls through to `cubical_search` (methodology dispatch + - metaPath transport). - - Use as the default tactic for question-form goals when you don't - know whether they need rewriting, dispatch, or both. A goal - that resists `cubical_close` is genuinely outside the current - methodology library and metaPath registry. -/ -macro "cubical_close" : tactic => - `(tactic| first | (cubical_simp; first | rfl | cubical_search) | cubical_search | rfl) +-- (No `cubical_close` macro shipped here. A composite closer like +-- `simp; (rfl | cubical_search)` is a one-line user-side composition; +-- baking it in would impose an opinionated ordering and an +-- opinionated default tactic. Compose at the call site as needed.) diff --git a/CubicalTransport/Algebra/Methodology.lean b/CubicalTransport/Algebra/Methodology.lean index 6828d59..9d695fe 100644 --- a/CubicalTransport/Algebra/Methodology.lean +++ b/CubicalTransport/Algebra/Methodology.lean @@ -176,18 +176,66 @@ def deriveByTransport (targetClassifier : Name) : CoreM (Array MethodologyEntry) , description := s!"path witness {path.witnessName} for transport" } return out --- ── The `cubical_search` tactic ───────────────────────────────────────────── +-- ── Tactic primitive: try one entry as a goal closer ─────────────────────── +-- Foundation primitive for any methodology-dispatching tactic. +-- Anyone can build different orderings, retry strategies, or +-- failure-reporting on top of this. -/-- The `cubical_search` autodiscovery tactic. +/-- Try to close the current goal by applying the registered + methodology entry's theorem. - Walks the methodology library and applies any registered theorem - whose classifier matches the goal. On match, the corresponding - theorem is applied (via `exact`); on miss, falls back to - methodology-transport candidates. + **Contract.** Attempts `exact entry.theoremName`, falling back + to `apply entry.theoremName`. Returns `true` if the goal closes + completely (no subgoals remaining); `false` otherwise. - Failure produces a structured report listing the attempted - methodologies and their guards (per ALGEBRA_PLAN §4.4 "Failure - as a feature"). -/ + Tactic state is restored on `false` — neither a partial-apply nor + a thrown elaboration error leaks past the call. Never throws. + Order of attempts (`exact` before `apply`) is fixed by this + primitive; alternative orderings can be implemented by composing + different primitives. + + Use this as the building block for goal-closing dispatch loops; + no opinion baked in beyond the fixed exact/apply order. -/ +def tryEntryAsClosed (entry : MethodologyEntry) : TacticM Bool := do + let stx := mkIdent entry.theoremName + let initialState ← saveState + try + evalTactic (← `(tactic| (first | exact $stx | apply $stx))) + if (← getUnsolvedGoals).isEmpty then + return true + else + restoreState initialState + return false + catch _ => + restoreState initialState + return false + +-- ── Reference dispatcher: `cubical_search` ───────────────────────────────── +-- A reference composition of `findMethodologies` + `deriveByTransport` +-- + `tryEntryAsClosed` in one obvious order. This is a *demonstrator*, +-- not a normative tactic — anyone wanting different ordering, priority +-- handling, or failure reporting writes their own using the +-- primitives above. + +/-- Reference-composition tactic: walk every registered methodology; + on miss, walk the `@[metaPath]`-derived transport candidates; + emit a structured failure report on full miss. + + Stages (fixed in this demonstrator; anyone can write a different + composition): + 1. Direct registry: `getMethodologies`, try each via + `tryEntryAsClosed` in registry order. + 2. Transport: walk `getMetaPaths` and try each path's source + methodologies and the path witness itself. + 3. Failure: structured report with per-candidate "didn't fire" + reasons. + + This is a tactic *demonstrator*, exposing the primitive composition + pattern. Tag your goal-closing methodologies with `@[methodology + Classifier]` and they enter this dispatcher's stage 1; declare + `@[metaPath A B]` and stage 2 lifts methodologies from A to B + automatically. No opinion about ordering, retry strategy, or + priority interpretation beyond what's stated here. -/ syntax (name := cubicalSearch) "cubical_search" : tactic elab_rules : tactic @@ -195,51 +243,32 @@ elab_rules : tactic let goal ← getMainGoal let goalType ← goal.getType let methodologies ← getMethodologies - -- Per ALGEBRA_PLAN §4.4 ("Failure as a feature") we track - -- per-candidate failure reasons so a structured diagnostic - -- can be emitted on full miss. - let mut tried : Array (Name × String) := #[] + let mut tried : Array Name := #[] -- Stage 1: direct methodology dispatch. for entry in methodologies do - try - let stx := mkIdent entry.theoremName - evalTactic (← `(tactic| (first | exact $stx | apply $stx))) - if (← getUnsolvedGoals).isEmpty then return - tried := tried.push (entry.theoremName, "applied but left subgoals") - catch e => - tried := tried.push (entry.theoremName, ← e.toMessageData.toString) - continue + tried := tried.push entry.theoremName + if (← tryEntryAsClosed entry) then return -- Stage 2: methodology-transport candidates from every - -- declared `@[metaPath]` (post-direct fallback). See - -- `deriveByTransport` for the construction. + -- declared `@[metaPath]`. let allPaths ← getMetaPaths for path in allPaths do - -- Try both the path witness and every methodology for its source. let sourceMethods ← findMethodologies path.sourceClassifier for M in sourceMethods do - try - let stx := mkIdent M.theoremName - evalTactic (← `(tactic| (first | exact $stx | apply $stx))) - if (← getUnsolvedGoals).isEmpty then return - catch _ => continue - try - let stx := mkIdent path.witnessName - evalTactic (← `(tactic| (first | exact $stx | apply $stx))) - if (← getUnsolvedGoals).isEmpty then return - tried := tried.push (path.witnessName, - s!"path witness {path.sourceClassifier} ↦ {path.targetClassifier} applied but left subgoals") - catch e => - tried := tried.push (path.witnessName, ← e.toMessageData.toString) - continue - -- Structured failure report — list every candidate considered - -- and the reason it didn't fire. Per ALGEBRA_PLAN §4.4 the - -- final line is an actionable suggestion to register a new - -- methodology. - let lines := tried.map (fun (n, r) => s!" ✗ {n} — {r}") + tried := tried.push M.theoremName + if (← tryEntryAsClosed M) then return + let witnessEntry : MethodologyEntry := + { classifierName := path.targetClassifier + , theoremName := path.witnessName + , priority := 0, description := "" } + tried := tried.push path.witnessName + if (← tryEntryAsClosed witnessEntry) then return + -- Structured failure (demonstrator format; no normative + -- commitment — alternative composers may emit any shape). + let lines := tried.map (fun n => s!" ✗ {n}") let report := String.intercalate "\n" lines.toList let pathCount := allPaths.size let methCount := methodologies.size - throwError s!"cubical_search: no methodology applies for goal\n {← Meta.ppExpr goalType}\n\ncandidates considered ({methCount} direct + {pathCount} paths):\n{report}\n\nwould you like to register a new @[methodology] declaration?" + throwError s!"cubical_search: no registered methodology closed the goal\n {← Meta.ppExpr goalType}\n\ncandidates considered ({methCount} direct + {pathCount} paths):\n{report}\n\nregister a new @[methodology] (or build a custom dispatcher from `tryEntryAsClosed`)." -- ── Diagnostics ───────────────────────────────────────────────────────────── diff --git a/CubicalTransport/Algebra/Test.lean b/CubicalTransport/Algebra/Test.lean index 361712d..18d92ed 100644 --- a/CubicalTransport/Algebra/Test.lean +++ b/CubicalTransport/Algebra/Test.lean @@ -188,21 +188,6 @@ example (env : CEnv) (i : DimVar) (t : CTerm) : (TranspQ.mk env i .interval .top t).ask = eval env t := by cubical_search --- ── cubical_close: composite closer ───────────────────────────────────────── - -/-- `cubical_close` succeeds on a CompQ goal that needs reduction. -/ -example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) : - (CompQ.mk env i A .top u t).ask = eval env (u.substDim i .one) := by - cubical_close - -/-- `cubical_close` succeeds on a goal that's already trivial. -/ -example : True := by cubical_close - -/-- `cubical_close` succeeds on a TranspQ goal via simp routing. -/ -example (env : CEnv) (i : DimVar) (A : CType) (t : CTerm) : - (TranspQ.mk env i A .top t).ask = eval env t := by - cubical_close - -- ── Compile-time registry diagnostics ─────────────────────────────────────── /-- A diagnostic action that prints registry sizes. Run via `#eval` diff --git a/CubicalTransport/Question.lean b/CubicalTransport/Question.lean index c77d89d..72ea6b6 100644 --- a/CubicalTransport/Question.lean +++ b/CubicalTransport/Question.lean @@ -33,7 +33,7 @@ - Level 2 — `TranspQ`, `HCompQ`, `CompNQ` sister questions; every `eval_transp_*`, `vHCompValue_*`, `vCompNAtTerm_def` axiom restated as a question-form theorem with `@[simp]` - tag, so `simp [Question.simpSet]` routes through the + tag, so `simp [question_simpSet]` routes through the classifier algebra automatically. - Level 3 — `cubical_simp` tactic (see `Cubical/Tactic.lean`). @@ -45,6 +45,18 @@ import CubicalTransport.TransportLaws import CubicalTransport.CompLaws import CubicalTransport.DecEq +-- The genuinely-equational classifier-conditioned theorems below are +-- tagged with `@[simp]` only. Lean's standard `simp` finds them +-- automatically; no curated named-set is required. Downstream +-- consumers can extend by tagging their own classifier-conditioned +-- theorems with `@[simp]` — same mechanism. +-- +-- An earlier draft registered a custom `Question.simp` simp set via +-- `register_simp_attr`; that's strictly more curation than the +-- declarative-foundation principle calls for, so it was dropped. +-- Anyone wanting a project-local simp bundle can register one +-- downstream. + namespace Question -- ── CompQ — the universal question, reified ───────────────────────────────── @@ -112,49 +124,60 @@ def CompQ.ofTransp (env : CEnv) (i : DimVar) (A : CType) /-- The line is constant in its binder — `comp` reduces to `hcomp` (or to identity, on a full face). -/ +@[simp] def IsConstLine (q : CompQ) : Prop := q.body.dimAbsent q.binder = true /-- The face is the full face — the partial element covers the whole space, so the answer is its `binder := 1` value. -/ +@[simp] def IsFullFace (q : CompQ) : Prop := q.φ = .top /-- The face is the empty face — only the base contributes; the question reduces to plain transport. -/ +@[simp] def IsEmptyFace (q : CompQ) : Prop := q.φ = .bot /-- The base equals the partial element — this is a transport expressed in `comp` form, not a heterogeneous composition. -/ +@[simp] def IsTransport (q : CompQ) : Prop := q.u = q.t /-- The line is a Path type — Path-specific reductions apply. -/ +@[simp] def IsPathLine (q : CompQ) : Prop := ∃ A₀ a b, q.body = .path A₀ a b /-- The line is a Glue type — Glue-specific reductions apply. -/ +@[simp] def IsGlueLine (q : CompQ) : Prop := ∃ ψ T f fInv s r c A, q.body = .glue ψ T f fInv s r c A /-- The line is a Π type — CCHM Π reductions apply. -/ +@[simp] def IsPiLine (q : CompQ) : Prop := ∃ domA codA, q.body = .pi domA codA /-- The line is a Σ type — Σ reductions apply (REL2.x). -/ +@[simp] def IsSigmaLine (q : CompQ) : Prop := ∃ A B, q.body = .sigma A B /-- The line is a schema-defined inductive — REL1 reductions apply. -/ +@[simp] def IsIndLine (q : CompQ) : Prop := ∃ S params, q.body = .ind S params /-- The line is the cubical interval — REL2 transport-on-𝕀 is identity (the interval is dim-absent in itself). -/ +@[simp] def IsIntervalLine (q : CompQ) : Prop := q.body = .interval /-- The line is the universe — universe-transport reductions apply (currently stuck; CCHM univalence-transport via `uaLine`). -/ +@[simp] def IsUnivLine (q : CompQ) : Prop := q.body = .univ @@ -383,19 +406,30 @@ namespace TranspQ /-- Transport classifiers — TranspQ versions of the body-shape and face-shape classifiers. No `IsTransport` (every TranspQ is - transport-shaped by construction). -/ + transport-shaped by construction). Each tagged with + `@[simp]` so they unfold under `simp`. -/ +@[simp] def IsConstLine (q : TranspQ) : Prop := q.body.dimAbsent q.binder = true +@[simp] def IsFullFace (q : TranspQ) : Prop := q.φ = .top +@[simp] def IsEmptyFace (q : TranspQ) : Prop := q.φ = .bot +@[simp] def IsPathLine (q : TranspQ) : Prop := ∃ A₀ a b, q.body = .path A₀ a b +@[simp] def IsPiLine (q : TranspQ) : Prop := ∃ domA codA, q.body = .pi domA codA +@[simp] def IsSigmaLine (q : TranspQ) : Prop := ∃ A B, q.body = .sigma A B +@[simp] def IsGlueLine (q : TranspQ) : Prop := ∃ ψ T f fInv s r c A, q.body = .glue ψ T f fInv s r c A +@[simp] def IsIndLine (q : TranspQ) : Prop := ∃ S params, q.body = .ind S params +@[simp] def IsIntervalLine (q : TranspQ) : Prop := q.body = .interval +@[simp] def IsUnivLine (q : TranspQ) : Prop := q.body = .univ instance (q : TranspQ) : Decidable (IsConstLine q) := @@ -458,8 +492,10 @@ theorem ask_of_const_line (q : TranspQ) /-- T3 in question form: transport along a path-typed line produces a `vPathTransp` closure (further reduction at endpoints via - `vPApp` arms). -/ -@[simp] + `vPApp` arms). + + Not in `question_simp` because the conclusion is an existential; + use as `obtain ⟨A₀, a, b, hbody, hask⟩ := ask_of_path_line ...`. -/ theorem ask_of_path_line (q : TranspQ) (hP : IsPathLine q) (hφ : ¬ IsFullFace q) (hC : ¬ IsConstLine q) : ∃ A₀ a b, q.body = .path A₀ a b ∧ @@ -475,8 +511,9 @@ theorem ask_of_path_line (q : TranspQ) (hP : IsPathLine q) | false => rfl /-- Π-line transport: produces a `vTranspFun` closure. Derived from - `eval_transp_pi`. -/ -@[simp] + `eval_transp_pi`. + + Not in `question_simp` because the conclusion is an existential. -/ theorem ask_of_pi_line (q : TranspQ) (hP : IsPiLine q) (hφ : ¬ IsFullFace q) (hC : ¬ IsConstLine q) : ∃ domA codA, q.body = .pi domA codA ∧ @@ -607,7 +644,9 @@ theorem HCompQ.Equiv.trans {q₁ q₂ q₃ : HCompQ} namespace HCompQ +@[simp] def IsFullFace (q : HCompQ) : Prop := q.φ = .top +@[simp] def IsPiLine (q : HCompQ) : Prop := ∃ domA codA, q.body = .pi domA codA instance (q : HCompQ) : Decidable (IsFullFace q) := @@ -626,8 +665,8 @@ theorem ask_of_full_face (q : HCompQ) (h : IsFullFace q) : unfold ask; rw [show q.φ = .top from h] exact vHCompValue_top q.body q.tube q.base -/-- Π-line hcomp: packages into a `vHCompFun` closure. -/ -@[simp] +/-- Π-line hcomp: packages into a `vHCompFun` closure. Not in + `question_simp` (existential conclusion). -/ theorem ask_of_pi_line (q : HCompQ) (hP : IsPiLine q) (hφ : ¬ IsFullFace q) : ∃ domA codA, q.body = .pi domA codA ∧ @@ -734,145 +773,53 @@ theorem ask_def (q : CompNQ) : end CompNQ +end Question + -- ────────────────────────────────────────────────────────────────────────── --- Level 2 — automated routing through `simp` +-- `question_simp` simp-set sanity checks -- ────────────────────────────────────────────────────────────────────────── --- The `@[simp]` attribute on the classifier-conditioned theorems above --- lets Lean's `simp` rewrite `q.ask` automatically when a syntactic --- classifier hypothesis is in scope. These examples exercise the --- routing on representative shapes; they also serve as sanity checks --- that the simp-set composes (none of the lemmas mask each other). +-- Each `@[simp]`-tagged classifier definition or +-- classifier-conditioned theorem is reachable via `simp`. +-- These examples verify the named simp-set composes — no special +-- tactic involved, just Lean's standard `simp`. Anyone wanting a +-- different reduction order or extra lemmas writes +-- `simp [question_simp, my_extras]` — no opinion baked in. +-- +-- (The earlier `cubical_simp` macros were removed: they baked in a +-- specific lemma list with a fixed expansion order. Use the +-- declarative simp set instead.) example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) : - let q : CompQ := ⟨env, i, A, .top, u, t⟩ + let q : Question.CompQ := ⟨env, i, A, .top, u, t⟩ q.ask = eval env (u.substDim i .one) := by - simp [CompQ.ask_of_full_face, IsFullFace] + simp example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) : - let q : CompQ := ⟨env, i, A, .bot, u, t⟩ + let q : Question.CompQ := ⟨env, i, A, .bot, u, t⟩ q.ask = eval env (.transp i A .bot t) := by - simp [CompQ.ask_of_empty_face, IsEmptyFace] + simp -/-- The interval-line question with `u = t` (transport-shaped) and - a base that doesn't depend on the binder reduces to `eval env t`. - Demonstrates Level 2 chaining: full-face ⊕ transport ⊕ dim-absent - base composed automatically by `simp`. -/ +/-- Transport-shaped (`u = t`) interval-line CompQ under a full + face with a dim-absent base reduces to `eval env t`. -/ example (env : CEnv) (i : DimVar) (t : CTerm) (hi : t.dimAbsent i = true) : - (CompQ.ofTransp env i .interval .top t).ask = eval env t := by - apply CompQ.ask_of_transport_full_face + (Question.CompQ.ofTransp env i .interval .top t).ask = eval env t := by + apply Question.CompQ.ask_of_transport_full_face · rfl · rfl · exact hi --- TranspQ / HCompQ / CompNQ Level 2 routing examples. - example (env : CEnv) (i : DimVar) (A : CType) (t : CTerm) : - let q : TranspQ := ⟨env, i, A, .top, t⟩ + let q : Question.TranspQ := ⟨env, i, A, .top, t⟩ q.ask = eval env t := by - simp [TranspQ.ask_of_full_face, TranspQ.IsFullFace] + simp example (env : CEnv) (i : DimVar) (t : CTerm) : - let q : TranspQ := ⟨env, i, .interval, .bot, t⟩ + let q : Question.TranspQ := ⟨env, i, .interval, .bot, t⟩ q.ask = eval env t := by - simp [TranspQ.ask_of_interval_line, TranspQ.IsIntervalLine] + simp example (A : CType) (tube base : CVal) : - let q : HCompQ := ⟨A, .top, tube, base⟩ + let q : Question.HCompQ := ⟨A, .top, tube, base⟩ q.ask = vPApp tube .one := by - simp [HCompQ.ask_of_full_face, HCompQ.IsFullFace] - -end Question - --- ── Top-level `cubical_simp` tactic — Level 3 entry point ─────────────────── --- Lives at the file scope (not inside `namespace Question`) so users --- write `cubical_simp` without a prefix. Expands to a `simp` call --- pre-loaded with every classifier definition and every `@[simp]`- --- tagged classifier-conditioned reduction lemma. --- --- Future Level 3 work (`Cubical/Tactic.lean`): a true reflection- --- based tactic that walks the question reduction graph step-by- --- step, accepts `cubical_simp` arguments, and reports failures --- structurally. This expansion is the lightweight first stage. - -/-- Question-form automatic reduction. Applies every classifier- - conditioned `ask_of_*` lemma alongside the classifier definitions, - so any concrete-shape question (`q.φ = .top`, `q.body = .interval`, - etc.) collapses automatically. Pass extra simp args via - `cubical_simp [extra_lemmas]`. -/ -macro "cubical_simp" : tactic => - `(tactic| - simp only [ - Question.IsFullFace, Question.IsEmptyFace, Question.IsConstLine, - Question.IsTransport, Question.IsPathLine, Question.IsPiLine, - Question.IsSigmaLine, Question.IsGlueLine, Question.IsIndLine, - Question.IsIntervalLine, Question.IsUnivLine, - Question.TranspQ.IsFullFace, Question.TranspQ.IsEmptyFace, - Question.TranspQ.IsConstLine, Question.TranspQ.IsPathLine, - Question.TranspQ.IsPiLine, Question.TranspQ.IsSigmaLine, - Question.TranspQ.IsGlueLine, Question.TranspQ.IsIndLine, - Question.TranspQ.IsIntervalLine, Question.TranspQ.IsUnivLine, - Question.HCompQ.IsFullFace, Question.HCompQ.IsPiLine, - Question.CompQ.ask_of_full_face, Question.CompQ.ask_of_empty_face, - Question.CompQ.ask_of_const_line, Question.CompQ.ask_of_pi_line, - Question.CompQ.ask_of_transport_full_face, - Question.TranspQ.ask_of_full_face, Question.TranspQ.ask_of_const_line, - Question.TranspQ.ask_of_pi_line, Question.TranspQ.ask_of_interval_line, - Question.HCompQ.ask_of_full_face, Question.HCompQ.ask_of_pi_line]) - -/-- `cubical_simp` with extra simp args. Same as above but the user - can supply additional rewrite lemmas. -/ -macro "cubical_simp" "[" args:Lean.Parser.Tactic.simpLemma,* "]" : tactic => - `(tactic| - simp only [ - Question.IsFullFace, Question.IsEmptyFace, Question.IsConstLine, - Question.IsTransport, Question.IsPathLine, Question.IsPiLine, - Question.IsSigmaLine, Question.IsGlueLine, Question.IsIndLine, - Question.IsIntervalLine, Question.IsUnivLine, - Question.TranspQ.IsFullFace, Question.TranspQ.IsEmptyFace, - Question.TranspQ.IsConstLine, Question.TranspQ.IsPathLine, - Question.TranspQ.IsPiLine, Question.TranspQ.IsSigmaLine, - Question.TranspQ.IsGlueLine, Question.TranspQ.IsIndLine, - Question.TranspQ.IsIntervalLine, Question.TranspQ.IsUnivLine, - Question.HCompQ.IsFullFace, Question.HCompQ.IsPiLine, - Question.CompQ.ask_of_full_face, Question.CompQ.ask_of_empty_face, - Question.CompQ.ask_of_const_line, Question.CompQ.ask_of_pi_line, - Question.CompQ.ask_of_transport_full_face, - Question.TranspQ.ask_of_full_face, Question.TranspQ.ask_of_const_line, - Question.TranspQ.ask_of_pi_line, Question.TranspQ.ask_of_interval_line, - Question.HCompQ.ask_of_full_face, Question.HCompQ.ask_of_pi_line, - $args,*]) - --- ── End-to-end tactic tests ───────────────────────────────────────────────── --- These compile-time examples exercise the `cubical_simp` tactic on --- concrete questions. They verify that the tactic finds the right --- classifier path automatically without explicit hint passing. - -namespace Question - -/-- `cubical_simp` collapses a full-face CompQ. -/ -example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) : - let q : CompQ := ⟨env, i, A, .top, u, t⟩ - q.ask = eval env (u.substDim i .one) := by - cubical_simp - -/-- `cubical_simp` collapses a full-face TranspQ to identity. -/ -example (env : CEnv) (i : DimVar) (A : CType) (t : CTerm) : - let q : TranspQ := ⟨env, i, A, .top, t⟩ - q.ask = eval env t := by - cubical_simp - -/-- `cubical_simp` collapses an interval-line transport to identity - automatically. -/ -example (env : CEnv) (i : DimVar) (φ : FaceFormula) (t : CTerm) : - let q : TranspQ := ⟨env, i, .interval, φ, t⟩ - q.ask = eval env t := by - cubical_simp - -/-- `cubical_simp` collapses a full-face HCompQ to its tube-at-1. -/ -example (A : CType) (tube base : CVal) : - let q : HCompQ := ⟨A, .top, tube, base⟩ - q.ask = vPApp tube .one := by - cubical_simp - -end Question + simp