ITP Exercise Sheet 01

Discussion: 23 April 2026

The exercise sheets themselves are written in "Literate Agda" with Markdown (*.lagda.md). If you download them (see the link at the very bottom), you can edit them interactively just like other *.agda files. That is why the last Agda snippet in them has to be followed by another ```.

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

Setting up Agda

  • Install Agda (version 2.8.0), cf. Setup. After a successful installation, agda can be invoked as follows:
$ agda --version
Agda version 2.8.0

Creating an Agda project

In the root directory of your personal Agda project, create a file itp.agda-lib with the following content:

name: itp
depend:
  standard-library-2.3
include:
  src
  • The name of the project is itp (freely choosable)
  • The project requires the agda stdlib at version 2.3
  • The Agda files of our project live in a subdirectory src/

Testing the Agda project

Create a file src/Test.agda with the following content:

id : ∀ (S : Set) → S → S
id S x = x
  • Let the editor type-check the file.
  • Run agda src/Test.agda manually.

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))

Define a function

even? : ℕ → Bool
even? = {!!}

Prove its correctness:

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

Church numerals

Convert natural numbers into Church numerals and back again:

open import Relation.Binary.PropositionalEquality

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

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

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

Prove that the conversion is correct (in one direction):

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

Agda Quellcode herunterladen