linarith certificate search as an LP problem

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.

def Linarith.SimplexAlgorithm.stateLP {matType : Nat → Nat → Type} [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] {n m : Nat} (A : matType n m) (strictIndexes : List Nat) : matType (n + 2) (m + 3)

Given matrix A and list strictIndexes of strict inequalities' indexes, we want to state the 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 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 homogenized problem is easier, but having some "unit" is necessary.
• To bound the problem we add the constraint x₁ + ... + xₘ + z = y introducing new variable z.

The objective function also interpreted as an auxiliary variable with constraint f = ∑ i ∈ strictIndexes, xᵢ.

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 nonnegative last column, meaning that we are starting from a feasible point.

Equations

• One or more equations did not get rendered due to their size.

def Linarith.SimplexAlgorithm.extractSolution {matType : Nat → Nat → Type} [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] (tableau : Linarith.SimplexAlgorithm.Tableau matType) : Array Rat

Extracts target vector from the tableau, putting auxiliary variables aside (see stateLP).

Equations

• One or more equations did not get rendered due to their size.

def Linarith.SimplexAlgorithm.findPositiveVector {n m : Nat} {matType : Nat → Nat → Type} [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] (A : matType n m) (strictIndexes : List Nat) : Lean.MetaM (Array Rat)

Finds a nonnegative vector v, such that A v = 0 and some of its coordinates from strictCoords are positive, in the case such v exists. If not, throws the error. The latter prevents linarith from doing useless post-processing.

Equations

• One or more equations did not get rendered due to their size.