Lean4
/-- Given indexes `exitIdx` and `enterIdx` of exiting and entering variables in the `basic` and `free`
arrays, performs pivot operation, i.e. expresses one through the other and makes the free one basic
and vice versa.
-/
def doPivotOperation (exitIdx enterIdx : Nat) : SimplexAlgorithmM matType Unit :=
modify fun s : Tableau matType =>
Id.run
(do
let mut mat := s.mat
let intersectCoef := mat[(exitIdx, enterIdx)]!
for i in [:s.basic.size]do
if i == exitIdx then
continue
let coef := mat[(i, enterIdx)]! / intersectCoef
if coef != 0 then
mat := subtractRow mat exitIdx i coef
mat := setElem mat i enterIdx coef
mat := setElem mat exitIdx enterIdx (-1)
mat := divideRow mat exitIdx (-intersectCoef)
let newBasic := s.basic.set! exitIdx s.free[enterIdx]!
let newFree := s.free.set! enterIdx s.basic[exitIdx]!
have hb : newBasic.size = s.basic.size := by apply Array.size_setIfInBounds
have hf : newFree.size = s.free.size := by apply Array.size_setIfInBounds
return (⟨newBasic, newFree, hb ▸ hf ▸ mat⟩ : Tableau matType))
