Some basic properties of natural numbers in Agda.

NatProps.agda

module NatProps where

open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.Sum
open import Function

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

infixl 7 _*_
infixl 6 _+_
infix  4 _≤_

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n} → zero ≤ n 
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

_≤?_ : ∀ a b → Dec (a ≤ b) 
zero ≤? b = yes z≤n
suc a ≤? zero = no λ()
suc a ≤? suc b with a ≤? b
... | yes p = yes (s≤s p)
... | no ¬p = no (¬p ∘ (λ {(s≤s p) → p}))

≤-total : ∀ a b → (a ≤ b) ⊎ (b ≤ a) 
≤-total zero    b       = inj₁ z≤n
≤-total (suc a) zero    = inj₂ z≤n
≤-total (suc a) (suc b) = map s≤s s≤s (≤-total a b)

_+_ : ℕ → ℕ → ℕ
zero  + b = b
suc a + b = suc (a + b)

_*_ : ℕ → ℕ → ℕ
zero  * b = zero
suc a * b = b + a * b 

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

+-comm : ∀ a b → a + b ≡ b + a
+-comm zero zero    = refl
+-comm zero (suc b) = cong suc (+-comm zero b)
+-comm (suc a) zero = cong suc (+-comm a zero)
+-comm (suc a) (suc b) rewrite 
    +-comm a (suc b) 
  | +-comm b (suc a) 
  | +-comm b a = refl

*-comm : ∀ a b → a * b ≡ b * a
*-comm zero zero = refl
*-comm (suc a) zero = *-comm a zero
*-comm zero (suc b) = *-comm zero b
*-comm (suc a) (suc b) rewrite 
    *-comm a (suc b) 
  | *-comm b (suc a) 
  | *-comm b a 
  | +-assoc b a (a * b) 
  | +-assoc a b (a * b)
  | +-comm b a = refl

*-ldist : ∀ a b c → a * (b + c) ≡ a * b + a * c
*-ldist zero b c = refl
*-ldist (suc a) b c rewrite
    sym $ +-assoc b (a * b) (c + a * c)
  | +-assoc (a * b) c (a * c)
  | +-comm (a * b) c 
  | sym $ +-assoc c (a * b) (a * c)
  | +-assoc b c (a * b + a * c)
  | *-ldist a b c = refl

*-rdist : ∀ a b c → (a + b) * c ≡ a * c + b * c
*-rdist a b c rewrite
    *-comm (a + b) c
  | *-comm a c
  | *-comm b c
  | *-ldist c a b = refl

*-assoc : ∀ a b c → a * (b * c) ≡ (a * b) * c
*-assoc zero b c = refl
*-assoc (suc a) b c rewrite
    *-rdist b (a * b) c
  | *-assoc a b c = refl