The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

This small example can also be solved using destruct
(hence light proof term and easy control on names).
The script is not that long either.

On Thu, Apr 07, 2011 at 09:45:08AM +0200, Guillaume Melquiond wrote:
> 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

intros H.
change (if false then True else a = 0).
destruct H as [e | _]; try exact I.

There are many variants. For more examples, including from sf, you may
have a look at "Small Inversions".
http://hal.inria.fr/inria-00489412/en/

Hope this helps,
JF