feat: lp tactic, parametric witnesses via symbolic QE (deferred)

[kim-em]

Deferred future work — tracks the parametric-witness fragment that v1 (Stages 1–4a) explicitly does not handle.

Problem statement

Goals of the form

example (a : Rat) : ∃ x : Rat, x = a                                 -- witness x := a
example (a : Rat) (ha : 0 ≤ a) : ∃ x : Rat, a ≤ x ∧ x ≤ a + 1        -- witness x := a
example (a : Rat) (ha : 0 ≤ a) :
    ∃ x : Rat, ∀ y : Rat, 0 ≤ y → y ≤ a → y ≤ x                      -- witness x := a

are all one-line Lean proofs using a parametric witness — the witness depends symbolically on outer Rat parameters. The v1 staged plan (#40) explicitly rejects these in Stage 3's variable-ownership classifier: outer Rat parameters appearing in the existential body itself force a witness that the LP-numeric machinery can't produce.

Stage 4a (#47) doesn't help either — its Benders loop produces numeric candidates, not symbolic ones. The third example above is particularly subtle: a appears only in the inner-∀ guard, looking syntactically like Stage 3's fragment, but the uniform strengthening Stage 3 attempts is false for that goal.

What would be needed

A separate algorithmic approach is required, likely Loos–Weispfenning-style symbolic quantifier elimination over Rat: case-split on dual bases, produce a piecewise-linear witness expression as a function of the outer parameters, reason about each piece's validity in the proof term.

LW QE is a complete decision procedure for the entire first-order theory of linear arithmetic over the rationals — so this issue, when implemented, would close the parametric-witness gap for any Lean goal expressible in that theory (including the three examples above).

Scope and tradeoffs

LW is substantially heavier than the LP-call-driven approach used in Stages 1–4a:

• Basis enumeration is exponential in the worst case (over the number of constraints).
• Piecewise reasoning in the proof term — each piece is a case-split, with corresponding bridge lemmas.
• Symbolic linear-coefficient arithmetic in the elaborator.

Implementing this is a significant effort. The right time to start is when v1 is in real use and the parametric-witness gap is identified as a recurring pain point.

Out of scope for this issue

• All of Stages 1–4a (already in their own issues).
• Strict-in-hypotheses extension (separate deferred issue: feat: lp tactic, strict-Farkas / slack-variable extension (deferred) #49).
• Performance-tuning of v1 (separate concern).

Status

Deferred. Not actively being worked on. Open for tracking. If you hit a Lean goal that Stage 3 rejects as parametric-witness and want it supported, comment here with the example.

🤖 Prepared with Claude Code