Skip to content

Instantly share code, notes, and snippets.

@banacorn
Created Aug 29, 2015
Embed
What would you like to do?
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment