Expand description
Structured Lean tactic-combinator tree — the proof-output substrate.
Auto-proofs are assembled today as raw first | (…) | (…) | sorry STRINGS
(AutoProof.proof_lines). Every rung KNOWS its portfolio of alternatives,
then immediately flattens it to a string — which forces any later
proof-output pass (--minimize, marker instrumentation, --explain) to
re-parse the multi-line, nested Lean it just produced. That round-trip is
the brittleness.
This thin tree keeps the CONTROL structure — sequencing, first
alternation, induction arms — first-class. Leaves stay opaque tactic text
(simp only […] <;> omega, grind […]; done, exact …): we model how a
proof is assembled, not Lean’s tactic semantics. With the structure
retained, --minimize collapses a Tactic::First to its winning branch
STRUCTURALLY (pick a child, re-print), never by text surgery; the only thing
that still has to consult Lean is which branch won — and that is one
instrumented lake build, not a parser.
Modules§
- minimize
- The
--minimizedriver state, thread-local so the two re-emit passes (instrument, then collapse) can steerTactic::render_bodywithout threading a mode + counter through every codegen signature. Codegen runs single-threaded pertranspile, and a normalaver proofnever enters a pass, so the default ([Mode::Off]) leaves emission untouched. - speculative
- The speculative-universal driver state — the “try-universal,
fall-back-to-sampled” mechanism for SINGLE-LIST conditional laws (the Gap-1
statement-form decision layer; analog of
minimizebut choosing the theorem’s STATEMENT FORM, not collapsing a tactic portfolio).
Structs§
- Induction
Arm - One
| <pattern> => <body>arm of anTactic::Induction.
Enums§
- Tactic
- A Lean tactic, modelled at the control level only.