From f2405442b5b4fe2ba540046b771e3d7181fb3987 Mon Sep 17 00:00:00 2001 From: Vasily Nesterov Date: Sun, 16 Jun 2024 19:40:06 +0000 Subject: [PATCH] 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 --- Mathlib.lean | 8 ++-- Mathlib/Tactic.lean | 8 ++-- Mathlib/Tactic/Linarith/Frontend.lean | 43 ++++++++++++------- .../Linarith/Oracle/SimplexAlgorithm.lean | 16 ++++--- .../SimplexAlgorithm/Datatypes.lean | 0 .../{ => Oracle}/SimplexAlgorithm/Gauss.lean | 2 +- .../SimplexAlgorithm/PositiveVector.lean | 32 ++++++++++---- .../SimplexAlgorithm/SimplexAlgorithm.lean | 5 ++- 8 files changed, 75 insertions(+), 39 deletions(-) rename Mathlib/Tactic/Linarith/{ => Oracle}/SimplexAlgorithm/Datatypes.lean (100%) rename Mathlib/Tactic/Linarith/{ => Oracle}/SimplexAlgorithm/Gauss.lean (97%) rename Mathlib/Tactic/Linarith/{ => Oracle}/SimplexAlgorithm/PositiveVector.lean (71%) rename Mathlib/Tactic/Linarith/{ => Oracle}/SimplexAlgorithm/SimplexAlgorithm.lean (95%) diff --git a/Mathlib.lean b/Mathlib.lean index 8f82219cdff03..98bf85ba044b0 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index 33db4ae3980e6..5a22f8d3325c4 100644 --- a/Mathlib/Tactic.lean +++ b/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 diff --git a/Mathlib/Tactic/Linarith/Frontend.lean b/Mathlib/Tactic/Linarith/Frontend.lean index 3f6866e435370..cfc203fd1189b 100644 --- a/Mathlib/Tactic/Linarith/Frontend.lean +++ b/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. diff --git a/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean b/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean index d07aaa144a1a4..e582844d49f0a 100644 --- a/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm.lean +++ b/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 diff --git a/Mathlib/Tactic/Linarith/SimplexAlgorithm/Datatypes.lean b/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean similarity index 100% rename from Mathlib/Tactic/Linarith/SimplexAlgorithm/Datatypes.lean rename to Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean diff --git a/Mathlib/Tactic/Linarith/SimplexAlgorithm/Gauss.lean b/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Gauss.lean similarity index 97% rename from Mathlib/Tactic/Linarith/SimplexAlgorithm/Gauss.lean rename to Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Gauss.lean index 81d6d89a1e899..ab46c5726b44f 100644 --- a/Mathlib/Tactic/Linarith/SimplexAlgorithm/Gauss.lean +++ b/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 diff --git a/Mathlib/Tactic/Linarith/SimplexAlgorithm/PositiveVector.lean b/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/PositiveVector.lean similarity index 71% rename from Mathlib/Tactic/Linarith/SimplexAlgorithm/PositiveVector.lean rename to Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/PositiveVector.lean index edc08bf4c980d..1c67ffae264eb 100644 --- a/Mathlib/Tactic/Linarith/SimplexAlgorithm/PositiveVector.lean +++ b/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) := diff --git a/Mathlib/Tactic/Linarith/SimplexAlgorithm/SimplexAlgorithm.lean b/Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/SimplexAlgorithm.lean similarity index 95% rename from Mathlib/Tactic/Linarith/SimplexAlgorithm/SimplexAlgorithm.lean rename to Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/SimplexAlgorithm.lean index da753de8dea95..924814fa69fce 100644 --- a/Mathlib/Tactic/Linarith/SimplexAlgorithm/SimplexAlgorithm.lean +++ b/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