LPTactic

New here? Start at leanprover/lp — the entry point for the lp / maximize tactics and the verified LP solver. This repository is one package of that family: the tactics and the backend registry.

The by lp and maximize tactics — Π₂ linear-rational-arithmetic goals reduced to LP solves, with the dual multipliers reconstructed into kernel-checked Lean proof terms — plus the LPBackend registry (registerBackend, resolveBackend, availableBackends), the default-backend dispatcher (LP.dispatchSolveExact), and the backend-pluggable verified-solve driver (solveVerifiedWith).

No moreLinkArgs. No FFI dependency. All solver calls go through LPBackend values fetched from the registry. A consumer who only wants to verify externally-produced certificates can depend on this package plus leanprover/lp-verify with zero native deps. For an actual default-FFI by lp, also depend on leanprover/lp-backend-soplex-ffi (or use the meta-package leanprover/lp, which bundles the FFI backend by default).

Quickstart

require LPTactic from git "https://github.com/leanprover/lp-tactic" @ "main"
require LPBackendSoplexFFI from git
  "https://github.com/leanprover/lp-backend-soplex-ffi" @ "main"

import LPTactic
import LPBackendSoplexFFI  -- self-registers "soplex-ffi" at priority 10

example (a b : Rat) (_ : 2 * a + b ≤ 5) (_ : a - b ≤ 1) :
    3 * a ≤ 6 := by lp

Without any backend registered, by lp reports a structured "no usable backend" diagnostic listing every registered backend and its probe verdict — so the failure mode is obvious.

Carriers

by lp and maximize work over a family of ordered carriers, not just Rat:

• Rat, Int, Dyadic, Nat — out of the box (core types).
• Real, or any Lean.Grind ordered field of characteristic 0 — once Mathlib is imported (it supplies the instances).

example (a b : Int) (_ : 2 * a + b ≤ 5) (_ : a - b ≤ 1) : 3 * a ≤ 6 := by lp
example (a b : Nat) (_ : 2 * a + b ≤ 5) (_ : a + b ≤ 3) : 3 * a + 2 * b ≤ 8 := by lp
-- with `import Mathlib`:
example (a b : ℝ)  (_ : 2 * a + b ≤ 5) (_ : a - b ≤ 1) : 3 * a ≤ 6 := by lp

The LP sent to the solver is always over ℚ; only the reconstructed proof term is over the carrier. lp proves ℚ-valid (Farkas) implications — integrality and cuts stay with omega/cutsat, so Nat subtraction (truncating) and Int/Nat division are rejected rather than mis-modelled.

Layout

LPTactic.lean              # top-level import
LPTactic/Basic.lean        # solveVerifiedWith, defaultDenomBudget
LPTactic/Registry.lean     # registerBackend, resolveBackend, availableBackends
LPTactic/Dispatch.lean     # dispatchSolveExact (registry-driven default)
LPTactic/Q.lean            # kernel-reducible rational literals
LPTactic/LP.lean           # `lp` and `maximize` tactic frontend
LPTactic/LP/Types.lean     # tactic state + telemetry
LPTactic/LP/Parse.lean     # goal parsing
LPTactic/LP/Problem.lean   # tactic-side Problem construction
LPTactic/LP/Atomic.lean    # direct-certificate path
LPTactic/LP/Exists.lean    # existential-witness LP path
LPTactic/LP/Forall.lean    # inner-∀ + Benders subproblem paths
LPTactic/LP/Maximize.lean  # `maximize` tactic body
LPTactic/LP/Certificate.lean
                           # certificate → kernel proof-term reconstruction
LPTactic/LP/Frontend.lean  # syntax elaboration entry point

Declarations remain under namespace LP (or LP, LP.Tactic.LP) so consumers writing LP.solveVerifiedWith or by lp resolve to the same definitions regardless of which package owns them. The synchronous, FFI-specialised LP.solveVerified (Except-typed) lives in leanprover/lp-backend-soplex-ffi, not here.

Licence

Apache License 2.0.