*************************************************************************
* Useful General-Purpose Tactics for Coq *
* Arthur Charguéraud *
* Distributed under the terms of the LGPL-v3 license *
**************************************************************************
* This file contains a set of tactics that extends the set of builtin
tactics provided with the standard distribution of Coq. It intends
to overcome a number of limitations of the standard set of tactics,
and thereby to help user to write shorter and more robust scripts.
Hopefully, Coq tactics will be improved as time goes by, and this
file should ultimately be useless. In the meanwhile, you will
probably find it very useful.
* The main features offered are:
- More convenient syntax for naming hypotheses, with tactics for
introduction and inversion that take as input only the name of
hypotheses of type Prop, rather than the name of all variables.
- Tactics providing true support for manipulating N-ary conjunctions,
disjunctions and existentials, hidding the fact that the underlying
implementation is based on binary predicates.
- Convenient support for automation: tactic followed with the symbol
"~" or "*" will call automation on the generated subgoals.
Symbol "~" stands for auto and "*" for intuition eauto.
These bindings can be customized.
- Forward-chaining tactics are provided to instantiate lemmas
either with variable or hypotheses or a mix of both.
- A more powerful implementation of apply is provided (it is based
on refine and thus behaves better with respect to conversion).
- An improved inversion tactic which substitutes equalities on variables
generated by the standard inversion mecanism. Moreover, it supports
the elimination of dependently-typed equalities (requires axiom K,
which is a weak form of Proof Irrelevance).
- Tactics for saving time when writing proofs, with tactics to
asserts hypotheses or sub-goals, and improved tactics for
clearing, renaming, and sorting hypotheses.
* External credits:
- thanks to Xavier Leroy for providing the idea of tactic forward,
- thanks to Georges Gonthier for the implementation trick in applys,
- thanks to Hugo Herbelin and Matthieu Sozeau for useful comments.
Set Implicit Arguments.
**********************************************************************
* * Additional notations for Coq
----------------------------------------------------------------------
* ** N-ary Existentials
* exists T1 ... TN, P is a shorthand for
exists T1, ..., exists TN, P. Note that
Coq.Program.Syntax already defines exists
for arity up to 4.
Notation "'
exists'
x1 ','
P" :=
(
exists x1,
P)
(
at level 200,
x1 ident,
right associativity) :
type_scope.
Notation "'
exists'
x1 x2 ','
P" :=
(
exists x1,
exists x2,
P)
(
at level 200,
x1 ident,
x2 ident,
right associativity) :
type_scope.
Notation "'
exists'
x1 x2 x3 ','
P" :=
(
exists x1,
exists x2,
exists x3,
P)
(
at level 200,
x1 ident,
x2 ident,
x3 ident,
right associativity) :
type_scope.
Notation "'
exists'
x1 x2 x3 x4 ','
P" :=
(
exists x1,
exists x2,
exists x3,
exists x4,
P)
(
at level 200,
x1 ident,
x2 ident,
x3 ident,
x4 ident,
right associativity) :
type_scope.
Notation "'
exists'
x1 x2 x3 x4 x5 ','
P" :=
(
exists x1,
exists x2,
exists x3,
exists x4,
exists x5,
P)
(
at level 200,
x1 ident,
x2 ident,
x3 ident,
x4 ident,
x5 ident,
right associativity) :
type_scope.
Notation "'
exists'
x1 x2 x3 x4 x5 x6 ','
P" :=
(
exists x1,
exists x2,
exists x3,
exists x4,
exists x5,
exists x6,
P)
(
at level 200,
x1 ident,
x2 ident,
x3 ident,
x4 ident,
x5 ident,
x6 ident,
right associativity) :
type_scope.
Notation "'
exists'
x1 x2 x3 x4 x5 x6 x7 ','
P" :=
(
exists x1,
exists x2,
exists x3,
exists x4,
exists x5,
exists x6,
exists x7,
P)
(
at level 200,
x1 ident,
x2 ident,
x3 ident,
x4 ident,
x5 ident,
x6 ident,
x7 ident,
right associativity) :
type_scope.
Notation "'
exists'
x1 x2 x3 x4 x5 x6 x7 x8 ','
P" :=
(
exists x1,
exists x2,
exists x3,
exists x4,
exists x5,
exists x6,
exists x7,
exists x8,
P)
(
at level 200,
x1 ident,
x2 ident,
x3 ident,
x4 ident,
x5 ident,
x6 ident,
x7 ident,
x8 ident,
right associativity) :
type_scope.
Notation "'
exists'
x1 x2 x3 x4 x5 x6 x7 x8 x9 ','
P" :=
(
exists x1,
exists x2,
exists x3,
exists x4,
exists x5,
exists x6,
exists x7,
exists x8,
exists x9,
P)
(
at level 200,
x1 ident,
x2 ident,
x3 ident,
x4 ident,
x5 ident,
x6 ident,
x7 ident,
x8 ident,
x9 ident,
right associativity) :
type_scope.
Notation "'
exists'
x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ','
P" :=
(
exists x1,
exists x2,
exists x3,
exists x4,
exists x5,
exists x6,
exists x7,
exists x8,
exists x9,
exists x10,
P)
(
at level 200,
x1 ident,
x2 ident,
x3 ident,
x4 ident,
x5 ident,
x6 ident,
x7 ident,
x8 ident,
x9 ident,
x10 ident,
right associativity) :
type_scope.
**********************************************************************
* * Tools for programming with Ltac
----------------------------------------------------------------------
* ** Untyped arguments for tactics
* Any Coq value can be boxed into the type Boxer. This is
useful to use Coq computations for implementing tactics.
Inductive Boxer :
Type :=
|
boxer :
forall (
A:
Type),
A ->
Boxer.
----------------------------------------------------------------------
* ** Optional arguments for tactics
* ltac_no_arg is a constant that can be used to simulate
optional arguments in tactic definitions.
Use mytactic ltac_no_arg on the tactic invokation,
and use match arg with ltac_no_arg => .. or
match type of arg with ltac_No_arg => .. to
test whether an argument was provided.
Inductive ltac_No_arg :
Set :=
|
ltac_no_arg :
ltac_No_arg.
----------------------------------------------------------------------
* ** Wildcard arguments for tactics
* ltac_wild is a constant that can be used to simulate
wildcard arguments in tactic definitions. Notation is __.
Inductive ltac_Wild :
Set :=
|
ltac_wild :
ltac_Wild.
Notation "'
__'" :=
ltac_wild :
ltac_scope.
* ltac_wilds is another constant that is typically used to
simulate a sequence of N wildcards, with N chosen
appropriately depending on the context. Notation is ___.
Inductive ltac_Wilds :
Set :=
|
ltac_wilds :
ltac_Wilds.
Notation "'
___'" :=
ltac_wilds :
ltac_scope.
Open Scope ltac_scope.
----------------------------------------------------------------------
* ** Position markers
* ltac_Mark and ltac_mark are dummy definitions used as sentinel
by tactics, to mark a certain position in the context or in the goal.
Inductive ltac_Mark :
Type :=
|
ltac_mark :
ltac_Mark.
* gen_until_mark repeats generalize on hypotheses from the
context, starting from the bottom and stopping as soon as reaching
an hypothesis of type Mark. If fails if Mark does not
appear in the context.
Ltac gen_until_mark :=
match goal with H: ?
T |-
_ =>
match T with
|
ltac_Mark =>
clear H
|
_ =>
generalize H;
clear H;
gen_until_mark
end end.
* intro_until_mark repeats intro until reaching an hypothesis of
type Mark. It throws away the hypothesis Mark.
It fails if Mark does not appear as an hypothesis in the
goal.
Ltac intro_until_mark :=
match goal with
| |- (
ltac_Mark ->
_) =>
intros _
|
_ =>
intro;
intro_until_mark
end.
----------------------------------------------------------------------
* ** List of arguments for tactics
* A datatype of type list Boxer is used to manipulate list of
Coq values in ltac. Notation is >>> v1 v2 ... vN for building
a list containing the values v1 through vN.
Require Import List.
Notation "'>>>'" :=
(@
nil Boxer)
(
at level 0)
:
ltac_scope.
Notation "'>>>'
v1" :=
((
boxer v1)::
nil)
(
at level 0,
v1 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2" :=
((
boxer v1)::(
boxer v2)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2 v3" :=
((
boxer v1)::(
boxer v2)::(
boxer v3)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0,
v3 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2 v3 v4" :=
((
boxer v1)::(
boxer v2)::(
boxer v3)::(
boxer v4)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0,
v3 at level 0,
v4 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2 v3 v4 v5" :=
((
boxer v1)::(
boxer v2)::(
boxer v3)::(
boxer v4)::(
boxer v5)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0,
v3 at level 0,
v4 at level 0,
v5 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2 v3 v4 v5 v6" :=
((
boxer v1)::(
boxer v2)::(
boxer v3)::(
boxer v4)::(
boxer v5)
::(
boxer v6)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0,
v3 at level 0,
v4 at level 0,
v5 at level 0,
v6 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2 v3 v4 v5 v6 v7" :=
((
boxer v1)::(
boxer v2)::(
boxer v3)::(
boxer v4)::(
boxer v5)
::(
boxer v6)::(
boxer v7)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0,
v3 at level 0,
v4 at level 0,
v5 at level 0,
v6 at level 0,
v7 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2 v3 v4 v5 v6 v7 v8" :=
((
boxer v1)::(
boxer v2)::(
boxer v3)::(
boxer v4)::(
boxer v5)
::(
boxer v6)::(
boxer v7)::(
boxer v8)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0,
v3 at level 0,
v4 at level 0,
v5 at level 0,
v6 at level 0,
v7 at level 0,
v8 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2 v3 v4 v5 v6 v7 v8 v9" :=
((
boxer v1)::(
boxer v2)::(
boxer v3)::(
boxer v4)::(
boxer v5)
::(
boxer v6)::(
boxer v7)::(
boxer v8)::(
boxer v9)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0,
v3 at level 0,
v4 at level 0,
v5 at level 0,
v6 at level 0,
v7 at level 0,
v8 at level 0,
v9 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2 v3 v4 v5 v6 v7 v8 v9 v10" :=
((
boxer v1)::(
boxer v2)::(
boxer v3)::(
boxer v4)::(
boxer v5)
::(
boxer v6)::(
boxer v7)::(
boxer v8)::(
boxer v9)::(
boxer v10)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0,
v3 at level 0,
v4 at level 0,
v5 at level 0,
v6 at level 0,
v7 at level 0,
v8 at level 0,
v9 at level 0,
v10 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11" :=
((
boxer v1)::(
boxer v2)::(
boxer v3)::(
boxer v4)::(
boxer v5)
::(
boxer v6)::(
boxer v7)::(
boxer v8)::(
boxer v9)::(
boxer v10)
::(
boxer v11)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0,
v3 at level 0,
v4 at level 0,
v5 at level 0,
v6 at level 0,
v7 at level 0,
v8 at level 0,
v9 at level 0,
v10 at level 0,
v11 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12" :=
((
boxer v1)::(
boxer v2)::(
boxer v3)::(
boxer v4)::(
boxer v5)
::(
boxer v6)::(
boxer v7)::(
boxer v8)::(
boxer v9)::(
boxer v10)
::(
boxer v11)::(
boxer v12)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0,
v3 at level 0,
v4 at level 0,
v5 at level 0,
v6 at level 0,
v7 at level 0,
v8 at level 0,
v9 at level 0,
v10 at level 0,
v11 at level 0,
v12 at level 0)
:
ltac_scope.
Notation "'>>>'
v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13" :=
((
boxer v1)::(
boxer v2)::(
boxer v3)::(
boxer v4)::(
boxer v5)
::(
boxer v6)::(
boxer v7)::(
boxer v8)::(
boxer v9)::(
boxer v10)
::(
boxer v11)::(
boxer v12)::(
boxer v13)::
nil)
(
at level 0,
v1 at level 0,
v2 at level 0,
v3 at level 0,
v4 at level 0,
v5 at level 0,
v6 at level 0,
v7 at level 0,
v8 at level 0,
v9 at level 0,
v10 at level 0,
v11 at level 0,
v12 at level 0,
v13 at level 0)
:
ltac_scope.
----------------------------------------------------------------------
* ** Databases of lemmas
* Use the hint facility to implement a database mapping
terms to terms. To declare a new database, use a definition:
Definition mydatabase := True.
Then, to map mykey to myvalue, write the hint:
Hint Extern 1 (Register mydatabase mykey) => Provide myvalue.
Finally, to query the value associated with a key, run the
tactic ltac_database_get mydatabase mykey. This will leave
at the head of the goal the term myvalue. It can then be
named and exploited using intro.
Definition ltac_database (
D:
Boxer) (
T:
Boxer) (
A:
Boxer) :=
True.
Notation "'
Register'
D T" := (
ltac_database (
boxer D) (
boxer T)
_)
(
at level 69,
D at level 0,
T at level 0).
Lemma ltac_database_provide :
forall (
A:
Boxer) (
D:
Boxer) (
T:
Boxer),
ltac_database D T A.
Proof.
split. Qed.
Ltac Provide T :=
apply (@
ltac_database_provide (
boxer T)).
Ltac ltac_database_get D T :=
let A :=
fresh "
TEMP"
in evar (
A:
Boxer);
let H :=
fresh "
TEMP"
in
assert (
H :
ltac_database (
boxer D) (
boxer T)
A);
[
subst A;
auto
|
subst A;
match type of H with ltac_database _ _ (
boxer ?
L) =>
generalize L end;
clear H ].
----------------------------------------------------------------------
* ** Instantiation modes for tactics
* ltac_inst is a datatype that describes the four instantiation
modes that can be used in tactics specializes, lets,
applys and forwards.
- Args: all arguments are to be provided,
- Hyps: only hypotheses are to be provided
(hypotheses = arguments not used dependently)
- Vars: only variables are to be provided
(variables = arguments used dependently)
- Hnts: the arguments provided are used as hints and are
affected to the first argument of matching type.
Inductive ltac_inst :
Set :=
|
Args :
ltac_inst
|
Hyps :
ltac_inst
|
Vars :
ltac_inst
|
Hnts :
ltac_inst.
* The tactic ltac_args inputs a term E and returns a term
of type "list boxer", according to the following rules:
- if E is already of type "list Boxer", then
- if its head value is an instantiation mode, it returns E;
- otherwise it returns (boxer Hnts)::E, as mode Hnts
is the default mode;
- otherwise, it returns the list (boxer Hnts)::(boxer E)::nil,
describing the fact that there is only one argument provided,
and that the mode is the default mode Hnts.
Ltac ltac_args E :=
match type of E with
|
List.list Boxer =>
match E with
| (@
boxer ltac_inst _)::
_ =>
constr:(
E)
|
_ =>
constr:((
boxer Hnts)::
E)
end
|
_ =>
constr:((
boxer Hnts)::(
boxer E)::
nil)
end.
----------------------------------------------------------------------
* ** Numbers as arguments
* When tactic takes a natural number as argument, it may be
parsed either as a natural number or as a relative number.
In order for tactics to convert their arguments into natural numbers,
we provide a conversion tactic.
The following implementation supports only natural numbers.
Support for relative number is added when importing the file LibInt,
through an overloading of the definition of this tactic.
Ltac nat_from_number N :=
constr:(
N).
* ltac_pattern E at K is the same as pattern E at K except that
K is a Coq natural rather than a Ltac integer. Syntax
ltac_pattern E as K in H is also available.
Tactic Notation "
ltac_pattern"
constr(
E) "
at"
constr(
K) :=
match nat_from_number K with
| 1 =>
pattern E at 1
| 2 =>
pattern E at 2
| 3 =>
pattern E at 3
| 4 =>
pattern E at 4
| 5 =>
pattern E at 5
| 6 =>
pattern E at 6
| 7 =>
pattern E at 7
| 8 =>
pattern E at 8
end.
Tactic Notation "
ltac_pattern"
constr(
E) "
at"
constr(
K) "
in"
hyp(
H) :=
match nat_from_number K with
| 1 =>
pattern E at 1
in H
| 2 =>
pattern E at 2
in H
| 3 =>
pattern E at 3
in H
| 4 =>
pattern E at 4
in H
| 5 =>
pattern E at 5
in H
| 6 =>
pattern E at 6
in H
| 7 =>
pattern E at 7
in H
| 8 =>
pattern E at 8
in H
end.
----------------------------------------------------------------------
* ** Testing tactics
* show tac executes a tactic tac that produces a result,
and then display its result.
Tactic Notation "
show"
tactic(
tac) :=
let R :=
tac in pose R.
* dup N produces N copies of the current goal. It is useful
for building examples on which to illustrate behaviour of tactics.
dup is short for dup 2.
Lemma dup_lemma :
forall P,
P ->
P ->
P.
Proof.
auto. Qed.
Ltac dup_tactic N :=
match nat_from_number N with
| 0 =>
idtac
|
S 0 =>
idtac
|
S ?
N' =>
apply dup_lemma; [ |
dup_tactic N' ]
end.
Tactic Notation "
dup"
constr(
N) :=
dup_tactic N.
Tactic Notation "
dup" :=
dup 2.
----------------------------------------------------------------------
* ** Tagging of hypotheses
* get_last_hyp tt is a function that returns the last hypothesis
at the bottom of the context. It is useful to obtain the default
name associated with the hypothesis, e.g.
intro; let H := get_last_hyp tt in let H' := fresh "P" H in ...
Ltac get_last_hyp tt :=
match goal with H:
_ |-
_ =>
constr:(
H)
end.
----------------------------------------------------------------------
* ** Tagging of hypotheses
* ltac_tag_subst is a specific marker for hypotheses
which is used to tag hypotheses that are equalities to
be substituted.
Definition ltac_tag_subst (
A:
Type) (
x:
A) :=
x.
* ltac_to_generalize is a specific marker for hypotheses
to be generalized.
Definition ltac_to_generalize (
A:
Type) (
x:
A) :=
x.
Ltac gen_to_generalize :=
repeat match goal with
H:
ltac_to_generalize _ |-
_ =>
generalize H;
clear H end.
Ltac mark_to_generalize H :=
let T :=
type of H in
change T with (
ltac_to_generalize T)
in H.
----------------------------------------------------------------------
* ** Deconstructing terms
* get_head E is a tactic that returns the head constant of the
term E, ie, when applied to a term of the form P x1 ... xN
it returns P. If E is not an application, it returns E.
Warning: the tactic seems to loop in some cases when the goal is
a product and one uses the result of this function.
Ltac get_head E :=
match E with
| ?
P _ _ _ _ _ _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ _ =>
constr:(
P)
| ?
P _ _ _ =>
constr:(
P)
| ?
P _ _ =>
constr:(
P)
| ?
P _ =>
constr:(
P)
| ?
P =>
constr:(
P)
end.
----------------------------------------------------------------------
* ** Action at occurence and action not at occurence
* ltac_action_at K of E do Tac isolates the K-th occurence of E in the
goal, setting it in the form P E for some named pattern P,
then calls tactic Tac, and finally unfolds P. Syntax
ltac_action_at K of E in H do Tac is also available.
Tactic Notation "
ltac_action_at"
constr(
K) "
of"
constr(
E) "
do"
tactic(
Tac) :=
let p :=
fresh in ltac_pattern E at K;
match goal with |- ?
P _ =>
set (
p:=
P)
end;
Tac;
unfold p;
clear p.
Tactic Notation "
ltac_action_at"
constr(
K) "
of"
constr(
E) "
in"
hyp(
H) "
do"
tactic(
Tac) :=
let p :=
fresh in ltac_pattern E at K in H;
match type of H with ?
P _ =>
set (
p:=
P)
in H end;
Tac;
unfold p in H;
clear p.
* protects E do Tac temporarily assigns a name to the expression E
so that the execution of tactic Tac will not modify E. This is
useful for instance to restrict the action of simpl.
Tactic Notation "
protects"
constr(
E) "
do"
tactic(
Tac) :=
let x := fresh "TEMP" in sets_eq x: E; T; subst x.
let x :=
fresh "
TEMP"
in let H :=
fresh "
TEMP"
in
set (
X :=
E)
in *;
assert (
H :
X =
E)
by reflexivity;
clearbody X;
Tac;
subst x.
Tactic Notation "
protects"
constr(
E) "
do"
tactic(
Tac) "/" :=
protects E do Tac.
----------------------------------------------------------------------
* ** An alias for eq
* eq' is an alias for eq to be used for equalities in
inductive definitions, so that they don't get mixed with
equalities generated by inversion.
Definition eq' := @
eq.
Hint Unfold eq'.
Notation "
x '=''
y" := (@
eq'
_ x y)
(
at level 70,
arguments at next level).
**********************************************************************
* * Backward and forward chaining
----------------------------------------------------------------------
* ** Application
* rapply is a tactic similar to eapply except that it is
based on the refine tactics, and thus is strictly more
powerful (at least in theory :). In short, it is able to perform
on-the-fly conversions when required for arguments to match,
and it is able to instantiate existentials when required.
Tactic Notation "
rapply"
constr(
t) :=
first
[
eexact (@
t)
|
refine (@
t)
|
refine (@
t _)
|
refine (@
t _ _)
|
refine (@
t _ _ _)
|
refine (@
t _ _ _ _)
|
refine (@
t _ _ _ _ _)
|
refine (@
t _ _ _ _ _ _)
|
refine (@
t _ _ _ _ _ _ _)
|
refine (@
t _ _ _ _ _ _ _ _)
|
refine (@
t _ _ _ _ _ _ _ _ _)
|
refine (@
t _ _ _ _ _ _ _ _ _ _)
|
refine (@
t _ _ _ _ _ _ _ _ _ _ _)
|
refine (@
t _ _ _ _ _ _ _ _ _ _ _ _)
|
refine (@
t _ _ _ _ _ _ _ _ _ _ _ _ _)
|
refine (@
t _ _ _ _ _ _ _ _ _ _ _ _ _ _)
|
refine (@
t _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
].
* The tactics applys_N T, where N is a natural number,
provides a more efficient way of using applys T. It avoids
trying out all possible arities, by specifying explicitely
the arity of function T.
Tactic Notation "
rapply_0"
constr(
t) :=
refine (@
t).
Tactic Notation "
rapply_1"
constr(
t) :=
refine (@
t _).
Tactic Notation "
rapply_2"
constr(
t) :=
refine (@
t _ _).
Tactic Notation "
rapply_3"
constr(
t) :=
refine (@
t _ _ _).
Tactic Notation "
rapply_4"
constr(
t) :=
refine (@
t _ _ _ _).
Tactic Notation "
rapply_5"
constr(
t) :=
refine (@
t _ _ _ _ _).
Tactic Notation "
rapply_6"
constr(
t) :=
refine (@
t _ _ _ _ _ _).
Tactic Notation "
rapply_7"
constr(
t) :=
refine (@
t _ _ _ _ _ _ _).
Tactic Notation "
rapply_8"
constr(
t) :=
refine (@
t _ _ _ _ _ _ _ _).
Tactic Notation "
rapply_9"
constr(
t) :=
refine (@
t _ _ _ _ _ _ _ _ _).
Tactic Notation "
rapply_10"
constr(
t) :=
refine (@
t _ _ _ _ _ _ _ _ _ _).
* lets_base H E adds an hypothesis H : T to the context, where T is
the type of term E. If H is an introduction pattern, it will
destruct H according to the pattern.
Ltac lets_base I E :=
generalize E;
intros I.
* applys_to H E transform the type of hypothesis H by
replacing it by the result of the application of the term
E to H. Intuitively, it is equivalent to lets H: (E H).
Tactic Notation "
applys_to"
hyp(
H)
constr(
E) :=
let H' :=
fresh in rename H into H';
(
first [
lets_base H (
E H')
|
lets_base H (
E _ H')
|
lets_base H (
E _ _ H')
|
lets_base H (
E _ _ _ H')
|
lets_base H (
E _ _ _ _ H')
|
lets_base H (
E _ _ _ _ _ H')
|
lets_base H (
E _ _ _ _ _ _ H')
|
lets_base H (
E _ _ _ _ _ _ _ H')
|
lets_base H (
E _ _ _ _ _ _ _ _ H')
|
lets_base H (
E _ _ _ _ _ _ _ _ _ H') ]
);
clear H'.
* constructors calls constructor or econstructor.
Tactic Notation "
constructors" :=
first [
constructor |
econstructor ];
unfold eq'.
----------------------------------------------------------------------
* ** Assertions
* false_goal replaces any goal by the goal False.
Contrary to the tactic false (below), it does not try to do
anything else
Tactic Notation "
false_goal" :=
elimtype False.
* false_post is the underlying tactic used to prove goals
of the form False. In the default implementation, it proves
the goal if the context contains False or an hypothesis of the
form C x1 .. xN = D y1 .. yM, or if the congruence tactic
finds a proof of x <> x for some x.
Ltac false_post :=
solve [
assumption |
discriminate |
congruence ].
* false replaces any goal by the goal False, and calls false_post
Tactic Notation "
false" :=
false_goal;
try false_post.
* tryfalse tries to solve a goal by contradiction, and leaves
the goal unchanged if it cannot solve it.
It is equivalent to try solve \[ false \].
Tactic Notation "
tryfalse" :=
try solve [
false ].
* tryfalse by tac / is that same as tryfalse except that
it tries to solve the goal using tactic tac if assumption
and discriminate do not apply.
It is equivalent to try solve \[ false; tac \].
Example: tryfalse by congruence/
Tactic Notation "
tryfalse" "
by"
tactic(
tac) "/" :=
try solve [
false;
tac ].
* false T tries false; apply T, or otherwise adds T as
an assumption and calls false.
Tactic Notation "
false"
constr(
T) "
by"
tactic(
tac) "/" :=
false_goal;
first
[
first [
apply T |
eapply T |
rapply T];
tac
|
let H :=
fresh in lets_base H T;
first [
discriminate H
|
false;
tac ] ].
todo: false (>>> H X1 X2)...
Tactic Notation "
false"
constr(
T) :=
false T by idtac/.
* false_invert proves any goal provided there is at least
one hypothesis H in the context that can be proved absurd
by calling inversion H.
Ltac false_invert_tactic :=
match goal with H:
_ |-
_ =>
solve [
inversion H
|
clear H;
false_invert_tactic
|
fail 2 ]
end.
Tactic Notation "
false_invert" :=
false_invert_tactic.
* tryfalse_invert tries to prove the goal using
false or false_invert, and leaves the goal
unchanged if it does not succeed.
Tactic Notation "
tryfalse_invert" :=
try solve [
false |
false_invert ].
* asserts H: T is another syntax for assert (H : T), which
also works with introduction patterns. For instance, one can write:
asserts \[x P\] (exists n, n = 3), or
asserts \[H|H\] (n = 0 \/ n = 1). *)
Tactic Notation "asserts" simple_intropattern(I) ":" constr(T) :=
let H := fresh in assert (H : T);
[ | generalize H; clear H; intros I ].
(** [asserts H1 .. HN: T] is a shorthand for
[asserts \[H1 \[H2 \[.. HN\]\]\]\]: T.
Tactic Notation "
asserts"
simple_intropattern(
I1)
simple_intropattern(
I2) ":"
constr(
T) :=
asserts [
I1 I2]:
T.
Tactic Notation "
asserts"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3) ":"
constr(
T) :=
asserts [
I1 [
I2 I3]]:
T.
Tactic Notation "
asserts"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4) ":"
constr(
T) :=
asserts [
I1 [
I2 [
I3 I4]]]:
T.
Tactic Notation "
asserts"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5) ":"
constr(
T) :=
asserts [
I1 [
I2 [
I3 [
I4 I5]]]]:
T.
Tactic Notation "
asserts"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5)
simple_intropattern(
I6) ":"
constr(
T) :=
asserts [
I1 [
I2 [
I3 [
I4 [
I5 I6]]]]]:
T.
* asserts: T is asserts H: T with H being chosen automatically.
Tactic Notation "
asserts" ":"
constr(
T) :=
let H :=
fresh in asserts H :
T.
* cuts H: T is the same as asserts H: T except that the two subgoals
generated are swapped: the subgoal T comes second. Note that contrary
to cut, it introduces the hypothesis.
Tactic Notation "
cuts"
simple_intropattern(
I) ":"
constr(
T) :=
cut (
T); [
intros I |
idtac ].
* cuts: T is cuts H: T with H being chosen automatically.
Tactic Notation "
cuts" ":"
constr(
T) :=
let H :=
fresh in cuts H:
T.
* cuts H1 .. HN: T is a shorthand for
cuts \[H1 \[H2 \[.. HN\]\]\]\: T].
Tactic Notation "
cuts"
simple_intropattern(
I1)
simple_intropattern(
I2) ":"
constr(
T) :=
cuts [
I1 I2]:
T.
Tactic Notation "
cuts"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3) ":"
constr(
T) :=
cuts [
I1 [
I2 I3]]:
T.
Tactic Notation "
cuts"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4) ":"
constr(
T) :=
cuts [
I1 [
I2 [
I3 I4]]]:
T.
Tactic Notation "
cuts"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5) ":"
constr(
T) :=
cuts [
I1 [
I2 [
I3 [
I4 I5]]]]:
T.
Tactic Notation "
cuts"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5)
simple_intropattern(
I6) ":"
constr(
T) :=
cuts [
I1 [
I2 [
I3 [
I4 [
I5 I6]]]]]:
T.
----------------------------------------------------------------------
* ** Instantiation and forward-chaining
* The instantiation tactics are used to instantiate a lemma E
(whose type is a product) on some arguments. The type of E is
made of implications and universal quantifications, e.g.
forall x, P x -> forall y z, Q x y z -> R z.
The first possibility is to provide arguments in order: first x,
then a proof of P x, then y etc... In this mode, called "Args",
all the arguments are to be provided. If a wildcard is provided
(written __), then an existential variable will be introduced in
place of the argument.
It often saves a lot of time to give only the dependent variables,
(here x, y and z), and have the hypotheses generated as
subgoals. In this "Vars" mode, only variables are to be provided.
For instance, lemma E applied to 3 and 4 is a term
of type forall z, Q 3 4 z -> R z, and P 3 is a new subgoal.
It is possible to use wildcards to introduce existential variables.
However, there are situations where some of the hypotheses already
exists, and it saves time to instantiate the lemma E using the
hypotheses. For instance, suppose F is a term of type P 2.
Then the application of E to F in this "Hyps" mode is a term of type
forall y z, Q 2 y z -> R z. Each wildcard use
will generate an assertion instead, for instance if G has type
Q 2 3 4, then the application of E to a wildcard and to G
in mode-h is a term of type R 4, and P 2 is a new subgoal.
It is very convenient to give some arguments the lemma should be
instantiated on, and let the tactic find out automatically where
underscores should be insterted. The technique is simple: try to
place an argument, and if it does not work insert an underscore.
In this "Hints" mode (Hnts for short), underscore __ would be useless,
since they can be omitted. So, we interpret underscore as follows:
an underscore means that we want to skip the argument that has the
same type as the next real argument provided (real means not an
underscore). If there is no real argument after underscore, then the
the underscore is used for the first possible argument.
There are four modes of instantiation:
- "Args": give all arguments,
- "Vars": give only variables,
- "Hyps": give only hypotheses,
- "Hnts": give some arguments.
The general syntax is tactic (>>>Mode E1 .. EN) where tactic is
the name of the tactic (possibly with some arguments) and Mode
is the name of the mode, and Ei are the arguments.
If Mode is omitted, Hnts will be inserted.
If >>>Mode is omitted, >>>Hnts will be inserted.
Moreover, some tactics accept the syntax tactic E1 .. EN
as short for tactic (>>>Hnts E1 .. EN).
Finally, if the argument EN given is a triple-underscore ___,
then it is equivalent to providing a list of wildcards, with
the appropriate number of wildcards. This means that all
the remaining arguments of the lemma will be instantiated.
Underlying implementation
Ltac app_assert t P cont :=
let H :=
fresh "
TEMP"
in
assert (
H :
P); [ |
cont(
t H);
clear H ].
Ltac app_evar t A cont :=
let x :=
fresh "
TEMP"
in
evar (
x:
A);
let t' :=
constr:(
t x)
in
let t'' := (
eval unfold x in t')
in
subst x;
cont t''.
Ltac app_arg t P v cont :=
let H :=
fresh "
TEMP"
in
assert (
H :
P); [
apply v |
cont(
t H);
try clear H ].
Ltac app_darg t A v cont :=
let x :=
fresh "
TEMP"
in
evar (
x:
A);
instantiate (1:=
v)
in (
Value of x);
let t' :=
constr:(
t x)
in
let t'' := (
eval unfold x in t')
in
subst x;
cont t''.
Ltac build_app_alls t final :=
let rec go t :=
match type of t with
| ?
P -> ?
Q =>
app_assert t P go
|
forall _:?
A,
_ =>
app_evar t A go
|
_ =>
final t
end in
go t.
Ltac build_app_args t vs final :=
let rec go t vs :=
match vs with
|
nil =>
first [
final t |
fail 1 ]
| (
boxer ltac_wilds)::
_ =>
first [
build_app_alls t final |
fail 1 ]
| (
boxer ?
v)::?
vs' =>
let cont t' :=
go t'
vs'
in
let T :=
type of t in
let T :=
eval hnf in T in
match v with
|
ltac_wild =>
match T with
| ?
P -> ?
Q =>
first [
app_assert t P cont |
fail 3 ]
|
forall _:?
A,
_ =>
first [
app_evar t A cont |
fail 3 ]
end
|
_ =>
match T with
| ?
P -> ?
Q =>
first [
app_arg t P v cont |
fail 3 ]
|
forall _:?
A,
_ =>
first [
cont (
t v) |
fail 3 ]
for v8.2 (bug!): first app_darg t A v cont | fail 3
end
end
end in
go t vs.
Ltac build_app_vars t vs final :=
let rec go t vs :=
match vs with
|
nil =>
first [
final t |
fail 1 ]
| (
boxer ltac_wilds)::
_ =>
first [
build_app_alls t final |
fail 1 ]
| (
boxer ?
v)::?
vs' =>
let T :=
type of t in
let T :=
eval hnf in T in
match T with
| ?
P -> ?
Q =>
let cont t' :=
go t'
vs in
first [
app_assert t P cont |
fail 3 ]
|
forall _:?
A,
_ =>
let cont t' :=
go t'
vs'
in
match v with
|
ltac_wild =>
first [
app_evar t A cont |
fail 3 ]
|
_ =>
first [
cont(
t v) |
fail 3 ]
end
end
end in
go t vs.
Ltac build_app_hyps t vs final :=
let rec go t vs :=
match vs with
|
nil =>
first [
final t |
fail 1 ]
| (
boxer ltac_wilds)::
_ =>
first [
build_app_alls t final |
fail 1 ]
| (
boxer ?
v)::?
vs' =>
let T :=
type of t in
let T :=
eval hnf in T in
match T with
| ?
P -> ?
Q =>
let cont t' :=
go t'
vs'
in
match v with
|
ltac_wild =>
first [
app_assert t P cont |
fail 3 ]
|
_ =>
first [
app_arg t P v cont |
fail 3 ]
if mismatch is authorized
first app_arg t P v cont
| let cont' t' := go t' vs in
app_assert t P cont'
end
|
forall _:?
A,
_ =>
let cont t' :=
go t'
vs in
first [
app_evar t A cont |
fail 3 ]
end
end in
go t vs.
todo: support lets: (>>> H ___ ___) to mean that the two head
constants of H should be unfolded
Ltac boxerlist_next_type vs :=
match vs with
|
nil =>
constr:(
ltac_wild)
| (
boxer ltac_wild)::?
vs' =>
boxerlist_next_type vs'
| (
boxer ltac_wilds)::
_ =>
constr:(
ltac_wild)
| (@
boxer ?
T _)::
_ =>
constr:(
T)
end.
Ltac build_app_hnts t vs final :=
let rec go t vs :=
match vs with
|
nil =>
first [
final t |
fail 1 ]
| (
boxer ltac_wilds)::
_ =>
first [
build_app_alls t final |
fail 1 ]
| (
boxer ?
v)::?
vs' =>
let cont t' :=
go t'
vs in
let cont'
t' :=
go t'
vs'
in
let T :=
type of t in
let T :=
eval hnf in T in
match v with
|
ltac_wild =>
first [
let U :=
boxerlist_next_type vs'
in
match U with
|
ltac_wild =>
match T with
| ?
P -> ?
Q =>
first [
app_assert t P cont' |
fail 3 ]
|
forall _:?
A,
_ =>
first [
app_evar t A cont' |
fail 3 ]
end
|
_ =>
match T with
|
U -> ?
Q =>
first [
app_assert t U cont' |
fail 3 ]
|
forall _:
U,
_ =>
first [
app_evar t U cont' |
fail 3 ]
| ?
P -> ?
Q =>
first [
app_assert t P cont |
fail 3 ]
|
forall _:?
A,
_ =>
first [
app_evar t A cont |
fail 3 ]
end
end
|
fail 2 ]
|
_ =>
match T with
| ?
P -> ?
Q =>
first [
app_arg t P v cont'
|
app_assert t P cont
|
fail 3 ]
|
forall _:?
A,
_ =>
first [
cont' (
t v)
|
app_evar t A cont
|
fail 3 ]
end
end
end in
go t vs.
Ltac build_app args final :=
first [
match args with (
boxer ?
mode)::(@
boxer ?
T ?
t)::?
vs =>
let t :=
constr:(
t:
T)
in
match mode with
|
Hnts =>
build_app_hnts t vs final
|
Args =>
build_app_args t vs final
|
Vars =>
build_app_vars t vs final
|
Hyps =>
build_app_hyps t vs final
end
end
|
fail 1 "
Instantiation fails for:"
args].
Ltac unfold_head_until_product T :=
let Hhead := get_head T in
let T' := eval unfold Hhead in T in
match constr:(T,T') with
| (?X,?X) => constr:(T)
| _ => unfold_head_until_product T'
end.
Ltac unfold_head_until_product T :=
eval hnf in T.
Ltac args_unfold_head_if_not_product args :=
match args with (
boxer ?
mode)::(@
boxer ?
T ?
t)::?
vs =>
let T' :=
unfold_head_until_product T in
constr:((
boxer mode)::(@
boxer T'
t)::
vs)
end.
Ltac args_unfold_head_if_not_product_but_params args :=
match args with
| (
boxer ?
mode)::(
boxer ?
t)::(
boxer ?
v)::?
vs =>
args_unfold_head_if_not_product args
|
_ =>
constr:(
args)
end.
* lets H: (>>> Mode E0 E1 .. EN) will instantiate lemma E0
on the arguments Ei (which may be wildcards __),
and name H the resulting term. H may be an introduction
pattern, or a sequence of introduction patterns I1 I2 IN,
or empty.
Syntax lets H: E0 E1 .. EN is available for mode Hnts.
The keyword "ok" may be replaced with "of_vars" or "of_hyps"
for providing only variables or only hypotheses. If the last
argument EN is ___ (triple-underscore), then all
arguments of H will be instantiated.
Ltac lets_build I Ei :=
let args :=
ltac_args Ei in
let args :=
args_unfold_head_if_not_product_but_params args in
let Ei''' := args_unfold_head_if_not_product Ei'' in
build_app args ltac:(
fun R =>
lets_base I R).
Tactic Notation "
lets"
simple_intropattern(
I) ":"
constr(
E) :=
lets_build I E.
Tactic Notation "
lets" ":"
constr(
E) :=
let H :=
fresh in lets H:
E.
Tactic Notation "
lets"
simple_intropattern(
I1)
simple_intropattern(
I2)
":"
constr(
E) :=
lets [
I1 I2]:
E.
Tactic Notation "
lets"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3) ":"
constr(
E) :=
lets [
I1 [
I2 I3]]:
E.
Tactic Notation "
lets"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4) ":"
constr(
E) :=
lets [
I1 [
I2 [
I3 I4]]]:
E.
Tactic Notation "
lets"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5)
":"
constr(
E) :=
lets [
I1 [
I2 [
I3 [
I4 I5]]]]:
E.
Tactic Notation "
lets"
simple_intropattern(
I) ":"
constr(
E0)
constr(
A1) :=
lets I: (>>>
E0 A1).
Tactic Notation "
lets"
simple_intropattern(
I) ":"
constr(
E0)
constr(
A1)
constr(
A2) :=
lets I: (>>>
E0 A1 A2).
Tactic Notation "
lets"
simple_intropattern(
I) ":"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3) :=
lets I: (>>>
E0 A1 A2 A3).
Tactic Notation "
lets"
simple_intropattern(
I) ":"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3)
constr(
A4) :=
lets I: (>>>
E0 A1 A2 A3 A4).
Tactic Notation "
lets"
simple_intropattern(
I) ":"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3)
constr(
A4)
constr(
A5) :=
lets I: (>>>
E0 A1 A2 A3 A4 A5).
Tactic Notation "
lets"
simple_intropattern(
I1)
simple_intropattern(
I2) ":"
constr(
E0)
constr(
A1) :=
lets [
I1 I2]:
E0 A1.
Tactic Notation "
lets"
simple_intropattern(
I1)
simple_intropattern(
I2) ":"
constr(
E0)
constr(
A1)
constr(
A2) :=
lets [
I1 I2]:
E0 A1 A2.
Tactic Notation "
lets"
simple_intropattern(
I1)
simple_intropattern(
I2) ":"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3) :=
lets [
I1 I2]:
E0 A1 A2 A3.
Tactic Notation "
lets"
simple_intropattern(
I1)
simple_intropattern(
I2) ":"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3)
constr(
A4) :=
lets [
I1 I2]:
E0 A1 A2 A3 A4.
Tactic Notation "
lets"
simple_intropattern(
I1)
simple_intropattern(
I2) ":"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3)
constr(
A4)
constr(
A5) :=
lets [
I1 I2]:
E0 A1 A2 A3 A4 A5.
* forwards H: (>>> Mode E0 E1 .. EN) is short for
forwards H: (>>> Mode E0 E1 .. EN ___).
The arguments Ei can be wildcards __ (except E0).
H may be an introduction pattern, or a sequence of
introduction pattern, or empty.
Syntax forwards H: E0 E1 .. EN is available for mode Hnts.
Tactic Notation "
forwards"
simple_intropattern(
I) ":"
constr(
Ei) :=
let args :=
ltac_args Ei in
let args := (
eval simpl in (
args ++ ((
boxer ___)::
nil)))
in
let args :=
args_unfold_head_if_not_product args in
lets I:
args.
Tactic Notation "
forwards" ":"
constr(
E) :=
let H :=
fresh in forwards H:
E.
Tactic Notation "
forwards"
simple_intropattern(
I1)
simple_intropattern(
I2)
":"
constr(
E) :=
forwards [
I1 I2]:
E.
Tactic Notation "
forwards"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3) ":"
constr(
E) :=
forwards [
I1 [
I2 I3]]:
E.
Tactic Notation "
forwards"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4) ":"
constr(
E) :=
forwards [
I1 [
I2 [
I3 I4]]]:
E.
Tactic Notation "
forwards"
simple_intropattern(
I1)
simple_intropattern(
I2)
simple_intropattern(
I3)
simple_intropattern(
I4)
simple_intropattern(
I5)
":"
constr(
E) :=
forwards [
I1 [
I2 [
I3 [
I4 I5]]]]:
E.
Tactic Notation "
forwards"
simple_intropattern(
I) ":"
constr(
E0)
constr(
A1) :=
forwards I: (>>>
E0 A1).
Tactic Notation "
forwards"
simple_intropattern(
I) ":"
constr(
E0)
constr(
A1)
constr(
A2) :=
forwards I: (>>>
E0 A1 A2).
Tactic Notation "
forwards"
simple_intropattern(
I) ":"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3) :=
forwards I: (>>>
E0 A1 A2 A3).
Tactic Notation "
forwards"
simple_intropattern(
I) ":"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3)
constr(
A4) :=
forwards I: (>>>
E0 A1 A2 A3 A4).
Tactic Notation "
forwards"
simple_intropattern(
I) ":"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3)
constr(
A4)
constr(
A5) :=
forwards I: (>>>
E0 A1 A2 A3 A4 A5).
* applys (>>> Mode E0 E1 .. EN) instantiates lemma E0
on the arguments Ei (which may be wildcards __),
and apply the resulting term to the current goal,
using the tactic applys defined earlier on.
applys E0 E1 E2 .. EN is short
for applys (>>>Hnts E0 E1 E2 .. EN).
Ltac applys_build Ei :=
let args :=
ltac_args Ei in
let args :=
args_unfold_head_if_not_product_but_params args in
build_app args ltac:(
fun R =>
first [
apply R |
eapply R |
rapply R ]).
Tactic Notation "
applys"
constr(
E0) :=
match type of E0 with
|
list Boxer =>
applys_build E0
|
_ =>
rapply E0
end.
Tactic Notation "
applys"
constr(
E0)
constr(
A1) :=
applys (>>>
E0 A1).
Tactic Notation "
applys"
constr(
E0)
constr(
A1)
constr(
A2) :=
applys (>>>
E0 A1 A2).
Tactic Notation "
applys"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3) :=
applys (>>>
E0 A1 A2 A3).
Tactic Notation "
applys"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3)
constr(
A4) :=
applys (>>>
E0 A1 A2 A3 A4).
Tactic Notation "
applys"
constr(
E0)
constr(
A1)
constr(
A2)
constr(
A3)
constr(
A4)
constr(
A5) :=
applys (>>>
E0 A1 A2 A3 A4 A5).
* specializes H (>>>Mode E1 E2 .. EN) will instantiate hypothesis H
on the arguments Ei (which may be wildcards __).
The keyword "ok" may be replaced with "of_vars" or "of_hyps"
for providing only variables or only hypotheses. If the last
argument EN is ___ (triple-underscore), then all
arguments of H will be instantiated.
Ltac specializes_build H Ei :=
let H' :=
fresh "
TEMP"
in rename H into H';
let args :=
ltac_args Ei in
match args with (
boxer ?
mode)::?
vs =>
let args :=
constr:((
boxer mode)::(
boxer H')::
vs)
in
let args :=
args_unfold_head_if_not_product args in
build_app args ltac:(
fun R =>
lets H:
R);
clear H'
end.
Tactic Notation "
specializes"
hyp(
H)
constr(
A) :=
specializes_build H A.
Tactic Notation "
specializes"
hyp(
H)
constr(
A1)
constr(
A2) :=
specializes H (>>>
A1 A2).
Tactic Notation "
specializes"
hyp(
H)
constr(
A1)
constr(
A2)
constr(
A3) :=
specializes H (>>>
A1 A2 A3).
Tactic Notation "
specializes"
hyp(
H)
constr(
A1)
constr(
A2)
constr(
A3)
constr(
A4) :=
specializes H (>>>
A1 A2 A3 A4).
Tactic Notation "
specializes"
hyp(
H)
constr(
A1)
constr(
A2)
constr(
A3)
constr(
A4)
constr(
A5) :=
specializes H (>>>
A1 A2 A3 A4 A5).
----------------------------------------------------------------------
* ** Experimental tactics for application
* fapply is a version of apply based on forwards.
Tactic Notation "
fapply"
constr(
E) :=
let H :=
fresh in forwards H:
E;
first [
apply H |
eapply H |
rapply H |
hnf;
apply H
|
hnf;
eapply H |
applys H ].
todo: is applys redundant with rapply ?
* sapply stands for "super apply". It tries
apply, eapply, applys and fapply,
and also tries to head-normalize the goal first.
Tactic Notation "
sapply"
constr(
H) :=
first [
apply H |
eapply H |
rapply H |
applys H
|
hnf;
apply H |
hnf;
eapply H |
hnf;
applys H
|
fapply H ].
----------------------------------------------------------------------
* ** Adding assumptions
* lets_simpl H: E is the same as lets H: E excepts that it
calls simpl on the hypothesis H.
Tactic Notation "
lets_simpl"
ident(
H) ":"
constr(
E) :=
lets H:
E;
simpl in H.
* lets_hnf H: E is the same as lets H: E excepts that it
calls hnf to set the definition in head normal form.
Tactic Notation "
lets_hnf"
ident(
H) ":"
constr(
E) :=
lets H:
E;
hnf in H.
* lets_simpl: E is the same as lets_simpl H: E with
the name H being choosed automatically.
Tactic Notation "
lets_simpl" ":"
constr(
T) :=
let H :=
fresh in lets_simpl H:
T.
* lets_hnf: E is the same as lets_hnf H: E with
the name H being choosed automatically.
Tactic Notation "
lets_hnf" ":"
constr(
T) :=
let H :=
fresh in lets_hnf H:
T.
* put X: E is a synonymous for pose (X := E).
Other syntaxes are put: E.
Tactic Notation "
put"
ident(
X) ":"
constr(
E) :=
pose (
X :=
E).
Tactic Notation "
put" ":"
constr(
E) :=
let X :=
fresh "
X"
in pose (
X :=
E).
----------------------------------------------------------------------
* ** Application of tautologies
*
logic E, where
E is a fact, is equivalent to
assert H:E; [tauto | eapply H; clear H]. It is useful for instance
to prove a conjunction [A /\ B] by showing first [A] and then [A -> B],
through the command [logic (foral A B, A -> (A -> B) -> A /\ B)] *)
Ltac logic_base E cont :=
assert (H:E); [ cont tt | eapply H; clear H ].
Tactic Notation "logic" constr(E) :=
logic_base E ltac:(fun _ => tauto).
(* ---------------------------------------------------------------------- *)
(** ** Application modulo equalities *)
(** The tactic [equates] replaces a goal of the form
[P x y z] with a goal of the form [P x ?a z] and a
subgoal [?a = y]. The introduction of the evar [?a] makes
it possible to apply lemmas that would not apply to the
original goal, for example a lemma of the form
[forall n m, P n n m], because [x] and [y] might be equal
but not convertible.
Usage is [equates i1 ... ik], where the indices are the
positions of the arguments to be replaced by evars,
counting from the right-hand side. *)
Section equatesLemma.
Variables
(A0 A1 : Type)
(A2 : forall (x1 : A1), Type)
(A3 : forall (x1 : A1) (x2 : A2 x1), Type)
(A4 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2), Type)
(A5 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2) (x4 : A4 x3), Type)
(A6 : forall (x1 : A1) (x2 : A2 x1) (x3 : A3 x2) (x4 : A4 x3) (x5 : A5 x4), Type).
Lemma equates_0 : forall (P Q:Prop),
P -> P = Q -> Q.
Proof. intros. subst. auto. Qed.
Lemma equates_1 :
forall (P:A0->Prop) x1 y1,
P y1 -> x1 = y1 -> P x1.
Proof. intros. subst. auto. Qed.
Lemma equates_2 :
forall y1 (P:A0->forall(x1:A1),Prop) x1 x2,
P y1 x2 -> x1 = y1 -> P x1 x2.
Proof. intros. subst. auto. Qed.
Lemma equates_3 :
forall y1 (P:A0->forall(x1:A1)(x2:A2 x1),Prop) x1 x2 x3,
P y1 x2 x3 -> x1 = y1 -> P x1 x2 x3.
Proof. intros. subst. auto. Qed.
Lemma equates_4 :
forall y1 (P:A0->forall(x1:A1)(x2:A2 x1)(x3:A3 x2),Prop) x1 x2 x3 x4,
P y1 x2 x3 x4 -> x1 = y1 -> P x1 x2 x3 x4.
Proof. intros. subst. auto. Qed.
Lemma equates_5 :
forall y1 (P:A0->forall(x1:A1)(x2:A2 x1)(x3:A3 x2)(x4:A4 x3),Prop) x1 x2 x3 x4 x5,
P y1 x2 x3 x4 x5 -> x1 = y1 -> P x1 x2 x3 x4 x5.
Proof. intros. subst. auto. Qed.
Lemma equates_6 :
forall y1 (P:A0->forall(x1:A1)(x2:A2 x1)(x3:A3 x2)(x4:A4 x3)(x5:A5 x4),Prop)
x1 x2 x3 x4 x5 x6,
P y1 x2 x3 x4 x5 x6 -> x1 = y1 -> P x1 x2 x3 x4 x5 x6.
Proof. intros. subst. auto. Qed.
End equatesLemma.
Ltac equates_lemma n :=
match nat_from_number n with
| 0 => constr:(equates_0)
| 1 => constr:(equates_1)
| 2 => constr:(equates_2)
| 3 => constr:(equates_3)
| 4 => constr:(equates_4)
| 5 => constr:(equates_5)
| 6 => constr:(equates_6)
end.
Ltac equates_one n :=
let L := equates_lemma n in
eapply L.
Ltac equates_several E cont :=
let all_pos := match type of E with
| List.list Boxer => constr:(E)
| _ => constr:((boxer E)::nil)
end in
let rec go pos :=
match pos with
| nil => cont tt
| (boxer ?n)::?pos' => equates_one n; [ instantiate; go pos' | ]
end in
go all_pos.
Tactic Notation "equates" constr(E) :=
equates_several E ltac:(fun _ => idtac).
Tactic Notation "equates" constr(n1) constr(n2) :=
equates (>>> n1 n2).
Tactic Notation "equates" constr(n1) constr(n2) constr(n3) :=
equates (>>> n1 n2 n3).
Tactic Notation "equates" constr(n1) constr(n2) constr(n3) constr(n4) :=
equates (>>> n1 n2 n3 n4).
(** [applys_eq H i1 .. iK] is the same as
[equates i1 .. iK] followed by [apply H]
on the first subgoal. *)
Tactic Notation "applys_eq" constr(H) constr(E) :=
equates_several E ltac:(fun _ => sapply H).
Tactic Notation "applys_eq" constr(H) constr(n1) constr(n2) :=
applys_eq H (>>> n1 n2).
Tactic Notation "applys_eq" constr(H) constr(n1) constr(n2) constr(n3) :=
applys_eq H (>>> n1 n2 n3).
Tactic Notation "applys_eq" constr(H) constr(n1) constr(n2) constr(n3) constr(n4) :=
applys_eq H (>>> n1 n2 n3 n4).
(* ********************************************************************** *)
(** * Introduction and generalization *)
(* ---------------------------------------------------------------------- *)
(** ** Introduction *)
(** [introv] iterates [intro] on all universally-quantified "variables"
at the head of the goal. More precisely, it introduces only the
dependently-used variables. For example, [introv] applied
to the goal [forall x y, P x -> Q] introduces [x] and [y] but not
the hypothesis [P x]. If the goal is a definition, then it will
unfold this definition.
[introv H1 .. HN] calls [introv] then introduces an hypothesis as [H1],
then call [introv] again and introduces an hypothesis as [H2],
and so on. It provides a convenient way of introducing all the arguments
of a theorem and name only the non-dependent hypotheses.
Note that [introv] without arguments will unfold the head constant
if the goal is not a product. *)
Ltac introv_rec :=
match goal with
| |- (ltac_tag_subst (?x = ?y) -> ?Q) =>
let H := fresh "Aux" in
intro H; unfold ltac_tag_subst in H;
try subst x; introv_rec
| |- ?P -> ?Q => idtac
| |- forall _, _ => intro; introv_rec
| |- _ => idtac
end.
Ltac introv_to :=
match goal with
| |- (ltac_tag_subst (?x = ?y) -> ?Q) =>
let H := fresh "Aux" in
intro H; unfold ltac_tag_subst in H;
try subst x; introv_to
| |- ?P -> ?Q => idtac
| |- forall _, _ => intro; introv_to
| |- ?G => let P := get_head G in progress (unfold P); introv_to
end.
Ltac introv_base :=
match goal with
| |- forall _, _ => introv_rec
| |- ?G => let P := get_head G in unfold P; introv_rec
end.
Tactic Notation "introv" :=
introv_base.
Tactic Notation "introv" simple_intropattern(I) :=
introv_to; intros I.
Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2) :=
introv_to; intros I1; introv_to; intros I2.
Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) :=
introv; intros I1; introv; intros I2; introv; intros I3.
Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) simple_intropattern(I4) :=
introv; intros I1; introv; intros I2; introv; intros I3;
introv; intros I4.
Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) :=
introv; intros I1; introv; intros I2; introv; intros I3;
introv; intros I4; introv; intros I5.
Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
simple_intropattern(I6) :=
introv; intros I1; introv; intros I2; introv; intros I3;
introv; intros I4; introv; intros I5; introv; intros I6.
Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
simple_intropattern(I6) simple_intropattern(I7) :=
introv; intros I1; introv; intros I2; introv; intros I3;
introv; intros I4; introv; intros I5; introv; intros I6;
introv; intros I7.
Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) :=
introv; intros I1; introv; intros I2; introv; intros I3;
introv; intros I4; introv; intros I5; introv; intros I6;
introv; intros I7; introv; intros I8.
Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8)
simple_intropattern(I9) :=
introv; intros I1; introv; intros I2; introv; intros I3;
introv; intros I4; introv; intros I5; introv; intros I6;
introv; intros I7; introv; intros I8; introv; intros I9.
Tactic Notation "introv" simple_intropattern(I1) simple_intropattern(I2)
simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8)
simple_intropattern(I9) simple_intropattern(I10) :=
introv; intros I1; introv; intros I2; introv; intros I3;
introv; intros I4; introv; intros I5; introv; intros I6;
introv; intros I7; introv; intros I8; introv; intros I9;
introv; intros I10.
(** [intros_all] repeats [intro] as long as possible. Contrary to [intros],
it unfolds any definition on the way. Remark that it also unfolds the
definition of negation, so applying [introz] to a goal of the form
[forall x, P x -> ~Q] will introduce [x] and [P x] and [Q], and will
leave [False] in the goal. *)
Tactic Notation "intros_all" :=
repeat intro.
(* ---------------------------------------------------------------------- *)
(** ** Generalization *)
(** [gen X1 .. XN] is a shorthand for calling [generalize dependent]
successively on variables [XN]...[X1]. Note that the variables
are generalized in reverse order, following the convention of
the [generalize] tactic: it means that [X1] will be the first
quantified variable in the resulting goal. *)
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.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5)
ident(X6) :=
gen X6; gen X5; gen X4; gen X3; gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5)
ident(X6) ident(X7) :=
gen X7; gen X6; gen X5; gen X4; gen X3; gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5)
ident(X6) ident(X7) ident(X8) :=
gen X8; gen X7; gen X6; gen X5; gen X4; gen X3; gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5)
ident(X6) ident(X7) ident(X8) ident(X9) :=
gen X9; gen X8; gen X7; gen X6; gen X5; gen X4; gen X3; gen X2; gen X1.
Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5)
ident(X6) ident(X7) ident(X8) ident(X9) ident(X10) :=
gen X10; gen X9; gen X8; gen X7; gen X6; gen X5; gen X4; gen X3; gen X2; gen X1.
(** [generalizes X] is a shorthand for calling [generalize X; clear X].
It is weaker than tactic [gen X] since it does not support
dependencies. It is mainly intended for writing tactics. *)
Tactic Notation "generalizes" hyp(X) :=
generalize X; clear X.
(* ---------------------------------------------------------------------- *)
(** ** Naming *)
(** [sets X: E] is the same as [set (X := E) in *], that is,
it replaces all occurences of [E] by a fresh meta-variable [X]
whose definition is [E]. *)
Tactic Notation "sets" ident(X) ":" constr(E) :=
set (X := E) in *.
(** [def_to_eq E X H] applies when [X := E] is a local
definition. It adds an assumption [H: X = E]
and then clears the definition of [X].
[def_to_eq_sym] is similar except that it generates
the equality [H: E = X]. *)
Ltac def_to_eq X HX E :=
assert (HX : X = E) by reflexivity; clearbody X.
Ltac def_to_eq_sym X HX E :=
assert (HX : E = X) by reflexivity; clearbody X.
(** [set_eq X H: E] generates the equality [H: X = E],
for a fresh name [X], and replaces [E] by [X] in the
current goal. Syntaxes [set_eq X: E] and
[set_eq: E] are also available. Similarly,
[set_eq <- X H: E] generates the equality [H: E = X].
[sets_eq X HX: E] does the same but replaces [E] by [X]
everywhere in the goal. [sets_eq X HX: E in H] replaces in [H].
[set_eq X HX: E in |-] performs no substitution at all. *)
Tactic Notation "set_eq" ident(X) ident(HX) ":" constr(E) :=
set (X := E); def_to_eq X HX E.
Tactic Notation "set_eq" ident(X) ":" constr(E) :=
let HX := fresh "EQ" X in set_eq X HX: E.
Tactic Notation "set_eq" ":" constr(E) :=
let X := fresh "X" in set_eq X: E.
Tactic Notation "set_eq" "<-" ident(X) ident(HX) ":" constr(E) :=
set (X := E); def_to_eq_sym X HX E.
Tactic Notation "set_eq" "<-" ident(X) ":" constr(E) :=
let HX := fresh "EQ" X in set_eq <- X HX: E.
Tactic Notation "set_eq" "<-" ":" constr(E) :=
let X := fresh "X" in set_eq <- X: E.
Tactic Notation "sets_eq" ident(X) ident(HX) ":" constr(E) :=
set (X := E) in *; def_to_eq X HX E.
Tactic Notation "sets_eq" ident(X) ":" constr(E) :=
let HX := fresh "EQ" X in sets_eq X HX: E.
Tactic Notation "sets_eq" ":" constr(E) :=
let X := fresh "X" in sets_eq X: E.
Tactic Notation "sets_eq" "<-" ident(X) ident(HX) ":" constr(E) :=
set (X := E) in *; def_to_eq_sym X HX E.
Tactic Notation "sets_eq" "<-" ident(X) ":" constr(E) :=
let HX := fresh "EQ" X in sets_eq <- X HX: E.
Tactic Notation "sets_eq" "<-" ":" constr(E) :=
let X := fresh "X" in sets_eq <- X: E.
Tactic Notation "set_eq" ident(X) ident(HX) ":" constr(E) "in" hyp(H) :=
set (X := E) in H; def_to_eq X HX E.
Tactic Notation "set_eq" ident(X) ":" constr(E) "in" hyp(H) :=
let HX := fresh "EQ" X in set_eq X HX: E in H.
Tactic Notation "set_eq" ":" constr(E) "in" hyp(H) :=
let X := fresh "X" in set_eq X: E in H.
Tactic Notation "set_eq" "<-" ident(X) ident(HX) ":" constr(E) "in" hyp(H) :=
set (X := E) in H; def_to_eq_sym X HX E.
Tactic Notation "set_eq" "<-" ident(X) ":" constr(E) "in" hyp(H) :=
let HX := fresh "EQ" X in set_eq <- X HX: E in H.
Tactic Notation "set_eq" "<-" ":" constr(E) "in" hyp(H) :=
let X := fresh "X" in set_eq <- X: E in H.
Tactic Notation "set_eq" ident(X) ident(HX) ":" constr(E) "in" "|-" :=
set (X := E) in |-; def_to_eq X HX E.
Tactic Notation "set_eq" ident(X) ":" constr(E) "in" "|-" :=
let HX := fresh "EQ" X in set_eq X HX: E in |-.
Tactic Notation "set_eq" ":" constr(E) "in" "|-" :=
let X := fresh "X" in set_eq X: E in |-.
Tactic Notation "set_eq" "<-" ident(X) ident(HX) ":" constr(E) "in" "|-" :=
set (X := E) in |-; def_to_eq_sym X HX E.
Tactic Notation "set_eq" "<-" ident(X) ":" constr(E) "in" "|-" :=
let HX := fresh "EQ" X in set_eq <- X HX: E in |-.
Tactic Notation "set_eq" "<-" ":" constr(E) "in" "|-" :=
let X := fresh "X" in set_eq <- X: E in |-.
(** [gen_eq X: E] is a tactic whose purpose is to introduce
equalities so as to work around the limitation of the [induction]
tactic which typically loses information. [gen_eq E as X] replaces
all occurences of term [E] with a fresh variable [X] and the equality
[X = E] as extra hypothesis to the current conclusion. In other words
a conclusion [C] will be turned into [(X = E) -> C].
[gen_eq: E] and [gen_eq: E as X] are also accepted. *)
Tactic Notation "gen_eq" ident(X) ":" constr(E) :=
let EQ := fresh in sets_eq X EQ: E; revert EQ.
Tactic Notation "gen_eq" ":" constr(E) :=
let X := fresh "X" in gen_eq X: E.
Tactic Notation "gen_eq" ":" constr(E) "as" ident(X) :=
gen_eq X: E.
Tactic Notation "gen_eq" ident(X1) ":" constr(E1) ","
ident(X2) ":" constr(E2) :=
gen_eq X2: E2; gen_eq X1: E1.
Tactic Notation "gen_eq" ident(X1) ":" constr(E1) ","
ident(X2) ":" constr(E2) "," ident(X3) ":" constr(E3) :=
gen_eq X3: E3; gen_eq X2: E2; gen_eq X1: E1.
(** [sets_let X] finds the first let-expression in the goal
and names its body [X]. [sets_eq_let X] is similar,
except that it generates an explicit equality.
Tactics [sets_let X in H] and [sets_eq_let X in H]
allow specifying a particular hypothesis (by default,
the first one that contains a [let] is considered).
Known limitation: it does not seem possible to support
naming of multiple let-in constructs inside a term, from ltac. *)
Ltac sets_let_base tac :=
match goal with
| |- context[let _ := ?E in _] => tac E; cbv zeta
| H: context[let _ := ?E in _] |- _ => tac E; cbv zeta in H
end.
Ltac sets_let_in_base H tac :=
match type of H with context[let _ := ?E in _] =>
tac E; cbv zeta in H end.
Tactic Notation "sets_let" ident(X) :=
sets_let_base ltac:(fun E => sets X: E).
Tactic Notation "sets_let" ident(X) "in" hyp(H) :=
sets_let_in_base H ltac:(fun E => sets X: E).
Tactic Notation "sets_eq_let" ident(X) :=
sets_let_base ltac:(fun E => sets_eq X: E).
Tactic Notation "sets_eq_let" ident(X) "in" hyp(H) :=
sets_let_in_base H ltac:(fun E => sets_eq X: E).
(* ********************************************************************** *)
(** * Rewriting *)
(* ---------------------------------------------------------------------- *)
(** ** Rewriting *)
(** [rewrite_all E] iterates version of [rewrite E] as long as possible.
Warning: this tactic can easily get into an infinite loop.
Syntax for rewriting from right to left and/or into an hypothese
is similar to the one of [rewrite]. *)
Tactic Notation "rewrite_all" constr(E) :=
repeat rewrite E.
Tactic Notation "rewrite_all" "<-" constr(E) :=
repeat rewrite <- E.
Tactic Notation "rewrite_all" constr(E) "in" ident(H) :=
repeat rewrite E in H.
Tactic Notation "rewrite_all" "<-" constr(E) "in" ident(H) :=
repeat rewrite <- E in H.
Tactic Notation "rewrite_all" constr(E) "in" "*" :=
repeat rewrite E in *.
Tactic Notation "rewrite_all" "<-" constr(E) "in" "*" :=
repeat rewrite <- E in *.
(** [asserts_rewrite E] asserts that an equality [E] holds (generating a
corresponding subgoal) and rewrite it straight away in the current
goal. It avoids giving a name to the equality and later clearing it.
Syntax for rewriting from right to left and/or into an hypothese
is similar to the one of [rewrite]. Note: the tactic [replaces]
plays a similar role. *)
Ltac asserts_rewrite_tactic E action :=
let EQ := fresh in (assert (EQ : E);
[ idtac | action EQ; clear EQ ]).
Tactic Notation "asserts_rewrite" constr(E) :=
asserts_rewrite_tactic E ltac:(fun EQ => rewrite EQ).
Tactic Notation "asserts_rewrite" "<-" constr(E) :=
asserts_rewrite_tactic E ltac:(fun EQ => rewrite <- EQ).
Tactic Notation "asserts_rewrite" constr(E) "in" hyp(H) :=
asserts_rewrite_tactic E ltac:(fun EQ => rewrite EQ in H).
Tactic Notation "asserts_rewrite" "<-" constr(E) "in" hyp(H) :=
asserts_rewrite_tactic E ltac:(fun EQ => rewrite <- EQ in H).
(** [cuts_rewrite E] is the same as [asserts_rewrite E] except
that subgoals are permuted. *)
Ltac cuts_rewrite_tactic E action :=
let EQ := fresh in (cuts EQ: E;
[ action EQ; clear EQ | idtac ]).
Tactic Notation "cuts_rewrite" constr(E) :=
cuts_rewrite_tactic E ltac:(fun EQ => rewrite EQ).
Tactic Notation "cuts_rewrite" "<-" constr(E) :=
cuts_rewrite_tactic E ltac:(fun EQ => rewrite <- EQ).
Tactic Notation "cuts_rewrite" constr(E) "in" hyp(H) :=
cuts_rewrite_tactic E ltac:(fun EQ => rewrite EQ in H).
Tactic Notation "cuts_rewrite" "<-" constr(E) "in" hyp(H) :=
cuts_rewrite_tactic E ltac:(fun EQ => rewrite <- EQ in H).
(** [rewrite_except H EQ] rewrites equality [EQ] everywhere
but in hypothesis [H]. *)
Ltac rewrite_except H EQ :=
let K := fresh in let T := type of H in
set (K := T) in H;
rewrite EQ in *; unfold K in H; clear K.
(** [rewrites E at K] applies when [E] is of the form [T1 = T2]
rewrites the equality [E] at the [K]-th occurence of [T1]
in the current goal.
Syntaxes [rewrites <- E at K] and [rewrites E at K in H]
are also available. *)
Tactic Notation "rewrites" constr(E) "at" constr(K) :=
match type of E with ?T1 = ?T2 =>
ltac_action_at K of T1 do (rewrite E) end.
Tactic Notation "rewrites" "<-" constr(E) "at" constr(K) :=
match type of E with ?T1 = ?T2 =>
ltac_action_at K of T2 do (rewrite <- E) end.
Tactic Notation "rewrites" constr(E) "at" constr(K) "in" hyp(H) :=
match type of E with ?T1 = ?T2 =>
ltac_action_at K of T1 in H do (rewrite E in H) end.
Tactic Notation "rewrites" "<-" constr(E) "at" constr(K) "in" hyp(H) :=
match type of E with ?T1 = ?T2 =>
ltac_action_at K of T2 in H do (rewrite <- E in H) end.
(* ---------------------------------------------------------------------- *)
(** ** Replace *)
(** [replaces E with F] is the same as [replace E with F] except that
the equality [E = F] is generated as first subgoal. Syntax
[replaces E with F in H] is also available. Note that contrary to
[replace], [replaces] does not try to solve the equality
by [assumption]. Note: [replaces E with F] is similar to
[asserts_rewrite (E = F)]. *)
Tactic Notation "replaces" constr(E) "with" constr(F) :=
let T := fresh in assert (T: E = F); [ | replace E with F; clear T ].
Tactic Notation "replaces" constr(E) "with" constr(F) "in" hyp(H) :=
let T := fresh in assert (T: E = F); [ | replace E with F in H; clear T ].
(** [replaces E at K with F] replaces the [K]-th occurence of [E]
with [F] in the current goal. Syntax [replaces E at K with F in H]
is also available. *)
Tactic Notation "replaces" constr(E) "at" constr(K) "with" constr(F) :=
let T := fresh in assert (T: E = F); [ | rewrites T at K; clear T ].
Tactic Notation "replaces" constr(E) "at" constr(K) "with" constr(F) "in" hyp(H) :=
let T := fresh in assert (T: E = F); [ | rewrites T at K in H; clear T ].
(* ---------------------------------------------------------------------- *)
(** ** Renaming *)
(** [renames X1 to Y1, ..., XN to YN] is a shorthand for a sequence of
renaming operations [rename Xi into Yi]. *)
Tactic Notation "renames" ident(X1) "to" ident(Y1) :=
rename X1 into Y1.
Tactic Notation "renames" ident(X1) "to" ident(Y1) ","
ident(X2) "to" ident(Y2) :=
renames X1 to Y1; renames X2 to Y2.
Tactic Notation "renames" ident(X1) "to" ident(Y1) ","
ident(X2) "to" ident(Y2) "," ident(X3) "to" ident(Y3) :=
renames X1 to Y1; renames X2 to Y2, X3 to Y3.
Tactic Notation "renames" ident(X1) "to" ident(Y1) ","
ident(X2) "to" ident(Y2) "," ident(X3) "to" ident(Y3) ","
ident(X4) "to" ident(Y4) :=
renames X1 to Y1; renames X2 to Y2, X3 to Y3, X4 to Y4.
Tactic Notation "renames" ident(X1) "to" ident(Y1) ","
ident(X2) "to" ident(Y2) "," ident(X3) "to" ident(Y3) ","
ident(X4) "to" ident(Y4) "," ident(X5) "to" ident(Y5) :=
renames X1 to Y1; renames X2 to Y2, X3 to Y3, X4 to Y4, X5 to Y5.
Tactic Notation "renames" ident(X1) "to" ident(Y1) ","
ident(X2) "to" ident(Y2) "," ident(X3) "to" ident(Y3) ","
ident(X4) "to" ident(Y4) "," ident(X5) "to" ident(Y5) ","
ident(X6) "to" ident(Y6) :=
renames X1 to Y1; renames X2 to Y2, X3 to Y3, X4 to Y4, X5 to Y5, X6 to Y6.
(* ---------------------------------------------------------------------- *)
(** ** Unfolding *)
(** [unfolds] unfolds the head definition in the goal, i.e. if the
goal has form [P x1 ... xN] then it calls [unfold P].
If the goal is an equality, it tries to unfold the head constant
on the left-hand side, and otherwise tries on the right-hand side.
If the goal is a product, it calls [intros] first. *)
Ltac apply_to_head_of E cont :=
let go E :=
let P := get_head E in cont P in
match E with
| forall _,_ => intros; apply_to_head_of E cont
| ?A = ?B => first [ go A | go B ]
| ?A => go A
end.
Ltac unfolds_base :=
match goal with |- ?G =>
apply_to_head_of G ltac:(fun P => unfold P) end.
Tactic Notation "unfolds" :=
unfolds_base.
(** [unfolds in H] unfolds the head definition of hypothesis [H], i.e. if
[H] has type [P x1 ... xN] then it calls [unfold P in H]. *)
Ltac unfolds_in_base H :=
match type of H with ?G =>
apply_to_head_of G ltac:(fun P => unfold P in H) end.
Tactic Notation "unfolds" "in" hyp(H) :=
unfolds_in_base H.
(** [unfolds P1,..,PN] is a shortcut for [unfold P1,..,PN in *]. *)
Tactic Notation "unfolds" reference(F1) :=
unfold F1 in *.
Tactic Notation "unfolds" reference(F1) "," reference(F2) :=
unfold F1,F2 in *.
Tactic Notation "unfolds" reference(F1) "," reference(F2)
"," reference(F3) :=
unfold F1,F2,F3 in *.
Tactic Notation "unfolds" reference(F1) "," reference(F2)
"," reference(F3) "," reference(F4) :=
unfold F1,F2,F3,F4 in *.
Tactic Notation "unfolds" reference(F1) "," reference(F2)
"," reference(F3) "," reference(F4) "," reference(F5) :=
unfold F1,F2,F3,F4,F5 in *.
Tactic Notation "unfolds" reference(F1) "," reference(F2)
"," reference(F3) "," reference(F4) "," reference(F5) "," reference(F6) :=
unfold F1,F2,F3,F4,F5,F6 in *.
Tactic Notation "unfolds" reference(F1) "," reference(F2)
"," reference(F3) "," reference(F4) "," reference(F5)
"," reference(F6) "," reference(F7) :=
unfold F1,F2,F3,F4,F5,F6,F7 in *.
Tactic Notation "unfolds" reference(F1) "," reference(F2)
"," reference(F3) "," reference(F4) "," reference(F5)
"," reference(F6) "," reference(F7) "," reference(F8) :=
unfold F1,F2,F3,F4,F5,F6,F7,F8 in *.
(** [folds P1,..,PN] is a shortcut for [fold P1 in *; ..; fold PN 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.
Tactic Notation "folds" constr(H1) "," constr(H2) "," constr(H3)
"," constr(H4) :=
folds H1; folds H2; folds H3; folds H4.
Tactic Notation "folds" constr(H1) "," constr(H2) "," constr(H3)
"," constr(H4) "," constr(H5) :=
folds H1; folds H2; folds H3; folds H4; folds H5.
(* ---------------------------------------------------------------------- *)
(** ** Simplification *)
(** [simpls] is a shortcut for [simpl in *]. *)
Tactic Notation "simpls" :=
simpl in *.
(** [simpls P1,..,PN] is a shortcut for
[simpl P1 in *; ..; simpl PN in *]. *)
Tactic Notation "simpls" reference(F1) :=
simpl F1 in *.
Tactic Notation "simpls" reference(F1) "," reference(F2) :=
simpls F1; simpls F2.
Tactic Notation "simpls" reference(F1) "," reference(F2)
"," reference(F3) :=
simpls F1; simpls F2; simpls F3.
Tactic Notation "simpls" reference(F1) "," reference(F2)
"," reference(F3) "," reference(F4) :=
simpls F1; simpls F2; simpls F3; simpls F4.
(** [unsimpl E] replaces all occurence of [X] by [E], where [X] is
the result which the tactic [simpl] would give when applied to [E].
It is useful to undo what [simpl] has simplified too far. *)
Tactic Notation "unsimpl" constr(E) :=
let F := (eval simpl in E) in change F with E.
(** [unsimpl E in H] is similar to [unsimpl E] but it applies
inside a particular hypothesis [H]. *)
Tactic Notation "unsimpl" constr(E) "in" hyp(H) :=
let F := (eval simpl in E) in change F with E in H.
(** [unsimpl E in *] applies [unsimpl E] everywhere possible.
[unsimpls E] is a synonymous. *)
Tactic Notation "unsimpl" constr(E) "in" "*" :=
let F := (eval simpl in E) in change F with E in *.
Tactic Notation "unsimpls" constr(E) :=
unsimpl E in *.
(** [nosimpl t] protects the Coq term[t] against some forms of
simplification. See Gonthier's work for details on this trick. *)
Notation "'nosimpl' t" := (match tt with tt => t end)
(at level 10).
(* ---------------------------------------------------------------------- *)
(** ** Evaluation *)
Tactic Notation "hnfs" := hnf in *.
(* ---------------------------------------------------------------------- *)
(** ** Substitution *)
(** [substs] does the same as [subst], except that it does not fail
when there are circular equalities in the context. *)
Tactic Notation "substs" :=
repeat (match goal with H: ?x = ?y |- _ =>
first [ subst x | subst y ] end).
(** Implementation of [substs below], which allows to call
[subst] on all the hypotheses that lie beyond a given
position in the proof context. *)
Ltac substs_below limit :=
match goal with H: ?T |- _ =>
match T with
| limit => idtac
| ?x = ?y =>
first [ subst x; substs_below limit
| subst y; substs_below limit
| generalizes H; substs_below limit; intro ]
end end.
(** [substs below body E] applies [subst] on all equalities that appear
in the context below the first hypothesis whose body is [E].
If there is no such hypothesis in the context, it is equivalent
to [subst]. For instance, if [H] is an hypothesis, then
[substs below H] will substitute equalities below hypothesis [H]. *)
Tactic Notation "substs" "below" "body" constr(M) :=
substs_below M.
(** [substs below H] applies [subst] on all equalities that appear
in the context below the hypothesis named [H]. Note that
the current implementation is technically incorrect since it
will confuse different hypotheses with the same body. *)
Tactic Notation "substs" "below" hyp(H) :=
match type of H with ?M => substs below body M end.
(** [subst_hyp H] substitutes the equality contained in [H].
The behaviour is extended in LibData --TODO *)
Ltac subst_hyp_base H :=
match type of H with
| ?x = ?y => first [ subst x | subst y ]
end.
Tactic Notation "subst_hyp" hyp(H) := subst_hyp_base H.
(** [subst_local] substitutes all local definition from the context *)
Ltac subst_local :=
repeat match goal with H:=_ |- _ => subst H end.
(** [subst_term E] takes an equality [x = t] and replace [x]
with [t] everywhere in the goal *)
Ltac subst_term_base E :=
let H := fresh "TEMP" in lets H: E; subst_hyp H.
Tactic Notation "subst_term" constr(E) :=
subst_term_base E.
(* ---------------------------------------------------------------------- *)
(** ** Tactics to work with proof irrelevance *)
Require Import ProofIrrelevance.
(** [pi_rewrite E] replaces [E] of type [Prop] with a fresh
unification variable, and is thus a practical way to
exploit proof irrelevance, without writing explicitly
[rewrite (proof_irrelevance E E')]. Particularly useful
when [E'] is a big expression. *)
Ltac pi_rewrite_base E rewrite_tac :=
let E' := fresh in let T := type of E in evar (E':T);
rewrite_tac (@proof_irrelevance _ E E'); subst E'.
Tactic Notation "pi_rewrite" constr(E) :=
pi_rewrite_base E ltac:(fun X => rewrite X).
Tactic Notation "pi_rewrite" constr(E) "in" hyp(H) :=
pi_rewrite_base E ltac:(fun X => rewrite X in H).
(* ---------------------------------------------------------------------- *)
(** ** Proving equalities *)
(** [fequal] is a variation on [f_equal] which has a better behaviour
on equalities between n-ary tuples. *)
Ltac fequal_base :=
let go := f_equal; [ fequal_base | ] in
match goal with
| |- (_,_,_) = (_,_,_) => go
| |- (_,_,_,_) = (_,_,_,_) => go
| |- (_,_,_,_,_) = (_,_,_,_,_) => go
| |- (_,_,_,_,_,_) = (_,_,_,_,_,_) => go
| |- _ => f_equal
end.
Tactic Notation "fequal" :=
fequal_base.
(** [fequals] is the same as [fequal] except that it tries and solve
all trivial subgoals, using [reflexivity] and [congruence],
and the [proof_irrelevance] lemma.
(It applies to goals of the form [f x1 .. xN = f y1 .. yN]
and may produce subgoals of the form [xi = yi]). *)
Ltac fequal_post :=
first [ reflexivity | congruence | apply proof_irrelevance | idtac ].
Tactic Notation "fequals" :=
fequal; fequal_post.
(** [fequals_rec] calls [fequals] recursively.
It is equivalent to [repeat (progress fequals)]. *)
Tactic Notation "fequals_rec" :=
repeat (progress fequals).
(* ********************************************************************** *)
(** * Inversion *)
(* ---------------------------------------------------------------------- *)
(** ** Basic inversion *)
(** [invert keep H] is same to [inversion H] except that it puts all the
facts obtained in the goal. The keyword [keep] means that the
hypothesis [H] should not be removed. *)
Tactic Notation "invert" "keep" hyp(H) :=
pose ltac_mark; inversion H; gen_until_mark.
(** [invert keep H as X1 .. XN] is the same as [inversion H as ...] except
that only hypotheses which are not variable need to be named
explicitely, in a similar fashion as [introv] is used to name
only hypotheses. *)
Tactic Notation "invert" "keep" hyp(H) "as" simple_intropattern(I1) :=
invert keep H; introv I1.
Tactic Notation "invert" "keep" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) :=
invert keep H; introv I1 I2.
Tactic Notation "invert" "keep" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) :=
invert keep H; introv I1 I2 I3.
(** [invert H] is same to [inversion H] except that it puts all the
facts obtained in the goal and clears hypothesis [H].
In other words, it is equivalent to [invert keep H; clear H]. *)
Tactic Notation "invert" hyp(H) :=
invert keep H; clear H.
(** [invert H as X1 .. XN] is the same as [invert keep H as X1 .. XN]
but it also clears hypothesis [H]. *)
Tactic Notation "invert_tactic" hyp(H) tactic(tac) :=
let H' := fresh in rename H into H'; tac H'; clear H'.
Tactic Notation "invert" hyp(H) "as" simple_intropattern(I1) :=
invert_tactic H (fun H => invert keep H as I1).
Tactic Notation "invert" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) :=
invert_tactic H (fun H => invert keep H as I1 I2).
Tactic Notation "invert" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) :=
invert_tactic H (fun H => invert keep H as I1 I2 I3).
(* ---------------------------------------------------------------------- *)
(** ** Inversion with substitution *)
(** Our inversion tactics is able to get rid of dependent equalities
generated by [inversion], using proof irrelevance. *)
(* --we do not import Eqdep because it imports nasty hints automatically
Require Import Eqdep. *)
Axiom inj_pair2 : forall (U : Type) (P : U -> Type) (p : U) (x y : P p),
existT P p x = existT P p y -> x = y.
(* Proof. apply Eqdep.EqdepTheory.inj_pair2. Qed.*)
Ltac inverts_tactic H i1 i2 i3 i4 i5 i6 :=
let rec go i1 i2 i3 i4 i5 i6 :=
match goal with
| |- (ltac_Mark -> _) => intros _
| |- (?x = ?y -> _) => let H := fresh in intro H;
first [ subst x | subst y ];
go i1 i2 i3 i4 i5 i6
| |- (existT ?P ?p ?x = existT ?P ?p ?y -> _) =>
let H := fresh in intro H;
generalize (inj_pair2 _ P p x y H);
clear H; go i1 i2 i3 i4 i5 i6
| |- (?P -> ?Q) => i1; go i2 i3 i4 i5 i6 ltac:(intro)
| |- (forall _, _) => intro; go i1 i2 i3 i4 i5 i6
end in
generalize ltac_mark; invert keep H; go i1 i2 i3 i4 i5 i6;
unfold eq' in *.
(** [inverts keep H] is same to [invert keep H] except that it
applies [subst] to all the equalities generated by the inversion. *)
Tactic Notation "inverts" "keep" hyp(H) :=
inverts_tactic H ltac:(intro) ltac:(intro) ltac:(intro)
ltac:(intro) ltac:(intro) ltac:(intro).
(** [inverts keep H as X1 .. XN] is the same as
[invert keep H as X1 .. XN] except that it applies [subst] to all the
equalities generated by the inversion *)
Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1) :=
inverts_tactic H ltac:(intros I1)
ltac:(intro) ltac:(intro) ltac:(intro) ltac:(intro) ltac:(intro).
Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) :=
inverts_tactic H ltac:(intros I1) ltac:(intros I2)
ltac:(intro) ltac:(intro) ltac:(intro) ltac:(intro).
Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) :=
inverts_tactic H ltac:(intros I1) ltac:(intros I2) ltac:(intros I3)
ltac:(intro) ltac:(intro) ltac:(intro).
Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) :=
inverts_tactic H ltac:(intros I1) ltac:(intros I2) ltac:(intros I3)
ltac:(intros I4) ltac:(intro) ltac:(intro).
Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4)
simple_intropattern(I5) :=
inverts_tactic H ltac:(intros I1) ltac:(intros I2) ltac:(intros I3)
ltac:(intros I4) ltac:(intros I5) ltac:(intro).
Tactic Notation "inverts" "keep" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4)
simple_intropattern(I5) simple_intropattern(I6) :=
inverts_tactic H ltac:(intros I1) ltac:(intros I2) ltac:(intros I3)
ltac:(intros I4) ltac:(intros I5) ltac:(intros I6).
(** [inverts H] is same to [inverts keep H] except that it
clears hypothesis [H]. *)
Tactic Notation "inverts" hyp(H) :=
inverts keep H; clear H.
(** [inverts H as X1 .. XN] is the same as [inverts keep H as X1 .. XN]
but it also clears the hypothesis [H]. *)
Tactic Notation "inverts_tactic" hyp(H) tactic(tac) :=
let H' := fresh in rename H into H'; tac H'; clear H'.
Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1) :=
invert_tactic H (fun H => inverts keep H as I1).
Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) :=
invert_tactic H (fun H => inverts keep H as I1 I2).
Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) :=
invert_tactic H (fun H => inverts keep H as I1 I2 I3).
Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) :=
invert_tactic H (fun H => inverts keep H as I1 I2 I3 I4).
Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4)
simple_intropattern(I5) :=
invert_tactic H (fun H => inverts keep H as I1 I2 I3 I4 I5).
Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4)
simple_intropattern(I5) simple_intropattern(I6) :=
invert_tactic H (fun H => inverts keep H as I1 I2 I3 I4 I5 I6).
(** [inverts H as] performs an inversion on hypothesis [H], substitutes
generated equalities, and put in the goal the other freshly-created
hypotheses, for the user to name explicitly.
[inverts keep H as] is the same except that it does not clear [H].
--TODO: reimplement [inverts] above using this one *)
Ltac inverts_as_tactic H :=
let rec go tt :=
match goal with
| |- (ltac_Mark -> _) => intros _
| |- (?x = ?y -> _) => let H := fresh "TEMP" in intro H;
first [ subst x | subst y ];
go tt
| |- (existT ?P ?p ?x = existT ?P ?p ?y -> _) =>
let H := fresh in intro H;
generalize (inj_pair2 _ P p x y H);
clear H; go tt
| |- (forall _, _) =>
intro; let H := get_last_hyp tt in mark_to_generalize H; go tt
end in
pose ltac_mark; inversion H;
generalize ltac_mark; gen_until_mark;
go tt; gen_to_generalize; unfolds ltac_to_generalize;
unfold eq' in *.
Tactic Notation "inverts" "keep" hyp(H) "as" :=
inverts_as_tactic H.
Tactic Notation "inverts" hyp(H) "as" :=
inverts_as_tactic H; clear H.
Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4)
simple_intropattern(I5) simple_intropattern(I6) simple_intropattern(I7) :=
inverts H as; introv I1 I2 I3 I4 I5 I6 I7.
Tactic Notation "inverts" hyp(H) "as" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4)
simple_intropattern(I5) simple_intropattern(I6) simple_intropattern(I7)
simple_intropattern(I8) :=
inverts H as; introv I1 I2 I3 I4 I5 I6 I7 I8.
(* ---------------------------------------------------------------------- *)
(** ** Injection with substitution *)
(** Underlying implementation of [injects] *)
Ltac injects_tactic H :=
let rec go _ :=
match goal with
| |- (ltac_Mark -> _) => intros _
| |- (?x = ?y -> _) => let H := fresh in intro H;
first [ subst x | subst y | idtac ];
go tt
end in
generalize ltac_mark; injection H; go tt.
(** [injects keep H] takes an hypothesis [H] of the form
[C a1 .. aN = C b1 .. bN] and substitute all equalities
[ai = bi] that have been generated. *)
Tactic Notation "injects" "keep" hyp(H) :=
injects_tactic H.
(** [injects H] is similar to [injects keep H] but clears
the hypothesis [H]. *)
Tactic Notation "injects" hyp(H) :=
injects_tactic H; clear H.
(** [inject H as X1 .. XN] is the same as [injection]
followed by [intros X1 .. XN] *)
Tactic Notation "inject" hyp(H) :=
injection H.
Tactic Notation "inject" hyp(H) "as" ident(X1) :=
injection H; intros X1.
Tactic Notation "inject" hyp(H) "as" ident(X1) ident(X2) :=
injection H; intros X1 X2.
Tactic Notation "inject" hyp(H) "as" ident(X1) ident(X2) ident(X3) :=
injection H; intros X1 X2 X3.
Tactic Notation "inject" hyp(H) "as" ident(X1) ident(X2) ident(X3)
ident(X4) :=
injection H; intros X1 X2 X3 X4.
Tactic Notation "inject" hyp(H) "as" ident(X1) ident(X2) ident(X3)
ident(X4) ident(X5) :=
injection H; intros X1 X2 X3 X4 X5.
(* ---------------------------------------------------------------------- *)
(** ** Inversion and injection with substitution --rough implementation *)
(** The tactics [inversions] and [injections] provided in this section
are similar to [inverts] and [injects] except that they perform
substitution on all equalities from the context and not only
the ones freshly generated. The counterpart is that they have
simpler implementations. *)
(** [inversions keep H] is the same as [inversions H] but it does
not clear hypothesis [H]. *)
Tactic Notation "inversions" "keep" hyp(H) :=
inversion H; subst.
(** [inversions H] is a shortcut for [inversion H] followed by [subst]
and [clear H].
It is a rough implementation of [inverts keep H] which behave
badly when the proof context already contains equalities.
It is provided in case the better implementation turns out to be
too slow. *)
Tactic Notation "inversions" hyp(H) :=
inversion H; subst; clear H.
(** [injections keep H] is the same as [injection H] followed
by [intros] and [subst]. It is a rough implementation of
[injects keep H] which behave
badly when the proof context already contains equalities,
or when the goal starts with a forall or an implication. *)
Tactic Notation "injections" "keep" hyp(H) :=
injection H; intros; subst.
(** [injections H] is the same as [injection H] followed
by [intros] and [clear H] and [subst]. It is a rough
implementation of [injects keep H] which behave
badly when the proof context already contains equalities,
or when the goal starts with a forall or an implication. *)
Tactic Notation "injections" "keep" hyp(H) :=
injection H; clear H; intros; subst.
(* ---------------------------------------------------------------------- *)
(** ** Case analysis *)
(** [case_if] looks for a pattern of the form [if ?B then ?E1 else ?E2]
in the goal, and perform a case analysis on [B] by calling
[destruct B]. It looks in the goal first, and otherwise in the
first hypothesis that contains and [if] statement.
[case_if in H] can be used to specify which hypothesis to consider.
Syntaxes [case_if as Eq] and [case_if in H as Eq] allows to name
the hypothesis coming from the case analysis. *)
Ltac case_if_on_tactic E Eq :=
match type of E with
| {_}+{_} => destruct E as [Eq | Eq]
| _ => let X := fresh in
sets_eq <- X Eq: E;
destruct X
end.
Tactic Notation "case_if_on" constr(E) "as" simple_intropattern(Eq) :=
case_if_on_tactic E Eq.
Tactic Notation "case_if" "as" simple_intropattern(Eq) :=
match goal with
| |- context [if ?B then _ else _] => case_if_on B as Eq
| K: context [if ?B then _ else _] |- _ => case_if_on B as Eq
end.
Tactic Notation "case_if" "in" hyp(H) "as" simple_intropattern(Eq) :=
match type of H with context [if ?B then _ else _] =>
case_if_on B as Eq end.
Tactic Notation "case_if" :=
let Eq := fresh in case_if as Eq.
Tactic Notation "case_if" "in" hyp(H) :=
let Eq := fresh in case_if in H as Eq.
(** [cases_if] is similar to [case_if] with two main differences:
if it creates an equality of the form [x = y] or [x == y],
it substitutes it in the goal *)
Ltac cases_if_on_tactic E Eq :=
match type of E with
| {_}+{_} => destruct E as [Eq|Eq]; try subst_hyp Eq
| _ => let X := fresh in
sets_eq <- X Eq: E;
destruct X
end.
Tactic Notation "cases_if_on" constr(E) "as" simple_intropattern(Eq) :=
cases_if_on_tactic E Eq.
Tactic Notation "cases_if" "as" simple_intropattern(Eq) :=
match goal with
| |- context [if ?B then _ else _] => case_if_on B as Eq
| K: context [if ?B then _ else _] |- _ => case_if_on B as Eq
end.
Tactic Notation "cases_if" "in" hyp(H) "as" simple_intropattern(Eq) :=
match type of H with context [if ?B then _ else _] =>
cases_if_on B as Eq end.
Tactic Notation "cases_if" :=
let Eq := fresh in cases_if as Eq.
Tactic Notation "cases_if" "in" hyp(H) :=
let Eq := fresh in cases_if in H as Eq.
(** [destruct_if] looks for a pattern of the form [if ?B then ?E1 else ?E2]
in the goal, and perform a case analysis on [B] by calling
[destruct B]. It looks in the goal first, and otherwise in the
first hypothesis that contains and [if] statement. *)
Ltac destruct_if_post := tryfalse.
Tactic Notation "destruct_if"
"as" simple_intropattern(Eq1) simple_intropattern(Eq2) :=
match goal with
| |- context [if ?B then _ else _] => destruct B as [Eq1|Eq2]
| K: context [if ?B then _ else _] |- _ => destruct B as [Eq1|Eq2]
end;
destruct_if_post.
Tactic Notation "destruct_if" "in" hyp(H)
"as" simple_intropattern(Eq1) simple_intropattern(Eq2) :=
match type of H with context [if ?B then _ else _] =>
destruct B as [Eq1|Eq2] end;
destruct_if_post.
Tactic Notation "destruct_if" "as" simple_intropattern(Eq) :=
destruct_if as Eq Eq.
Tactic Notation "destruct_if" "in" hyp(H) "as" simple_intropattern(Eq) :=
destruct_if in H as Eq Eq.
Tactic Notation "destruct_if" :=
let Eq := fresh "C" in destruct_if as Eq Eq.
Tactic Notation "destruct_if" "in" hyp(H) :=
let Eq := fresh "C" in destruct_if in H as Eq Eq.
(** [destruct_head_match] performs a case analysis on the argument
of the head pattern matching when the goal has the form
[match ?E with ...] or [match ?E with ... = _] or
[_ = match ?E with ...]. Due to the limits of Ltac, this tactic
will not fail if a match does not occur. Instead, it might
perform a case analysis on an unspecified subterm from the goal.
--- Warning: experimental. *)
Ltac find_head_match T :=
match T with context [?E] =>
match T with
| E => fail 1
| _ => constr:(E)
end
end.
Ltac destruct_head_match_core cont :=
match goal with
| |- ?T1 = ?T2 => first [ let E := find_head_match T1 in cont E
| let E := find_head_match T2 in cont E ]
| |- ?T1 => let E := find_head_match T1 in cont E
end;
destruct_if_post.
Tactic Notation "destruct_head_match" "as" simple_intropattern(I) :=
destruct_head_match_core ltac:(fun E => destruct E as I).
Tactic Notation "destruct_head_match" :=
destruct_head_match_core ltac:(fun E => destruct E).
(* ********************************************************************** *)
(** * Induction *)
(** [inductions E] is a shorthand for [dependent induction E].
[inductions E gen X1 .. XN] is a shorthand for
[dependent induction E generalizing X1 .. XN]. *)
(*--temp
Module Start.
Section Test.
Require Coq.Program.Equality.
End Test.
End Start.
Print HintDb core.
do_depind ltac:(fun hyp => do_ind hyp) H.
Require Import Coq.Program.Equality.
Print HintDb core.
Tactic Notation "inductions" ident(E) :=
dependent induction E.
Tactic Notation "inductions" ident(E) "gen" ident(X1) :=
dependent induction E generalizing X1.
Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2) :=
dependent induction E generalizing X1 X2.
Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2)
ident(X3) :=
dependent induction E generalizing X1 X2 X3.
Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2)
ident(X3) ident(X4) :=
dependent induction E generalizing X1 X2 X3 X4.
Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2)
ident(X3) ident(X4) ident(X5) :=
dependent induction E generalizing X1 X2 X3 X4 X5.
Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2)
ident(X3) ident(X4) ident(X5) ident(X6) :=
dependent induction E generalizing X1 X2 X3 X4 X5 X6.
Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2)
ident(X3) ident(X4) ident(X5) ident(X6) ident(X7) :=
dependent induction E generalizing X1 X2 X3 X4 X5 X6 X7.
Tactic Notation "inductions" ident(E) "gen" ident(X1) ident(X2)
ident(X3) ident(X4) ident(X5) ident(X6) ident(X7) ident(X8) :=
dependent induction E generalizing X1 X2 X3 X4 X5 X6 X7 X8.
*)
(** [induction_wf IH: E X] is used to apply the well-founded induction
principle, for a given well-founded relation. It applies to a goal
[PX] where [PX] is a proposition on [X]. First, it sets up the
goal in the form [(fun a => P a) X], using [pattern X], and then
it applies the well-founded induction principle instantiated on [E],
where [E] is a term of type [well_founded R], and [R] is a binary
relation.
Syntaxes [induction_wf: E X] and [induction_wf E X]. *)
Tactic Notation "induction_wf" ident(IH) ":" constr(E) ident(X) :=
pattern X; apply (well_founded_ind E); clear X; intros X IH.
Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
let IH := fresh "IH" in induction_wf IH: E X.
Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
induction_wf: E X.
(* ********************************************************************** *)
(** * Decidable equality *)
(** [decides_equality] is the same as [decide equality] excepts that it
is able to unfold definitions at head of the current goal. *)
Ltac decides_equality_tactic :=
first [ decide equality | progress(unfolds); decides_equality_tactic ].
Tactic Notation "decides_equality" :=
decides_equality_tactic.
(* ********************************************************************** *)
(** * Equivalence *)
(** [iff H] can be used to prove an equivalence [P <-> Q] and name [H]
the hypothesis obtained in each case. The syntaxes [iff] and [iff H1 H2]
are also available to specify zero or two names. The tactic [iff <- H]
swaps the two subgoals, i.e. produces (Q -> P) as first subgoal. *)
Lemma iff_intro_swap : forall (P Q : Prop),
(Q -> P) -> (P -> Q) -> (P <-> Q).
Proof. intuition. Qed.
Tactic Notation "iff" simple_intropattern(H1) simple_intropattern(H2) :=
split; [ intros H1 | intros H2 ].
Tactic Notation "iff" simple_intropattern(H) :=
iff H H.
Tactic Notation "iff" :=
let H := fresh "H" in iff H.
Tactic Notation "iff" "<-" simple_intropattern(H1) simple_intropattern(H2) :=
apply iff_intro_swap; [ intros H1 | intros H2 ].
Tactic Notation "iff" "<-" simple_intropattern(H) :=
iff <- H H.
Tactic Notation "iff" "<-" :=
let H := fresh "H" in iff <- H.
(* ********************************************************************** *)
(** * N-ary Conjunctions and Disjunctions *)
(* ---------------------------------------------------------------------- *)
(** N-ary Conjunctions Splitting in Goals *)
(** Underlying implementation of [splits]. *)
Ltac splits_tactic N :=
match N with
| O => fail
| S O => idtac
| S ?N' => split; [| splits_tactic N']
end.
Ltac unfold_goal_until_conjunction :=
match goal with
| |- _ /\ _ => idtac
| _ => progress(unfolds); unfold_goal_until_conjunction
end.
Ltac get_term_conjunction_arity T :=
match T with
| _ /\ _ /\ _ /\ _ /\ _ /\ _ /\ _ /\ _ => constr:(8)
| _ /\ _ /\ _ /\ _ /\ _ /\ _ /\ _ => constr:(7)
| _ /\ _ /\ _ /\ _ /\ _ /\ _ => constr:(6)
| _ /\ _ /\ _ /\ _ /\ _ => constr:(5)
| _ /\ _ /\ _ /\ _ => constr:(4)
| _ /\ _ /\ _ => constr:(3)
| _ /\ _ => constr:(2)
| _ -> ?T' => get_term_conjunction_arity T'
| _ => let P := get_head T in
let T' := eval unfold P in T in
match T' with
| T => fail 1
| _ => get_term_conjunction_arity T'
end
(* todo: warning this can loop... *)
end.
Ltac get_goal_conjunction_arity :=
match goal with |- ?T => get_term_conjunction_arity T end.
(** [splits] applies to a goal of the form [(T1 /\ .. /\ TN)] and
destruct it into [N] subgoals [T1] .. [TN]. If the goal is not a
conjunction, then it unfolds the head definition. *)
Tactic Notation "splits" :=
unfold_goal_until_conjunction;
let N := get_goal_conjunction_arity in
splits_tactic N.
(** [splits N] is similar to [splits], except that it will unfold as many
definitions as necessary to obtain an [N]-ary conjunction. *)
Tactic Notation "splits" constr(N) :=
splits_tactic N.
(** [splits_all] will recursively split any conjunction, unfolding
definitions when necessary. Warning: this tactic will loop
on goals of the form [well_founded R]. Todo: fix this *)
Ltac splits_all_base := repeat split.
Tactic Notation "splits_all" :=
splits_all_base.
(* ---------------------------------------------------------------------- *)
(** N-ary Conjunctions Deconstruction *)
(** Underlying implementation of [destructs]. *)
Ltac destructs_conjunction_tactic N T :=
match N with
| 2 => destruct T as [? ?]
| 3 => destruct T as [? [? ?]]
| 4 => destruct T as [? [? [? ?]]]
| 5 => destruct T as [? [? [? [? ?]]]]
| 6 => destruct T as [? [? [? [? [? ?]]]]]
| 7 => destruct T as [? [? [? [? [? [? ?]]]]]]
end.
(** [destructs T] allows destructing a term [T] which is a N-ary
conjunction. It is equivalent to [destruct T as (H1 .. HN)],
except that it does not require to manually specify N different
names. *)
Tactic Notation "destructs" constr(T) :=
let TT := type of T in
let N := get_term_conjunction_arity TT in
destructs_conjunction_tactic N T.
(** [destructs N T] is equivalent to [destruct T as (H1 .. HN)],
except that it does not require to manually specify N different
names. Remark that it is not restricted to N-ary conjunctions. *)
Tactic Notation "destructs" constr(N) constr(T) :=
destructs_conjunction_tactic N T.
(* ---------------------------------------------------------------------- *)
(** Proving goals which are N-ary disjunctions *)
(** Underlying implementation of [branch]. *)
Ltac branch_tactic K N :=
let K := nat_from_number K in
let N := nat_from_number N in
match constr:(K,N) with
| (_,0) => fail 1
| (0,_) => fail 1
| (1,1) => idtac
| (1,_) => left
| (S ?K', S ?N') => right; branch_tactic K' N'
end.
Ltac unfold_goal_until_disjunction :=
match goal with
| |- _ \/ _ => idtac
| _ => progress(unfolds); unfold_goal_until_disjunction
end.
Ltac get_term_disjunction_arity T :=
match T with
| _ \/ _ \/ _ \/ _ \/ _ \/ _ \/ _ \/ _ => constr:(8)
| _ \/ _ \/ _ \/ _ \/ _ \/ _ \/ _ => constr:(7)
| _ \/ _ \/ _ \/ _ \/ _ \/ _ => constr:(6)
| _ \/ _ \/ _ \/ _ \/ _ => constr:(5)
| _ \/ _ \/ _ \/ _ => constr:(4)
| _ \/ _ \/ _ => constr:(3)
| _ \/ _ => constr:(2)
| _ -> ?T' => get_term_disjunction_arity T'
| _ => let P := get_head T in
let T' := eval unfold P in T in
match T' with
| T => fail 1
| _ => get_term_disjunction_arity T'
end
end.
Ltac get_goal_disjunction_arity :=
match goal with |- ?T => get_term_disjunction_arity T end.
(** [branch N] applies to a goal of the form
[P1 \/ ... \/ PK \/ ... \/ PN] and leaves the goal [PK].
It only able to unfold the head definition (if there is one),
but for more complex unfolding one should use the tactic
[branch K of N]. *)
Tactic Notation "branch" constr(K) :=
unfold_goal_until_disjunction;
let N := get_goal_disjunction_arity in
branch_tactic K N.
(** [branch K of N] is similar to [branch K] except that the
arity of the disjunction [N] is given manually, and so this
version of the tactic is able to unfold definitions.
In other words, applies to a goal of the form
[P1 \/ ... \/ PK \/ ... \/ PN] and leaves the goal [PK]. *)
Tactic Notation "branch" constr(K) "of" constr(N) :=
branch_tactic K N.
(* ---------------------------------------------------------------------- *)
(** N-ary Disjunction Deconstruction *)
(** Underlying implementation of [branches]. *)
Ltac destructs_disjunction_tactic N T :=
match N with
| 2 => destruct T as [? | ?]
| 3 => destruct T as [? | [? | ?]]
| 4 => destruct T as [? | [? | [? | ?]]]
| 5 => destruct T as [? | [? | [? | [? | ?]]]]
end.
(** [branches T] allows destructing a term [T] which is a N-ary
disjunction. It is equivalent to [destruct T as [ H1 | .. | HN ] ],
and produces [N] subgoals corresponding to the [N] possible cases. *)
Tactic Notation "branches" constr(T) :=
let TT := type of T in
let N := get_term_disjunction_arity TT in
destructs_disjunction_tactic N T.
(** [branches N T] is the same as [branches T] except that the arity is
forced to [N]. This version is useful to unfold definitions
on the fly. *)
Tactic Notation "branches" constr(N) constr(T) :=
destructs_disjunction_tactic N T.
(* ---------------------------------------------------------------------- *)
(** N-ary Existentials *)
(* Underlying implementation of [exists]. *)
Ltac get_term_existential_arity T :=
match T with
| exists x1 x2 x3 x4 x5 x6 x7 x8, _ => constr:(8)
| exists x1 x2 x3 x4 x5 x6 x7, _ => constr:(7)
| exists x1 x2 x3 x4 x5 x6, _ => constr:(6)
| exists x1 x2 x3 x4 x5, _ => constr:(5)
| exists x1 x2 x3 x4, _ => constr:(4)
| exists x1 x2 x3, _ => constr:(3)
| exists x1 x2, _ => constr:(2)
| exists x1, _ => constr:(1)
| _ -> ?T' => get_term_existential_arity T'
| _ => let P := get_head T in
let T' := eval unfold P in T in
match T' with
| T => fail 1
| _ => get_term_existential_arity T'
end
end.
Ltac get_goal_existential_arity :=
match goal with |- ?T => get_term_existential_arity T end.
(** [exists T1 ... TN] is a shorthand for [exists T1; ...; exists TN].
It is intended to prove goals of the form [exist X1 .. XN, P].
If an argument provided is [__] (double underscore), then an
evar is introduced. [exists T1 .. TN ___] is equivalent to
[exists T1 .. TN __ __ __] with as many [__] as possible. *)
Tactic Notation "exists_original" constr(T1) :=
exists T1.
Tactic Notation "exists" constr(T1) :=
match T1 with
| ltac_wild => esplit
| ltac_wilds => repeat esplit
| _ => exists T1
end.
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.
Tactic Notation "exists" constr(T1) constr(T2) constr(T3) constr(T4)
constr(T5) :=
exists T1; exists T2; exists T3; exists T4; exists T5.
Tactic Notation "exists" constr(T1) constr(T2) constr(T3) constr(T4)
constr(T5) constr(T6) :=
exists T1; exists T2; exists T3; exists T4; exists T5; exists T6.
(* The tactic [exists___ N] is short for [exists __ ... __]
with [N] double-underscores. The tactic [exists_] is equivalent
to calling [exists___ N], where the value of [N] is obtained
by counting the number of existentials syntactically present
at the head of the goal. The behaviour of [exists___] differs
from that of [exists ___] is the case where the goal is a
definition which yields an existential only after unfolding. *)
Tactic Notation "exists___" constr(N) :=
let rec aux N :=
match N with
| 0 => idtac
| S ?N' => esplit; aux N'
end in
let N := nat_from_number N in aux N.
Tactic Notation "exists___" :=
let N := get_goal_existential_arity in
exists___ N.
(* ********************************************************************** *)
(** * Tactics to prove typeclass instances *)
(** [typeclass] is an automation tactic specialized for finding
typeclass instances. *)
Tactic Notation "typeclass" :=
let go _ := eauto with typeclass_instances in
solve [ go tt | constructor; go tt ].
(** [solve_typeclass] is a simpler version of [typeclass], to use
in hint tactics for resolving instances *)
Tactic Notation "solve_typeclass" :=
solve [ eauto with typeclass_instances ].
(* ********************************************************************** *)
(** * Tactics to invoke automation *)
(* ---------------------------------------------------------------------- *)
(** ** Definitions of automation tactics *)
(** The two following tactics defined the default behaviour of
"light automation" and "strong automation". These tactics
may be redefined at any time using the syntax [Ltac .. ::= ..]. *)
(** [auto_tilde] is the tactic which will be called each time a symbol
[~] is used after a tactic. *)
Ltac auto_tilde := auto.
(** [auto_star] is the tactic which will be called each time a symbol
[*] is used after a tactic. *)
Ltac auto_star := try solve [ auto | eauto | intuition eauto ].
(** [auto~] is a notation for tactic [auto_tilde]. It may be followed
by lemmas (or proofs terms) which auto will be able to use
for solving the goal. *)
Tactic Notation "auto" "~" :=
auto_tilde.
Tactic Notation "auto" "~" constr(E1) :=
lets: E1; auto_tilde.
Tactic Notation "auto" "~" constr(E1) constr(E2) :=
lets: E1; lets: E2; auto_tilde.
Tactic Notation "auto" "~" constr(E1) constr(E2) constr(E3) :=
lets: E1; lets: E2; lets: E3; auto_tilde.
(** [auto*] is a notation for tactic [auto_star]. It may be followed
by lemmas (or proofs terms) which auto will be able to use
for solving the goal. *)
Tactic Notation "auto" "*" :=
auto_star.
Tactic Notation "auto" "*" constr(E1) :=
lets: E1; auto_star.
Tactic Notation "auto" "*" constr(E1) constr(E2) :=
lets: E1; lets: E2; auto_star.
Tactic Notation "auto" "*" constr(E1) constr(E2) constr(E3) :=
lets: E1; lets: E2; lets: E3; auto_star.
(** [auto_false] is a version of [auto] able to spot some contradictions.
[auto_false~] and [auto_false*] are also available. *)
Ltac auto_false_base cont :=
try solve [ cont tt | tryfalse by congruence/
| try split; intros_all; tryfalse by congruence/ ].
Tactic Notation "auto_false" :=
auto_false_base ltac:(fun tt => auto).
Tactic Notation "auto_false" "~" :=
auto_false_base ltac:(fun tt => auto~).
Tactic Notation "auto_false" "*" :=
auto_false_base ltac:(fun tt => auto*).
(* ---------------------------------------------------------------------- *)
(** ** Definitions for parsing compatibility *)
Tactic Notation "f_equal" :=
f_equal.
Tactic Notation "constructor" :=
constructor.
Tactic Notation "simple" :=
simpl.
(* ---------------------------------------------------------------------- *)
(** ** Parsing for light automation *)
(** Any tactic followed by the symbol [~] will have [auto_tilde] called
on all of its subgoals. Three exceptions:
- [cuts] and [asserts] only call [auto] on their first subgoal,
- [apply~] relies on [sapply] rather than [apply],
- [tryfalse~] is defined as [tryfalse by auto_tilde].
Some builtin tactics are not defined using tactic notations
and thus cannot be extended, e.g. [simpl] and [unfold].
For these, notation such as [simpl~] will not be available. *)
Tactic Notation "equates" "~" constr(E) :=
equates E; auto~.
Tactic Notation "equates" "~" constr(n1) constr(n2) :=
equates n1 n2; auto~.
Tactic Notation "equates" "~" constr(n1) constr(n2) constr(n3) :=
equates n1 n2 n3; auto~.
Tactic Notation "equates" "~" constr(n1) constr(n2) constr(n3) constr(n4) :=
equates n1 n2 n3 n4; auto~.
Tactic Notation "applys_eq" "~" constr(H) constr(E) :=
applys_eq H E; auto_tilde.
Tactic Notation "applys_eq" "~" constr(H) constr(n1) constr(n2) :=
applys_eq H n1 n2; auto_tilde.
Tactic Notation "applys_eq" "~" constr(H) constr(n1) constr(n2) constr(n3) :=
applys_eq H n1 n2 n3; auto_tilde.
Tactic Notation "applys_eq" "~" constr(H) constr(n1) constr(n2) constr(n3) constr(n4) :=
applys_eq H n1 n2 n3 n4; auto_tilde.
Tactic Notation "apply" "~" constr(H) :=
sapply H; auto_tilde.
Tactic Notation "applys" "~" constr(H) :=
sapply H; auto_tilde.
Tactic Notation "destruct" "~" constr(H) :=
destruct H; auto_tilde.
Tactic Notation "destruct" "~" constr(H) "as" simple_intropattern(I) :=
destruct H as I; auto_tilde.
Tactic Notation "f_equal" "~" :=
f_equal; auto_tilde.
Tactic Notation "induction" "~" constr(H) :=
induction H; auto_tilde.
Tactic Notation "inversion" "~" constr(H) :=
inversion H; auto_tilde.
Tactic Notation "split" "~" :=
split; auto_tilde.
Tactic Notation "subst" "~" :=
subst; auto_tilde.
Tactic Notation "right" "~" :=
right; auto_tilde.
Tactic Notation "left" "~" :=
left; auto_tilde.
Tactic Notation "constructor" "~" :=
constructor; auto_tilde.
Tactic Notation "constructors" "~" :=
constructors; auto_tilde.
Tactic Notation "false" "~" :=
false; auto_tilde.
Tactic Notation "false" "~" constr(T) :=
false T by auto_tilde/.
Tactic Notation "tryfalse" "~" :=
tryfalse by auto_tilde/.
Tactic Notation "tryfalse_invert" "~" :=
first [ tryfalse~ | false_invert ].
Tactic Notation "asserts" "~" simple_intropattern(H) ":" constr(E) :=
asserts H: E; [ auto_tilde | idtac ].
Tactic Notation "cuts" "~" simple_intropattern(H) ":" constr(E) :=
cuts H: E; [ auto_tilde | idtac ].
Tactic Notation "cuts" "~" ":" constr(E) :=
cuts: E; [ auto_tilde | idtac ].
Tactic Notation "lets" "~" simple_intropattern(I) ":" constr(E) :=
lets I: E; auto_tilde.
Tactic Notation "lets" "~" ":" constr(E1) :=
lets: E1; auto_tilde.
Tactic Notation "applys" "~" constr(E) constr(A) :=
applys E A; auto_tilde.
Tactic Notation "specializes" "~" hyp(H) constr(A) :=
specializes H A; auto_tilde.
Tactic Notation "lets" "~" simple_intropattern(I) ":" constr(E) constr(A) :=
lets I: E A; auto_tilde.
Tactic Notation "lets" "~" simple_intropattern(I) ":" constr(E) constr(A1) constr(A2) :=
lets I: E A1 A2; auto_tilde.
Tactic Notation "lets" "~" simple_intropattern(I) ":" constr(E) constr(A1) constr(A2) constr(A3) :=
lets I: E A1 A2 A3; auto_tilde.
Tactic Notation "forwards" "~" simple_intropattern(I) ":" constr(E) :=
forwards I: E; auto_tilde.
Tactic Notation "forwards" "~" ":" constr(E) :=
forwards: E; auto_tilde.
Tactic Notation "fapply" "~" constr(E) :=
fapply E; auto_tilde.
Tactic Notation "sapply" "~" constr(E) :=
sapply E; auto_tilde.
Tactic Notation "logic" "~" constr(E) :=
logic_base E ltac:(fun _ => auto_tilde).
Tactic Notation "intros_all" "~" :=
intros_all; auto_tilde.
Tactic Notation "unfolds" "~" :=
unfolds; auto_tilde.
Tactic Notation "unfolds" "~" reference(F1) :=
unfolds F1; auto_tilde.
Tactic Notation "unfolds" "~" reference(F1) "," reference(F2) :=
unfolds F1, F2; auto_tilde.
Tactic Notation "unfolds" "~" reference(F1) "," reference(F2) "," reference(F3) :=
unfolds F1, F2, F3; auto_tilde.
Tactic Notation "unfolds" "~" reference(F1) "," reference(F2) "," reference(F3) ","
reference(F4) :=
unfolds F1, F2, F3, F4; auto_tilde.
Tactic Notation "simple" "~" :=
simpl; auto_tilde.
Tactic Notation "simple" "~" "in" hyp(H) :=
simpl in H; auto_tilde.
Tactic Notation "simpls" "~" :=
simpls; auto_tilde.
Tactic Notation "hnfs" "~" :=
hnfs; auto_tilde.
Tactic Notation "substs" "~" :=
substs; auto_tilde.
Tactic Notation "subst_term" "~" constr(E) :=
subst_term E; auto_tilde.
Tactic Notation "rewrite" "~" constr(E) :=
rewrite E; auto_tilde.
Tactic Notation "rewrite" "~" "<-" constr(E) :=
rewrite <- E; auto_tilde.
Tactic Notation "rewrite" "~" constr(E) "in" hyp(H) :=
rewrite E in H; auto_tilde.
Tactic Notation "rewrite" "~" "<-" constr(E) "in" hyp(H) :=
rewrite <- E in H; auto_tilde.
Tactic Notation "rewrite_all" "~" constr(E) :=
rewrite_all E; auto_tilde.
Tactic Notation "rewrite_all" "~" "<-" constr(E) :=
rewrite_all <- E; auto_tilde.
Tactic Notation "rewrite_all" "~" constr(E) "in" ident(H) :=
rewrite_all E in H; auto_tilde.
Tactic Notation "rewrite_all" "~" "<-" constr(E) "in" ident(H) :=
rewrite_all <- E in H; auto_tilde.
Tactic Notation "rewrite_all" "~" constr(E) "in" "*" :=
rewrite_all E in *; auto_tilde.
Tactic Notation "rewrite_all" "~" "<-" constr(E) "in" "*" :=
rewrite_all <- E in *; auto_tilde.
Tactic Notation "asserts_rewrite" "~" constr(E) :=
asserts_rewrite E; auto_tilde.
Tactic Notation "asserts_rewrite" "~" "<-" constr(E) :=
asserts_rewrite <- E; auto_tilde.
Tactic Notation "asserts_rewrite" "~" constr(E) "in" hyp(H) :=
asserts_rewrite E in H; auto_tilde.
Tactic Notation "asserts_rewrite" "~" "<-" constr(E) "in" hyp(H) :=
asserts_rewrite <- E in H; auto_tilde.
Tactic Notation "cuts_rewrite" "~" constr(E) :=
cuts_rewrite E; auto_tilde.
Tactic Notation "cuts_rewrite" "~" "<-" constr(E) :=
cuts_rewrite <- E; auto_tilde.
Tactic Notation "cuts_rewrite" "~" constr(E) "in" hyp(H) :=
cuts_rewrite E in H; auto_tilde.
Tactic Notation "cuts_rewrite" "~" "<-" constr(E) "in" hyp(H) :=
cuts_rewrite <- E in H; auto_tilde.
Tactic Notation "fequal" "~" :=
fequal; auto_tilde.
Tactic Notation "fequals" "~" :=
fequals; auto_tilde.
Tactic Notation "pi_rewrite" "~" constr(E) :=
pi_rewrite E; auto_tilde.
Tactic Notation "pi_rewrite" "~" constr(E) "in" hyp(H) :=
pi_rewrite E in H; auto_tilde.
Tactic Notation "invert" "~" hyp(H) :=
invert H; auto_tilde.
Tactic Notation "inverts" "~" hyp(H) :=
inverts H; auto_tilde.
Tactic Notation "injects" "~" hyp(H) :=
injects H; auto_tilde.
Tactic Notation "inversions" "~" hyp(H) :=
inversions H; auto_tilde.
Tactic Notation "case_if" "~" :=
case_if; auto_tilde.
Tactic Notation "case_if" "~" "in" hyp(H) :=
case_if in H; auto_tilde.
Tactic Notation "cases_if" "~" :=
cases_if; auto_tilde.
Tactic Notation "cases_if" "~" "in" hyp(H) :=
cases_if in H; auto_tilde.
Tactic Notation "destruct_if" "~" :=
destruct_if; auto_tilde.
Tactic Notation "destruct_if" "~" "in" hyp(H) :=
destruct_if in H; auto_tilde.
Tactic Notation "destruct_head_match" "~" :=
destruct_head_match; auto_tilde.
Tactic Notation "decides_equality" "~" :=
decides_equality; auto_tilde.
Tactic Notation "splits" "~" :=
splits; auto_tilde.
Tactic Notation "splits" "~" constr(N) :=
splits N; auto_tilde.
Tactic Notation "destructs" "~" constr(T) :=
destructs T; auto_tilde.
Tactic Notation "destructs" "~" constr(N) constr(T) :=
destructs N T; auto_tilde.
Tactic Notation "branch" "~" constr(N) :=
branch N; auto_tilde.
Tactic Notation "branch" "~" constr(K) "of" constr(N) :=
branch K of N; auto_tilde.
Tactic Notation "branches" "~" constr(T) :=
branches T; auto_tilde.
Tactic Notation "branches" "~" constr(N) constr(T) :=
branches N T; auto_tilde.
Tactic Notation "exists___" "~" :=
exists___; auto_tilde.
Tactic Notation "exists" "~" constr(T1) :=
exists T1; auto_tilde.
Tactic Notation "exists" "~" constr(T1) constr(T2) :=
exists T1 T2; auto_tilde.
Tactic Notation "exists" "~" constr(T1) constr(T2) constr(T3) :=
exists T1 T2 T3; auto_tilde.
Tactic Notation "exists" "~" constr(T1) constr(T2) constr(T3) constr(T4) :=
exists T1 T2 T3 T4; auto_tilde.
Tactic Notation "exists" "~" constr(T1) constr(T2) constr(T3) constr(T4)
constr(T5) :=
exists T1 T2 T3 T4 T5; auto_tilde.
Tactic Notation "exists" "~" constr(T1) constr(T2) constr(T3) constr(T4)
constr(T5) constr(T6) :=
exists T1 T2 T3 T4 T5 T6; auto_tilde.
(* ---------------------------------------------------------------------- *)
(** ** Parsing for strong automation *)
(** Any tactic followed by the symbol [*] will have [auto*] called
on all of its subgoals. The exceptions to these rules are the
same as for light automation.
Exception: use [subs*] instead of [subst*] if you
import the library [Coq.Classes.Equivalence]. *)
Tactic Notation "equates" "*" constr(E) :=
equates E; auto_star.
Tactic Notation "equates" "*" constr(n1) constr(n2) :=
equates n1 n2; auto_star.
Tactic Notation "equates" "*" constr(n1) constr(n2) constr(n3) :=
equates n1 n2 n3; auto_star.
Tactic Notation "equates" "*" constr(n1) constr(n2) constr(n3) constr(n4) :=
equates n1 n2 n3 n4; auto_star.
Tactic Notation "applys_eq" "*" constr(H) constr(E) :=
applys_eq H E; auto_star.
Tactic Notation "applys_eq" "*" constr(H) constr(n1) constr(n2) :=
applys_eq H n1 n2; auto_star.
Tactic Notation "applys_eq" "*" constr(H) constr(n1) constr(n2) constr(n3) :=
applys_eq H n1 n2 n3; auto_star.
Tactic Notation "applys_eq" "*" constr(H) constr(n1) constr(n2) constr(n3) constr(n4) :=
applys_eq H n1 n2 n3 n4; auto_star.
Tactic Notation "apply" "*" constr(H) :=
sapply H; auto_star.
Tactic Notation "applys" "*" constr(H) :=
sapply H; auto_star.
Tactic Notation "destruct" "*" constr(H) :=
destruct H; auto_star.
Tactic Notation "destruct" "*" constr(H) "as" simple_intropattern(I) :=
destruct H as I; auto_star.
Tactic Notation "f_equal" "*" :=
f_equal; auto_star.
Tactic Notation "induction" "*" constr(H) :=
induction H; auto_star.
Tactic Notation "inversion" "*" constr(H) :=
inversion H; auto_star.
Tactic Notation "split" "*" :=
split; auto_star.
Tactic Notation "subs" "*" :=
subst; auto_star.
Tactic Notation "subst" "*" :=
subst; auto_star.
Tactic Notation "right" "*" :=
right; auto_star.
Tactic Notation "left" "*" :=
left; auto_star.
Tactic Notation "constructor" "*" :=
constructor; auto_star.
Tactic Notation "constructors" "*" :=
constructors; auto_star.
Tactic Notation "false" "*" :=
false; auto_star.
Tactic Notation "false" "*" constr(T) :=
false T by auto_star/.
Tactic Notation "tryfalse" "*" :=
tryfalse by auto_star/.
Tactic Notation "tryfalse_invert" "*" :=
first [ tryfalse* | false_invert ].
Tactic Notation "asserts" "*" simple_intropattern(H) ":" constr(E) :=
asserts H: E; [ auto_star | idtac ].
Tactic Notation "cuts" "*" simple_intropattern(H) ":" constr(E) :=
cuts H: E; [ auto_star | idtac ].
Tactic Notation "cuts" "*" ":" constr(E) :=
cuts: E; [ auto_star | idtac ].
Tactic Notation "lets" "*" simple_intropattern(I) ":" constr(E) :=
lets I: E; auto_star.
Tactic Notation "lets" "*" ":" constr(E1) :=
lets: E1; auto_star.
Tactic Notation "applys" "*" constr(E) constr(A) :=
applys E A; auto_star.
Tactic Notation "specializes" "*" hyp(H) constr(A) :=
specializes H A; auto_star.
Tactic Notation "lets" "*" simple_intropattern(I) ":" constr(E) constr(A) :=
lets I: E A; auto_star.
Tactic Notation "lets" "*" simple_intropattern(I) ":" constr(E) constr(A1) constr(A2) :=
lets I: E A1 A2; auto_star.
Tactic Notation "lets" "*" simple_intropattern(I) ":" constr(E) constr(A1) constr(A2) constr(A3) :=
lets I: E A1 A2 A3; auto_star.
Tactic Notation "forwards" "*" simple_intropattern(I) ":" constr(E) :=
forwards I: E; auto_star.
Tactic Notation "forwards" "*" ":" constr(E) :=
forwards: E; auto_star.
Tactic Notation "fapply" "*" constr(E) :=
fapply E; auto_star.
Tactic Notation "sapply" "*" constr(E) :=
sapply E; auto_star.
Tactic Notation "logic" constr(E) :=
logic_base E ltac:(fun _ => auto_star).
Tactic Notation "intros_all" "*" :=
intros_all; auto_star.
Tactic Notation "unfolds" "*" :=
unfolds; auto_star.
Tactic Notation "unfolds" "*" reference(F1) :=
unfolds F1; auto_star.
Tactic Notation "unfolds" "*" reference(F1) "," reference(F2) :=
unfolds F1, F2; auto_star.
Tactic Notation "unfolds" "*" reference(F1) "," reference(F2) "," reference(F3) :=
unfolds F1, F2, F3; auto_star.
Tactic Notation "unfolds" "*" reference(F1) "," reference(F2) "," reference(F3) ","
reference(F4) :=
unfolds F1, F2, F3, F4; auto_star.
Tactic Notation "simple" "*" :=
simpl; auto_star.
Tactic Notation "simple" "*" "in" hyp(H) :=
simpl in H; auto_star.
Tactic Notation "simpls" "*" :=
simpls; auto_star.
Tactic Notation "hnfs" "*" :=
hnfs; auto_star.
Tactic Notation "substs" "*" :=
substs; auto_star.
Tactic Notation "subst_term" "*" constr(E) :=
subst_term E; auto_star.
Tactic Notation "rewrite" "*" constr(E) :=
rewrite E; auto_star.
Tactic Notation "rewrite" "*" "<-" constr(E) :=
rewrite <- E; auto_star.
Tactic Notation "rewrite" "*" constr(E) "in" hyp(H) :=
rewrite E in H; auto_star.
Tactic Notation "rewrite" "*" "<-" constr(E) "in" hyp(H) :=
rewrite <- E in H; auto_star.
Tactic Notation "rewrite_all" "*" constr(E) :=
rewrite_all E; auto_star.
Tactic Notation "rewrite_all" "*" "<-" constr(E) :=
rewrite_all <- E; auto_star.
Tactic Notation "rewrite_all" "*" constr(E) "in" ident(H) :=
rewrite_all E in H; auto_star.
Tactic Notation "rewrite_all" "*" "<-" constr(E) "in" ident(H) :=
rewrite_all <- E in H; auto_star.
Tactic Notation "rewrite_all" "*" constr(E) "in" "*" :=
rewrite_all E in *; auto_star.
Tactic Notation "rewrite_all" "*" "<-" constr(E) "in" "*" :=
rewrite_all <- E in *; auto_star.
Tactic Notation "asserts_rewrite" "*" constr(E) :=
asserts_rewrite E; auto_star.
Tactic Notation "asserts_rewrite" "*" "<-" constr(E) :=
asserts_rewrite <- E; auto_star.
Tactic Notation "asserts_rewrite" "*" constr(E) "in" hyp(H) :=
asserts_rewrite E; auto_star.
Tactic Notation "asserts_rewrite" "*" "<-" constr(E) "in" hyp(H) :=
asserts_rewrite <- E; auto_star.
Tactic Notation "cuts_rewrite" "*" constr(E) :=
cuts_rewrite E; auto_star.
Tactic Notation "cuts_rewrite" "*" "<-" constr(E) :=
cuts_rewrite <- E; auto_star.
Tactic Notation "cuts_rewrite" "*" constr(E) "in" hyp(H) :=
cuts_rewrite E in H; auto_star.
Tactic Notation "cuts_rewrite" "*" "<-" constr(E) "in" hyp(H) :=
cuts_rewrite <- E in H; auto_star.
Tactic Notation "fequal" "*" :=
fequal; auto_star.
Tactic Notation "fequals" "*" :=
fequals; auto_star.
Tactic Notation "pi_rewrite" "*" constr(E) :=
pi_rewrite E; auto_star.
Tactic Notation "pi_rewrite" "*" constr(E) "in" hyp(H) :=
pi_rewrite E in H; auto_star.
Tactic Notation "invert" "*" hyp(H) :=
invert H; auto_star.
Tactic Notation "inverts" "*" hyp(H) :=
inverts H; auto_star.
Tactic Notation "injects" "*" hyp(H) :=
injects H; auto_star.
Tactic Notation "inversions" "*" hyp(H) :=
inversions H; auto_star.
Tactic Notation "case_if" "*" :=
case_if; auto_star.
Tactic Notation "case_if" "*" "in" hyp(H) :=
case_if in H; auto_star.
Tactic Notation "cases_if" "*" :=
cases_if; auto_star.
Tactic Notation "cases_if" "*" "in" hyp(H) :=
cases_if in H; auto_star.
Tactic Notation "destruct_if" "*" :=
destruct_if; auto_star.
Tactic Notation "destruct_if" "*" "in" hyp(H) :=
destruct_if in H; auto_star.
Tactic Notation "destruct_head_match" "*" :=
destruct_head_match; auto_star.
Tactic Notation "decides_equality" "*" :=
decides_equality; auto_star.
Tactic Notation "splits" "*" :=
splits; auto_star.
Tactic Notation "splits" "*" constr(N) :=
splits N; auto_star.
Tactic Notation "destructs" "*" constr(T) :=
destructs T; auto_star.
Tactic Notation "destructs" "*" constr(N) constr(T) :=
destructs N T; auto_star.
Tactic Notation "branch" "*" constr(N) :=
branch N; auto_star.
Tactic Notation "branch" "*" constr(K) "of" constr(N) :=
branch K of N; auto_star.
Tactic Notation "branches" "*" constr(T) :=
branches T; auto_star.
Tactic Notation "branches" "*" constr(N) constr(T) :=
branches N T; auto_star.
Tactic Notation "exists___" "*" :=
exists___; auto_star.
Tactic Notation "exists" "*" constr(T1) :=
exists T1; auto_star.
Tactic Notation "exists" "*" constr(T1) constr(T2) :=
exists T1 T2; auto_star.
Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) :=
exists T1 T2 T3; auto_star.
Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) constr(T4) :=
exists T1 T2 T3 T4; auto_star.
Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) constr(T4)
constr(T5) :=
exists T1 T2 T3 T4 T5; auto_star.
Tactic Notation "exists" "*" constr(T1) constr(T2) constr(T3) constr(T4)
constr(T5) constr(T6) :=
exists T1 T2 T3 T4 T5 T6; auto_star.
(* ********************************************************************** *)
(** * Tactics to sort out the proof context *)
(* ---------------------------------------------------------------------- *)
(** ** Sorting hypotheses *)
(** [sort] sorts out hypotheses from the context by moving all the
propositions (hypotheses of type Prop) to the bottom of the context. *)
Ltac sort_tactic :=
match goal with H: ?T |- _ =>
match type of T with Prop =>
generalizes H; (try sort_tactic); intro
end end.
Tactic Notation "sort" :=
sort_tactic.
(* ---------------------------------------------------------------------- *)
(** ** Clearing hypotheses *)
(** [clears X1 ... XN] is a variation on [clear] which clears
the variables [X1]..[XN] as well as all the hypotheses which
depend on them. Contrary to [clear], it never fails. *)
Tactic Notation "clears" ident(X1) :=
let rec doit _ :=
match goal with
| H:context[X1] |- _ => clear H; try (doit tt)
| _ => clear X1
end in doit tt.
Tactic Notation "clears" ident(X1) ident(X2) :=
clears X1; clears X2.
Tactic Notation "clears" ident(X1) ident(X2) ident(X3) :=
clears X1; clears X2; clear X3.
Tactic Notation "clears" ident(X1) ident(X2) ident(X3) ident(X4) :=
clears X1; clears X2; clear X3; clear X4.
Tactic Notation "clears" ident(X1) ident(X2) ident(X3) ident(X4)
ident(X5) :=
clears X1; clears X2; clear X3; clear X4; clear X5.
Tactic Notation "clears" ident(X1) ident(X2) ident(X3) ident(X4)
ident(X5) ident(X6) :=
clears X1; clears X2; clear X3; clear X4; clear X5; clear X6.
(** [clears] (without any argument) clears all the unused variables
from the context. In other words, it removes any variable
which is not a proposition (i.e. not of type Prop) and which
does not appear in another hypothesis nor in the goal. *)
Ltac clears_tactic :=
match goal with H: ?T |- _ =>
match type of T with
| Prop => generalizes H; (try clears_tactic); intro
| ?TT => clear H; (try clears_tactic)
| ?TT => generalizes H; (try clears_tactic); intro
end end.
Tactic Notation "clears" :=
clears_tactic.
(** [clears_all] clears all the hypotheses from the context
that can be cleared. It leaves only the hypotheses that
are mentioned in the goal. *)
Tactic Notation "clears_all" :=
repeat match goal with H: _ |- _ => clear H end.
(** [clears_last] clears the last hypothesis in the context.
[clears_last N] clears the last [N] hypotheses in the context. *)
Tactic Notation "clears_last" :=
match goal with H: ?T |- _ => clear H end.
Ltac clears_last_base N :=
match nat_from_number N with
| 0 => idtac
| S ?p => clears_last; clears_last_base p
end.
Tactic Notation "clears_last" constr(N) :=
clears_last_base N.
(* ********************************************************************** *)
(** * Tactics for development purposes *)
(* ---------------------------------------------------------------------- *)
(** ** Skipping subgoals *)
(** The [skip] tactic can be used at any time to admit the current
goal. Using [skip] is much more efficient than using the [Focus]
top-level command to reach a particular subgoal.
There are two possible implementations of [skip]. The first one
relies on the use of an existential variable. The second one
relies on an axiom of type [False]. Remark that the builtin tactic
[admit] is not applicable if the current goal contains uninstantiated
variables.
The advantage of the first technique is that a proof using [skip]
must end with [Admitted], since [Qed] will be rejected with the message
"[uninstantiated existential variables]". It is thereafter clear
that the development is incomplete.
The advantage of the second technique is exactly the converse: one
may conclude the proof using [Qed], and thus one saves the pain from
renaming [Qed] into [Admitted] and vice-versa all the time.
Note however, that it is still necessary to instantiate all the existential
variables introduced by other tactics in order for [Qed] to be accepted.
The two implementation are provided, so that you can select the one that
suits you best. By default [skip'] uses the first implementation, and
[skip] uses the second implementation.
*)
Ltac skip_with_existential :=
match goal with |- ?G =>
let H := fresh in evar(H:G); eexact H end.
Variable skip_axiom : False.
(* To obtain a safe development, change to [skip_axiom : True] *)
Ltac skip_with_axiom :=
elimtype False; apply skip_axiom.
Tactic Notation "skip" :=
skip_with_axiom.
Tactic Notation "skip'" :=
skip_with_existential.
(** [skip H: T] adds an assumption named [H] of type [T] to the
current context, blindly assuming that it is true.
[skip: T] and [skip H_asserts: T] and [skip_asserts: T]
are other possible syntax.
Note that H may be an intro pattern.
The syntax [skip H1 .. HN: T] can be used when [T] is a
conjunction of [N] items. *)
Tactic Notation "skip" simple_intropattern(I) ":" constr(T) :=
asserts I: T; [ skip | ].
Tactic Notation "skip" ":" constr(T) :=
let H := fresh in skip H: T.
Tactic Notation "skip" simple_intropattern(I1)
simple_intropattern(I2) ":" constr(T) :=
skip [I1 I2]: T.
Tactic Notation "skip" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3) ":" constr(T) :=
skip [I1 [I2 I3]]: T.
Tactic Notation "skip" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3)
simple_intropattern(I4) ":" constr(T) :=
skip [I1 [I2 [I3 I4]]]: T.
Tactic Notation "skip" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3)
simple_intropattern(I4) simple_intropattern(I5) ":" constr(T) :=
skip [I1 [I2 [I3 [I4 I5]]]]: T.
Tactic Notation "skip" simple_intropattern(I1)
simple_intropattern(I2) simple_intropattern(I3)
simple_intropattern(I4) simple_intropattern(I5)
simple_intropattern(I6) ":" constr(T) :=
skip [I1 [I2 [I3 [I4 [I5 I6]]]]]: T.
Tactic Notation "skip_asserts" simple_intropattern(I) ":" constr(T) :=
skip I: T.
Tactic Notation "skip_asserts" ":" constr(T) :=
skip: T.
(** [skip_cuts T] simply replaces the current goal with [T]. *)
Tactic Notation "skip_cuts" constr(T) :=
cuts: T; [ skip | ].
(** [skip_goal H] applies to any goal. It simply assumes
the current goal to be true. The assumption is named "H".
It is useful to set up proof by induction or coinduction.
Syntax [skip_goal] is also accepted.*)
Tactic Notation "skip_goal" ident(H) :=
match goal with |- ?G => skip H: G end.
Tactic Notation "skip_goal" :=
let IH := fresh "IH" in skip_goal IH.
(** [skip_rewrite T] can be applied when [T] is an equality.
It blindly assumes this equality to be true, and rewrite it in
the goal. *)
Tactic Notation "skip_rewrite" constr(T) :=
let M := fresh in skip_asserts M: T; rewrite M; clear M.
(** [skip_rewrite T in H] is similar as [rewrite_skip], except that
it rewrites in hypothesis [H]. *)
Tactic Notation "skip_rewrite" constr(T) "in" hyp(H) :=
let M := fresh in skip_asserts M: T; rewrite M in H; clear M.
(** [skip_rewrites_all T] is similar as [rewrite_skip], except that
it rewrites everywhere (goal and all hypotheses). *)
Tactic Notation "skip_rewrite_all" constr(T) :=
let M := fresh in skip_asserts M: T; rewrite_all M; clear M.
(** [skip_induction E] applies to any goal. It simply assumes
the current goal to be true (the assumption is named "IH" by
default), and call [destruct E] instead of [induction E].
It is useful to try and set up a proof by induction
first, and fix the applications of the induction hypotheses
during a second pass on the proof. *)
Tactic Notation "skip_induction" constr(E) :=
let IH := fresh "IH" in skip_goal IH; destruct E.
(* ********************************************************************** *)
(** * Compatibility with standard library *)
(** The module [Program] contains definitions that conflict with the
current module. If you import [Program], either directly or indirectly
(e.g. through [Setoid] or [ZArith]), you will need to import the
compability definitions through the top-level command:
[Require Import LibTacticsCompatibility]. *)
Module LibTacticsCompatibility.
Tactic Notation "apply" "*" constr(H) :=
sapply H; auto_star.
Tactic Notation "subst" "*" :=
subst; auto_star.
End LibTacticsCompatibility.