The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

On 13 March 2013 10:35, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Wed, Mar 13, 2013 at 09:22:46AM +0100, Arnaud Spiwack wrote:
> 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).

Can you be more specific?  What goes wrong?  Is Qed too slow?  Were you
using types depending on proofs?  Do you consider your practice an hack
to work around an inefficiency?

Well the point is that I do

Definition f : T.
Proof.
  yada-yada. (* computational part of f. *)
  abstract tac. (* proof-part of f *)
Defined.

Then I use 'f' as a program. It's important that the proof parts are not evaluated. So I guess it's a hack in the same sense as the fact that opaqueness is a hack: to avoid evaluating proofs.

 

> I must say, I'm amazed it works.

Why shouldn't it work?  It is exactly what abstract does, but instead of
putting the abstracted term in the environment my code puts it in a
letin.  The type of the term is the same, its body is the same, the
typing rule used to typecheck its occurrences is the same (lookup in the
context/environment for a rel/name to find its type).
Am I missing something?

I just meant the interactive proof engine was really not made with this sort of transformation in mind. So it's kind of impressive that you were able to implement it.