The Coq mailing list

[Jacques Garrigue <garrigue AT math.nagoya-u.ac.jp>]

On 2011/04/07, at 22:39, Benjamin C. Pierce wrote:

> Thanks to everyone for the enlightening comments!
> 
>> The downside is that inversion terms are heavyweight, so you
>> should not use it for plain inductive types for instance.
> 
> So one possible conclusion of the discussion so far could be "inversion is 
> a fancier version of destruct, so if I don't care so much about the size of 
> proof terms and I do care a lot about minimizing the number of tactics I 
> have to explain, I should just use inversion for everything."  
> 
> I know there are some caveats to this...
> 
>  - inversion requires an identifier, so you may have to do a "remember" 
> before it
> 
>  - inversion sometimes generates lots of equalities that have to be tidied 
> using subst
> 
> ... but are there situations where inversion doesn't work and destruct does?

I'm not sure of what kind of teaching context your are thinking about, but 
for me inversion and destruct are very different beasts.

* destruct is essentially a "clever" version of case, which matches closely 
elimination rules in logic
  (elim and induction are also supposed to do that, but they use generated 
definitions, and in my opinion
   require a deeper understanding to use them)
  So I teach students to use destruct in their proofs.
  Also destruct is very regular, and it is easy to name the generated values 
and goals when using it.

* inversion may be seen indeed as a "fancier" version of destruct, but it 
does so much more that it is hard to predict
  for the beginner. I am yet to find an easy way to name the generated goals. 
So it looks more like a big hammer,
  where it would actually be better to know that you can do the same thing 
with more elementary tactics.
  Of course you have to use inversion in practice to keep proofs short, but 
it is good to know that it is not primitive.
  Maybe it could be different if there were an easier way to control 
generated variables and hypotheses.

As for situations where inversion doesn't "work", you can probably find some 
with dependent types.
Independently of that, if you write a program using tactics, which may be a 
good exercise, destruct
corresponds to pattern-matching, and in most cases you don't want to use 
inversion there.

Jacques Garrigue