# Strongly-specified Functions in Coq

I started to play with Coq, the interactive theorem prover developed by Inria, a few weeks ago. It is a very powerful tool, yet hard to master. Fortunately, there are some very good readings if you want to learn1. This article is not one of them.

In this article, we will see how to implement strongly-specified list manipulation functions in Coq. Strong specifications are used to ensure some properties on functions’ arguments and return value. It makes Coq type system very expressive. Thus, it is possible to specify in the type of the function `pop` that the return value is the list passed in argument in which the first element has been removed!

## Defining the `list` type

Thanks to Coq polymorphism and inductive types, it is very simple to define what a list is. Note that to deal with polymorphism, we enclose all our Coq definitions in a `Section` block.

``````Section lists.
Variable A:Set.

Inductive list:Set :=
| nil: list
| cons: A → list → list.
End lists.``````

We can take a look at Ocaml extracted code.

``````type 'a list =
| Nil
| Cons of 'a * 'a list``````

## Is this list empty?

It’s the first question to deal with when manipulating lists. There are some functions that require their arguments not to be empty. It’s the case for the `pop` function, for instance: it is not possible to remove the first element of a list that does not have any elements in the first place.

When one wants to answer such a question as “Is this list empty?”, he has to keep in mind that there are two ways to do it: by a predicate or by a boolean function. Indeed, `Prop` and `bool` are two different worlds that do not mix easily. One solution is to write two definitions and to prove their equivalence. That is `∀ args`, `predicate args ↔ bool_function args = true`.

Another solution is to use the `Sumbool` type as middleman. The scheme is the following:

1. Defining `predicate: args → Prop`
2. Defining `predicate_dec: args → { predicate args } + { ~predicate args }`
3. Defining `predicate_b`:
``````  Definition predicate_b (args) :=
if predicate_dec args then true else false.``````

### Defining the `empty` predicate

A list is empty if it is `nil`. It’s as simple as that!

``  Definition empty (l:list):Prop := l = nil.``

### Defining a decidable version of `empty`

A decidable version of `empty` (`empty_dec`) is a function that takes a list and returns a `sumbool (empty l) (¬empty l)`. Such function can be used in an `if ... then ... else ...` construction.

``````  Definition empty_dec (l:list): {empty l} + {¬empty l}.
refine (
match l with
| nil => left _ _
| _ => right _ _
end
); unfold empty; trivial.
unfold not; intro H; discriminate H.
Defined.``````

The definition of `empty_dec`2 uses the refine tactic. It’s a powerful tactic that helps when it comes to dealing with specified types, such as `Sumbool`.

### Defining `empty_b`

With `empty_dec`, we can define `empty_b`.

``````  Definition empty_b (l:list):bool :=
if empty_dec l then true else false.``````

Let’s try to extract empty_b code:

``````type bool =
| True
| False

type sumbool =
| Left
| Right

type 'a list =
| Nil
| Cons of 'a * 'a list

(** val empty_dec : 'a1 list -> sumbool **)

let empty_dec = function
| Nil -> Left
| Cons (a, l0) -> Right

(** val empty_b : 'a1 list -> bool **)

let empty_b l =
match empty_dec l with
| Left -> True
| Right -> False``````

In addition to `list 'a`, Coq has created the `sumbool` and `bool` types and `empty_b` is basically a translation from the first to the second. We could have stopped with `empty_dec`, but `Left` and `Right` are less readable that `True` and `False`.

## Defining some utility functions

### Defining `pop`

There are several ways to write a function that removes the first element of a list. One is to return `nil` if the given list was already empty:

``````Definition pop (l:list) :=
match l with
| nil => nil
| cons a l => l
end.``````

But it’s not really satisfying. A `pop` call over an empty list should not be possible. It can be done by adding an argument to `pop`: the proof that the list is not empty.

``````Definition pop (l:list)(h:¬empty l): list.
induction l.
+ unfold not, empty in h. intuition. (* case (nil), absurd *)
+ exact l. (* case (cons a l) *)
Defined.``````

It’s better and yet it can still be improved. Indeed, according to its type, `pop` returns “some list”. As a matter of fact, `pop` returns “the same list without its first argument”. It is possible to write such precise definition thanks to sigma-types, defined as:

``````Inductive sig (A:Type) (P:A -> Prop) : Type :=
exist : forall x:A, P x -> sig P.``````

Rather that `sig A p`, sigma-types can be written using the notation `{ a | P }`. They express subsets. Thus, it is possible to write a strongly-specified version of `pop` that way:

``````Definition pop (l:list)(h:¬empty l): {l' | exists a, l = cons a l'}.
induction l.
+ unfold not, empty in h; intuition.
+ refine ( exist _ l _ ).
exists a.
trivial.
Defined.``````

`{l' | exists a, l = cons a l'}` expresses the condition “the same list without the first element”. The tactic `refine` is used to construct the result.

Let’s have a look at the extracted code:

``````(** val pop : 'a1 list -> 'a1 list **)

let pop = function
| Nil -> assert false (* absurd case *)
| Cons (a, l0) -> l0``````

If one tries to call `(pop nil)`, the `assert` ensures the call fails. Extra information given by the sigma-type have been stripped away. It can be confusing, but the implementation still respects the related property.

### Defining `push`

It is possible to specify `push` the same way `pop` has been. The only difference is `push` accepts lists with no restriction at all. Thus, its definition is a simpler, but it still uses `refine` to deal with the `exist` constructor.

``````Definition push (l:list) (a:A): {l' | l' = cons a l}.
refine (
exist _ (cons a l) _
); reflexivity.
Defined.``````

And the extracted code:

``````let push l a =
Cons (a, l)``````

### Defining `head`

Same as `pop` and `push`, it is possible to add extra information in the type of `head`. It’s not a surprise its definition is very close to `pop`.

``````Definition head (l:list)(h:¬empty l): { a | ∃ r, l = cons a r }.
induction l.
+ unfold not, empty in h; intuition.
+ refine ( exist _ a _ ).
exists l.
trivial.
Defined.``````

And the extracted code:

``````let head = function
| Nil -> assert false (* absurd case *)
| Cons (a, l0) -> a``````

## Let’s prove some theorems

`head`, `push` and `pop` are well-specified and the type alone gives enough information about what the function is doing. However, we might want to prove some generic list properties, just to be sure.

### `push` and `head`

For instance, given a list `l` and a `a`, the result of `head (push l a)` should always be `a`.

``````Theorem push_head_equal: ∀ l a,
match push l a with
| exist l' h => ∀ h',
match head l' h' with
| exist a' h'' => a = a'
end
end.
Proof.
intros; unfold push; intros; unfold head.
reflexivity.
Qed.``````

The use of sigma-type and proofs as argument makes the theorem a little hard to read, but the proof stays simple.

### `push` and `pop`

Our implementation of `push` and `pop` must guarantee that their composition is the identity function, that is `l = pop (push l)`.

``````Theorem push_pop_equal: ∀ l a,
match push l a with
| exist l' h => ∀ h',
(match pop l' h' with
| exist l'' h'' => l = l''
end)
end.
Proof.
intros.
unfold push.
intros.
unfold pop.
reflexivity.
Qed.``````

And if you want, here is a complete gist of the code.

1. I recommend Coq’Art. I myself read it (or at least much of it) and found it very clear.

2. We lack a decidable version of the equality between two lists, so we have to use a `match ... with` construction to deconstruct the list.