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.
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
cons : { xs ys : BitString } { b : Bool } → xs ≈ ys → b ∷ xs ≈ b ∷ ys
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' = {!!}
Reference solutions
decode : BitString → ℕ
decode [] = zero
decode ( false ∷ xs ) = twice ( decode xs )
decode ( true ∷ xs ) = succ ( twice ( decode xs ))
succᵇ : BitString → BitString
succᵇ [] = true ∷ []
succᵇ ( false ∷ xs ) = true ∷ xs
succᵇ ( true ∷ xs ) = false ∷ succᵇ xs
succᵇ-correct : ( xs : BitString ) → decode ( succᵇ xs ) ≡ succ ( decode xs )
succᵇ-correct [] = refl
succᵇ-correct ( false ∷ xs ) = refl
succᵇ-correct ( true ∷ xs ) = begin
decode ( succᵇ ( true ∷ xs )) ≡⟨⟩
decode ( false ∷ succᵇ xs ) ≡⟨⟩
twice ( decode ( succᵇ xs )) ≡⟨ cong twice ( succᵇ-correct xs ) ⟩
twice ( succ ( decode xs )) ≡⟨⟩
succ ( succ ( twice ( decode xs ))) ≡⟨⟩
succ ( decode ( true ∷ xs )) ∎
encode : ℕ → BitString
encode zero = []
encode ( succ x ) = succᵇ ( encode x )
decode-encode : ( x : ℕ ) → decode ( encode x ) ≡ x
decode-encode zero = refl
decode-encode ( succ x ) = trans ( succᵇ-correct ( encode x )) ( cong succ ( decode-encode x ))
decode-allZero : { xs : BitString } → AllZero xs → decode xs ≡ zero
decode-allZero triv = refl
decode-allZero ( cons p ) = cong twice ( decode-allZero p )
decode-≈ : { xs ys : BitString } → xs ≈ ys → decode xs ≡ decode ys
decode-≈ ( base p q ) = trans ( decode-allZero p ) ( sym ( decode-allZero q ))
decode-≈ ( cons { b = false } p ) = cong twice ( decode-≈ p )
decode-≈ ( cons { b = true } p ) = cong succ ( cong twice ( decode-≈ p ))
unique-zero : { xs : BitString } → decode xs ≡ zero → AllZero xs
unique-zero { [] } p = triv
unique-zero { false ∷ xs } p = cons ( unique-zero ( twice-zero p ))
where
twice-zero : { x : ℕ } → twice x ≡ zero → x ≡ zero
twice-zero p = twice-injective p
unique : { xs ys : BitString } → decode xs ≡ decode ys → xs ≈ ys
unique { [] } { ys } p = base triv ( unique-zero ( sym p ))
unique { x ∷ xs } { [] } p = base ( unique-zero p ) triv
unique { false ∷ xs } { false ∷ ys } p = cons ( unique ( twice-injective p ))
unique { false ∷ xs } { true ∷ ys } p = ⊥-elim ( impossible-twice p )
unique { true ∷ xs } { false ∷ ys } p = ⊥-elim ( impossible-twice ( sym p ))
unique { true ∷ xs } { true ∷ ys } p = cons ( unique ( twice-injective ( succ-injective p )))
addᵇ : BitString → BitString → BitString
addᵇ [] ys = ys
addᵇ ( x ∷ xs ) [] = x ∷ xs
addᵇ ( false ∷ xs ) ( y ∷ ys ) = y ∷ addᵇ xs ys
addᵇ ( true ∷ xs ) ( false ∷ ys ) = true ∷ addᵇ xs ys
addᵇ ( true ∷ xs ) ( true ∷ ys ) = false ∷ succᵇ ( addᵇ xs ys )
addᵇ-correct : ( xs ys : BitString ) → decode ( addᵇ xs ys ) ≡ decode xs + decode ys
addᵇ-correct [] ys = refl
addᵇ-correct ( x ∷ xs ) [] = sym ( +-zero ( decode ( x ∷ xs )))
addᵇ-correct ( false ∷ xs ) ( false ∷ ys ) = begin
decode ( addᵇ ( false ∷ xs ) ( false ∷ ys )) ≡⟨⟩
decode ( false ∷ addᵇ xs ys ) ≡⟨⟩
twice ( decode ( addᵇ xs ys )) ≡⟨ cong twice ( addᵇ-correct xs ys ) ⟩
twice ( decode xs + decode ys ) ≡⟨ twice-homo ( decode xs ) ( decode ys ) ⟩
twice ( decode xs ) + twice ( decode ys ) ≡⟨⟩
decode ( false ∷ xs ) + decode ( false ∷ ys ) ∎
addᵇ-correct ( false ∷ xs ) ( true ∷ ys ) = begin
decode ( addᵇ ( false ∷ xs ) ( true ∷ ys )) ≡⟨⟩
decode ( true ∷ addᵇ xs ys ) ≡⟨⟩
succ ( twice ( decode ( addᵇ xs ys ))) ≡⟨ cong succ ( cong twice ( addᵇ-correct xs ys )) ⟩
succ ( twice ( decode xs + decode ys )) ≡⟨ cong succ ( twice-homo ( decode xs ) ( decode ys )) ⟩
succ ( twice ( decode xs ) + twice ( decode ys )) ≡˘⟨ +-succ ( twice ( decode xs )) ( twice ( decode ys )) ⟩
twice ( decode xs ) + succ ( twice ( decode ys )) ≡⟨⟩
decode ( false ∷ xs ) + decode ( true ∷ ys ) ∎
addᵇ-correct ( true ∷ xs ) ( false ∷ ys ) = begin
decode ( addᵇ ( true ∷ xs ) ( false ∷ ys )) ≡⟨⟩
decode ( true ∷ addᵇ xs ys ) ≡⟨⟩
succ ( twice ( decode ( addᵇ xs ys ))) ≡⟨ cong succ ( cong twice ( addᵇ-correct xs ys )) ⟩
succ ( twice ( decode xs + decode ys )) ≡⟨ cong succ ( twice-homo ( decode xs ) ( decode ys )) ⟩
succ ( twice ( decode xs ) + twice ( decode ys )) ≡⟨⟩
succ ( twice ( decode xs )) + twice ( decode ys ) ≡⟨⟩
decode ( true ∷ xs ) + decode ( false ∷ ys ) ∎
addᵇ-correct ( true ∷ xs ) ( true ∷ ys ) = begin
decode ( addᵇ ( true ∷ xs ) ( true ∷ ys )) ≡⟨⟩
decode ( false ∷ succᵇ ( addᵇ xs ys )) ≡⟨⟩
twice ( decode ( succᵇ ( addᵇ xs ys ))) ≡⟨ cong twice ( succᵇ-correct ( addᵇ xs ys )) ⟩
twice ( succ ( decode ( addᵇ xs ys ))) ≡⟨ cong twice ( cong succ ( addᵇ-correct xs ys )) ⟩
twice ( succ ( decode xs + decode ys )) ≡⟨⟩
succ ( succ ( twice ( decode xs + decode ys ))) ≡⟨ cong succ ( cong succ ( twice-homo ( decode xs ) ( decode ys ))) ⟩
succ ( succ ( twice ( decode xs ) + twice ( decode ys ))) ≡˘⟨ cong succ ( +-succ ( twice ( decode xs )) ( twice ( decode ys ))) ⟩
succ ( twice ( decode xs ) + succ ( twice ( decode ys ))) ≡⟨⟩
succ ( twice ( decode xs )) + succ ( twice ( decode ys )) ≡⟨⟩
decode ( true ∷ xs ) + decode ( true ∷ ys ) ∎
addᵇ-comm : ( xs ys : BitString ) → addᵇ xs ys ≡ addᵇ ys xs
addᵇ-comm [] [] = refl
addᵇ-comm [] ( y ∷ ys ) = refl
addᵇ-comm ( x ∷ xs ) [] = refl
addᵇ-comm ( false ∷ xs ) ( false ∷ ys ) = cong ( false ∷_ ) ( addᵇ-comm xs ys )
addᵇ-comm ( false ∷ xs ) ( true ∷ ys ) = cong ( true ∷_ ) ( addᵇ-comm xs ys )
addᵇ-comm ( true ∷ xs ) ( false ∷ ys ) = cong ( true ∷_ ) ( addᵇ-comm xs ys )
addᵇ-comm ( true ∷ xs ) ( true ∷ ys ) = cong ( false ∷_ ) ( cong succᵇ ( addᵇ-comm xs ys ))
addᵇ-comm' : ( xs ys : BitString ) → addᵇ xs ys ≈ addᵇ ys xs
addᵇ-comm' xs ys = unique
( begin
decode ( addᵇ xs ys ) ≡⟨ addᵇ-correct xs ys ⟩
decode xs + decode ys ≡⟨ +-comm ( decode xs ) ( decode ys ) ⟩
decode ys + decode xs ≡˘⟨ addᵇ-correct ys xs ⟩
decode ( addᵇ ys xs ) ∎
)
+-comm' : ( x y : ℕ ) → x + y ≡ y + x
+-comm' x y = begin
x + y ≡˘⟨ cong₂ _+_ ( decode-encode x ) ( decode-encode y ) ⟩
decode ( encode x ) + decode ( encode y ) ≡˘⟨ addᵇ-correct ( encode x ) ( encode y ) ⟩
decode ( addᵇ ( encode x ) ( encode y )) ≡⟨ cong decode ( addᵇ-comm ( encode x ) ( encode y )) ⟩
decode ( addᵇ ( encode y ) ( encode x )) ≡⟨ addᵇ-correct ( encode y ) ( encode x ) ⟩
decode ( encode y ) + decode ( encode x ) ≡⟨ cong₂ _+_ ( decode-encode y ) ( decode-encode x ) ⟩
y + x ∎