Inductive types

Samuel Mimram

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

3.6 The recurrence principle

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

the \(P(n)\) holds for every natural number \(n\). Prove the recurrence principle in Agda (a proposition can be formalized as a function 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

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:

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

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