Documentation

Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm

The oracle based on Simplex Algorithm #

This file contains hooks to enable the use of the Simplex Algorithm in linarith. The algorithm's entry point is the function Linarith.SimplexAlgorithm.findPositiveVector. See the file PositiveVector.lean for details of how the procedure works.

source
def Mathlib.Tactic.Linarith.SimplexAlgorithm.preprocess (matType : ℕ → ℕ → Type) [UsableInSimplexAlgorithm matType] (hyps : List Comp) (maxVar : ℕ) :
matType (maxVar + 1) hyps.length × List ℕ

Preprocess the goal to pass it to Linarith.SimplexAlgorithm.findPositiveVector.

Equations
    Instances For
      source
      def Mathlib.Tactic.Linarith.SimplexAlgorithm.postprocess (vec : Array ℚ) :
      Std.HashMap ℕ ℕ

      Extract the certificate from the vec found by Linarith.SimplexAlgorithm.findPositiveVector.

      Equations
        Instances For
          source
          def Mathlib.Tactic.Linarith.CertificateOracle.simplexAlgorithmSparse :
          CertificateOracle

          An oracle that uses the Simplex Algorithm.

          Equations
            Instances For
              source
              def Mathlib.Tactic.Linarith.CertificateOracle.simplexAlgorithmDense :
              CertificateOracle

              The same oracle as CertificateOracle.simplexAlgorithmSparse, but uses dense matrices. Works faster on dense states.

              Equations
                Instances For