# ITP Blatt 04

Besprechung: am 21.05.2026

```
{-# OPTIONS --allow-unsolved-metas #-}
open import Level using (Level)
open import Data.Nat
open import Data.Fin
open import Data.List
open import Data.Empty
open import Data.Vec hiding (length)
open import Data.Product
open import Data.Unit
open import Data.Sum
open import Data.Bool hiding (_≤_; _<_)
open import Function.Base using (_∘_; id; case_of_)
import Level as L
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary.Negation

module _ where

private
  variable
    ℓ ℓ' ℓ'' : Level
    A : Set ℓ
    B : Set ℓ'
    C : Set ℓ''

```

## Fin-access
Definieren Sie Index-Zugriff auf eine Liste mittels `Data.Fin`:
```
_at[_] : (l : List A) → Fin (length l) → A
_at[_] = {! !}
```

## Fin vs Vec
Wir betrachten die zwei Darstellungen von Listen der Länge `k`, mittels `Vec`
sowie als Abbildungen `Fin k → -`. Definieren Sie die Übersetzungen:
```
module Fin-vs-Vec (X : Set ℓ) where
  fin-to-vec : ∀ {k} → (Fin k → X) → (Vec X k)
  fin-to-vec = {! !}
  vec-to-fin : ∀ {k} → (Vec X k) → (Fin k → X)
  vec-to-fin = {! !}
```
Beweisen Sie, dass die beiden Abbildungen invers zueinander sind:
```
  iso-on-fin : ∀ k (f : Fin k → X) → vec-to-fin (fin-to-vec f) ≗ f
  iso-on-fin = {! !}

  iso-on-vec : ∀ {k} → fin-to-vec ∘ vec-to-fin {k} ≗ id
  iso-on-vec = {! !}
```

## Logic
Wir betrachten die folgenden aussagenlogischen Gesetze:
```
LEM : ∀ (A : Set) → Set
LEM A = A ⊎ ¬ A

peirce : ∀ (A B : Set) → Set
peirce A B = ((A → B) → A) → A

¬¬-elim : ∀ (A : Set) → Set
¬¬-elim A = ¬ ¬ A → A

contraposition⁻¹ : ∀ (A B : Set) → Set
contraposition⁻¹ A B = (¬ B → ¬ A) → (A → B)

deMorgan : ∀ (A B : Set) → Set
deMorgan A B = ¬ (A × B) → (¬ A ⊎ ¬ B)
```
Zeigen sie, dass diese äquivalent zueinander sind:
```
LEM⇒peirce : ∀ A B  → (∀ A → LEM A) → peirce A B
LEM⇒peirce A B LEM = {! !}

peirce⇒¬¬-elim : ∀ A → (∀ B → peirce A B) → ¬¬-elim A
peirce⇒¬¬-elim A = {! !}

¬¬-elim⇒contraposition⁻¹ : (∀ A → ¬¬-elim A) → ∀ A B → contraposition⁻¹ A B
¬¬-elim⇒contraposition⁻¹ ¬¬A→A A B = {! !}

contraposition⁻¹⇒LEM : (∀ A B → contraposition⁻¹ A B) → (∀ A → LEM A)
contraposition⁻¹⇒LEM contra A = {! !}

```