linarith

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

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.

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 {discharger := tac, restrict_type := tp, exfalso := ff} 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 currently include ring SOP or simp for basic problems.
• restrict_type 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.
• 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 exfalso is false, linarith will fail when the goal is neither an inequality nor false. (True by default.)

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.

nlinarith

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.

omega

omega attempts to discharge goals in the quantifier-free fragment of linear integer and natural number arithmetic using the Omega test. In other words, the core procedure of omega works with goals of the form

∀ x₁, ... ∀ xₖ, P

where x₁, ... xₖ are integer (resp. natural number) variables, and P is a quantifier-free formula of linear integer (resp. natural number) arithmetic. For instance:

example : ∀ (x y : int), (x ≤ 5 ∧ y ≤ 3) → x + y ≤ 8 := by omega

By default, omega tries to guess the correct domain by looking at the goal and hypotheses, and then reverts all relevant hypotheses and variables (e.g., all variables of type nat and Props in linear natural number arithmetic, if the domain was determined to be nat) to universally close the goal before calling the main procedure. Therefore, omega will often work even if the goal is not in the above form:

example (x y : nat) (h : 2 * x + 1 = 2 * y) : false := by omega

But this behaviour is not always optimal, since it may revert irrelevant hypotheses or incorrectly guess the domain. Use omega manual to disable automatic reverts, and omega int or omega nat to specify the domain.

example (x y z w : int) (h1 : 3 * y ≥ x) (h2 : z > 19 * w) : 3 * x ≤ 9 * y :=
by {revert h1 x y, omega manual}

example (i : int) (n : nat) (h1 : i = 0) (h2 : n < n) : false := by omega nat

example (n : nat) (h1 : n < 34) (i : int) (h2 : i * 9 = -72) : i = -8 :=
by {revert h2 i, omega manual int}

omega handles nat subtraction by repeatedly rewriting goals of the form P[t-s] into P[x] ∧ (t = s + x ∨ (t ≤ s ∧ x = 0)), where x is fresh. This means that each (distinct) occurrence of subtraction will cause the goal size to double during DNF transformation.

omega implements the real shadow step of the Omega test, but not the dark and gray shadows. Therefore, it should (in principle) succeed whenever the negation of the goal has no real solution, but it may fail if a real solution exists, even if there is no integer/natural number solution.

You can enable set_option trace.omega true to see how omega interprets your goal.