Drop Infoductor dependency; cubical-transport is now pure cubical engine
Some checks failed
Lean Action CI / build (push) Has been cancelled
Some checks failed
Lean Action CI / build (push) Has been cancelled
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) <noreply@anthropic.com>
This commit is contained in:
Maximus Gorog
parent
e26ada2fbc
commit
d03746497b
6 changed files with 13 additions and 354 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.)
|
||||
|
|
@ -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
|
||||
|
|
@ -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 => "<no ops>"),
|
||||
"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. -/
|
||||
|
|
|
|||
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue