Bin.agda

module Bin where

--  `Set` is a reserved word in Agda, it's the type of all types
--  We are declaring that `Bin` is of type `Set`, `■` is of type `Bin`, and so on ...
data Bin : Set where
    ■   : Bin        -- 0
    0,_ : Bin → Bin  -- 2n
    1,_ : Bin → Bin  -- 2n+1

-- Binary number in a reversed order, for example
module BinExample where
    three : Bin
    three = 1, 1, ■

    eight : Bin
    eight = 0, 0, 0, 1, ■

--------------------------------------------------------------------------------
--  Conversions between Bin and ℕ
--------------------------------------------------------------------------------

-- Natural number à la Peano
open import Data.Nat

toℕ : Bin → ℕ
toℕ ■      = zero
toℕ (0, b) =     2 * toℕ b
toℕ (1, b) = 1 + 2 * toℕ b

--  increment
incr : Bin → Bin
incr ■      = 1, ■
incr (0, b) = 1, b
incr (1, b) = 0, incr b

fromℕ : ℕ → Bin
fromℕ zero    = ■
fromℕ (suc n) = incr (fromℕ n)

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
--  Prove that, converting ℕ back and forth yields the same number
--
--  Syntax explanation:
--      `∀ n` sugars `(n : _)`
--      `(n : _)` rather than `(n : ℕ)` because Agda can determine that `n` is a `ℕ`
--      `(n : ℕ)` gives the argument in a type a name, so that the latter terms can "depends" on it.
--
--      `_+_ : ℕ → ℕ → ℕ` is actually a syntax sugar for `_+_ : (_ : ℕ) → (_ : ℕ) → (_ : ℕ)`,
--      it's just that the latter does not depends on the former, we don't care their names
--
--  `_≡_`, `begin_`, `≡⟨_⟩_` ... are all defined by someone, not language built-in
toℕ∘fromℕ-id : ∀ n → toℕ (fromℕ n) ≡ n
toℕ∘fromℕ-id zero    = refl     -- the compiler can figure this out, by just by normalizing with definition
toℕ∘fromℕ-id (suc n) = begin
        toℕ (fromℕ (suc n))
    ≡⟨ refl ⟩   -- just normalizing, by the definition of `fromℕ`, `fromℕ (suc n)` ⇒ `incr (fromℕ n)`
        toℕ (incr (fromℕ n))
    ≡⟨ coherence (fromℕ n) ⟩
        suc (toℕ (fromℕ n))
    ≡⟨ cong suc (toℕ∘fromℕ-id n) ⟩
        suc n
    ∎

    where   --  lemma
            open import Data.Nat.Properties.Simple using (+-*-suc)
            --  +-*-suc : ∀ m n → m * suc n ≡ m + m * n
            coherence : ∀ b → toℕ (incr b) ≡ suc (toℕ b)
            coherence ■      = refl
            coherence (0, b) = refl
            coherence (1, b) = begin
                    toℕ (incr (1, b))
                ≡⟨ refl ⟩
                    toℕ (0, incr b)
                ≡⟨ refl ⟩
                    2 * toℕ (incr b)
                ≡⟨ cong (_*_ 2) (coherence b) ⟩
                    2 * (1 + toℕ b)
                ≡⟨ +-*-suc 2 (toℕ b) ⟩
                    2 + 2 * toℕ b
                ∎

--  ∀ b → fromℕ (toℕ b) ≢ b
--  because `toℕ` is a retraction (epimorphism) of `fromℕ`
--  and `fromℕ` is a section (monomorphism) of `toℕ`
--  but their composite: `fromℕ ∘ toℕ` is just a split idempotent, not an isomorphism

normalize : Bin → Bin
normalize b = fromℕ (toℕ b)

split-idempotency : ∀ b → fromℕ (toℕ b) ≡ normalize b
split-idempotency b = refl -- boring as is