# Joachim Breitner's Homepage

## Proof reuse in Coq using existential variables

This is another technical post that is only of interest only to Coq users.

TL;DR: Using existential variable for hypotheses allows you to easily refactor a complicated proof into an induction schema and the actual proofs.

### Setup

As a running example, I will use a small theory of “bags”, which you can think of as lists represented as trees, to allow an *O*(1) append operation:

```
Require Import Coq.Arith.Arith.
Require Import Psatz.
Require FunInd.
(* The data type *)
Inductive Bag a : Type :=
| Empty : Bag a
| Unit : a -> Bag a
| Two : Bag a -> Bag a -> Bag a.
Arguments Empty {_}.
Arguments Unit {_}.
Arguments Two {_}.
Fixpoint length {a} (b : Bag a) : nat :=
match b with
| Empty => 0
| Unit _ => 1
| Two b1 b2 => length b1 + length b2
end.
(* A smart constructor that ensures that a [Two] never
has [Empty] as subtrees. *)
Definition two {a} (b1 b2 : Bag a) : Bag a := match b1 with
| Empty => b2
| _ => match b2 with | Empty => b1
| _ => Two b1 b2 end end.
Lemma length_two {a} (b1 b2 : Bag a) :
length (two b1 b2) = length b1 + length b2.
Proof. destruct b1, b2; simpl; lia. Qed.
(* A first non-trivial function *)
Function take {a : Type} (n : nat) (b : Bag a) : Bag a :=
if n =? 0
then Empty
else match b with
| Empty => b
| Unit x => b
| Two b1 b2 => two (take n b1) (take (n - length b1) b2)
end.
```

### The theorem

The theorem that I will be looking at in this proof describes how `length`

and `take`

interact:

```
Theorem length_take''':
forall {a} n (b : Bag a),
length (take n b) = min n (length b).
```

Before I dive into it, let me point out that this example itself is too simple to warrant the techniques that I will present in this post. I have to rely on your imagination to scale this up to appreciate the effect on significantly bigger proofs.

### Naive induction

How would we go about proving this lemma? Surely, `induction`

is the way to go! And indeed, this is provable using induction (on the `Bag`

) just fine:

```
Proof.
intros.
revert n.
induction b; intros n.
* simpl.
destruct (Nat.eqb_spec n 0).
+ subst. rewrite Nat.min_0_l. reflexivity.
+ rewrite Nat.min_0_r. reflexivity.
* simpl.
destruct (Nat.eqb_spec n 0).
+ subst. rewrite Nat.min_0_l. reflexivity.
+ simpl. lia.
* simpl.
destruct (Nat.eqb_spec n 0).
+ subst. rewrite Nat.min_0_l. reflexivity.
+ simpl. rewrite length_two, IHb1, IHb2. lia.
Qed.
```

But there is a problem: A proof by induction on the `Bag`

argument immediately creates three subgoals, one for each constructor. But that is not how `take`

is defined, which *first* checks the value of `n`

, independent of the constructor. This means that we have to do the case-split and the proof for the case `n = 0`

three times, although they are identical. It’s a one-line proof here, but imagine something bigger…

### Proof by fixpoint

Can we refactor the proof to handle the case `n = 0`

first? Yes, but not with a simple invocation of the `induction`

tactic. We could do well-founded induction on the `length`

of the argument, or we can do the proof using the more primitive `fix`

tactic. The latter is a bit hairy, you won’t know if your proof is accepted until you do `Qed`

(or check with `Guarded`

), but when it works it can yield some nice proofs.

```
Proof.
intros a.
fix IH 2.
intros.
rewrite take_equation.
destruct (Nat.eqb_spec n 0).
+ subst n. rewrite Nat.min_0_l. reflexivity.
+ destruct b.
* rewrite Nat.min_0_r. reflexivity.
* simpl. lia.
* simpl. rewrite length_two, !IH. lia.
Qed.
```

Nice: we eliminated the duplication of proofs!

### A functional induction lemma

Again, imagine that we jumped through more hoops here … maybe some well-founded recursion with a tricky size measure and complex proofs that the measure decreases … or maybe you need to carry around an invariant about your arguments and you have to work hard to satisfy the assumption of the induction hypothesis.

As long as you do only one proof about `take`

, that is fine. As soon as you do a second proof, you will notice that you have to repeat all of that, and it can easily make up most of your proof…

Wouldn’t it be nice if you can do the common parts of the proofs only once, obtain a generic proof scheme that you can use for (most) proofs about `take`

, and then just fill in the blanks?

Incidentally, the `Function`

command provides precisely that:

```
take_ind
: forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
(forall (n : nat) (b : Bag a), (n =? 0) = true -> P n b Empty) ->
(forall (n : nat) (b : Bag a), (n =? 0) = false -> b = Empty -> P n Empty b) ->
(forall (n : nat) (b : Bag a), (n =? 0) = false -> forall x : a, b = Unit x -> P n (Unit x) b) ->
(forall (n : nat) (b : Bag a),
(n =? 0) = false ->
forall b1 b2 : Bag a,
b = Two b1 b2 ->
P n b1 (take n b1) ->
P (n - length b1) b2 (take (n - length b1) b2) ->
P n (Two b1 b2) (two (take n b1) (take (n - length b1) b2))) ->
forall (n : nat) (b : Bag a), P n b (take n b)
```

which is great if you can use `Function`

(although not perfect – we’d rather see `n = 0`

instead of `(n =? 0) = true`

), but often `Function`

is not powerful enough to define the function you care about.

### Extracting the scheme from a proof

We could define our own `take_ind'`

by hand, but that is a lot of work, and we may not get it right easily, and when we change out functions, there is now this big proof statement to update.

Instead, let us use existentials, which are variables where Coq infers their type from how we use them, so we don’t have to declare them. Unfortunately, Coq does not support writing just

```
Lemma take_ind':
forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
forall (IH1 : ?) (IH2 : ?) (IH3 : ?) (IH4 : ?),
forall n b, P n b (take n b).
```

where we just leave out the type of the assumptions (Isabelle does…), but we can fake it using some generic technique.

We begin with stating an auxiliary lemma using a sigma type to say “there exist some assumption that are sufficient to show the conclusion”:

```
Lemma take_ind_aux:
forall a (P : _ -> _ -> _ -> Prop),
{ Hs : Prop |
Hs -> forall n (b : Bag a), P n b (take n b)
}.
```

We use the `eexist`

tactic (existential `exists`

) to construct the sigma type without committing to the type of `Hs`

yet.

```
Proof.
intros a P.
eexists.
intros Hs.
```

This gives us an assumption `Hs : ?Hs`

– note the existential type. We need four of those, which we can achieve by writing

```
pose proof Hs as H1. eapply proj1 in H1. eapply proj2 in Hs.
pose proof Hs as H2. eapply proj1 in H2. eapply proj2 in Hs.
pose proof Hs as H3. eapply proj1 in H3. eapply proj2 in Hs.
rename Hs into H4.
```

we now have this goal state:

```
1 subgoal
a : Type
P : nat -> Bag a -> Bag a -> Prop
H4 : ?Goal2
H1 : ?Goal
H2 : ?Goal0
H3 : ?Goal1
______________________________________(1/1)
forall (n : nat) (b : Bag a), P n b (take n b)
```

At this point, we start reproducing the proof of `length_take`

: The same approach to induction, the same case splits:

```
fix IH 2.
intros.
rewrite take_equation.
destruct (Nat.eqb_spec n 0).
+ subst n.
revert b.
refine H1.
+ rename n0 into Hnot_null.
destruct b.
* revert n Hnot_null.
refine H2.
* rename a0 into x.
revert x n Hnot_null.
refine H3.
* assert (IHb1 : P n b1 (take n b1)) by apply IH.
assert (IHb2 : P (n - length b1) b2 (take (n - length b1) b2)) by apply IH.
revert n b1 b2 Hnot_null IHb1 IHb2.
refine H4.
Defined. (* Important *)
```

Inside each case, we move all relevant hypotheses into the goal using `revert`

and `refine`

with the corresponding assumption, thus instantiating it. In the recursive case (`Two`

), we assert that `P`

holds for the subterms, by induction.

It is important to end this proofs with `Defined`

, and not `Qed`

, as we will see later.

In a next step, we can remove the sigma type:

`Definition take_ind' a P := proj2_sig (take_ind_aux a P).`

The type of `take_ind'`

is as follows:

```
take_ind'
: forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
proj1_sig (take_ind_aux a P) ->
forall n b, P n b (take n b)
```

This looks almost like an induction lemma. The assumptions of this lemma have the not very helpful type `proj1_sig (take_ind_aux a P)`

, but we can already use this to prove `length_take`

:

```
Theorem length_take:
forall {a} n (b : Bag a),
length (take n b) = min n (length b).
Proof.
intros a.
intros.
apply take_ind' with (P := fun n b r => length r = min n (length b)).
repeat apply conj; intros.
* rewrite Nat.min_0_l. reflexivity.
* rewrite Nat.min_0_r. reflexivity.
* simpl. lia.
* simpl. rewrite length_two, IHb1, IHb2. lia.
Qed.
```

In this case I have to explicitly state `P`

where I invoke `take_ind'`

, because Coq cannot figure out this instantiation on its own (it requires higher-order unification, which is undecidable and unpredictable). In other cases I had more luck.

After I `apply take_ind'`

, I have this proof goal:

```
______________________________________(1/1)
proj1_sig (take_ind_aux a (fun n b r => length r = min n (length b)))
```

which is the type that Coq inferred for `Hs`

above. We know that this is a conjunction of a bunch of assumptions, and we can split it as such, using `repeat apply conj`

. At this point, Coq needs to look inside `take_ind_aux`

; this would fail if we used `Qed`

to conclude the proof of `take_ind_aux`

.

This gives me four goals, one for each case of `take`

, and the remaining proofs really only deals with the specifics of `length_take`

– no more general dealing with worrying about getting the induction right and doing the case-splitting the right way.

Also note that, very conveniently, Coq uses the same name for the induction hypotheses `IHb1`

and `IHb2`

that we used in `take_ind_aux`

!

### Making it prettier

It may be a bit confusing to have this `proj1_sig`

in the type, especially when working in a team where others will use your induction lemma without knowing its internals. But we can resolve that, and also turn the conjunctions into normal arrows, using a bit of tactic support. This is completely generic, so if you follow this procedure, you can just copy most of that:

```
Lemma uncurry_and: forall {A B C}, (A /\ B -> C) -> (A -> B -> C).
Proof. intros. intuition. Qed.
Lemma under_imp: forall {A B C}, (B -> C) -> (A -> B) -> (A -> C).
Proof. intros. intuition. Qed.
Ltac iterate n f x := lazymatch n with
| 0 => x
| S ?n => iterate n f uconstr:(f x)
end.
Ltac uncurryN n x :=
let n' := eval compute in n in
lazymatch n' with
| 0 => x
| S ?n => let uc := iterate n uconstr:(under_imp) uconstr:(uncurry_and) in
let x' := uncurryN n x in
uconstr:(uc x')
end.
```

With this in place, we can define our final proof scheme lemma:

```
Definition take_ind'' a P
:= ltac:(let x := uncurryN 3 (proj2_sig (take_ind_aux a P)) in exact x).
Opaque take_ind''.
```

The type of `take_ind''`

is now exactly what we’d wish for: All assumptions spelled out, and the `n =? 0`

already taken of (compare this to the `take_ind`

provided by the `Function`

command above):

```
take_ind''
: forall (a : Type) (P : nat -> Bag a -> Bag a -> Prop),
(forall b : Bag a, P 0 b Empty) ->
(forall n : nat, n <> 0 -> P n Empty Empty) ->
(forall (x : a) (n : nat), n <> 0 -> P n (Unit x) (Unit x)) ->
(forall (n : nat) (b1 b2 : Bag a),
n <> 0 ->
P n b1 (take n b1) ->
P (n - length b1) b2 (take (n - length b1) b2) ->
P n (Two b1 b2) (two (take n b1) (take (n - length b1) b2))) ->
forall (n : nat) (b : Bag a), P n b (take n b)
```

At this point we can mark `take_ind''`

as `Opaque`

, to hide how we obtained this lemma.

Our proof does not change a lot; we merely no longer have to use `repeat apply conj`

:

```
Theorem length_take''':
forall {a} n (b : Bag a),
length (take n b) = min n (length b).
Proof.
intros a.
intros.
apply take_ind'' with (P := fun n b r => length r = min n (length b)); intros.
* rewrite Nat.min_0_l. reflexivity.
* rewrite Nat.min_0_r. reflexivity.
* simpl. lia.
* simpl. rewrite length_two, IHb1, IHb2. lia.
Qed.
```

### Is it worth it?

It was in my case: Applying this trick in our ongoing work of verifying parts of the Haskell compiler GHC separated a somewhat proof into a re-usable proof scheme (`go_ind`

), making the actual proofs (`go_all_WellScopedFloats`

, `go_res_WellScoped`

) much neater and to the point. It saved “only” 60 lines (if I don’t count the 20 “generic” lines above), but the pay-off will increase as I do even more proofs about this function.

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.