60f7ecdf54
Some checks are pending
Lean Action CI / build (push) Waiting to run
Phase D'.5 of ALGEBRA_PLAN.md and the §4.4 "Failure as a feature"
diagnostic. Closes the methodology-transport loop end-to-end.
CubicalTransport/Algebra/MetaPath.lean (NEW):
- MetaPathEntry: source classifier + target classifier + witness Name.
- metaPathRegistryExt: persistent EnvExtension storing declared paths.
- @[metaPath SourceClassifier TargetClassifier] attribute: tags a
declaration as a structural Path; the tagged decl serves as the
witness theorem.
- Lookup helpers: findPathsFromSource / findPathsToTarget.
- Diagnostic printer.
CubicalTransport/Algebra/Methodology.lean:
- deriveByTransport replaces its earlier stub. Walks the metaPath
registry; for each path A ↦ B and each methodology M registered
against A, derives a candidate against B (priority M.priority - 10)
plus a candidate using the path witness directly (priority - 20).
- cubical_search now collects per-candidate failure reasons and
emits a structured §4.4-shaped report:
"candidates considered (N direct + K paths):
✗ candidate1 — error1
✗ candidate2 — applied but left subgoals
would you like to register a new @[methodology] declaration?"
- Stage 1 (direct) and Stage 2 (transport) are exhausted in order;
on full miss, structured report fires.
CubicalTransport/Algebra/Test.lean:
- Phase D'.5 example: refl_path_to_true tagged @[metaPath
IsReflGoal IsTrueGoal] declares a structural Path.
- Engine-bound methodologies: compq_top_concrete (full-face CompQ),
transpq_top_concrete (full-face TranspQ), transpq_interval_concrete
(interval-line TranspQ). All discharge their classifier via rfl
(struct-projection-driven evaluation; no decide-on-free-vars
failure).
- Two end-to-end cubical_search examples exercise the dispatch on
concrete CompQ and TranspQ goals, succeeding via the engine-bound
methodologies.
CubicalTransport.lean: import the new MetaPath module.
93/93 tests pass. cubical_search now demonstrably closes both
trivial (True, Eq.refl, Iff.refl) and substantive (concrete
question-form equations) goals end-to-end.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
190 lines
8.1 KiB
Text
190 lines
8.1 KiB
Text
/-
|
||
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 CubicalTransport.Algebra.Methodology
|
||
import CubicalTransport.Algebra.MetaPath
|
||
import CubicalTransport.Question
|
||
|
||
namespace CubicalTransport.Algebra.Test
|
||
|
||
open CubicalTransport.Algebra
|
||
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
|
||
|
||
end CubicalTransport.Algebra.Test
|