1 Getting started

In the labs we are going to use Agda. In case you have a problem, feel free to - ask me, - have a look at this page recalling the basics of Agda, - read the official documentation.

All the labs are following each other: - you should work in the same directory for all labs - you should work regularly

The labs are graded: - the best and most simple is that you create a private github repository for that and add me (smimram) to it - otherwise, please send me regularly you Agda files by mail

1.1 Installing Agda on your own computer

1.1.1 Linux

If you have a Linux distribution such as Ubuntu or Debian simply type

sudo apt-get install agda

in order to install Agda.

1.1.2 Permission denied in Ubuntu

If you have a permission denied problem with Ubuntu, you have probably hit a known bug in the package for the standard library (agda-stdlib version 1.7.3-1). Make sure that we are talking about the incriminated package by typing

apt-cache policy agda-stdlib

and check that the installed version is 1.7.3-1. If this is the case, you can to the following in order to circumvent it. Type as root:

cd /usr/share/agda-stdlib
echo "name: standard-library-1.7.1" > standard-library.agda-lib
echo "flags: -WnoUnsupportedIndexedMatch" >> standard-library.agda-lib
mkdir _build
chmod 777 _build

1.1.3 MacOS

On MacOS, you can install Agda via Homebrew with

brew install agda

Beware, you should also follow the instructions displayed in the end in order to properly install the standard library.

1.1.4 Windows

On Windows, you should use Windows subsystem for Linux (aka WSL) and refer to the above documentation for Linux.

1.2 Editors

The following editors support Agda:

• Emacs (with the Agda mode which is usually installed along with Agda)
• VSCode with the dedicated Agda mode (called agda-mode)
• vim with the dedicated Agda mode

If you are using VSCode you might need to type UTF-8 symbols as *times instead of \times.

1.3 Shortcuts

We recall that the most useful shortcuts are

2 Our first proof

2.1 Minimal standard library

You first need to download our ``minimal standard library’’ which is in the file Prelude.agda and put it in the same directory as the one you will work in during the labs.

Have a look at this file.

2.2 Getting started

Open a new file name Introduction.agda and type the following (recall that “×” is entered with \times and “→” with \to):

open import Prelude

comm× : {A B : Type} → A × B → B × A
comm× (a , b) = b , a

Then

1. Use C-c C-l to load the file.
2. Use C-c C-, to obtain the type of the hole.
3. Use C-c C-c then p to observe the argument.
4. Use C-c C-r to refine the hole.
5. Enter the answers in the two holes and use C-c C-space.

In this example, you could have directly defined the λ-term, but in general you will see that it is necessary to use the holes, so start getting used to those!

3 Products and coproducts

3.1 Commutativity of product

Show that product is commutative, i.e. provide a proof of

comm× : {A B : Type} → A × B → B × A

3.2 Involutivity of commutativity

Show that the function you have just defined is involutive:

comm×-involutive : {A B : Type} (a : A) (b : B) → comm× (comm× (a , b)) ≡ (a , b)

We recall that the constructor for equality is called refl.

3.3 Associativity of product

Show that product is associative:

assoc× : {A B C : Type} → (A × B) × C → A × (B × C)

3.4 Commutativity of coproduct

Show that coproduct is commutative:

comm⊎ : {A B : Type} → A ⊎ B → B ⊎ A

We recall that the symbol “⊎” is typed \uplus and that the two canonical injections into the coproduct are noted inl and inr, i.e. coproduct is defined as the inductive type

data _⊎_ (A : Type) (B : Type) : Type where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

3.5 Involutivity of commutativity

Define a function comm⊎-involutive showing that the function comm⊎ is involutive.

3.6 Distributivity

Show that product distributes over coproducts:

dist⊎ : {A B C : Type} → A × (B ⊎ C) → (A × B) ⊎ (A × C)

3.7 Currying

Define equivalence with

_↔_ : (A B : Type) → Type
A ↔ B = (A → B) × (B → A)

Show that we have the following equivalence:

currying : {A B C : Type} → (A × B → C) ↔ (A → B → C)

We recall that you can capture the optional arguments by taking arguments of the form {A}. It will be useful two define two local functions, we recall that this can be done with the where keyword.

4 Natural numbers

We recall that natural numbers are defined in the standard library as

data ℕ : Type where
  zero : ℕ
  suc  : ℕ → ℕ

You can type “ℕ” as \bN.

4.1 Addition

Define addition by induction on the first argument:

_+_ : ℕ → ℕ → ℕ

(you should perform a recurrence on the first argument).

4.2 Predecessor

Define predecessor:

pred : ℕ → ℕ

4.3 Neutral element on the left

Show that zero is neutral on the left for addition

+-unitl : (n : ℕ) → zero + n ≡ n

The symbol “≡” for equality is typed \equiv.

4.4 Congruence

Show that equality is a congruence:

cong : {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y

Hint: we recall that equality is defined as the inductive type

data _≡_ {A : Type} (x : A) : (y : A) → Type where
  refl : x ≡ x

so that you can reason on equality proofs with pattern matching.

4.5 Neutral element on the right

Show that zero is neutral on the right for addition:

+-assoc : (m n o : ℕ) → (m + n) + o ≡ m + (n + o)

4.6 Symmetry

Show that equality is symmetric:

sym : {A : Type} {x y : A} → x ≡ y → y ≡ x

4.7 Transitivity

Show that equality is transitive:

trans : {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z

4.8 Adding a successor

Show the following useful lemma:

+-suc : (m n : ℕ) → m + (suc n) ≡ suc (m + n)

4.9 Addition is commutative

Show that addition is commutative:

+-comm : (m n : ℕ) → m + n ≡ n + m

4.10 Predecessor of successor

Show that predecessor is left inverse for successor:

pred-suc : (n : ℕ) → pred (suc n) ≡ n

4.11 Successor of predecessor

Show that successor is left inverse for predecessor on non-zero numbers:

suc-pred : (n : ℕ) → ¬ (n ≡ zero) → suc (pred n) ≡ n

We recall that ¬ A is defined as A → ⊥ and that the recurrence principle for ⊥ is called ⊥-rec (it states that if we can prove false then anything can be deduced).

4.12 Zero and successor

Show that 0 is different from any succesor:

zero-suc : (n : ℕ) → ¬ (zero ≡ suc n)

4.13 Successor is injective

Show that successor is injective:

suc-inj : {m n : ℕ} → suc m ≡ suc n → m ≡ n

4.14 Equality is decidable

Show that equality is decidable on natural numbers:

nat-eq-dec : (m n : ℕ) → (m ≡ n) ⊎ ¬ (m ≡ n)

4.15 Division by 2

Define division by 2 on natural numbers:

div2 : (n : ℕ) → Σ ℕ (λ q → q + q ≡ n ⊎ suc (q + q) ≡ n)

4.16 Substitutivity

Show that equality is substitutive:

subst : {A : Type} (P : A → Type) {x y : A} → x ≡ y → P x → P y

4.17 Even numbers

Define the predicate of being even as

data Even : ℕ → Type where
  evenZero : Even zero
  evenSuc  : {n : ℕ} → Even n → Even (suc (suc n))

and show that doubling a natural number produces an even number:

double-even : (n : ℕ) → Even (n + n)