Naturals.agda

Naturals.agda

module plfa.part1.Naturals where

data N : Set where
  zero : N
  suc : N -> N

{-# BUILTIN NATURAL N #-}

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


_+_ : N -> N -> N
zero + n = n
(suc m) + n = suc (m + n)

_ : 3 + 4 ≡ 7
_ =
  begin
    3 + 4
  ≡⟨⟩
    suc 2 + 4
  ≡⟨⟩
    suc (2 + 4)
  ≡⟨⟩
    suc (suc 1 + 4)
  ≡⟨⟩
    suc (suc (1 + 4))
  ≡⟨⟩
    suc (suc (suc 0 + 4))
  ≡⟨⟩
    suc (suc (suc (0 + 4)))
  ≡⟨⟩
    suc (suc (suc (zero + 4)))
  ≡⟨⟩
    suc (suc (suc 4))
  ≡⟨⟩
    7
  ∎

_*_ : N -> N -> N
zero * n = zero
suc m * n = n + (m * n)

_ : 3 * 4 ≡ 12
_ =
  begin
    3 * 4
  ≡⟨⟩
    suc 2 * 4
  ≡⟨⟩
    4 + (2 * 4)
  ≡⟨⟩
    4 + (suc 1 * 4)
  ≡⟨⟩
    4 + (4 + (1 * 4))
  ≡⟨⟩
    4 + (4 + (suc zero * 4))
  ≡⟨⟩
    4 + (4 + (4 + (zero * 4)))
  ≡⟨⟩
    4 + (4 + (4 + zero))
  ≡⟨⟩
    4 + (4 + (4 + 0))
  ≡⟨⟩
    4 + (4 + 4)
  ≡⟨⟩
    4 + 8
  ≡⟨⟩
    12
  ∎

_^_ : N -> N -> N
m ^ suc n = m * (m ^ n)
x ^ zero = 1

_ : 3 ^ 4 ≡ 81
_ =
  begin
    3 ^ 4
  ≡⟨⟩
    3 ^ suc 3
  ≡⟨⟩
    3 * (3 ^ 3)
  ≡⟨⟩
    3 * (3 ^ suc 2)
  ≡⟨⟩
    3 * (3 * (3 ^ 2))
  ≡⟨⟩
    3 * (3 * (3 ^ suc 1))
  ≡⟨⟩
    3 * (3 * (3 * (3 ^ 1)))
  ≡⟨⟩
    3 * (3 * (3 * (3 ^ (suc 0))))
  ≡⟨⟩
    3 * (3 * (3 * (3 * (3 ^ 0))))
  ≡⟨⟩
    3 * (3 * (3 * (3 * (3 ^ zero))))
  ≡⟨⟩
    3 * (3 * (3 * (3 * 1)))
  ≡⟨⟩
    3 * (3 * (3 * 3))
  ≡⟨⟩
    3 * (3 * 9)
  ≡⟨⟩
    3 * 27
  ≡⟨⟩
    81
  ∎


_-_ : N -> N -> N
n - zero = n
zero - suc n = zero
suc m - suc n = m - n


_ : 5 - 3 ≡ 2
_ =
  begin
    5 - 3
  ≡⟨⟩
    suc 4 - suc 2
  ≡⟨⟩
    4 - 2
  ≡⟨⟩
    suc 3 - suc 1
  ≡⟨⟩
    3 - 1
  ≡⟨⟩
    suc 2 - suc 0
  ≡⟨⟩
    2 - 0
  ≡⟨⟩
    2 - zero
  ≡⟨⟩
    2
  ∎


_ : 3 - 5 ≡ 0
_ =
  begin
    3 - 5
  ≡⟨⟩
    suc 2 - suc 4
  ≡⟨⟩
    2 - 4
  ≡⟨⟩
    suc 1 - suc 3
  ≡⟨⟩
    1 - 3
  ≡⟨⟩
    suc 0 - suc 2
  ≡⟨⟩
    0 - 2
  ≡⟨⟩
    zero - suc 1
  ≡⟨⟩
    zero
  ∎

infixl 6  _+_  _-_
infixl 7  _*_


_++_ : N -> N -> N
zero ++ n = n
suc m ++ n = suc (m ++ n)

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


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


inc : Bin -> Bin
inc ⟨⟩ = ⟨⟩ I
inc (n O) = n I
inc (n I) = (inc n) O


zilch = ⟨⟩ O O O O
one = ⟨⟩ O O O I
two = ⟨⟩ O O I O
three = ⟨⟩ O O I I
four = ⟨⟩ O O I O O
five = ⟨⟩ O O I O I
seven = ⟨⟩ O O I I I
eight = ⟨⟩ O I O O O

_ =
  begin
    inc zilch
  ≡⟨⟩
    one
  ∎

_ =
  begin
    inc two
  ≡⟨⟩
    inc (inc (inc zilch))
  ≡⟨⟩
    inc (inc one)
  ≡⟨⟩
    three
  ∎


_ =
  begin
    inc seven
  ≡⟨⟩
    eight
  ∎

to : N -> Bin
to zero = ⟨⟩ O
to (suc n) = inc (to n)


_ =
  begin
    to 0
  ≡⟨⟩
    ⟨⟩ O
  ∎
_ =
  begin
    to 1
  ≡⟨⟩
    ⟨⟩ I
  ∎
_ =
  begin
    to 2
  ≡⟨⟩
    ⟨⟩ I O
  ∎
_ =
  begin
    to 3
  ≡⟨⟩
    ⟨⟩ I I
  ∎
_ =
  begin
    to 4
  ≡⟨⟩
    ⟨⟩ I O O
  ∎

from : Bin -> N
from ⟨⟩ = zero
from (n O) =  2 * (from n)
from (n I) = 1 + 2 * (from n)


_ =
  begin
    0
  ≡⟨⟩
    from (⟨⟩ O)
  ∎
_ =
  begin
    1
  ≡⟨⟩
    from (⟨⟩ I)
  ∎
_ =
  begin
    2
  ≡⟨⟩
    from (⟨⟩ I O)
  ∎
_ =
  begin
    3
  ≡⟨⟩
    from (⟨⟩ I I)
  ∎
_ =
  begin
    4
  ≡⟨⟩
    from (⟨⟩ I O O)
  ∎