The Coq mailing list

[Nathan Collins <nathan.collins AT gmail.com>]

On Wed, Apr 6, 2011 at 9:50 AM, Benjamin C. Pierce
<bcpierce AT cis.upenn.edu>
 wrote:
> Dear Coq experts,
>
> Someone in my class asked a question about destruct vs. inversion: They can 
> be described in similar terms  ("generate subgoals for each of the possible 
> ways that such-and-such could have been built..."), and there are many 
> situations where either can be used; so what's the actual difference?
>
> Does anyone have a concise, intuitive way of explaining how they overlap in 
> function and how they differ, and/or a snappy characterization of when to 
> use one and when the other?

There is a nice discussion of some differences between inversion and
destruct (and induction), and some guidelines and gotchas, in chapter
4.4 (pages 72-3) of Adam Chlipala's CPDT [1].

Another difference is that destruct will work on a compound
expression, but inversion needs a name.  E.g. you can do

  destruct (f n)

to simplify

  match (f n) with ...

whereas

  inversion (f n)

is not allowed.

-nathan

[1] http://adam.chlipala.net/cpdt/