ITP Blatt 02

Besprechung: am 30.04.2026

{-# OPTIONS --allow-unsolved-metas #-}
open import Level using (Level)
open import Function.Base using (_∘_; id)
open import Relation.Binary.PropositionalEquality

Implizite Allquantifizierung

Wenn man mehrere Funktionen schreiben möchte, die alle in einer Variable all-quantifiziert sind, dann lässt sich das so deklarieren:

private
  variable
    ℓ ℓ' ℓ'' : Level
    X : Set ℓ
    Y : Set ℓ'
    Z : Set ℓ''

Reverse ∘ Reverse ≗ id

Da reverse in der Vorlesung leicht anders definiert ist als in der standard library, wiederholen wir hier die Definitionen:

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 []

Beweisen Sie, dass reverse zu sich selbst invers ist. Hierfür ist es nötig, ein Hilfslemma für das um den Akkumulator verallgemeinerte rev-acc zu beweisen. (Der Typ des Hilfslemmas ist unten im Abschnitt "Tipps")

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>

Binärdarstellung

Definieren Sie eine Funktion, die eine Binärzahl in eine natürlichen Zahl umwandelt. Hierbei gibt es zwei Möglichkeiten, welche Binärziffern (Bits) am Anfang der Liste stehen: die nieder- oder die höchstwertigsten Bits. Definieren Sie beide Varianten:

(Tipp: Da die Operatoren _+_ und _*_ per Rekursion über das erste Argument definiert sind, empfiehlt es sich, Konstanten nach links zu schreiben, also z.B. 5 + (8 * x).)

open import Data.Bool
open import Data.Nat

--  Binärdarstellung "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>

-- Nach korrekter Definition können Sie zum Test folgenden
-- Code aktivieren:
-- <COMMENT>
_ : lsb→nat (true ∷ true ∷ false ∷ true ∷ []) ≡ 
_ = refl
-- </COMMENT>

-- Definieren Sie zusätzlich die Umwandlung von Binärzahlen
-- in der Reihenfolge "most-significant bit first" zu natürlichen Zahlen
-- explizit mittels Akkumulator:
-- <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 

-- Nach korrekter Definition können Sie zum Test folgenden
-- Code aktivieren:
-- <COMMENT>
_ : msb→nat (true ∷ false ∷ true ∷ true ∷ []) ≡ 
_ = refl

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

Zeigen Sie, dass LSB und MSB gleichwertig sind; der Typ der Hilfsfunktion ist unten in den "Tipps".

-- <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 erhält Komposition

Beweisen Sie, dass sich map mit Funktions-Komposition verträgt:

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>

Tipps

Typen der Hilfslemmatas:

• ∀ (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