norm_cast needs extra help with inequalities

Stream: new members

[Rado Kirov]

This was a bit surprising to me

import Mathlib

example {n: ℕ} (h: n > 1): (((n - 1): ℕ): ℝ) = (n: ℝ) - (1:ℝ) := by norm_cast -- error
example {n: ℕ} (h: n ≥ 1): (((n - 1): ℕ): ℝ) = (n: ℝ) - (1:ℝ) := by norm_cast -- ok

-- easy work around, but quite hard to make a lucky guess what would help norm_cast
example {n: ℕ} (h: n > 1): (((n - 1): ℕ): ℝ) = (n: ℝ) - (1:ℝ) := by
  have := h.le
  norm_cast

Is this a bug or a reasonable feature request for norm_cast or WAE?

[Kevin Buzzard]

That looks like feature creep to me for norm_cast (its job is not to figure out side goals) but I agree that the current situation is not ideal. As a rule I avoid natural subtraction like the plague.

[Kevin Buzzard]

I guess it would not be unreasonable to have a norm_cast! which leaves n >= 1 as a new goal, and then linarith or omega could take it from there.

[Robin Arnez]

Or maybe allow providing a discharger?