This TD introduces inductive types in Agda. It is supposed to be done over two sessions. The various parts are mostly independent.

1 Booleans

Start with a new file Bool.agda.

1.1 The type of booleans

Define the type Bool of booleans as an inductive type with two constructors:

data Bool : Set where
  true  : Bool
  false : Bool

1.2 Negation

Define the negation not as the function of type Bool → Bool. You can start with

not : Bool → Bool
not b = ?

1.3 Conjunction

Define the conjunction _∧_ of type Bool → Bool → Bool (we recall that ∧ is typed on the keyboard as \and). The “underscore” notation means that this operation is infix. You can start with

_∧_ : Bool → Bool → Bool
a ∧ b = ?

1.4 Disjunction

Define disjunction.

2 Equality

Define equality by

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

infix 4 _≡_

Equality is an inductive type which depends on two terms x and y. It has only one constructor (named refl) which is of type x ≡ x, for any term x. You can forget about the “infix” line, which is only to indicate the priorities when parsing the symbol ≡. By the way, the symbol ≡ is typed by \equiv.

2.1 Negation is involutive

We want to show that applying twice the negation does not change anything. A first idea is thus the following proof:

not-inv : (b : Bool) → not (not b) ≡ b
not-inv b = refl

Try it and read the error message: the problem here is that not (not b) and b are not the same, whereas the refl constructor has type x ≡ x for some x. This comes from the fact that b is a variable, which prevents not (not b) from reducing. How can we complete the proof?

2.2 Conjunction and negation

Construct a term of the following type:

(b : Bool) → (not b) ∧ b ≡ false

3 Natural numbers

We are now going to define natural numbers and show some basic properties about those. Start a new file Nat.agda.

3.1 Definition

Define the type ℕ of natural numbers, coded in unary, as an inductive type with two constructors zero and suc. The symbol ℕ is typed as \bN.

3.2 Addition

Define addition as a term of type

_+_ : ℕ → ℕ → ℕ

3.3 Multiplication

Define multiplication (noted *).

3.4 Equality is a congruence for successor

Copy again the definition of equality in this file

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

infix 4 _≡_

We want to show that equality is a congruence:

\[ \forall m\in\mathbb{N}. \forall n\in\mathbb{N}. m=n \Rightarrow (m+1)=(n+1) \]

We thus begin defining a term with

suc-≡ : {m n : ℕ} → (m ≡ n) → (suc m ≡ suc n)
suc-≡ e = ?

Note that we have declared the two arguments m and n as implicit since they can be inferred from the third argument (which is a proof of m ≡ n).

Reason by case analysis on the argument e, observe what is happening and explain it. Finish the proof.

3.5 Some properties

Show that the following properties are satisfied:

1. \(\forall n\in\mathbb{N}. 0+n=n\)
2. \(\forall n\in\mathbb{N}. n+0=n\)
3. \(\forall m,n,p\in\mathbb{N}. (m+n)+p=m+(n+p)\)
4. \(\forall m,n\in\mathbb{N}. (m+n)+1=m+(n+1)\)
5. \(\forall n, 0\neq n+1\)

Above, “\(n+1\)” is always understood as the successor of \(n\). In the last question, you should open import Relation.Nullary in order to have access to negation.

3.6 The recurrence principle

In mathematics, the recurrence principle asserts that if \(P\) is a predicate on natural numbers such that

• \(P(0)\) holds, and
• for every \(n\in\mathbb{N}\), \(P(n)\) holds implies \(P(n+1)\) holds,

the \(P(n)\) holds for every natural number \(n\).

Prove the recurrence principle in Agda (a proposition can be formalized as a function ℕ → Set) :

rec : (P : ℕ → Set) → ...

Use this to prove \(\forall n\in\mathbb{N}. n+0=n\) again.

3.7 More equality

Show that equality is symmetric:

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

transitive

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

and a congruence

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

How can you prove suc-≡ using cong?

3.8 Commutativity of addition

Show that addition is commutative:

\[ \forall m,n\in\mathbb{N}. m+n=n+m \]

3.9 Injectivity of successor

Show that suc is injective.

3.10 Decidability of equality

Show that equality is decidable on natural numbers. This means that we have an algorithm which, given two natural numbers says whether they are equal or not. In Agda, this can be formalized by constructing a term of the following type:

(m n : ℕ) → (m ≡ n) ∨ ¬ (m ≡ n)

In order to have access to the negation (¬) and the disjunction (∨), you should first import the required modules:

open import Relation.Nullary
open import Data.Sum renaming (_⊎_ to _∨_ ; inj₁ to left ; inj₂ to right)

We recall that the syntax for defining a function f n by matching with another argument looks like

f n with bla
... | b = ?

3.11 Recurrence for equality

We shown the recurrence principle for natural numbers. In fact, any inductive type has an associated recurrence principle. The one for equality is called “J”:

J : (A : Set) → (P : (x : A) → (y : A) → (p : x ≡ y) → Set) → (r : (x : A) → P x x refl) → (x : A) → (y : A) → (p : x ≡ y) → P x y p

Read it carefully: what does it mean? Then, prove it.

3.12 Properties of multiplication

We now turn to multiplication. You can skip this part at first and come back to it later if you have time.

• Show that multiplication is commutative \[ \forall m,n\in\mathbb{N}. m\times n=n\times m \] You will certainly need to show preliminary lemmas.
• Also, show that multiplication is associative \[ \forall m,n,p\in\mathbb{N}. (m\times n)\times p=m\times(n\times p) \]

4 Lists

In a new file List.agda, define lists by

data List (A : Set) : Set where
  []  : List A
  _∷_ : A → List A → List A

infixr 5 _∷_

The symbol ∷ is not ::, it is typed as \::.

4.1 Length

Import the library defining functions related to natural numbers and equality:

open import Data.Nat
open import Relation.Binary.PropositionalEquality

Define the length function:

length : {A : Set} → List A → ℕ

Note that we have chosen to make the type parameter A is implicit since it can be inferred from the list (the second argument).

4.2 Concatenation

• Define a function concat which concatenates two lists (of arbitrary type).
• Show that the length of the concatenation of two lists is the sum of their lengths.
• Show that concatenation is associative.

4.3 List reversal

Our aim is now to define and study in Agda the function which reverses the order of elements of a list. For instance, in OCaml this function is called List.rev:

# List.rev [1;4;5;7];;
- : int list = [7; 5; 4; 1]

1. Define (in Agda) a function snoc which appends an element at the end of a list (the element becomes the last element).
2. Define the function rev which reverses the order of the elements of a list.
3. Show that the rev function preserves the length. In order to complete your proof you are likely to need to prove an auxiliary lemma first.
4. More difficult, show that the rev function applied twice to a list does not change the list. Here also you are likely to need an appropriate lemma.

4.4 Filtering

In OCaml, there is a List.filter function whose type is

('a -> bool) -> 'a list -> 'a list

such that List.filter p l returns the list obtained from l by keeping only the elements x such that p x is true. For instance, we can compute the even elements of a list of integers:

# List.filter (fun n -> n mod 2 = 0) [1;3;4;6;7;10;11;12];; 
- : int list = [4; 6; 10; 12]

In Agda, import the library for booleans

open import Data.Bool

and define a similar function

filter : {A : Set} → (p : A → Bool) → (l : List A) → List A

• Complete the definition of filter.
• Show that filtering a list by the constant function equal to false always gives the empty list.
• Show that filtering a list by the constant function equal to true always gives the original list.

5 Division by 2

In this section, we are going to prove the correctness of a first (very simple) algorithm: division by two. There are two approaches for that:

• in the extrinsic approach, we define the algorithm and after that show that it is correct,
• int the intrinsic approach, we directly give the algorithm a type which is rich enough to ensure that it is correct.

We are going to try both ways. Start a new file Div2.agda and import the libraries you will need:

• equality:

  open import Relation.Binary.PropositionalEquality

• natural numbers:

  open import Data.Nat
  open import Data.Nat.Properties using (+-suc)

• conjunction and disjunction:

  open import Data.Product renaming (_×_ to _∧_)
  open import Data.Sum renaming (_⊎_ to _∨_ ; inj₁ to left ; inj₂ to right)

In particular, you can use the +-suc lemma which is

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

5.1 Extrinsic approach

Define a function

div2 : ℕ → ℕ

which computes the quotient of the division by two of its argument. You can test your function by defining a value such as

test5 : ℕ
test5 = div2 (suc (suc (suc (suc (suc zero)))))

which corresponds to div2 applied to 5 and evaluate it by typing C-c C-n, which is the shortcut to normalize an expression, and asking to normalize text5: the answer should be 2 here, i.e., suc (suc zero).

The correctness of this function is given by the specification of division: we want to show that

\[ \forall n\in\mathbb{N}.\exists r\in\mathbb{N}. (0\leq r<2) \land (n = 2 \times \mathrm{div2}(n) + r) \]

where \(r\) is the remainder of the division. Since the remainder can only be \(0\) or \(1\), this is equivalent to

\[ \forall n\in\mathbb{N}.(n = 2 \times \mathrm{div2}(n))\lor(n = 2 \times \mathrm{div2}(n)+1) \]

Import the module required for disjunction

open import Data.Sum renaming (_⊎_ to _∨_ ; inj₁ to left ; inj₂ to right)

and show the Agda transcription of the above property:

div2-correct : (n : ℕ) → (2 * div2 n ≡ n ∨ suc (2 * div2 n) ≡ n)

5.2 Intrinsic approach

In the intrinsic approach, we want to directly define the function of division by 2 with a type which ensures that its result is correct. In order to do so, we must first import the functions related to dependent sums (also called Σ-types):

open import Data.Product

The allows the use of the Agda notation

Σ A P

which is the type of dependent pairs (a , b) whose first element a is of type A and second element b is of type P a (note that P is a predicate of type A → Set, and the type of the second element depends on the first element). From a logical point of view, it can be read as “there exists an a in A such that P a”.

Now, construct a function of the following type:

div2' : (n : ℕ) → Σ ℕ (λ q → (2 * q ≡ n) ∨ (suc (2 * q) ≡ n))

6 Vectors

Start a new file Vector.agda.

6.1 Warmup

Import the library of lists

open import Data.List

and try to define the head function

head : {A : Set} → List A → A

which returns the first element of a list. What is the problem?

6.2 Definition

Import the library of natural numbers as

open import Data.Nat

and define the type of vectors as

data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

An term of type Vec n can be thought of as a list whose length is exactly n.

6.3 Head and tail

Define functions to compute the head and tail of a vector. Be careful to correctly type those so that they are always defined.

6.4 Concatenation

Define a concatenation function on vectors. Note that the type proves that it corresponds to sum on lengths.

6.5 Reversal

Define the reversal function on vectors.

6.6 Accessing an element

We define the type

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

The elements of Fin n can be thought of as natural numbers i with 0 ≤ i < n.

Define the function which, given \(i\) and a vector, computes the \(i\)th element of the vector.

6.7 Zipping

Given two vectors \(x_1,\ldots,x_n\) and \(y_1,\ldots,y_n\), define the zip function which returns the vector of pairs \((x_1,y_1),\ldots,(x_n,y_n)\). You should first do

open import Data.Product hiding (zip)

in order to have access to products.

6.8 Optional: associativity of concatenation

Import the functions related to equality

open import Relation.Binary.PropositionalEquality

Try to prove that concatenation is associative for vectors. What is the problem?

Define the coercion function which expresses the fact that when two types are equal we can see an element of the first as an element of the second:

coe : {A B : Set} → A ≡ B → A → B

Use it to correctly formulate the fact that concatenation of vectors is associative. It can be useful to import the proof of associativity of addition (+-assoc) by

open import Data.Nat.Properties using (+-assoc)

Show that concatenation of vectors is associative. You will certainly need first a lemma expressing the fact that if l is a vector of length n and l' is a vector of length n' such that n and n' are equal and l and l' are equal then x ∷ l and x ∷ l' are also equal, for any x of the expected type (you need to use the appropriate congruences and coercions in order to properly formulate that).

As you can see this is fairly complicated… This can be simplified by using a variant of equality, called heterogeneous equality, which allows the comparison of two elements of distinct types. It is defined in the module

import Relation.Binary.HeterogeneousEquality

by

data _≅_ : {A B : Set} (x : A) (y : B) → Set where
  refl : {A : Set} {x : A} → x ≅ x

Use it to simplify the above proof.

7 The Gauss formula

The goal of this section is to prove the Gauss formula for summing the first \(n+1\) natural numbers:

\[ \sum_{i=0}^ni=\frac{n(n+1)}{2} \]

Start a new file Gauss.agda and import libraries concerning natural numbers and equality

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

We also want to import our definition div2 of division by two defined in the Div2.agda file: add

open import Div2

you will also need to add

module Div2 where

at the beginning of Div2.agda in order to specify that it declares a public module.

7.1 Reasoning with equality

As you have been able to see, reasoning with equality can be tedious. In order to improve the situation, the standard library defines notations which allow reasoning with equality in the usual way. Import those by adding

open ≡-Reasoning

Once this is done, we can prove commutativity of addition with

+-com : (m n : ℕ) → m + n ≡ n + m
+-com zero    n = sym (+-identityʳ n)
+-com (suc m) n = begin
  suc m + n   ≡⟨ refl ⟩
  suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩
  suc (n + m) ≡⟨ sym (+-suc n m) ⟩
  n + suc m   ∎

which is equivalent to the following, but much easier to read:

+-com : (m n : ℕ) → m + n ≡ n + m
+-com (suc m) n = trans refl (trans (cong suc (+-comm m n)) (sym (+-suc n m)))

Exercise yourself by reproving +-com with the new notation. You begin with

+-com : (m n : ℕ) → m + n ≡ n + m
+-com zero    n = sym (+-identityʳ n)
+-com (suc m) n = begin
  suc m + n   ≡⟨ ? ⟩
  n + suc m   ∎

and progressively add the required reasoning steps and fill in the holes.

7.2 Dividing a double

Show that division is a semi-inverse of multiplication by two by proving

div2-double : (n : ℕ) → div2 (2 * n) ≡ n

using the above notation when useful.

7.3 Triangular numbers

Define a function

triangular : ℕ → ℕ

which to a natural number \(n\) associates the \(n\)-th triangular number

\[ T_n=\sum_{i=0}^ni \]

7.4 Gauss formula

Show the Gauss formula by proving

gauss : (n : ℕ) → triangular n ≡ div2 (n * suc n)

You can draw inspiration from the traditional proof but be prepared to prove a few auxiliary lemmas. You are advised to use the above notation for reasoning about equality.

8 Optional: Euclidean division

In the following you are not expected to deal with termination issues. You can therefore assume that functions are terminating by using the pragma

{-# TERMINATING #-}

before their definition (we will see how to handle those issues in subsequent courses).

8.1 Definition

Define the quotient and remainder functions over natural numbers.

8.2 Correctness

Show that your definitions are correct according to the usual specification of division: for every natural numbers \(m\) and \(n\), with \(n\neq 0\), we have

\[ m = (m / n) * n + (m \operatorname{mod} n) \]

8.3 Internal approach

Define euclidean division and show its correction using the intrinsic approach.