# Zulip Chat Archive

## 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

#### Mario Carneiro (Mar 12 2021 at 14:17):

#### Scott Morrison (Mar 12 2021 at 22:39):

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