Parsing input expressions into linear form
linarith computes the linear form of its input expressions,
assuming (without justification) that the type of these expressions
is a commutative semiring.
It identifies atoms up to ring-equivalence: that is,
(y*3)*x will be identified
where the monomial
x*y is the linear atom.
- Variables are represented by natural numbers.
- Monomials are represented by
monom := rb_map ℕ ℕ. The monomial
1is represented by the empty map.
- Linear combinations of monomials are represented by
sum := rb_map monom ℤ.
All input expressions are converted to
sums, preserving the map from expressions to variables.
We then discard the monomial information, mapping each distinct monomial to a natural number.
rb_map ℕ ℤ represents the ring-normalized linear form of the expression.
This is ultimately converted into a
linexp in the obvious way.
linear_forms_and_vars is the main entry point into this file. Everything else is contained.
Variables (represented by natural numbers) map to their power.
Linear combinations of monomials are represented by mapping monomials to coefficients.
linear_form_of_atom red map e is the atomic case for
e appears with index
map, it returns the singleton sum
Otherwise it updates
e with index
n, and returns the singleton sum
linear_form_of_expr red map e computes the linear form of
map is a lookup map from atomic expressions to variable numbers.
If a new atomic expression is encountered, it is added to the map with a new number.
It matches atomic expressions up to reducibility given by
sum_to_lf s map eliminates the monomial level of the
map is a lookup map from monomials to variable numbers.
rb_map ℕ ℤ has the same structure as
but each monomial key is replaced with its index according to
If any new monomials are encountered, they are assigned variable numbers and
map is updated.
to_comp red e e_map monom_map converts an expression of the form
t < 0,
t ≤ 0, or
t = 0
e_map maps atomic expressions to indices;
monom_map maps monomials to indices.
Both of these are updated during processing and returned.
to_comp_fold red e_map exprs monom_map folds
monom_map as it goes.
linear_forms_and_vars red pfs is the main interface for computing the linear forms of a list
of expressions. Given a list
pfs of proofs of comparisons, it produces a list
the same length, such that
c[i] represents the linear form of the type of
It also returns the largest variable index that appears in comparisons in