| products/Sources/formale Sprachen/Coq/doc/sphinx/proof-engine/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: Sprache: Lisp
|
Untersuchungsergebnis.rst Download desHaskell {Haskell[382] Ada[591] Abap[676]}zum Wurzelverzeichnis wechseln .. _tactics: Tactics ======== A deduction rule is a link between some (unique) formula, that we call the *conclusion* and (several) formulas that we call the *premises*. A deduction rule can be read in two ways. The first one says: “if I know this and this then I can deduce this”. For instance, if I have a proof of A and a proof of B then I have a proof of A ∧ B. This is forward reasoning from premises to conclusion. The other way says: “to prove this I have to prove this and this”. For instance, to prove A ∧ B, I have to prove A and I have to prove B. This is backward reasoning from conclusion to premises. We say that the conclusion is the *goal* to prove and premises are the *subgoals*. The tactics implement *backward reasoning*. When applied to a goal, a tactic replaces this goal with the subgoals it generates. We say that a tactic reduces a goal to its subgoal(s). Each (sub)goal is denoted with a number. The current goal is numbered 1. By default, a tactic is applied to the current goal, but one can address a particular goal in the list by writing n:tactic which means “apply tactic tactic to goal number n”. We can show the list of subgoals by typing Show (see Section :ref:`requestinginformation`). Since not every rule applies to a given statement, not every tactic can be used to reduce a given goal. In other words, before applying a tactic to a given goal, the system checks that some *preconditions* are satisfied. If it is not the case, the tactic raises an error message. Tactics are built from atomic tactics and tactic expressions (which extends the folklore notion of tactical) to combine those atomic tactics. This chapter is devoted to atomic tactics. The tactic language will be described in Chapter :ref:`ltac`. Common elements of tactics -------------------------- .. _invocation-of-tactics: Invocation of tactics ~~~~~~~~~~~~~~~~~~~~~ A tactic is applied as an ordinary command. It may be preceded by a goal selector (see Section :ref:`ltac-semantics`). If no selector is specified, the default selector is used. .. _tactic_invocation_grammar: .. productionlist:: sentence tactic_invocation : `toplevel_selector` : `tactic`. : `tactic`. .. opt:: Default Goal Selector "@toplevel_selector" :name: Default Goal Selector This option controls the default selector, used when no selector is specified when applying a tactic. The initial value is 1, hence the tactics are, by default, applied to the first goal. Using value ``all`` will make it so that tactics are, by default, applied to every goal simultaneously. Then, to apply a tactic tac to the first goal only, you can write ``1:tac``. Using value ``!`` enforces that all tactics are used either on a single focused goal or with a local selector (’’strict focusing mode’’). Although more selectors are available, only ``all``, ``!`` or a single natural number are valid default goal selectors. .. _bindingslist: Bindings list ~~~~~~~~~~~~~~~~~~~ Tactics that take a term as an argument may also support a bindings list to instantiate some parameters of the term by name or position. The general form of a term with a bindings list is :n:`@term with @bindings_list` where :token:`bindings_list` can take two different forms: .. _bindings_list_grammar: .. productionlist:: bindings_list ref : `ident` : `num` bindings_list : (`ref` := `term`) ... (`ref` := `term`) : `term` ... `term` + In a bindings list of the form :n:`{+ (@ref:= @term)}`, :n:`@ref` is either an :n:`@ident` or a :n:`@num`. The references are determined according to the type of :n:`@term`. If :n:`@ref` is an identifier, this identifier has to be bound in the type of :n:`@term` and the binding provides the tactic with an instance for the parameter of this name. If :n:`@ref` is a number ``n``, it refers to the ``n``-th non dependent premise of the :n:`@term`, as determined by the type of :n:`@term`. .. exn:: No such binder. :undocumented: + A bindings list can also be a simple list of terms :n:`{* @term}`. In that case the references to which these terms correspond are determined by the tactic. In case of :tacn:`induction`, :tacn:`destruct`, :tacn:`elim` and :tacn:`case`, the terms have to provide instances for all the dependent products in the type of term while in the case of :tacn:`apply`, or of :tacn:`constructor` and its variants, only instances for the dependent products that are not bound in the conclusion of the type are required. .. exn:: Not the right number of missing arguments. :undocumented: .. _intropatterns: Intro patterns ~~~~~~~~~~~~~~ Intro patterns let you specify the name to assign to variables and hypotheses introduced by tactics. They also let you split an introduced hypothesis into multiple hypotheses or subgoals. Common tactics that accept intro patterns include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`. .. productionlist:: coq intropattern_list : `intropattern` ... `intropattern` : `empty` empty : intropattern : * : ** : `simple_intropattern` simple_intropattern : `simple_intropattern_closed` [ % `term` ... % `term` ] simple_intropattern_closed : `naming_intropattern` : _ : `or_and_intropattern` : `equality_intropattern` naming_intropattern : `ident` : ? : ?`ident` or_and_intropattern : [ `intropattern_list` | ... | `intropattern_list` ] : ( `simple_intropattern` , ... , `simple_intropattern` ) : ( `simple_intropattern` & ... & `simple_intropattern` ) equality_intropattern : -> : <- : [= `intropattern_list` ] or_and_intropattern_loc : `or_and_intropattern` : `ident` Note that the intro pattern syntax varies between tactics. Most tactics use :n:`@simple_intropattern` in the grammar. :tacn:`destruct`, :tacn:`edestruct`, :tacn:`induction`, :tacn:`einduction`, :tacn:`case`, :tacn:`ecase` and the various :tacn:`inversion` tactics use :n:`@or_and_intropattern_loc`, while :tacn:`intros` and :tacn:`eintros` use :n:`@intropattern_list`. The :n:`eqn:` construct in various tactics uses :n:`@naming_intropattern`. **Naming patterns** Use these elementary patterns to specify a name: * :n:`@ident` — use the specified name * :n:`?` — let Coq choose a name * :n:`?@ident` — generate a name that begins with :n:`@ident` * :n:`_` — discard the matched part (unless it is required for another hypothesis) * if a disjunction pattern omits a name, such as :g:`[|H2]`, Coq will choose a name **Splitting patterns** The most common splitting patterns are: * split a hypothesis in the form :n:`A /\ B` into two hypotheses :g:`H1: A` and :g:`H2: B` using the pattern :g:`(H1 & H2)` or :g:`(H1, H2)` or :g:`[H1 H2]`. :ref:`Example <intropattern_conj_ex>`. This also works on :n:`A <-> B`, which is just a notation representing :n:`(A -> B) /\ (B -> A)`. * split a hypothesis in the form :g:`A \/ B` into two subgoals using the pattern :g:`[H1|H2]`. The first subgoal will have the hypothesis :g:`H1: A` and the second subgoal will have the hypothesis :g:`H2: B`. :ref:`Example <intropattern_disj_ex>` * split a hypothesis in either of the forms :g:`A /\ B` or :g:`A \/ B` using the pattern :g:`[]`. Patterns can be nested: :n:`[[Ha|Hb] H]` can be used to split :n:`(A \/ B) /\ C`. Note that there is no equivalent to intro patterns for goals. For a goal :g:`A /\ B`, use the :tacn:`split` tactic to replace the current goal with subgoals :g:`A` and :g:`B`. For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A`, or :tacn:`right` to replace the current goal with :g:`B`. * :n:`( {+, @simple_intropattern}` ) — matches a product over an inductive type with a :ref:`single constructor <intropattern_cons_note>`. If the number of patterns equals the number of constructor arguments, then it applies the patterns only to the arguments, and :n:`( {+, @simple_intropattern} )` is equivalent to :n:`[{+ @simple_intropattern}]`. If the number of patterns equals the number of constructor arguments plus the number of :n:`let-ins`, the patterns are applied to the arguments and :n:`let-in` variables. * :n:`( {+& @simple_intropattern} )` — matches a right-hand nested term that consists of one or more nested binary inductive types such as :g:`a1 OP1 a2 OP2 ...` (where the :g:`OPn` are right-associative). (If the :g:`OPn` are left-associative, additional parentheses will be needed to make the term right-hand nested, such as :g:`a1 OP1 (a2 OP2 ...)`.) The splitting pattern can have more than 2 names, for example :g:`(H1 & H2 & H3)` matches :g:`A /\ B /\ C`. The inductive types must have a :ref:`single constructor with two parameters <intropattern_cons_note>`. :ref:`Example <intropattern_ampersand_ex>` * :n:`[ {+| @intropattern_list} ]` — splits an inductive type that has :ref:`multiple constructors <intropattern_cons_note>` such as :n:`A \/ B` into multiple subgoals. The number of :token:`intropattern_list` must be the same as the numb constructors for the matched part. * :n:`[ {+ @intropattern} ]` — splits an inductive type that has a :ref:`single constructor with multiple parameters <intropattern_cons_note>` such as :n:`A /\ B` into multiple hypotheses. Use :n:`[H1 [H2 H3]]` to match :g:`A /\ B /\ C`. * :n:`[]` — splits an inductive type: If the inductive type has multiple constructors, such as :n:`A \/ B`, create one subgoal for each constructor. If the inductive type has a single constructor with multiple parameters, such as :n:`A /\ B`, split it into multiple hypotheses. **Equality patterns** These patterns can be used when the hypothesis is an equality: * :n:`->` — replaces the right-hand side of the hypothesis with the left-hand side of the hypothesis in the conclusion of the goal; the hypothesis is cleared; if the left-hand side of the hypothesis is a variable, it is substituted everywhere in the context and the variable is removed. :ref:`Example <intropattern_rarrow_ex>` * :n:`<-` — similar to :n:`->`, but replaces the left-hand side of the hypothesis with the right-hand side of the hypothesis. * :n:`[= {*, @intropattern} ]` — If the product is over an equality type, applies either :tacn:`injection` or :tacn:`discriminate`. If :tacn:`injection` is applicable, the intropattern is used on the hypotheses generated by :tacn:`injection`. If the number of patterns is smaller than the number of hypotheses generated, the pattern :n:`?` is used to complete the list. :ref:`Example <intropattern_inj_discr_ex>` **Other patterns** * :n:`*` — introduces one or more quantified variables from the result until there are no more quantified variables. :ref:`Example <intropattern_star_ex>` * :n:`**` — introduces one or more quantified variables or hypotheses from the result until ther no more quantified variables or implications (:g:`->`). :g:`intros **` is equivalent to :g:`intros`. :ref:`Example <intropattern_2stars_ex>` * :n:`@simple_intropattern_closed {* % @term}` — first applies each of the terms with the :tacn:`apply ... in` tactic on the hypothesis to be introduced, then it uses :n:`@simple_intropattern_closed`. :ref:`Example <intropattern_injection_ex>` .. flag:: Bracketing Last Introduction Pattern For :n:`intros @intropattern_list`, controls how to handle a conjunctive pattern that doesn't give enough simple patterns to match all the arguments in the constructor. If set (the default), |Coq| generates additional names to match the number of arguments. Unsetting the option will put the additional hypotheses in the goal instead, behavior that is m similar to |SSR|'s intro patterns. .. deprecated:: 8.10 .. _intropattern_cons_note: .. note:: :n:`A \/ B` and :n:`A /\ B` use infix notation to refer to the inductive types :n:`or` and :n:`and`. :n:`or` has multiple constructors (:n:`or_introl` and :n:`or_intror`), while :n:`and` has a single constructor (:n:`conj`) with multiple parameters (:n:`A` and :n:`B`). These are defined in theories/Init/Logic.v. The "where" clauses define the infix notation for "or" and "and". .. coqdoc:: Inductive or (A B:Prop) : Prop := | or_introl : A -> A \/ B | or_intror : B -> A \/ B where "A \/ B" := (or A B) : type_scope. Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B where "A /\ B" := (and A B) : type_scope. .. note:: :n:`intros {+ p}` is not always equivalent to :n:`intros p; ... ; intros p` if some of the :n:`p` are :g:`_`. In the first form, all erasures are done at once, while they're done sequentially for each tactic in the second form. If the second matched term depends on the first matched term and the pattern for both is :g:`_` (i.e., both will be erased), the first :n:`intros` in the second form will fail because the second matched term still has the dependency on the first. Examples: .. _intropattern_conj_ex: .. example:: intro pattern for /\\ .. coqtop:: reset none Goal forall (A: Prop) (B: Prop), (A /\ B) -> True. .. coqtop:: out intros. .. coqtop:: all destruct H as (HA & HB). .. _intropattern_disj_ex: .. example:: intro pattern for \\/ .. coqtop:: reset none Goal forall (A: Prop) (B: Prop), (A \/ B) -> True. .. coqtop:: out intros. .. coqtop:: all destruct H as [HA|HB]. all: swap 1 2. .. _intropattern_rarrow_ex: .. example:: -> intro pattern .. coqtop:: reset none Goal forall (x:nat) (y:nat) (z:nat), (x = y) -> (y = z) -> (x = z). .. coqtop:: out intros * H. .. coqtop:: all intros ->. .. _intropattern_inj_discr_ex: .. example:: [=] intro pattern The first :n:`intros [=]` uses :tacn:`injection` to strip :n:`(S ...)` from both sides of the matched equality. The second uses :tacn:`discriminate` on the contradiction :n:`1 = 2` (internally represented as :n:`(S O) = (S (S O))`) to complete the goal. .. coqtop:: reset none Goal forall (n m:nat), (S n) = (S m) -> (S O)=(S (S O)) -> False. .. coqtop:: out intros *. .. coqtop:: all intros [= H]. .. coqtop:: all intros [=]. .. _intropattern_ampersand_ex: .. example:: (A & B & ...) intro pattern .. coqtop:: reset none Parameters (A : Prop) (B: nat -> Prop) (C: Prop). .. coqtop:: out Goal A /\ (exists x:nat, B x /\ C) -> True. .. coqtop:: all intros (a & x & b & c). .. _intropattern_star_ex: .. example:: * intro pattern .. coqtop:: reset out Goal forall (A: Prop) (B: Prop), A -> B. .. coqtop:: all intros *. .. _intropattern_2stars_ex: .. example:: ** pattern ("intros \**" is equivalent to "intros") .. coqtop:: reset out Goal forall (A: Prop) (B: Prop), A -> B. .. coqtop:: all intros **. .. example:: compound intro pattern .. coqtop:: reset out Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. .. coqtop:: all intros * [a | (_,c)] f. all: swap 1 2. .. _intropattern_injection_ex: .. example:: combined intro pattern using [=] -> and % .. coqtop:: reset none Require Import Coq.Lists.List. Section IntroPatterns. Variables (A : Type) (xs ys : list A). .. coqtop:: out Example ThreeIntroPatternsCombined : S (length ys) = 1 -> xs ++ ys = xs. .. coqtop:: all intros [=->%length_zero_iff_nil]. * `intros` would add :g:`H : S (length ys) = 1` * `intros [=]` would additionally apply :tacn:`injection` to :g:`H` to yield :g:`H0 : length y * `intros [=->%length_zero_iff_nil]` applies the theorem, making H the equality :g:`l=nil`, which is then applied as for :g:`->`. .. coqdoc:: Theorem length_zero_iff_nil (l : list A): length l = 0 <-> l=nil. The example is based on `Tej Chajed's coq-tricks <https://github.com/tchajed/coq-tricks .. _occurrencessets: Occurrence sets and occurrence clauses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ An occurrence clause is a modifier to some tactics that obeys the following syntax: .. productionlist:: coq occurrence_clause : in `goal_occurrences` goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [` : * |- [* [`at_occurrences`]] : * at_occurrences : at `occurrences` occurrences : [-] `num` ... `num` The role of an occurrence clause is to select a set of occurrences of a term in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate that occurrences have to be selected in the hypotheses named :token:`ident`. If no numbers are given for hypothesis :token:`ident`, then all the occurrences of :token:`term` in the hypothesis are selected. If numbers are given, they refer to occurrences of :token:`term` when the term is printed using option :flag:`Printing All`, counting from left to right. In particular, occurrences of :token:`term` in implicit arguments (see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are counted. If a minus sign is given between ``at`` and the list of occurrences, it negates the condition so that the clause denotes all the occurrences except the ones explicitly mentioned after the minus sign. As an exception to the left-to-right order, the occurrences in the return subexpression of a match are considered *before* the occurrences in the matched term. In the second case, the ``*`` on the left of ``|-`` means that all occurrences of term are selected in every hypothesis. In the first and second case, if ``*`` is mentioned on the right of ``|-``, the occurrences of the conclusion of the goal have to be selected. If some numbers are given, then only the occurrences denoted by these numbers are selected. If no numbers are given, all occurrences of :token:`term` in the goal are selected. Finally, the last notation is an abbreviation for ``* |- *``. Note also that ``|-`` is optional in the first case when no ``*`` is given. Here are some tactics that understand occurrence clauses: :tacn:`set`, :tacn:`remember`, :tacn:`induction`, :tacn:`destruct`. .. seealso:: :ref:`Managingthelocalcontext`, :ref:`caseanalysisandinduction`, :ref:`printing_constructions_full`. .. _applyingtheorems: Applying theorems --------------------- .. tacn:: exact @term :name: exact This tactic applies to any goal. It gives directly the exact proof term of the goal. Let ``T`` be our goal, let ``p`` be a term of type ``U`` then ``exact p`` succeeds iff ``T`` and ``U`` are convertible (see :ref:`Conversion-rules`). .. exn:: Not an exact proof. :undocumented: .. tacv:: eexact @term. :name: eexact This tactic behaves like :tacn:`exact` but is able to handle terms and goals with existential variables. .. tacn:: assumption :name: assumption This tactic looks in the local context for a hypothesis whose type is convertible to the goal. If it is the case, the subgoal is proved. Otherwise, it fails. .. exn:: No such assumption. :undocumented: .. tacv:: eassumption :name: eassumption This tactic behaves like :tacn:`assumption` but is able to handle goals with existential variables. .. tacn:: refine @term :name: refine This tactic applies to any goal. It behaves like :tacn:`exact` with a big difference: the user can leave some holes (denoted by ``_`` or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many subgoals as there are holes in the term. The type of holes must be either synthesized by the system or declared by an explicit cast like ``(_ : nat -> Prop)``. Any subgoal that occurs in other subgoals is automatically shelved, as if calling :tacn:`shelve_unifiable`. This low-level tactic can be useful to advanced users. .. example:: .. coqtop:: reset all Inductive Option : Set := | Fail : Option | Ok : bool -> Option. Definition get : forall x:Option, x <> Fail -> bool. refine (fun x:Option => match x return x <> Fail -> bool with | Fail => _ | Ok b => fun _ => b end). intros; absurd (Fail = Fail); trivial. Defined. .. exn:: Invalid argument. The tactic :tacn:`refine` does not know what to do with the term you gave. .. exn:: Refine passed ill-formed term. The term you gave is not a valid proof (not easy to debug in general). This message may also occur in higher-level tactics that call :tacn:`refine` internally. .. exn:: Cannot infer a term for this placeholder. :name: Cannot infer a term for this placeholder. (refine) There is a hole in the term you gave whose type cannot be inferred. Put a cast around it. .. tacv:: simple refine @term :name: simple refine This tactic behaves like refine, but it does not shelve any subgoal. It does not perform any beta-reduction either. .. tacv:: notypeclasses refine @term :name: notypeclasses refine This tactic behaves like :tacn:`refine` except it performs type checking without resolution of typeclasses. .. tacv:: simple notypeclasses refine @term :name: simple notypeclasses refine This tactic behaves like :tacn:`simple refine` except it performs type checking without resolution of typeclasses. .. flag:: Debug Unification Enables printing traces of unification steps used during elaboration/typechecking and the :tacn:`refine` tactic. .. tacn:: apply @term :name: apply This tactic applies to any goal. The argument term is a term well-formed in the local context. The tactic :tacn:`apply` tries to match the current goal against the conclusion of the type of :token:`term`. If it succeeds, then the tactic returns as many subgoals as the number of non-dependent premises of the type of term. If the conclusion of the type of :token:`term` does not match the goal *and* the conclusion is an inductive type isomorphic to a tuple type, then each component of the tuple is recursively matched to the goal in the left-to-right order. The tactic :tacn:`apply` relies on first-order unification with dependent types unless the conclusion of the type of :token:`term` is of the form :n:`P (t__1 ... t__n)` with ``P`` to be instantiated. In the latter case, the behavior depends on the form of the goal. If the goal is of the form :n:`(fun x => Q) u__1 ... u__n` and the :n:`t__i` and :n:`u__i` unify, then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise, :tacn:`apply` tries to define :g:`P` by abstracting over :g:`t_1 ... t__n` in the goal. See :tacn:`pattern` to transform the goal so that it gets the form :n:`(fun x => Q) u__1 ... u__n`. .. exn:: Unable to unify @term with @term. The :tacn:`apply` tactic failed to match the conclusion of :token:`term` and the current goal. You can help the :tacn:`apply` tactic by transforming your goal with the :tacn:`change` or :tacn:`pattern` tactics. .. exn:: Unable to find an instance for the variables {+ @ident}. This occurs when some instantiations of the premises of :token:`term` are not deducible from the unification. This is the case, for instance, when you want to apply a transitivity property. In this case, you have to use one of the variants below: .. tacv:: apply @term with {+ @term} Provides apply with explicit instantiations for all dependent premises of the type of term that do not occur in the conclusion and consequently cannot be found by unification. Notice that the collection :n:`{+ @term}` must be given according to the order of these dependent premises of the type of term. .. exn:: Not the right number of missing arguments. :undocumented: .. tacv:: apply @term with @bindings_list This also provides apply with values for instantiating premises. Here, variables are referred by names and non-dependent products by increasing numbers (see :ref:`bindings list <bindingslist>`). .. tacv:: apply {+, @term} This is a shortcut for :n:`apply @term__1; [.. | ... ; [ .. | apply @term__n] ... ]`, i.e. for the successive applications of :n:`@term`:sub:`i+1` on the last subgoal generated by :n:`apply @term__i` , starting from the application of :n:`@term__1`. .. tacv:: eapply @term :name: eapply The tactic :tacn:`eapply` behaves like :tacn:`apply` but it does not fail when no instantiations are deducible for some variables in the premises. Rather, it turns these variables into existential variables which are variables still to instantiate (see :ref:`Existential-Variables`). The instantiation is intended to be found later in the proof. .. tacv:: simple apply @term. This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms that contain no variables to instantiate. For instance, the following example does not succeed because it would require the conversion of ``id ?foo`` and :g:`O`. .. example:: .. coqtop:: all Definition id (x : nat) := x. Parameter H : forall y, id y = y. Goal O = O. Fail simple apply H. Because it reasons modulo a limited amount of conversion, :tacn:`simple apply` fails quicker than :tacn:`apply` and it is then well-suited for uses in user-defined tactics that backtrack often. Moreover, it does not traverse tuples as :tacn:`apply` does. .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} {? simple} eapply {+, @term {? with @bindings_list}} :name: simple apply; simple eapply This summarizes the different syntaxes for :tacn:`apply` and :tacn:`eapply`. .. tacv:: lapply @term :name: lapply This tactic applies to any goal, say :g:`G`. The argument term has to be well-formed in the current context, its type being reducible to a non-dependent product :g:`A -> B` with :g:`B` possibly containing products. Then it generates two subgoals :g:`B->G` and :g:`A`. Applying ``lapply H`` (where :g:`H` has type :g:`A->B` and :g:`B` does not start with a product) does the same as giving the sequence ``cut B. 2:apply H.`` where ``cut`` is described below. .. warn:: When @term contains more than one non dependent product the tactic lapply only takes i :undocumented: .. example:: Assume we have a transitive relation ``R`` on ``nat``: .. coqtop:: reset in Parameter R : nat -> nat -> Prop. Axiom Rtrans : forall x y z:nat, R x y -> R y z -> R x z. Parameters n m p : nat. Axiom Rnm : R n m. Axiom Rmp : R m p. Consider the goal ``(R n p)`` provable using the transitivity of ``R``: .. coqtop:: in Goal R n p. The direct application of ``Rtrans`` with ``apply`` fails because no value for ``y`` in ``Rtrans`` is found by ``apply``: .. coqtop:: all fail apply Rtrans. A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``. .. coqtop:: all apply (Rtrans n m p). Note that ``n`` can be inferred from the goal, so the following would work too. .. coqtop:: in restart apply (Rtrans _ m). More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the unknown m: .. coqtop:: in restart apply Rtrans with (y := m). Another solution is to mention the proof of ``(R x y)`` in ``Rtrans`` .. coqtop:: all restart apply Rtrans with (1 := Rnm). ... or the proof of ``(R y z)``. .. coqtop:: all restart apply Rtrans with (2 := Rmp). On the opposite, one can use ``eapply`` which postpones the problem of finding ``m``. Then one can apply the hypotheses ``Rnm`` and ``Rmp``. This instantiates the existential variable and completes the proof. .. coqtop:: all restart abort eapply Rtrans. apply Rnm. apply Rmp. .. note:: When the conclusion of the type of the term to ``apply`` is an inductive type isomorphic to a tuple type and ``apply`` looks recursively whether a component of the tuple matches the goal, it excludes components whose statement would result in applying an universal lemma of the form ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by setting the following option: .. flag:: Universal Lemma Under Conjunction This option, which preserves compatibility with versions of Coq prior to 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`). .. tacn:: apply @term in @ident :name: apply ... in This tactic applies to any goal. The argument :token:`term` is a term well-formed in the local context and the argument :token:`ident` is an hypothesis of the context. The tactic :n:`apply @term in @ident` tries to match the conclusion of the type of :token:`ident` against a non-dependent premise of the type of :token:`term`, trying them from right to left. If it succeeds, the statement of hypothesis :token:`ident` is replaced by the conclusion of the type of :token:`term`. The tactic also returns as many subgoals as the number of other non-dependent premises in the type of :token:`term` and of the non-dependent premises of the type of :token:`ident`. If the conclusion of the type of :token:`term` does not match the goal *and* the conclusion is an inductive type isomorphic to a tuple type, then the tuple is (recursively) decomposed and the first component of the tuple of which a non-dependent premise matches the conclusion of the type of :token:`ident`. Tuples are decomposed in a width-first left-to-right order (for instance if the type of :g:`H1` is :g:`A <-> B` and the type of :g:`H2` is :g:`A` then :g:`apply H1 in H2` transforms the type of :g:`H2` into :g:`B`). The tactic :tacn:`apply` relies on first-order pattern matching with dependent types. .. exn:: Statement without assumptions. This happens if the type of :token:`term` has no non-dependent premise. .. exn:: Unable to apply. This happens if the conclusion of :token:`ident` does not match any of the non-dependent premises of the type of :token:`term`. .. tacv:: apply {+, @term} in @ident This applies each :token:`term` in sequence in :token:`ident`. .. tacv:: apply {+, @term with @bindings_list} in @ident This does the same but uses the bindings in each :n:`(@ident := @term)` to instantiate the parameters of the corresponding type of :token:`term` (see :ref:`bindings list <bindingslist>`). .. tacv:: eapply {+, @term {? with @bindings_list } } in @ident This works as :tacn:`apply ... in` but turns unresolved bindings into existential variables, if any, instead of failing. .. tacv:: apply {+, @term {? with @bindings_list } } in @ident as @simple_intropattern :name: apply ... in ... as This works as :tacn:`apply ... in` then applies the :token:`simple_intropattern` to the hypothesis :token:`ident`. .. tacv:: simple apply @term in @ident This behaves like :tacn:`apply ... in` but it reasons modulo conversion only on subterms that contain no variables to instantiate. For instance, if :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and :g:`H0 : O = O` then :g:`simple apply H in H0` does not succeed because it would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is an existential variable to instantiate. Tactic :n:`simple apply @term in @ident` does not either traverse tuples as :n:`apply @term in @ident` does. .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropat {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern} This summarizes the different syntactic variants of :n:`apply @term in @ident` and :n:`eapply @term in @ident`. .. tacn:: constructor @num :name: constructor This tactic applies to a goal such that its conclusion is an inductive type (say :g:`I`). The argument :token:`num` must be less or equal to the numbers of constructor(s) of :g:`I`. Let :n:`c__i` be the i-th constructor of :g:`I`, then :g:`constructor i` is equivalent to :n:`intros; apply c__i`. .. exn:: Not an inductive product. :undocumented: .. exn:: Not enough constructors. :undocumented: .. tacv:: constructor This tries :g:`constructor 1` then :g:`constructor 2`, ..., then :g:`constructor n` where ``n`` is the number of constructors of the head of the goal. .. tacv:: constructor @num with @bindings_list Let ``c`` be the i-th constructor of :g:`I`, then :n:`constructor i with @bindings_list` is equivalent to :n:`intros; apply c with @bindings_list`. .. warning:: The terms in the :token:`bindings_list` are checked in the context where constructor is executed and not in the context where :tacn:`apply` is executed (the introductions are not taken into account). .. tacv:: split {? with @bindings_list } :name: split This applies only if :g:`I` has a single constructor. It is then equivalent to :n:`constructor 1 {? with @bindings_list }`. It is typically used in the case of a conjunction :math:`A \wedge B`. .. tacv:: exists @bindings_list :name: exists This applies only if :g:`I` has a single constructor. It is then equivalent to :n:`intros; constructor 1 with @bindings_list.` It is typically used in the case of an existential quantification :math:`\exists x, P(x).` .. tacv:: exists {+, @bindings_list } This iteratively applies :n:`exists @bindings_list`. .. exn:: Not an inductive goal with 1 constructor. :undocumented: .. tacv:: left {? with @bindings_list } right {? with @bindings_list } :name: left; right These tactics apply only if :g:`I` has two constructors, for instance in the case of a disjunction :math:`A \vee B`. Then, they are respectively equivalent to :n:`constructor 1 {? with @bindings_list }` and :n:`constructor 2 {? with @bindings_list }`. .. exn:: Not an inductive goal with 2 constructors. :undocumented: .. tacv:: econstructor eexists esplit eleft eright :name: econstructor; eexists; esplit; eleft; eright These tactics and their variants behave like :tacn:`constructor`, :tacn:`exists`, :tacn:`split`, :tacn:`left`, :tacn:`right` and their variants but they introduce existential variables instead of failing when the instantiation of a variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`). .. flag:: Debug Tactic Unification Enables printing traces of unification steps in tactic unification. Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`. .. _managingthelocalcontext: Managing the local context ------------------------------ .. tacn:: intro :name: intro This tactic applies to a goal that is either a product or starts with a let-binder. If the goal is a product, the tactic implements the "Lam" rule given in :ref:`Typing-rules` [1]_. If the goal starts with a let-binder, then the tactic implements a mix of the "Let" and "Conv". If the current goal is a dependent product :g:`forall x:T, U` (resp :g:`let x:=t in U`) then :tacn:`intro` puts :g:`x:T` (resp :g:`x:=t`) in the local context. The new subgoal is :g:`U`. If the goal is a non-dependent product :math:`T \rightarrow U`, then it puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or :g:`Prop`) or :g:`Xn:T` (if the type of :g:`T` is :g:`Type`). The optional index ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the new subgoal is :g:`U`. If the goal is an existential variable, :tacn:`intro` forces the resolution of the existential variable into a dependent product :math:`\forall`\ :g:`x:?X, ?Y`, puts :g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to depend on :g:`x`. The tactic :tacn:`intro` applies the tactic :tacn:`hnf` until :tacn:`intro` can be applied or the goal is not head-reducible. .. exn:: No product even after head-reduction. :undocumented: .. tacv:: intro @ident This applies :tacn:`intro` but forces :token:`ident` to be the name of the introduced hypothesis. .. exn:: @ident is already used. :undocumented: .. note:: If a name used by intro hides the base name of a global constant then the latter can still be referred to by a qualified name (see :ref:`Qualified-names`). .. tacv:: intros :name: intros This repeats :tacn:`intro` until it meets the head-constant. It never reduces head-constants and it never fails. .. tacv:: intros {+ @ident}. This is equivalent to the composed tactic :n:`intro @ident; ... ; intro @ident`. .. tacv:: intros until @ident This repeats intro until it meets a premise of the goal having the form :n:`(@ident : @type)` and discharges the variable named :token:`ident` of the current goal. .. exn:: No such hypothesis in current goal. :undocumented: .. tacv:: intros until @num This repeats :tacn:`intro` until the :token:`num`\-th non-dependent product. .. example:: On the subgoal :g:`forall x y : nat, x = y -> y = x` the tactic :n:`intros until 1` is equivalent to :n:`intros x y H`, as :g:`x = y -> y = x` is the first non-dependent product. On the subgoal :g:`forall x y z : nat, x = y -> y = x` the tactic :n:`intros until 1` is equivalent to :n:`intros x y z` as the product on :g:`z` can be rewritten as a non-dependent product: :g:`forall x y : nat, nat -> x = y -> y = x`. .. exn:: No such hypothesis in current goal. This happens when :token:`num` is 0 or is greater than the number of non-dependent products of the goal. .. tacv:: intro {? @ident__1 } after @ident__2 intro {? @ident__1 } before @ident__2 intro {? @ident__1 } at top intro {? @ident__1 } at bottom These tactics apply :n:`intro {? @ident__1}` and move the freshly introduced hypothesis respectively after the hypothesis :n:`@ident__2`, before the hypothesis :n:`@ident__2`, at the top of the local context, or at the bottom of the local context. All hypotheses on which the new hypothesis depends are moved too so as to respect the order of dependencies between hypotheses. It is equivalent to :n:`intro {? @ident__1 }` followed by the appropriate call to :tacn:`move ... after ...`, :tacn:`move ... before ...`, :tacn:`move ... at top`, or :tacn:`move ... at bottom`. .. note:: :n:`intro at bottom` is a synonym for :n:`intro` with no argument. .. exn:: No such hypothesis: @ident. :undocumented: .. tacn:: intros @intropattern_list :name: intros ... Introduces one or more variables or hypotheses from the goal by matching the intro patterns. See the description in :ref:`intropatterns`. .. tacn:: eintros @intropattern_list :name: eintros Works just like :tacn:`intros ...` except that it creates existential variables for any unresolved variables rather than failing. .. tacn:: clear @ident :name: clear This tactic erases the hypothesis named :n:`@ident` in the local context of the current goal. As a consequence, :n:`@ident` is no more displayed and no more usable in the proof development. .. exn:: No such hypothesis. :undocumented: .. exn:: @ident is used in the conclusion. :undocumented: .. exn:: @ident is used in the hypothesis @ident. :undocumented: .. tacv:: clear {+ @ident} This is equivalent to :n:`clear @ident. ... clear @ident.` .. tacv:: clear - {+ @ident} This variant clears all the hypotheses except the ones depending in the hypotheses named :n:`{+ @ident}` and in the goal. .. tacv:: clear This variants clears all the hypotheses except the ones the goal depends on. .. tacv:: clear dependent @ident This clears the hypothesis :token:`ident` and all the hypotheses that depend on it. .. tacv:: clearbody {+ @ident} :name: clearbody This tactic expects :n:`{+ @ident}` to be local definitions and clears their respective bodies. In other words, it turns the given definitions into assumptions. .. exn:: @ident is not a local definition. :undocumented: .. tacn:: revert {+ @ident} :name: revert This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses (possibly defined) to the goal, if this respects dependencies. This tactic is the inverse of :tacn:`intro`. .. exn:: No such hypothesis. :undocumented: .. exn:: @ident__1 is used in the hypothesis @ident__2. :undocumented: .. tacv:: revert dependent @ident :name: revert dependent This moves to the goal the hypothesis :token:`ident` and all the hypotheses that depend on it. .. tacn:: move @ident__1 after @ident__2 :name: move ... after ... This moves the hypothesis named :n:`@ident__1` in the local context after the hypothesis named :n:`@ident__2`, where “after” is in reference to the direction of the move. The proof term is not changed. If :n:`@ident__1` comes before :n:`@ident__2` in the order of dependencies, then all the hypotheses between :n:`@ident__1` and :n:`@ident__2` that (possibly indirectly) depend on :n:`@ident__1` are moved too, and all of them are thus moved after :n:`@ident__2` in the order of dependencies. If :n:`@ident__1` comes after :n:`@ident__2` in the order of dependencies, then all the hypotheses between :n:`@ident__1` and :n:`@ident__2` that (possibly indirectly) occur in the type of :n:`@ident__1` are moved too, and all of them are thus moved before :n:`@ident__2` in the order of dependencies. .. tacv:: move @ident__1 before @ident__2 :name: move ... before ... This moves :n:`@ident__1` towards and just before the hypothesis named :n:`@ident__2`. As for :tacn:`move ... after ...`, dependencies over :n:`@ident__1` (when :n:`@ident__1` comes before :n:`@ident__2` in the order of dependencies) or in the type of :n:`@ident__1` (when :n:`@ident__1` comes after :n:`@ident__2` in the order of dependencies) are moved too. .. tacv:: move @ident at top :name: move ... at top This moves :token:`ident` at the top of the local context (at the beginning of the context). .. tacv:: move @ident at bottom :name: move ... at bottom This moves :token:`ident` at the bottom of the local context (at the end of the context). .. exn:: No such hypothesis. :undocumented: .. exn:: Cannot move @ident__1 after @ident__2: it occurs in the type of @ident__2. :undocumented: .. exn:: Cannot move @ident__1 after @ident__2: it depends on @ident__2. :undocumented: .. example:: .. coqtop:: reset all Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. intros x H z y H0. move x after H0. Undo. move x before H0. Undo. move H0 after H. Undo. move H0 before H. .. tacn:: rename @ident__1 into @ident__2 :name: rename This renames hypothesis :n:`@ident__1` into :n:`@ident__2` in the current context. The name of the hypothesis in the proof-term, however, is left unchanged. .. tacv:: rename {+, @ident__i into @ident__j} This renames the variables :n:`@ident__i` into :n:`@ident__j` in parallel. In particular, the target identifiers may contain identifiers that exist in the source context, as long as the latter are also renamed by the same tactic. .. exn:: No such hypothesis. :undocumented: .. exn:: @ident is already used. :undocumented: .. tacn:: set (@ident := @term) :name: set This replaces :token:`term` by :token:`ident` in the conclusion of the current goal and adds the new definition :n:`@ident := @term` to the local context. If :token:`term` has holes (i.e. subexpressions of the form “`_`”), the tactic first checks that all subterms matching the pattern are compatible before doing the replacement using the leftmost subterm matching the pattern. .. exn:: The variable @ident is already defined. :undocumented: .. tacv:: set (@ident := @term) in @goal_occurrences This notation allows specifying which occurrences of :token:`term` have to be substituted in the context. The :n:`in @goal_occurrences` clause is an occurrence clause whose syntax and behavior are described in :ref:`goal occurrences <occurrencessets>`. .. tacv:: set (@ident @binders := @term) {? in @goal_occurrences } This is equivalent to :n:`set (@ident := fun @binders => @term) {? in @goal_occurrences }`. .. tacv:: set @term {? in @goal_occurrences } This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }` but :token:`ident` is generated by Coq. .. tacv:: eset (@ident {? @binders } := @term) {? in @goal_occurrences } eset @term {? in @goal_occurrences } :name: eset; _ While the different variants of :tacn:`set` expect that no existential variables are generated by the tactic, :tacn:`eset` removes this constraint. In practice, this is relevant only when :tacn:`eset` is used as a synonym of :tacn:`epose`, i.e. when the :token:`term` does not occur in the goal. .. tacn:: remember @term as @ident__1 {? eqn:@naming_intropattern } :name: remember This behaves as :n:`set (@ident := @term) in *`, using a logical (Leibniz’s) equality instead of a local definition. Use :n:`@naming_intropattern` to name or split up the new equation. .. tacv:: remember @term as @ident__1 {? eqn:@naming_intropattern } in @goal_occurrences This is a more general form of :tacn:`remember` that remembers the occurrences of :token:`term` specified by an occurrence set. .. tacv:: eremember @term as @ident__1 {? eqn:@naming_intropattern } {? in @goal_occurrence :name: eremember While the different variants of :tacn:`remember` expect that no existential variables are generated by the tactic, :tacn:`eremember` removes this constraint. .. tacn:: pose (@ident := @term) :name: pose This adds the local definition :n:`@ident := @term` to the current context without performing any replacement in the goal or in the hypotheses. It is equivalent to :n:`set (@ident := @term) in |-`. .. tacv:: pose (@ident @binders := @term) This is equivalent to :n:`pose (@ident := fun @binders => @term)`. .. tacv:: pose @term This behaves as :n:`pose (@ident := @term)` but :token:`ident` is generated by Coq. .. tacv:: epose (@ident {? @binders} := @term) epose @term :name: epose; _ While the different variants of :tacn:`pose` expect that no existential variables are generated by the tactic, :tacn:`epose` removes this constraint. .. tacn:: decompose [{+ @qualid}] @term :name: decompose This tactic recursively decomposes a complex proposition in order to obtain atomic ones. .. example:: .. coqtop:: reset all Goal forall A B C:Prop, A /\ B /\ C \/ B /\ C \/ C /\ A -> C. intros A B C H; decompose [and or] H. all: assumption. Qed. .. note:: :tacn:`decompose` does not work on right-hand sides of implications or products. .. tacv:: decompose sum @term This decomposes sum types (like :g:`or`). .. tacv:: decompose record @term This decomposes record types (inductive types with one constructor, like :g:`and` and :g:`exists` and those defined with the :cmd:`Record` command. .. _controllingtheproofflow: Controlling the proof flow ------------------------------ .. tacn:: assert (@ident : @type) :name: assert This tactic applies to any goal. :n:`assert (H : U)` adds a new hypothesis of name :n:`H` asserting :g:`U` to the current goal and opens a new subgoal :g:`U` [2]_. The subgoal :g:`U` comes first in the list of subgoals remaining to prove. .. exn:: Not a proposition or a type. Arises when the argument :token:`type` is neither of type :g:`Prop`, :g:`Set` nor :g:`Type`. .. tacv:: assert @type This behaves as :n:`assert (@ident : @type)` but :n:`@ident` is generated by Coq. .. tacv:: assert @type by @tactic This tactic behaves like :tacn:`assert` but applies tactic to solve the subgoals generated by assert. .. exn:: Proof is not complete. :name: Proof is not complete. (assert) :undocumented: .. tacv:: assert @type as @simple_intropattern If :n:`simple_intropattern` is an intro pattern (see :ref:`intropatterns`), the hypothesis is named after this introduction pattern (in particular, if :n:`simple_intropattern` is :n:`@ident`, the tactic behaves like :n:`assert (@ident : @type)`). If :n:`simple_intropattern` is an action introduction pattern, the tactic behaves like :n:`assert @type` followed by the action done by this introduction pattern. .. tacv:: assert @type as @simple_intropattern by @tactic This combines the two previous variants of :tacn:`assert`. .. tacv:: assert (@ident := @term) This behaves as :n:`assert (@ident : @type) by exact @term` where :token:`type` is the type of :token:`term`. This is equivalent to using :tacn:`pose proof`. If the head of term is :token:`ident`, the tactic behaves as :tacn:`specialize`. .. exn:: Variable @ident is already declared. :undocumented: .. tacv:: eassert @type as @simple_intropattern by @tactic :name: eassert While the different variants of :tacn:`assert` expect that no existential variables are generated by the tactic, :tacn:`eassert` removes this constraint. This lets you avoid specifying the asserted statement completely before starting to prove it. .. tacv:: pose proof @term {? as @simple_intropattern} :name: pose proof This tactic behaves like :n:`assert @type {? as @simple_intropattern} by exact @term` where :token:`type` is the type of :token:`term`. In particular, :n:`pose proof @term as @ident` behaves as :n:`assert (@ident := @term)` and :n:`pose proof @term as @simple_intropattern` is the same as applying the :token:`simple_intropattern` to :token:`term`. .. tacv:: epose proof @term {? as @simple_intropattern} :name: epose proof While :tacn:`pose proof` expects that no existential variables are generated by the tactic, :tacn:`epose proof` removes this constraint. .. tacv:: enough (@ident : @type) :name: enough This adds a new hypothesis of name :token:`ident` asserting :token:`type` to the goal the tactic :tacn:`enough` is applied to. A new subgoal stating :token:`type` is inserted after the initial goal rather than before it as :tacn:`assert` would do. .. tacv:: enough @type This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of the hypothesis generated by Coq. .. tacv:: enough @type as @simple_intropattern This behaves like :n:`enough @type` using :token:`simple_intropattern` to name or destruct the new hypothesis. .. tacv:: enough (@ident : @type) by @tactic enough @type {? as @simple_intropattern } by @tactic This behaves as above but with :token:`tactic` expected to solve the initial goal after the extra assumption :token:`type` is added and possibly destructed. If the :n:`as @simple_intropattern` clause generates more than one subgoal, :token:`tactic` is applied to all of them. .. tacv:: eenough @type {? as @simple_intropattern } {? by @tactic } eenough (@ident : @type) {? by @tactic } :name: eenough; _ While the different variants of :tacn:`enough` expect that no existential variables are generated by the tactic, :tacn:`eenough` removes this constraint. .. tacv:: cut @type :name: cut This tactic applies to any goal. It implements the non-dependent case of the “App” rule given in :ref:`typing-rules`. (This is Modus Ponens inference rule.) :n:`cut U` transforms the current goal :g:`T` into the two following subgoals: :g:`U -> T` and :g:`U`. The subgoal :g:`U -> T` comes first in the list of remaining subgoal to prove. .. tacv:: specialize (@ident {* @term}) {? as @simple_intropattern} specialize @ident with @bindings_list {? as @simple_intropattern} :name: specialize; _ This tactic works on local hypothesis :n:`@ident`. The premises of this hypothesis (either universal quantifications or non-dependent implications) are instantiated by concrete terms coming either from arguments :n:`{* @term}` or from a :ref:`bindings list <bindingslist>`. In the first form the application to :n:`{* @term}` can be partial. The first form is equivalent to :n:`assert (@ident := @ident {* @term})`. In the second form, instantiation elements can also be partial. In this case the uninstantiated arguments are inferred by unification if possible or left quantified in the hypothesis otherwise. With the :n:`as` clause, the local hypothesis :n:`@ident` is left unchanged and instead, the modified hypothesis is introduced as specified by the :token:`simple_intropattern`. The name :n:`@ident` can also refer to a global lemma or hypothesis. In this case, for compatibility reasons, the behavior of :tacn:`specialize` is close to that of :tacn:`generalize`: the instantiated statement becomes an additional premise of the goal. The ``as`` clause is especially useful in this case to immediately introduce the instantiated statement as a local hypothesis. .. exn:: @ident is used in hypothesis @ident. :undocumented: .. exn:: @ident is used in conclusion. :undocumented: .. tacn:: generalize @term :name: generalize This tactic applies to any goal. It generalizes the conclusion with respect to some term. .. example:: .. coqtop:: reset none Goal forall x y:nat, 0 <= x + y + y. Proof. intros *. .. coqtop:: all Show. generalize (x + y + y). If the goal is :g:`G` and :g:`t` is a subterm of type :g:`T` in the goal, then :n:`generalize t` replaces the goal by :g:`forall (x:T), G′` where :g:`G′` is obtained from :g:`G` by replacing all occurrences of :g:`t` by :g:`x`. The name of the variable (here :g:`n`) is chosen based on :g:`T`. .. tacv:: generalize {+ @term} This is equivalent to :n:`generalize @term; ... ; generalize @term`. Note that the sequence of term :sub:`i` 's are processed from n to 1. .. tacv:: generalize @term at {+ @num} This is equivalent to :n:`generalize @term` but it generalizes only over the specified occurrences of :n:`@term` (counting from left to right on the expression printed using option :flag:`Printing All`). .. tacv:: generalize @term as @ident This is equivalent to :n:`generalize @term` but it uses :n:`@ident` to name the generalized hypothesis. .. tacv:: generalize {+, @term at {+ @num} as @ident} This is the most general form of :n:`generalize` that combines the previous behaviors. .. tacv:: generalize dependent @term This generalizes term but also *all* hypotheses that depend on :n:`@term`. It clears the generalized hypotheses. .. tacn:: evar (@ident : @term) :name: evar The :n:`evar` tactic creates a new local definition named :n:`@ident` with type :n:`@term` in the context. The body of this binding is a fresh existential variable. .. tacn:: instantiate (@ident := @term ) :name: instantiate The instantiate tactic refines (see :tacn:`refine`) an existential variable :n:`@ident` with the term :n:`@term`. It is equivalent to :n:`only [ident]: refine @term` (preferred alternative). .. note:: To be able to refer to an existential variable by name, the user must have given the name explicitly (see :ref:`Existential-Variables`). .. note:: When you are referring to hypotheses which you did not name explicitly, be aware that Coq may make a different decision on how to name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors. .. tacv:: instantiate (@num := @term) This variant allows to refer to an existential variable which was not named by the user. The :n:`@num` argument is the position of the existential variable from right to left in the goal. Because this variant is not robust to slight changes in the goal, its use is strongly discouraged. .. tacv:: instantiate ( @num := @term ) in @ident instantiate ( @num := @term ) in ( value of @ident ) instantiate ( @num := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition. .. tacv:: instantiate Without argument, the instantiate tactic tries to solve as many existential variables as possible, using information gathered from other tactics in the same tactical. This is automatically done after each complete tactic (i.e. after a dot in proof mode), but not, for example, between each tactic when they are sequenced by semicolons. .. tacn:: admit :name: admit This tactic allows temporarily skipping a subgoal so as to progress further in the rest of the proof. A proof containing admitted goals cannot be closed with :cmd:`Qed` but only with :cmd:`Admitted`. .. tacv:: give_up Synonym of :tacn:`admit`. .. tacn:: absurd @term :name: absurd This tactic applies to any goal. The argument term is any proposition :g:`P` of type :g:`Prop`. This tactic applies False elimination, that is it deduces the current goal from False, and generates as subgoals :g:`∼P` and :g:`P`. It is very useful in proofs by cases, where some cases are impossible. In most cases, :g:`P` or :g:`∼P` is one of the hypotheses of the local context. .. tacn:: contradiction :name: contradiction This tactic applies to any goal. The contradiction tactic attempts to find in the current context (after all intros) a hypothesis that is equivalent to an empty inductive type (e.g. :g:`False`), to the negation of a singleton inductive type (e.g. :g:`True` or :g:`x=x`), or two contradictory hypotheses. .. exn:: No such assumption. :undocumented: .. tacv:: contradiction @ident The proof of False is searched in the hypothesis named :n:`@ident`. .. tacn:: contradict @ident :name: contradict This tactic allows manipulating negated hypothesis and goals. The name :n:`@ident` should correspond to a hypothesis. With :n:`contradict H`, the current goal and context is transformed in the following way: + H:¬A ⊢ B becomes ⊢ A + H:¬A ⊢ ¬B becomes H: B ⊢ A + H: A ⊢ B becomes ⊢ ¬A + H: A ⊢ ¬B becomes H: B ⊢ ¬A .. tacn:: exfalso :name: exfalso This tactic implements the “ex falso quodlibet” logical principle: an elimination of False is performed on the current goal, and the user is then required to prove that False is indeed provable in the current context. This tactic is a macro for :n:`elimtype False`. .. _CaseAnalysisAndInduction: Case analysis and induction ------------------------------- The tactics presented in this section implement induction or case analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`). .. tacn:: destruct @term :name: destruct This tactic applies to any goal. The argument :token:`term` must be of inductive or co-inductive type and the tactic generates subgoals, one for each possible form of :token:`term`, i.e. one for each constructor of the inductive or co-inductive type. Unlike :tacn:`induction`, no induction hypothesis is generated by :tacn:`destruct`. .. tacv:: destruct @ident If :token:`ident` denotes a quantified variable of the conclusion of the goal, then :n:`destruct @ident` behaves as :n:`intros until @ident; destruct @ident`. If :token:`ident` is not anymore dependent in the goal after application of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). If :token:`ident` is a hypothesis of the context, and :token:`ident` is not anymore dependent in the goal after application of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). .. tacv:: destruct @num :n:`destruct @num` behaves as :n:`intros until @num` followed by destruct applied to the last introduced hypothesis. .. note:: For destruction of a numeral, use syntax :n:`destruct (@num)` (not very interesting anyway). .. tacv:: destruct @pattern The argument of :tacn:`destruct` can also be a pattern of which holes are denoted by “_”. In this case, the tactic checks that all subterms matching the pattern in the conclusion and the hypotheses are compatible and performs case analysis using this subterm. .. tacv:: destruct {+, @term} This is a shortcut for :n:`destruct @term; ...; destruct @term`. .. tacv:: destruct @term as @or_and_intropattern_loc This behaves as :n:`destruct @term` but uses the names in :token:`or_and_intropattern_loc` to name the variables introduced in the context. The :token:`or_and_intropattern_loc` must have the form :n:`[p11 ... p1n | ... | pm1 ... pmn ]` with ``m`` being the number of constructors of the type of :token:`term`. Each variable introduced by :tacn:`destruct` in the context of the ``i``-th goal gets its name from the list :n:`pi1 ... pin` in order. If there are not enough names, :tacn:`destruct` invents names for the remaining variables to introduce. More generally, the :n:`pij` can be any introduction pattern (see :tacn:`intros`). This provides a concise notation for chaining destruction of a hypothesis. .. tacv:: destruct @term eqn:@naming_intropattern :name: destruct ... eqn: This behaves as :n:`destruct @term` but adds an equation between :token:`term` and the value that it takes in each of the possible cases. The name of the equation is specified by :token:`naming_intropattern` (see :tacn:`intros`), in particular ``?`` can be used to let Coq generate a fresh name. .. tacv:: destruct @term with @bindings_list This behaves like :n:`destruct @term` providing explicit instances for the dependent premises of the type of :token:`term`. .. tacv:: edestruct @term :name: edestruct This tactic behaves like :n:`destruct @term` except that it does not fail if the instance of a dependent premises of the type of :token:`term` is not inferable. Instead, the unresolved instances are left as existential variables to be inferred later, in the same way as :tacn:`eapply` does. .. tacv:: destruct @term using @term {? with @bindings_list } This is synonym of :n:`induction @term using @term {? with @bindings_list }`. .. tacv:: destruct @term in @goal_occurrences This syntax is used for selecting which occurrences of :token:`term` the case analysis has to be done on. The :n:`in @goal_occurrences` clause is an occurrence clause whose syntax and behavior is described in :ref:`occurrences sets <occurrencessets>`. --> -------------------- --> maximum size reached --> -------------------- [ zur Elbe Produktseite wechseln0.336Quellennavigators ] |