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

Start with a new file `Bool.agda`

.

Define the type `Bool`

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

```
data Bool : Set where
: Bool
true : Bool false
```

Define the negation `not`

as the function of type
`Bool → Bool`

. You can start with

```
: Bool → Bool
not = ? not b
```

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

Define disjunction.

Define equality by

```
data _≡_ {A : Set} (x : A) : (y : A) → Set where
: x ≡ x
refl
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`

.

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

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

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:

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

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

```
data _≡_ {A : Set} (x : A) : (y : A) → Set where
: x ≡ x
refl
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

```
: {m n : ℕ} → (m ≡ n) → (suc m ≡ suc n)
suc-≡ = ? 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.

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 the last question, you should
`open import Relation.Nullary`

in order to have access to
negation.

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`

)
:

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

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

Show that equality is symmetric:

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

transitive

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

and a congruence

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

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:

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

```
with bla
f n ... | b = ?
```

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

`: (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 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

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

The symbol `∷`

is *not* `::`

, it is
typed as `\::`

.

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

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

Define the length function:

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

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`

:

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

- 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

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

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

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

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

`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

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

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 = div2 (suc (suc (suc (suc (suc zero))))) test5
```

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:

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

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:

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

Start a new file `Vector.agda`

.

Import the library of lists

`open import Data.List`

and try to define the *head* function

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

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

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.

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

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

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

`open import Data.Product hiding (zip)`

in order to have access to products.

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:

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

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
: {A : Set} {x : A} → x ≅ x refl
```

Use it to simplify the above proof.

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.

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

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

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

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

Exercise yourself by reproving `+-com`

with the new
notation. You begin with

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

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

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

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

using the above notation when useful.

Define a function

`: ℕ → ℕ triangular `

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

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

Show the Gauss formula by proving

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

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.

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

Define the quotient and remainder functions over natural numbers.

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

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