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 = {!!}
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 = {!!} -- Nach korrekter Definition können Sie zum Test folgenden -- Code aktivieren: -- _ : lsb→nat (true ∷ true ∷ false ∷ true ∷ []) ≡ 11 -- _ = refl -- Definieren Sie zusätzlich die Umwandlung von Binärzahlen -- in der Reihenfolge "most-significant bit first" zu natürlichen Zahlen -- explizit mittels Akkumulator: msb+acc→nat : ℕ → List Bool → ℕ msb+acc→nat = {!!} msb→nat : List Bool → ℕ msb→nat = msb+acc→nat 0 -- Nach korrekter Definition können Sie zum Test folgenden -- Code aktivieren: -- _ : msb→nat (true ∷ false ∷ true ∷ true ∷ []) ≡ 11 -- _ = refl -- -- _ : msb→nat (true ∷ true ∷ false ∷ true ∷ []) ≡ 13 -- _ = refl
Zeigen Sie, dass LSB und MSB gleichwertig sind; der Typ der Hilfsfunktion ist unten in den "Tipps".
lsb≗msb∘rev : ∀ (xs : List Bool) → lsb→nat (rev xs) ≡ msb→nat xs lsb≗msb∘rev xs = {!!}
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} = {!!}
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