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
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 RuteOct 27 at 1:12
-
$\begingroup$ thanks. that is fine $\endgroup$– Tim EricOct 27 at 1:19
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
3
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.
-
-
-
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$ Oct 29 at 4:35