mathlib documentation

tactic.linarith.parsing

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 3*(x*y), where the monomial x*y is the linear atom.

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. The resulting 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.

Parsing datatypes #

@[reducible]
meta def linarith.monom  :
Type

Variables (represented by natural numbers) map to their power.

1 is represented by the empty monomial, the product of no variables.

@[reducible]
meta def linarith.monom.lt  :

Compare monomials by first comparing their keys and then their powers.

@[protected, instance]
@[reducible]
meta def linarith.sum  :
Type

Linear combinations of monomials are represented by mapping monomials to coefficients.

1 is represented as the singleton sum of the monomial monom.one with coefficient 1.

sum.scale_by_monom s m multiplies every monomial in s by m.

sum.mul s1 s2 distributes the multiplication of two sums.`

The nth power of s : sum is the n-fold product of s, with s.pow 0 = sum.one.

sum_of_monom m lifts m to a sum with coefficient 1.

The unit monomial one is represented by the empty rb map.

meta def linarith.scalar (z : ) :

A scalar z is represented by a sum with coefficient z and monomial one

meta def linarith.var (n : ) :

A single variable n is represented by a sum with coefficient 1 and monomial n.

Parsing algorithms #

linear_form_of_atom red map e is the atomic case for linear_form_of_expr. If e appears with index k in map, it returns the singleton sum var k. Otherwise it updates map, adding e with index n, and returns the singleton sum var n.

linear_form_of_expr red map e computes the linear form of e.

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 red.

Because it matches up to definitional equality, this function must be in the tactic monad, and forces some functions that call it into tactic as well.

sum_to_lf s map eliminates the monomial level of the sum s.

map is a lookup map from monomials to variable numbers. The output rb_map ℕ ℤ has the same structure as sum, but each monomial key is replaced with its index according to map. 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 into a comp object.

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 to_comp over exprs, updating e_map and 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 c of comps of the same length, such that c[i] represents the linear form of the type of pfs[i].

It also returns the largest variable index that appears in comparisons in c.