# Zulip Chat Archive

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