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 and Mathlib/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 implemented Linarith.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.

Estimated changes