为什么这段代码在 agda 中不起作用？

Question

我试图在乘法运算中证明自然数的交换性。

--proving comm over *
*comm : ∀ a b → (a * b) ≡ (b * a)
*comm zero b = sym (rightId* b)
*comm (suc a) b = {!!}

当我检查目标时，我发现它是b + a * b ≡ b * suc a。所以我证明了这一点。

lemma*-swap : ∀ a b → a + a * b ≡ a * suc b

现在当我尝试时：

*comm : ∀ a b → (a * b) ≡ (b * a)
*comm zero b = sym (rightId* b)
*comm (suc a) b = lemma*-swap b a

这应该可以满足目标，但为什么这不起作用？请建议我哪里错了。

Answer 1

b + a * b（目标中的表达式）和a + a * b（lemma*-swap 中的表达式）是不同的，因此应用lemma*-swap 不满足目标。

你需要rewrite归纳假设*comm a b把a * b变成目标中的b * a，这样lemma*-swap b a就可以用来排放目标了。