The Coq mailing list

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

Le mercredi 13 mars 2013 à 09:22 +0100, Arnaud Spiwack a écrit :

> I have written a number of functions using tactics that used abstract
> to opacify their proofy parts (whithout which they simply couldn't run
> in an efficient time). It's actually pretty common.

Speaking about common usage, I would be glad if the following construct
was not lost in the process. All of my reflection-based decision
procedures are based on the following idiom:

Ltac perform_reflection parameters :=
  abstract (
    refine (proof_by_reflection parameters _) ;
    vm_cast_no_check (refl_equal true).
  ).

The idea is that abstract forces a Qed at the time it is invoked. As a
consequence, when combined with _no_check tactics, it divides by two the
time taken by decision procedures while preserving full typecheck safety
and instant user feedback. (And I am not exaggerating, it is an actual
2x speedup with no impact on safety.)

Best regards,

Guillaume