doc(Tactic/Linarith): update docs (#13856)

This PR updates the documentation following the integration of the oracle based on the Simplex Algorithm, as merged in PRs #12014, #13535, #12819, and #13800. Additionally, it moves the `SimplexAlgorithm` folder into the `Oracle` directory.



Co-authored-by: Rob Lewis <[email protected]>

Mathlib.lean

@@ -3865,12 +3865,12 @@ import Mathlib.Tactic.Linarith.Frontend
 import Mathlib.Tactic.Linarith.Lemmas
 import Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
 import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
 import Mathlib.Tactic.Linarith.Parsing
 import Mathlib.Tactic.Linarith.Preprocessing
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.Datatypes
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.PositiveVector
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithm
 import Mathlib.Tactic.Linarith.Verification
 import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.Linter

Mathlib/Tactic.lean

@@ -105,12 +105,12 @@ import Mathlib.Tactic.Linarith.Frontend
 import Mathlib.Tactic.Linarith.Lemmas
 import Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
 import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
 import Mathlib.Tactic.Linarith.Parsing
 import Mathlib.Tactic.Linarith.Preprocessing
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.Datatypes
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.PositiveVector
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithm
 import Mathlib.Tactic.Linarith.Verification
 import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.Linter

Mathlib/Tactic/Linarith/Frontend.lean

@@ -54,17 +54,29 @@ Preprocessors are allowed to branch, that is, to case split on disjunctions. `li
 overall if it succeeds in all cases. This leads to exponential blowup in the number of `linarith`
 calls, and should be used sparingly. The default preprocessor set does not include case splits.
 
-## Fourier-Motzkin elimination
-
-The oracle implemented to search for certificates uses Fourier-Motzkin variable elimination.
-This technique transforms a set of inequalities in `n` variables to an equisatisfiable set in
-`n - 1` variables. Once all variables have been eliminated, we conclude that the original set was
-unsatisfiable iff the comparison `0 < 0` is in the resulting set.
-
-While performing this elimination, we track the history of each derived comparison. This allows us
-to represent any comparison at any step as a positive combination of comparisons from the original
-set. In particular, if we derive `0 < 0`, we can find our desired list of coefficients
-by counting how many copies of each original comparison appear in the history.
+## Oracles
+
+There are two oracles that can be used in `linarith` so far.
+
+1. **Fourier-Motzkin elimination.**
+  This technique transforms a set of inequalities in `n` variables to an equisatisfiable set in
+  `n - 1` variables. Once all variables have been eliminated, we conclude that the original set was
+  unsatisfiable iff the comparison `0 < 0` is in the resulting set.
+  While performing this elimination, we track the history of each derived comparison. This allows us
+  to represent any comparison at any step as a positive combination of comparisons from the original
+  set. In particular, if we derive `0 < 0`, we can find our desired list of coefficients
+  by counting how many copies of each original comparison appear in the history.
+  This oracle was historically implemented earlier, and is sometimes faster on small states, but it
+  has [bugs](https://github.com/leanprover-community/mathlib4/issues/2717) and can not handle
+  large problems. You can use it with `linarith (config := { oracle := .fourierMotzkin })`.
+
+2. **Simplex Algorithm (default).**
+  This oracle reduces the search for a unsatisfiability certificate to some Linear Programming
+  problem. The problem is then solved by a standard Simplex Algorithm. We use
+  [Bland's pivot rule](https://en.wikipedia.org/wiki/Bland%27s_rule) to guarantee that the algorithm
+  terminates.
+  The default version of the algorithm operates with sparse matrices as it is usually faster. You
+  can invoke the dense version by `linarith (config := { oracle := .simplexAlgorithmDense })`.
 
 ## Implementation details
 
@@ -79,8 +91,8 @@ goals by splitting them into two weak inequalities and running twice. But it doe
 disequality hypotheses, since this would lead to a number of runs exponential in the number of
 disequalities in the context.
 
-The Fourier-Motzkin oracle is very modular. It can easily be replaced with another function of type
-`certificateOracle := List Comp → ℕ → TacticM ((Batteries.HashMap ℕ ℕ))`,
+The oracle is very modular. It can easily be replaced with another function of type
+`List Comp → ℕ → MetaM ((Batteries.HashMap ℕ ℕ))`,
 which takes a list of comparisons and the largest variable
 index appearing in those comparisons, and returns a map from comparison indices to coefficients.
 An alternate oracle can be specified in the `LinarithConfig` object.
@@ -93,7 +105,7 @@ proof term of type `False`.
 
 Some of the behavior of `linarith` can be inspected with the option
 `set_option trace.linarith true`.
-Because the variable elimination happens outside the tactic monad, we cannot trace intermediate
+However, both oracles mainly runs outside the tactic monad, so we cannot trace intermediate
 steps there.
 
 ## File structure
@@ -107,7 +119,8 @@ The components of `linarith` are spread between a number of files for the sake o
 * `Preprocessing.lean` contains functions used at the beginning of the tactic to transform
   hypotheses into a shape suitable for the main routine.
 * `Parsing.lean` contains functions used to compute the linear structure of an expression.
-* `Elimination.lean` contains the Fourier-Motzkin elimination routine.
+* The `Oracle` folder contains files implementing the oracles that can be used to produce a
+  certificate of unsatisfiability.
 * `Verification.lean` contains the certificate checking functions that produce a proof of `False`.
 * `Frontend.lean` contains the control methods and user-facing components of the tactic.
 

Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean

@@ -4,17 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Vasily Nesterov
 -/
 import Mathlib.Tactic.Linarith.Datatypes
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.PositiveVector
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector
 
 /-!
-# Hooks to enable the use of the simplex algorithm in `linarith`
+# The oracle based on Simplex Algorithm
+
+This file contains hooks to enable the use of the Simplex Algorithm in `linarith`.
+The algorithm's entry point is the function `Linarith.SimplexAlgorithm.findPositiveVector`.
+See the file `PositiveVector.lean` for details of how the procedure works.
 -/
 
 open Batteries
 
 namespace Linarith.SimplexAlgorithm
 
-/-- Preprocess the goal to pass it to `findPositiveVector`. -/
+/-- Preprocess the goal to pass it to `Linarith.SimplexAlgorithm.findPositiveVector`. -/
 def preprocess (matType : ℕ → ℕ → Type) [UsableInSimplexAlgorithm matType] (hyps : List Comp)
     (maxVar : ℕ) : matType (maxVar + 1) (hyps.length) × List Nat :=
   let values : List (ℕ × ℕ × ℚ) := hyps.foldlIdx (init := []) fun idx cur comp =>
@@ -23,7 +27,9 @@ def preprocess (matType : ℕ → ℕ → Type) [UsableInSimplexAlgorithm matTyp
   let strictIndexes := hyps.findIdxs (·.str == Ineq.lt)
   (ofValues values, strictIndexes)
 
-/-- Extract the certificate from the `vec` found by `findPositiveVector`. -/
+/--
+Extract the certificate from the `vec` found by `Linarith.SimplexAlgorithm.findPositiveVector`.
+-/
 def postprocess (vec : Array ℚ) : HashMap ℕ ℕ :=
   let common_den : ℕ := vec.foldl (fun acc item => acc.lcm item.den) 1
   let vecNat : Array ℕ := vec.map (fun x : ℚ => (x * common_den).floor.toNat)
@@ -34,7 +40,7 @@ end SimplexAlgorithm
 
 open SimplexAlgorithm
 
-/-- An oracle that uses the simplex algorithm. -/
+/-- An oracle that uses the Simplex Algorithm. -/
 def CertificateOracle.simplexAlgorithmSparse : CertificateOracle where
   produceCertificate hyps maxVar := do
     let (A, strictIndexes) := preprocess SparseMatrix hyps maxVar

Mathlib/Tactic/Linarith/SimplexAlgorithm/Gauss.lean → Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Gauss.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Vasily Nesterov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Vasily Nesterov
 -/
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.Datatypes
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
 
 /-!
 # Gaussian Elimination algorithm

Mathlib/Tactic/Linarith/SimplexAlgorithm/PositiveVector.lean → Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/PositiveVector.lean

@@ -3,17 +3,33 @@ Copyright (c) 2024 Vasily Nesterov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Vasily Nesterov
 -/
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithm
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.Gauss
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss
 
 /-!
-# `linarith` certificate search a LP problem
+# `linarith` certificate search as an LP problem
 
-`linarith` certificate search can easily be reduced to this LP problem: given the matrix `A` and the
-list `strictIndexes`, find the non-negative vector `v` such that some of its coordinates from
+`linarith` certificate search can easily be reduced to the following problem:
+given the matrix `A` and the list `strictIndexes`,
+find the nonnegative vector `v` such that some of its coordinates from
 the `strictIndexes` are positive and `A v = 0`.
 
 The function `findPositiveVector` solves this problem.
+
+# Algorithm sketch
+
+1. We translate the problem stated above to some Linear Programming problem. See `stateLP` for
+  details. Let us denote the corresponding matrix `B`.
+
+2. We solve the equation `B x = 0` using Gauss Elimination, splitting the set of variables into
+  *free* variables, which can take any value,
+  and *basic* variables which are linearly expressed through the free one.
+  This gives us an initial tableau for the Simplex Algorithm.
+  See `Linarith.SimplexAlgorithm.Gauss.getTableau`.
+
+3. We run the Simplex Algorithm until it finds a solution.
+  See the file `SimplexAlgorithm.lean`.
+
 -/
 
 namespace Linarith.SimplexAlgorithm
@@ -22,11 +38,11 @@ variable {matType : Nat → Nat → Type} [UsableInSimplexAlgorithm matType]
 
 /--
 Given matrix `A` and list `strictIndexes` of strict inequalities' indexes, we want to state the
-Linear Programming problem which solution produces solution for the initial problem (see
+Linear Programming problem which solution would give us a solution for the initial problem (see
 `findPositiveVector`).
 
 As an objective function (that we are trying to maximize) we use sum of coordinates from
-`strictIndexes`: it suffices to find the non-negative vector that makes this function positive.
+`strictIndexes`: it suffices to find the nonnegative vector that makes this function positive.
 
 We introduce two auxiliary variables and one constraint:
 * The variable `y` is interpreted as "homogenized" `1`. We need it because dealing with a
@@ -39,7 +55,7 @@ The objective function also interpreted as an auxiliary variable with constraint
 The variable `f` has to always be basic while `y` has to be free. Our Gauss method implementation
 greedy collects basic variables moving from left to right. So we place `f` before `x`-s and `y`
 after them. We place `z` between `f` and `x` because in this case `z` will be basic and
-`Gauss.getTableau` produce tableau with non-negative last column, meaning that we are starting from
+`Gauss.getTableau` produce tableau with nonnegative last column, meaning that we are starting from
 a feasible point.
 -/
 def stateLP {n m : Nat} (A : matType n m) (strictIndexes : List Nat) : matType (n + 2) (m + 3) :=

Mathlib/Tactic/Linarith/SimplexAlgorithm/SimplexAlgorithm.lean → Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/SimplexAlgorithm.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Vasily Nesterov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Vasily Nesterov
 -/
-import Mathlib.Tactic.Linarith.SimplexAlgorithm.Datatypes
+import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
 
 /-!
 # Simplex Algorithm
@@ -101,7 +101,8 @@ def chooseExitingVar (enterIdx : Nat) : SimplexAlgorithmM matType Nat := do
   return exitIdxOpt.get! -- such variable always exists because our problem is bounded
 
 /--
-Chooses entering and exiting variables using Bland's rule that guarantees that the Simplex
+Chooses entering and exiting variables using
+(Bland's rule)[(https://en.wikipedia.org/wiki/Bland%27s_rule)] that guarantees that the Simplex
 Algorithm terminates.
 -/
 def choosePivots : SimplexAlgorithmM matType (Nat × Nat) := do