Commit 2024-05-09 22:39 f993b414
View on Github →feat(Tactic/Linarith): Simplex Algorithm oracle (#12014)
- Reduce the
linarith
certificate search problem to some Linear Programming problem and implement the Simplex Algorithm to solve it. - Set the default oracle for
linarith
to this. - Remove unnecessary hypotheses in
Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
andMathlib/Analysis/Distribution/SchwartzSpace.lean
which were needed with the Fourier-Motzkin oracle. - Adjust the definition of
CerficateOracle
to enable dot notation to choose between oracles. This addresses #2717 and #8875 (except when the user overrides the oracle) Also, this oracle is far more efficient: The example below takes lots of time with the Fourier-Motzkin oracle: I waited 5 minutes and still didn't get it. But with the just implementedLinarith.SimplexAlgo.produceCertificate
oracle the proof succeeds in less than a second.
import Mathlib.Tactic.Linarith
example (x0 x1 x2 x3 x4 : ℚ) :
3 * x0 - 15 * x1 - 30 * x2 + 20 * x3 + 12 * x4 ≤ 0 →
35 * x0 - 30 * x1 + 12 * x2 - 15 * x3 + 18 * x4 ≤ 0 →
5 * x0 + 20 * x1 + 24 * x2 + 20 * x3 + 9 * x4 ≤ 0 →
-2 * x0 - 30 * x1 + 30 * x2 - 10 * x3 - 12 * x4 ≤ 0 →
-4 * x0 - 25 * x1 + 6 * x2 - 20 * x3 ≤ 0 →
25 * x1 + 30 * x2 - 25 * x3 + 12 * x4 ≤ 0 →
10 * x1 - 18 * x2 - 30 * x3 + 18 * x4 ≤ 0 →
4 * x0 + 10 * x1 - 18 * x2 - 15 * x3 + 15 * x4 ≤ 0 →
-4 * x0 + 15 * x1 - 30 * x2 + 15 * x3 + 6 * x4 ≤ 0 →
-2 * x0 - 5 * x1 + 18 * x2 - 25 * x3 - 161 * x4 ≤ 0 →
-6 * x0 + 30 * x1 + 6 * x2 - 15 * x3 ≤ 0 →
3 * x0 + 10 * x1 - 30 * x2 + 25 * x3 + 12 * x4 ≤ 0 →
2 * x0 + 10 * x1 - 24 * x2 - 15 * x3 + 3 * x4 ≤ 0 →
82 * x1 + 36 * x2 + 20 * x3 + 9 * x4 ≤ 0 →
2 * x0 - 30 * x1 - 30 * x2 - 15 * x3 + 6 * x4 ≤ 0 →
4 * x0 - 15 * x1 + 25 * x2 < 0 →
-4 * x0 - 10 * x1 + 30 * x2 - 15 * x3 ≤ 0 →
2 * x0 + 6 * x2 + 133 * x3 + 12 * x4 ≤ 0 →
3 * x0 + 15 * x1 - 6 * x2 - 15 * x3 - 15 * x4 ≤ 0 →
10 * x1 + 6 * x2 - 25 * x3 + 3 * x4 ≤ 0 →
-2 * x0 + 5 * x1 + 12 * x2 - 20 * x3 + 12 * x4 ≤ 0 →
-5 * x0 - 25 * x1 + 30 * x3 - 12 * x4 ≤ 0 →
-6 * x0 - 30 * x1 - 36 * x2 + 20 * x3 + 12 * x4 ≤ 0 →
5 * x0 - 5 * x1 + 6 * x2 - 25 * x3 ≤ 0 →
-3 * x0 - 20 * x1 - 30 * x2 + 5 * x3 + 3 * x4 ≤ 0 →
False := by intros; linarith (config := {oracle := Linarith.FourierMotzkin.produceCertificate})
I am planning to prove the "completeness" of the oracle in the next PRs, but so far I have run a stress test on randomly generated examples of various sizes, and it seems that everything is OK.