From d03746497bcbb538e6722433401f4fe36716f1b2 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Fri, 1 May 2026 07:52:59 -0600 Subject: [PATCH] Drop Infoductor dependency; cubical-transport is now pure cubical engine MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The cubical-flavored methodology bindings move out of cubical- transport-hott-lean4 into a new private bridge repo `infoductor-cubical` (separate next commit on that repo). Files removed (moved to infoductor-cubical): - CubicalTransport/Algebra/EngineMethodologies.lean - CubicalTransport/Algebra/Test.lean - (CubicalTransport/Algebra/ directory now empty, removed.) Files modified: - CubicalTransport.lean: drop the 8 Infoductor + Algebra imports. - CubicalTransport/FFITest.lean: drop `import Infoductor.Foundation .Restructure` + `open Infoductor` + the 4 Infoductor.Foundation smoke tests (they belong in the bridge repo, not in the engine). - lakefile.toml: drop the `[[require]] infoductor` block. Architecture rationale: - Public Infoductor: Foundation + Comonad — generic Lean 4 repo- organization primitives, Mathlib-only-when-needed. - Public cubical-transport-hott-lean4: pure cubical engine, no Infoductor dep, no methodology bindings. - Private infoductor-cubical (next): bridges Infoductor.Foundation + cubical-transport into a "Cubical" methodology surface for Infoductor. Test count: 47 → 43 smoke (the 4 Algebra smokes leave with the moved files). 46/46 properties. Total 89/89 passing. 46 build jobs (was 53 with Infoductor pulled in). Co-Authored-By: Claude Opus 4.7 (1M context) --- CubicalTransport.lean | 8 - .../Algebra/EngineMethodologies.lean | 85 -------- CubicalTransport/Algebra/Test.lean | 206 ------------------ CubicalTransport/FFITest.lean | 42 +--- lake-manifest.json | 12 +- lakefile.toml | 14 +- 6 files changed, 13 insertions(+), 354 deletions(-) delete mode 100644 CubicalTransport/Algebra/EngineMethodologies.lean delete mode 100644 CubicalTransport/Algebra/Test.lean diff --git a/CubicalTransport.lean b/CubicalTransport.lean index 2a7f342..8eaf001 100644 --- a/CubicalTransport.lean +++ b/CubicalTransport.lean @@ -23,12 +23,4 @@ import CubicalTransport.Soundness import CubicalTransport.Inductive import CubicalTransport.Bridge import CubicalTransport.Question -import Infoductor.Foundation.Meta -import Infoductor.Foundation.Edit -import Infoductor.Foundation.Restructure -import Infoductor.Foundation.MacroAlias -import Infoductor.Foundation.MetaPath -import Infoductor.Foundation.Methodology -import CubicalTransport.Algebra.EngineMethodologies -import CubicalTransport.Algebra.Test import CubicalTransport.PropertyTest diff --git a/CubicalTransport/Algebra/EngineMethodologies.lean b/CubicalTransport/Algebra/EngineMethodologies.lean deleted file mode 100644 index a7884bc..0000000 --- a/CubicalTransport/Algebra/EngineMethodologies.lean +++ /dev/null @@ -1,85 +0,0 @@ -/- - 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 Infoductor.Foundation.Methodology -import CubicalTransport.Question - -namespace CubicalTransport.Algebra.EngineMethodologies - -open Infoductor -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 - --- (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/Test.lean b/CubicalTransport/Algebra/Test.lean deleted file mode 100644 index 96528b4..0000000 --- a/CubicalTransport/Algebra/Test.lean +++ /dev/null @@ -1,206 +0,0 @@ -/- - CubicalTransport.Algebra.Test — end-to-end tests - ================================================ - Exercises the Phase A–D' Algebra layer at compile time: - - - Phase A: construct meta-mirror values; verify decidable - equality. - - Phase B: build an `Edit Unit` value via `restructure` and check - `selfConsistent`; run the headless interpreter. - - Phase C: register an alias via `@[macroAlias]` and verify it - appears in the registry. - - Phase D': register a methodology via `@[methodology]` and verify - `cubical_search` finds it on a representative goal. - - These are compile-time correctness tests; the runtime smoke tests - live in `FFITest.lean`. --/ - -import Infoductor.Foundation.Methodology -import Infoductor.Foundation.MetaPath -import CubicalTransport.Algebra.EngineMethodologies -import CubicalTransport.Question - -namespace CubicalTransport.Algebra.Test - -open Infoductor -open Question - --- ── Phase A: meta-mirror types ───────────────────────────────────────────── - -/-- Meta-mirror types are inhabited and well-formed. -/ -example : MetaCType := .theorem_ -example : MetaCType := .file -example : MetaCType := .classifierSet - -example : MetaClassifier := .always -example : MetaClassifier := .never -example : MetaClassifier := .meet (.atDecl `Foo) (.inFile "Bar.lean") - -example : MetaArtifact := .source "def x := 1" -example : MetaArtifact := .empty -example : MetaArtifact := .refTo `Existing - -example : MetaPosition := - { declName := `Test, filePath := "Test.lean", range := none } - -/-- DecidableEq fires correctly on MetaClassifier. -/ -example : decide (MetaClassifier.always = .always) = true := by decide -example : decide (MetaClassifier.always = .never) = false := by decide -example : decide ((.meet .always (.atDecl `Foo) : MetaClassifier) = - (.meet .always (.atDecl `Foo))) = true := by decide - --- ── Phase B: Edit + Context + restructure ─────────────────────────────────── - -/-- A simple restructure call produces an Edit with one op. -/ -example : - let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none } - let e := restructure pos .theorem_ .always (.source "def x := 1") .empty - e.ops.length = 1 := by - rfl - -/-- The restructure picks `witness` when the classifier is `.always`. -/ -example : - let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none } - let e := restructure pos .theorem_ .always (.source "yes") (.source "no") - (e.ops.head?).isSome = true := by - rfl - -/-- The restructure picks `fallback` when the classifier is `.never`. -/ -example : - let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none } - let e := restructure pos .theorem_ .never (.source "yes") (.source "no") - (e.ops.head?).isSome = true := by - rfl - -/-- Self-consistency check on a single restructure op. -/ -example : - let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none } - let e := restructure pos .theorem_ .always (.source "x") .empty - e.selfConsistent = true := by - rfl - -/-- A batch that removes a decl AND references it by `refTo` is - flagged as inconsistent. -/ -example : - let pos₁ : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none } - let pos₂ : MetaPosition := { declName := `Bar, filePath := "F.lean", range := none } - let e : Edit Unit := do - restructure pos₁ .theorem_ .always .empty .empty -- removes Foo - restructure pos₂ .theorem_ .always (.refTo `Foo) .empty -- refs Foo - e.selfConsistent = false := by - rfl - --- ── Frozen aliases ────────────────────────────────────────────────────────── - -/-- The `transport_artifact` alias produces a single Edit op. -/ -example : - let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none } - let e := transport_artifact pos .theorem_ (.source "x") - e.ops.length = 1 := by rfl - -/-- The `materialize` alias emits raw Lean source. -/ -example : - let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none } - let e := materialize pos .theorem_ "theorem x : True := trivial" - e.ops.length = 1 := by rfl - --- ── Phase C: @[macroAlias] registration ───────────────────────────────────── - -/-- A custom alias for testing. Registered via the attribute below. -/ -@[macroAlias] -def custom_alias_test (i : MetaPosition) : Edit Unit := - restructure i .definition .always (.source "test") .empty - --- ── Phase D': @[methodology] registration ─────────────────────────────────── - -/-- A trivial methodology: solves `True` goals. Registered against - a placeholder classifier name `IsTrueGoal`. -/ -@[methodology IsTrueGoal] -theorem trueMethodology : True := True.intro - -/-- `cubical_search` finds the registered methodology for `True` - goals. Demonstrates the dispatch loop end-to-end. -/ -example : True := by cubical_search - -/-- Methodology for `Eq.refl`-shaped goals. Lean's `rfl` tactic - handles these natively — registering as a methodology - demonstrates that `cubical_search` can dispatch to non-trivial - universe-equality goals. -/ -@[methodology IsReflGoal] -theorem reflMethodologyNat (n : Nat) : n = n := rfl - -example : 7 = 7 := by cubical_search - --- ── Phase D'.5: @[metaPath] + methodology-transport ───────────────────────── - -/-- A trivial structural Path: every reflexivity goal is also a - "trivial-truth" goal. This declares the meta-Path so - methodology-transport can lift `IsTrueGoal` methodologies onto - `IsReflGoal` targets and vice versa. -/ -@[metaPath IsReflGoal IsTrueGoal] -theorem refl_path_to_true (n : Nat) (_ : n = n) : True := True.intro - -/-- An identity methodology that closes any `Iff.refl`-shaped goal. -/ -@[methodology IsIffReflGoal] -theorem iffRefl (P : Prop) : P ↔ P := Iff.rfl - -example : True ↔ True := by cubical_search - --- ── Engine-bound methodologies — concrete CompQ closers ───────────────────── --- These register classifier-conditioned engine theorems as --- `cubical_search`-applicable methodologies. Each one fully --- discharges its classifier via `decide` (since the classifier --- predicates are Decidable for concrete `.top`/`.bot`/`.interval` --- shapes), turning a hypothesis-bearing simp lemma into a stand- --- alone closer. - -/-- Closing methodology for full-face CompQ: literal `.top` face - questions reduce to `eval env (u.substDim i .one)`. Discharges - `IsFullFace` via `rfl` (`.top = .top` after struct projection). -/ -@[methodology IsCompQFullFace] -theorem compq_top_concrete (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 - -/-- Closing methodology for full-face TranspQ: literal `.top` face - transports reduce to identity. -/ -@[methodology IsTranspQFullFace] -theorem transpq_top_concrete (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 - -/-- Closing methodology for interval-line TranspQ: any face on - `.interval` reduces to identity. -/ -@[methodology IsTranspQInterval] -theorem transpq_interval_concrete (env : CEnv) (i : DimVar) - (φ : FaceFormula) (t : CTerm) : - (TranspQ.mk env i .interval φ t).ask = eval env t := - TranspQ.ask_of_interval_line _ rfl - -/-- `cubical_search` on a concrete CompQ full-face goal. -/ -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_search - -/-- `cubical_search` on a concrete TranspQ interval-line goal. -/ -example (env : CEnv) (i : DimVar) (t : CTerm) : - (TranspQ.mk env i .interval .top t).ask = eval env t := by - cubical_search - --- ── Compile-time registry diagnostics ─────────────────────────────────────── - -/-- A diagnostic action that prints registry sizes. Run via `#eval` - inside a Lean session to verify that @[methodology] / - @[macroAlias] / @[metaPath] declarations have populated the - EnvExtensions. This is the live way to inspect the registries - (the standalone CLI in `AlgebraRestructure.lean` cannot — see - its docstring for the Lean 4 EnvExtension limitation). -/ -def printRegistrySizes : Lean.CoreM Unit := do - let aliases ← getAliases - let methodologies ← getMethodologies - let paths ← getMetaPaths - IO.println s!"[Algebra.Test] aliases={aliases.size} \ - methodologies={methodologies.size} paths={paths.size}" - -end CubicalTransport.Algebra.Test diff --git a/CubicalTransport/FFITest.lean b/CubicalTransport/FFITest.lean index ccc7efb..075a7a4 100644 --- a/CubicalTransport/FFITest.lean +++ b/CubicalTransport/FFITest.lean @@ -23,13 +23,11 @@ import CubicalTransport.FFI import CubicalTransport.Inductive import CubicalTransport.Bridge import CubicalTransport.Question -import Infoductor.Foundation.Restructure open CubicalTransport.Inductive open CubicalTransport.Inductive.CTerm open CubicalTransport.Bridge open Question -open Infoductor namespace CubicalTransportFFITest @@ -272,41 +270,11 @@ def tests : List (String × String × String) := { env := .nil, binder := ⟨"i"⟩, body := .univ , φ := .top, u := .var "u", t := .var "t" } then "yes" else "no"), - "no"), - -- Algebra Phase B: restructure produces Edit ops - ("Algebra: restructure with .always emits 1 op", - (let pos : MetaPosition := - { declName := `Foo, filePath := "F.lean", range := none } - let e := restructure pos .theorem_ .always - (.source "yes") (.source "no") - toString e.ops.length), - "1"), - ("Algebra: restructure with .never picks fallback", - (let pos : MetaPosition := - { declName := `Foo, filePath := "F.lean", range := none } - let e := restructure pos .theorem_ .never - (.source "yes") (.source "no") - match e.ops.head? with - | some op => op.newContent.toString - | none => ""), - "source(no)"), - ("Algebra: brokenRefs flags removed-but-referenced batch", - (let pos₁ : MetaPosition := - { declName := `Foo, filePath := "F.lean", range := none } - let pos₂ : MetaPosition := - { declName := `Bar, filePath := "F.lean", range := none } - let e : Edit Unit := do - restructure pos₁ .theorem_ .always .empty .empty - restructure pos₂ .theorem_ .always (.refTo `Foo) .empty - if e.selfConsistent then "consistent" else "broken"), - "broken"), - ("Algebra: MetaClassifier.atPosition meet/join lattice", - (let p : MetaPosition := - { declName := `Foo, filePath := "F.lean", range := none } - let φ : MetaClassifier := .meet (.atDecl `Foo) (.inFile "F.lean") - let ψ : MetaClassifier := .join .never (.atDecl `Foo) - s!"{φ.atPosition p}/{ψ.atPosition p}"), - "true/true") ] + "no") ] +-- Note: Algebra/Infoductor smoke tests moved to the +-- `infoductor-cubical` bridge repo (private), where the Infoductor +-- dependency now lives. cubical-transport-hott-lean4 has no +-- Infoductor dep — pure cubical engine. /-- Run every smoke test, print its actual vs expected. Returns the number of failures. -/ diff --git a/lake-manifest.json b/lake-manifest.json index a89b720..fefa3dc 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,16 +1,6 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", - "packages": - [{"url": "https://maxgit.wg/max/infoductor.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "ba0a49823bf33adca771365f03db6a757f318b0a", - "name": "infoductor", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": false, - "configFile": "lakefile.toml"}], + "packages": [], "name": "cubicalTransport", "lakeDir": ".lake", "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml index cffe311..d1e4a44 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -2,13 +2,13 @@ name = "cubicalTransport" version = "0.1.0" defaultTargets = ["cubical-test"] -# Generic methodology / repo-organization machinery — registries, -# restructure operation, Edit/Context monad-comonad pair, attribute -# infrastructure — extracted to its own repo on 2026-05-01. -[[require]] -name = "infoductor" -git = "https://maxgit.wg/max/infoductor.git" -rev = "master" +# cubical-transport-hott-lean4 is the pure cubical engine. Its +# previous Infoductor.Foundation dependency (which bridged +# methodology / restructure machinery into the cubical engine) was +# moved into the private bridge repo `infoductor-cubical` on +# 2026-05-01. This repo no longer depends on Infoductor — it is +# exclusively the cubical engine and exists to be `require`d by +# downstream projects (paideia, topolei, infoductor-cubical, …). [[lean_lib]] name = "CubicalTransport"