proof - Agda 重写不会改变 _*_ 交换性证明中的目标

Question

已解决:在遵循白狼的建议后，我有了一个解决方案。如果您对我的解决方案感兴趣，请随时给我留言。

---

我正在尝试用 Agda 编写乘法交换律的证明:

lem3 : (x y : ℕ) → (x * y) ≡ (y * x)
lem3 0 y rewrite pr3a y = refl
lem3 (suc x) y rewrite lem3 x y | pr3b x y = refl

我们有:

pr3a : (x : ℕ) → (x * 0) ≡ 0
pr3a 0 = refl
pr3a (suc x) with (x * 0) | pr3a x
... | .0 | refl = refl

pr3b : (x y : ℕ) →  y + y * x ≡ y * suc x
pr3b 0 0 = refl
pr3b 0 (suc y) rewrite pr3b 0 y = refl
pr3b (suc x) y = {!!}

我在实现这个最终目标时遇到了困难。预期类型为 y + y * suc x ≡ y * suc (suc x) ，我预计使用 rewrite会给我y * suc (suc x) ≡ y * suc (suc x)作为目标。但是:

pr3b (suc x) y rewrite pr3b x y = {!!}

期望与之前相同的目标:y + y * suc x ≡ y * suc (suc x) .

据我了解rewrite可以有效地将 RHS 替换为 LHS，得到 x = x，给出 y * suc x ≡ y * suc x ，然后使用 x = suc x 给出 y * suc (suc x) ≡ y * suc (suc x) 。我是否误解了如何rewrite有效还是我犯了其他错误？

Answer 1

您的目标是y + y * suc x ≡ y * suc (suc x)。你的归纳假设是y + y * x ≡ y * suc x。我可以通过将 pr3b x y 放入目标中并输入 C-c C- 来检查这一点。

Goal: y + y * suc x ≡ y * suc (suc x)
Have: y + y * x ≡ y * suc x

这意味着通过重写，您应该能够将 y * suc x 替换为 y * x。然而，你看到两侧被交换了，所以你必须像这样对称地重写

pr3b : (x y : ℕ) →  y + y * x ≡ y * suc x
pr3b 0 0 = refl
pr3b 0 (suc y) rewrite pr3b 0 y = refl
pr3b (suc x) y rewrite sym $ pr3b x y = {!!}

这将目标提升为y + (y + y * x) ≡ y * suc (suc x)。这个特殊的证明需要完成加法的结合律和交换律。

编辑

我认为你应该尝试通过对 y 而不是 x 进行归纳来证明这一点。