AdditionalTactics.v

(** 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.
Ltac SSSCase name := Case_aux subsubsubcase 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" ].
>>

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