Library Copland.Preamble

Tactics that provide useful automation.

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

Expand let expressions in both the antecedent and the conclusion.

Ltac expand_let_pairs :=
  match goal with
  | |- context [let (_,_) := ?e in _] ⇒
    rewrite (surjective_pairing e)
  | [ H: context [let (_,_) := ?e in _] |- _ ] ⇒
    rewrite (surjective_pairing e) in H
  end.

Destruct disjuncts in the antecedent without naming them.

Ltac destruct_disjunct :=
  match goal with
  | [ H: _ ∨ _ |- _ ] ⇒ destruct H as [H|H]
  end.