coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Apply multiple rewrites

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Michael <michaelschausten AT googlemail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Apply multiple rewrites
Date: Wed, 11 Aug 2010 13:48:27 -0400
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; b=vEjcyomuogm85tzoJywjxXO3OjHYH4c32UujxVS1IsZ8EDZHg49Lyq6gicjkr5OxU4 cs2Ajzcl2m+JUP6VpEkAuVqtgfkk/6lN7V/FN5K8k2lH1hNogv/rihJ0mg0hqOSLfd9/ 6uKGjKJcaKyoLb3OlBwpZMKzdMwLrKHss1Ul8=

Dear Micheal

It does not work for "complexe" equalities, but if you have things
like "x = y" or "x = expression", then the tactif "subst" should do
the trick

Cheers

Alexandre Pilkiewicz

2010/8/11 Michael
<michaelschausten AT googlemail.com>:
> Hello,
>
> I have a proof with a lot of hypotheses of the form X=Y. I already completed
> the proof, but it is a lot of typing. At the moment, I manually look for a
> maching hypthesis, and then rewrite the goal. The proof then looks like
> this:
>
> rewrite H0.
> rewrite H13.
> rewrite H5.
> (* Rest of the Proof *)
>
> I tried to use [congruence] to solve my proof. However, this is only
> possible
> if the proof is completed by rewrites. What I'd like to do is apply all
> hypothesis with [rewrite] (the local assumptions, and maybe a couple of
> other
> "external" theorems, until none of them is possible anymore. Is there a way
> to
> do this (maybe with Ltac)?
>
> Sincerely
>

[Coq-Club] Apply multiple rewrites, Michael
- Re: [Coq-Club] Apply multiple rewrites, Alexandre Pilkiewicz
- Re: [Coq-Club] Apply multiple rewrites, Adam Chlipala