module Naturals where

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

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

{-# BUILTIN NATURAL ℕ #-}

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

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

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

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

infixl 6  _+_  _∸_
infixl 7  _*_

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

-- Bin stretch exercise

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

inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (m O) =  m I
inc (m I) = (inc m) O

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

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

to : ℕ -> Bin
to 0 = ⟨⟩
to (suc n) = inc (to n)

_ : to 11 ≡ ⟨⟩ I O I I
_ = refl

from : Bin -> ℕ
from ⟨⟩ = 0
from (m O) = 2 * from m
from (m I) = 1 + 2 * from m

_ : from (⟨⟩ I O I I) ≡ 11
_ = refl