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. Nach erfolgreicher Installation lässt sich agda wie folgt aufrufen:
$ agda --version
Agda version 2.8.0

Erstellen eines Agda-Projekts

Erstellen Sie im Wurzel-Verzeichnis Ihres persönlichen Agda-Projekts eine Datei itp.agda-lib mit dem Inhalt:

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:

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

open import Data.Nat using (ℕ; zero ; suc; _+_)
open import Data.Bool using (Bool; true; false; 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? = {!!}

Beweisen Sie deren Korrektheit:

even?-correct₁ : ∀ k → Even k → T (even? k)
even?-correct₁ = {!!}
even?-correct₂ : ∀ k → T (even? k) → Even k
even?-correct₂ = {!!}

Church-Numerale

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

open import Relation.Binary.PropositionalEquality

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

⌈_⌉ : ℕ → Numeral
⌈_⌉ = {!!}

toℕ : Numeral → ℕ
toℕ = {!!}

Beweisen Sie, dass die Umwandlung (in die eine Richtung) korrekt ist:

toℕ⌈n⌉≡n : ∀ n → toℕ ⌈ n ⌉ ≡ n
toℕ⌈n⌉≡n = {!!}

Agda Quellcode herunterladen