Zulip Chat Archive

Stream: general

Topic: explain behaviour of norm_num?


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

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

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

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

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

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

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

view this post on Zulip Mario Carneiro (Feb 23 2020 at 07:00):

does norm_num [max] at h not work?

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

view this post on Zulip Mario Carneiro (Feb 23 2020 at 07:01):

with true as the goal simp accidentally solves the goal

view this post on Zulip Scott Morrison (Feb 23 2020 at 07:14):

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

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

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