The Coq mailing list

[roconnor AT theorem.ca]

On Sat, 4 Jul 2009, Robin Green wrote:

> If I use Proof. ... Defined. to build a term, and I use inversion in
> the proof, the generated proof term can be quite complicated. If I use
> "info inversion" to see what tactics are being used in that proof step,
> the output is quite long. So it looks like it would be a lot of work
> for me to understand how the inversion tactic works in this particular
> situation.
>
> Is there any way, apart from using the simple inversion tactic, to make
> the proof terms less complicated for a proof involving inversion? Or at
> least, in some sense easier to work with in a subsequent proof
> involving that definition?

I'm not sure why no one mentioned this, but you can write:

Derive Inversion MyInversionLemma ...

to automatically generate a new lemma called "MyInversionLemma". Then you 
can use this lemma in your proof.

Check the manual for how to use "Derive Inversion".

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''