mathlib3 documentation

tactic.linarith.preprocessing

Linarith preprocessing #

This file contains methods used to preprocess inputs to linarith.

In particular, linarith works over comparisons of the form t R 0, where R ∈ {<,≤,=}. It assumes that expressions in t have integer coefficients and that the type of t has well-behaved subtraction.

Implementation details #

A global_preprocessor is a function list expr → tactic(list expr). Users can add custom preprocessing steps by adding them to the linarith_config object. linarith.default_preprocessors is the main list, and generally none of these should be skipped unless you know what you're doing.

Preprocessing #

meta def linarith.rem_neg (prf : expr) :

expr → tactic expr

If prf is a proof of ¬ e, where e is a comparison, rem_neg prf e flips the comparison in e and returns a proof. For example, if prf : ¬ a < b, rem_neg prf `(a < b) returns a proof of a ≥ b.

meta def linarith.rearr_comp (e : expr) :

rearr_comp e takes a proof e of an equality, inequality, or negation thereof, and turns it into a proof of a comparison _ R 0, where R ∈ {=, ≤, <}.

meta def linarith.is_nat_int_coe :

expr → option expr

If e is of the form ((n : ℕ) : ℤ), is_nat_int_coe e returns n : ℕ.

meta def linarith.mk_coe_nat_nonneg_prf (e : expr) :

If e : ℕ, returns a proof of 0 ≤ (e : ℤ).

meta def linarith.get_nat_comps :

expr → list expr

get_nat_comps e returns a list of all subexpressions of e of the form ((t : ℕ) : ℤ).

meta def linarith.mk_non_strict_int_pf_of_strict_int_pf (pf : expr) :

If pf is a proof of a strict inequality (a : ℤ) < b, mk_non_strict_int_pf_of_strict_int_pf pf returns a proof of a + 1 ≤ b, and similarly if pf proves a negated weak inequality.

meta def linarith.is_nat_prop :

is_nat_prop tp is true iff tp is an inequality or equality between natural numbers or the negation thereof.

meta def linarith.is_strict_int_prop :

is_strict_int_prop tp is true iff tp is a strict inequality between integers or the negation of a weak inequality between integers.

meta def linarith.filter_comparisons :

linarith.preprocessor

Removes any expressions that are not proofs of inequalities, equalities, or negations thereof.

meta def linarith.remove_negations :

linarith.preprocessor

Replaces proofs of negations of comparisons with proofs of the reversed comparisons. For example, a proof of ¬ a < b will become a proof of a ≥ b.

meta def linarith.nat_to_int :

linarith.global_preprocessor

If h is an equality or inequality between natural numbers, nat_to_int lifts this inequality to the integers. It also adds the facts that the integers involved are nonnegative. To avoid adding the same nonnegativity facts many times, it is a global preprocessor.

meta def linarith.strengthen_strict_int :

linarith.preprocessor

strengthen_strict_int h turns a proof h of a strict integer inequality t1 < t2 into a proof of t1 ≤ t2 + 1.

meta def linarith.make_comp_with_zero :

linarith.preprocessor

mk_comp_with_zero h takes a proof h of an equality, inequality, or negation thereof, and turns it into a proof of a comparison _ R 0, where R ∈ {=, ≤, <}.

meta def linarith.normalize_denominators_in_lhs (h lhs : expr) :

normalize_denominators_in_lhs h lhs assumes that h is a proof of lhs R 0. It creates a proof of lhs' R 0, where all numeric division in lhs has been cancelled.

meta def linarith.cancel_denoms :

linarith.preprocessor

cancel_denoms pf assumes pf is a proof of t R 0. If t contains the division symbol /, it tries to scale t to cancel out division by numerals.

meta def linarith.find_squares :

native.rb_set (expr × bool) → expr → tactic (native.rb_set (expr ×ₗ bool))

find_squares m e collects all terms of the form a ^ 2 and a * a that appear in e and adds them to the set m. A pair (a, tt) is added to m when a^2 appears in e, and (a, ff) is added to m when a*a appears in e.

meta def linarith.nlinarith_extras :

linarith.global_preprocessor

nlinarith_extras is the preprocessor corresponding to the nlinarith tactic.

For every term t such that t^2 or t*t appears in the input, adds a proof of t^2 ≥ 0 or t*t ≥ 0.
For every pair of comparisons t1 R1 0 and t2 R2 0, adds a proof of t1*t2 R 0.

This preprocessor is typically run last, after all inputs have been canonized.

meta def linarith.remove_ne_aux :

list expr → tactic (list linarith.branch)

remove_ne_aux case splits on any proof h : a ≠ b in the input, turning it into a < b ∨ a > b. This produces 2^n branches when there are n such hypotheses in the input.

meta def linarith.remove_ne :

linarith.global_branching_preprocessor

remove_ne case splits on any proof h : a ≠ b in the input, turning it into a < b ∨ a > b, by calling linarith.remove_ne_aux. This produces 2^n branches when there are n such hypotheses in the input.

meta def linarith.default_preprocessors :

list linarith.global_branching_preprocessor

The default list of preprocessors, in the order they should typically run.

meta def linarith.preprocess (pps : list linarith.global_branching_preprocessor) (l : list expr) :

tactic (list linarith.branch)

preprocess pps l takes a list l of proofs of propositions. It maps each preprocessor pp ∈ pps over this list. The preprocessors are run sequentially: each recieves the output of the previous one. Note that a preprocessor may produce multiple or no expressions from each input expression, so the size of the list may change.