Commutativity of addition in Agda (for autumn school)

com.agda

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

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

trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl

sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

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

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


infix 4 _≡_
infixr 6 _+_


module Proof1 where
  com : ∀ n m → n + m ≡ m + n
  com zero zero = refl
  com zero (suc m) = cong suc (com zero m)
  com (suc n) zero = cong suc (com n zero)
  com (suc n) (suc m) = cong suc (trans p q)
    where
      -- This is the right-handed version of addition
      p : n + suc m ≡ suc (m + n)
      p = com n (suc m)
      -- Lemma
      suc≡ : ∀ n m → suc (n + m) ≡ n + suc m
      suc≡ zero m = refl
      suc≡ (suc n) m = cong suc (suc≡ n m)
      -- This is the counterpart to p
      q : suc (m + n) ≡ m + suc n
      q = suc≡ m n

module Proof2 where
  com : ∀ n m → n + m ≡ m + n
  com zero zero = refl
  com zero (suc m) = cong suc (com zero m)
  com (suc n) zero = cong suc (com n zero)
  com (suc n) (suc m) = cong suc (trans p (trans q r))
    where
      -- This is the right-handed version of addition
      p : n + suc m ≡ suc (m + n)
      p = com n (suc m)
      -- Recurse commutativity
      q : suc (m + n) ≡ suc (n + m)
      q = (cong suc (com m n))
      -- This is the opposite of p
      r : suc (n + m) ≡ m + suc n
      r = com (suc n) m


_≡⟨_⟩_ : {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
x ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z

_∎ : {A : Set} → (x : A) → x ≡ x
x ∎ = refl

infixr 2 _≡⟨_⟩_
infixr 3 _∎

module Proof3 where
  com : ∀ n m → n + m ≡ m + n
  com zero    zero    = refl
  com zero    (suc m) = cong suc (com zero m)
  com (suc n) zero    = cong suc (com n zero)
  com (suc n) (suc m) = cong suc Φ
    where
      Φ : n + suc m ≡ m + suc n
      Φ = n + suc m   ≡⟨ com n (suc m) ⟩
          suc (m + n) ≡⟨ cong suc (com m n) ⟩
          suc (n + m) ≡⟨ com (suc n) m ⟩
          m + suc n   ∎

open Proof2 public