Naturals.agda

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

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

{-# BUILTIN NATURAL ℕ #-}

seven : ℕ
seven = suc (suc (suc (suc (suc (suc (suc zero))))))

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

_ : 3 + 4 ≡ 7
_ = refl

+-example : 3 + 4 ≡ 7
+-example =
  begin
    3 + 4
  ≡⟨⟩  -- is shorthand for
    suc (suc (suc zero)) + suc (suc (suc (suc zero)))

  ≡⟨⟩  -- associativity
    suc (suc (suc zero) + suc (suc (suc (suc zero))))

  ≡⟨⟩  -- associativity
    suc (suc (suc (zero + suc (suc (suc (suc zero))))))

  ≡⟨⟩  -- identity
    suc (suc (suc (suc (suc (suc (suc zero))))))

  ≡⟨⟩  -- is longhand for
    7
  ∎

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

*-example : 3 * 4 ≡ 12
*-example =
  begin
    3 * 4
  ≡⟨⟩  -- inductive m=2 n=4
    4 + (2 * 4)
  ≡⟨⟩  -- inductive m=1 n=4
    4 + (4 + (1 * 4))
  ≡⟨⟩  -- inductive m=0 n=4
    4 + (4 + (4 + (0 * 4)))
  ≡⟨⟩  -- base
    4 + (4 + (4 + 0))
  ≡⟨⟩  -- simpl
    12
  ∎

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

_ : 3 ^ 4 ≡ 81
_ = refl

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   =  m
zero  ∸ suc n  =  zero
suc m ∸ suc n  =  m ∸ n

_ : 5 ∸ 3 ≡ 2
_ = refl
∸-example1 =
  begin
    5 ∸ 3
  ≡⟨⟩  -- third
    4 ∸ 2
  ≡⟨⟩  -- third
    3 ∸ 1
  ≡⟨⟩  -- third
    2 ∸ 0
  ≡⟨⟩  -- first
    2
  ∎

_ : 3 ∸ 5 ≡ 0
_ = refl
∸-example2 =
  begin
    3 ∸ 5
  ≡⟨⟩  -- third
    2 ∸ 4
  ≡⟨⟩  -- third
    1 ∸ 5
  ≡⟨⟩  -- third
    0 ∸ 4
  ≡⟨⟩  -- second
    0
  ∎

_plus_ : ℕ → ℕ → ℕ
zero plus n = n
suc m plus n = suc (m + n)

_ : 12 plus 21 ≡ 33
_ = refl

{-# BUILTIN NATPLUS _+_ #-}
{-# BUILTIN NATTIMES _*_ #-}
{-# BUILTIN NATMINUS _∸_ #-}

data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin

from : Bin -> ℕ
from b = h b 0 0 where
  h : Bin -> ℕ -> ℕ -> ℕ
  h (rest I) acc i = h rest (acc + (2 ^ i)) (i + 1)
  h (rest O) acc i = h rest acc             (i + 1)
  h input    acc i = acc
_ : from (⟨⟩ O) ≡ 0
_ = refl
_ : from (⟨⟩ I) ≡ 1
_ = refl
_ : from (⟨⟩ I O) ≡ 2
_ = refl
_ : from (⟨⟩ I I) ≡ 3
_ = refl
_ : from (⟨⟩ I O O) ≡ 4
_ = refl
_ : from (⟨⟩ I O I I) ≡ 11
_ = refl

inc : Bin → Bin
inc (⟨⟩)     = ⟨⟩ I
inc (⟨⟩ O)   = ⟨⟩ I
inc (rest O) = rest I
inc (⟨⟩ I)   = ⟨⟩ I O
inc (rest I) = (inc rest) O
_ : inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
_ = refl

to : ℕ -> Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)
_ : to 0 ≡ ⟨⟩ O
_ = refl
_ : to 1 ≡ ⟨⟩ I
_ = refl
_ : to 2 ≡ ⟨⟩ I O
_ = refl
_ : to 3 ≡ ⟨⟩ I I
_ = refl
_ : to 4 ≡ ⟨⟩ I O O
_ = refl