ITree.Basics.Tacs

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

Global Tactic Notation "intros !" := repeat intro.

Ltac flatten_goal :=
  match goal with
  | |- context[match ?x with | _ ⇒ _ end] ⇒ let Heq := fresh "Heq" in destruct x eqn:Heq
  end.

Ltac flatten_hyp h :=
  match type of h with
  | context[match ?x with | _ ⇒ _ end] ⇒ let Heq := fresh "Heq" in destruct x eqn:Heq
  end.

Ltac flatten_all :=
  match goal with
  | h: context[match ?x with | _ ⇒ _ end] |- _ ⇒ let Heq := fresh "Heq" in destruct x eqn:Heq
  | |- context[match ?x with | _ ⇒ _ end] ⇒ let Heq := fresh "Heq" in destruct x eqn:Heq
  end.

(* inv by name of the Inductive relation *)
Ltac invn f :=
    match goal with
    | [ id: f |- _ ] ⇒ inv id
    | [ id: f _ |- _ ] ⇒ inv id
    | [ id: f _ _ |- _ ] ⇒ inv id
    | [ id: f _ _ _ |- _ ] ⇒ inv id
    | [ id: f _ _ _ _ |- _ ] ⇒ inv id
    | [ id: f _ _ _ _ _ |- _ ] ⇒ inv id
    | [ id: f _ _ _ _ _ _ |- _ ] ⇒ inv id
    | [ id: f _ _ _ _ _ _ _ |- _ ] ⇒ inv id
    | [ id: f _ _ _ _ _ _ _ _ |- _ ] ⇒ inv id
    end.

(* destruct by name of the Inductive relation *)
Ltac destructn f :=
    match goal with
    | [ id: f |- _ ] ⇒ destruct id
    | [ id: f _ |- _ ] ⇒ destruct id
    | [ id: f _ _ |- _ ] ⇒ destruct id
    | [ id: f _ _ _ |- _ ] ⇒ destruct id
    | [ id: f _ _ _ _ |- _ ] ⇒ destruct id
    | [ id: f _ _ _ _ _ |- _ ] ⇒ destruct id
    | [ id: f _ _ _ _ _ _ |- _ ] ⇒ destruct id
    | [ id: f _ _ _ _ _ _ _ |- _ ] ⇒ destruct id
    | [ id: f _ _ _ _ _ _ _ _ |- _ ] ⇒ destruct id
    end.

(* apply by name of the Inductive relation *)
Ltac appn f :=
    match goal with
    | [ id: f |- _ ] ⇒ apply id
    | [ id: f _ |- _ ] ⇒ apply id
    | [ id: f _ _ |- _ ] ⇒ apply id
    | [ id: f _ _ _ |- _ ] ⇒ apply id
    | [ id: f _ _ _ _ |- _ ] ⇒ apply id
    | [ id: f _ _ _ _ _ |- _ ] ⇒ apply id
    | [ id: f _ _ _ _ _ _ |- _ ] ⇒ apply id
    | [ id: f _ _ _ _ _ _ _ |- _ ] ⇒ apply id
    | [ id: f _ _ _ _ _ _ _ _ |- _ ] ⇒ apply id
    end.

(* eapply by name of the Inductive relation *)
Ltac eappn f :=
    match goal with
    | [ id: f |- _ ] ⇒ eapply id
    | [ id: f _ |- _ ] ⇒ eapply id
    | [ id: f _ _ |- _ ] ⇒ eapply id
    | [ id: f _ _ _ |- _ ] ⇒ eapply id
    | [ id: f _ _ _ _ |- _ ] ⇒ eapply id
    | [ id: f _ _ _ _ _ |- _ ] ⇒ eapply id
    | [ id: f _ _ _ _ _ _ |- _ ] ⇒ eapply id
    | [ id: f _ _ _ _ _ _ _ |- _ ] ⇒ eapply id
    | [ id: f _ _ _ _ _ _ _ _ |- _ ] ⇒ eapply id
    end.

Ltac crunch :=
  repeat match goal with
          | [ H : ∃ X, _ |- _ ] ⇒ destruct H
          | [ H : _ ∧ _ |- _ ] ⇒ destruct H
          | [ H : _ ∨ _ |- _ ] ⇒ destruct H
          | [ |- _ ∧ _ ] ⇒ split
          end.

Ltac saturate H :=
  match goal with
          | [ H1 : ∀ a b, ?R a b → _,
              H2 : ∀ a b, ?R b a → _,
                H : ?R ?A ?B |- _ ] ⇒ pose proof (H1 A B H);
                                        pose proof (H2 B A H);
                                        clear H; crunch
          end.