Using eexists to construct record terms in Coq

Question

Suppose there is a denary relation R over some type A.

Variable A : Type.
Variable R : A -> A -> A -> A -> A -> A -> A -> A -> A -> A -> Prop.

X and Y are slightly different propositions which both assert that R holds over some 10 terms of type A.

Inductive X : Prop :=
| X_intro : forall a0 a1 a2 a3 a4 a5 a6 a7 a8 a9, 
R a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 -> X. 

Record Y : Prop :=
{ a0 : A; a1 : A; a2 : A; a3 : A; a4 : A;
  a5 : A; a6 : A; a7 : A; a8 : A; a9 : A;
  RY : R a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 }. 

Since X and Y assert the same things, it should be easy to prove X -> Y. We could, for instance, do it by explicitly constructing a proof of Y.

Theorem XY : X -> Y.
inversion 1. exists a0 a1 a2 a3 a4 
a5 a6 a7 a8 a9. apply H0. Qed.

But this seems unnecessary. The last proposition obtained by inversion on premise completely determines the 10 terms, so we shouldn't have to spell their names out. We could postpone their identification with eexists and unify them later.

Theorem XY' : X -> Y.
intro. eexists. inversion H. apply H0.

But unification fails here. This is what my goals look like before apply H0:

H0 : R a0 a1 a2 a3 a4 a5 a6 a7 a8 a9

======================== ( 1 / 1 )
R ?46 ?47 ?48 ?49 ?50 ?51 ?52 ?53 ?54 ?55

All arguments to R are undetermined, so it should be possible to unify ?46 with a0, ?47 with a1, and so on. Why does it fail?

Answer 1

The error message you get is something along the lines of:

unable to unify "?a0" with "a0" (cannot instantiate "?a0" because "a0" is not in its scope)

This is a fairly common error. Let me explain it with a simple example.

Let's start by defining an inductive data type that wraps a value of type A:

Variable A : Type.

Inductive Box :=
| elem : A -> Box.

Next, let's define a theorem about this data type which states that if you have a box, then there exists an element that is equal to the thing in the box:

Theorem boxOk (b:Box) : exists a, match b with elem a' => a = a' end.

We can try to prove this your way:

  eexists.
  destruct b.
  Fail reflexivity.
Restart.

But reflexivity fails, with the dreaded error message:

Unable to unify "?a" with "a" (cannot instantiate "?a" because "a" is not in its scope: available arguments are "elem a").

So what happens here? The term that these tactics construct looks like the following:

ex_intro _ ?a (match b with elem a => eq_refl end).

And you are now asking Coq to fill in ?a with a, which cannot work because a is not defined in the scope of ?a. The most common problem with this error is that eexists was called too early.

So instead, we should destruct first, and then call eexists. And it works:

  destruct b.
  eexists.
  reflexivity.
Qed.

The term that these tactics construct looks like the following:

match b with elem a => (ex_intro _ ?a eq_refl) end.

And now a is in ?a's scope and can easily be filled in.

In your example, you should do the following (which is actually what you did in your manual proof).

Theorem XY' : X -> Y.
  intro h. 
  inversion h as [? ? ? ? ? ? ? ? ? ? h'].
  eexists. 
  apply h'.
Qed.