Datatypes for the Simplex Algorithm implementation

class Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm (α : Nat → Nat → Type) : Type

Specification for matrix types over ℚ which can be used in the Gauss Elimination and the Simplex Algorithm. It was introduced to unify dense matrices and sparse matrices.

• getElem : {n m : Nat} → α n m → Nat → Nat → Rat

  Returns mat[i, j].

• setElem : {n m : Nat} → α n m → Nat → Nat → Rat → α n m

  Sets mat[i, j].

• getValues : {n m : Nat} → α n m → List (Nat × Nat × Rat)

  Returns the list of elements of mat in the form (i, j, mat[i, j]).

• ofValues : {n m : Nat} → List (Nat × Nat × Rat) → α n m

  Creates a matrix from a list of elements in the form (i, j, mat[i, j]).

• swapRows : {n m : Nat} → α n m → Nat → Nat → α n m

  Swaps two rows.

• subtractRow : {n m : Nat} → α n m → Nat → Nat → Rat → α n m

  Subtracts i-th row multiplied by coef from j-th row.

• divideRow : {n m : Nat} → α n m → Nat → Rat → α n m

  Divides the i-th row by coef.

instance Linarith.SimplexAlgorithm.instGetElemProdNatRatAndLtFstSndOfUsableInSimplexAlgorithm (n : Nat) (m : Nat) (matType : Nat → Nat → Type) [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] : GetElem (matType n m) (Nat × Nat) Rat fun (x : matType n m) (p : Nat × Nat) => p.fst < n ∧ p.snd < m

Equations

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

structure Linarith.SimplexAlgorithm.DenseMatrix (n : Nat) (m : Nat) : Type

Structure for matrices over ℚ.

So far it is just a 2d-array carrying dimensions (that are supposed to match with the actual dimensions of data), but the plan is to add some Prop-data and make the structure strict and safe.

Note: we avoid using the Matrix from Mathlib.Data.Matrix because it is far more efficient to store matrix as its entries than as function between Fin-s.

• data : Array (Array Rat)

  The content of the matrix.

instance Linarith.SimplexAlgorithm.instUsableInSimplexAlgorithmDenseMatrix : Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm Linarith.SimplexAlgorithm.DenseMatrix

Equations

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

structure Linarith.SimplexAlgorithm.SparseMatrix (n : Nat) (m : Nat) : Type

Structure for sparse matrices over ℚ, implemented as an array of hashmaps, containing only nonzero values.

• data : Array (Lean.HashMap Nat Rat)

  The content of the matrix.

instance Linarith.SimplexAlgorithm.instUsableInSimplexAlgorithmSparseMatrix : Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm Linarith.SimplexAlgorithm.SparseMatrix

Equations

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

structure Linarith.SimplexAlgorithm.Tableau (matType : Nat → Nat → Type) [Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] : Type

Tableau is a structure the Simplex Algorithm operates on. The i-th row of mat expresses the variable basic[i] as a linear combination of variables from free.

• basic : Array Nat

  Array containing the basic variables' indexes

• free : Array Nat

  Array containing the free variables' indexes

• mat : matType self.basic.size self.free.size

  Matrix of coefficients the basic variables expressed through the free ones.