The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Michael wrote:
> 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)?
>    

Here's a simple tactic definition that should do what you want:

Ltac t := repeat match goal with
                   | [ H : _ |- _ ] => rewrite H
                 end.

If you have quantified equality hypotheses with side conditions, you'll 
need to be a little more clever.

The [autorewrite] tactic is the appropriate choice for applying 
already-proved theorems.