[Merged by Bors] - feat(Tactic/Linarith): Simplex Algorithm oracle

[vasnesterov]

• 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.

---

[eric-wieser]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5567bba.
There were significant changes against commit 1c351ac:

  Benchmark                                  Metric         Change
  ================================================================
+ ~Mathlib.Analysis.Normed.Group.AddCircle   instructions   -65.0%

[eric-wieser]

At first glance this looks great! Could you add the examples from the two issues this closes as test cases in the test directory? Simply creating them is enough for them to be picked up as tests.

It's unfortunate that over mathlib as a whole this has almost no performance impact (besides the outlier Mathlib.Analysis.Normed.Group.AddCircle), but perhaps it only makes a difference on very large states; certainly this is not an argument against this PR :)

[vasnesterov]

@eric-wieser Thank you for your feedback! I have addressed your comments and slightly revised the code, making it shorter and (I hope) easier to read.

[eric-wieser]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6bff856.
The entire run failed.
Found no significant differences.

[vasnesterov]

!bench

[leanprover-bot]

Here are the benchmark results for commit 18974fc.
There were significant changes against commit 78e447b:

  Benchmark                                     Metric         Change
  ===================================================================
+ ~Mathlib.Analysis.Normed.Group.AddCircle      instructions   -62.6%
- ~Mathlib.Geometry.Manifold.Instances.Sphere   instructions     7.0%

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style