Folding tactics

Pierre Letouzey edited this page Oct 27, 2017 · 4 revisions

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 *.
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.