# Inductive types

This TD introduces inductive types in Agda. It is supposed to be done over two sessions.

# 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 neg 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. A solution here consists in reasoning by case analysis on b: do this and 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.

Define addition as a term of type

_+_ : ℕ → ℕ → ℕ

## 3.3 Multiplication

Define multiplication (noted *).

## 3.4 Equality is a congruence for successor

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

Above, “$$n+1$$” is always understood as the successor of $$n$$.

## 3.6 The recurrence principle

In mathematics, the recurrence principle asserts that if $$P$$ is a proposition 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).

## 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?

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

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

## 3.10 Optional: Properties of multiplication

Do this part only if you have finished early or decided to work late at home.

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.

## 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]

Our goal is to define a similar function

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

in Agda, which requires a new construction, called with, that we now explain. As usual, we begin with

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

and perform a case analysis on l so that we obtain

filter : {A : Set} → (p : A → Bool) → (l : List A) → List A
filter p [] = ?
filter p (x ∷ l) = ?

The first case is easily handled, but for the second case we need to reason by case analysis on the value of p x. We thus replace, the second line as follows:

filter : {A : Set} → (p : A → Bool) → (l : List A) → List A
filter p [] = ?
filter p (x ∷ l) with p x
... | b = ?

The with p x indicates that we want to match on the result of p x. In the line after, the ... are a shortcuts for the above line (i.e., filter p (x ∷ l)) and the variable b after the bar | is the result of p x: we can now reason by case analysis on b as usual.

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

## 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.

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)