# Zulip Chat Archive

## Stream: general

### Topic: explain behaviour of norm_num?

#### Scott Morrison (Feb 23 2020 at 03:13):

In

import tactic.norm_num example (n : ℕ) (h : n = max (max ⊥ 2) 3 + 1) : true := begin conv at h { norm_num, }, trivial, end

The invocation of `norm_num`

converts `max (max ⊥ 2) 3 + 1`

to `1 + max 2 3`

. Why? I really wish it would do a little more, and give me just `n = 4`

.

#### Mario Carneiro (Feb 23 2020 at 03:44):

`norm_num`

doesn't know about `max`

. Unfortunately it doesn't interact optimally with simp when it comes to applying conditional rewrite rules and proving the side conditions (like `a <= b -> max a b = b`

in this case).

#### Mario Carneiro (Feb 23 2020 at 03:44):

You should be able to explicitly rewrite with this and then use `norm_num`

to prove the rest

#### Scott Morrison (Feb 23 2020 at 05:18):

Ah! I was confused how `norm_num`

was doing anything, but of course it was just the internal call to `simp`

that made progress.

#### Scott Morrison (Feb 23 2020 at 05:21):

Hmm... so if I'm expecting to expressions which look like `max (max (max a b) c) d`

to some arbitrary depth, and all arguments explicit `nat`

s (or `int`

s or something), what's the least effort simplifier?

#### Mario Carneiro (Feb 23 2020 at 05:30):

I think if you rewrite with `max`

, it will unfold to the if definition, then norm_num will be able to simplify the target to true or false, then simp will make progress. So `norm_num [max]`

should do the trick

#### Scott Morrison (Feb 23 2020 at 06:47):

oh... oops. I thought this was working, but it's not.

import tactic.norm_num example (n : ℕ) (h : n = max (max ⊥ 2) 3 + 1) : true := begin conv at h { norm_num [max], }, trivial, end

just gives `h : n = 1 + ite (2 ≤ 3) 3 2`

.

#### Mario Carneiro (Feb 23 2020 at 07:00):

does `norm_num [max] at h`

not work?

#### Mario Carneiro (Feb 23 2020 at 07:01):

This works for me:

example (n : ℕ) (h : n = max (max ⊥ 2) 3 + 1) : false := begin norm_num [max] at h, end

#### Mario Carneiro (Feb 23 2020 at 07:01):

with `true`

as the goal `simp`

accidentally solves the goal

#### Scott Morrison (Feb 23 2020 at 07:14):

okay, using `norm_num [max] at h`

does indeed work.

#### Scott Morrison (Feb 23 2020 at 07:15):

I can work around `conv at h { norm_num [max] }`

not working, but I do worry that that is a bug

#### Mario Carneiro (Feb 23 2020 at 07:15):

Using `conv at h {norm_num [max]}`

repeatedly makes progress, so there must be something wrong with the repeat ending early

Last updated: May 14 2021 at 03:27 UTC