coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Mathieu Boespflug <mboes AT tweag.net>
- To: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
- Cc: Adam Chlipala <adam AT chlipala.net>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Avoiding some unfold with simpl
- Date: Tue, 26 Oct 2010 14:27:38 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=tVhKsryYjEUhhCpBjyP5IV6E8JGNGF+9p1Oz0cIjgyKlPha+LdihqL8CTFoyLjmsWI lFv5lNsFOYAt8XVYFrfiRaPWSJBivjzLpWsTSL7ToWdrcyF/JPwHQa0aNN8qSHyXLwwE h60DNQXy1vSQtCLsqQEtFtYHvZ4hpmI4ki7CE=
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
>
>
- [Coq-Club] Avoiding some unfold with simpl, Alexandre Pilkiewicz
- Re: [Coq-Club] Avoiding some unfold with simpl,
Adam Chlipala
- Re: [Coq-Club] Avoiding some unfold with simpl,
Alexandre Pilkiewicz
- Re: [Coq-Club] Avoiding some unfold with simpl, Mathieu Boespflug
- Re: [Coq-Club] Avoiding some unfold with simpl,
Alexandre Pilkiewicz
- Re: [Coq-Club] Avoiding some unfold with simpl,
Lauri Alanko
- Re: [Coq-Club] Avoiding some unfold with simpl, Alexandre Pilkiewicz
- Re: [Coq-Club] Avoiding some unfold with simpl,
Adam Chlipala
Archive powered by MhonArc 2.6.16.