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.
Ltac cases_in H :=
repeat match type of H with
|
context [
match negb ?
x with _ => _
end ] =>
destruct x;
simpl;
try solve [
inv H;
auto]
|
context [
match ?
x with _ => _
end ] =>
destruct x;
try solve [
inv H;
auto]
end;
auto.
Create HintDb conjs.
Ltac destruct_conjs :=
autounfold with conjs in *;
repeat
match goal with
|
H:
exists _, _ |- _ =>
destruct H
|
H: _ /\ _ |- _ =>
destruct H
|
x: _ * _ |- _ =>
destruct x
end;
simpl in *.
Lemma option_map_inv:
forall {
A B} (
f:
A ->
B)
oa b,
option_map f oa =
Some b ->
exists a,
oa =
Some a /\
b =
f a.
Proof.
unfold option_map;
intros *
E.
cases;
inv E;
eauto.
Qed.
Lemma option_map_None:
forall {
A B} (
f:
A ->
B)
oa,
option_map f oa =
None <->
oa =
None.
Proof.
unfold option_map;
intros;
cases;
intuition;
discriminate.
Qed.
Ltac inv_equalities :=
destruct_conjs;
subst;
repeat
match goal with
|
H: (_, _) = (_, _) |- _ =>
inv H
|
H:
option_map _ _ =
Some _ |- _ =>
let Hf :=
fresh "Hf" in
let Heq :=
fresh "Heq" in
apply option_map_inv in H as (?&
Hf&
Heq);
destruct_conjs
|
H:
option_map _ _ =
None |- _ =>
apply option_map_None in H
end;
subst.
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).
Tactic Notation "take" uconstr(
ty1)
"," uconstr(
ty2)
"and" tactic(
tac) :=
let it1 :=
fresh "it1" in
let it2 :=
fresh "it2" in
summon ty1 as it1;
summon ty2 as it2;
tac.