The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

coqletsgo AT yahoo.com
 wrote:
> If I understand it correctly, it's an issue I find myself often into: I do a
> case analysis on some variable, which spawns dozens of cases, all of which
> require some particular treatment *in the beginning*, but then are all 
> resolved
> in a similar fashion. Since the initial tactics are different, it's quite hard
> to compose using semicolon and brackets, but afterwards I end up repeating 10
> lines of simple tactics for each goal (since they are already split in
> different subgoals, there's not much semicolon can do).
>
> I resorted to using some "local Ltac definitions" inside the lemmas, but they
> are ugly and they survive the end of the lemma (which forces me to choose
> different names each time). Is there a more elegant solution? Like some
> multi-goal repeat (that applies not only to the current goal, but to each goal
> that appears after the previous one was solved, until the current goal cannot
> be solved)? Or a reason that such a beast should not exist?

Yes, there are principled ways to get readable solutions without 
unneeded repetition, almost every time.  This is one of the main topics 
threaded throughout CPDT:
    http://adam.chlipala.net/cpdt/