时间戳

首页 > 解决方案 > 为什么在 LEAN 的二项式定理证明中“重写”关联性失败？

proof - 为什么在 LEAN 的二项式定理证明中“重写”关联性失败？

问题描述

帝国理工学院开发的自然数博弈是一个很棒的想法，它极大地帮助了用 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策略无法在此处识别应该替换的模式，尽管它的打印与目标中出现的完全一样。在线提供的解决方案没有解释为什么会发生这种情况，而是使用了ring绕过它的策略。但是，游戏的作者说有一个解决方案，只使用rw. 你能帮我理解这里有什么问题吗？此外，任何额外的代码或提示都会很棒！我从来没有上过抽象代数课，虽然我很喜欢这个游戏并且学到了很多东西，但这里可能有些东西我没有意识到。

标签： prooftheorem-provinglean

解决方案

a * a + a * b + (a * b + b * b)实际上是(a * a + a * b) + (a * b + b * b)。如果你rw add_assoc (a * a)先，那么rw ← add_assoc (a*b) (a*b) (b*b)将工作。

当然ring，当您不玩自然数游戏时，该策略也可以解决这样的目标。

推荐阅读