explain behaviour of norm_num?

Stream: general

[Scott Morrison]

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]

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]

You should be able to explicitly rewrite with this and then use norm_num to prove the rest

[Scott Morrison]

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]

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 nats (or ints or something), what's the least effort simplifier?

[Mario Carneiro]

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]

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]

does norm_num [max] at h not work?

[Mario Carneiro]

This works for me:

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

[Mario Carneiro]

with true as the goal simp accidentally solves the goal

[Scott Morrison]

okay, using norm_num [max] at h does indeed work.

[Scott Morrison]

I can work around conv at h { norm_num [max] } not working, but I do worry that that is a bug

[Mario Carneiro]

Using conv at h {norm_num [max]} repeatedly makes progress, so there must be something wrong with the repeat ending early