linarith: solving linear arithmetic goals

linarith is a tactic for solving goals with linear arithmetic.

Suppose we have a set of hypotheses in n variables S = {a₁x₁ + a₂x₂ + ... + aₙxₙ R b₁x₁ + b₂x₂ + ... + bₙxₙ}, where R ∈ {<, ≤, =, ≥, >}. Our goal is to determine if the inequalities in S are jointly satisfiable, that is, if there is an assignment of values to x₁, ..., xₙ such that every inequality in S is true.

Specifically, we aim to show that they are not satisfiable. This amounts to proving a contradiction. If our goal is also a linear inequality, we negate it and move it to a hypothesis before trying to prove false.

When the inequalities are over a dense linear order, linarith is a decision procedure: it will prove false if and only if the inequalities are unsatisfiable. linarith will also run on some types like ℤ that are not dense orders, but it will fail to prove false on some unsatisfiable problems. It will run over concrete types like ℕ, ℚ, and ℝ, as well as abstract types that are instances of LinearOrderedCommRing.

Algorithm sketch

First, the inequalities in the set S are rearranged into the form tᵢ Rᵢ 0, where Rᵢ ∈ {<, ≤, =} and each tᵢ is of the form ∑ cⱼxⱼ.

linarith uses an untrusted oracle to search for a certificate of unsatisfiability. The oracle searches for a list of natural number coefficients kᵢ such that ∑ kᵢtᵢ = 0, where for at least one i, kᵢ > 0 and Rᵢ = <.

Given a list of such coefficients, linarith verifies that ∑ kᵢtᵢ = 0 using a normalization tactic such as ring. It proves that ∑ kᵢtᵢ < 0 by transitivity, since each component of the sum is either equal to, less than or equal to, or less than zero by hypothesis. This produces a contradiction.

Preprocessing

linarith does some basic preprocessing before running. Most relevantly, inequalities over natural numbers are cast into inequalities about integers, and rational division by numerals is canceled into multiplication. We do this so that we can guarantee the coefficients in the certificate are natural numbers, which allows the tactic to solve goals over types that are not fields.

Preprocessors are allowed to branch, that is, to case split on disjunctions. linarith will succeed overall if it succeeds in all cases. This leads to exponential blowup in the number of linarith calls, and should be used sparingly. The default preprocessor set does not include case splits.

Fourier-Motzkin elimination

The oracle implemented to search for certificates uses Fourier-Motzkin variable elimination. This technique transforms a set of inequalities in n variables to an equisatisfiable set in n - 1 variables. Once all variables have been eliminated, we conclude that the original set was unsatisfiable iff the comparison 0 < 0 is in the resulting set.

While performing this elimination, we track the history of each derived comparison. This allows us to represent any comparison at any step as a positive combination of comparisons from the original set. In particular, if we derive 0 < 0, we can find our desired list of coefficients by counting how many copies of each original comparison appear in the history.

Implementation details

linarith homogenizes numerical constants: the expression 1 is treated as a variable t₀.

Often linarith is called on goals that have comparison hypotheses over multiple types. This creates multiple linarith problems, each of which is handled separately; the goal is solved as soon as one problem is found to be contradictory.

Disequality hypotheses t ≠ 0 do not fit in this pattern. linarith will attempt to prove equality goals by splitting them into two weak inequalities and running twice. But it does not split disequality hypotheses, since this would lead to a number of runs exponential in the number of disequalities in the context.

The Fourier-Motzkin oracle is very modular. It can easily be replaced with another function of type certificateOracle := List Comp → ℕ → TacticM ((Std.HashMap ℕ ℕ)), which takes a list of comparisons and the largest variable index appearing in those comparisons, and returns a map from comparison indices to coefficients. An alternate oracle can be specified in the LinarithConfig object.

-- TODO Not implemented yet A variant, nlinarith, adds an extra preprocessing step to handle some basic nonlinear goals. There is a hook in the linarith_config configuration object to add custom preprocessing routines.

The certificate checking step is not by reflection. linarith converts the certificate into a proof term of type false.

Some of the behavior of linarith can be inspected with the option set_option trace.linarith true. Because the variable elimination happens outside the tactic monad, we cannot trace intermediate steps there.

File structure

The components of linarith are spread between a number of files for the sake of organization.

• Lemmas.lean contains proofs of some arithmetic lemmas that are used in preprocessing and in verification.
• Datatypes.lean contains data structures that are used across multiple files, along with some useful auxiliary functions.
• Preprocessing.lean contains functions used at the beginning of the tactic to transform hypotheses into a shape suitable for the main routine.
• Parsing.lean contains functions used to compute the linear structure of an expression.
• Elimination.lean contains the Fourier-Motzkin elimination routine.
• Verification.lean contains the certificate checking functions that produce a proof of false.
• Frontend.lean contains the control methods and user-facing components of the tactic.

Tags

linarith, nlinarith, lra, nra, Fourier-Motzkin, linear arithmetic, linear programming

Control

def Linarith.getContrLemma (e : Lean.Expr) : Option (Lean.Name × Lean.Expr)

If e is a comparison a R b or the negation of a comparison ¬ a R b, found in the target, getContrLemma e returns the name of a lemma that will change the goal to an implication, along with the type of a and b.

For example, if e is (a : ℕ) < b, returns (`lt_of_not_ge, ℕ).

Equations

• One or more equations did not get rendered due to their size.

def Linarith.applyContrLemma (g : Lean.MVarId) : Lean.MetaM (Option (Lean.Expr × Lean.Expr) × Lean.MVarId)

applyContrLemma inspects the target to see if it can be moved to a hypothesis by negation. For example, a goal ⊢ a ≤ b can become a > b ⊢ false. If this is the case, it applies the appropriate lemma and introduces the new hypothesis. It returns the type of the terms in the comparison (e.g. the type of a and b above) and the newly introduced local constant. Otherwise returns none.

Equations

• One or more equations did not get rendered due to their size.

@[inline, reducible]

abbrev Linarith.ExprMultiMap (α : Type u_1) : Type u_1

A map of keys to values, where the keys are Expr up to defeq and one key can be associated to multiple values.

Equations

• Linarith.ExprMultiMap α = Array (Lean.Expr × List α)

def Linarith.ExprMultiMap.find {α : Type} (self : Linarith.ExprMultiMap α) (k : Lean.Expr) : Lean.MetaM (ℕ × List α)

Retrieves the list of values at a key, as well as the index of the key for later modification. (If the key is not in the map it returns self.size as the index.)

Equations

• One or more equations did not get rendered due to their size.

def Linarith.ExprMultiMap.insert {α : Type} (self : Linarith.ExprMultiMap α) (k : Lean.Expr) (v : α) : Lean.MetaM (Linarith.ExprMultiMap α)

Insert a new value into the map at key k. This does a defeq check with all other keys in the map.

Equations

• One or more equations did not get rendered due to their size.

def Linarith.partitionByType (l : List Lean.Expr) : Lean.MetaM (Linarith.ExprMultiMap Lean.Expr)

partitionByType l takes a list l of proofs of comparisons. It sorts these proofs by the type of the variables in the comparison, e.g. (a : ℚ) < 1 and (b : ℤ) > c will be separated. Returns a map from a type to a list of comparisons over that type.

Equations

• Linarith.partitionByType l = List.foldlM (fun m h => do let __do_lift ← Linarith.typeOfIneqProof h Linarith.ExprMultiMap.insert m __do_lift h) #[] l

def Linarith.findLinarithContradiction (cfg : Linarith.LinarithConfig) (g : Lean.MVarId) (ls : List (List Lean.Expr)) : Lean.MetaM Lean.Expr

Given a list ls of lists of proofs of comparisons, findLinarithContradiction cfg ls will try to prove false by calling linarith on each list in succession. It will stop at the first proof of false, and fail if no contradiction is found with any list.

Equations

• One or more equations did not get rendered due to their size.

def Linarith.runLinarith (cfg : Linarith.LinarithConfig) (prefType : Option Lean.Expr) (g : Lean.MVarId) (hyps : List Lean.Expr) : Lean.MetaM Unit

Given a list hyps of proofs of comparisons, runLinarith cfg hyps prefType preprocesses hyps according to the list of preprocessors in cfg. This results in a list of branches (typically only one), each of which must succeed in order to close the goal.

In each branch, we partition the list of hypotheses by type, and run linarith on each class in the partition; one of these must succeed in order for linarith to succeed on this branch. If prefType is given, it will first use the class of proofs of comparisons over that type.

Equations

• One or more equations did not get rendered due to their size.

partial def Linarith.linarith (only_on : Bool) (hyps : List Lean.Expr) (cfg : optParam Linarith.LinarithConfig { discharger := do let __do_lift ← do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure { raw := Lean.Syntax.node2 info `Mathlib.Tactic.Ring.ring1 (Lean.Syntax.atom info "ring1") (Lean.Syntax.node info `null #[]) } Lean.Elab.Tactic.evalTactic __do_lift.raw, exfalso := true, transparency := Lean.Meta.TransparencyMode.reducible, splitHypotheses := true, splitNe := false, preprocessors := none, oracle := none }) (g : Lean.MVarId) : Lean.MetaM Unit

linarith only_on hyps cfg tries to close the goal using linear arithmetic. It fails if it does not succeed at doing this.

• hyps is a list of proofs of comparisons to include in the search.
• If only_on is true, the search will be restricted to hyps. Otherwise it will use all comparisons in the local context.
• If cfg.transparency := semireducible, it will unfold semireducible definitions when trying to match atomic expressions.

User facing functions

def linarithArgsRest : Lean.ParserDescr

Syntax for the arguments of linarith, after the optional !.

Equations

• One or more equations did not get rendered due to their size.

def linarith : Lean.ParserDescr

linarith attempts to find a contradiction between hypotheses that are linear (in)equalities. Equivalently, it can prove a linear inequality by assuming its negation and proving False.

In theory, linarith should prove any goal that is true in the theory of linear arithmetic over the rationals. While there is some special handling for non-dense orders like Nat and Int, this tactic is not complete for these theories and will not prove every true goal. It will solve goals over arbitrary types that instantiate LinearOrderedCommRing.

An example:

example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0)  : False :=
by linarith

linarith will use all appropriate hypotheses and the negation of the goal, if applicable. Disequality hypotheses require case splitting and are not normally considered (see the splitNe option below).

linarith [t1, t2, t3] will additionally use proof terms t1, t2, t3.

linarith only [h1, h2, h3, t1, t2, t3] will use only the goal (if relevant), local hypotheses h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context.

linarith! will use a stronger reducibility setting to try to identify atoms. For example,

example (x : ℚ) : id x ≥ x :=
by linarith

will fail, because linarith will not identify x and id x. linarith! will. This can sometimes be expensive.

linarith (config := { .. }) takes a config object with five optional arguments:

• discharger specifies a tactic to be used for reducing an algebraic equation in the proof stage. The default is ring. Other options include simp for basic problems.
• transparency controls how hard linarith will try to match atoms to each other. By default it will only unfold reducible definitions.
• If split_hypotheses is true, linarith will split conjunctions in the context into separate hypotheses.
• If splitNe is true, linarith will case split on disequality hypotheses. For a given x ≠ y hypothesis, linarith is run with both x < y and x > y, and so this runs linarith exponentially many times with respect to the number of disequality hypotheses. (False by default.)
• If exfalso is false, linarith will fail when the goal is neither an inequality nor false. (True by default.)
• restrict_type (not yet implemented in mathlib4) will only use hypotheses that are inequalities over tp. This is useful if you have e.g. both integer and rational valued inequalities in the local context, which can sometimes confuse the tactic.

A variant, nlinarith, does some basic preprocessing to handle some nonlinear goals.

The option set_option trace.linarith true will trace certain intermediate stages of the linarith routine.

Equations

• One or more equations did not get rendered due to their size.

def tacticLinarith!_ : Lean.ParserDescr

linarith attempts to find a contradiction between hypotheses that are linear (in)equalities. Equivalently, it can prove a linear inequality by assuming its negation and proving False.

In theory, linarith should prove any goal that is true in the theory of linear arithmetic over the rationals. While there is some special handling for non-dense orders like Nat and Int, this tactic is not complete for these theories and will not prove every true goal. It will solve goals over arbitrary types that instantiate LinearOrderedCommRing.

An example:

example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0)  : False :=
by linarith

linarith will use all appropriate hypotheses and the negation of the goal, if applicable. Disequality hypotheses require case splitting and are not normally considered (see the splitNe option below).

linarith [t1, t2, t3] will additionally use proof terms t1, t2, t3.

linarith only [h1, h2, h3, t1, t2, t3] will use only the goal (if relevant), local hypotheses h1, h2, h3, and proofs t1, t2, t3. It will ignore the rest of the local context.

linarith! will use a stronger reducibility setting to try to identify atoms. For example,

example (x : ℚ) : id x ≥ x :=
by linarith

will fail, because linarith will not identify x and id x. linarith! will. This can sometimes be expensive.

linarith (config := { .. }) takes a config object with five optional arguments:

• discharger specifies a tactic to be used for reducing an algebraic equation in the proof stage. The default is ring. Other options include simp for basic problems.
• transparency controls how hard linarith will try to match atoms to each other. By default it will only unfold reducible definitions.
• If split_hypotheses is true, linarith will split conjunctions in the context into separate hypotheses.
• If splitNe is true, linarith will case split on disequality hypotheses. For a given x ≠ y hypothesis, linarith is run with both x < y and x > y, and so this runs linarith exponentially many times with respect to the number of disequality hypotheses. (False by default.)
• If exfalso is false, linarith will fail when the goal is neither an inequality nor false. (True by default.)
• restrict_type (not yet implemented in mathlib4) will only use hypotheses that are inequalities over tp. This is useful if you have e.g. both integer and rational valued inequalities in the local context, which can sometimes confuse the tactic.

A variant, nlinarith, does some basic preprocessing to handle some nonlinear goals.

The option set_option trace.linarith true will trace certain intermediate stages of the linarith routine.

Equations

• tacticLinarith!_ = Lean.ParserDescr.node `tacticLinarith!_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "linarith!" false) linarithArgsRest)

def nlinarith : Lean.ParserDescr

An extension of linarith with some preprocessing to allow it to solve some nonlinear arithmetic problems. (Based on Coq's nra tactic.) See linarith for the available syntax of options, which are inherited by nlinarith; that is, nlinarith! and nlinarith only [h1, h2] all work as in linarith. The preprocessing is as follows:

• For every subterm a ^ 2 or a * a in a hypothesis or the goal, the assumption 0 ≤ a ^ 2 or 0 ≤ a * a is added to the context.
• For every pair of hypotheses a1 R1 b1, a2 R2 b2 in the context, R1, R2 ∈ {<, ≤, =}, the assumption 0 R' (b1 - a1) * (b2 - a2) is added to the context (non-recursively), where R ∈ {<, ≤, =} is the appropriate comparison derived from R1, R2.

Equations

• One or more equations did not get rendered due to their size.

def tacticNlinarith!_ : Lean.ParserDescr

An extension of linarith with some preprocessing to allow it to solve some nonlinear arithmetic problems. (Based on Coq's nra tactic.) See linarith for the available syntax of options, which are inherited by nlinarith; that is, nlinarith! and nlinarith only [h1, h2] all work as in linarith. The preprocessing is as follows:

• For every subterm a ^ 2 or a * a in a hypothesis or the goal, the assumption 0 ≤ a ^ 2 or 0 ≤ a * a is added to the context.
• For every pair of hypotheses a1 R1 b1, a2 R2 b2 in the context, R1, R2 ∈ {<, ≤, =}, the assumption 0 R' (b1 - a1) * (b2 - a2) is added to the context (non-recursively), where R ∈ {<, ≤, =} is the appropriate comparison derived from R1, R2.

Equations

• tacticNlinarith!_ = Lean.ParserDescr.node `tacticNlinarith!_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "nlinarith!" false) linarithArgsRest)

def elabLinarithConfig : Lean.Syntax → Lean.Elab.TermElabM Linarith.LinarithConfig

Allow elaboration of LinarithConfig arguments to tactics.

Equations

• One or more equations did not get rendered due to their size.