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

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 (https://github.com/kim-em/soplex/issues/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 (https://github.com/kim-em/soplex/issues/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: https://github.com/kim-em/soplex/issues/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

Start by reading the staged-plan issues #40 and #47 to understand the rejected parametric-witness fragment and existing LP approach. Investigate the tactic and elaborator entry points for implementing Loos–Weispfenning-style symbolic quantifier elimination over Rat. Done means supporting the three example goals and the broader first-order linear-arithmetic fragment with verified piecewise witness proofs.