Proving commutativity of addition in Agda

Question

I'm trying to prove that addition is commutative in Agda, and I can't get it to work. Here is the relevant code, with the two troublesome goals at the bottom:

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

The goal Agda finds is

Goal: .y ≡ .y + zero

That obviously looks a lot like plus-zero, but if I don't know how to do a rewrite with .y.

The second goal is

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

If I try a rewrite with plus-suc like so:

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

I get this error:

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

I can't really make sense of this error. Any clues? I could rewrite the whole thing without implicit variables, since that seems to be making things much harder, but I was given the code as is and so I'd like to keep it like it is, if possible.

Thanks!

white_wolf white_wolf · Accepted Answer · 2018-09-11T20:37:35

You can keep the proof functions with y as an implicit argument, but you need and can use it in the definition.

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

You can also supply implicit arguments when calling a function, e.g., pcomm x {y}. The function is missing a key argument in order to complete the rewrite.

Tip: If a function has many implicit arguments and you only care about providing a specific one, you can do the following.

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

Proving commutativity of addition in Agda

1 Answers