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

Start with a new file `Bool.agda`

.

Define the type `Bool`

of *booleans* as an inductive type with two constructors:

Define the negation `neg`

as the function of type `Bool → Bool`

. You can start with

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

Define disjunction.

Define equality by

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`

.

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

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?

Construct a term of the following type:

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

.

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

Define multiplication (noted `*`

).

Copy again the definition of equality in this file

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

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.

Show that the following properties are satisfied:

- \(\forall n\in\mathbb{N}. 0+n=n\)
- \(\forall n\in\mathbb{N}. n+0=n\)
- \(\forall m,n,p\in\mathbb{N}. (m+n)+p=m+(n+p)\)
- \(\forall m,n\in\mathbb{N}. (m+n)+1=m+(n+1)\)
- \(\forall n, 0\neq n+1\)

Above, “\(n+1\)” is always understood as the successor of \(n\).

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`

).

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

Show that equality is symmetric:

transitive

and a congruence

How can you prove `suc-≡`

using `cong`

?

Show that addition is commutative:

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

Show that `suc`

is injective.

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:

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

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”:

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

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

In a new file `List.agda`

, define lists by

The symbol `∷`

is *not* `::`

, it is typed as `\::`

.

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

Define the length function:

Note that we have chosen to make the type parameter `A`

is implicit since it can be inferred from the list (the second argument).

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.

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`

:

- Define (in Agda) a function
`snoc`

which appends an element at the end of a list (the element becomes the last element). - Define the function
`rev`

which reverses the order of the elements of a list. - 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. - 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.

In OCaml, there is a `List.filter`

function whose type is

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:

In Agda, import the library for booleans

and define a similar function

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

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:

natural numbers:

conjunction and disjunction:

In particular, you can use the `+-suc`

lemma which is

Define a function

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

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

and show the Agda transcription of the above property:

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

The allows the use of the Agda notation

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:

Start a new file `Vector.agda`

.

Import the library of lists

and try to define the *head* function

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

Import the library of natural numbers as

and define the type of *vectors* as

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.

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

Define the *reversal* function on vectors.

We define the type

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.

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

in order to have access to products.

Import the functions related to equality

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:

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

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

by

Use it to simplify the above proof.