The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 27 Nov 2012 20:18:48 +0800,
Yucheng Zhang 
<yczhang89 AT gmail.com>
 a écrit :

> Hello,
> 
> Suppose I have a goal:
> 
> H1 : P x
> H2 : P y
> H3 : P z
> -------------
> Q
> 
> where P is an inductive predicate. I want to do 'inversion' on each
> of the hypothesis automatically. I know I can do like this:
> 
> do 3 match goal with
>   | [ H : P _ |- _ ] => inversion H; move H at top
> end
> 
> But is there a 'better' way?
> 
> Thanks
> 
> 
> Yucheng Zhang

I do not know if there is a better way, but I would tend to "clear H"
instead of "move H at top" (or rather 'at bottom', I think).
Most of the time, I do not want to keep the original hypothesis.

So maybe a

Ltac cleanP :=
 match goal with [ H : P _ |- _ ] => inversion H; clear H; subst end.

would help. (Note: the subst may not do what you wish, since it would
use all already present equalities)

> H1 : P x
> H2 : P y
> H3 : P z
> -------------
> Q

repeat cleanP. (* alternatively 'do 3 cleanP.' *)

If your P predicate is recursive, you will encounter problems with
tactic called endlessly.