Natural Number World

Stream: new members

[Alexander Kurz]

I am working myself througth the Naural Number World ... I love it. I am stuck at

succ (a * n + (n + a)) = succ (a * n + (a + n))

I want to swap the n+a. I have add_comm. But I dont manage to apply it in the right place. I tried all kind of variations of nth_rewrite but without success. For example, nth_rewrite 2 [add_comm] gives

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  a * n + (n + a)

while nth_rewrite 1 [add_comm] swaps the "wrong" +.

[Martin Dvořák]

I'd do rw [add_comm n a].

[Alexander Kurz]

Martin Dvořák said:

I'd do rw [add_comm n a].

Thanks, that worked!!

[Yaël Dillies]

Yes, currently nth_rw has a bug, sorry :grimacing:

[Alexander Kurz]

I expected repeat rw [mul_zero} to do the same as rw [mul_zero, mul_zero, mul_zero] in (a + b) * 0 = a * 0 + b * 0 but that is not the case. How should I think about repeat then?