-- My solution to:
-- https://plfa.github.io/Naturals/#Bin

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

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

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

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

n_two : ℕ
n_two = (suc (suc zero))

n_three : ℕ
n_three = (suc n_two)
_ : (suc zero) + zero ≡ suc zero; _ = refl


-- Data is to be represented right to left
-- 2 = 0b10 = x0 (x1 nil)
data Bin : Set where
  nil : Bin
  x0 : Bin → Bin
  x1 : Bin → Bin

inc : Bin → Bin

inc nil = (x1 nil)
inc (x0 x) = (x1 x)
inc (x1 x) = (x0 (inc x))

b_zero : Bin
b_zero = x0 nil

b_one : Bin
b_one = x1 nil

b_two : Bin
b_two = x0 (x1 nil)

b_three : Bin
b_three = x1 (x1 nil)

_ : inc b_one ≡ b_two; _ = refl
_ : inc b_two ≡ b_three; _ = refl
_ : inc (inc (inc b_zero)) ≡ b_three; _ = refl
_ : inc (x1 (x1 (x0 (x1 nil)))) ≡ (x0 (x0 (x1 (x1 nil)))); _ = refl

tob : ℕ → Bin
fromb : Bin → ℕ

tob zero = x0 nil
tob (suc zero) = x1 nil
tob (suc n) = (inc (tob n))

_ : tob n_three ≡ b_three; _ = refl

fromb nil = zero
fromb (x0 nil) = zero
fromb (x1 nil) = suc zero
fromb (x0 x) = n_two * fromb x
fromb (x1 x) = suc (n_two * (fromb x))

_ : fromb b_two ≡ n_two; _ = refl
_ : fromb b_three ≡ n_three; _ = refl
_ : tob (n_two * n_two) ≡ inc b_three; _ = refl