The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi list,

I think it is folklore that vm_compute cannot handle terms that
contains existential variables (evars), and that it is not possible to
forbid it to unfold some terms (e.g., it does not respect opacity, and
using tricks like modules is unpractical).

I realized during the last week that it is in fact possible to get
around both limitations...

The idea is that when you have a term [T] that contains evars, it is
possible to transform [T] into a function [F] in which evars have been
abstracted, applied to these evars; and then compute in the head term
[F]. For instance,  if [T] is [f ?1 ?2], it can be transformed into
[(fun a b => f a b) ?1 ?2]; then one uses vm_compute to compute the
normal form of [fun a b => f a b], and then reduce the beta redexes
that we introduced.

The same strategy applies to abstract over a "black list" of constants.

For instance, black listing [plus] in the following goal
\[
5 * 4 + ?3
\]

reduces to
\[
20 + ?3
\]

(Note that the instances of [plus] that appears during the reductions
have been unfolded.)

I have implemented a prototype tactic that implements the ideas above
(a wrapper around vm_compute) using a plugin available here [1].
Comments are welcome.

A note: I tried to use tactics (as seen from OCaml) to build this
plugin, but it was not that efficient. It turned out that to  make the
tactic fast, I had to build a proof term by hand. I wonder if we could
get a  performance improvement by reimplementing tactics that stacks
more "primitive" tactics using such "bare" proof term manipulations...
(ALso, I believe that it is not possible to implement this tactic in
LTac.)

Thomas
[1] https://github.com/braibant/evm_compute (working with coq 8.4 pl1)