open Data.Nat.Base using (_*_)
open Data.Nat.Properties using (*-comm;+-assoc)
data Bin : Set where
  ⟨⟩ : Bin
  _O : Bin → Bin
  _I : Bin → Bin
inc : Bin → Bin
inc ⟨⟩ = ⟨⟩ I
inc (rest O) = rest I
inc (rest I) = (inc rest) O
toᴮ   : ℕ → Bin
toᴮ zero = ⟨⟩ O
toᴮ (suc n) = inc (toᴮ n)
fromᴮ : Bin → ℕ
fromᴮ ⟨⟩ = 0
fromᴮ (rest O) = 2 * (fromᴮ rest)
fromᴮ (rest I) = 1 + 2 * (fromᴮ rest)
*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
*-distrib-+ zero n p = refl
*-distrib-+ (suc m) n p rewrite *-distrib-+ m n p | +-assoc p (m * p) (n * p) = refl

from-inc-suc-from : ∀ (b : Bin) → fromᴮ (inc b) ≡ suc (fromᴮ b)
from-inc-suc-from ⟨⟩ = refl
from-inc-suc-from (b O) = refl
from-inc-suc-from (b I) =
  begin
    fromᴮ (inc (b I))
  ≡⟨⟩
    fromᴮ ((inc b) O)
  ≡⟨⟩
    2 * (fromᴮ (inc b))
  ≡⟨ cong (\x → 2 * x) (from-inc-suc-from b) ⟩
    2 * suc (fromᴮ b)
  ≡⟨⟩
    2 * (1 + (fromᴮ b))
  ≡⟨ *-comm 2 (1 + (fromᴮ b)) ⟩
    (1 + (fromᴮ b)) * 2
  ≡⟨ *-distrib-+ 1 (fromᴮ b) 2 ⟩
    2 + (fromᴮ b) * 2
  ≡⟨ cong (\x → 2 + x) (*-comm (fromᴮ b) 2) ⟩
    2 + 2 * (fromᴮ b)
  ≡⟨⟩
    suc (1 + 2 * (fromᴮ b))
  ≡⟨⟩
    suc (fromᴮ (b I))
  ∎
fromᴮ∘toᴮ : ∀ (n : ℕ) → (fromᴮ ∘ toᴮ) n ≡ n
fromᴮ∘toᴮ zero = refl
fromᴮ∘toᴮ (suc n) =
  begin
    (fromᴮ ∘ toᴮ) (suc n)
  ≡⟨⟩
    fromᴮ (toᴮ (suc n))
  ≡⟨⟩
    fromᴮ (inc (toᴮ n))
  ≡⟨ from-inc-suc-from (toᴮ n) ⟩
    suc (fromᴮ (toᴮ n))
  ≡⟨ cong suc (fromᴮ∘toᴮ n) ⟩
    suc n
  ∎

open import plfa.part1.Induction using (Bin)

  { to = toᴮ
  ; from = fromᴮ
  ; from∘to = fromᴮ∘toᴮ

  { to = plfa.part1.Induction.to
  ; from = plfa.part1.Induction.from
  ; from∘to = plfa.part1.Induction.from-to-id