Some of the data structures here are used in multiple parts of the tactic. We split them into their own file.
This file also contains a few convenient auxiliary functions.
Linear expressions #
A linear expression is a list of pairs of variable indices and coefficients, representing the sum of the products of each coefficient with its corresponding variable.
Some functions on
linexp assume that
n : ℕ occurs at most once as the first element of a pair,
and that the list is sorted in decreasing order of the first argument.
This is not enforced by the type but the operations here preserve it.
l.scale c scales the values in
c without modifying the order or keys.
l.get n returns the value in
l associated with key
n, if it exists, and
This function assumes that
l is sorted in decreasing order of the first argument,
that is, it will return
none as soon as it finds a key smaller than
l.zfind n returns the value associated with key
n if there is one, and 0 otherwise.
Defines a lex ordering on
linexp. This function is performance critical.
- linarith.linexp.cmp ((n1, z1) :: t1) ((n2, z2) :: t2) = ite (n1 < n2) ordering.lt (ite (n2 < n1) ordering.gt (ite (z1 < z2) ordering.lt (ite (z2 < z1) ordering.gt (linarith.linexp.cmp t1 t2))))
- linarith.linexp.cmp ((fst, snd) :: tl) list.nil = ordering.gt
- linarith.linexp.cmp list.nil (hd :: tl) = ordering.lt
- linarith.linexp.cmp list.nil list.nil = ordering.eq
The three-element type
ineq is used to represent the strength of a comparison between
max R1 R2 computes the strength of the sum of two inequalities. If
t1 R1 0 and
t2 R2 0,
t1 + t2 (max R1 R2) 0.
- linarith.ineq.lt.max linarith.ineq.lt = linarith.ineq.lt
- linarith.ineq.lt.max linarith.ineq.le = linarith.ineq.lt
- linarith.ineq.lt.max linarith.ineq.eq = linarith.ineq.lt
- linarith.ineq.le.max linarith.ineq.lt = linarith.ineq.lt
- linarith.ineq.le.max linarith.ineq.le = linarith.ineq.le
- linarith.ineq.le.max linarith.ineq.eq = linarith.ineq.le
- linarith.ineq.eq.max linarith.ineq.lt = linarith.ineq.lt
- linarith.ineq.eq.max linarith.ineq.le = linarith.ineq.le
- linarith.ineq.eq.max linarith.ineq.eq = linarith.ineq.eq
ineq is ordered
eq < le < lt.
- linarith.ineq.lt.cmp linarith.ineq.lt = ordering.eq
- linarith.ineq.lt.cmp linarith.ineq.le = ordering.gt
- linarith.ineq.lt.cmp linarith.ineq.eq = ordering.gt
- linarith.ineq.le.cmp linarith.ineq.lt = ordering.lt
- linarith.ineq.le.cmp linarith.ineq.le = ordering.eq
- linarith.ineq.le.cmp linarith.ineq.eq = ordering.gt
- linarith.ineq.eq.cmp linarith.ineq.lt = ordering.lt
- linarith.ineq.eq.cmp linarith.ineq.le = ordering.lt
- linarith.ineq.eq.cmp linarith.ineq.eq = ordering.eq
Comparisons with 0 #
The main datatype for FM elimination.
Variables are represented by natural numbers, each of which has an integer coefficient.
Index 0 is reserved for constants, i.e.
coeffs.find 0 is the coefficient of 1.
The represented term is
coeffs.sum (λ ⟨k, v⟩, v * Var[k]).
str determines the strength of the comparison -- is it < 0, ≤ 0, or = 0?
Parsing into linear form #
Auxiliary functions #
These functions are used by multiple modules, so we put them here for accessibility.