The Coq mailing list

[gallais <guillaume.allais AT ens-lyon.org>]

Hi Yucheng,

Here is a potential solution: maintaining a list of values

on which inversion was already performed and skip them

next time we encounter them.

This way you should avoid looping forever.

==============================

Require Import List.

Inductive P : nat -> Prop :=

  p0 : P 0.

(* here we have a **syntactic** search for n in the list ns *)

Ltac is_in_dec n ns := match ns with

  | nil     => false

  | n :: _  => true

  | _ :: ?tl => is_in_dec n tl

end.

(* Here the first case looks for new values by failing on old ones,

and the catch-all one allows the tactics to succeed when all the

work has been done. 

cf. this bit of cpdt for more details on the behaviour of the first

match: http://adam.chlipala.net/cpdt/html/Match.html *)

Ltac inverse_P ns := match goal with

  | [ H: P ?x |- _ ] =>

    let test := is_in_dec x ns in

    match constr:test with

    | true  => fail

    | false => inversion H ; inverse_P (x :: ns)

    end

  | _ => idtac ""

end.

(* Finally an example *)

Goal forall x y z, P x -> P y -> P z.

intros.

inverse_P (@nil nat).

==============================

Cheers,

--
gallais

On 28 November 2012 01:41, Yucheng Zhang <yczhang89 AT gmail.com> wrote:

On Nov 27, 2012, at 8:49 PM, AUGER Cédric <sedrikov AT gmail.com> wrote:
> 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.

Thanks for the detailed answer.

I am not satisfied with the solution though, as my P predicate is indeed
recursive, and the number of P hypotheses is not known in advance. (I should
have formulated my question more accurately..)

Maybe a solution is 'do 5 cleanP', where 5 is an arbitarily chosen finite
number that is large enough, but this looks not so elegant.