Agda 重写不会改变 _*_ 交换性证明中的目标
Agda rewrite does not change goal in _*_ commutativity proof
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
的工作原理还是我犯了其他错误?
您的目标是 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
的归纳来证明这一点。
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
的工作原理还是我犯了其他错误?
您的目标是 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
的归纳来证明这一点。