# Implementing Strongly-Specified Functions with the `refine`

Tactic

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 learn (I recommend the Coq'Art). 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 as an argument in which the first element has been
removed, for example.

## 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
`forall args, predicate args <-> bool_function args = true`

.

Another solution is to use the `sumbool`

type as middlemen. The
scheme is the following:

- Defining
`predicate : args → Prop`

- Defining
`predicate_dec : args -> { predicate args } + { ~predicate args }`

- 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 {a} (l : list a) : Prop := l = [].
```

### Defining a decidable version of `empty`

A decidable version of `empty`

is a function which takes a list
`l`

as its argument and returns either a proof that `l`

is empty,
or a proof that `l`

is not empty. This is encoded in the Coq
standard library with the `sumbool`

type, and is written as
follows: `{ empty l } + { ~ empty l }`

.

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

In this example, I decided to use the `refine`

tactic which is
convenient when we manipulate the `Set`

and `Prop`

sorts at the
same time.

### Defining `empty_b`

With `empty_dec`

, we can define `empty_b`

.

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

Let's try to extract `empty_b`

:

```
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 `'a list`

, Coq has created the `sumbool`

and
`bool`

types and `empty_b`

is basically a translation from the
former to the latter. We could have stopped with `empty_dec`

, but
`Left`

and `Right`

are less readable that `True`

and
`False`

. Note that it is possible to configure the Extraction mechanism
to use primitive OCaml types instead, but this is out of the scope of this
article.

## 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 {a} ( l :list a) :=
match l with
| _ :: 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 {a} (l : list a) (h : ~ empty l)
: list a.
```

There are, as usual when it comes to lists, two cases to consider.

`l = x :: rst`

, and therefore`pop (x :: rst) h`

is`rst`

`l = []`

, which is not possible since we know`l`

is not empty.

The challenge is to convince Coq that our reasoning is
correct. There are, again, several approaches to achieve that. We
can, for instance, use the `refine`

tactic again, but this time we
need to know a small trick to succeed as using a “regular” `match`

will not work.

From the following goal:

```
a : Type
l : list a
h : ~ empty l
============================
list a
```

Using the `refine`

tactic naively, for instance, this way:

```
refine (match l with
| _ :: rst => rst
| [] => _
end).
```

leaves us the following goal to prove:

```
a : Type
l : list a
h : ~ empty l
============================
list a
```

Nothing has changed! Well, not exactly. See, `refine`

has taken
our incomplete Gallina term, found a hole, done some
type-checking, found that the type of the missing piece of our
implementation is `list a`

and therefore has generated a new
goal of this type. What `refine`

has not done, however, is
remembering that we are in the case where `l = []`

.

We need to generate a goal from a hole wherein this information is
available. It is possible to use a long form of `match`

. The
general approach is this: rather than returning a value of type
`list a`

, our match will return a function of type `l = ?l' -> list a`

, where `?l`

is a value of `l`

for a given case (that is,
either `x :: rst`

or `[]`

). Of course and as a consequence, the type
of the `match`

in now a function which awaits a proof to return
the expected result. Fortunately, this proof is trivial: it is
`eq_refl`

.

```
refine (match l as l'
return l = l' -> list a
with
| _ :: rst => fun _ => rst
| [] => fun equ => _
end eq_refl).
```

For us to conclude the proof, this is way better.

```
a : Type
l : list a
h : ~ empty l
equ : l = []
============================
list a
```

We conclude the proof, and therefore the definition of `pop`

.

```
rewrite equ in h.
exfalso.
now apply h.
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 than `sig A p`

, sigma-types can be written using the
notation `{ a | P }`

. They express subsets, and can be used to constraint
arguments and results of functions.

We finally propose a strongly specified definition of `pop`

.

```
Definition pop {a} (l : list a | ~ empty l)
: { l' | exists a, proj1_sig l = cons a l' }.
```

If you think the previous use of `match`

term was ugly, brace yourselves.

```
refine (match proj1_sig l as l'
return proj1_sig l = l'
-> { l' | exists a, proj1_sig l = cons a l' }
with
| [] => fun equ => _
| (_ :: rst) => fun equ => exist _ rst _
end eq_refl).
```

This leaves us two goals to tackle.

First, we need to discard the case where `l`

is the empty list.

```
a : Type
l : {l : list a | ~ empty l}
equ : proj1_sig l = []
============================
{l' : list a | exists a0 : a, proj1_sig l = a0 :: l'}
```

```
+ destruct l as [l nempty]; cbn in *.
rewrite equ in nempty.
exfalso.
now apply nempty.
```

Then, we need to prove that the result we provide (`rst`

) when the
list is not empty is correct with respect to the specification of
`pop`

.

```
a : Type
l : {l : list a | ~ empty l}
a0 : a
rst : list a
equ : proj1_sig l = a0 :: rst
============================
exists a1 : a, proj1_sig l = a1 :: rst
```

```
+ destruct l as [l nempty]; cbn in *.
rewrite equ.
now exists a0.
Defined.
```

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 has been stripped away. It can be
confusing, and in practice it means that, we you rely on the extraction
mechanism to provide a certified OCaml module, you *cannot expose
strongly specified functions in its public interface* because nothing in the
OCaml type system will prevent a misuse which will in practice leads to an
`assert false`

. *)

## 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, and we can write it without `refine`

.

```
Definition push {a} (l : list a) (x : a)
: { l' | l' = x :: l } :=
exist _ (x :: l) eq_refl.
```

And the extracted code is just as straightforward.

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

, namely the returned value of `head`

is indeed the first value
of `l`

.

```
Definition head {a} (l : list a | ~ empty l)
: { x | exists r, proj1_sig l = x :: r }.
```

It's not a surprise its definition is very close to `pop`

.

```
refine (match proj1_sig l as l'
return proj1_sig l = l' -> _
with
| [] => fun equ => _
| x :: _ => fun equ => exist _ x _
end eq_refl).
```

The proof is also very similar, and are left to read as an exercise for passionate readers.

```
+ destruct l as [l falso]; cbn in *.
rewrite equ in falso.
exfalso.
now apply falso.
+ exists l0.
now rewrite equ.
Defined.
```

Finally, the extracted code is as straightforward as it can get.

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

## Conclusion

Writing strongly specified functions allows for reasoning about the result
correctness while computing it. This can help in practice. However, writing
these functions with the `refine`

tactic does not enable a very idiomatic
Coq code.

To improve the situation, the `Program`

framework distributed with the
Coq standard library helps, but it is better to understand what `Program`

achieves under its hood, which is basically what we have done in this article.