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).