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
- linarith.linexp.get n ((a, b) :: t) = ite (a < n) option.none (ite (a = n) (option.some b) (linarith.linexp.get n t))
- linarith.linexp.get n list.nil = option.none
l.contains n is true iff
n is the first element of a pair in
l.zfind n returns the value associated with key
n if there is one, and 0 otherwise.
- linarith.linexp.zfind n l = linarith.linexp.zfind._match_1 (linarith.linexp.get n l)
- linarith.linexp.zfind._match_1 (option.some v) = v
- linarith.linexp.zfind._match_1 option.none = 0
l.vars returns the list of variables that occur in
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
- eq : linarith.ineq
- le : linarith.ineq
- lt : linarith.ineq
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
ineq as the corresponding infix symbol.
- linarith.ineq.lt.to_string = "<"
- linarith.ineq.le.to_string = "≤"
- linarith.ineq.eq.to_string = "="
Comparisons with 0 #
- str : linarith.ineq
- coeffs : linarith.linexp
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?
c.vars returns the list of variables that appear in the linear expression contained in
comp.coeff_of c a projects the coefficient of variable
a out of
- c.coeff_of a = linarith.linexp.zfind a c.coeffs
comp.scale c n scales the coefficients of
Parsing into linear form #
Auxiliary functions #
These functions are used by multiple modules, so we put them here for accessibility.