instUsableInSimplexAlgorithmDenseMatrix

Lean4
instance : UsableInSimplexAlgorithm DenseMatrix
    where
  getElem mat i j := mat.data[i]![j]!
  setElem mat i j v := ⟨mat.data.modify i fun row => row.set! j v⟩
  getValues
    mat :=
    mat.data.zipIdx.foldl (init := []) fun acc (row, i) =>
      let rowVals := Array.toList <| row.zipIdx.filterMap fun (v, j) => if v != 0 then some (i, j, v) else none
      rowVals ++ acc
  ofValues {n m : Nat} vals :
    DenseMatrix _ _ :=
    Id.run
      (do
        let mut data : Array (Array Rat) := Array.replicate n <| Array.replicate m 0
        for ⟨i, j, v⟩ in vals do
          data := data.modify i fun row => row.set! j v
        return ⟨data⟩)
  swapRows mat i j := ⟨mat.data.swapIfInBounds i j⟩
  subtractRow mat i j
    coef :=
    let newData : Array (Array Rat) :=
      mat.data.modify j fun row => Array.zipWith (fun x y => x - coef * y) row mat.data[i]!
    ⟨newData⟩
  divideRow mat i coef := ⟨mat.data.modify i (·.map (· / coef))⟩
Похожие утверждения