coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [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.