From 333f31d4bc426dfb549f9551b2382885ad805da2 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Fri, 1 May 2026 01:06:04 -0600 Subject: [PATCH] =?UTF-8?q?EngineMethodologies=20+=20cubical=5Fclose:=20AL?= =?UTF-8?q?GEBRA=20=C2=A79=20closer=20set?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Phase D'.6 — closes the "every existing theorem has a methodology" criterion from ALGEBRA_PLAN.md §9 for the auto-discharging set (@[simp]-tagged closers whose classifier hypotheses reduce to struct-projection rfl). CubicalTransport/Algebra/EngineMethodologies.lean (NEW): - @[methodology IsCompQTopFace] compQ_top_face - @[methodology IsCompQBotFace] compQ_bot_face - @[methodology IsTranspQTopFace] transpQ_top_face - @[methodology IsTranspQIntervalLine] transpQ_interval_line - @[methodology IsHCompQTopFace] hcompQ_top_face Each registration is a closing-form theorem: it takes the relevant field tuple of the question and asserts equality to the expected reduced form, with the classifier hypothesis discharged inline by `rfl`. Together with the methodologies in `Algebra/Test.lean` (`trueMethodology`, `reflMethodologyNat`, `iffRefl`, `compq_top_concrete`, `transpq_top_concrete`, `transpq_interval_concrete`), the registry now covers the auto-discharging core engine theorems. `cubical_close` macro (in EngineMethodologies.lean): cubical_simp; (rfl | cubical_search) — fall-through composition. First reduces the goal via @[simp] routing; then closes any trivial residue via rfl; then dispatches via the methodology library. The "default tactic" for question-form goals. Three new end-to-end tests in Algebra/Test.lean exercising cubical_close on full-face CompQ, trivial True, and full-face TranspQ goals. Methodologies still pending @[methodology] tagging (need richer dispatch for non-trivial classifier conjunctions or Glue/Path specialisations, scheduled REL2.6+): - ask_of_const_line (needs ¬IsFullFace ∧ ¬IsEmptyFace ∧ IsConstLine conjunction; currently covered by cubical_simp's simp-routing). - ask_of_pi_line, ask_of_path_line, ask_of_stuck. - The 9 Glue-transport face-disjoint variants. Co-Authored-By: Claude Opus 4.7 (1M context) --- CubicalTransport.lean | 1 + .../Algebra/EngineMethodologies.lean | 98 +++++++++++++++++++ CubicalTransport/Algebra/Test.lean | 16 +++ 3 files changed, 115 insertions(+) create mode 100644 CubicalTransport/Algebra/EngineMethodologies.lean diff --git a/CubicalTransport.lean b/CubicalTransport.lean index d0db845..4bc4c2b 100644 --- a/CubicalTransport.lean +++ b/CubicalTransport.lean @@ -29,5 +29,6 @@ import CubicalTransport.Algebra.Restructure import CubicalTransport.Algebra.MacroAlias import CubicalTransport.Algebra.MetaPath import CubicalTransport.Algebra.Methodology +import CubicalTransport.Algebra.EngineMethodologies import CubicalTransport.Algebra.Test import CubicalTransport.PropertyTest diff --git a/CubicalTransport/Algebra/EngineMethodologies.lean b/CubicalTransport/Algebra/EngineMethodologies.lean new file mode 100644 index 0000000..6191a39 --- /dev/null +++ b/CubicalTransport/Algebra/EngineMethodologies.lean @@ -0,0 +1,98 @@ +/- + CubicalTransport.Algebra.EngineMethodologies + ============================================ + Engine-bound methodology registrations. Per ALGEBRA_PLAN.md §9: + + > Every existing `eval_*` / `vTransp_*` / `vCompValue_*` / Glue / + > Soundness theorem has at least one corresponding `@[methodology]` + > registration that closes its representative question via + > `cubical_search`. + + Each registration here is a *closing form* — a theorem that closes + a concrete-shape question goal directly, with its classifier + hypothesis discharged automatically (typically by `rfl` after + struct projection). This turns a hypothesis-bearing simp lemma + (`ask_of_full_face`) into a `cubical_search`-applicable closer + (`compq_top_concrete`). + + Goals targeted: + - Full-face / empty-face / interval-line questions (all three + question shapes: CompQ, TranspQ, HCompQ). + - hcomp on `.pi` and on `.top` — closing forms with concrete body. + + Out of scope here: + - Methodologies requiring non-trivial classifier discharge + (e.g., `ask_of_const_line` wants `¬IsFullFace ∧ ¬IsEmptyFace ∧ + IsConstLine`). These would need a richer dispatch tactic; for + now `cubical_simp` covers them via the simp-routing path. + - Methodologies depending on Glue / Path body shape. The Glue + transport axioms have ~10 face-disjoint cases that each need + their own concrete closers; they land in a follow-up. +-/ + +import CubicalTransport.Algebra.Methodology +import CubicalTransport.Question + +namespace CubicalTransport.Algebra.EngineMethodologies + +open CubicalTransport.Algebra +open Question + +-- ── CompQ closers ─────────────────────────────────────────────────────────── + +/-- C1 closer: literal `.top` face on a CompQ → `eval env (u.substDim + binder .one)`. Classifier discharged by struct-projection rfl. -/ +@[methodology IsCompQTopFace] +theorem compQ_top_face (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) : + (CompQ.mk env i A .top u t).ask = eval env (u.substDim i .one) := + CompQ.ask_of_full_face _ rfl + +/-- C2 closer: literal `.bot` face on a CompQ → `eval env (.transp + binder body .bot t)`. -/ +@[methodology IsCompQBotFace] +theorem compQ_bot_face (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) : + (CompQ.mk env i A .bot u t).ask = eval env (.transp i A .bot t) := + CompQ.ask_of_empty_face _ rfl + +-- ── TranspQ closers ───────────────────────────────────────────────────────── + +/-- T1 closer: literal `.top` face on a TranspQ → identity. -/ +@[methodology IsTranspQTopFace] +theorem transpQ_top_face (env : CEnv) (i : DimVar) (A : CType) (t : CTerm) : + (TranspQ.mk env i A .top t).ask = eval env t := + TranspQ.ask_of_full_face _ rfl + +/-- T2 specialisation: any face on `.interval` → identity. -/ +@[methodology IsTranspQIntervalLine] +theorem transpQ_interval_line (env : CEnv) (i : DimVar) + (φ : FaceFormula) (t : CTerm) : + (TranspQ.mk env i .interval φ t).ask = eval env t := + TranspQ.ask_of_interval_line _ rfl + +-- ── HCompQ closers ────────────────────────────────────────────────────────── + +/-- HCompQ full-face closer: `vPApp tube .one`. -/ +@[methodology IsHCompQTopFace] +theorem hcompQ_top_face (A : CType) (tube base : CVal) : + (HCompQ.mk A .top tube base).ask = vPApp tube .one := + HCompQ.ask_of_full_face _ rfl + +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) diff --git a/CubicalTransport/Algebra/Test.lean b/CubicalTransport/Algebra/Test.lean index a2fb962..c1087ea 100644 --- a/CubicalTransport/Algebra/Test.lean +++ b/CubicalTransport/Algebra/Test.lean @@ -18,6 +18,7 @@ import CubicalTransport.Algebra.Methodology import CubicalTransport.Algebra.MetaPath +import CubicalTransport.Algebra.EngineMethodologies import CubicalTransport.Question namespace CubicalTransport.Algebra.Test @@ -187,4 +188,19 @@ 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 + end CubicalTransport.Algebra.Test