The Coq mailing list

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

Artisanal bug fix: name the hypotheses created by inversion and

if they are Ps then add their argument to the watch list. This makes

for a really ad-hoc solution and I'd be curious to see if it's possible

to build a more reusable one.

I guess it's possible in Ocaml (?) but what about pure Ltac?

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

Require Import List.

Inductive P : nat -> Prop :=

    p0 : P 0

  | p1 : forall n, P n -> P (S n).

(* 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 =>

      let H' := fresh "H" in

      let m' := fresh "m" in

      inversion H as [H' | m' H'] ;

      match type of H' with

      | P ?z => inverse_P (z :: x :: ns)

      | _ => inverse_P (x :: ns)

      end

    end

  | _ => idtac ""

end.

(* Finally an example *)

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

intros.

inverse_P (@nil nat).

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

--
gallais

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

Inductive P : nat -> Prop :=
    p0 : P 0

  | p1 : forall n, P n -> P (S n).