2

已解决：在遵循white-wolf的建议后，我有一个解决方案。如果您对我的解决方案感兴趣，请随时给我留言。

我正在尝试在 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)，我曾预计 usingrewrite会给我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对于 x = x, give ，将有效地将 RHS 替换为 LHS，y * suc x ≡ y * suc x然后使用 x = suc x give y * suc (suc x) ≡ y * suc (suc x)。我是否误解了rewrite工作原理还是犯了其他错误？

4

1 回答 1

3

你的目标是y + y * suc x ≡ y * suc (suc x)。你的归纳假设是y + y * x ≡ y * suc x。我可以通过pr3b x y输入目标并输入 Cc 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.

于 2018-08-06T17:37:58.507 回答