Why is vm_compute faster in definitions than in proofs in Coq?

Question

I have a Fixpoint function f and a lemma of the following form:

Lemma L: forall x, f x = true -> P x.

When I define a variable a for which f a = true, I can prove P a in the following way:

Lemma: P a.
Proof. apply L. vm_compute. easy. Qed.

However, the evaluation of f is much faster (2mn versus 6mn) inside a definition:

Definition foo := Eval vm_compute in (f a).

Is there a reason for this difference, and is there a way to use it to prove P a faster?

PS: just in case, a is actually a long list of trees.

Answer 1

You might know that Coq's proof mode is just a wrapper to build proof terms interactively. During this process, Coq does some preliminary checking to rule out errors, but the real work happens when you hit Qed, which causes Coq to type check the resulting term. My guess is that f a is being computed twice: once for the preliminary checks, and then for the definitive checks.