Library AdditionalTactics

A library of additional tactics.





Require Export String.

Open Scope string_scope.

Extensions of the standard library

"remember c as x in |-" replaces the term c by the identifier x in the conclusion of the current goal and introduces the hypothesis x=c into the context. This tactic differs from a similar one in the standard library in that the replacmement is made only in the conclusion of the goal; the context is left unchanged.





Tactic Notation "remember" constr(c) "as" ident(x) "in" "|-" :=

  let x := fresh x in

  let H := fresh "Heq" x in

  (set (x := c); assert (H : x = c) by reflexivity; clearbody x).

"unsimpl E" replaces all occurence of X by E, where X is the result that tactic simpl would give when used to evaluate E.





Tactic Notation "unsimpl" constr(E) :=

  let F := (eval simpl in E) in change F with E.

The following tactic calls the apply tactic with the first hypothesis that succeeds, "first" meaning the hypothesis that comes earlist in the context (i.e., higher up in the list).





Ltac apply_first_hyp :=

  match reverse goal with

    | H : _ |- _ => apply H

  end.

Variations on `auto`

The auto* and eauto* tactics are intended to be "stronger" versions of the auto and eauto tactics. Similar to auto and eauto, they each take an optional "depth" argument. Note that if we declare these tactics using a single string, e.g., "auto*", then the resulting tactics are unusable since they fail to parse.





Tactic Notation "auto" "*" :=

  try solve [ congruence | auto | intuition auto ].




Tactic Notation "auto" "*" integer(n) :=

  try solve [ congruence | auto n | intuition (auto n) ].




Tactic Notation "eauto" "*" :=

  try solve [ congruence | eauto | intuition eauto ].




Tactic Notation "eauto" "*" integer(n) :=

  try solve [ congruence | eauto n | intuition (eauto n) ].

Delineating cases in proofs

This section was taken from the POPLmark Wiki ( http://alliance.seas.upenn.edu/~plclub/cgi-bin/poplmark/ ).

Tactic definitions





Ltac move_to_top x :=

  match reverse goal with

  | H : _ |- _ => try move x after H

  end.




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_to_top x

  | 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.

Example

One mode of use for the above tactics is to wrap Coq's induction tactic such that 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" ].