Let us try to code the Natural Numbers ℕ (sometimes one writes Nat) from scratch.

{-# OPTIONS --without-K --safe #-}

module simplethms-1 where

For simplicity, let us just copy the definition from our experiments with the natural numbers:

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

data 𝔹 : Set where
  t : 𝔹
  f : 𝔹

Let us define addition and Multiplication of natural numbers:

_+_ : ℕ → ℕ → ℕ
zero + m = m
suc n + m = suc (n + m)

_*_ : ℕ → ℕ → ℕ
zero * m = zero
suc n * m = m + (n * m)

We observed

n : ℕ, m : ℕ ⊢ (n + m) = (m + n) --Wrong!!!

because the equal sign = is what Agda uses for definitional equality.

For The notion of propositional equality we need a new type:

infix 4 _≡_  
data _≡_ {A : Set} (x : A) : A → Set  where
  instance refl : x ≡ x

This says that for x , y : A we have a type x ≡ y corresponding to (the proposition that) x is equal to y. We judge that there is a canonical term, refl, corresponding to the fact that x ≡ x.

So, let us try to prove that addition is commutative:

is-comm+ : ∀ (n m : ℕ) → n + m ≡ m + n
is-comm+ zero m = {!!}
is-comm+ suc n m = {!!}

The first hole computes to

m ≡ m + zero

where for the left-hand side we have zero + m = m definitionally. However, for the right-hand side, Agda doesn’t know how to proceed, unless we prove it ourselves:

+0 : ∀ (x : ℕ) → x + zero ≡ x
+0 zero = refl
+0 (suc x) rewrite +0 x = refl

in the last line we are using a rewrite rule: what we do is rewrite the goal. The term +0 x reduces the situation to one where we can use the reflexivity constructor.

Also, the asymmetry in the definition of + causes x + suc y not to be definitionally equal to suc (x + y). Therefore we need another lemma to prove it:

+suc : ∀ (x y : ℕ) → x + suc y ≡ suc x + y
+suc zero y = refl
+suc (suc x) y rewrite +suc x y = refl

We have used the same technique to rewrite the goal in the last line.

Now, we can solve the first goal by using a rewrite with our first lemma. 
is-comm+ : ∀ (n m : ℕ) → n + m ≡ m + n
is-comm+ zero m rewrite (+0 m) = refl

Similarly, we use the second lemma to deal with the successor case 1. Here, we do a rewrite as above, but we need an additional step: after

is-comm+ (suc n) m rewrite +suc m n  = {!!}0

the goal is:

suc (n + m) ≡ suc (m + n)

and as you can see we have the exact statement we are proving wrapped in the suc constructor: a clear-cut case for recursively call the function is-comm+ itself, but with decreased argument:

is-comm+ (suc n) m rewrite +suc m n | is-comm+ n m = refl

The vertical bar in the above line denotes that we are rewriting using two rules (separated by the | sign).

  1. This, in another style of proof, would be the inductive step, or something closely related to it.↩︎