nat.add_comm need hints for rewriting

Stream: new members

[Adrián Doña Mateo]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

do you have a #mwe?

[Adrián Doña Mateo]

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

[Adrián Doña Mateo]

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]

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]

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]

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]

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