The Coq mailing list

[Mathieu Boespflug <mboes AT tweag.net>]

In Ssreflect they define the "nosimpl" notation for this purpose.

From the Ssreflect manual (http://hal.inria.fr/inria-00258384/, page 51):

"Notation "’nosimpl’ t" := (let: tt := tt in t).

The term (nosimpl t) simplifies to t except in a definition. More
precisely, given:

  Definition foo := (nosimpl bar).

the term foo (or (foo t’)) will not be expanded by the simpl tactic
unless it is in a
forcing context (e.g., in match foo t’ with ... end, foo t’ will be
reduced if this allows
match to be reduced). Note that nosimpl bar is simply notation for a
term that reduces to
bar; hence unfold foo will replace foo by bar, and fold foo will
replace bar by foo.

Hope this helps,

Mathieu


On Tue, Oct 26, 2010 at 2:17 PM, Alexandre Pilkiewicz
<alexandre.pilkiewicz AT polytechnique.org>
 wrote:
> Hi Adam
>
> 2010/10/26 Adam Chlipala 
> <adam AT chlipala.net>:
>>
>> The only way I've found to do this is to put the definition inside a module
>> with opaque signature ascription.
>
> I don't really see the difference with Opaque.
>
>>  You can also export from the module a
>> theorem giving the equation defining the identifier; then, in cases where
>> you do want reduction, you have to rewrite with that equality, rather than
>> relying on the definitional equality.
>
> That's what I'm doing, yes.
>
> Then I tried a couple of "clever" things to simplify this usage :
>
> First I wanted to name those renaming lemma myconst_unfold, and have a 
> tactic
>
> Ltac unfold' X :=
>  let H = concat X "_unfold" in
>  rewrite H.
> where concat would be a tactic that concatenate names like fresh does,
> but without the freshning. But it seems it does not exists.
>
> Then I just wanted to put the rewriting lemma in a Rewrite base:
>
> Hint Rewrite myconst_unfold: myconst.
>
> and have
>
> Ltac unfold' X := autorewrite with X.
>
> but then I encountered what seems to be a bug of ltac (
> http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2417 ;)
>
> I will continue with just rewrite.
>
> Thanks anyway!
>
> Alexandre
>
>