## Verifying local definitions in Coq

Published 2018-04-22 in sections English, 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

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

1. 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`.
2. We do not give a type to `go`. We could, but that would again just be copying information that is already there.
3. We define go via an `ltac` expression: Instead of a term we give a tactic that calculates the term.
4. 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.)
5. 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 …`.
6. The `lazymatch` line matches `e` against the pattern `let x := ?def in _`, and binds the definition of `go` to the name `def`.
7. 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.
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.
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.