# ITP Blatt 01

Besprechung: am 23.04.2026

Die Übungsblätter sidn selbst in "Literate Agda" mit Markdown (`*.lagda.md`)
geschrieben. Wenn Sie diese herunterladen (siehe Link ganz unten), dann können
Sie diese wie andere `*.agda`-Dateien interaktiv bearbeiten. Nach dem letzten
Agda-Schnippsel darin muss deshalb erneut ``` folgen.

```
{-# OPTIONS --allow-unsolved-metas #-}
```

## Einrichten von Agda
* Installieren Sie Agda (Version 2.8.0), vgl. [Setup](Setup.md). Nach erfolgreicher Installation lässt sich `agda` wie folgt aufrufen:
```text
$ agda --version
Agda version 2.8.0
```

* Konfigurieren Sie den Texteditor Ihrer Wahl
    ([Siehe offizielle Agda-Doc](https://agda.readthedocs.io/en/latest/getting-started/installation.html#step-2-configure-a-text-editor))


## Erstellen eines Agda-Projekts

Erstellen Sie im Wurzel-Verzeichnis Ihres persönlichen Agda-Projekts eine Datei
`itp.agda-lib` mit dem Inhalt:
```text
name: itp
depend:
  standard-library-2.3
include:
  src
```

* Der Name des Projekts ist `itp` (frei wählbar)
* Das Projekt verlangt die agda stdlib in Version 2.3
* Die Agda-Dateien unseres Projekts sind in einem Unterordner `src/`

## Test des Agda-Projekts
Erstellen Sie eine Datei `src/Test.agda` mit dem Inhalt:
```agda
id : ∀ (S : Set) → S → S
id S x = x
```
* Lassen Sie den Editor die Datei Typ-prüfen.
* Führen Sie `agda src/Test.agda` manuell aus.

## Even/Odd
```agda

open import Data.Unit
open import Data.Empty
open import Data.Nat using (ℕ; zero ; suc; _+_)
open import Data.Bool using (Bool; true; false; not; T)
open import Function.Bundles using (_⇔_)

data Even : ℕ → Set where
  0-Even : Even zero
  2+-Even : ∀ k → Even k → Even (suc (suc k))
```
Definieren Sie eine Funktion
```
even? : ℕ → Bool
even? zero = true
even? (suc zero) = false
even? (suc (suc x)) = even? x

even?' : ℕ → Bool
even?' zero = true
even?' (suc x) = not (even?' x)

open import Relation.Binary.PropositionalEquality

not∘not≡id : ∀ b → not (not b) ≡ b
not∘not≡id false = refl
not∘not≡id true = refl

even?≗even?' : ∀ n → even? n ≡ even?' n
even?≗even?' zero = refl
even?≗even?' (suc zero) = refl
even?≗even?' (suc (suc n)) = sym goal
  where
    IH : even?' n ≡ even? n
    IH = sym (even?≗even?' n)
    x = even?' n
    y = even? n

    goal : not (not x) ≡ y
    goal = trans (not∘not≡id x) IH

    -- Alternativer Beweis:
    P : Bool → Set
    P z = not (not x) ≡ z

    goal' : not (not x) ≡ y
    goal' = subst P IH (not∘not≡id x)
```
Beweisen Sie deren Korrektheit:
```
even?-correct₁ : ∀ k → Even k → T (even? k)
even?-correct₁ 0 0-Even = tt
even?-correct₁ (suc (suc k)) (2+-Even k e) = even?-correct₁ k e

even?-correct₂ : ∀ k → T (even? k) → Even k
even?-correct₂ zero e = 0-Even
even?-correct₂ (suc (suc k)) e = 2+-Even k (even?-correct₂ k e)
```

## Church-Numerale

Wandeln Sie natürliche Zahlen in Church-Numerale und wieder zurück um:
```

Numeral : Set₁
Numeral = ∀ {X : Set} → (X → X) → (X → X)

⌈_⌉ : ℕ → Numeral
⌈ zero ⌉ f x = x
⌈ suc k ⌉ f x = f (⌈ k ⌉ f x)

toℕ : Numeral → ℕ
toℕ g = g suc zero
```

Beweisen Sie, dass die Umwandlung (in die eine Richtung) korrekt ist:
```
toℕ⌈n⌉≡n : ∀ n → toℕ ⌈ n ⌉ ≡ n
toℕ⌈n⌉≡n zero = refl
toℕ⌈n⌉≡n (suc n) = cong suc (toℕ⌈n⌉≡n n)

```