ssr_inversion.v

From mathcomp.ssreflect Require Import all_ssreflect.

Ltac injection_top :=
    match goal with 
    | |- ?x = ?y -> _ => 
      first
        [ by discriminate
        | is_var x; move=>? 
        | is_var y; move=>? 
        | move=>[]
        ]
    end.

Ltac injection_all0 tac :=
repeat
    match goal with 
    | |- _ = _ -> _ => 
        injection_top
    | |- forall (_:_), _ =>
        let x := fresh in 
        move=>x; try injection_all0 tac; move:x
    | |- ?P -> _ =>
        let H := fresh in 
        move=>H; try injection_all0 tac ; move:H
    | |- ?X => 
        tac
    end.

Ltac injection_all :=
    injection_all0 ltac:(idtac).

Ltac injection_subst :=
    injection_all0 ltac:(subst=>//=).

Ltac inversion_subst P Hinv :=
    elim/Hinv: P => _ ; injection_subst.

Ltac inversion_using P Hinv :=
    elim/Hinv: P => _.


Inductive even : nat -> Prop :=
| even_O : even O
| even_SS : forall n, 
    even n -> 
    even (S (S n)).
Hint Constructors even.
Derive Inversion even_inv with (forall n, even n) Sort Prop.


Goal forall n, even n -> even (S (S n)).
move=>n H.
inversion_subst H even_inv => [|n0] =>//=.
by constructor. 
by constructor;constructor.
Qed.