Lvc.Infra.CoreTactics

Some generally useful tactics.

The venerable if tactical. (from cocorico)

Tactic Notation "if" tactic(t) "then" tactic(t1) "else" tactic(t2) :=
first [ t; first [ t1 | fail 2 ] | t2 ].

Destruct if arguments for case analysis.

Tactic Notation "decompose" "records" :=
  repeat (
    match goal with
      | H: _ |- _ ⇒ progress (decompose record H); clear H
    end).

Tactic Notation "dcr" :=
  repeat (
    match goal with
      | H: _ |- _ ⇒ progress (decompose record H); clear H
    end).

Tactic Notation "subst" "++" :=
  repeat (
    match goal with
      | H : _ |- _ ⇒ subst H
    end);
  cbv zeta beta in ×.

Ltac dependent_intros :=
  repeat match goal with
      | [|- ?A → ?B] ⇒ fail 1
      | [|- ?A → _] ⇒ intros ?
    end.

Ltac abstract_pair a b :=
  let r := fresh "r" in
    pose (r := (a,b));
      replace (a,b) with r in × by reflexivity;
      replace a with (fst r) in × by reflexivity;
      replace b with (snd r) in × by reflexivity.

Ltac destruct_one_pair :=
match goal with
   | [H : (_ ∧ _) |- _] ⇒ destruct H
   | [H : prod _ _ |- _] ⇒ destruct H
end.

Ltac destruct_pairs := repeat (destruct_one_pair).