The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 25/04/2017 08:55, Pierre Casteran wrote:
> Hi,
> 
>   I wrote a small proof on fast growing functions (Wainer's hierarchy).
> 
>   The statement is F_3 (2) > F_omega (2). The proof term is not so big,
> but it contains several occurrences of (f_2 23), which is known as
> greater than 2^23.
> 
>   The problem may come from the fact that all these subterms are
> computed after Qed, thus I had to interrupt after some time. Is there an
> option for preventing Coq to expand function calls ?

As Laurent said, the kernel should not compute if computing is not
needed. The hard part is to convince the kernel that it is indeed not
needed. Usually, generalizing or abstracting tend to give enough
information to the kernel to avoid useless computations.

Here is a small example. Suppose you want to prove (fact 100 = 100 *
fact 99). There is a trivial proof term, which is (eq_refl 100 : fact
100 = fact 100). Unfortunately, when comparing the right-hand sides, the
kernel decides to reduce (fact 99) instead of (fact 100), which causes
the verification to run forever. To avoid this issue, just generalize
away 99. This gives a needlessly complicated proof term but at least the
kernel now checks it instantly.

Goal fact 100 = 100 * fact 99.
Proof.
  assert (exists i, i = 99) as [i <-] by now eexists.
  reflexivity.
Qed.

Best regards,

Guillaume