Почему vm_compute быстрее в определениях, чем в доказательствах в Coq?

Question

У меня есть Fixpoint функция f и лемма следующего вида:

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

Когда я определяю переменную a, для которой f a = true, я могу доказать P aследующим образом:

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

Однако оценка f намного быстрее (2мн против 6мн) внутри определения:

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

Есть ли причина для такой разницы, и есть ли способ использовать его, чтобы доказать P a быстрее?

PS: на всякий случай, a на самом деле длинный список деревьев.

Answer 1

Возможно, вы знаете, что режим проверки Coq - это просто оболочка для интерактивного создания терминов проверки. Во время этого процесса Coq выполняет некоторую предварительную проверку, чтобы исключить ошибки, но настоящая работа происходит, когда вы нажимаете Qed, что заставляет Coq проверять тип полученного термина. Я предполагаю, что f a вычисляется дважды : один раз для предварительных проверок, а затем для окончательных проверок.