Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Avoiding some unfold with simpl

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Avoiding some unfold with simpl


chronological Thread 
  • From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
  • To: Adam Chlipala <adam AT chlipala.net>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Avoiding some unfold with simpl
  • Date: Tue, 26 Oct 2010 14:17:28 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=RMTQRaYCskszzE/QZq4rV98ghGHW9pfCoVSdzctHM1RnzWeoLN7m4ZdO42bWpjN4Ae /82448WpBfJ+lTZb2kgPuw413zGi5g4TI+0/JpXDs0M00yGMV/kalTZ61t+43gaZuN1U 3dBjLQ7t0fMD3Ng/cmh/SOlfZVJeA9ljJMBk0=

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




Archive powered by MhonArc 2.6.16.

Top of Page