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.

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.

Lemma option_map_None:
  forall {A B} (f: A -> B) oa,
    option_map f oa = None <-> oa = None.

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.