The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Wednesday 06 April 2011 09:50:29 Benjamin C. Pierce 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?
> 
> Thanks!
> 
>    - Benjamin

inversion generates equalities and automatically does discriminate/injection 
as appropriate, whereas destruct doesn't.  My rule of thumb is: if the 
inductive variables of the type are complex expressions, especially if they 
involve constructors of that type, then I use inversion; otherwise, if 
they're 
all just variable names (or the complex ones don't really matter), I use 
destruct.  (Actually, it might be better just to try destruct first, and if 
that doesn't generate enough context to continue, back up and use inversion 
instead.)

An exception is when the goal contains something like "(foo (bar a b) c)" 
where foo returns a subset type or something similar, then I tend to use 
"destruct foo" to split out the value and the satisfaction hypothesis.
-- 
Daniel Schepler