# Dependently typed programming

Matthieu Sozeau

Exercises on dependent pattern-matching and recursion. Lecture at CASS 2020.

## Buffer

We define a type buffer that can hold 0 to 2 values of a type [A].
Exercise: Define two boolean predicates that tell if a buffer is empty or full, named [empty_buffer] and [full_buffer]. Exercise: Using Program and subset types, Write functions [give] that removes an element from a non-empty buffer and [take] that adds an element to a non-full buffer.

## Filter

Give a strong specification and program a variant of [filter] on lists that returns the filtered list and a proof that all its elements satisfy the predicate. You can use the [In] predicate to express membership in the list [r]. To reflect [if then else] conditionals on booleans, used the [dec] combinator that transforms a boolean b into a proof of [{ b = true } + { b = false }].

### Dependent elimination:

We define the following indexed inductive type:
The proposition [excl_or p q] is inhabited only if p is true and q is false or vice-versa Show that <= and > have mutually exclusive results:
A typical use of this property is to dependently eliminate the proof of [excl_or] in a goal containing occurrences of [Nat.leb] and [gtb]: this will replace all occurrences with either [true] and [false], cutting down the 2^2 possible boolean combinations down to the two combinations of interest:
This uses a dependent elimination of the [excl_or] inductive. Following this example, prove the following proposition using dependent pattern-matching explicitely. Use the [refine] tactic to gradually build the proof term.
The exact same principle applies to the elimination of the [reflect] predicate seen in the first lecture.

## A small universe

Indexed inductive types are often used to reflect the typing structure of values in some particular domain. Here we define type code for natural and boolean values:
We can then make a new type of natural or boolean values, indexed by the type code:
A value in [val ty] can either be a natural number when [ty] is [Nat] or a boolean when [ty] is [Bool]. This allows to write generic functions that can work on either natural or boolean values. Here: a function that tests if the value is the least value in the naturals or booleans (false is considered below true).
Moreover, using dependent elimination, we can write *type-preserving* functions, that ensure that if the generic operation takes a value in type [ty] it returns a value in the same type. Write such a function [val_incr] that takes a nat or bool value and increments it (adding 1 to the natural, and mapping true and false to true)
State and prove a lemma showing that for any typ and [val] [v] of this type, val_bottom of val_incr of this value always returns false.

## Quicksort:

Quicksort is not a structurally recursive definition: [[ qs : list A -> list A qs [] = [] qs (x :: xs) = qs lower ++ (x :: qs upper) where lower = filter (fun y => y <= x) xs upper = filter (fun y => x < y) xs ]] Using Program Fixpoint, find a measure for which this function is terminating and solve the corresponding proof obligations. Use [About filter] to find lemmas related to [skipn] and the [lia] decision procedure to solve arithmetic goals. You can consult the fine reference manual page for help: https://coq.inria.fr/refman/addendum/program.html#coq:cmd.program-fixpoint You will need to prove lemmas about the relation of [filter] and [length] to solve the generated obligations. You can use the [Nat.leb] and [Nat.ltb] functions to program the comparisons.

# Extra exercise, Difficult (requires inductive predicates): prove the correctness properties of QuickSort.

- First show that the returned list has the same elements as the first one. - Then that the list is sorted, using the [Sorted] predicate below. You will need lemmas about concatenation of [Sorted] lists and use the [last] function on lists.

## Merge sort function

Suppose now we want to implement a merging sort algorithm: as a building block, we need a function that takes two sorted lists and interleaves their elements to produce a sorted lists containing the two original lists. Use [Nat.ltb] to compare the head elements of the two lists.
Again, this function is not structurally recursive, as the recursive calls will make only one of the arguments decrease. Use a measure to show its termination.

## Ackermann

The ackermann function is a standard example of non-primitive recursive definition. As such, it falls outside the syntactic guard criterion of recursive definitions:
Indeed [ackermann] is neither structurally recursive on [m] or [n] as we call [ackerman] on [S m'] in the inner recursive call (not a strict subterm of [m]) and on [m'] (a strict subterm of [m]) and [ackermann (S m') n'] (not a subterm of [n]) in the outer one. The function is however well-founded on the *lexicographic* ordering of the pair of arguments [(m, n)]: at each recursive call, either the first argument [m] decreases strictly or it stays the same but the second argument decreases strictly.