Игра с натуральными числами , разработанная в Имперском колледже, - отличная идея, которая очень помогла с основами написания корректур в LEAN. Однако после прохождения большей части из них возникает «дополнительная» проблема, которую я пока не могу понять. Ниже приведена упрощенная версия этой проблемы, которая может быть помещена в пустой файл и может быть запущена автономно в 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
rw tacti c не может распознать здесь шаблон, который должен быть заменен, хотя он печатается именно так, как он отображается в цели. Предлагаемое онлайн решение не объясняет, почему это происходит, вместо этого вместо ring tacti c до go. Тем не менее, автор игры говорит, что есть решение, которое использует только rw. Можете ли вы помочь мне понять, в чем здесь проблема? Кроме того, любой дополнительный код или подсказка к go мимо было бы здорово! Я никогда не учился на уроках абстрактной алгебры, и хотя я наслаждался игрой и многому научился, могут быть вещи, которые я не могу распознать здесь.