Theorem.agda

-- http://people.inf.elte.hu/divip/AgdaTutorial/Functions.Equality_Proofs.html
module Theorem where

import Level

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

infix 4 _≡_

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

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

infixl 6 _+_

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

sym : ∀ {l} {A : Set l} {a b : A} → a ≡ b → b ≡ a
sym refl = refl

trans : ∀ {l} {A : Set l} {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans a≡b b≡c rewrite a≡b | b≡c = refl

cong : ∀ {a b} {A : Set a} {B : Set b} {m n : A} → (f : A → B) → m ≡ n → f m ≡ f n
cong f m≡n rewrite m≡n = refl

infixl 1 _⟨_⟩_

_⟨_⟩_ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} → A → (A → B → C) → B → C
x ⟨ f ⟩ y = f x y

+-right-identity : ∀ n → n + 0 ≡ n
+-right-identity zero    = refl
+-right-identity (suc n) = cong suc (+-right-identity n)

+-assoc : ∀ a b c → a + (b + c) ≡ (a + b) + c
+-assoc zero b c = refl
+-assoc (suc a) b c = cong suc (+-assoc a b c)

+-comm : ∀ a b → a + b ≡ b + a
+-comm zero b = sym (+-right-identity b)
+-comm (suc a) b = +-assoc 1 a b
         ⟨ trans ⟩ cong suc (+-comm a b)
         ⟨ trans ⟩ sym (n+1≡1+n (b + a))
         ⟨ trans ⟩ sym (+-assoc b a 1)
         ⟨ trans ⟩ cong (_+_ b) (n+1≡1+n a)
  where
    n+1≡1+n : ∀ n → n + 1 ≡ 1 + n
    n+1≡1+n zero = refl
    n+1≡1+n (suc n) = cong suc (n+1≡1+n n)