# 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' [] = 0
    lsb→nat' (true ∷ xs) = 1 + 2 * lsb→nat' xs
    lsb→nat' (false ∷ xs) = 2 * lsb→nat' xs
  -- </LSG>

-- Nach korrekter Definition können Sie zum Test folgenden
-- Code aktivieren:
-- <COMMENT>
_ : lsb→nat (true ∷ true ∷ false ∷ true ∷ []) ≡ 11
_ = 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' (2 * acc) xs
msb→nat' acc (true ∷ xs) = msb→nat' (1 + 2 * acc) xs
-- </LSG>

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

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

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

_ : msb→nat (true ∷ true ∷ false ∷ true ∷ []) ≡ 13
_ = 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 (2 * 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`