Library LibTactics


A library of additional tactics.

Require Import Coq.Lists.List.
Require Import Coq.Strings.String.

Implementation note: We want string_scope to be available for the Case tactics below, but we want "++" to denote list concatenation.

Open Scope string_scope.
Open Scope list_scope.

Variations on built-in tactics


unsimpl E replaces all occurences of X in the goal by E, where X is the result that tactic simpl would give when used to reduce E.

Tactic Notation "unsimpl" constr(E) :=
  let F := (eval simpl in E) in change F with E.

fold any not folds all occurrences of not in the goal. It's useful for "cleaning up" after the intuition tactic.

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

The following tactics call (e)apply with the first hypothesis that succeeds, "first" meaning the hypothesis that comes earliest in the context, i.e., higher up in the list.

Ltac apply_first_hyp :=
  match reverse goal with
    | H : _ |- _ => apply H
  end.

Ltac eapply_first_hyp :=
  match reverse goal with
    | H : _ |- _ => eapply H
  end.

Delineating cases in proofs


Tactic definitions


Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move x at top
  | assert_eq x name
  | fail 1 "because we are working on a different case." ].

Ltac Case name := Case_aux case name.
Ltac SCase name := Case_aux subcase name.
Ltac SSCase name := Case_aux subsubcase name.
Ltac SSSCase name := Case_aux subsubsubcase name.
Ltac SSSSCase name := Case_aux subsubsubsubcase name.

Example



One mode of use for the above tactics is to wrap Coq's induction tactic such that it automatically inserts "case" markers into each branch of the proof. For example: 

 Tactic Notation "induction" "nat" ident(n) :=
   induction n; [ Case "O" | Case "S" ].
 Tactic Notation "sub" "induction" "nat" ident(n) :=
   induction n; [ SCase "O" | SCase "S" ].
 Tactic Notation "sub" "sub" "induction" "nat" ident(n) :=
   induction n; [ SSCase "O" | SSCase "S" ].


Within a proof, one might use the tactics as follows: 

    induction nat n.  (* or [induction n] *)
    Case "O".
      ...
    Case "S".
      ...


If you use such customized versions of the induction tactics, then the Case tactic will verify that you are working on the case that you think you are. You may also use the Case tactic with the standard version of induction, in which case no verification is done.

In general, you may use the Case tactics anywhere in a proof you wish to leave a "comment marker" in the context.

Tactics for working with lists and proof contexts


ltac_map applies a function F, with return type T and exactly one non-implicit argument, to everything in the context such that the application type checks. The tactic returns a list containing the results of the applications.

Implementation note: The check for duplicates in the accumulator (match acc with ...) is necessary to ensure that the tactic does not go into an infinite loop.

Ltac ltac_map F :=
  let rec map acc :=
    match goal with
      | H : _ |- _ =>
        let FH := constr:(F H) in
          match acc with
            | context [FH] => fail 1
            | _ => map (List.cons FH acc)
          end
      | _ => acc
    end
  in
  let rec ret T :=
    match T with
      | _ -> ?T' => ret T'
      | ?T' => T'
    end
  in
  let T := ret ltac:(type of F) in
  let res := map (@List.nil T) in
  eval simpl in res.

ltac_map_list tac xs applies tac to each element of xs, where xs is a Coq list.

Ltac ltac_map_list tac xs :=
  match xs with
    | List.nil => idtac
    | List.cons ?x ?xs => tac x; ltac_map_list tac xs
  end.

ltac_remove_dups takes a list and removes duplicate items from it. The supplied list must, after simplification via simpl, be built from only nil and cons. Duplicates are recognized only "up to syntax," i.e., the limitations of Ltac's context check.

Ltac ltac_remove_dups xs :=
  let rec remove xs acc :=
    match xs with
      | List.nil => acc
      | List.cons ?x ?xs =>
        match acc with
          | context [x] => remove xs acc
          | _ => remove xs (List.cons x acc)
        end
    end
  in
  match type of xs with
    | List.list ?A =>
      let xs := eval simpl in xs in
      let xs := remove xs (@List.nil A) in
      eval simpl in (List.rev xs)
  end.


Axiom skip : False.
Ltac skip := assert False; [ apply skip | contradiction ].

Simple variations on existing tactics


contradictions replace the goal by False and prove it if False is derivable from the context or if discriminate applies.

Ltac contradictions :=
  assert False; [ try discriminate | contradiction ].

cuts does cut then intro in the first subgoal.

Ltac cuts H E :=
  cut (E); [ intro H | idtac ].

inversions H is a shortcut for inversion H followed by subst.

Ltac inversions H :=
  inversion H; subst.

poses H E adds an hypothesis with name H and with type the type of E.

Ltac poses H E :=
  pose (H := E); clearbody H.

puts is a version of poses where Coq chooses the name introduced.

Ltac puts E :=
  let H := fresh in poses H E.

asserts H E is a synonymous for assert (X : E) provided for uniformity with the rest of the syntax.

Ltac asserts H E :=
  assert (H : E).

sets X E replaces all occurences of E by a name X, and forgets the fact that X is equal to X -- it makes the goal more general

Ltac sets X E :=
  set (X := E) in *; clearbody X.

introz repeats intro as long as possible. Contrary to intros, it unfolds any definition on the way.

Ltac introz :=
  intro; try introz.

Unfolding


folds is a shortcut for fold in *

Tactic Notation "folds" constr(H) :=
  fold H in *.
Tactic Notation "folds" constr(H1) constr(H2) :=
  folds H1; folds H2.
Tactic Notation "folds" constr(H1) constr(H2) constr(H3) :=
  folds H1; folds H2; folds H3.

unfolds is a shortcut for unfold in *

Tactic Notation "unfolds" reference(F1) :=
  unfold F1 in *.
Tactic Notation "unfolds" reference(F1) reference(F2) :=
  unfold F1 in *; unfold F2 in *.
Tactic Notation "unfolds" reference(F1) reference(F2) reference(F3) :=
  unfold F1 in *; unfold F2 in *; unfold F3 in *.

unfold_hd unfolds the definition at the head of the goal.

Tactic Notation "unfold_hd" :=
  match goal with
  | |- ?P => unfold P
  | |- ?P _ => unfold P
  | |- ?P _ _ => unfold P
  | |- ?P _ _ _ => unfold P
  | |- ?P _ _ _ _ => unfold P
  end.

Simplification


simpls is a shortcut for simpl in *

Tactic Notation "simpls" :=
  simpl in *.
Tactic Notation "simpls" reference(F1) :=
  simpl F1 in *.
Tactic Notation "simpls" reference(F1) reference(F2) :=
  simpl F1 in *; simpl F2 in *.
Tactic Notation "simpls" reference(F1) reference(F2) reference(F3) :=
  simpl F1 in *; simpl F2 in *; simpl F3 in *.

unsimpl E replaces all occurence of X by E, where X is the result which tactic simpl would give when applied to E.

Tactic Notation "unsimpl" constr(E) :=
  let F := (eval simpl in E) in change F with E.

Tactic Notation "unsimpl" constr(E) "in" hyp(H) :=
  let F := (eval simpl in E) in change F with E in H.

Rewriting


rewrites is an iterated version of rewrite. Beware of loops!

Tactic Notation "rewrites" constr(E) :=
  repeat rewrite E.
Tactic Notation "rewrites" "<-" constr(E) :=
  repeat rewrite <- E.
Tactic Notation "rewrites" constr(E) "in" ident(H) :=
  repeat rewrite E in H.
Tactic Notation "rewrites" "<-" constr(E) "in" ident(H) :=
  repeat rewrite <- E in H.

asserts_rew can be used to assert an equality holds and rewrite it straight away in the current goal

Tactic Notation "asserts_rew" constr(E) :=
  let EQ := fresh in (assert (EQ : E);
  [ idtac | rewrite EQ; clear EQ ]).
Tactic Notation "asserts_rew" "<-" constr(E) :=
  let EQ := fresh in (assert (EQ : E);
  [ idtac | rewrite <- EQ; clear EQ ]).
Tactic Notation "asserts_rew" constr(E) "in" hyp(H) :=
  let EQ := fresh in (assert (EQ : E);
  [ idtac | rewrite EQ in H; clear EQ ]).
Tactic Notation "asserts_rew" "<-" constr(E) "in" hyp(H) :=
  let EQ := fresh in (assert (EQ : E);
  [ idtac | rewrite <- EQ in H; clear EQ ]).

do_rew is used to perform the sequence: rewrite the goal, execute a tactic, rewrite the goal back

Tactic Notation "do_rew" constr(E) tactic(T) :=
  rewrite E; T; try rewrite <- E.

Tactic Notation "do_rew" "<-" constr(E) tactic(T) :=
  rewrite <- E; T; try rewrite E.

do_rew_2 is the same as do_rew but it does rewrite twice

Tactic Notation "do_rew_2" constr(E) tactic(T) :=
  do 2 rewrite E; T; try do 2 rewrite <- E.

Tactic Notation "do_rew_2" "<-" constr(E) tactic(T) :=
  do 2 rewrite <- E; T; try do 2 rewrite E.

Tactic Notation "repeat_rew" constr(E) tactic(T) :=
  repeat rewrite E; T; try repeat rewrite <- E.

Tactic Notation "repeat_rew" "<-" constr(E) tactic(T) :=
  repeat rewrite <- E; T; repeat rewrite E.

Generalization


gen_eq c as x H takes all occurrences of c in the current goal's conclusion, replaces them by the variable x, and introduces the equality x = c as the hypothesis H. Useful if one needs to generalize the goal prior to applying an induction tactic.

Tactic Notation "gen_eq" constr(c) "as" ident(x) ident(H) :=
  set (x := c); assert (H : x = c) by reflexivity; clearbody x.

Tactic Notation "gen_eq" constr(c) "as" ident(x) ident(H) "at" integer(n) :=
  set (x := c) at n ; assert (H : x = c) by reflexivity; clearbody x.

A variation on the above in which all occurrences of c in the goal are replaced, not only those in the conclusion.

Tactic Notation "gen_eq" constr(c) "as" ident(x) :=
  set (x := c) in *;
  let H := fresh in (assert (H : x = c) by reflexivity; clearbody x; revert H).

gen is a shortname for the generalize dependent tactic.

Tactic Notation "gen" ident(X1) :=
  generalize dependent X1.
Tactic Notation "gen" ident(X1) ident(X2) :=
  gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) :=
  gen X3; gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) :=
  gen X4; gen X3; gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5) :=
  gen X5; gen X4; gen X3; gen X2; gen X1.

Splitting N-ary Conjonctions


split3 and split4 respectively destruct a triple and a quadruple of propositions.

Tactic Notation "split3" :=
  split; [ idtac | split ].
Tactic Notation "split4" :=
  split; [ idtac | split3 ].

splits calls split recursively as long as possible.

Tactic Notation "splits" :=
  repeat split.

esplitN are iterated version of esplit, used to introduce uninstanciated variables in goal of the form exists x, P x.

Tactic Notation "esplit2" :=
  esplit; esplit.
Tactic Notation "esplit3" :=
  esplit; esplit; esplit.
Tactic Notation "esplit4" :=
  esplit; esplit; esplit; esplit.

Branching N-ary Disjunction


Short-hand tactics for branching when the goal is of the form P1 \/ P2 \/ P3.

Tactic Notation "or_31" := left.
Tactic Notation "or_32" := right; left.
Tactic Notation "or_33" := right; right.

Destructing conjonctions behind implications


destructi T is to be used on a T of the form A1 -> .. -> AN -> X /\ Y. It generates the Ai as subgoals and adds two hypotheses X and Y to the current goal.

Tactic Notation "destructi" constr(T) :=
  let rec doit H :=
    match type of H with
    | ?P -> ?Q => let A := fresh "A" in
      (assert (A : P); [ idtac | doit (H A); clear A ])
    | _ => first [destruct H | puts H]
    end in doit T.

Tactic Notation "destructi" constr(T) "as" simple_intropattern(I) :=
  let rec doit H :=
    match type of H with
    | ?P -> ?Q => let A := fresh "A" in
      (assert (A : P); [ idtac | doit (H A); clear A ])
    | _ => first [destruct H as I | poses I H]
    end in doit T.

destructs T calls destruct recursively on T as long as possible

Ltac destructs H :=
  let X := fresh in let Y := fresh in
  first [ destruct H as [X Y]; destructs X; destructs Y | idtac ].

Introduction


introv is used to repeat intro on all dependent variables; basically it introduces all the names which are mentionned further in the goal.

Tactic Notation "introv" :=
  let rec go _ := match goal with
  | |- ?P -> ?Q => idtac
  | |- forall _, _ => intro; try go tt
  end in first [ go tt | intro; go tt ].

Tactic Notation "introv" simple_intropattern(I) :=
  introv; intros I.
Tactic Notation "introv" simple_intropattern(I1) ident(I2) :=
  introv; intros I1 I2.
Tactic Notation "introv" simple_intropattern(I1) ident(I2) ident(I3) :=
  introv; intros I1 I2 I3.
Tactic Notation "introv" simple_intropattern(I1) ident(I2) ident(I3) ident(I4) :=
  introv; intros I1 I2 I3 I4.
Tactic Notation "introv" simple_intropattern(I1) ident(I2) ident(I3) ident(I4) ident(I5) :=
  introv; intros I1 I2 I3 I4 I5.

Exists


exists T1 ... TN is a shorthand for exists T1; ...; exists TN.

Tactic Notation "exists" constr(T1) :=
  exists T1.
Tactic Notation "exists" constr(T1) constr(T2) :=
  exists T1; exists T2.
Tactic Notation "exists" constr(T1) constr(T2) constr(T3) :=
  exists T1; exists T2; exists T3.
Tactic Notation "exists" constr(T1) constr(T2) constr(T3) constr(T4) :=
  exists T1; exists T2; exists T3; exists T4.

Forward Chaining - Adapted from a suggestion by Xavier Leroy


Lemma modus_ponens : forall (P Q : Prop),
  P -> (P -> Q) -> Q.
Proof. auto. Qed.

Implicit Arguments modus_ponens [P Q].

Tactic Notation "forward" constr(x) "as" simple_intropattern(H) :=
    (refine (modus_ponens (x _ _ _ _ _ _ _ _ _) _); [ | | | | | | | | | intros H ])
 || (refine (modus_ponens (x _ _ _ _ _ _ _ _) _); [ | | | | | | | | intros H ])
 || (refine (modus_ponens (x _ _ _ _ _ _ _) _); [ | | | | | | | intros H ])
 || (refine (modus_ponens (x _ _ _ _ _ _) _); [ | | | | | | intros H ])
 || (refine (modus_ponens (x _ _ _ _ _) _); [ | | | | | intros H ])
 || (refine (modus_ponens (x _ _ _ _) _); [ | | | | intros H ])
 || (refine (modus_ponens (x _ _ _) _); [ | | | intros H ])
 || (refine (modus_ponens (x _ _) _); [ | | intros H ])
 || (refine (modus_ponens (x _) _); [ | intros H ])
 || (refine (modus_ponens (x _ _ _ _ _ _ _ _ _) _); [ | | | | | | | | intros H ])
 || (refine (modus_ponens (x _ _ _ _ _ _ _ _) _); [ | | | | | | | intros H ])
 || (refine (modus_ponens (x _ _ _ _ _ _ _) _); [ | | | | | | intros H ])
 || (refine (modus_ponens (x _ _ _ _ _ _) _); [ | | | | | intros H ])
 || (refine (modus_ponens (x _ _ _ _ _) _); [ | | | | intros H ])
 || (refine (modus_ponens (x _ _ _ _) _); [ | | | intros H ])
 || (refine (modus_ponens (x _ _ _) _); [ | | intros H ])
 || (refine (modus_ponens (x _ _) _); [ | intros H ])
 || (refine (modus_ponens (x _) _); [ intros H ]).

Tactic Notation "forward" constr(x) :=
    refine (modus_ponens (x _ _ _ _ _ _ _ _ _ _) _)
 || refine (modus_ponens (x _ _ _ _ _ _ _ _ _) _)
 || refine (modus_ponens (x _ _ _ _ _ _ _ _) _)
 || refine (modus_ponens (x _ _ _ _ _ _ _) _)
 || refine (modus_ponens (x _ _ _ _ _ _) _)
 || refine (modus_ponens (x _ _ _ _ _) _)
 || refine (modus_ponens (x _ _ _ _) _)
 || refine (modus_ponens (x _ _ _) _)
 || refine (modus_ponens (x _ _) _)
 || refine (modus_ponens (x _) _).

Tactics with Automation


The name of a tactic followed by a star means: apply the tactic, then applies auto* on the generated subgoals. auto* is a tactic which tries to solve the goal with either auto or intuition eauto. It leaves the goal unchanged if it can't solve the goal.

Exceptions to the naming convention are: take which stands for exists* and use which stands for puts*. Exceptions to the behaviour for asserts* which only calls auto* in the new subgoal, and apply* which first tries apply and if it fails it tries eapply and then in both cases calls auto*.

Tactic Notation "auto" "*" :=
  try solve [ auto | intuition eauto ].
Tactic Notation "auto" "*" int_or_var(n) :=
  try solve [ auto | intuition (eauto n) ].
Tactic Notation "asserts" "*" ident(H) constr(E) :=
  assert (H : E); [ auto* | idtac ].
Tactic Notation "apply" "*" constr(H) :=
  first [ apply H | eapply H ]; auto*.
Tactic Notation "apply" "*" constr(H) :=
  first [ apply H | eapply H ]; auto*.
Tactic Notation "contradictions" "*" :=
  contradictions; auto*.
Tactic Notation "destruct" "*" constr(H) :=
  destruct H; auto*.
Tactic Notation "destruct" "*" constr(H) "as" simple_intropattern(I) :=
  destruct H as I; auto*.
Tactic Notation "f_equal" "*" :=
  f_equal; auto*.
Tactic Notation "induction" "*" constr(H) :=
  induction H; auto*.
Tactic Notation "inversion" "*" constr(H) :=
  inversion H; auto*.
Tactic Notation "inversions" "*" constr(H) :=
  inversions H; auto*.
Tactic Notation "rewrite" "*" constr(H) :=
  rewrite H; auto*.
Tactic Notation "rewrite" "*" "<-" constr(H) :=
  rewrite <- H; auto*.
Tactic Notation "do_rew" "*" constr(E) tactic(T) :=
  (do_rew E T); auto*.
Tactic Notation "do_rew" "*" "<-" constr(E) tactic(T) :=
  (do_rew <- E T); auto*.
Tactic Notation "do_rew_2" "*" constr(E) tactic(T) :=
  (do_rew_2 E T); auto*.
Tactic Notation "do_rew_2" "*" "<-" constr(E) tactic(T) :=
  (do_rew_2 <- E T); auto*.
Tactic Notation "simpl" "*" :=
  simpl; auto*.
Tactic Notation "simpls" "*" :=
  simpls; auto*.
Tactic Notation "unsimpl" "*" constr(E) :=
  unsimpl E; auto*.
Tactic Notation "unsimpl" "*" constr(E) "in" hyp(H) :=
  unsimpl E in H; auto*.
Tactic Notation "split" "*" :=
  split; auto*.
Tactic Notation "split3" "*" :=
  split3; auto*.
Tactic Notation "split4" "*" :=
  split4; auto*.
Tactic Notation "splits" "*" :=
  splits; auto*.
Tactic Notation "esplit2" "*" :=
  esplit2; auto*.
Tactic Notation "esplit3" "*" :=
  esplit3; auto*.
Tactic Notation "esplit4" "*" :=
  esplit4; auto*.
Tactic Notation "right" "*" :=
  right; auto*.
Tactic Notation "left" "*" :=
  left; auto*.
Tactic Notation "or_31" "*" :=
  or_31; auto*.
Tactic Notation "or_32" "*" :=
  or_32; auto*.
Tactic Notation "or_33" "*" :=
  or_33; auto*.
Tactic Notation "destructi" "*" constr(H) :=
  destructi H; auto*.
Tactic Notation "subst" "*" :=
  subst; auto*.
Tactic Notation "use" constr(expr) :=
  puts expr; auto*.
Tactic Notation "use" constr(expr1) constr(expr2) :=
  puts expr1; use expr2.
Tactic Notation "use" constr(expr1) constr(expr2) constr(expr3) :=
  puts expr1; use expr2 expr3.
Tactic Notation "exists" "*" constr(T1) :=
  exists T1; auto*.
Tactic Notation "exists" "*" constr(T1) constr(T2) :=
  exists T1 T2; auto*.
Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) :=
  exists T1 T2 T3.
Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) constr(T4) :=
  exists T1 T2 T3 T4.
Tactic Notation "forward" "*" constr(x) "as" simple_intropattern(H) :=
  forward x; auto*.
Tactic Notation "forward" "*" constr(x) :=
  forward x; auto*.

Tactics with Limited Automation


Tactic Notation "rewrite" "~" constr(H) :=
  rewrite H; auto.
Tactic Notation "rewrite" "~" "<-" constr(H) :=
  rewrite <- H; auto.
Tactic Notation "apply" "~" constr(H) :=
  first [ apply H | eapply H ]; auto.
Tactic Notation "destructi" "~" constr(H) :=
  destructi H; auto.
Tactic Notation "destruct" "~" constr(H) :=
  destruct H; auto.
Tactic Notation "destruct" "~" constr(H) "as" simple_intropattern(I) :=
  destruct H as I; auto.
Tactic Notation "destructi" "~" constr(H) "as" simple_intropattern(I) :=
  destructi H as I; auto.
Tactic Notation "split" "~" :=
  split; auto.
Tactic Notation "split3" "~" :=
  split3; auto.
Tactic Notation "split4" "~" :=
  split4; auto.
Tactic Notation "splits" "~" :=
  splits; auto.
Tactic Notation "forward" "~" constr(x) "as" simple_intropattern(H) :=
  forward x as H; auto.
Tactic Notation "forward" "~" constr(x) :=
  forward x; auto.

Projections


Short-hand notations for projections from triples.

Notation "'proj31' P" := (proj1 P) (at level 69).
Notation "'proj32' P" := (proj1 (proj2 P)) (at level 69).
Notation "'proj33' P" := (proj2 (proj2 P)) (at level 69).

Notation "'proj41' P" := (proj1 P) (at level 69).
Notation "'proj42' P" := (proj1 (proj2 P)) (at level 69).
Notation "'proj43' P" := (proj1 (proj2 (proj2 P))) (at level 69).
Notation "'proj44' P" := (proj2 (proj2 (proj2 P))) (at level 69).