-
Notifications
You must be signed in to change notification settings - Fork 251
/
Datatypes.lean
127 lines (114 loc) · 4.99 KB
/
Datatypes.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
/-
Copyright (c) 2024 Vasily Nesterov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Vasily Nesterov
-/
import Batteries.Data.Rat.Basic
/-!
# Datatypes for the Simplex Algorithm implementation
-/
namespace Linarith.SimplexAlgorithm
/--
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.
-/
class UsableInSimplexAlgorithm (α : Nat → Nat → Type) where
/-- Returns `mat[i, j]`. -/
getElem {n m : Nat} (mat : α n m) (i j : Nat) : Rat
/-- Sets `mat[i, j]`. -/
setElem {n m : Nat} (mat : α n m) (i j : Nat) (v : Rat) : α n m
/-- Returns the list of elements of `mat` in the form `(i, j, mat[i, j])`. -/
getValues {n m : Nat} (mat : α n m) : List (Nat × Nat × Rat)
/-- Creates a matrix from a list of elements in the form `(i, j, mat[i, j])`. -/
ofValues {n m : Nat} (values : List (Nat × Nat × Rat)) : α n m
/-- Swaps two rows. -/
swapRows {n m : Nat} (mat : α n m) (i j : Nat) : α n m
/-- Subtracts `i`-th row multiplied by `coef` from `j`-th row. -/
subtractRow {n m : Nat} (mat : α n m) (i j : Nat) (coef : Rat) : α n m
/-- Divides the `i`-th row by `coef`. -/
divideRow {n m : Nat} (mat : α n m) (i : Nat) (coef : Rat) : α n m
export UsableInSimplexAlgorithm (setElem getValues ofValues swapRows subtractRow divideRow)
instance (n m : Nat) (matType : Nat → Nat → Type) [UsableInSimplexAlgorithm matType] :
GetElem (matType n m) (Nat × Nat) Rat fun _ p => p.1 < n ∧ p.2 < m where
getElem mat p _ := UsableInSimplexAlgorithm.getElem mat p.1 p.2
/--
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.
-/
structure DenseMatrix (n m : Nat) where
/-- The content of the matrix. -/
data : Array (Array Rat)
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.zipWithIndex.foldl (init := []) fun acc (row, i) =>
let rowVals := Array.toList <| row.zipWithIndex.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.mkArray n <| Array.mkArray 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.swap! i j⟩
subtractRow mat i j coef :=
let newData : Array (Array Rat) := mat.data.modify j fun row =>
row.zipWith mat.data[i]! fun x y => x - coef * y
⟨newData⟩
divideRow mat i coef := ⟨mat.data.modify i (·.map (· / coef))⟩
/--
Structure for sparse matrices over ℚ, implemented as an array of hashmaps, containing only nonzero
values.
-/
structure SparseMatrix (n m : Nat) where
/-- The content of the matrix. -/
data : Array <| Lean.HashMap Nat Rat
instance : UsableInSimplexAlgorithm SparseMatrix where
getElem mat i j := mat.data[i]!.findD j 0
setElem mat i j v :=
if v == 0 then
⟨mat.data.modify i fun row => row.erase j⟩
else
⟨mat.data.modify i fun row => row.insert j v⟩
getValues mat :=
mat.data.zipWithIndex.foldl (init := []) fun acc (row, i) =>
let rowVals := row.toList.map fun (j, v) => (i, j, v)
rowVals ++ acc
ofValues {n _ : Nat} vals := Id.run do
let mut data : Array (Lean.HashMap Nat Rat) := Array.mkArray n .empty
for ⟨i, j, v⟩ in vals do
if v != 0 then
data := data.modify i fun row => row.insert j v
return ⟨data⟩
swapRows mat i j := ⟨mat.data.swap! i j⟩
subtractRow mat i j coef :=
let newData := mat.data.modify j fun row =>
mat.data[i]!.fold (fun cur k val =>
let newVal := (cur.findD k 0) - coef * val
if newVal != 0 then cur.insert k newVal else cur.erase k
) row
⟨newData⟩
divideRow mat i coef :=
let newData : Array (Lean.HashMap Nat Rat) := mat.data.modify i fun row =>
row.fold (fun cur k v => cur.insert k (v / coef)) row
⟨newData⟩
/--
`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`.
-/
structure Tableau (matType : Nat → Nat → Type) [UsableInSimplexAlgorithm matType] where
/-- Array containing the basic variables' indexes -/
basic : Array Nat
/-- Array containing the free variables' indexes -/
free : Array Nat
/-- Matrix of coefficients the basic variables expressed through the free ones. -/
mat : matType basic.size free.size
end Linarith.SimplexAlgorithm