Proof that addition (of Peano numbers) is associative in Agda.

Peano.agda

module Peano where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ
zero + x     = x
(suc x) + y = suc (x + y)

+-assoc : ∀ (a b c : ℕ) → (a + b) + c ≡ a + (b + c)
+-assoc zero b c = refl
+-assoc (suc a) b c =
  begin
    (suc a + b) + c
  ≡⟨⟩
    suc (a + b) + c
  ≡⟨⟩
    suc ((a + b) + c)
  ≡⟨ cong suc (+-assoc a b c) ⟩
    suc (a + (b + c))
  ≡⟨⟩
    suc a + (b + c)
  ∎

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

ack : ℕ → ℕ → ℕ
ack zero n          = n + 1
ack (suc m) zero    = ack m 1
ack (suc m) (suc n) = ack m (ack (suc m) n)