# Module CommonTactics

Ltac inv H := inversion H; clear H; subst.

Ltac cases :=
repeat match goal with
| H: context [ match negb ?x with _ => _ end ] |- _ =>
destruct x; simpl; try solve [inv H; auto]
| H: context [ match ?x with _ => _ end ] |- _ =>
destruct x; try solve [inv H; auto]
| |- context [ match negb ?x with _ => _ end ] =>
destruct x; simpl
| |- context [ match ?x with _ => _ end ] =>
destruct x
end; auto.

Ltac cases_eqn E :=
repeat match goal with
| H: context [ match negb ?x with _ => _ end ] |- _ =>
let E := fresh E in
destruct x eqn: E; simpl; try solve [inv H; auto]
| H: context [ match ?x with _ => _ end ] |- _ =>
let E := fresh E in
destruct x eqn: E; try solve [inv H; auto]
| |- context [ match negb ?x with _ => _ end ] =>
let E := fresh E in
destruct x eqn: E; simpl
| |- context [ match ?x with _ => _ end ] =>
let E := fresh E in
destruct x eqn: E
end; auto.

Tactic Notation "summon" uconstr(ty) "as" ident(id) :=
match goal with H : _ |- _ => pose (id := H : ty); clear id; rename H into id end.

Tactic Notation "take" uconstr(ty) "and" tactic(tac) :=
let new_it := fresh "it"
in try (rename it into new_it);
summon ty as it; tac;
try (rename new_it into it).