diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 187 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 35 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 294 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 961 |
4 files changed, 936 insertions, 541 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 1071682ead..c134563efe 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -41,117 +41,121 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: - - The infix tacticals “… \|\| …”, “… + …”, and “… ; …” are associative. + - The infix tacticals ``… || …`` , ``… + …`` , and ``… ; …`` are associative. - - In :token:`tacarg`, there is an overlap between qualid as a direct tactic - argument and :token:`qualid` as a particular case of term. The resolution is - done by first looking for a reference of the tactic language and if - it fails, for a reference to a term. To force the resolution as a - reference of the tactic language, use the form :g:`ltac:(@qualid)`. To - force the resolution as a reference to a term, use the syntax - :g:`(@qualid)`. + .. example:: - - As shown by the figure, tactical ``\|\|`` binds more than the prefix - tacticals try, repeat, do and abstract which themselves bind more - than the postfix tactical “… ;[ … ]” which binds more than “… ; …”. + If you want that :n:`@tactic__2; @tactic__3` be fully run on the first + subgoal generated by :n:`@tactic__1`, before running on the other + subgoals, then you should not write + :n:`@tactic__1; (@tactic__2; @tactic__3)` but rather + :n:`@tactic__1; [> @tactic__2; @tactic__3 .. ]`. - For instance + - In :token:`tacarg`, there is an overlap between :token:`qualid` as a + direct tactic argument and :token:`qualid` as a particular case of + :token:`term`. The resolution is done by first looking for a reference + of the tactic language and if it fails, for a reference to a term. + To force the resolution as a reference of the tactic language, use the + form :n:`ltac:(@qualid)`. To force the resolution as a reference to a + term, use the syntax :n:`(@qualid)`. - .. coqtop:: in + - As shown by the figure, tactical ``… || …`` binds more than the prefix + tacticals :tacn:`try`, :tacn:`repeat`, :tacn:`do` and :tacn:`abstract` + which themselves bind more than the postfix tactical ``… ;[ … ]`` + which binds at the same level as ``… ; …`` . - try repeat tac1 || tac2; tac3; [tac31 | ... | tac3n]; tac4. + .. example:: - is understood as + :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; [ {+| @tactic } ]; @tactic__4` - .. coqtop:: in + is understood as: - try (repeat (tac1 || tac2)); - ((tac3; [tac31 | ... | tac3n]); tac4). + :n:`((try (repeat (@tactic__1 || @tactic__2)); @tactic__3); [ {+| @tactic } ]); @tactic__4` .. productionlist:: coq expr : `expr` ; `expr` - : | [> `expr` | ... | `expr` ] - : | `expr` ; [ `expr` | ... | `expr` ] - : | `tacexpr3` - tacexpr3 : do (`natural` | `ident`) tacexpr3 - : | progress `tacexpr3` - : | repeat `tacexpr3` - : | try `tacexpr3` - : | once `tacexpr3` - : | exactly_once `tacexpr3` - : | timeout (`natural` | `ident`) `tacexpr3` - : | time [`string`] `tacexpr3` - : | only `selector`: `tacexpr3` - : | `tacexpr2` + : [> `expr` | ... | `expr` ] + : `expr` ; [ `expr` | ... | `expr` ] + : `tacexpr3` + tacexpr3 : do (`natural` | `ident`) `tacexpr3` + : progress `tacexpr3` + : repeat `tacexpr3` + : try `tacexpr3` + : once `tacexpr3` + : exactly_once `tacexpr3` + : timeout (`natural` | `ident`) `tacexpr3` + : time [`string`] `tacexpr3` + : only `selector`: `tacexpr3` + : `tacexpr2` tacexpr2 : `tacexpr1` || `tacexpr3` - : | `tacexpr1` + `tacexpr3` - : | tryif `tacexpr1` then `tacexpr1` else `tacexpr1` - : | `tacexpr1` + : `tacexpr1` + `tacexpr3` + : tryif `tacexpr1` then `tacexpr1` else `tacexpr1` + : `tacexpr1` tacexpr1 : fun `name` ... `name` => `atom` - : | let [rec] `let_clause` with ... with `let_clause` in `atom` - : | match goal with `context_rule` | ... | `context_rule` end - : | match reverse goal with `context_rule` | ... | `context_rule` end - : | match `expr` with `match_rule` | ... | `match_rule` end - : | lazymatch goal with `context_rule` | ... | `context_rule` end - : | lazymatch reverse goal with `context_rule` | ... | `context_rule` end - : | lazymatch `expr` with `match_rule` | ... | `match_rule` end - : | multimatch goal with `context_rule` | ... | `context_rule` end - : | multimatch reverse goal with `context_rule` | ... | `context_rule` end - : | multimatch `expr` with `match_rule` | ... | `match_rule` end - : | abstract `atom` - : | abstract `atom` using `ident` - : | first [ `expr` | ... | `expr` ] - : | solve [ `expr` | ... | `expr` ] - : | idtac [ `message_token` ... `message_token`] - : | fail [`natural`] [`message_token` ... `message_token`] - : | fresh [ `component` … `component` ] - : | context `ident` [`term`] - : | eval `redexpr` in `term` - : | type of `term` - : | constr : `term` - : | uconstr : `term` - : | type_term `term` - : | numgoals - : | guard `test` - : | assert_fails `tacexpr3` - : | assert_succeeds `tacexpr3` - : | `atomic_tactic` - : | `qualid` `tacarg` ... `tacarg` - : | `atom` + : let [rec] `let_clause` with ... with `let_clause` in `atom` + : match goal with `context_rule` | ... | `context_rule` end + : match reverse goal with `context_rule` | ... | `context_rule` end + : match `expr` with `match_rule` | ... | `match_rule` end + : lazymatch goal with `context_rule` | ... | `context_rule` end + : lazymatch reverse goal with `context_rule` | ... | `context_rule` end + : lazymatch `expr` with `match_rule` | ... | `match_rule` end + : multimatch goal with `context_rule` | ... | `context_rule` end + : multimatch reverse goal with `context_rule` | ... | `context_rule` end + : multimatch `expr` with `match_rule` | ... | `match_rule` end + : abstract `atom` + : abstract `atom` using `ident` + : first [ `expr` | ... | `expr` ] + : solve [ `expr` | ... | `expr` ] + : idtac [ `message_token` ... `message_token`] + : fail [`natural`] [`message_token` ... `message_token`] + : fresh [ `component` … `component` ] + : context `ident` [`term`] + : eval `redexpr` in `term` + : type of `term` + : constr : `term` + : uconstr : `term` + : type_term `term` + : numgoals + : guard `test` + : assert_fails `tacexpr3` + : assert_succeeds `tacexpr3` + : `atomic_tactic` + : `qualid` `tacarg` ... `tacarg` + : `atom` atom : `qualid` - : | () - : | `integer` - : | ( `expr` ) + : () + : `integer` + : ( `expr` ) component : `string` | `qualid` message_token : `string` | `ident` | `integer` tacarg : `qualid` - : | () - : | ltac : `atom` - : | `term` + : () + : ltac : `atom` + : `term` let_clause : `ident` [`name` ... `name`] := `expr` context_rule : `context_hyp`, ..., `context_hyp` |- `cpattern` => `expr` - : | `cpattern` => `expr` - : | |- `cpattern` => `expr` - : | _ => `expr` + : `cpattern` => `expr` + : |- `cpattern` => `expr` + : _ => `expr` context_hyp : `name` : `cpattern` - : | `name` := `cpattern` [: `cpattern`] + : `name` := `cpattern` [: `cpattern`] match_rule : `cpattern` => `expr` - : | context [ident] [ `cpattern` ] => `expr` - : | _ => `expr` + : context [`ident`] [ `cpattern` ] => `expr` + : _ => `expr` test : `integer` = `integer` - : | `integer` (< | <= | > | >=) `integer` + : `integer` (< | <= | > | >=) `integer` selector : [`ident`] - : | `integer` - : | (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) + : `integer` + : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) toplevel_selector : `selector` - : | all - : | par - : | ! + : all + : par + : ! .. productionlist:: coq top : [Local] Ltac `ltac_def` with ... with `ltac_def` ltac_def : `ident` [`ident` ... `ident`] := `expr` - : | `qualid` [`ident` ... `ident`] ::= `expr` + : `qualid` [`ident` ... `ident`] ::= `expr` .. _ltac-semantics: @@ -855,6 +859,10 @@ We can carry out pattern matching on terms with: Goal True. f (3+4). + .. coqtop:: none + + Abort. + .. _ltac-match-goal: Pattern matching on goals @@ -1022,6 +1030,10 @@ Counting the goals all:pr_numgoals. + .. coqtop:: none + + Abort. + Testing boolean expressions ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1150,6 +1162,15 @@ Printing |Ltac| tactics Debugging |Ltac| tactics ------------------------ +Backtraces +~~~~~~~~~~ + +.. flag:: Ltac Backtrace + + Setting this flag displays a backtrace on Ltac failures that can be useful + to find out what went wrong. It is disabled by default for performance + reasons. + Info trace ~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 590d71b5f3..24645a8cc3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -346,11 +346,46 @@ Navigation in the proof tree Goals are just existential variables and existential variables do not get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. + You may also wrap this in an Ltac-definition like: + + .. coqtop:: in + + Ltac name_goal name := refine ?[name]. .. seealso:: :ref:`existential-variables` .. example:: + This first example uses the Ltac definition above, and the named goals + only serve for documentation. + + .. coqtop:: all + + Goal forall n, n + 0 = n. + Proof. + induction n; [ name_goal base | name_goal step ]. + [base]: { + + .. coqtop:: all + + reflexivity. + + .. coqtop:: in + + } + + .. coqtop:: all + + [step]: { + + .. coqtop:: all + + simpl. + f_equal. + assumption. + } + Qed. + This can also be a way of focusing on a shelved goal, for instance: .. coqtop:: all diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 92bd4dbd1d..0bcca0fe56 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -233,7 +233,7 @@ construct differs from the latter in that .. coqtop:: reset all - Definition f u := let (m, n) := u in m + n. + Fail Definition f u := let (m, n) := u in m + n. The ``let:`` construct is just (more legible) notation for the primitive @@ -413,7 +413,7 @@ each point of use, e.g., the above definition can be written: Variable all : (T -> bool) -> list T -> bool. - .. coqtop:: all undo + .. coqtop:: all Prenex Implicits null. Definition all_null (s : list T) := all null s. @@ -436,7 +436,7 @@ The syntax of the new declaration is a ``Set Printing All`` command). All |SSR| library files thus start with the incantation - .. coqtop:: all undo + .. coqdoc:: Set Implicit Arguments. Unset Strict Implicit. @@ -505,7 +505,7 @@ Definitions |SSR| pose tactic supports *open syntax*: the body of the definition does not need surrounding parentheses. For instance: -.. coqtop:: in +.. coqdoc:: pose t := x + y. @@ -534,7 +534,7 @@ The |SSR| pose tactic also supports (co)fixpoints, by providing the local counterpart of the ``Fixpoint f := …`` and ``CoFixpoint f := …`` constructs. For instance, the following tactic: -.. coqtop:: in +.. coqdoc:: pose fix f (x y : nat) {struct x} : nat := if x is S p then S (f p y) else 0. @@ -544,7 +544,7 @@ on natural numbers. Similarly, local cofixpoints can be defined by a tactic of the form: -.. coqtop:: in +.. coqdoc:: pose cofix f (arg : T) := … . @@ -553,26 +553,26 @@ offers a smooth way of defining local abstractions. The type of “holes” is guessed by type inference, and the holes are abstracted. For instance the tactic: -.. coqtop:: in +.. coqdoc:: pose f := _ + 1. is shorthand for: -.. coqtop:: in +.. coqdoc:: pose f n := n + 1. When the local definition of a function involves both arguments and holes, hole abstractions appear first. For instance, the tactic: -.. coqtop:: in +.. coqdoc:: pose f x := x + _. is shorthand for: -.. coqtop:: in +.. coqdoc:: pose f n x := x + n. @@ -580,13 +580,13 @@ The interaction of the pose tactic with the interpretation of implicit arguments results in a powerful and concise syntax for local definitions involving dependent types. For instance, the tactic: -.. coqtop:: in +.. coqdoc:: pose f x y := (x, y). adds to the context the local definition: -.. coqtop:: in +.. coqdoc:: pose f (Tx Ty : Type) (x : Tx) (y : Ty) := (x, y). @@ -766,7 +766,7 @@ Moreover: .. coqtop:: all Lemma test : forall x : nat, x + 1 = 0. - set t := _ + 1. + Fail set t := _ + 1. + Typeclass inference should fill in any residual hole, but matching should never assign a value to a global existential variable. @@ -889,7 +889,7 @@ only one occurrence of the selected term. .. coqtop:: all Lemma test x y z : (x + y) + (z + z) = z + z. - set a := {2}(_ + _). + Fail set a := {2}(_ + _). .. _basic_localization_ssr: @@ -1079,7 +1079,7 @@ constants to the goal. Because they are tacticals, ``:`` and ``=>`` can be combined, as in -.. coqtop:: in +.. coqdoc:: move: m le_n_m => p le_n_p. @@ -1139,7 +1139,7 @@ Basic tactics like apply and elim can also be used without the ’:’ tactical: for example we can directly start a proof of ``subnK`` by induction on the top variable ``m`` with -.. coqtop:: in +.. coqdoc:: elim=> [|m IHm] n le_n. @@ -1150,7 +1150,7 @@ explained in terms of the goal stack:: is basically equivalent to -.. coqtop:: in +.. coqdoc:: move: a H1 H2; tactic => a H1 H2. @@ -1163,13 +1163,13 @@ temporary abbreviation to hide the statement of the goal from The general form of the in tactical can be used directly with the ``move``, ``case`` and ``elim`` tactics, so that one can write -.. coqtop:: in +.. coqdoc:: elim: n => [|n IHn] in m le_n_m *. instead of -.. coqtop:: in +.. coqdoc:: elim: n m le_n_m => [|n IHn] m le_n_m. @@ -1398,7 +1398,7 @@ Switches affect the discharging of a :token:`d_item` as follows: For example, the tactic: -.. coqtop:: in +.. coqdoc:: move: n {2}n (refl_equal n). @@ -1409,7 +1409,7 @@ For example, the tactic: Therefore this tactic changes any goal ``G`` into -.. coqtop:: +.. coqdoc:: forall n n0 : nat, n = n0 -> G. @@ -1445,6 +1445,16 @@ section constant. If tactic is ``move`` or ``case`` and an equation :token:`ident` is given, then clear (step 3) for :token:`d_item` is suppressed (see section :ref:`generation_of_equations_ssr`). +Intro patterns (see section :ref:`introduction_ssr`) +and the ``rewrite`` tactic (see section :ref:`rewriting_ssr`) +let one place a :token:`clear_switch` in the middle of other items +(namely identifiers, views and rewrite rules). This can trigger the +addition of proof context items to the ones being explicitly +cleared, and in turn this can result in clear errors (e.g. if the +context item automatically added occurs in the goal). The +relevant sections describe ways to avoid the unintended clear of +context items. + Matching for apply and exact ```````````````````````````` @@ -1572,6 +1582,9 @@ The :token:`i_pattern`\s can be seen as a variant of *intro patterns* (see :tacn:`intros`:) each performs an introduction operation, i.e., pops some variables or assumptions from the goal. +Simplification items +````````````````````` + An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: + ``//`` removes all the “trivial” subgoals that can be resolved by the @@ -1583,18 +1596,32 @@ An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: ``/= //``, i.e., ``simpl; try done``. -When an :token:`s_item` bears a :token:`clear_switch`, then the +When an :token:`s_item` immediately precedes a :token:`clear_switch`, then the :token:`clear_switch` is executed *after* the :token:`s_item`, e.g., ``{IHn}//`` will solve some subgoals, possibly using the fact ``IHn``, and will erase ``IHn`` from the context of the remaining subgoals. +Views +````` + The first entry in the :token:`i_view` grammar rule, :n:`/@term`, represents a view (see section :ref:`views_and_reflection_ssr`). It interprets the top of the stack with the view :token:`term`. -It is equivalent to ``move/term``. The optional flag ``{}`` can -be used to signal that the :token:`term`, when it is a context entry, -has to be cleared. +It is equivalent to :n:`move/@term`. + +A :token:`clear_switch` that immediately precedes an :token:`i_view` +is complemented with the name of the view if an only if the :token:`i_view` +is a simple proof context entry [#10]_. +E.g. ``{}/v`` is equivalent to ``/v{v}``. +This behavior can be avoided by separating the :token:`clear_switch` +from the :token:`i_view` with the ``-`` intro pattern or by putting +parentheses around the view. + +A :token:`clear_switch` that immediately precedes an :token:`i_view` +is executed after the view application. + + If the next :token:`i_item` is a view, then the view is applied to the assumption in top position once all the previous :token:`i_item` have been performed. @@ -1608,6 +1635,9 @@ Notations can be used to name tactics, for example:: lets one write just ``/myop`` in the intro pattern. Note the scope annotation: views are interpreted opening the ``ssripat`` scope. +Intro patterns +`````````````` + |SSR| supports the following :token:`i_pattern`\s: :token:`ident` @@ -1615,6 +1645,13 @@ annotation: views are interpreted opening the ``ssripat`` scope. a new constant, fact, or defined constant :token:`ident`, respectively. Note that defined constants cannot be introduced when δ-expansion is required to expose the top variable or assumption. + A :token:`clear_switch` (even an empty one) immediately preceding an + :token:`ident` is complemented with that :token:`ident` if and only if + the identifier is a simple proof context entry [#10]_. + As a consequence by prefixing the + :token:`ident` with ``{}`` one can *replace* a context entry. + This behavior can be avoided by separating the :token:`clear_switch` + from the :token:`ident` with the ``-`` intro pattern. ``>`` pops every variable occurring in the rest of the stack. Type class instances are popped even if they don't occur @@ -1708,6 +1745,9 @@ annotation: views are interpreted opening the ``ssripat`` scope. Note that |SSR| does not support the syntax ``(ipat, …, ipat)`` for destructing intro-patterns. +Clear switch +```````````` + Clears are deferred until the end of the intro pattern. .. example:: @@ -1730,6 +1770,9 @@ is performed behind the scenes. Facts mentioned in a clear switch must be valid names in the proof context (excluding the section context). +Branching and destructuring +``````````````````````````` + The rules for interpreting branching and destructing :token:`i_pattern` are motivated by the fact that it would be pointless to have a branching pattern if tactic is a ``move``, and in most of the remaining cases @@ -1754,6 +1797,9 @@ interpretation, e.g.: are all equivalent. +Block introduction +`````````````````` + |SSR| supports the following :token:`i_block`\s: :n:`[^ @ident ]` @@ -1797,7 +1843,7 @@ Generation of equations The generation of named equations option stores the definition of a new constant as an equation. The tactic: -.. coqtop:: in +.. coqdoc:: move En: (size l) => n. @@ -1805,7 +1851,7 @@ where ``l`` is a list, replaces ``size l`` by ``n`` in the goal and adds the fact ``En : size l = n`` to the context. This is quite different from: -.. coqtop:: in +.. coqdoc:: pose n := (size l). @@ -1890,7 +1936,7 @@ be substituted. inferred looking at the type of the top assumption. This allows for the compact syntax: - .. coqtop:: in + .. coqdoc:: case: {2}_ / eqP. @@ -2066,7 +2112,7 @@ In the script provided as example in section :ref:`indentation_ssr`, the paragraph corresponding to each sub-case ends with a tactic line prefixed with a ``by``, like in: -.. coqtop:: in +.. coqdoc:: by apply/eqP; rewrite -dvdn1. @@ -2101,13 +2147,13 @@ A natural and common way of closing a goal is to apply a lemma which is the exact one needed for the goal to be solved. The defective form of the tactic: -.. coqtop:: in +.. coqdoc:: exact. is equivalent to: -.. coqtop:: in +.. coqdoc:: do [done | by move=> top; apply top]. @@ -2115,13 +2161,13 @@ where ``top`` is a fresh name assigned to the top assumption of the goal. This applied form is supported by the ``:`` discharge tactical, and the tactic: -.. coqtop:: in +.. coqdoc:: exact: MyLemma. is equivalent to: -.. coqtop:: in +.. coqdoc:: by apply: MyLemma. @@ -2133,19 +2179,19 @@ is equivalent to: follows the ``by`` keyword is considered to be a parenthesized block applied to the current goal. Hence for example if the tactic: - .. coqtop:: in + .. coqdoc:: by rewrite my_lemma1. succeeds, then the tactic: - .. coqtop:: in + .. coqdoc:: by rewrite my_lemma1; apply my_lemma2. usually fails since it is equivalent to: - .. coqtop:: in + .. coqdoc:: by (rewrite my_lemma1; apply my_lemma2). @@ -2201,7 +2247,7 @@ Finally, the tactics ``last`` and ``first`` combine with the branching syntax of Ltac: if the tactic generates n subgoals on a given goal, then the tactic -.. coqtop:: in +.. coqdoc:: tactic ; last k [ tactic1 |…| tacticm ] || tacticn. @@ -2216,7 +2262,6 @@ to the others. .. coqtop:: reset - Abort. From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. @@ -2250,13 +2295,13 @@ Iteration A tactic of the form: -.. coqtop:: in +.. coqdoc:: do [ tactic 1 | … | tactic n ]. is equivalent to the standard Ltac expression: -.. coqtop:: in +.. coqdoc:: first [ tactic 1 | … | tactic n ]. @@ -2281,14 +2326,14 @@ Their meaning is: For instance, the tactic: -.. coqtop:: in +.. coqdoc:: tactic; do 1? rewrite mult_comm. rewrites at most one time the lemma ``mult_comm`` in all the subgoals generated by tactic , whereas the tactic: -.. coqtop:: in +.. coqdoc:: tactic; do 2! rewrite mult_comm. @@ -2472,7 +2517,7 @@ tactics of the form: which behave like: -.. coqtop:: in +.. coqdoc:: have: term ; first by tactic. move=> clear_switch i_item. @@ -2485,7 +2530,7 @@ to introduce the new assumption itself. The ``by`` feature is especially convenient when the proof script of the statement is very short, basically when it fits in one line like in: -.. coqtop:: in +.. coqdoc:: have H23 : 3 + 2 = 2 + 3 by rewrite addnC. @@ -2513,7 +2558,7 @@ the further use of the intermediate step. For instance, Thanks to the deferred execution of clears, the following idiom is also supported (assuming x occurs in the goal only): -.. coqtop:: in +.. coqdoc:: have {x} -> : x = y. @@ -2589,7 +2634,7 @@ Since the :token:`i_pattern` can be omitted, to avoid ambiguity, bound variables can be surrounded with parentheses even if no type is specified: -.. coqtop:: in +.. coqdoc:: have (x) : 2 * x = x + x by omega. @@ -2717,14 +2762,14 @@ typeclass inference. Goal True. -+ .. coqtop:: in undo + .. coqdoc:: have foo : ty. Full inference for ``ty``. The first subgoal demands a proof of such instantiated statement. -+ .. coqdoc:: + .. coqdoc:: have foo : ty := . @@ -2733,13 +2778,13 @@ typeclass inference. statement. Note that no proof term follows ``:=``, hence two subgoals are generated. -+ .. coqtop:: in undo + .. coqdoc:: have foo : ty := t. No inference for ``ty`` and ``t``. -+ .. coqtop:: in undo + .. coqdoc:: have foo := t. @@ -2770,7 +2815,7 @@ The + but the optional clear item is still performed in the *second* branch. This means that the tactic: - .. coqtop:: in + .. coqdoc:: suff {H} H : forall x : nat, x >= 0. @@ -2842,7 +2887,7 @@ name of the local definition with the ``@`` character. In the second subgoal, the tactic: -.. coqtop:: in +.. coqdoc:: move=> clear_switch i_item. @@ -2949,10 +2994,13 @@ illustrated in the following example. the pattern ``id (addx x)``, that would produce the following first subgoal - .. coqtop:: none + .. coqtop:: none reset + + From Coq Require Import ssreflect Omega. + Set Implicit Arguments. + Unset Strict Implicit. + Unset Printing Implicit Defensive. - Abort All. - From Coq Require Import Omega. Section Test. Variable x : nat. Definition addx z := z + x. @@ -3030,13 +3078,22 @@ operation should be performed: pattern. In its simplest form, it is a regular term. If no explicit redex switch is present the rewrite pattern to be matched is inferred from the :token:`r_item`. -+ This optional term, or the :token:`r_item`, may be preceded by an occurrence - switch (see section :ref:`selectors_ssr`) or a clear item - (see section :ref:`discharge_ssr`), - these two possibilities being exclusive. An occurrence switch selects ++ This optional term, or the :token:`r_item`, may be preceded by an + :token:`occ_switch` (see section :ref:`selectors_ssr`) or a + :token:`clear_switch` (see section :ref:`discharge_ssr`), + these two possibilities being exclusive. + + An occurrence switch selects the occurrences of the rewrite pattern which should be affected by the rewrite operation. + A clear switch, even an empty one, is performed *after* the + :token:`r_item` is actually processed and is complemented with the name of + the rewrite rule if an only if it is a simple proof context entry [#10]_. + As a consequence one can + write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately + afterwards. + This behavior can be avoided by putting parentheses around the rewrite rule. An :token:`r_item` can be: @@ -3098,7 +3155,7 @@ An :token:`r_item` can be: Definition f := fun x y => x + y. Lemma test x y : x + y = f y x. - rewrite -[f y]/(y + _). + Fail rewrite -[f y]/(y + _). but the following script succeeds @@ -3137,7 +3194,7 @@ tactics. In a rewrite tactic of the form: -.. coqtop:: in +.. coqdoc:: rewrite occ_switch [term1]term2. @@ -3180,7 +3237,7 @@ Performing rewrite and simplification operations in a single tactic enhances significantly the concision of scripts. For instance the tactic: -.. coqtop:: in +.. coqdoc:: rewrite /my_def {2}[f _]/= my_eq //=. @@ -3261,7 +3318,7 @@ the equality. .. coqtop:: all Lemma test (H : forall t u, t + u * 0 = t) x y : x + y * 4 + 2 * 0 = x + 2 * 0. - rewrite [x + _]H. + Fail rewrite [x + _]H. Indeed the left hand side of ``H`` does not match the redex identified by the pattern ``x + y * 4``. @@ -3291,10 +3348,6 @@ the rewrite tactic. The effect of the tactic on the initial goal is to rewrite this lemma at the second occurrence of the first matching ``x + y + 0`` of the explicit rewrite redex ``_ + y + 0``. -An empty occurrence switch ``{}`` is not interpreted as a valid occurrence -switch. It has the effect of clearing the :token:`r_item` (when it is the name -of a context entry). - Occurrence selection and repetition ``````````````````````````````````` @@ -3447,7 +3500,7 @@ reasoning purposes. The library also provides one lemma per such operation, stating that both versions return the same values when applied to the same arguments: -.. coqtop:: in +.. coqdoc:: Lemma addE : add =2 addn. Lemma doubleE : double =1 doublen. @@ -3463,7 +3516,7 @@ hand side. In order to reason conveniently on expressions involving the efficient operations, we gather all these rules in the definition ``trecE``: -.. coqtop:: in +.. coqdoc:: Definition trecE := (addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))). @@ -3521,14 +3574,14 @@ cases: + |SSR| never accepts to rewrite indeterminate patterns like: - .. coqtop:: in + .. coqdoc:: Lemma foo (x : unit) : x = tt. |SSR| will however accept the ηζ expansion of this rule: - .. coqtop:: in + .. coqdoc:: Lemma fubar (x : unit) : (let u := x in u) = tt. @@ -3566,7 +3619,7 @@ cases: .. coqtop:: all - rewrite H. + Fail rewrite H. Rewriting with ``H`` first requires unfolding the occurrences of ``f`` @@ -3678,7 +3731,7 @@ copy of any term t. However this copy is (on purpose) *not convertible* to t in the |Coq| system [#8]_. The job is done by the following construction: -.. coqtop:: in +.. coqdoc:: Lemma master_key : unit. Proof. exact tt. Qed. Definition locked A := let: tt := master_key in fun x : A => x. @@ -3742,14 +3795,14 @@ some functions by the partial evaluation switch ``/=``, unless this allowed the evaluation of a condition. This is possible thanks to another mechanism of term tagging, resting on the following *Notation*: -.. coqtop:: in +.. coqdoc:: Notation "'nosimpl' t" := (let: tt := tt in t). The term ``(nosimpl t)`` simplifies to ``t`` *except* in a definition. More precisely, given: -.. coqtop:: in +.. coqdoc:: Definition foo := (nosimpl bar). @@ -3765,7 +3818,7 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to The ``nosimpl`` trick only works if no reduction is apparent in ``t``; in particular, the declaration: - .. coqtop:: in + .. coqdoc:: Definition foo x := nosimpl (bar x). @@ -3773,14 +3826,14 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to function, and to use the following definition, which blocks the reduction as expected: - .. coqtop:: in + .. coqdoc:: Definition foo x := nosimpl bar x. A standard example making this technique shine is the case of arithmetic operations. We define for instance: -.. coqtop:: in +.. coqdoc:: Definition addn := nosimpl plus. @@ -3800,7 +3853,7 @@ Congruence Because of the way matching interferes with parameters of type families, the tactic: -.. coqtop:: in +.. coqdoc:: apply: my_congr_property. @@ -3996,7 +4049,7 @@ For a quick glance at what can be expressed with the last :token:`r_pattern` consider the goal ``a = b`` and the tactic -.. coqtop:: in +.. coqdoc:: rewrite [in X in _ = X]rule. @@ -4097,14 +4150,14 @@ patterns over simple terms, but to interpret a pattern with double parentheses as a simple term. For example, the following tactic would capture any occurrence of the term ``a in A``. -.. coqtop:: in +.. coqdoc:: set t := ((a in A)). Contextual patterns can also be used as arguments of the ``:`` tactical. For example: -.. coqtop:: in +.. coqdoc:: elim: n (n in _ = n) (refl_equal n). @@ -4195,7 +4248,7 @@ context shortcuts. The following example is taken from ``ssreflect.v`` where the ``LHS`` and ``RHS`` shortcuts are defined. -.. coqtop:: in +.. coqdoc:: Notation RHS := (X in _ = X)%pattern. Notation LHS := (X in X = _)%pattern. @@ -4203,7 +4256,7 @@ The following example is taken from ``ssreflect.v`` where the Shortcuts defined this way can be freely used in place of the trailing ``ident in term`` part of any contextual pattern. Some examples follow: -.. coqtop:: in +.. coqdoc:: set rhs := RHS. rewrite [in RHS]rule. @@ -4236,13 +4289,13 @@ The view syntax combined with the ``elim`` tactic specifies an elimination scheme to be used instead of the default, generated, one. Hence the |SSR| tactic: -.. coqtop:: in +.. coqdoc:: elim/V. is a synonym for: -.. coqtop:: in +.. coqdoc:: intro top; elim top using V; clear top. @@ -4252,13 +4305,13 @@ Since an elimination view supports the two bookkeeping tacticals of discharge and introduction (see section :ref:`basic_tactics_ssr`), the |SSR| tactic: -.. coqtop:: in +.. coqdoc:: elim/V: x => y. is a synonym for: -.. coqtop:: in +.. coqdoc:: elim x using V; clear x; intro y. @@ -4316,13 +4369,13 @@ command) can be combined with the type family switches described in section :ref:`type_families_ssr`. Consider an eliminator ``foo_ind`` of type: -.. coqtop:: in +.. coqdoc:: foo_ind : forall …, forall x : T, P p1 … pm. and consider the tactic: -.. coqtop:: in +.. coqdoc:: elim/foo_ind: e1 … / en. @@ -4373,7 +4426,7 @@ Here is an example of a regular, but nontrivial, eliminator. The following tactics are all valid and perform the same elimination on this goal. - .. coqtop:: in + .. coqdoc:: elim/plus_ind: z / (plus _ z). elim/plus_ind: {z}(plus _ z). @@ -4422,7 +4475,7 @@ Here is an example of a regular, but nontrivial, eliminator. .. coqtop:: all - elim/plus_ind: y / _. + Fail elim/plus_ind: y / _. triggers an error: in the conclusion of the ``plus_ind`` eliminator, the first argument of the predicate @@ -4443,7 +4496,7 @@ Here is an example of a truncated eliminator: Unset Printing Implicit Defensive. Section Test. - .. coqtop:: in + .. coqdoc:: Lemma test p n (n_gt0 : 0 < n) (pr_p : prime p) : p %| \prod_(i <- prime_decomp n | i \in prime_decomp n) i.1 ^ i.2 -> @@ -4454,7 +4507,7 @@ Here is an example of a truncated eliminator: where the type of the ``big_prop`` eliminator is - .. coqtop:: in + .. coqdoc:: big_prop: forall (R : Type) (Pb : R -> Type) (idx : R) (op1 : R -> R -> R), Pb idx -> @@ -4467,7 +4520,7 @@ Here is an example of a truncated eliminator: inferred one is used instead: ``big[_/_]_(i <- _ | _ i) _ i``, and after the introductions, the following goals are generated: - .. coqtop:: in + .. coqdoc:: subgoal 1 is: p %| 1 -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1 @@ -4533,13 +4586,18 @@ disjunction. Lemma test a : P (a || a) -> True. - .. coqtop:: all undo + .. coqtop:: all move=> HPa; move/P2Q: HPa => HQa. or more directly: - .. coqtop:: all undo + .. coqtop:: none + + Abort. + Lemma test a : P (a || a) -> True. + + .. coqtop:: all move/P2Q=> HQa. @@ -4573,7 +4631,7 @@ equation name generation mechanism (see section :ref:`generation_of_equations_ss This view tactic performs: - .. coqtop:: in + .. coqdoc:: move=> HQ; case: {HQ}(Q2P HQ) => [HPa | HPb]. @@ -4610,14 +4668,14 @@ relevant for the current goal. the double implication into the expected simple implication. The last script is in fact equivalent to: - .. coqtop:: in + .. coqdoc:: Lemma test a b : P (a || b) -> True. move/(iffLR (PQequiv _ _)). where: - .. coqtop:: in + .. coqdoc:: Lemma iffLR P Q : (P <-> Q) -> P -> Q. @@ -4759,7 +4817,7 @@ decidable predicate to its boolean version. First, booleans are injected into propositions using the coercion mechanism: -.. coqtop:: in +.. coqdoc:: Coercion is_true (b : bool) := b = true. @@ -4776,7 +4834,7 @@ To get all the benefits of the boolean reflection, it is in fact convenient to introduce the following inductive predicate ``reflect`` to relate propositions and booleans: -.. coqtop:: in +.. coqdoc:: Inductive reflect (P: Prop): bool -> Type := | Reflect_true : P -> reflect P true @@ -4787,7 +4845,7 @@ logically equivalent propositions. For instance, the following lemma: -.. coqtop:: in +.. coqdoc:: Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). @@ -4802,20 +4860,20 @@ to the case analysis of |Coq|’s inductive types. Since the equivalence predicate is defined in |Coq| as: -.. coqtop:: in +.. coqdoc:: Definition iff (A B:Prop) := (A -> B) /\ (B -> A). where ``/\`` is a notation for ``and``: -.. coqtop:: in +.. coqdoc:: Inductive and (A B:Prop) : Prop := conj : A -> B -> and A B. This make case analysis very different according to the way an equivalence property has been defined. -.. coqtop:: in +.. coqdoc:: Lemma andE (b1 b2 : bool) : (b1 /\ b2) <-> (b1 && b2). @@ -4837,11 +4895,15 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2). - .. coqtop:: all undo + .. coqtop:: all case: (@andE b1 b2). - .. coqtop:: all undo + .. coqtop:: none + + Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2). + + .. coqtop:: all case: (@andP b1 b2). @@ -4899,13 +4961,13 @@ Specializing assumptions The |SSR| tactic: -.. coqtop:: in +.. coqdoc:: move/(_ term1 … termn). is equivalent to the tactic: -.. coqtop:: in +.. coqdoc:: intro top; generalize (top term1 … termn); clear top. @@ -4962,13 +5024,13 @@ If ``term`` is a double implication, then the view hint will be one of the defined view hints for implication. These hints are by default the ones present in the file ``ssreflect.v``: -.. coqtop:: in +.. coqdoc:: Lemma iffLR : forall P Q, (P <-> Q) -> P -> Q. which transforms a double implication into the left-to-right one, or: -.. coqtop:: in +.. coqdoc:: Lemma iffRL : forall P Q, (P <-> Q) -> Q -> P. @@ -5072,7 +5134,7 @@ equality, while the second term is the one applied to the right hand side. In this context, the identity view can be used when no view has to be applied: -.. coqtop:: in +.. coqdoc:: Lemma idP : reflect b1 b1. @@ -5147,7 +5209,7 @@ in sequence. Both move and apply can be followed by an arbitrary number of ``/term``. The main difference between the following two tactics -.. coqtop:: in +.. coqdoc:: apply/v1/v2/v3. apply/v1; apply/v2; apply/v3. @@ -5159,7 +5221,7 @@ line would apply the view ``v2`` to all the goals generated by ``apply/v1``. Note that the NO-OP intro pattern ``-`` can be used to separate two views, making the two following examples equivalent: -.. coqtop:: in +.. coqdoc:: move=> /v1; move=> /v2. move=> /v1 - /v2. @@ -5520,3 +5582,5 @@ Settings in the metatheory .. [#9] The current state of the proof shall be displayed by the Show Proof command of |Coq| proof mode. +.. [#10] A simple proof context entry is a naked identifier (i.e. not between + parentheses) designating a context entry that is not a section variable. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 59602581c7..6f57cc53a9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -33,10 +33,13 @@ 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 @@ -44,9 +47,9 @@ specified, the default selector is used. .. _tactic_invocation_grammar: - .. productionlist:: `sentence` - tactic_invocation : toplevel_selector : tactic. - : |tactic . + .. productionlist:: sentence + tactic_invocation : `toplevel_selector` : `tactic`. + : `tactic`. .. opt:: Default Goal Selector "@toplevel_selector" :name: Default Goal Selector @@ -71,29 +74,31 @@ specified, the default selector is used. Bindings list ~~~~~~~~~~~~~~~~~~~ -Tactics that take a term as argument may also support a bindings list, -so as to instantiate some parameters of the term by name or position. -The general form of a term equipped with a bindings list is ``term with -bindings_list`` where ``bindings_list`` may be of two different forms: +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` - bindings_list : (ref := `term`) ... (ref := `term`) + .. 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 ++ 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 - ``term``. If :n:`ref` is an identifier, this identifier has to be bound in the - type of ``term`` and the binding provides the tactic with an instance for the - parameter of this name. If :n:`ref` is some number ``n``, this number denotes - the ``n``-th non dependent premise of the ``term``, as determined by the type - of ``term``. + :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}`. ++ 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 @@ -105,6 +110,350 @@ bindings_list`` where ``bindings_list`` may be of two different forms: .. 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 number of + 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 there are + 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 more + 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 + + Variables (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 ys = 0` + * `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/blob/8e6efe4971ed828ac8bdb5512c1f615d7d62691e/src/IntroPatterns.v>`_ + .. _occurrencessets: Occurrence sets and occurrence clauses @@ -113,11 +462,11 @@ Occurrence sets and occurrence clauses An occurrence clause is a modifier to some tactics that obeys the following syntax: - .. productionlist:: `sentence` + .. productionlist:: sentence occurrence_clause : in `goal_occurrences` - goal_occurrences : [`ident` [`at_occurrences`], ... , ident [`at_occurrences`] [|- [* [`at_occurrences`]]]] - :| * |- [* [`at_occurrences`]] - :| * + goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [`at_occurrences`]]]] + : * |- [* [`at_occurrences`]] + : * at_occurrences : at `occurrences` occurrences : [-] `num` ... `num` @@ -406,33 +755,49 @@ Applying theorems A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``. - .. coqtop:: all undo + .. coqtop:: all apply (Rtrans n m p). Note that ``n`` can be inferred from the goal, so the following would work too. - .. coqtop:: in undo + .. coqtop:: none + + Abort. Goal R n p. + + .. coqtop:: in apply (Rtrans _ m). More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the unknown m: - .. coqtop:: in undo + .. coqtop:: none + + Abort. Goal R n p. + + .. coqtop:: in apply Rtrans with (y := m). Another solution is to mention the proof of ``(R x y)`` in ``Rtrans`` - .. coqtop:: all undo + .. coqtop:: none + + Abort. Goal R n p. + + .. coqtop:: all apply Rtrans with (1 := Rnm). ... or the proof of ``(R y z)``. - .. coqtop:: all undo + .. coqtop:: none + + Abort. Goal R n p. + + .. coqtop:: all apply Rtrans with (2 := Rmp). @@ -440,6 +805,10 @@ Applying theorems finding ``m``. Then one can apply the hypotheses ``Rnm`` and ``Rmp``. This instantiates the existential variable and completes the proof. + .. coqtop:: none + + Abort. Goal R n p. + .. coqtop:: all eapply Rtrans. @@ -508,10 +877,10 @@ Applying theorems 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 @intro_pattern + .. 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:`intro_pattern` + This works as :tacn:`apply ... in` then applies the :token:`simple_intropattern` to the hypothesis :token:`ident`. .. tacv:: simple apply @term in @ident @@ -525,8 +894,8 @@ Applying theorems 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 @intro_pattern} - {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} + .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @simple_intropattern} + {? 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`. @@ -726,149 +1095,17 @@ Managing the local context .. exn:: No such hypothesis: @ident. :undocumented: -.. tacn:: intros @intro_pattern_list +.. tacn:: intros @intropattern_list :name: intros ... - This extension of the tactic :n:`intros` allows to apply tactics on the fly - on the variables or hypotheses which have been introduced. An - *introduction pattern list* :n:`@intro_pattern_list` is a list of - introduction patterns possibly containing the filling introduction - patterns `*` and `**`. An *introduction pattern* is either: - - + a *naming introduction pattern*, i.e. either one of: - - + the pattern :n:`?` - - + the pattern :n:`?ident` - - + an identifier - - + an *action introduction pattern* which itself classifies into: - - + a *disjunctive/conjunctive introduction pattern*, i.e. either one of - - + a disjunction of lists of patterns - :n:`[@intro_pattern_list | ... | @intro_pattern_list]` - - + a conjunction of patterns: :n:`({+, p})` - - + a list of patterns - :n:`({+& p})` - for sequence of right-associative binary constructs - - + an *equality introduction pattern*, i.e. either one of: - - + a pattern for decomposing an equality: :n:`[= {+ p}]` - + the rewriting orientations: :n:`->` or :n:`<-` - - + the on-the-fly application of lemmas: :n:`p{+ %term}` where :n:`p` - itself is not a pattern for on-the-fly application of lemmas (note: - syntax is in experimental stage) - - + the wildcard: :n:`_` - - - Assuming a goal of type :g:`Q → P` (non-dependent product), or of type - :g:`forall x:T, P` (dependent product), the behavior of - :n:`intros p` is defined inductively over the structure of the introduction - pattern :n:`p`: - - Introduction on :n:`?` performs the introduction, and lets Coq choose a fresh - name for the variable; + Introduces one or more variables or hypotheses from the goal by matching the + intro patterns. See the description in :ref:`intropatterns`. - Introduction on :n:`?@ident` performs the introduction, and lets Coq choose a - fresh name for the variable based on :n:`@ident`; +.. tacn:: eintros @intropattern_list + :name: eintros - Introduction on :n:`@ident` behaves as described in :tacn:`intro` - - Introduction over a disjunction of list of patterns - :n:`[@intro_pattern_list | ... | @intro_pattern_list ]` expects the product - to be over an inductive type whose number of constructors is `n` (or more - generally over a type of conclusion an inductive type built from `n` - constructors, e.g. :g:`C -> A\/B` with `n=2` since :g:`A\/B` has `2` - constructors): it destructs the introduced hypothesis as :n:`destruct` (see - :tacn:`destruct`) would and applies on each generated subgoal the - corresponding tactic; - - The introduction patterns in :n:`@intro_pattern_list` are expected to consume - no more than the number of arguments of the `i`-th constructor. If it - consumes less, then Coq completes the pattern so that all the arguments of - the constructors of the inductive type are introduced (for instance, the - list of patterns :n:`[ | ] H` applied on goal :g:`forall x:nat, x=0 -> 0=x` - behaves the same as the list of patterns :n:`[ | ? ] H`); - - Introduction over a conjunction of patterns :n:`({+, p})` expects - the goal to be a product over an inductive type :g:`I` with a single - constructor that itself has at least `n` arguments: It performs a case - analysis over the hypothesis, as :n:`destruct` would, and applies the - patterns :n:`{+ p}` to the arguments of the constructor of :g:`I` (observe - that :n:`({+ p})` is an alternative notation for :n:`[{+ p}]`); - - Introduction via :n:`({+& p})` is a shortcut for introduction via - :n:`(p,( ... ,( ..., p ) ... ))`; it expects the hypothesis to be a sequence of - right-associative binary inductive constructors such as :g:`conj` or - :g:`ex_intro`; for instance, a hypothesis with type - :g:`A /\(exists x, B /\ C /\ D)` can be introduced via pattern - :n:`(a & x & b & c & d)`; - - If the product is over an equality type, then a pattern of the form - :n:`[= {+ p}]` applies either :tacn:`injection` or :tacn:`discriminate` - instead of :tacn:`destruct`; if :tacn:`injection` is applicable, the patterns - :n:`{+, p}` are 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. - - Introduction over ``->`` (respectively over ``<-``) - expects the hypothesis to be an equality and the right-hand-side - (respectively the left-hand-side) is replaced by the left-hand-side - (respectively the right-hand-side) in the conclusion of the goal; - the hypothesis itself is erased; if the term to substitute is a variable, it - is substituted also in the context of goal and the variable is removed too. - - Introduction over a pattern :n:`p{+ %term}` first applies :n:`{+ term}` - on the hypothesis to be introduced (as in :n:`apply {+, term}`) prior to the - application of the introduction pattern :n:`p`; - - Introduction on the wildcard depends on whether the product is dependent or not: - in the non-dependent case, it erases the corresponding hypothesis (i.e. it - behaves as an :tacn:`intro` followed by a :tacn:`clear`) while in the - dependent case, it succeeds and erases the variable only if the wildcard is part - of a more complex list of introduction patterns that also erases the hypotheses - depending on this variable; - - Introduction over :n:`*` introduces all forthcoming quantified variables - appearing in a row; introduction over :n:`**` introduces all forthcoming - quantified variables or hypotheses until the goal is not any more a - quantification or an implication. - - .. example:: - - .. coqtop:: reset all - - Goal forall A B C:Prop, A \/ B /\ C -> (A -> C) -> C. - intros * [a | (_,c)] f. - -.. note:: - - :n:`intros {+ p}` is not equivalent to :n:`intros p; ... ; intros p` - for the following reason: If one of the :n:`p` is a wildcard pattern, it - might succeed in the first case because the further hypotheses it - depends on are eventually erased too while it might fail in the second - case because of dependencies in hypotheses which are not yet - introduced (and a fortiori not yet erased). - -.. note:: - - In :n:`intros @intro_pattern_list`, if the last introduction pattern - is a disjunctive or conjunctive pattern - :n:`[{+| @intro_pattern_list}]`, the completion of :n:`@intro_pattern_list` - so that all the arguments of the i-th constructors of the corresponding - inductive type are introduced can be controlled with the following option: - - .. flag:: Bracketing Last Introduction Pattern - - Force completion, if needed, when the last introduction pattern is a - disjunctive or conjunctive pattern (on by default). + Works just like :tacn:`intros ...` except that it creates existential variables + for any unresolved variables rather than failing. .. tacn:: clear @ident :name: clear @@ -1057,19 +1294,19 @@ Managing the local context 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:@ident__2 } +.. tacn:: remember @term as @ident__1 {? eqn:@naming_intropattern } :name: remember - This behaves as :n:`set (@ident__1 := @term) in *`, using a logical + This behaves as :n:`set (@ident := @term) in *`, using a logical (Leibniz’s) equality instead of a local definition. - If :n:`@ident__2` is provided, it will be the name of the new equation. + Use :n:`@naming_intropattern` to name or split up the new equation. - .. tacv:: remember @term as @ident__1 {? eqn:@ident__2 } in @goal_occurrences + .. 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:@ident__2 } {? in @goal_occurrences } + .. tacv:: eremember @term as @ident__1 {? eqn:@naming_intropattern } {? in @goal_occurrences } :name: eremember While the different variants of :tacn:`remember` expect that no @@ -1163,16 +1400,16 @@ Controlling the proof flow :name: Proof is not complete. (assert) :undocumented: - .. tacv:: assert @type as @intro_pattern + .. tacv:: assert @type as @simple_intropattern - If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`), + If :n:`simple_intropattern` is an intro pattern (see :ref:`intropatterns`), the hypothesis is named after this introduction pattern (in particular, if - :n:`intro_pattern` is :n:`@ident`, the tactic behaves like - :n:`assert (@ident : @type)`). If :n:`intro_pattern` is an action + :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 @intro_pattern by @tactic + .. tacv:: assert @type as @simple_intropattern by @tactic This combines the two previous variants of :tacn:`assert`. @@ -1186,7 +1423,7 @@ Controlling the proof flow .. exn:: Variable @ident is already declared. :undocumented: -.. tacv:: eassert @type as @intro_pattern by @tactic +.. tacv:: eassert @type as @simple_intropattern by @tactic :name: eassert While the different variants of :tacn:`assert` expect that no existential @@ -1194,16 +1431,16 @@ Controlling the proof flow This allows not to specify the asserted statement completeley before starting to prove it. -.. tacv:: pose proof @term {? as @intro_pattern} +.. tacv:: pose proof @term {? as @simple_intropattern} :name: pose proof - This tactic behaves like :n:`assert @type {? as @intro_pattern} by exact @term` + 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 @intro_pattern` is the same as applying the - :token:`intro_pattern` to :token:`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 @intro_pattern} +.. tacv:: epose proof @term {? as @simple_intropattern} :name: epose proof While :tacn:`pose proof` expects that no existential variables are generated by @@ -1221,20 +1458,20 @@ Controlling the proof flow This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of the hypothesis generated by Coq. -.. tacv:: enough @type as @intro_pattern +.. tacv:: enough @type as @simple_intropattern - This behaves like :n:`enough @type` using :token:`intro_pattern` to name or + 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 @intro_pattern } 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 @intro_pattern` clause generates more than one subgoal, :token:`tactic` is + :n:`as @simple_intropattern` clause generates more than one subgoal, :token:`tactic` is applied to all of them. -.. tacv:: eenough @type {? as @intro_pattern } {? by @tactic } +.. tacv:: eenough @type {? as @simple_intropattern } {? by @tactic } eenough (@ident : @type) {? by @tactic } :name: eenough; _ @@ -1250,8 +1487,8 @@ Controlling the proof flow 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 @intro_pattern} - specialize @ident with @bindings_list {? as @intro_pattern} +.. 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 @@ -1264,7 +1501,7 @@ Controlling the proof flow 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:`intro_pattern`. The name :n:`@ident` + 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 @@ -1477,11 +1714,11 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This is a shortcut for :n:`destruct @term; ...; destruct @term`. - .. tacv:: destruct @term as @disj_conj_intro_pattern + .. tacv:: destruct @term as @or_and_intropattern_loc This behaves as :n:`destruct @term` but uses the names - in :token:`disj_conj_intro_pattern` to name the variables introduced in the - context. The :token:`disj_conj_intro_pattern` must have the + 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 @@ -1491,13 +1728,13 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) pattern (see :tacn:`intros`). This provides a concise notation for chaining destruction of a hypothesis. - .. tacv:: destruct @term eqn:@naming_intro_pattern + .. 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_intro_pattern` (see :tacn:`intros`), + 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 @@ -1525,8 +1762,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) clause is an occurrence clause whose syntax and behavior is described in :ref:`occurrences sets <occurrencessets>`. - .. tacv:: destruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } - edestruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } + .. tacv:: destruct @term {? with @bindings_list } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } + edestruct @term {? with @bindings_list } {? as @or_and_intropattern_loc } {? eqn:@naming_intropattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences } These are the general forms of :tacn:`destruct` and :tacn:`edestruct`. They combine the effects of the ``with``, ``as``, ``eqn:``, ``using``, @@ -1622,11 +1859,11 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) Use in this case the variant :tacn:`elim ... with` below. -.. tacv:: induction @term as @disj_conj_intro_pattern +.. tacv:: induction @term as @or_and_intropattern_loc This behaves as :tacn:`induction` but uses the names in - :n:`@disj_conj_intro_pattern` to name the variables introduced in the - context. The :n:`@disj_conj_intro_pattern` must typically be of the form + :n:`@or_and_intropattern_loc` to name the variables introduced in the + context. The :n:`@or_and_intropattern_loc` must typically be of the form :n:`[ p` :sub:`11` :n:`... p` :sub:`1n` :n:`| ... | p`:sub:`m1` :n:`... p`:sub:`mn` :n:`]` with :n:`m` being the number of constructors of the type of :n:`@term`. Each variable introduced by induction in the context of the i-th goal gets its @@ -1686,8 +1923,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) induction y in x |- *. Show 2. -.. tacv:: induction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences - einduction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences +.. tacv:: induction @term with @bindings_list as @or_and_intropattern_loc using @term with @bindings_list in @goal_occurrences + einduction @term with @bindings_list as @or_and_intropattern_loc using @term with @bindings_list in @goal_occurrences These are the most general forms of :tacn:`induction` and :tacn:`einduction`. It combines the effects of the with, as, using, and in clauses. @@ -1898,7 +2135,7 @@ and an explanation of the underlying technique. .. exn:: Not the right number of induction arguments. :undocumented: -.. tacv:: functional induction (@qualid {+ @term}) as @disj_conj_intro_pattern using @term with @bindings_list +.. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving explicitly the name of the introduced variables, the induction principle, and @@ -2053,18 +2290,18 @@ and an explanation of the underlying technique. .. exn:: goal does not satisfy the expected preconditions. :undocumented: - .. tacv:: injection @term {? with @bindings_list} as {+ @intro_pattern} - injection @num as {+ intro_pattern} - injection as {+ intro_pattern} - einjection @term {? with @bindings_list} as {+ intro_pattern} - einjection @num as {+ intro_pattern} - einjection as {+ intro_pattern} + .. tacv:: injection @term {? with @bindings_list} as {+ @simple_intropattern} + injection @num as {+ simple_intropattern} + injection as {+ simple_intropattern} + einjection @term {? with @bindings_list} as {+ simple_intropattern} + einjection @num as {+ simple_intropattern} + einjection as {+ simple_intropattern} - These variants apply :n:`intros {+ @intro_pattern}` after the call to + These variants apply :n:`intros {+ @simple_intropattern}` after the call to :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in - the context of hypotheses. The number of :n:`@intro_pattern` must not exceed + the context of hypotheses. The number of :n:`@simple_intropattern` must not exceed the number of equalities newly generated. If it is smaller, fresh - names are automatically generated to adjust the list of :n:`@intro_pattern` + names are automatically generated to adjust the list of :n:`@simple_intropattern` to the number of new equalities. The original equality is erased if it corresponds to a hypothesis. @@ -2115,13 +2352,14 @@ and an explanation of the underlying technique. where :n:`@ident` is the identifier for the last introduced hypothesis. .. tacv:: inversion_clear @ident + :name: inversion_clear This behaves as :n:`inversion` and then erases :n:`@ident` from the context. -.. tacv:: inversion @ident as @intro_pattern +.. tacv:: inversion @ident as @or_and_intropattern_loc - This generally behaves as inversion but using names in :n:`@intro_pattern` - for naming hypotheses. The :n:`@intro_pattern` must have the form + This generally behaves as inversion but using names in :n:`@or_and_intropattern_loc` + for naming hypotheses. The :n:`@or_and_intropattern_loc` must have the form :n:`[p`:sub:`11` :n:`... p`:sub:`1n` :n:`| ... | p`:sub:`m1` :n:`... p`:sub:`mn` :n:`]` with `m` being the number of constructors of the type of :n:`@ident`. Be careful that the list must be of length `m` even if ``inversion`` discards @@ -2153,12 +2391,12 @@ and an explanation of the underlying technique. Goal forall l:list nat, contains0 (1 :: l) -> contains0 l. intros l H; inversion H as [ | l' p Hl' [Heqp Heql'] ]. -.. tacv:: inversion @num as @intro_pattern +.. tacv:: inversion @num as @or_and_intropattern_loc This allows naming the hypotheses introduced by :n:`inversion @num` in the context. -.. tacv:: inversion_clear @ident as @intro_pattern +.. tacv:: inversion_clear @ident as @or_and_intropattern_loc This allows naming the hypotheses introduced by ``inversion_clear`` in the context. Notice that hypothesis names can be provided as if ``inversion`` @@ -2170,7 +2408,7 @@ and an explanation of the underlying technique. Let :n:`{+ @ident}` be identifiers in the local context. This tactic behaves as generalizing :n:`{+ @ident}`, and then performing ``inversion``. -.. tacv:: inversion @ident as @intro_pattern in {+ @ident} +.. tacv:: inversion @ident as @or_and_intropattern_loc in {+ @ident} This allows naming the hypotheses introduced in the context by :n:`inversion @ident in {+ @ident}`. @@ -2180,7 +2418,7 @@ and an explanation of the underlying technique. Let :n:`{+ @ident}` be identifiers in the local context. This tactic behaves as generalizing :n:`{+ @ident}`, and then performing ``inversion_clear``. -.. tacv:: inversion_clear @ident as @intro_pattern in {+ @ident} +.. tacv:: inversion_clear @ident as @or_and_intropattern_loc in {+ @ident} This allows naming the hypotheses introduced in the context by :n:`inversion_clear @ident in {+ @ident}`. @@ -2192,7 +2430,7 @@ and an explanation of the underlying technique. ``inversion`` and then substitutes :n:`@ident` for the corresponding :n:`@@term` in the goal. -.. tacv:: dependent inversion @ident as @intro_pattern +.. tacv:: dependent inversion @ident as @or_and_intropattern_loc This allows naming the hypotheses introduced in the context by :n:`dependent inversion @ident`. @@ -2202,7 +2440,7 @@ and an explanation of the underlying technique. Like ``dependent inversion``, except that :n:`@ident` is cleared from the local context. -.. tacv:: dependent inversion_clear @ident as @intro_pattern +.. tacv:: dependent inversion_clear @ident as @or_and_intropattern_loc This allows naming the hypotheses introduced in the context by :n:`dependent inversion_clear @ident`. @@ -2216,7 +2454,7 @@ and an explanation of the underlying technique. then :n:`@term` must be of type :g:`I:forall (x:T), I x -> s'` where :g:`s'` is the type of the goal. -.. tacv:: dependent inversion @ident as @intro_pattern with @term +.. tacv:: dependent inversion @ident as @or_and_intropattern_loc with @term This allows naming the hypotheses introduced in the context by :n:`dependent inversion @ident with @term`. @@ -2226,7 +2464,7 @@ and an explanation of the underlying technique. Like :tacn:`dependent inversion ... with ...` with but clears :n:`@ident` from the local context. -.. tacv:: dependent inversion_clear @ident as @intro_pattern with @term +.. tacv:: dependent inversion_clear @ident as @or_and_intropattern_loc with @term This allows naming the hypotheses introduced in the context by :n:`dependent inversion_clear @ident with @term`. @@ -2237,7 +2475,7 @@ and an explanation of the underlying technique. It is a very primitive inversion tactic that derives all the necessary equalities but it does not simplify the constraints as ``inversion`` does. -.. tacv:: simple inversion @ident as @intro_pattern +.. tacv:: simple inversion @ident as @or_and_intropattern_loc This allows naming the hypotheses introduced in the context by ``simple inversion``. @@ -2273,47 +2511,54 @@ and an explanation of the underlying technique. *Non-dependent inversion*. - Let us consider the relation Le over natural numbers and the following - variables: + Let us consider the relation :g:`Le` over natural numbers: - .. coqtop:: all + .. coqtop:: reset in Inductive Le : nat -> nat -> Set := | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. - Variable Q : forall n m:nat, Le n m -> Prop. + Let us consider the following goal: .. coqtop:: none + Section Section. + Variable P : nat -> nat -> Prop. + Variable Q : forall n m:nat, Le n m -> Prop. Goal forall n m, Le (S n) m -> P n m. intros. - .. coqtop:: all + .. coqtop:: out Show. - To prove the goal, we may need to reason by cases on H and to derive - that m is necessarily of the form (S m 0 ) for certain m 0 and that - (Le n m 0 ). Deriving these conditions corresponds to proving that the - only possible constructor of (Le (S n) m) isLeS and that we can invert - the-> in the type of LeS. This inversion is possible because Le is the - smallest set closed by the constructors LeO and LeS. + To prove the goal, we may need to reason by cases on :g:`H` and to derive + that :g:`m` is necessarily of the form :g:`(S m0)` for certain :g:`m0` and that + :g:`(Le n m0)`. Deriving these conditions corresponds to proving that the only + possible constructor of :g:`(Le (S n) m)` is :g:`LeS` and that we can invert + the arrow in the type of :g:`LeS`. This inversion is possible because :g:`Le` + is the smallest set closed by the constructors :g:`LeO` and :g:`LeS`. - .. coqtop:: undo all + .. coqtop:: all inversion_clear H. - Note that m has been substituted in the goal for (S m0) and that the - hypothesis (Le n m0) has been added to the context. + Note that :g:`m` has been substituted in the goal for :g:`(S m0)` and that the + hypothesis :g:`(Le n m0)` has been added to the context. - Sometimes it is interesting to have the equality m=(S m0) in the - context to use it after. In that case we can use inversion that does + Sometimes it is interesting to have the equality :g:`m = (S m0)` in the + context to use it after. In that case we can use :tacn:`inversion` that does not clear the equalities: - .. coqtop:: undo all + .. coqtop:: none + + Abort. + Goal forall n m, Le (S n) m -> P n m. + intros. + + .. coqtop:: all inversion H. @@ -2323,31 +2568,27 @@ and an explanation of the underlying technique. Let us consider the following goal: - .. coqtop:: reset none + .. coqtop:: none - Inductive Le : nat -> nat -> Set := - | LeO : forall n:nat, Le 0 n - | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. - Variable Q : forall n m:nat, Le n m -> Prop. + Abort. Goal forall n m (H:Le (S n) m), Q (S n) m H. intros. - .. coqtop:: all + .. coqtop:: out Show. - As H occurs in the goal, we may want to reason by cases on its - structure and so, we would like inversion tactics to substitute H by + As :g:`H` occurs in the goal, we may want to reason by cases on its + structure and so, we would like inversion tactics to substitute :g:`H` by the corresponding @term in constructor form. Neither :tacn:`inversion` nor - :n:`inversion_clear` do such a substitution. To have such a behavior we + :tacn:`inversion_clear` do such a substitution. To have such a behavior we use the dependent inversion tactics: .. coqtop:: all dependent inversion_clear H. - Note that H has been substituted by (LeS n m0 l) andm by (S m0). + Note that :g:`H` has been substituted by :g:`(LeS n m0 l)` and :g:`m` by :g:`(S m0)`. .. example:: @@ -2716,6 +2957,12 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + .. tacv:: now_show @term + + This is a synonym of :n:`change @term`. It can be used to + make some proof steps explicit when refactoring a proof script + to make it readable. + .. seealso:: :ref:`Performing computations <performingcomputations>` .. _performingcomputations: @@ -3090,12 +3337,29 @@ the conversion in hypotheses :n:`{+ @ident}`. :name: fold This tactic applies to any goal. The term :n:`@term` is reduced using the - ``red`` tactic. Every occurrence of the resulting :n:`@term` in the goal is - then replaced by :n:`@term`. + :tacn:`red` tactic. Every occurrence of the resulting :n:`@term` in the goal is + then replaced by :n:`@term`. This tactic is particularly useful when a fixpoint + definition has been wrongfully unfolded, making the goal very hard to read. + On the other hand, when an unfolded function applied to its argument has been + reduced, the :tacn:`fold` tactic won't do anything. + + .. example:: + + .. coqtop:: all + + Goal ~0=0. + unfold not. + Fail progress fold not. + pattern (0 = 0). + fold not. + + .. coqtop:: none -.. tacv:: fold {+ @term} + Abort. - Equivalent to :n:`fold @term ; ... ; fold @term`. + .. tacv:: fold {+ @term} + + Equivalent to :n:`fold @term ; ... ; fold @term`. .. tacn:: pattern @term :name: pattern @@ -3171,130 +3435,141 @@ Automation :name: auto This tactic implements a Prolog-like resolution procedure to solve the - current goal. It first tries to solve the goal using the assumption - tactic, then it reduces the goal to an atomic one using intros and + current goal. It first tries to solve the goal using the :tacn:`assumption` + tactic, then it reduces the goal to an atomic one using :tacn:`intros` and introduces the newly generated hypotheses as hints. Then it looks at the list of tactics associated to the head symbol of the goal and tries to apply one of them (starting from the tactics with lower cost). This process is recursively applied to the generated subgoals. - By default, auto only uses the hypotheses of the current goal and the - hints of the database named core. + By default, :tacn:`auto` only uses the hypotheses of the current goal and + the hints of the database named ``core``. + + .. warning:: + + :tacn:`auto` uses a weaker version of :tacn:`apply` that is closer to + :tacn:`simple apply` so it is expected that sometimes :tacn:`auto` will + fail even if applying manually one of the hints would succeed. + + .. tacv:: auto @num -.. tacv:: auto @num + Forces the search depth to be :token:`num`. The maximal search depth + is 5 by default. - Forces the search depth to be :token:`num`. The maximal search depth - is 5 by default. + .. tacv:: auto with {+ @ident} + + Uses the hint databases :n:`{+ @ident}` in addition to the database ``core``. + + .. note:: -.. tacv:: auto with {+ @ident} + Use the fake database `nocore` if you want to *not* use the `core` + database. - Uses the hint databases :n:`{+ @ident}` in addition to the database core. + .. tacv:: auto with * + + Uses all existing hint databases. Using this variant is highly discouraged + in finished scripts since it is both slower and less robust than the variant + where the required databases are explicitly listed. .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of pre-defined databases and the way to create or extend a database. -.. tacv:: auto with * + .. tacv:: auto using {+ @ident__i} {? with {+ @ident } } - Uses all existing hint databases. + Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an + inductive type, it is the collection of its constructors which are added + as hints. - .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + .. note:: -.. tacv:: auto using {+ @ident__i} {? with {+ @ident } } + The hints passed through the `using` clause are used in the same + way as if they were passed through a hint database. Consequently, + they use a weaker version of :tacn:`apply` and :n:`auto using @ident` + may fail where :n:`apply @ident` succeeds. - Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an - inductive type, it is the collection of its constructors which are added - as hints. + Given that this can be seen as counter-intuitive, it could be useful + to have an option to use full-blown :tacn:`apply` for lemmas passed + through the `using` clause. Contributions welcome! -.. tacv:: info_auto + .. tacv:: info_auto - Behaves like auto but shows the tactics it uses to solve the goal. This - variant is very useful for getting a better understanding of automation, or - to know what lemmas/assumptions were used. + Behaves like :tacn:`auto` but shows the tactics it uses to solve the goal. This + variant is very useful for getting a better understanding of automation, or + to know what lemmas/assumptions were used. -.. tacv:: debug auto - :name: debug auto + .. tacv:: debug auto + :name: debug auto - Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, - including failing paths. + Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, + including failing paths. -.. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - This is the most general form, combining the various options. + This is the most general form, combining the various options. .. tacv:: trivial :name: trivial - This tactic is a restriction of auto that is not recursive + This tactic is a restriction of :tacn:`auto` that is not recursive and tries only hints that cost `0`. Typically it solves trivial equalities like :g:`X=X`. -.. tacv:: trivial with {+ @ident} - :undocumented: - -.. tacv:: trivial with * - :undocumented: - -.. tacv:: trivial using {+ @lemma} - :undocumented: - -.. tacv:: debug trivial - :name: debug trivial - :undocumented: - -.. tacv:: info_trivial - :name: info_trivial - :undocumented: - -.. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} - :undocumented: + .. tacv:: trivial with {+ @ident} + trivial with * + trivial using {+ @lemma} + debug trivial + info_trivial + {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} + :name: _; _; _; debug trivial; info_trivial; _ + :undocumented: .. note:: - :tacn:`auto` either solves completely the goal or else leaves it - intact. :tacn:`auto` and :tacn:`trivial` never fail. - -The following options enable printing of informative or debug information for -the :tacn:`auto` and :tacn:`trivial` tactics: + :tacn:`auto` and :tacn:`trivial` either solve completely the goal or + else succeed without changing the goal. Use :g:`solve [ auto ]` and + :g:`solve [ trivial ]` if you would prefer these tactics to fail when + they do not manage to solve the goal. .. flag:: Info Auto Debug Auto Info Trivial Debug Trivial - :undocumented: -.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + These options enable printing of informative or debug information for + the :tacn:`auto` and :tacn:`trivial` tactics. .. tacn:: eauto :name: eauto This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try resolution hints which would leave existential variables in the goal, - :tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply` - where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto` + :tacn:`eauto` does try them (informally speaking, it internally uses a tactic + close to :tacn:`simple eapply` instead of a tactic close to :tacn:`simple apply` + in the case of :tacn:`auto`). As a consequence, :tacn:`eauto` can solve such a goal: .. example:: .. coqtop:: all - Hint Resolve ex_intro. + Hint Resolve ex_intro : core. Goal forall P:nat -> Prop, P 0 -> exists n, P n. eauto. Note that ``ex_intro`` should be declared as a hint. -.. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - The various options for :tacn:`eauto` are the same as for :tacn:`auto`. + The various options for :tacn:`eauto` are the same as for :tacn:`auto`. -:tacn:`eauto` also obeys the following options: + :tacn:`eauto` also obeys the following options: -.. flag:: Info Eauto - Debug Eauto - :undocumented: + .. flag:: Info Eauto + Debug Eauto + :undocumented: -.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` .. tacn:: autounfold with {+ @ident} @@ -3586,15 +3861,15 @@ The general command to add a hint to some databases :n:`{+ @ident}` is the following. Beware, there is no operator precedence during parsing, one can check with :cmd:`Print HintDb` to verify the current cut expression: - .. productionlist:: `regexp` - e : ident hint or instance identifier - :| _ any hint - :| e\|e′ disjunction - :| e e′ sequence - :| e * Kleene star - :| emp empty - :| eps epsilon - :| ( e ) + .. productionlist:: regexp + e : `ident` hint or instance identifier + : _ any hint + : `e` | `e` disjunction + : `e` `e` sequence + : `e` * Kleene star + : emp empty + : eps epsilon + : ( `e` ) The `emp` regexp does not match any search path while `eps` matches the empty path. During proof search, the path of @@ -4299,15 +4574,15 @@ Automating .. _btauto_grammar: - .. productionlist:: `sentence` - t : x - :∣ true - :∣ false - :∣ orb t1 t2 - :∣ andb t1 t2 - :∣ xorb t1 t2 - :∣ negb t - :∣ if t1 then t2 else t3 + .. productionlist:: sentence + t : `x` + : true + : false + : orb `t` `t` + : andb `t` `t` + : xorb `t` `t` + : negb `t` + : if `t` then `t` else `t` Whenever the formula supplied is not a tautology, it also provides a counter-example. @@ -4343,7 +4618,7 @@ Automating distributivity, constant propagation) and comparing syntactically the results. -.. tacn:: ring_simplify {+ @term} +.. tacn:: ring_simplify {* @term} :name: ring_simplify This tactic applies the normalization procedure described above to @@ -4357,7 +4632,7 @@ the tactic and how to declare new ring structures. All declared field structures can be printed with the ``Print Rings`` command. .. tacn:: field - field_simplify {+ @term} + field_simplify {* @term} field_simplify_eq :name: field; field_simplify; field_simplify_eq |