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. A solution here consists in reasoning by case analysis on `b`

: do this and 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 `*`

).

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

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`

).

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

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

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.

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:

Our goal is to define a similar function

in Agda, which requires a new construction, called `with`

, that we now explain. As usual, we begin with

and perform a case analysis on `l`

so that we obtain

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.

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:

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.