0
$\begingroup$

In Macbeth's book 'The Mechanics of Proof,' the author provides a tactic called addarith to eliminate the need to write calc proofs for facts that can be derived from addition and subtraction. For example,

example {x : ℤ} (h1 : x + 4 = 2) : x = -2 := by addarith [h1]

Is an equivalent already part of mathlib4? If so, how would I find it?

(I wasn't able to find it in either the prelude or searching, but I haven't developed enough familiarity and good search patterns yet.)

$\endgroup$
1

1 Answer 1

1
$\begingroup$

There is such at tactic, it is called linarith, the following statement works for me using leanprover/lean4:v4.4.0-rc1 (but it will probably work with much older versions of mathlib4/lean4 combos):

example {x : ℤ} (h1 : x + 4 = 2) : x = -2 := by linarith

I do not think mathlib4 has expository or tutorial documentation for the existing tactics, but it does have reference documentation here: https://leanprover-community.github.io/mathlib4_docs/index.html

The Mathlib tab has a Tactics tab where you can discover the Linarith tactic as well as many other tactics for various theories, such as a ring solver.

$\endgroup$
1
  • $\begingroup$ Wonderful. Thank you, Andrew. Thanks for the pointer to the Tactics tab. $\endgroup$ Jan 1 at 21:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.