The Coq mailing list

[Yucheng Zhang <yczhang89 AT gmail.com>]

On Nov 28, 2012, at 10:58 AM, gallais 
<guillaume.allais AT ens-lyon.org>
 wrote:

> 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

Thanks!

It still goes into an infinite loop when the P predicate is recursive, e.g.

Inductive P : nat -> Prop :=
    p0 : P 0
  | p1 : forall n, P n -> P (S n).

This is only caused by the particular behaviour of 'inversion' tactic, so the
solution with maintaining a list may fit other situations nicely.