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} (mat : α n m) (i j : Nat) : Rat

  Returns mat[i, j].

• setElem {n m : Nat} (mat : α n m) (i j : Nat) (v : Rat) : α n m

  Sets mat[i, j].

• getValues {n m : Nat} (mat : α 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} (values : 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} (mat : α n m) (i j : Nat) : α n m

  Swaps two rows.

• subtractRow {n m : Nat} (mat : α n m) (i j : Nat) (coef : Rat) : α n m

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

• divideRow {n m : Nat} (mat : α n m) (i : Nat) (coef : Rat) : α n m

  Divides the i-th row by coef.

instance Linarith.SimplexAlgorithm.instGetElemProdNatRatAndLtFstSndOfUsableInSimplexAlgorithm (n m : Nat) (matType : Nat → Nat → Type) [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 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 : UsableInSimplexAlgorithm DenseMatrix

Equations

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

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

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

• data : Array (Std.HashMap Nat Rat)

  The content of the matrix.

instance Linarith.SimplexAlgorithm.instUsableInSimplexAlgorithmSparseMatrix : UsableInSimplexAlgorithm SparseMatrix

Equations

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

structure Linarith.SimplexAlgorithm.Tableau (matType : Nat → Nat → Type) [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.