# 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`