(************************************************************************** * Useful General-Purpose Tactics for Coq * * Arthur Chargu\u00e9raud * * 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). - An improved induction tactic that saves the relevant information by introducing equalities before doing the induction and substitutes these equality in each subgoal generated by [induction]. - 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 with the idea of tactic [forward], - thanks to Georges Gonthier for the implementation trick in [applys], - thanks to Hugo Herbelin for useful feedback on several tactics. *) 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. (* ---------------------------------------------------------------------- *) (** ** Partial application of equality *) (** [= x] is a unary predicate which holds of values equal to [x]. It simply denotes the partial application of equality. *) Notation "'=' x" := (fun y => y = x) (at level 71). (* ---------------------------------------------------------------------- *) (** ** Notation for projections *) Notation "'proj21' P" := (proj1 P) (at level 69, only parsing). Notation "'proj22' P" := (proj2 P) (at level 69, only parsing). Notation "'proj31' P" := (proj1 P) (at level 69). Notation "'proj32' P" := (proj1 (proj2 P)) (at level 69). Notation "'proj33' P" := (proj2 (proj2 P)) (at level 69). Notation "'proj41' P" := (proj1 P) (at level 69). Notation "'proj42' P" := (proj1 (proj2 P)) (at level 69). Notation "'proj43' P" := (proj1 (proj2 (proj2 P))) (at level 69). Notation "'proj44' P" := (proj2 (proj2 (proj2 P))) (at level 69). Notation "'proj51' P" := (proj1 P) (at level 69). Notation "'proj52' P" := (proj1 (proj2 P)) (at level 69). Notation "'proj53' P" := (proj1 (proj2 (proj2 P))) (at level 69). Notation "'proj54' P" := (proj1 (proj2 (proj2 (proj2 P)))) (at level 69). Notation "'proj55' P" := (proj2 (proj2 (proj2 (proj2 P)))) (at level 69). (* ********************************************************************** *) (** * Tools for programming with Ltac *) (* ---------------------------------------------------------------------- *) (** ** Programming 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. (* ---------------------------------------------------------------------- *) (** ** Returning values *) (** Ltac tactics are not allowed to both perform side-effect on the goal and return a value in the same time. To work around this limitation, we can use either the current goal or the proof context as a stack to place return values. To avoid interferences, we box the return values. When the goal is used as stack, we use [ltac_tag_result] to box values. When the context is used, we use the type [Carrier] to box values. *) Definition ltac_tag_result (A:Type) (x:A) := x. (** [build_result E] changes the goal from [G] to [ltac_tag_result T -> G] where [T] is the type of [E]. *) Ltac build_result t := match type of t with ?T => let H := fresh "TEMP" in assert (H : ltac_tag_result T); [ unfold ltac_tag_result; exact t | generalize H; clear H ] end. (** [if_is_result] is the identity on a goal of the form [ltac_tag_result T -> G] and fails otherwise. *) Ltac if_is_result := match goal with |- ltac_tag_result _ -> _ => idtac end. (** [name_result H] expects a of the form [ltac_tag_result T -> G] and changes the goal to [G] by introducing an hypothesis [H:T]. *) Tactic Notation "name_result" simple_intropattern(H) := match goal with |- ltac_tag_result _ -> _ => unfold ltac_tag_result at 1; first [ intros H | let H' := fresh "NameAlreadyUsed" in intros H'] end. (** With the type [Carrier], we implement the three following tactics: - [_put x] is used to return a value (leaving it on the stack) - [_get] is used to obtain the last returned value - [_rem] is used to remove the last returned value from the context. The typicall usage is: [mytactic args; let result := _get in _rem; ...]. *) Inductive Carrier : forall A, A -> Type := | carrier : forall A x, @Carrier A x. (** [_put x] adds on hypothesis of type [Carrier x]. [_put2 x y] and [_put3 x y z] can be used for functions that return pairs or triples of values. *) Ltac _put x := generalize (carrier x); intro. Ltac _put2 x y := _put y; _put x. Ltac _put3 x y z := _put z; _put y; _put x. (** [_get] returns the value [x] contained in the last hypothesis of type [Carrier x] available in the context. If fails if there is no such hypothesis. *) Ltac _get := match goal with H: Carrier ?t |- _ => t end. (** [_rem] clears the last hypothesis of type [Carrier _]. If fails if there is no such hypothesis. *) Ltac _rem := match goal with H: Carrier ?t |- _ => clear H end. (* ---------------------------------------------------------------------- *) (** ** List of arguments for tactics *) Require Import List. (** [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 can be 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. (** [Boxer] is a datatype such that the type [list Boxer] can be used to manipulate list of values in ltac. *) Inductive Boxer : Type := | boxer : forall (A:Type), A -> Boxer. 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. Open Scope ltac_scope. (** [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. (** [ltac_args] inputs a term [E] and returns a term of type "list boxer": - if [E] is already of type "list Boxer" that starts with the value of an instantiation mode, it returns [E], - otherwise if [E] is already of type "list Boxer", it returns [(boxer Hnts)::E], in other words, mode [Hnts] is the default, - otherwise, it returns the list containing [(boxer Hnts)::(boxer E)::nil], describing the fact that there is only one argument provided, in the 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 as a relative number. In order for tactics to convert their arguments into natural numbers, we provide a conversion tactic that behaves appropriately when the module LibInt is loaded. *) Ltac nat_from_number N := constr:(N). (* ---------------------------------------------------------------------- *) (** ** Testing tactics *) (** [show tac] executes a tactic [tac] that produces a result (not performing any side-effect on the goal) 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. (* ---------------------------------------------------------------------- *) (** ** 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]. *) 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) end. (* [is_metavar E] returns whether E is a meta-variable. However, its implementation is approximative, since it returns [true] also for constants (i.e. not-applicative terms). *) Ltac is_metavar E := match E with | ?P _ _ _ _ _ _ _ _ _ => constr:(false) | ?P _ _ _ _ _ _ _ _ => constr:(false) | ?P _ _ _ _ _ _ _ => constr:(false) | ?P _ _ _ _ _ _ => constr:(false) | ?P _ _ _ _ _ => constr:(false) | ?P _ _ _ _ => constr:(false) | ?P _ _ _ => constr:(false) | ?P _ _ => constr:(false) | ?P _ => constr:(false) | ?P => constr:(true) end. (* ********************************************************************** *) (** * Backward and forward chaining *) (* ---------------------------------------------------------------------- *) (** ** Adding assumptions *) (** [lets 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. *) Tactic Notation "lets" simple_intropattern(I) ":" constr(E) := generalize E; intros I. (** [lets H1 .. HN : E] is the same as [lets \[H1 \[H2 \[.. HN\]\]\]\]:E], and thus equivalent to [destruct E as \[H1 \[H2 \[.. HN\]\]\]\]]. *) 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(I1) simple_intropattern(I2) simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) simple_intropattern(I6) ":" constr(E) := lets [I1 [I2 [I3 [I4 [I5 I6]]]]]: E. (** [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: E] is equivalent to [lets H: E], only the name [H] is automatically chosen by Coq. It is useful to type-check a term (like the top-level command [Check]), but also to add facts that are going to be used by automation. Syntax [lets: E1 .. EN] is short for [lets: E1; ..; lets: EN]. *) Tactic Notation "lets" ":" constr(E1) := generalize E1; intro. Tactic Notation "lets" ":" constr(E1) constr(E2) := lets: E1; lets: E2. Tactic Notation "lets" ":" constr(E1) constr(E2) constr(E3) := lets: E1; lets: E2; lets: E3. (** [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 *) (** [applys] 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 "applys" constr(t) := first [ 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]. This version is to be preferred for programming intensively-used tactics. *) Tactic Notation "applys_0" constr(t) := refine (@t). Tactic Notation "applys_1" constr(t) := refine (@t _). Tactic Notation "applys_2" constr(t) := refine (@t _ _). Tactic Notation "applys_3" constr(t) := refine (@t _ _ _). Tactic Notation "applys_4" constr(t) := refine (@t _ _ _ _). Tactic Notation "applys_5" constr(t) := refine (@t _ _ _ _ _). Tactic Notation "applys_6" constr(t) := refine (@t _ _ _ _ _ _). Tactic Notation "applys_7" constr(t) := refine (@t _ _ _ _ _ _ _). Tactic Notation "applys_8" constr(t) := refine (@t _ _ _ _ _ _ _ _). Tactic Notation "applys_9" constr(t) := refine (@t _ _ _ _ _ _ _ _ _). Tactic Notation "applys_10" constr(t) := refine (@t _ _ _ _ _ _ _ _ _ _). (** [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 H: (E H') | lets H: (E _ H') | lets H: (E _ _ H') | lets H: (E _ _ _ H') | lets H: (E _ _ _ _ H') | lets H: (E _ _ _ _ _ H') | lets H: (E _ _ _ _ _ _ H') | lets H: (E _ _ _ _ _ _ _ H') | lets H: (E _ _ _ _ _ _ _ _ H') | lets H: (E _ _ _ _ _ _ _ _ _ H') ] ); clear H'. (** [applys_in H E] transform the hypothesis [H] by replacing it by the result of the application of [H] to the term [E] Intuitively, it is equivalent to [lets H: (H E)]. DEPRECATED: use [specializes H E] instead. *) Tactic Notation "applys_in" hyp(H) constr(E) := let H' := fresh in rename H into H'; (first [ lets H: (H' E) | lets H: (H' _ E) | lets H: (H' _ _ E) | lets H: (H' _ _ _ E) | lets H: (H' _ _ _ _ E) | lets H: (H' _ _ _ _ _ E) | lets H: (H' _ _ _ _ _ _ E) | lets H: (H' _ _ _ _ _ _ _ E) | lets H: (H' _ _ _ _ _ _ _ _ E) | lets H: (H' _ _ _ _ _ _ _ _ _ E) ] ); clear H'. (** [applys_clear E] performs [applys E] and then calls [clear] on the head term of [E]. It fails if this head term is not an hypothesis or if it used dependently. *) Tactic Notation "applys_clear" constr(E) := applys E; let H := get_head E in clear E. Tactic Notation "apply_clear" constr(E) := applys_clear E. (** [constructors] calls [constructor] or [econstructor]. *) (* TODO: is [econstructor] stricly more powerful than [constructor]? *) Tactic Notation "constructors" := first [ constructor | econstructor ]. (* ---------------------------------------------------------------------- *) (** ** 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. (* alternative implementation: assert False; [ | contradiction ]. *) (** [false] replaces any goal by the goal [False]. Furthermore, it discharges the obligation if the context contains [False] or an hypothesis of the form [C x1 .. xN = D y1 .. yM]. *) Tactic Notation "false" := false_goal; try assumption; try discriminate. (** [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 \]]. *) Tactic Notation "tryfalse" "by" tactic(tac) "/" := try solve [ false; tac ]. (** [false T] is equivalent to [false; apply T]. It also solves the goal if [T] has type [C x1 .. xN = D y1 .. yM]. *) Tactic Notation "false" constr(T) "by" tactic(tac) "/" := false_goal; first [ first [ apply T | eapply T | applys T]; tac | let H := fresh in lets H: T; discriminate H ]. Tactic Notation "false" constr(T) := false T by idtac/. (** [false_inv] proves any goal provided there is an hypothesis [H] in the context that can be proved absurd by calling [inversion H]. *) Ltac false_inv_tactic := match goal with H:_ |- _ => solve [ inversion H | clear H; false_inv_tactic | fail 2 ] end. Tactic Notation "false_inv" := false_inv_tactic. (** [tryfalse_inv] tries to prove the goal using [false] or [false_inv], and leaves the goal unchanged if it does not succeed. *) Tactic Notation "tryfalse_inv" := try solve [ false | false_inv ]. (** [asserts H: T] is another syntax for [assert (H : T)], which also works with introduction patterns. For instance, we 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 the same as [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 as H] is another syntax for [asserts H: T] *) Tactic Notation "asserts" ":" constr(T) "as" simple_intropattern(I) := asserts I : 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 the same as [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 *) (* -- to be used once v8.1pl4 is no longer supported 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 app_arg t P v cont := let H := fresh "TEMP" in assert (H : P); [ apply v | cont(t H); try clear H ]. 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 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 match v with | ltac_wild => match type of t with | ?P -> ?Q => first [ app_assert t P cont | fail 3 ] | forall _:?A, _ => first [ app_evar t A cont | fail 3 ] end | _ => match type of t with | ?P -> ?Q => first [ app_arg t P v cont | fail 3 ] | forall _:?A, _ => first [ cont (t v) | fail 3 ] (*todo: v8.2, use: app_darg t A v cont *) 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' => match type of 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' => match type of 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. 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 match v with | ltac_wild => first [ let T := boxerlist_next_type vs' in match T with | ltac_wild => match type of t with | ?P -> ?Q => first [ app_assert t P cont' | fail 3 ] | forall _:?A, _ => first [ app_evar t A cont' | fail 3 ] end | _ => match type of t with (* should test T for unifiability *) | T -> ?Q => first [ app_assert t T cont' | fail 3 ] | forall _:T, _ => first [ app_evar t T 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 type of 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 Ei final := let args := ltac_args Ei in first [ match args with (boxer ?mode)::(boxer ?t)::?vs => 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]. (** [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 := build_app Ei ltac:(fun R => lets 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(E) := let E' := ltac_args E in let E'' := (eval simpl in (E' ++ ((boxer ___)::nil))) in lets I: E''. 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 := build_app Ei ltac:(fun R => first [ apply R | eapply R | applys R ]). Tactic Notation "applys" constr(E0) := match type of E0 with | list Boxer => applys_build E0 | _ => applys 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 Ei' := ltac_args Ei in match Ei' with (boxer ?mode)::?vs => let Ei'' := constr:((boxer mode)::(boxer H')::vs) in build_app Ei'' 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 | hnf; apply H | hnf; eapply H | applys H ]. (** [sapply] stands for "super apply". It tries [apply], [eapply], [applys] and [fapply], plus [hnf;apply] and [hnf;eapply]. *) Tactic Notation "sapply" constr(H) := first [ apply H | eapply H | applys H | hnf; apply H | hnf; eapply H | hnf; applys H | fapply H ]. (* ********************************************************************** *) (** * Introduction and generalization *) (* ---------------------------------------------------------------------- *) (** ** Introduction *) Definition ltac_tag_subst (A:Type) (x:A) := x. (** [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. *) 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. (** [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. (** [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 |-. (* ********************************************************************** *) (** * Rewriting *) (* ---------------------------------------------------------------------- *) (** ** Pattern *) (** [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 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 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. (* ---------------------------------------------------------------------- *) (** ** 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(T) := let x := fresh in sets_eq x: E; T; subst x. Tactic Notation "protects" constr(E) "do" tactic(T) "/" := protects E do T. (* ---------------------------------------------------------------------- *) (** ** 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: [asserts_rewrite] plays a similar role. *) 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 not in this form, it tries and call [intros] first. *) Ltac unfolds_callback E cont := let go E := let P := get_head E in cont P in match E with | ?A = ?B => first [ go A | go B ] | ?A => go A end. Ltac unfolds_base := match goal with |- ?G => unfolds_callback 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 => unfolds_callback 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 *. (** [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. *) Tactic Notation "unsimpl" constr(E) "in" "*" := let F := (eval simpl in E) in change F with E 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]. *) 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. (* ---------------------------------------------------------------------- *) (** ** 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]. (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 | 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 *) (* ---------------------------------------------------------------------- *) (** ** Tools for naming hypotheses generated by inversion *) (** [ltac_Mark] and [ltac_mark] are dummy definitions used as sentinel by tactics. The [ltac_mark] has type [ltac_Mark]. *) 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 | _ => generalizes 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. (* ---------------------------------------------------------------------- *) (** ** 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. *) Require Import Eqdep. Ltac inverts_tactic H i1 i2 i3 i4 i5 := let rec go i1 i2 i3 i4 i5 := 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 | |- (existT ?P ?p ?x = existT ?P ?p ?y -> _) => let H := fresh in intro H; generalize (@EqdepTheory.inj_pair2 _ P p x y H); clear H; go i1 i2 i3 i4 i5 | |- (?P -> ?Q) => i1; go i2 i3 i4 i5 ltac:(intro) | |- (forall _, _) => intro; go i1 i2 i3 i4 i5 end in generalize ltac_mark; invert keep H; go i1 i2 i3 i4 i5. (** [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). (** [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). 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). 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). 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). 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). (** [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). (* ---------------------------------------------------------------------- *) (** ** 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 := let X := fresh in sets_eq <- X Eq: E; destruct X. 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. (* ********************************************************************** *) (** * Induction *) (** [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. (** [inductions H] is a tactic similar to [induction H] except that it is able to introduce equalities in order to avoid losing information. The syntax [inductions H gen X1 .. XN end] is to be used in order to generalize variables before the induction. Syntaxes [inductions H as I] and [inductions H as I gen X1 .. XN end] are also available. For technical reasons, the tactic [inductions] will not introduce equalities for constants (e.g. if [H] has type [P 0 x], [inductions] will not save the information that the first argument is [0]). However, the tactic [inductions'] aggressively introduces equalities for all arguments, and will apply. The reason why [inductions'] is not the default tactic is that it may introduce more equalities than necessary, which slightly pollutes the induction hypotheses. *) Ltac gen_eq_for_inductions H E := let X := fresh "aux" in let HX := fresh "H" X in set (X := E) in H |-; assert (HX : ltac_tag_subst (X = E)); [ unfold ltac_tag_subst; reflexivity | clearbody X; generalizes HX ]. (* [apply_to_all_args T Tac] expects the type [T] to be of the form [P E1 .. En] and applies the tactic [Tac] to all the arguments [Ei]. *) Ltac apply_to_all_args T go := match T with | ?P ?E1 ?E2 ?E3 ?E4 ?E5 ?E6 => go E1; go E2; go E3; go E4; go E5; go E6 | ?P ?E1 ?E2 ?E3 ?E4 ?E5 => go E1; go E2; go E3; go E4; go E5 | ?P ?E1 ?E2 ?E3 ?E4 => go E1; go E2; go E3; go E4 | ?P ?E1 ?E2 ?E3 => go E1; go E2; go E3 | ?P ?E1 ?E2 => go E1; go E2 | ?P ?E1 => go E1 end. (* [gens_eqs' H] introduces equalities to name arguments in [H]. *) Tactic Notation "gen_eqs'" hyp(H) := let T := type of H in let go E := try gen_eq_for_inductions H E in apply_to_all_args T go. (* [gens_eqs H] is same as [gens_eqs' H] but it tries to be slightly more clever. As a consequence, it generates fewer equalities, but sometimes it forgets some equalities. This happens when some arguments of [H] are constants. *) Tactic Notation "gen_eqs" hyp(H) := let T := type of H in let go E := match is_metavar E with | true => idtac | false => try gen_eq_for_inductions H E end in apply_to_all_args T go. Ltac intros_head_ltac_tag_subst := try 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; intros_head_ltac_tag_subst end. Ltac inductions_post := intros_head_ltac_tag_subst; unfold ltac_tag_subst in * |-. Tactic Notation "inductions" hyp(H) := gen_eqs H; induction H; inductions_post. Tactic Notation "inductions" hyp(H) "as" simple_intropattern(I) := gen_eqs H; induction H as I; inductions_post. Tactic Notation "inductions" hyp(H) tactic(Gen) "end" := gen_eqs H; Gen; induction H; inductions_post. Tactic Notation "inductions" hyp(H) "as" simple_intropattern(I) tactic(Gen) "end" := gen_eqs H; Gen; induction H as I; inductions_post. Tactic Notation "inductions'" hyp(H) := gen_eqs' H; induction H; inductions_post. Tactic Notation "inductions'" hyp(H) "as" simple_intropattern(I) := gen_eqs' H; induction H as I; inductions_post. Tactic Notation "inductions'" hyp(H) tactic(Gen) "end" := gen_eqs' H; Gen; induction H; inductions_post. Tactic Notation "inductions'" hyp(H) "as" simple_intropattern(I) tactic(Gen) "end" := gen_eqs' H; Gen; induction H as I; inductions_post. (** [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] and [induction_wf E X as IH] are also available. *) 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) "as" ident(IH) := 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. (* ********************************************************************** *) (** * 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 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. *) Tactic Notation "splits_all" := repeat split. (* ---------------------------------------------------------------------- *) (** 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 := 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 [? | ? | ? | ? | ?] | 6 => destruct T as [? | ? | ? | ? | ? | ?] | 7 => 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. Calling [exists_ N] is short for [exists __ ... __] with [N] double-underscores. Last, [exists_] is equivalent to calling [exists_ N] for the appropriate value of [N]. *) Tactic Notation "exists_original" constr(T1) := exists T1. Tactic Notation "exists" constr(T1) := match T1 with | ltac_wild => 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. Tactic Notation "exists_" constr(N) := let rec aux N := match N with | 0 => idtac | S ?N' => esplit; aux N' end in aux N. Tactic Notation "exists_" := let N := get_goal_existential_arity in exists_ N. (* ********************************************************************** *) (** * 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 | 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 E2; auto_tilde. Tactic Notation "auto" "~" constr(E1) constr(E2) constr(E3) := lets: E1 E2 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 E2; auto_star. Tactic Notation "auto" "*" constr(E1) constr(E2) constr(E3) := lets: E1 E2 E3; auto_star. (* ---------------------------------------------------------------------- *) (** ** 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 "apply" "~" constr(H) := sapply H; auto_tilde. Tactic Notation "applys" "~" constr(H) := sapply H; auto_tilde. Tactic Notation "apply_clear" "~" constr(H) := apply_clear H; auto_tilde. Tactic Notation "applys_clear" "~" constr(H) := applys_clear 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_inv" "~" := first [ tryfalse~ | false_inv ]. 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 "lets" "~" ":" constr(E1) constr(E2) := lets: E1 E2; auto_tilde. Tactic Notation "lets" "~" ":" constr(E1) constr(E2) constr(E3) := lets: E1 E2 E3; 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 "intros_all" "~" := intros_all; 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 "substs" "~" := substs; 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 "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 "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 "apply" "*" constr(H) := sapply H; auto_star. Tactic Notation "applys" "*" constr(H) := sapply H; auto_star. Tactic Notation "apply_clear" "*" constr(H) := applys_clear H; auto_star. Tactic Notation "applys_clear" "*" constr(H) := applys_clear 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_inv" "*" := first [ tryfalse* | false_inv ]. 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 "lets" "*" ":" constr(E1) constr(E2) := lets: E1 E2; auto_star. Tactic Notation "lets" "*" ":" constr(E1) constr(E2) constr(E3) := lets: E1 E2 E3; 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 "intros_all" "*" := intros_all; 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 "substs" "*" := substs; 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 "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 "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. (** [clear_last] clears the last hypothesis in the context. [clear_last N] clears the last [N] hypothesis in the context. *) Tactic Notation "clear_last" := match goal with H: ?T |- _ => clear H end. Ltac clear_last_base n := match n with | 0 => idtac | S ?p => clear_last; clear_last_base p end. Tactic Notation "clear_last" constr(n) := clear_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. Ltac skip_with_axiom := assert False; [ apply skip_axiom | contradiction ]. (* todo: apply False_rect skip_axim *) 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. (* TODO: why needed? *) Tactic Notation "apply" "*" constr(H) := sapply H; auto_star.