The Natural Number Game developed at Imperial College is a great idea that helped tremendously with the basics of proof writing in LEAN. After going through most of it there is however an "extra" problem that I can't figure out yet. Below is a stripped-down version of this problem that can be placed in an empty file and can be run stand-alone in LEAN.
open nat
lemma two_eq_succ_one : 2 = succ(1) := rfl
lemma one_eq_succ_zero : 1 = succ(0) := rfl
theorem add_squared (a b : ℕ) :
(a + b) ^ (2 : ℕ) = a ^ (2 : ℕ) + b ^ (2 : ℕ) + (2 : ℕ) * a * b :=
begin
rw two_eq_succ_one,
rw pow_succ (a+b) 1,
rw pow_one (a+b),
rw mul_add (a+b) a b,
rw add_mul a b a,
rw add_mul a b b,
rw ← mul_comm a b,
-- uncomment the rw below to see it fails
--rw ← add_assoc (a*b) (a*b) (b*b),
end
The rw tactic fails to recognize here the pattern that should be replaced, although it is printed exactly as it appears in the goal. The solution offered online does not explain why this happens, using instead the ring tactic to go past it. However, the author of the game says that there is a solution that only uses rw. Can you help me understand what is the problem here? Also any extra code or hint to go past it would be great! I never took an abstract algebra class and although I enjoyed the game and learned a lot, there may be things that I fail to recognize here.
a * a + a * b + (a * b + b * b) is actually (a * a + a * b) + (a * b + b * b). If you rw add_assoc (a * a) first, then rw ← add_assoc (a*b) (a*b) (b*b) will work.
Of course, the ring tactic will solves goals like this as well, when you're not playing the natural number game.