Datatypes for Simplex Algorithm implementation

structure Linarith.SimplexAlgorithm.Matrix (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.instGetElemMatrixNatArrayRatLt (n : Nat) (m : Nat) : GetElem (Linarith.SimplexAlgorithm.Matrix n m) Nat (Array Rat) fun (x : Linarith.SimplexAlgorithm.Matrix n m) (i : Nat) => i < n

Equations

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

structure Linarith.SimplexAlgorithm.Table : Type

Table is a structure 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 : Linarith.SimplexAlgorithm.Matrix self.basic.size self.free.size

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