Zulip Chat Archive

Stream: new members

Topic: nat.add_comm need hints for rewriting


view this post on Zulip Adrián Doña Mateo (Oct 05 2020 at 22:39):

Hi! I have only recently started learning Lean by reading Theorem Proving in Lean. I trying stuff out with inductive types and I wanted to define my own multiplication on natural numbers and prove some of its properties. However, I am having some trouble using the rewrite tactic with nat.add_comm. If you have a look at by proof of right_distrib below, you can see that I had to specify that I wanted to use commutativity of addition with the term m. If I let this hint out, the tactic would fail.

Is this what should happen? To me it seems that it should be smart enough to know where I want to apply nat.add_comm. Initially I wanted to have two of these steps in one, but simp wouldn't work with nat.add_assoc either.

Thanks!

theorem right_distrib (m n k : ) : (m + n) * k = m * k + n * k :=
begin
    induction k,
    case zero : { show (m + n) * 0 = m * 0 + n * 0, refl },
    case succ : k ih
    { show (m + n) * k.succ = m * k.succ + n * k.succ, from
            calc
                (m + n) * k.succ = (m + n) * k + (m + n)   : by rw mul_succ
                             ... = m * k + n * k + (m + n) : by rw ih
                             ... = m * k + (n * k + m) + n : by simp [nat.add_assoc]
                             ... = m * k + (m + n * k) + n : by rw nat.add_comm m
                             ... = m * k.succ + n * k.succ : by simp [nat.add_assoc, mul_succ] }
end

view this post on Zulip Mario Carneiro (Oct 05 2020 at 22:50):

This is expected behavior. rw doesn't try to guess where you want to rewrite, it always rewrites the first applicable subterm

view this post on Zulip Mario Carneiro (Oct 05 2020 at 22:51):

so you sometimes need to restrict applicable subterms by providing a partial instantiation, exactly as you've done

view this post on Zulip Mario Carneiro (Oct 05 2020 at 22:52):

You can however use simp [nat.add_comm] instead. This will work because it will rewrite all additions (on both sides of the equality) into a normal form, after which point it should be true by refl

view this post on Zulip Adrián Doña Mateo (Oct 06 2020 at 07:15):

Thanks a lot for the answer! You were right, it worked fine if I changed rw to simp. However, if I try to combine the third and fourth steps into one by removing the third one and using simp [nat.add_assoc, nat.add_comm], the tactic fails. Can you help me understand why this is?

view this post on Zulip Mario Carneiro (Oct 06 2020 at 07:16):

do you have a #mwe?

view this post on Zulip Adrián Doña Mateo (Oct 06 2020 at 07:16):

PS: It does work if I write simp [nat.add_assoc, nat.add_comm n] instead.

view this post on Zulip Adrián Doña Mateo (Oct 06 2020 at 07:18):

This works:

theorem right_distrib (m n k : ) : (m + n) * k = m * k + n * k :=
begin
    induction k,
    case zero : { show (m + n) * 0 = m * 0 + n * 0, refl },
    case succ : k ih
    { show (m + n) * k.succ = m * k.succ + n * k.succ, from
            calc
                (m + n) * k.succ = (m + n) * k + (m + n)   : by rw mul_succ
                                         ... = m * k + n * k + (m + n) : by rw ih
                                         ... = m * k + (m + n * k) + n : by simp [nat.add_assoc, nat.add_comm m]
                                         ... = m * k.succ + n * k.succ : by simp [nat.add_assoc, mul_succ] }
end

but this doesn't (only third to last line changes):

theorem right_distrib (m n k : ) : (m + n) * k = m * k + n * k :=
begin
    induction k,
    case zero : { show (m + n) * 0 = m * 0 + n * 0, refl },
    case succ : k ih
    { show (m + n) * k.succ = m * k.succ + n * k.succ, from
            calc
                (m + n) * k.succ = (m + n) * k + (m + n)   : by rw mul_succ
                                         ... = m * k + n * k + (m + n) : by rw ih
                                         ... = m * k + (m + n * k) + n : by simp [nat.add_assoc, nat.add_comm]
                                         ... = m * k.succ + n * k.succ : by simp [nat.add_assoc, mul_succ] }
end

view this post on Zulip Mario Carneiro (Oct 06 2020 at 07:18):

Due to the way simp does its normal forms, it is often not good enough to have just comm and assoc, you also need left_comm

view this post on Zulip Mario Carneiro (Oct 06 2020 at 07:19):

theorem right_distrib (m n k : ) : (m + n) * k = m * k + n * k :=
begin
    induction k,
    case zero : { show (m + n) * 0 = m * 0 + n * 0, refl },
    case succ : k ih
    { show (m + n) * k.succ = m * k.succ + n * k.succ, from
            calc
                (m + n) * k.succ = (m + n) * k + (m + n)   : by rw mul_succ
                             ... = m * k + n * k + (m + n) : by rw ih
                             ... = m * k + (m + n * k) + n : by simp [nat.add_assoc, nat.add_comm, nat.add_left_comm]
                             ... = m * k.succ + n * k.succ : by simp [nat.add_assoc, mul_succ] }

view this post on Zulip Mario Carneiro (Oct 06 2020 at 07:21):

simp will only use the rules from left to right, but it has special support for commutative-like lemmas like nat.add_comm and nat.add_left_comm, and will use it to shuffle all the addends around to a normal form. With only nat.add_comm and nat.add_assoc, it will fully right associate, and then get stuck trying to figure out how to turn b + (a + c) into a + (b + c) without using associativity backwards

view this post on Zulip Adrián Doña Mateo (Oct 06 2020 at 07:21):

I see. This works fine even without nat.add_comm. Thank you!


Last updated: May 16 2021 at 21:11 UTC