1
$\begingroup$

It should be simple but dig it for a while and still not successful. theorem example (a : R) : 2 + 2 + a = 4 + a := ...

can someone help to figure out how to do next? many thanks

$\endgroup$
2
  • 1
    $\begingroup$ I recommend learning a bit about MWEs. There is a good website on MWEs in Lean. In particular, use triple backquotes for code and provide all imports (say for the real numbers in your example). $\endgroup$
    – Jason Rute
    Oct 27, 2023 at 1:12
  • $\begingroup$ thanks. that is fine $\endgroup$
    – Tim Eric
    Oct 27, 2023 at 1:19

1 Answer 1

1
$\begingroup$

norm_num is a good tactic for this sort of stuff:

import Mathlib.Tactic.NormNum
import Mathlib.Data.Real.Basic

example (a : ℝ) : 2 + 2 + a = 4 + a := by norm_num

(I couldn't find the tactic documentation for Lean 4, so I gave you the documentation for norm_num in Lean 3.). But in short, norm_num normalizes both sides of this equation. It works in many places that rfl can't work.

$\endgroup$
3
  • $\begingroup$ thanks. it works. $\endgroup$
    – Tim Eric
    Oct 27, 2023 at 1:18
  • $\begingroup$ What does norm_num do? $\endgroup$ Oct 29, 2023 at 3:49
  • 1
    $\begingroup$ @AgnishomChattopadhyay I believe it uses various rewrite rules to simplify the expression efficiently. In particular, I think it uses binary to represent integers (even integer real numbers like in this example). I know it’s also extensible and you can mark lemmas to be used in norm_num. This allows you to use norm_num on custom functions or even custom types. I think for more details it’s best to ask a question here or on the lean Zulip, since I don’t know. $\endgroup$
    – Jason Rute
    Oct 29, 2023 at 4:35

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.