Optimize PDL proof search and tableau measures

[Vilin97]

PDL was chosen as a large, completed target with 52 modules and repeated broad automation in interpolation, local tableau rules, and path/measure arguments. Those proof bodies offered concrete optimization opportunities while leaving its public import graph and definitions intact. PDL repeatedly reconstructs finite-set membership, tableau paths, and natural-number measure facts with broad automation. Use direct witnesses and existing lemmas for those steps, and restrict proof search and local simplification contexts to the facts each proof uses.

The selected completed project is LeanPool/PDL (52 owned modules). The audited base is 6cce96e685eab8843a5ee5de170cf28313d31fbe and the measured head is 3a4036061f4509778d7d2b7487c9eb7da222fe59. Main was verified immediately before commit at 2fc3a737eb236f260197b4ef2e296d5f076ca728; its selected project, dependency, policy, and pin inputs match the audited base. The original base was retained under the native-queue policy. The unchanged repository pins are Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e.

• Build modal interpolant membership and contradiction arguments directly with Finset lemmas.
• Compose witnesses in Qsteps_append and localTableauTruth, use path-structural induction for PathIn.elem_allPaths, and transport histories directly along tableau edges.
• Use omega and a direct successor inequality for eligible natural-number arguments. Existing arithmetic steps are retained where a different certificate would remove an old generated helper.
• Restrict grind and Aesop searches and remove unused large hypotheses inside local box/model-graph arguments. The public import graph is preserved; lake shake was investigated with public imports retained.

Before the first edit, Lean environment inspection recorded every project-owned declaration, including private helpers, generated matchers, and recursive auxiliary definitions: 9,423 module records and 9,416 distinct names. The baseline manifest SHA-256 is 9a1bb5498cf51e6c21e3f6b8fa0dd53af4b9177d4206bf2ba507d9d7ff06949d.

The audit compares complete elaborated types, universes, binder order/implicitness, names, safety, mutual membership, all definition/opaque values and reducibility hints, and inductive/constructor/recursor metadata. Only theorem proof values are exempt. All 9,423 old records remain present and compare identically after omitting nonsemantic source metadata and applying Name.eraseMacroScopes only to bound lambda/forall/let names. Ordinary binder names, constant names, and universe names are retained; there is no expression reduction or logical-equivalence comparison. All old definition values also match the raw manifest structurally. The 52 raw type differences are bound hygienic identifiers in generated helpers (including PDL.Q_then_relate._mutual). Source declaration signatures are unchanged. There are 34 additional private proof helpers. All 52 audited source Git blobs match this committed head.

Measurement uses isolated base/head worktrees, removes only PDL build artifacts, retains identical prebuilt pinned dependencies, and runs LEAN_NUM_THREADS=4 lake build --wfail LeanPool.PDL.Imports in base/head/head/base/base/head order. GNU time records wall time, child CPU, and maximum compiler-process RSS. Every completed sample is included:

Sample order	Revision	Wall (s)	User + system CPU (s)	Peak compiler RSS (KiB)
1	base 1	174.44	362.61	1,248,700
2	head 1	193.69	348.65	1,241,400
3	head 2	204.60	355.36	1,249,968
4	base 2	228.36	390.93	1,250,172
5	base 3	229.16	385.76	1,246,620
6	head 3	198.71	351.45	1,248,096

Three-run median	Base	Head	Reduction
Wall time	228.36 s	198.71 s	12.98%
User + system CPU	385.76 s	351.45 s	8.89%
Peak compiler RSS	1,248,700 KiB	1,248,096 KiB	0.05%

The observed median meets the 10% stopping criterion.

Validation passed: the warning-free target build; Mathlib declaration linters over all 52 modules; lake exe lint-style LeanPool.PDL.Imports; lake exe mk_all --module --check; repository header, forbidden-text, file/proof-size, project-card, Lake/style-option, axiom-closure, and option-backdoor audits; dependency pin checks; and git diff --check. The lint command was LEAN_NUM_THREADS=4 lake env lean --run scripts/ci/lint-project.lean with the complete 52-module list. The quality/trust run invoked unchanged repository checker functions scoped to all owned PDL files and its card.

The VM is heavily shared, so wall time varies substantially. Peak RSS measures one compiler process; aggregate build memory was not measured. Standalone synchronous profiles are advisory: a Local.Rules variant exceeded the unchanged default heartbeat limit, and that failed timing was excluded. Normal project builds and all required local checks passed. This PR is submitted for review; this task requests no merge or auto-merge.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low impact] No actionable defect was found in this proof-only refactor.

Summary

This PR narrows proof search across 32 existing PDL modules without changing source declaration signatures or the public import graph.

• Modal interpolation proofs build membership arguments directly.
• Tableau and program paths follow their structure to compose proofs.
• Local tableau proofs compose rule children with their end nodes.
• Measure proofs use direct natural-number bounds and successor steps.
• PDL proof searches use fewer default rules and fewer unrelated facts.

Validation limits: builds, timing samples, and the complete elaborated-declaration audit were not rerun. External source and license evidence were not independently reverified; this PR leaves the project card and attribution unchanged.

Acknowledged limitation: Vilin97 states that the shared VM causes substantial wall-time variation, aggregate build memory was not measured, and a failed standalone profile was excluded from advisory timing.

_{Reviews (1) · Last reviewed commit: "Limit PDL box proof search to relevant f..." · Reviewed by Greptile}

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: 3a4036061f4509778d7d2b7487c9eb7da222fe59

Verdict: ✅ approve

The refactor narrows automation across 32 PDL modules and replaces selected searches with explicit witnesses, structural induction, and direct history transport. Existing case analysis, intermediate claims, and reusable helpers remain intact; the rewritten arguments expose their dependencies more clearly. I found no actionable maintenance regression. A targeted Lean check stopped at missing Mathlib imports, so builds and the reported speedup were not independently verified.

Aspect	Value
Scope	proof and tactic rewrites
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

Explicit proof steps and narrower searches improve maintainability without introducing actionable technical debt.

---

Tokens: 1,876,369 in / 8,413 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $7.6317 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

{
"summary": "At 3a40360, the PDL refactor narrows Aesop/Grind search and replaces inferred membership, path and history arguments with explicit witnesses. Qsteps_append now exposes composition directly, localTableauTruth carries the child/leaf witnesses in both directions, and PathIn.elem_allPaths follows the path constructors. These changes make the argument easier to follow without an observed API or import change. The author's reported 12.98% median wall-time reduction is advisory; I did not rerun the benchmark or independently reproduce the compiled declaration manifest.",
"assessment": {
"scope": "proof-search and tableau-measure refactor",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "The complete 32-file proof refactor improves local reasoning and constrains automation without a source-level compatibility concern."
},
"verdict": "approve",
"findings": []
}