The Coq mailing list

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

On 27/06/2015 09:52, Chris Dams wrote:
> Dear all,
>
> I was doing a proof where I used
>
> destruct (Nlt_ge_dec (i + j) (2 ^ 32)) as a tactic.
>
> At this point it is clear why the Qed never finishes.

No, it is not that clear. The kernel does not normalize a proof term 
when checking it at Qed, unless you explicitly asked for it through a 
tactic such as vm_compute. Otherwise the following script would never go 
through:

Goal fact 99 * 100 = 100 * fact 99.
Proof. apply mult_comm. Qed. (* OK *)

But whether the kernel unfolds a definition or not is a heuristic 
unfortunately. And it might happen that the kernel always unfolds the 
worst definition, thus ending up normalizing the proof term.

Goal fact 99 * 100 = fact 100.
Proof. exact_no_check (mult_comm (fact 99) 100). Qed. (* Fail *)

Here, for some reason, the kernel thought that unfolding mult was making 
more sense then unfolding fact. So, in addition to the solution you 
already suggested, you can also help the kernel deciding which 
definitions should be unfolded first.

Strategy 1 [ mult ]. (* set mult at priority 1, so that it has a lower 
priority than fact, which is at priority 0 by default *)

Goal fact 99 * 100 = fact 100.
Proof. exact_no_check (mult_comm (fact 99) 100). Qed. (* OK *)

Best regards,

Guillaume