The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi,

On Wed, Apr 06, 2011 at 06:50:54PM +0200, Benjamin C. Pierce wrote:

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

I generally prefer using 'destruct' when possible because it is more
elementary and generates shorter proof terms (I am maniacal, I like
generating short proofs, I frequently use "Show Proof" to see them).

On the other hand, 'inversion' almost always generates long terms. I
don't like that, even if it has no importance: it is just not 'pretty'
in my eyes.

But, well, for a value of an inductive type in a hypothesis, only
'inversion' seems to work.

There is another reason why I don't like inversion: it often generates
a lot of unuseful sub-variables, I don't know why. I often write:
   inversion x; subst.
Or I try to name these variables through:
    inversion x as [x y z t | u v a b...].
But it is not obvious to see which and how many variables are generated.
I just experiment several times.

Inversion is good for generating just the minimum number of goals.

For an hypothesis of the form (e.g. for the type 'option'):
    H: Some x = None
I prefer using 'discriminate H'.

But I don't konw Coq for a long time and perhaps there are things and
tricks I did not discover yet.

BTW, I learnt it with your tutorial! Very good one!

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/