Simplex Algorithm

To obtain required vector in Linarith.SimplexAlgorithm.findPositiveVector we run the Simplex Algorithm. We use Bland's rule for pivoting, which guarantees that the algorithm terminates.

inductive Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmException : Type

An exception in the SimplexAlgorithmM monad.

• infeasible : SimplexAlgorithmException

  The solution is infeasible.

@[reducible, inline]

abbrev Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmM (matType : ℕ → ℕ → Type) [UsableInSimplexAlgorithm matType] (α : Type) : Type

The monad for the Simplex Algorithm.

def Mathlib.Tactic.Linarith.SimplexAlgorithm.doPivotOperation {matType : ℕ → ℕ → Type} [UsableInSimplexAlgorithm matType] (exitIdx enterIdx : ℕ) : SimplexAlgorithmM matType Unit

Given indexes exitIdx and enterIdx of exiting and entering variables in the basic and free arrays, performs pivot operation, i.e. expresses one through the other and makes the free one basic and vice versa.

def Mathlib.Tactic.Linarith.SimplexAlgorithm.checkSuccess {matType : ℕ → ℕ → Type} [UsableInSimplexAlgorithm matType] : SimplexAlgorithmM matType Bool

Check if the solution is found: the objective function is positive and all basic variables are nonnegative.

def Mathlib.Tactic.Linarith.SimplexAlgorithm.chooseEnteringVar {matType : ℕ → ℕ → Type} [UsableInSimplexAlgorithm matType] : SimplexAlgorithmM matType ℕ

Chooses an entering variable: among the variables with a positive coefficient in the objective function, the one with the smallest index (in the initial indexing).

def Mathlib.Tactic.Linarith.SimplexAlgorithm.chooseExitingVar {matType : ℕ → ℕ → Type} [UsableInSimplexAlgorithm matType] (enterIdx : ℕ) : SimplexAlgorithmM matType ℕ

Chooses an exiting variable: the variable imposing the strictest limit on the increase of the entering variable, breaking ties by choosing the variable with smallest index.

def Mathlib.Tactic.Linarith.SimplexAlgorithm.choosePivots {matType : ℕ → ℕ → Type} [UsableInSimplexAlgorithm matType] : SimplexAlgorithmM matType (ℕ × ℕ)

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 Mathlib.Tactic.Linarith.SimplexAlgorithm.runSimplexAlgorithm {matType : ℕ → ℕ → Type} [UsableInSimplexAlgorithm matType] : SimplexAlgorithmM matType Unit

Runs the Simplex Algorithm inside the SimplexAlgorithmM. It always terminates, finding solution if such exists.