Folding tactics

These tactic definitions can be used to fold multiple instances of negations:

Tactic Notation "fold" "any" "not" :=
  repeat (
    match goal with
    | |- context [?P -> False] =>
      fold (~ P)
    end).

Tactic Notation "fold" "any" "not" "in" ident(H) "|-" :=
  repeat (
    match goal with
    | J: context [?P -> False] |- _ =>
      fold (~ P) in H
    end).

Tactic Notation "fold" "any" "not" "in" ident(H) :=
  fold any not in H |-.

Tactic Notation "fold" "any" "not" "in" "*" "|-" :=
  repeat (
    match goal with
    | H: context [?P -> False] |- _ =>
      fold (~ P) in H
    end).

Tactic Notation "fold" "any" "not" "in" "*" :=
  fold any not in * |-; fold any not.

Tactic Notation "fold" "any" "not" "in" "*" "|-" "*" :=
  fold any not in *.

Similarly, these tactics can be uses to fold logical equivalences:

Tactic Notation "fold" "any" "iff" :=
  repeat (
    match goal with
    | |- context [(?P -> ?Q) /\ (?Q -> ?P)] =>
      fold (P <-> Q)
    end).

Tactic Notation "fold" "any" "iff" "in" ident(H) "|-" :=
  repeat (
    match goal with
    | J: context [(?P -> ?Q) /\ (?Q -> ?P)] |- _ =>
      fold (P <-> Q) in H
    end).

Tactic Notation "fold" "any" "iff" "in" ident(H) :=
  fold any iff in H |-.

Tactic Notation "fold" "any" "iff" "in" "*" "|-" :=
  repeat (
    match goal with
    | H: context [(?P -> ?Q) /\ (?Q -> ?P)] |- _ =>
      fold (P <-> Q) in H
    end).

Tactic Notation "fold" "any" "iff" "in" "*" :=
  fold any iff in * |-; fold any iff.

Tactic Notation "fold" "any" "iff" "in" "*" "|-" "*" :=
  fold any iff in *.