The Coq mailing list

[Thomas Dinsdale-Young <td202 AT doc.ic.ac.uk>]

It's a bit of a hack, but something like the opaque tactic you describe 
may be implemented in Ltac as:

Ltac opaque_in id t := let y := fresh in let H := fresh in
    (* introduce y for id *)
  set (y := id); assert (H: y = id) by reflexivity;
    (* forget about the definition of y *)
  generalize dependent y; intros y H;
    (* do t *)
  t;
    (* substitute back y *)
  rewrite H in *; clear y H.

Something like "opaque_in x simpl" would prevent simpl from seeing the 
definition of x by substituting it for y.

In a related note, I'd quite like to see a tactic along the lines of 
"hide H in t" which runs tactic t without letting it make use of 
hypothesis H (and any hypotheses in which H occurs, providing H does not 
occur in the goal).

-- Thomas


On 24/02/2012 21:29, Francois Pottier wrote:
> Dear all,
>
> I find that, in some cases, it is necessary (or at least useful) to use the
> commands Opaque and Transparent in order to control the amount of
> simplification performed by the tactic "simpl". If "simpl" is too
> aggressive, making certain definitions opaque helps.
>
> This technique could be really useful if Opaque and Transparent were
> tactics, as opposed to commands. This would allow them to be used as
> building blocks in the construction of more complex tactics.
>
> Have the Coq implementors given some thought to this idea? One might
> imagine extending Ltac with tactics of the form "opaque foo in t" and
> "transparent foo in t", where "t" is a tactic and "foo" is an identifier.
> This would have the effect of changing the status of "foo" while "t" is
> executed, and restoring it upon exit.