Lean4
/-- `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 `CommRing`, `LinearOrder` and `IsStrictOrderedRing`.
An example:
```lean
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,
```lean
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 `splitHypotheses` 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.
-/
@[tactic_parser 1000]
public meta def linarith : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.linarith 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "linarith" false✝)
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "!")))
Mathlib.Tactic.linarithArgsRest)
