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

Improve this question
$\endgroup$
1

1 Answer 1

Reset to default
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.

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

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