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 GlobalPreprocessor is a function List Expr → TacticM (List Expr). Users can add custom preprocessing steps by adding them to the LinarithConfig object. Linarith.defaultPreprocessors is the main list, and generally none of these should be skipped unless you know what you're doing.

Preprocessing

def Mathlib.Tactic.Linarith.splitConjunctions : Preprocessor

Processor that recursively replaces P ∧ Q hypotheses with the pair P and Q.

def Mathlib.Tactic.Linarith.filterComparisons : Preprocessor

Removes any expressions that are not proofs of inequalities, equalities, or negations thereof. Negations are pushed into inequalities when possible.

def Mathlib.Tactic.Linarith.isNatProp (e : Lean.Expr) : Lean.MetaM Bool

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

def Mathlib.Tactic.Linarith.isNatCoe (e : Lean.Expr) : Option (Lean.Expr × Lean.Expr)

If e is of the form ((n : ℕ) : C), isNatCoe e returns ⟨n, C⟩.

partial def Mathlib.Tactic.Linarith.getNatComparisons (e : Lean.Expr) : List (Lean.Expr × Lean.Expr)

getNatComparisons e returns a list of all subexpressions of e of the form ((t : ℕ) : C).

def Mathlib.Tactic.Linarith.mk_natCast_nonneg_prf (p : Lean.Expr × Lean.Expr) : Lean.MetaM (Option Lean.Expr)

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

def Mathlib.Tactic.Linarith.natToInt : GlobalBranchingPreprocessor

If h is an equality or inequality between natural numbers, natToInt 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.

def Mathlib.Tactic.Linarith.mkNonstrictIntProof (pf : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

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

def Mathlib.Tactic.Linarith.strengthenStrictInt : Preprocessor

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

def Mathlib.Tactic.Linarith.rearrangeComparison (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

rearrangeComparison 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 ∈ {=, ≤, <}.

def Mathlib.Tactic.Linarith.compWithZero : Preprocessor

compWithZero 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 ∈ {=, ≤, <}.

theorem Mathlib.Tactic.Linarith.without_one_mul {M : Type u_1} [MulOneClass M] {a b : M} (h : 1 * a = b) : a = b

def Mathlib.Tactic.Linarith.normalizeDenominatorsLHS (h lhs : Lean.Expr) : Lean.MetaM Lean.Expr

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

def Mathlib.Tactic.Linarith.cancelDenoms : Preprocessor

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

partial def Mathlib.Tactic.Linarith.findSquares (s : Std.TreeSet (ℕ × Bool) compare) (e : Lean.Expr) : AtomM (Std.TreeSet (ℕ × Bool) compare)

findSquares s e collects all terms of the form a ^ 2 and a * a that appear in e and adds them to the set s. A pair (i, true) is added to s when atoms[i]^2 appears in e, and (i, false) is added to s when atoms[i]*atoms[i] appears in e.

def Mathlib.Tactic.Linarith.nlinarithExtras : GlobalPreprocessor

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

partial def Mathlib.Tactic.Linarith.removeNe_aux : Lean.MVarId → List Lean.Expr → Lean.MetaM (List Branch)

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

def Mathlib.Tactic.Linarith.removeNe : GlobalBranchingPreprocessor

removeNe case splits on any proof h : a ≠ b in the input, turning it into a < b ∨ a > b, by calling linarith.removeNe_aux, provided the type has a LinearOrder instance. This produces 2^n branches when there are n such hypotheses in the input.

opaque Mathlib.Tactic.Linarith.nnrealToRealTransform : IO.Ref (List Lean.Expr → Lean.MetaM (List Lean.Expr))

Definition overridden in Mathlib.Tactic.Linarith.NNRealPreprocessor.

def Mathlib.Tactic.Linarith.nnrealToReal : GlobalPreprocessor

If h is an equality or inequality between NNReals, nnrealToReal lifts this inequality to the Reals. It also adds the facts that the reals involved are nonnegative. To avoid adding the same nonnegativity facts many times, it is a global preprocessor. This preprocessor does nothing unless Mathlib.Tactic.Linarith.NNRealPreprocessor is imported

def Mathlib.Tactic.Linarith.defaultPreprocessors : List GlobalBranchingPreprocessor

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

def Mathlib.Tactic.Linarith.preprocess (pps : List GlobalBranchingPreprocessor) (g : Lean.MVarId) (l : List Lean.Expr) : Lean.MetaM (List 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 receives 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.