I am trying to define the sum of 1..n ∈ ℕ as n * (n + 1) / 2 in Agda and need a proof that n*(n + 1) is even for that. The proof is pretty simple, but there seems to be a concept I don't understand, as I am new to Agda (though neither to maths nor haskell) and learned it from http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf (pointers to more advanced tutorials more than welcome!).
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Data.Sum
-- A natural number is even, if there is a k ∈ ℕ with k * 2 = n.
data IsEven : ℕ → Set where
even : (k : ℕ) → IsEven (k * 2)
-- A product is even, if one of the factors is even.
even-product : {n m : ℕ} → IsEven n ⊎ IsEven m → IsEven (m * n)
even-product {n} {m} (inj₁ (even k)) = even (m * k)
even-product {n} {m} (inj₂ (even k)) = even (n * k)
The code returns
m != 2 of type ℕ
when checking that the expression even (k * m) has type
IsEven (k * 2 * m)
I already tried using with patterns to convince the compiler that k * 2 is in fact n, but to no avail. Switching m * k to k * m gives
k * m != m of type ℕ
when checking that the expression even (k * m) has type
IsEven (m * (k * 2))
You can find out what the problem is by putting {! !} markers around your attempted solution and using the C-c C-. shortcut.
even-product : {n m : ℕ} → IsEven n ⊎ IsEven m → IsEven (m * n)
even-product {n} {m} (inj₁ (even k)) = {!even (m * k)!}
even-product {n} {m} (inj₂ (even k)) = {!even (n * k)!}
Reloading the file and then pressing C-c C-. with your cursor in the first hole gives the following response:
Goal: IsEven (m * (k * 2))
Have: IsEven (m * k * 2)
————————————————————————————————————————————————————————————
n : ℕ
m : ℕ
k : ℕ
Now the problem is clear: the goal is to prove that (m * (k * 2)) is even, but you have a proof that (m * k * 2) is even.
To fix this problem, you have to use the fact that * is associative. I'll postulate it here by means of example, but obviously you'd want to give it an actual proof later.
postulate
*-assoc : (k l m : ℕ) → k * (l * m) ≡ (k * l) * m
Now we can use the rewrite keyword with *-assoc to fix the first case:
even-product : {n m : ℕ} → IsEven n ⊎ IsEven m → IsEven (m * n)
even-product {n} {m} (inj₁ (even k)) rewrite *-assoc m k 2 = even (m * k)
even-product {n} {m} (inj₂ (even k)) = {!even (n * k)!}
In the second case, C-c C-. gives the following response:
Goal: IsEven (k * 2 * n)
Have: IsEven (n * k * 2)
————————————————————————————————————————————————————————————
m : ℕ
n : ℕ
k : ℕ
So now you need to use commutativity of * as well as associativity. I'll leave the full solution as an exercise to the reader.