ITP Exercise Sheet 02
Discussion: 30 April 2026
{-# OPTIONS --allow-unsolved-metas #-} open import Level using (Level) open import Function.Base using (_∘_; id) open import Relation.Binary.PropositionalEquality
Implicit universal quantification
If you want to write several functions that are all universally quantified in the same variable, this can be declared as follows:
private variable ℓ ℓ' ℓ'' : Level X : Set ℓ Y : Set ℓ' Z : Set ℓ''
Reverse ∘ Reverse ≗ id
Since reverse is defined slightly differently in the lecture than in the standard
library, we repeat the definitions here:
open import Data.List open import Data.List.Properties using (++-identityʳ) rev-acc : List X → List X → List X rev-acc [] acc = acc rev-acc (x ∷ xs) acc = rev-acc xs (x ∷ acc) rev : List X → List X rev xs = rev-acc xs []
Prove that reverse is its own inverse. For this it is necessary to prove an
auxiliary lemma about rev-acc, i.e. the version generalised over the
accumulator. (The type of the auxiliary lemma is below in the "Hints" section.)
rev∘rev≗id : ∀ {X : Set ℓ} → rev ∘ rev ≗ id {ℓ} {List X} rev∘rev≗id xs = {!!}
Binary representation
Define a function that converts a binary number into a natural number. There are two possibilities for which binary digits (bits) come at the beginning of the list: the least or the most significant bits. Define both variants:
(Hint: since the operators _+_ and _*_ are defined by recursion on the first
argument, it is advisable to write constants on the left, e.g. 5 + (8 * x).)
open import Data.Bool open import Data.Nat -- binary representation "least-significant bit first" lsb→nat : List Bool → ℕ lsb→nat = {!!} -- Once your definition is correct, you can enable the following -- code as a test: -- _ : lsb→nat (true ∷ true ∷ false ∷ true ∷ []) ≡ 11 -- _ = refl -- Additionally define the conversion of binary numbers in the order -- "most-significant bit first" to natural numbers, explicitly using -- an accumulator: msb+acc→nat : ℕ → List Bool → ℕ msb+acc→nat = {!!} msb→nat : List Bool → ℕ msb→nat = msb+acc→nat 0 -- Once your definition is correct, you can enable the following -- code as a test: -- _ : msb→nat (true ∷ false ∷ true ∷ true ∷ []) ≡ 11 -- _ = refl -- -- _ : msb→nat (true ∷ true ∷ false ∷ true ∷ []) ≡ 13 -- _ = refl
Show that LSB and MSB are equivalent; the type of the auxiliary function is below in the "Hints".
lsb≗msb∘rev : ∀ (xs : List Bool) → lsb→nat (rev xs) ≡ msb→nat xs lsb≗msb∘rev xs = {!!}
Map preserves composition
Prove that map is compatible with function composition:
map-preserves-∘ : {g : Y → Z} {f : X → Y} → map (g ∘ f) ≗ map g ∘ map f map-preserves-∘ {g = g} {f = f} = {!!}
Hints
Types of the auxiliary lemmas:
∀ (xs ys zs : List X) → rev-acc (rev-acc xs ys) zs ≡ rev-acc ys (xs ++ zs)∀ (xs ys : List Bool) → lsb→nat (rev-acc xs ys) ≡ msb+acc→nat (lsb→nat ys) xs