The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le mercredi 06 avril 2011 à 12:50 -0400, Benjamin C. Pierce a écrit :

> 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? 

Here is a short answer that encompasses the ones you already got:
Whenever using dependent types, inversion looks at the dependency to
keep only meaningful cases, while case/destruct generates all of the
branches. The downside is that inversion terms are heavyweight, so you
should not use it for plain inductive types for instance.

Here is a small example:

Variable a : nat.
Inductive W : bool -> Type :=
  | W1 : a = 0 -> W false
  | W2 : a <> 0 -> W true.
Goal W false -> a = 0.
intros H.
- destruct H. (* ignores "false" in H and generate two subgoals, one
being unprovable! *)
- inversion H. (* generates only the goal for the W1 branch *)

Best regards,

Guillaume