agda

Binary Numeration

A common early exercise in familiarizing oneself with Agda is the implementation of tally marks, a unary numeration using one symbol. Further, a second symbol is added for expression of binary literals:

data Bin : Set where
   [] : Bin
   _O : Bin → Bin
   _I : Bin → Bin

usage

two : Bin
two = [] I O

thirteen : Bin
thirteen = [] I I O I

Defining an equivalent to the successor function, these binary literals can be shown in correspondence with the natural numbers:

inc : Bin → Bin
inc [] = []
inc ([] O) = [] I
inc ([] I) = [] I O
inc (n O) = n I
inc (n I) = (inc n) O

usage

inc₀ : inc ([] O) ≡ ([] I)
inc₀ = refl

inc₁ : inc ([] I) ≡ ([] I O)
inc₁ = refl

inc₅ : inc ([] I O I) ≡ ([] I I O)
inc₅ = refl

inc₇ : inc ([] I I I) ≡ ([] I O O O)
inc₇ = refl

to : ℕ → Bin
to zero = [] O
to (succ n) = inc (to n)

from : Bin → ℕ
from [] = zero
from (b O) = let tail = from b in tail + tail
from (b I) = let tail = from b in succ (tail + tail)

usage

to₀ : to 0 ≡ ([] O)
to₀ = refl

to₁ : to 1 ≡ ([] I)
to₁ = refl

to₁₃ : to 13 ≡ ([] I I O I)
to₁₃ = refl

from₁ : from ([] I O I) ≡ 5
from₁ = refl

from₂ : from ([] I I I O I O) ≡ 58
from₂ = refl

inc⇔succ : ( n : ℕ ) → inc (to n) ≡ to (succ n)
inc⇔succ n = refl

Boolean Logic

data Bool : Set where
    tt : Bool
    ff : Bool

-- not
¬ : Bool → Bool
¬ tt = ff
¬ ff = tt

-- and
_∧_ : Bool → Bool → Bool
tt ∧ b = b
ff ∧ _ = ff

-- or
_∨_ : Bool → Bool → Bool
tt ∨ _ = tt
ff ∨ b = b

-- xor
_⊕_ : Bool → Bool → Bool
tt ⊕ b = ¬ b
ff ⊕ b = b

-- xnor
_⊗_ : Bool → Bool → Bool
tt ⊗ b = b
ff ⊗ b = ¬ b

not-all-equal/3 logical completeness

nae₃ : Bool → Bool → Bool → Bool
nae₃ tt tt tt = ff
nae₃ ff ff ff = ff
nae₃ _  _  _  = tt

This kind of higher-order equality check is, maybe surprisingly, logically complete: this is demonstrated by expressions with checked equivalence to the ¬, ∧, ∨ basis with further expression for ⊕/⊗.

nae₃-¬ : ( a : Bool ) →
  (nae₃ tt tt a) ≡ (¬ a)

nae₃-∧ : ( a b : Bool ) →
  (nae₃ tt tt (nae₃ tt a b)) ≡ (a ∧ b)

nae₃-∨ : ( a b : Bool ) →
  (nae₃ ff a b) ≡ (a ∨ b)

nae₃-⊕ : ( a b : Bool ) →
  (nae₃ a a b) ≡ (a ⊕ b)

nae₃-⊗ : ( a b : Bool ) →
  (nae₃ tt tt (nae₃ a a b)) ≡ (a ⊗ b)