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 =
  -- <LSG>
  trans (rev-acc∘rev-acc xs [] []) (++-identityʳ xs)
  where
    rev-acc∘rev-acc : ∀ (xs ys zs : List X) → rev-acc (rev-acc xs ys) zs ≡ rev-acc ys (xs ++ zs)
    rev-acc∘rev-acc [] ys zs = refl
    rev-acc∘rev-acc (x ∷ xs) ys zs =
      begin
      rev-acc (rev-acc xs (x ∷ ys)) zs ≡⟨ rev-acc∘rev-acc xs _ zs ⟩
      rev-acc (x ∷ ys) (xs ++ zs) ≡⟨⟩
      rev-acc ys ((x ∷ xs) ++ zs)
      ∎
      where open ≡-Reasoning
  -- </LSG>

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 =
  -- <LSG>
  lsb→nat'
  where
    lsb→nat' : List Bool → ℕ
    lsb→nat' [] = 
    lsb→nat' (true ∷ xs) =  +  * lsb→nat' xs
    lsb→nat' (false ∷ xs) =  * lsb→nat' xs
  -- </LSG>

-- Once your definition is correct, you can enable the following
-- code as a test:
-- <COMMENT>
_ : lsb→nat (true ∷ true ∷ false ∷ true ∷ []) ≡ 
_ = refl
-- </COMMENT>

-- Additionally define the conversion of binary numbers in the order
-- "most-significant bit first" to natural numbers, explicitly using
-- an accumulator:
-- <LSG>
msb→nat' : ℕ → List Bool → ℕ
msb→nat' acc [] = acc
msb→nat' acc (false ∷ xs) = msb→nat' ( * acc) xs
msb→nat' acc (true ∷ xs) = msb→nat' ( +  * acc) xs
-- </LSG>

msb+acc→nat : ℕ → List Bool → ℕ
msb+acc→nat =
  -- <LSG>
  msb→nat'
  -- </LSG>

msb→nat : List Bool → ℕ
msb→nat = msb+acc→nat 

-- Once your definition is correct, you can enable the following
-- code as a test:
-- <COMMENT>
_ : msb→nat (true ∷ false ∷ true ∷ true ∷ []) ≡ 
_ = refl

_ : msb→nat (true ∷ true ∷ false ∷ true ∷ []) ≡ 
_ = refl
-- </COMMENT>

Show that LSB and MSB are equivalent; the type of the auxiliary function is below in the "Hints".

-- <LSG>
lsb≗msb∘rev' : ∀ (xs ys : List Bool) → lsb→nat (rev-acc xs ys) ≡ msb+acc→nat (lsb→nat ys) xs
lsb≗msb∘rev' [] ys = refl
lsb≗msb∘rev' (false ∷ xs) ys = begin
  lsb→nat (rev-acc (false ∷ xs) ys)  ≡⟨⟩
  lsb→nat (rev-acc xs (false ∷ ys))  ≡⟨ lsb≗msb∘rev' xs (false ∷ ys) ⟩
  msb+acc→nat ( * lsb→nat ys) xs ≡⟨⟩
  msb+acc→nat (lsb→nat ys) (false ∷ xs)
  ∎
  where open ≡-Reasoning
lsb≗msb∘rev' (true ∷ xs) ys = lsb≗msb∘rev' xs (true ∷ ys)
-- </LSG>

lsb≗msb∘rev : ∀ (xs : List Bool) → lsb→nat (rev xs) ≡ msb→nat xs
lsb≗msb∘rev  xs =
    -- <LSG>
    lsb≗msb∘rev' xs []
    -- </LSG>

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} =
  -- <LSG>
  helper
  where
    helper : ∀ x → map (g ∘ f) x ≡ map g (map f x)
    helper [] = refl
    helper (x ∷ xs) = cong ((g (f x)) ∷_) (helper xs)
  -- </LSG>

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

Agda Quellcode herunterladen