The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

Hi,

 

The following is the tactic I developed for the same purpose.

 

==================================================

 

Definition _Evar_Gil_ (A:Type) (x:A) := x.

Tactic Notation "hide_evar" int_or_var(n) := let QQ := fresh "QQ" in
  hget_evar n; intro;
  lazymatch goal with [ H := ?X |- _] =>
    set (QQ := X) in *; fold (@_Evar_Gil_ _ X) in QQ; clear H
  end.

Ltac hide_evars := repeat (hide_evar 1).

Ltac show_evars :=
  repeat (match goal with [ H := @_Evar_Gil_ _ _ |- _ ] =>
    unfold _Evar_Gil_ in H; unfold H in *; clear H end).

==================================================

 

You can use it as follows.

 

===========================

(* Example *)

Goal exists n, n = 0.
eexists.

hide_evars.

do something such as vm_compute

show_evars.

 

the rest of the proof.

Qed.
===========================

 

This might help, or maybe have the same problem.

 

Best,

Gil

 

 

On Thu, Jan 24, 2013 at 6:38 PM, Thomas Braibant <thomas.braibant AT gmail.com> wrote:

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)