## Stream: new members

### Topic: nat.add_comm need hints for rewriting

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


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

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

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

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

#### Mario Carneiro (Oct 06 2020 at 07:16):

do you have a #mwe?

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

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


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

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


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

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