Lean4
/-- Given matrix `A` and list `strictIndexes` of strict inequalities' indexes, we want to state the
Linear Programming problem which solution would give us a solution for the initial problem (see
`findPositiveVector`).
As an objective function (that we are trying to maximize) we use sum of coordinates from
`strictIndexes`: it suffices to find the nonnegative vector that makes this function positive.
We introduce two auxiliary variables and one constraint:
* The variable `y` is interpreted as "homogenized" `1`. We need it because dealing with a
homogenized problem is easier, but having some "unit" is necessary.
* To bound the problem we add the constraint `x₁ + ... + xₘ + z = y` introducing new variable `z`.
The objective function also interpreted as an auxiliary variable with constraint
`f = ∑ i ∈ strictIndexes, xᵢ`.
The variable `f` has to always be basic while `y` has to be free. Our Gauss method implementation
greedy collects basic variables moving from left to right. So we place `f` before `x`-s and `y`
after them. We place `z` between `f` and `x` because in this case `z` will be basic and
`Gauss.getTableau` produce tableau with nonnegative last column, meaning that we are starting from
a feasible point.
-/
def stateLP {n m : Nat} (A : matType n m) (strictIndexes : List Nat) : matType (n + 2) (m + 3) :=
/- +2 due to shifting by `f` and `z` -/
let objectiveRow : List (Nat × Nat × Rat) := (0, 0, -1) :: strictIndexes.map fun idx => (0, idx + 2, 1)
let constraintRow : List (Nat × Nat × Rat) :=
[(1, 1, 1), (1, m + 2, -1)] ++ (List.range m).map (fun i => (1, i + 2, 1))
let valuesA := getValues A |>.map fun (i, j, v) => (i + 2, j + 2, v)
ofValues (objectiveRow ++ constraintRow ++ valuesA)
