The goal of this TD is to prove a (somewhat) realistic algorithm: a sorting algorithm on lists. It is supposed to be done over two sessions.

Create a new file `Sort.agda`

and begin by importing the libraries necessary to have access to equality, truth, conjunction, disjunction, natural numbers, products and lists:

```
open import Relation.Binary.PropositionalEquality
open import Data.Unit using (⊤ ; tt)
open import Data.Product renaming (_×_ to _∧_ ; proj₁ to fst ; proj₂ to snd)
open import Data.Sum renaming (_⊎_ to _∨_ ; inj₁ to left ; inj₂ to right)
open import Data.Nat using (ℕ ; zero ; suc)
open import Data.Product renaming (proj₁ to fst ; proj₂ to snd)
open import Data.List hiding (length ; head)
```

For simplicity, we are going to sort lists of natural numbers. We must thus first define the order on those.

The usual order on natural numbers can be defined as the inductive type

```
data _≤_ : ℕ → ℕ → Set where
: {n : ℕ} → zero ≤ n
z≤n : {m n : ℕ} (m≤n : m ≤ n) → suc m ≤ suc n s≤s
```

(the symbol `≤`

is typed by `\le`

).

Show that it is compatible with successor by constructing terms

`: {m n : ℕ} → (suc m ≤ suc n) → m ≤ n ≤-pred `

and

`: {m n : ℕ} → m ≤ n → suc m ≤ suc n ≤-suc `

and

`: (n : ℕ) → n ≤ suc n ≤s `

Show that the order is reflexive:

`≤-refl : (n : ℕ) → n ≤ n`

Show that the order is transitive:

`: {m n p : ℕ} → (m ≤ n) → (n ≤ p) → (m ≤ p) ≤-trans `

Show that the order is total, meaning that any pair of natural number can be compared:

`_≤?_ : (m n : ℕ) → (m ≤ n) ∨ (n ≤ m)`

We are interested in the insertion sort algorithm, which is a simple sorting algorithm, although not very efficient.

Define a function

`: (x : ℕ) → (l : List ℕ) → List ℕ insert `

which given an element `x`

and a list `l`

, which is supposed to be sorted, inserts `x`

in `l`

so that the result is sorted.

Use this function to program a function

`: List ℕ → List ℕ sort `

which sorts a list (by iteratively inserting its elements to the empty list).

In order to test your function, you can define a term such as

```
: List ℕ
test = sort (4 ∷ 1 ∷ 45 ∷ 8 ∷ 32 ∷ 12 ∷ 1 ∷ []) test
```

and normalize it using the `C-c C-n`

shortcut.

Define a predicate

`_≤*_ : (x : ℕ) → (l : List ℕ) → Set`

such that `x ≤* l`

means that `x ≤ y`

is satisfied for every element of `l`

(this function can be defined recursively, without defining the predicate of belonging to a list). You can either define this directly or as an inductive type, as you wish.

Define a predicate

`: (l : List ℕ) → Set sorted `

which expresses that a list is sorted.

Show that `insert`

ing an element in a sorted list produces a sorted list:

`: (x : ℕ) → (l : List ℕ) → sorted l → sorted (insert x l) insert-sorting `

This proof might first require you to show (two) auxiliary lemmas.

Finally, show that the function `sort`

always produces a sorted list.

Actually, the specification is not complete. Construct a (very simple) function

`: List ℕ → List ℕ f `

which is *not* sorting its argument, and for which we can prove

`: (l : List ℕ) → sorted (f l) f-sorting `

What is missing from the specification of the `sort`

function? We shall address this issue later on. For now, we are only interested in proving that `sort`

is returning a sorted list.

The above proof method was *extrinsic*: we first defined the sorting function and then showed that it was correct. We now investigate the *intrinsic* approach, which consists in directly defining the function with a type ensuring its correctness.

Try to define an inductive `Sorted`

type with two constructors, such that the terms of this type can be thought of as the sorted lists. Do you manage to do it? If not, why?

In Agda, we can define functions which are *mutually recursive*: one is calling the other and vice versa. For instance, the functions `even`

and `odd`

, which determine whether a natural number is even or odd, can be defined by mutual recursion by

```
mutual
: ℕ → Bool
even = true
even zero (suc n) = odd n
even
: ℕ → Bool
odd = false
odd zero (suc n) = even n odd
```

Define by mutual recursion the inductive type `Sorted`

(whose constructors are called `nil`

and `cons`

) together with a function `head`

which returns the first element of a sorted list or a default value if the list is empty:

```
mutual
data Sorted : Set where
...
: ℕ → Sorted → ℕ
head = ? head d l
```

Define an insertion function

`: (x : ℕ) → Sorted → Sorted insert' `

For the last case of the definition, you might need to prove a lemma, formulated as a mutually recursive function.

Finally, define a sorting function

`: (l : List ℕ) → Sorted sort' `

*Please do next sections first and come back here if you have time.*

The goal of this section is to show that the insertion sort function is actually returning a sorted version of its input list. As we have seen, it is not enough to show that it returns a sorted list since the sorted list might have nothing to do with the original list. What is missing is that the list in the output of `sort l`

has the same elements of the input list `l`

. We might want to be even more picky and show that the sorting function preserves the multiplicities of the elements, i.e,

`(3 ∷ 1 ∷ 1 ∷ []) sort `

is

`1 ∷ 1 ∷ 3 ∷ []`

and not

`1 ∷ 3 ∷ 3 ∷ []`

nor

`1 ∷ 3 ∷ []`

A way to show this is to prove that the sorted list is a *permutation* of the original one. Since permutations are generated by transpositions (exchanging two consecutive elements), we can define the following relation `∼`

which expresses that a list is a permutation of another:

```
data _∼_ {A : Set} : List A → List A → Set where
: [] ∼ []
∼-nil : (x : A) {l l' : List A} → l ∼ l' → (x ∷ l) ∼ (x ∷ l')
∼-drop : (x y : A) (l : List A) → (x ∷ y ∷ l) ∼ (y ∷ x ∷ l)
∼-swap : {l l' l'' : List A} → l ∼ l' → l' ∼ l'' → l ∼ l'' ∼-trans
```

Show that the relation `∼`

is reflexive

`: {A : Set} {l : List A} → l ∼ l ∼-refl `

and symmetric

`: {A : Set} {l l' : List A} → l ∼ l' → l' ∼ l ∼-sym `

Show that insertion permutes the first element:

`: (x : ℕ) (l : List ℕ) → (x ∷ l) ∼ (insert x l) insert-∼ `

Show that insertion is compatible with permutation

`: (x : ℕ) {l l' : List ℕ} → l ∼ l' → insert x l ∼ insert x l' ∼-insert `

(recall that the `C-c C-a`

shortcut instructs Agda to try to automatically fill a hole).

Show that sorting produces a permutation of the original list:

`: (l : List ℕ) → l ∼ (sort l) sort-∼ `

As indicated above, the insertion sort we studied is not realistic because not very efficient. We now turn to *merge sort* which has a decent complexity. This sorting algorithm proceeds in three phases:

- split the input list \(l\) into two lists \(l_1\) and \(l_2\) of roughly the same size (up to a difference of 1 if the length of the input list is odd),
- recursively sort the lists \(l_1\) and \(l_2\),
- recombine the two sorted lists into a sorted list.

We recall that `A × B`

is the notation for the product of the types `A`

and `B`

: terms of this type are pairs `(a , b)`

consisting of a term `a`

of type `A`

and a term `b`

of type `B`

. The functions `fst`

and `snd`

can be used to retrieve the first and second component of a pair.

Define a function

`: {A : Set} → List A → List A × List A split `

which splits a list in two (by returning the elements at even / odd position). For instance, the result of

`(4 ∷ 1 ∷ 45 ∷ 8 ∷ 32 ∷ 12 ∷ 1 ∷ []) split `

will be the pair

`(4 ∷ 45 ∷ 32 ∷ 1 ∷ [] , 1 ∷ 8 ∷ 12 ∷ [])`

Define a function

`: (l m : List ℕ) → List ℕ merge `

such that if `l`

and `m`

are sorted lists then their merge is the sorted list containing the elements of both. It can be defined recursively by comparing the first elements of `l`

and `m`

with `≤?`

.

*It might be the case that Agda thinks that your function is not terminating whereas it should, simply ignore this.*

Finally, define the function

`: List ℕ → List ℕ mergesort `

You will certainly get an error message such as

`Termination checking failed for the following functions: mergesort`

because Agda could not ensure that the function is terminating. Of course, the function is terminating, because the lengths of the lists in the recursive calls do decrease, but Agda is not able to show it because it only considers functions which are *structurally decreasing*, i.e., those for which the recursive calls are performed on subterms of the arguments.

You can instruct Agda to trust it is by adding, just before the declaration of the function,

`{-# TERMINATING #-}`

Do this and test your function by normalizing (using the shortcut `C-c C-n`

) the term `test-merge`

defined by

```
: List ℕ
test-merge = mergesort (4 ∷ 1 ∷ 45 ∷ 8 ∷ 32 ∷ 12 ∷ 1 ∷ []) test-merge
```

The answer should be

`1 ∷ 1 ∷ 4 ∷ 8 ∷ 12 ∷ 32 ∷ 45 ∷ []`

and should be computed instantaneously. If you do not obtain an answer, this might indicate that your program is looping. This is case, use the menu *Agda* > *Kill and restart Agda* (or the shortcut `C-c C-x C-r`

) to stop Agda (and `C-c C-l`

should restart it).

Using `{-# TERMINATING #-}`

in Agda is cheating since we might not detect that your program is not terminating. Moreover, it might lead to inconsistencies:

```
open import Data.Empty
{-# TERMINATING #-}
: ⊥
absurd = absurd absurd
```

We would thus rather avoid that, and prove the termination of our program, which is the goal of the questions below.

Define the strict order `<`

on natural numbers (this can be done in one sort line, using `≤`

and `suc`

).

Define the `length`

function on lists by

```
: {A : Set} (l : List A) → ℕ
length = zero
length [] (x ∷ l) = suc (length l) length
```

Show that, given a list `l`

, the length of the first component of `split l`

is strictly smaller than the length of `l`

, for almost all lists `l`

.

Do the same proof for the second component.

In order for Agda, to know that the function is terminating, we construct a variant of the `mergesort`

function with an extra integer argument `n`

, the *fuel*, which is a bound on the number of steps the functions can make. The last added argument, of type `length l ≤ n`

, is here to ensure that we can actually make recursive calls when we are not in the base case. Define the function

`: (n : ℕ) → (l : List ℕ) → (length l ≤ n) → List ℕ mergesort-fuel `

Use it to give a proper definition of

`: (l : List ℕ) → List ℕ mergesort `

Test it as above.

Show that your implementation is returning a sorted list:

`: (l : List ℕ) → sorted (mergesort l) mergesort-sorting `

You are left with the choice of using the extrinsic or intrinsic approach (although the second one is advised). As in the first part, you will certainly have to prove some preliminary lemmas.

The types of relations on a given type is

```
: (A : Set) → Set₁
Rel = A → A → Set Rel A
```

We define the predicates of accessibility and well-foundedness by

```
data Acc {A : Set} (_<_ : Rel A) (x : A) : Set where
: ((y : A) → y < x → Acc _<_ y) → Acc _<_ x
acc
: {A : Set} → (_<_ : Rel A) → Set
WellFounded {A} _<_ = (x : A) → Acc _<_ x WellFounded
```

For now, we assume that ℕ is well-founded:

`postulate wfNat : WellFounded _<_`

Define merge sort by well-founded induction on the length of the list. You should first define an auxiliary function which acts like merge sort, but takes as extra argument a proof that the length of the list is accessible.

Our goal is now to show the above postulate. First, show the two auxiliary lemmas

`: {m n : ℕ} → (m ≤ n) → m ≡ n ∨ m < n ≤-< `

and

`<-last : {m n : ℕ} → (m < suc n) → m ≡ n ∨ m < n`

Remove the above postulate and show

`: WellFounded _<_ wfNat `