norm_num bug

Stream: general

[Calle Sönne]

Here is what I think is a bug in norm_num:

import tactic.norm_num
import analysis.real

example : ((8 : ℕ) : ℝ) < 9 := by norm_num

"tactic failed"

[Simon Hudon]

@Mario Carneiro is norm_num supposed to handle coercions?

[Mario Carneiro]

no, or at least it has not been extended to coercions

[Simon Hudon]

That could be a nice feature

[Kevin Buzzard]

In the mean time, following the tips at https://github.com/leanprover/mathlib/blob/master/docs/extras/casts.md, you can always do this:

import tactic.norm_num
import analysis.real

example : ((8 : ℕ) : ℝ) < 9 := begin
  rw (show ((8 : ℕ) : ℝ) = (8 : ℝ), by simp),
  norm_num
end

[Nicholas Scheel]

I once made a stupid tactic to do exactly this: https://github.com/MonoidMusician/MATH361/blob/lean-3.4.1/src/naturally.lean

[Nicholas Scheel]

you can also do the same with rat