Documentation

Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes

Datatypes for the Simplex Algorithm implementation #

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.

Instances
    instance Linarith.SimplexAlgorithm.instGetElemProdNatRatAndLtFstSndOfUsableInSimplexAlgorithm (n m : Nat) (matType : NatNatType) [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 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.

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

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

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

        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.

        Instances For