norm_num fails when simp is too effective

Stream: general

[Scott Morrison]

Sometimes when the simp set becomes too powerful, and can reduce a hypothesis to false, norm_num can no longer close goals.

Here's an example:

import tactic.linarith

example (n : ℕ) (h : 2 ≤ n) (w : n < 2): false :=
begin
  rcases n with _|_|n,
  { norm_num at h, }, -- works great
  { norm_num at h, },
  { simp [nat.succ_eq_add_one] at w, linarith, },
end

-- I would like to have this as a simp lemma:
attribute [simp] nat.bit0_ne_zero

example (n : ℕ) (h : 2 ≤ n) (w : n < 2): false :=
begin
  rcases n with _|_|n,
  { norm_num at h, }, -- we end up with `h : false`, but the goal is still open
  { norm_num at h, },
  { simp [nat.succ_eq_add_one] at w, linarith, },
end

[Scott Morrison]

I was hoping to be able to make norm_num a bit more robust, so that if its internal calls to the simplifier reduced a hypothesis to false, it could always make use of that. However I've never fully understood the inner workings of norm_num, and couldn't work this out.

[Scott Morrison]

Any advice, e.g. from @Mario Carneiro?

[Ruben Van de Velde]

Thanks for bringing this up, I just ran into something like that this week when some of my proofs broke after updating mathlib

[Mario Carneiro]

This looks like an issue in src#tactic.norm_num1. When the hypothesis simplifies to false, we attempt a call to tactic.contradiction which is what closes the goal. But when the hypothesis is already false, the simplify fails and so does norm_num (because there was nothing to simplify), and we don't perform cleanup actions

[Mario Carneiro]

#6655

[Scott Morrison]

Thank you!

[Scott Morrison]

(it's just amazing to work with a system which, from top to bottom, is continually improving, and in a community where questions and requests receive so much help!)