Zulip Chat Archive

Stream: general

Topic: norm_num fails when simp is too effective


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 12 2021 at 10:16):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 12 2021 at 14:17):

#6655

view this post on Zulip Scott Morrison (Mar 12 2021 at 22:39):

Thank you!

view this post on Zulip 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