norm_num

Summary

The norm_num tactic solves equalities and inequalities which involve only normalised numerical expressions. It doesn’t deal with variables, but it will prove things like A = B, A ≤ B, A < B and A ≠ B, as long as A and B involve only numbers like -37/5.

Examples

(with data.real.basic imported to get the reals, and of course tactic imported to get the tactics)

example : (1 : ℝ) + 1 = 2 :=
begin
  norm_num,
end

example : (1 : ℝ) + 1 ≤ 3 :=
begin
  norm_num,
end

example : (1 : ℝ) + 1 < 4 :=
begin
  norm_num,
end

example : (1 : ℝ) + 1 ≠ 5 :=
begin
  norm_num,
end

I put a comma after norm_num so that I can check that the “goals accomplished” message is there.

norm_num also knows about a few other things; for example it seems to know about the absolute value on the real numbers.

example : |(3 : ℝ) - 7| = 4 :=
begin
  norm_num,
end