Stream: general

Topic: norm_num fails when simp is too effective

Scott Morrison (Mar 12 2021 at 10:15):

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 (Mar 12 2021 at 10:16):

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 (Mar 12 2021 at 10:16):

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

Ruben Van de Velde (Mar 12 2021 at 10:57):

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 (Mar 12 2021 at 13:38):

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

#6655

Thank you!

Scott Morrison (Mar 12 2021 at 22:42):

(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!)

Last updated: May 15 2021 at 02:11 UTC