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

Question

SOLVED: 我按照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)，我曾预计使用 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 会有效地将 x = x 的 RHS 替换为 LHS，得到 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 的归纳来证明这一点。

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

Agda rewrite does not change goal in _*_ commutativity proof

proof

agda

commutativity