Tactic Notation "solve_by_inversion_aux" tactic(t) :=
    match goal with
    | H : _ |- _ => solve [ inversion H; subst++; t ]
    end
    || fail "because the goal is not solvable by inversion.".
  
  Tactic Notation "solve" "by" "inversion" "1" :=
    solve_by_inversion_aux idtac.
  Tactic Notation "solve" "by" "inversion" "2" :=
    solve_by_inversion_aux (solve by inversion 1).
  Tactic Notation "solve" "by" "inversion" "3" :=
    solve_by_inversion_aux (solve by inversion 2).
  Tactic Notation "solve" "by" "inversion" :=
    solve by inversion 1.

solve by inversion n will attempt to solve the goal by n successive uses of inversion (where n may range between 1 and 3, given the above definitions). This tactic uses subst++ to maximize its effectiveness but could work almost as well replacing subst++ with subst.

Cocorico: solve by inversion (tactic) (last edited 11-05-2008 00:30:54 by JeffVaughan)

Cocorico!WikiLicense