{-# OPTIONS --cubical-compatible #-}
module Padova2025.VerifiedAlgorithms.Binary where
Case study: Binary representation of natural numbers
We have defined the natural numbers in an unary manner, freely
generating ℕ by zero
and succ
; this approach
is logically pleasing, but computationally inefficient. Let us introduce
binary representations of natural numbers, define the basic arithmetical
operations on binary representations, and then prove these operations
correct with respect to the unary model.
open import Padova2025.ProgrammingBasics.Naturals.Base open import Padova2025.ProgrammingBasics.Naturals.Arithmetic open import Padova2025.ProgrammingBasics.Booleans open import Padova2025.ProgrammingBasics.Lists open import Padova2025.ProvingBasics.Negation open import Padova2025.ProvingBasics.Equality.Base open import Padova2025.ProvingBasics.Equality.General open import Padova2025.ProvingBasics.Equality.NaturalNumbers open import Padova2025.ProvingBasics.Equality.Reasoning.Core
A binary representation is just a list of zeros and ones (with trailing zeros) allowed:
BitString : Set BitString = List Bool
For instance, we represent the number 12 (binary 1100
)
as false ∷ false ∷ true ∷ true ∷ []
, i.e. with the least
significant bit in the front. Every bit string represents some natural
number:
decode : BitString → ℕ decode = {!!}
Exercise: Binary successor
Implement the successor operation on bit strings, then prove it correct with respect to the model.
succᵇ : BitString → BitString succᵇ = {!!}
succᵇ-correct : (xs : BitString) → decode (succᵇ xs) ≡ succ (decode xs) succᵇ-correct = {!!}
Exercise: Encoding natural numbers
Implement a function which encodes a given natural number as a bit string, then prove your implementation correct.
encode : ℕ → BitString encode = {!!}
The function succᵇ
from above might come in handy.
decode-encode : (x : ℕ) → decode (encode x) ≡ x decode-encode = {!!}
Exercise: Uniqueness of binary representations
Every natural number admits infinitely many binary representations, as we can always add trailing zeros. Let us prove that such trailing zeros are the only source of non-uniqueness of binary representations.
To this end, we first define a predicate
AllZero : BitString → Set
expressing that a given bit
string consists just of zeros. Think about how this could be done, then
have a look at the following reference definition.
data AllZero : BitString → Set where triv : AllZero [] cons : {xs : BitString} → AllZero xs → AllZero (false ∷ xs)
With the predicate AllZero
at hand, we can define what
it means that two bit strings are equivalent:
infix 4 _≈_ data _≈_ : BitString → BitString → Set where base : {xs ys : BitString} → AllZero xs → AllZero ys → xs ≈ ys -- "Equivalent because both strings just consist of zeros." cons : {xs ys : BitString} {b : Bool} → xs ≈ ys → b ∷ xs ≈ b ∷ ys -- "Equivalent because both strings have the same least significant digit, -- and then continue in an equivalent manner."
As a warm-up, let us prove that equivalent bit strings represent the same natural number.
decode-allZero : {xs : BitString} → AllZero xs → decode xs ≡ zero decode-allZero = {!!}
decode-≈ : {xs ys : BitString} → xs ≈ ys → decode xs ≡ decode ys decode-≈ = {!!}
Now let us prove that bit strings which represent the same number are equivalent.
unique-zero : {xs : BitString} → decode xs ≡ zero → AllZero xs unique-zero = {!!}
unique : {xs ys : BitString} → decode xs ≡ decode ys → xs ≈ ys unique = {!!}
Exercise: Binary addition
Implement the addition operation on bit strings, then prove it correct with respect to the unary model.
addᵇ : BitString → BitString → BitString addᵇ = {!!}
addᵇ-correct : (xs ys : BitString) → decode (addᵇ xs ys) ≡ decode xs + decode ys addᵇ-correct = {!!}
Exercise: Commutativity of binary addition
Let us check, without using that addition of natural numbers is
commutative, that addᵇ
is commutative:
addᵇ-comm : (xs ys : BitString) → addᵇ xs ys ≡ addᵇ ys xs addᵇ-comm = {!!}
Alternatively, we could also translate to the unary model and use the
commutativity of _+_
:
addᵇ-comm' : (xs ys : BitString) → addᵇ xs ys ≈ addᵇ ys xs addᵇ-comm' = {!!}
As a curiosity, we can rederive commutativity of addition in the
unary model, by translating to binary representations and using
commutativity of addᵇ
:
+-comm' : (x y : ℕ) → x + y ≡ y + x +-comm' = {!!}