在 Agda 中证明加法的交换性

Question

我试图证明在 Agda 中加法是可交换的，但我无法让它工作。下面是相关代码，底部有两个麻烦的目标：

cong : ∀{A B : Set} (f : A → B) {x y : A} (eq : x ≡ y) → f x ≡ f y
cong f refl = refl

plus-assoc : ∀ x {y z} → (x + y) + z ≡ x + (y + z)
plus-assoc zero = refl
plus-assoc (suc x) = cong suc (plus-assoc x)

plus-zero : ∀ x → x + zero ≡ x
plus-zero zero = refl
plus-zero (suc x) rewrite plus-zero x = refl

plus-suc : ∀ x {y} → x + suc y ≡ suc (x + y)
plus-suc zero = refl
plus-suc (suc x) = cong suc (plus-suc x)

plus-comm : ∀ x {y} → x + y ≡ y + x
plus-comm zero = { }0
plus-comm (suc x) = { }1

Agda 找到的目标是

Goal: .y ≡ .y + zero

这显然看起来很像加零，但如果我不知道如何用 .y 进行重写。

第二个目标是

Goal: suc (x + .y) ≡ .y + suc x
——————————————————————————————————————————
.y : Nat
x  : Nat

如果我尝试像这样用 plus-suc 重写：

plus-comm (suc x) rewrite plus-suc x = { }1

我收到此错误：

Cannot rewrite by equation of type {y : Nat} →
                               x + suc y ≡ suc (x + y)
when checking that the clause
plus-comm (suc x) rewrite plus-suc x = ? has type
(x : Nat) {y : Nat} → x + y ≡ y + x

我真的无法理解这个错误。有什么线索吗？我可以在不使用隐式变量的情况下重写整个内容，因为这似乎使事情变得更加困难，但我得到的是原样的代码，所以如果可能的话，我想保持原样。

谢谢！

Answer 1

您可以使用 y 作为隐式参数保留证明函数，但您需要并且可以在定义中使用它。

pcomm : ∀ x {y} → x + y ≡ y + x
pcomm zero {y} = {!!}
pcomm (suc x) {y} = {!!} 

您还可以在调用函数时提供隐式参数，例如，pcomm x {y}。该函数缺少一个关键参数以完成重写。

提示：如果一个函数有很多隐式参数，而您只关心提供一个特定参数，则可以执行以下操作。

-- f {C = X}
f : ∀ {A B C : Set} → Set
f {C = C} = C