110 lines
3.6 KiB
Text
110 lines
3.6 KiB
Text
|
(** 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" ].
|
||
|
|
>>
|
||
|
|
|
||
|
|
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. *)
|