The Coq mailing list

[Paolo Herms <paolo.herms AT cea.fr>]

On Thursday 07 April 2011 09:45:24 Guillaume Melquiond wrote:
> 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. 

But Benjamin doesn't like to talk about dependent types, he just uses them.
So an easier example is this one:

Goal forall x, x ≤ 0 → x = 0.
  destruct 1.
   (* leads to two subgoals, of which the second one is unprovable *)
  Undo.  
  inversion 1.
   (* leads to one trivial subgoal *)

Why? Because "destruct" generalises the subterm "0" to some "m" that all 
information about is lost. You can still solve the goal with "destruct" but 
you need to keep the information that "m" is equal to 0:

  Undo.
  remember 0 as m. destruct 1.
   (* leads to two subgoals, of which the second one is provable by absurd. *)

This is what "inversion" does, discharging the absurd second subgoal 
automatically.

-- 
Paolo Herms
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
Paris, France