# Joachim Breitner's Homepage

## Verifying local definitions in Coq

TL;DR: We can give top-level names to local definitions, so that we can state and prove stuff about them without having to rewrite the programs.

### When a Haskeller writes Coq

Imagine you teach Coq to a Haskell programmer, and give them the task of pairing each element in a list with its index. The Haskell programmer might have

```
addIndex :: [a] -> [(Integer, a)]
addIndex xs = go 0 xs
where go n [] = []
go n (x:xs) = (n,x) : go (n+1) xs
```

in mind and write this Gallina function (Gallina is the programming language of Coq):

```
Require Import Coq.Lists.List.
Import ListNotations.
Definition addIndex {a} (xs : list a) : list (nat * a) :=
let fix go n xs := match xs with
| [] => []
| x::xs => (n, x) :: go (S n) xs
end
in go 0 xs.
```

Alternatively, imagine you are using `hs-to-coq`

to mechanically convert the Haskell definition into Coq.

### When a Coq user tries to verify that

Now your task is to prove something about this function, for example

```
Theorem addIndex_spec:
forall {a} n (xs : list a),
nth n (map fst (addIndex xs)) n = n.
```

If you just have learned Coq, you will think “I can do this, this surely holds by induction on `xs`

.” But if you have a bit more experience, you will already see a problem with this (if you do not see the problem yet, I encourage you to stop reading, copy the few lines above, and try to prove it).

The problem is that – as so often – you have to generalize the statement for the induction to go through. The theorem as stated says something about `addIndex`

or, in other words, about `go 0`

. But in the inductive case, you will need some information about `go 1`

. In fact, you need a lemma like this:

```
Lemma go_spec:
forall {a} n m k (xs : list a), k = n + m ->
nth n (map fst (go m xs)) k = k.
```

But `go`

is not a (top-level) function! How can we fix that?

- We can try to awkwardly work-around not having a name for
`go`

in our proofs, and essentially prove`go_spec`

inside the proof of`addIndex_spec`

. Might work in this small case, but does not scale up to larger proofs. - We can ask the programmer to avoid using local functions, and first define
`go`

as a top-level fixed point. But maybe we don’t want to bother them because of that. (Or, more likely, we are using`hs-to-coq`

and that tool stubbornly tries to make the output as similar to the given Haskell code as possible.) - We can copy’n’paste the definition of
`go`

and make a separate, after-the-fact top-level definition. But this is not nice from a maintenance point of view: If the code changes, we have to update this copy. - Or we apply this one weird trick...

### The weird trick

We can define `go`

after-the-fact, but instead of copy’n’pasting the definition, we can use Coq’s tactics to define it. Here it goes:

```
Definition go {a} := ltac:(
let e := eval cbv beta delta [addIndex] in (@addIndex a []) in
(* idtac e; *)
lazymatch e with | let x := ?def in _ =>
exact def
end).
```

Let us take it apart:

- We define
`go`

, and give the parameters that`go`

depends upon. Note that of the two parameters of`addIndex`

, the definition of`go`

only depends on (“captures”)`a`

, but not`xs`

. - We do
*not*give a type to`go`

. We could, but that would again just be copying information that is already there. - We define go via an
`ltac`

expression: Instead of a term we give a tactic that calculates the term. - This tactic first binds
`e`

to the body of`addIndex`

. To do so, it needs to pass enough arguments to`addIndex`

. The concrete value of the list argument does not matter, so we pass`[]`

. The term`@addIndex a []`

is now evaluated with the evaluation flags`eval cbv beta delta [addIndex]`

, which says “unfold`addIndex`

and do beta reduction, but nothing else”. In particularly, we do not do`zeta`

reduction, which would reduce the`let go := …`

definition. (The user manual very briefly describes these flags.) - The
`idtac e`

line can be used to peek at`e`

, for example when the next tactic fails. We can use this to check that`e`

really is of the form`let fix go := … in …`

. - The
`lazymatch`

line matches`e`

against the pattern`let x := ?def in _`

, and binds the definition of`go`

to the name`def`

. - And the
`exact def`

tactic tells Coq to use`def`

as the definition of`go`

.

We now have defined `go`

, of type `go : forall {a}, nat -> list a -> list (nat * a)`

, and can state and prove the auxiliary lemma:

```
Lemma go_spec:
forall {a} n m k (xs : list a), k = n + m ->
nth n (map fst (go m xs)) k = k.
Proof.
intros ?????.
revert n m k.
induction xs; intros; destruct n; subst; simpl.
1-3:reflexivity.
apply IHxs; lia.
Qed.
```

When we come to the theorem about `addIndex`

, we can play a little trick with `fold`

to make the proof goal pretty:

```
Theorem addIndex_spec:
forall {a} n (xs : list a),
nth n (map fst (addIndex xs)) n = n.
Proof.
intros.
unfold addIndex.
fold (@go a).
(* goal here: nth n (map fst (go 0 xs)) n = n *)
apply go_spec; lia.
Qed.
```

### Multiple local definitions

The trick extends to multiple local definitions, but needs some extra considerations to ensure that terms are closed. A bit contrived, but let us assume that we have this function definition:

```
Definition addIndex' {a} (xs : list a) : list (nat * a) :=
let inc := length xs in
let fix go n xs := match xs with
| [] => []
| x::xs => (n, x) :: go (inc + n) xs
end in
go 0 xs.
```

We now want to give names to `inc`

*and* to `go`

. I like to use a section to collect the common parameters, but that is not essential here. The trick above works flawlessly for `inc':

```
Section addIndex'.
Context {a} (xs : list a).
Definition inc := ltac:(
let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
lazymatch e with | let x := ?def in _ =>
exact def
end).
```

But if we try it for `go'`

, like such:

```
Definition go' := ltac:(
let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
lazymatch e with | let x := _ in let y := ?def in _ =>
exact def
end).
```

we get “Ltac variable def depends on pattern variable name x which is not bound in current context”. To fix this, we use higher-order pattern matchin (`@?def`

) to substitute “our” `inc`

for the local `inc`

:

```
Definition go' := ltac:(
let e := eval cbv beta delta [addIndex'] in (@addIndex' a xs) in
lazymatch e with | let x := _ in let y := @?def x in _ =>
let def' := eval cbv beta in (def inc) in
exact def'
end).
```

instead. We have now defined both `inc`

and `go'`

and can use them in proofs about `addIndex'`

:

```
Theorem addIndex_spec':
forall n, nth n (map fst (addIndex' xs)) n = n * length xs.
Proof.
intros.
unfold addIndex'.
fold inc go'. (* order matters! *)
(* goal here: nth n (map fst (go' 0 xs)) n = n * inc *)
```

### Reaching into a match

This trick also works when the local definition we care about is inside a match statement. Consider:

```
Definition addIndex_weird {a} (oxs : option (list a))
:= match oxs with
| None => []
| Some xs =>
let fix go n xs := match xs with
| [] => []
| x::xs => (n, x) :: go (S n) xs
end in
go 0 xs
end.
Definition go_weird {a} := ltac:(
let e := eval cbv beta match delta [addIndex_weird]
in (@addIndex_weird a (Some [])) in
idtac e;
lazymatch e with | let x := ?def in _ =>
exact def
end).
```

Note the addition of `match`

to the list of evaluation flags passed to `cbv`

.

### Conclusion

While local definitions are idiomatic in Haskell (in particular thanks to the `where`

syntax), they are usually avoided in Coq, because they get in the way of verification. If, for some reason, one is stuck with such definitions, then this trick presents a reasonable way out.

Have something to say? You can post a comment by sending an e-Mail to me at <mail@joachim-breitner.de>, and I will include it here.