diff options
Diffstat (limited to 'doc/sphinx/proofs')
| -rw-r--r-- | doc/sphinx/proofs/automatic-tactics/auto.rst | 671 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/index.rst | 1 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/proof-mode.rst | 102 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 860 |
4 files changed, 1634 insertions, 0 deletions
diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst new file mode 100644 index 0000000000..961af65b86 --- /dev/null +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -0,0 +1,671 @@ +.. _automation: + +Automation +---------- + +.. tacn:: auto + :name: auto + + This tactic implements a Prolog-like resolution procedure to solve the + 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, :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 @natural + + Forces the search depth to be :token:`natural`. 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:: + + Use the fake database `nocore` if you want to *not* use the `core` + database. + + .. 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 using {+ @qualid__i} {? with {+ @ident } } + + Uses lemmas :n:`@qualid__i` in addition to hints. If :n:`@qualid` is an + inductive type, it is the collection of its constructors which are added + as hints. + + .. note:: + + 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 @qualid` + may fail where :n:`apply @qualid` succeeds. + + 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 + + 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 + + Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, + including failing paths. + + .. tacv:: {? info_}auto {? @natural} {? using {+ @qualid}} {? with {+ @ident}} + + This is the most general form, combining the various options. + +.. tacv:: trivial + :name: trivial + + 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} + trivial with * + trivial using {+ @qualid} + debug trivial + info_trivial + {? info_}trivial {? using {+ @qualid}} {? with {+ @ident}} + :name: _; _; _; debug trivial; info_trivial; _ + :undocumented: + +.. note:: + :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 + + These flags 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 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 : 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 {? @natural} {? using {+ @qualid}} {? with {+ @ident}} + + The various options for :tacn:`eauto` are the same as for :tacn:`auto`. + + :tacn:`eauto` also obeys the following flags: + + .. flag:: Info Eauto + Debug Eauto + :undocumented: + + .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + + +.. tacn:: autounfold with {+ @ident} + :name: autounfold + + This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` + in the given databases. + +.. tacv:: autounfold with {+ @ident} in @goal_occurrences + + Performs the unfolding in the given clause (:token:`goal_occurrences`). + +.. tacv:: autounfold with * + + Uses the unfold hints declared in all the hint databases. + +.. tacn:: autorewrite with {+ @ident} + :name: autorewrite + + This tactic carries out rewritings according to the rewriting rule + bases :n:`{+ @ident}`. + + Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until + it fails. Once all the rules have been processed, if the main subgoal has + progressed (e.g., if it is distinct from the initial main goal) then the rules + of this base are processed again. If the main subgoal has not progressed then + the next base is processed. For the bases, the behavior is exactly similar to + the processing of the rewriting rules. + + The rewriting rule bases are built with the :cmd:`Hint Rewrite` + command. + +.. warning:: + + This tactic may loop if you build non terminating rewriting systems. + +.. tacv:: autorewrite with {+ @ident} using @tactic + + Performs, in the same way, all the rewritings of the bases :n:`{+ @ident}` + applying tactic to the main subgoal after each rewriting step. + +.. tacv:: autorewrite with {+ @ident} in @qualid + + Performs all the rewritings in hypothesis :n:`@qualid`. + +.. tacv:: autorewrite with {+ @ident} in @qualid using @tactic + + Performs all the rewritings in hypothesis :n:`@qualid` applying :n:`@tactic` + to the main subgoal after each rewriting step. + +.. tacv:: autorewrite with {+ @ident} in @goal_occurrences + + Performs all the rewriting in the clause :n:`@goal_occurrences`. + +.. seealso:: + + :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by + :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic. + +.. tacn:: easy + :name: easy + + This tactic tries to solve the current goal by a number of standard closing steps. + In particular, it tries to close the current goal using the closing tactics + :tacn:`trivial`, :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`contradiction` + and :tacn:`inversion` of hypothesis. + If this fails, it tries introducing variables and splitting and-hypotheses, + using the closing tactics afterwards, and splitting the goal using + :tacn:`split` and recursing. + + This tactic solves goals that belong to many common classes; in particular, many cases of + unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic. + +.. tacv:: now @tactic + :name: now + + Run :n:`@tactic` followed by :tacn:`easy`. This is a notation for :n:`@tactic; easy`. + +Controlling automation +-------------------------- + +.. _thehintsdatabasesforautoandeauto: + +The hints databases for auto and eauto +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The hints for :tacn:`auto` and :tacn:`eauto` are stored in databases. Each database +maps head symbols to a list of hints. + +.. cmd:: Print Hint @ident + + Use this command + to display the hints associated to the head symbol :n:`@ident` + (see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative + integer, and an optional pattern. The hints with lower cost are tried first. A + hint is tried by :tacn:`auto` when the conclusion of the current goal matches its + pattern or when it has no pattern. + +Creating Hint databases +``````````````````````` + +One can optionally declare a hint database using the command +:cmd:`Create HintDb`. If a hint is added to an unknown database, it will be +automatically created. + +.. cmd:: Create HintDb @ident {? discriminated} + + This command creates a new database named :n:`@ident`. The database is + implemented by a Discrimination Tree (DT) that serves as an index of + all the lemmas. The DT can use transparency information to decide if a + constant should be indexed or not + (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`), + making the retrieval more efficient. The legacy implementation (the default one + for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto` + goals), for non-Immediate hints and does not make use of transparency + hints, putting more work on the unification that is run after + retrieval (it keeps a list of the lemmas in case the DT is not used). + The new implementation enabled by the discriminated option makes use + of DTs in all cases and takes transparency information into account. + However, the order in which hints are retrieved from the DT may differ + from the order in which they were inserted, making this implementation + observationally different from the legacy one. + +.. cmd:: Hint @hint_definition : {+ @ident} + + The general command to add a hint to some databases :n:`{+ @ident}`. + + This command supports the :attr:`local`, :attr:`global` and :attr:`export` + locality attributes. When no locality is explictly given, the + command is :attr:`local` inside a section and :attr:`global` otherwise. + + + :attr:`local` hints are never visible from other modules, even if they + require or import the current module. Inside a section, the :attr:`local` + attribute is useless since hints do not survive anyway to the closure of + sections. + + + :attr:`export` are visible from other modules when they import the current + module. Requiring it is not enough. This attribute is only effective for + the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and + :cmd:`Hint Extern` variants of the command. + + + :attr:`global` hints are made available by merely requiring the current + module. + + The various possible :production:`hint_definition`\s are given below. + + .. cmdv:: Hint @hint_definition + + No database name is given: the hint is registered in the ``core`` database. + + .. deprecated:: 8.10 + + .. cmdv:: Hint Resolve @qualid {? | {? @natural} {? @pattern}} : @ident + :name: Hint Resolve + + This command adds :n:`simple apply @qualid` to the hint list with the head + symbol of the type of :n:`@qualid`. The cost of that hint is the number of + subgoals generated by :n:`simple apply @qualid` or :n:`@natural` if specified. The + associated :n:`@pattern` is inferred from the conclusion of the type of + :n:`@qualid` or the given :n:`@pattern` if specified. In case the inferred type + of :n:`@qualid` does not start with a product the tactic added in the hint list + is :n:`exact @qualid`. In case this type can however be reduced to a type + starting with a product, the tactic :n:`simple apply @qualid` is also stored in + the hints list. If the inferred type of :n:`@qualid` contains a dependent + quantification on a variable which occurs only in the premisses of the type + and not in its conclusion, no instance could be inferred for the variable by + unification with the goal. In this case, the hint is added to the hint list + of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A + typical example of a hint that is used only by :tacn:`eauto` is a transitivity + lemma. + + .. exn:: @qualid cannot be used as a hint + + The head symbol of the type of :n:`@qualid` is a bound variable + such that this tactic cannot be associated to a constant. + + .. cmdv:: Hint Resolve {+ @qualid} : @ident + + Adds each :n:`Hint Resolve @qualid`. + + .. cmdv:: Hint Resolve -> @qualid : @ident + + Adds the left-to-right implication of an equivalence as a hint (informally + the hint will be used as :n:`apply <- @qualid`, although as mentioned + before, the tactic actually used is a restricted version of + :tacn:`apply`). + + .. cmdv:: Hint Resolve <- @qualid + + Adds the right-to-left implication of an equivalence as a hint. + + .. cmdv:: Hint Immediate @qualid : @ident + :name: Hint Immediate + + This command adds :n:`simple apply @qualid; trivial` to the hint list associated + with the head symbol of the type of :n:`@ident` in the given database. This + tactic will fail if all the subgoals generated by :n:`simple apply @qualid` are + not solved immediately by the :tacn:`trivial` tactic (which only tries tactics + with cost 0).This command is useful for theorems such as the symmetry of + equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited + use in order to avoid useless proof-search. The cost of this tactic (which + never generates subgoals) is always 1, so that it is not used by :tacn:`trivial` + itself. + + .. exn:: @qualid cannot be used as a hint + :undocumented: + + .. cmdv:: Hint Immediate {+ @qualid} : @ident + + Adds each :n:`Hint Immediate @qualid`. + + .. cmdv:: Hint Constructors @qualid : @ident + :name: Hint Constructors + + If :token:`qualid` is an inductive type, this command adds all its constructors as + hints of type ``Resolve``. Then, when the conclusion of current goal has the form + :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor. + + .. exn:: @qualid is not an inductive type + :undocumented: + + .. cmdv:: Hint Constructors {+ @qualid} : @ident + + Extends the previous command for several inductive types. + + .. cmdv:: Hint Unfold @qualid : @ident + :name: Hint Unfold + + This adds the tactic :n:`unfold @qualid` to the hint list that will only be + used when the head constant of the goal is :token:`qualid`. + Its cost is 4. + + .. cmdv:: Hint Unfold {+ @qualid} + + Extends the previous command for several defined constants. + + .. cmdv:: Hint Transparent {+ @qualid} : @ident + Hint Opaque {+ @qualid} : @ident + :name: Hint Transparent; Hint Opaque + + This adds transparency hints to the database, making :n:`@qualid` + transparent or opaque constants during resolution. This information is used + during unification of the goal with any lemma in the database and inside the + discrimination network to relax or constrain it in the case of discriminated + databases. + + .. cmdv:: Hint Variables {| Transparent | Opaque } : @ident + Hint Constants {| Transparent | Opaque } : @ident + :name: Hint Variables; Hint Constants + + This sets the transparency flag used during unification of + hints in the database for all constants or all variables, + overwriting the existing settings of opacity. It is advised + to use this just after a :cmd:`Create HintDb` command. + + .. cmdv:: Hint Extern @natural {? @pattern} => @tactic : @ident + :name: Hint Extern + + This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and + :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a + :n:`@tactic` to execute. + + .. example:: + + .. coqtop:: in + + Hint Extern 4 (~(_ = _)) => discriminate : core. + + Now, when the head of the goal is a disequality, ``auto`` will try + discriminate if it does not manage to solve the goal with hints with a + cost less than 4. + + One can even use some sub-patterns of the pattern in + the tactic script. A sub-pattern is a question mark followed by an + identifier, like ``?X1`` or ``?X2``. Here is an example: + + .. example:: + + .. coqtop:: reset all + + Require Import List. + Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. + Goal forall a b:list (nat * nat), {a = b} + {a <> b}. + Info 1 auto with eqdec. + + .. cmdv:: Hint Cut @regexp : @ident + :name: Hint Cut + + .. warning:: + + These hints currently only apply to typeclass proof search and the + :tacn:`typeclasses eauto` tactic. + + This command can be used to cut the proof-search tree according to a regular + expression matching paths to be cut. The grammar for regular expressions is + the following. Beware, there is no operator precedence during parsing, one can + check with :cmd:`Print HintDb` to verify the current cut expression: + + .. prodn:: + regexp ::= @ident (hint or instance identifier) + | _ (any hint) + | @regexp | @regexp (disjunction) + | @regexp @regexp (sequence) + | @regexp * (Kleene star) + | emp (empty) + | eps (epsilon) + | ( @regexp ) + + The `emp` regexp does not match any search path while `eps` + matches the empty path. During proof search, the path of + successive successful hints on a search branch is recorded, as a + list of identifiers for the hints (note that :cmd:`Hint Extern`\’s do not have + an associated identifier). + Before applying any hint :n:`@ident` the current path `p` extended with + :n:`@ident` is matched against the current cut expression `c` associated to + the hint database. If matching succeeds, the hint is *not* applied. The + semantics of :n:`Hint Cut @regexp` is to set the cut expression + to :n:`c | regexp`, the initial cut expression being `emp`. + + .. cmdv:: Hint Mode @qualid {* {| + | ! | - } } : @ident + :name: Hint Mode + + This sets an optional mode of use of the identifier :n:`@qualid`. When + proof-search faces a goal that ends in an application of :n:`@qualid` to + arguments :n:`@term ... @term`, the mode tells if the hints associated to + :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``, + ``!`` or ``-`` items that specify if an argument of the identifier is to be + treated as an input (``+``), if its head only is an input (``!``) or an output + (``-``) of the identifier. For a mode to match a list of arguments, input + terms and input heads *must not* contain existential variables or be + existential variables respectively, while outputs can be any term. Multiple + modes can be declared for a single identifier, in that case only one mode + needs to match the arguments for the hints to be applied. The head of a term + is understood here as the applicative head, or the match or projection + scrutinee’s head, recursively, casts being ignored. :cmd:`Hint Mode` is + especially useful for typeclasses, when one does not want to support default + instances and avoid ambiguity in general. Setting a parameter of a class as an + input forces proof-search to be driven by that index of the class, with ``!`` + giving more flexibility by allowing existentials to still appear deeper in the + index but not at its head. + + .. note:: + + + One can use a :cmd:`Hint Extern` with no pattern to do + pattern matching on hypotheses using ``match goal with`` + inside the tactic. + + + If you want to add hints such as :cmd:`Hint Transparent`, + :cmd:`Hint Cut`, or :cmd:`Hint Mode`, for typeclass + resolution, do not forget to put them in the + ``typeclass_instances`` hint database. + + +Hint databases defined in the |Coq| standard library +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Several hint databases are defined in the |Coq| standard library. The +actual content of a database is the collection of hints declared +to belong to this database in each of the various modules currently +loaded. Especially, requiring new modules may extend the database. +At |Coq| startup, only the core database is nonempty and can be used. + +:core: This special database is automatically used by ``auto``, except when + pseudo-database ``nocore`` is given to ``auto``. The core database + contains only basic lemmas about negation, conjunction, and so on. + Most of the hints in this database come from the Init and Logic directories. + +:arith: This database contains all lemmas about Peano’s arithmetic proved in the + directories Init and Arith. + +:zarith: contains lemmas about binary signed integers from the + directories theories/ZArith. The database also contains + high-cost hints that call :tacn:`lia` on equations and + inequalities in ``nat`` or ``Z``. + +:bool: contains lemmas about booleans, mostly from directory theories/Bool. + +:datatypes: is for lemmas about lists, streams and so on that are mainly proved + in the Lists subdirectory. + +:sets: contains lemmas about sets and relations from the directories Sets and + Relations. + +:typeclass_instances: contains all the typeclass instances declared in the + environment, including those used for ``setoid_rewrite``, + from the Classes directory. + +:fset: internal database for the implementation of the ``FSets`` library. + +:ordered_type: lemmas about ordered types (as defined in the legacy ``OrderedType`` module), + mainly used in the ``FSets`` and ``FMaps`` libraries. + +You are advised not to put your own hints in the core database, but +use one or several databases specific to your development. + +.. _removehints: + +.. cmd:: Remove Hints {+ @term} : {+ @ident} + + This command removes the hints associated to terms :n:`{+ @term}` in databases + :n:`{+ @ident}`. + +.. _printhint: + +.. cmd:: Print Hint + + This command displays all hints that apply to the current goal. It + fails if no proof is being edited, while the two variants can be used + at every moment. + +**Variants:** + + +.. cmd:: Print Hint @ident + + This command displays only tactics associated with :n:`@ident` in the hints + list. This is independent of the goal being edited, so this command will not + fail if no goal is being edited. + +.. cmd:: Print Hint * + + This command displays all declared hints. + +.. cmd:: Print HintDb @ident + + This command displays all hints from database :n:`@ident`. + +.. _hintrewrite: + +.. cmd:: Hint Rewrite {+ @term} : {+ @ident} + + This vernacular command adds the terms :n:`{+ @term}` (their types must be + equalities) in the rewriting bases :n:`{+ @ident}` with the default orientation + (left to right). Notice that the rewriting bases are distinct from the :tacn:`auto` + hint bases and that :tacn:`auto` does not take them into account. + + This command is synchronous with the section mechanism (see :ref:`section-mechanism`): + when closing a section, all aliases created by ``Hint Rewrite`` in that + section are lost. Conversely, when loading a module, all ``Hint Rewrite`` + declarations at the global level of that module are loaded. + +**Variants:** + +.. cmd:: Hint Rewrite -> {+ @term} : {+ @ident} + + This is strictly equivalent to the command above (we only make explicit the + orientation which otherwise defaults to ->). + +.. cmd:: Hint Rewrite <- {+ @term} : {+ @ident} + + Adds the rewriting rules :n:`{+ @term}` with a right-to-left orientation in + the bases :n:`{+ @ident}`. + +.. cmd:: Hint Rewrite {? {| -> | <- } } {+ @one_term } {? using @ltac_expr } {? : {* @ident } } + + When the rewriting rules :n:`{+ @term}` in :n:`{+ @ident}` will be used, the + tactic ``tactic`` will be applied to the generated subgoals, the main subgoal + excluded. + +.. cmd:: Print Rewrite HintDb @ident + + This command displays all rewrite hints contained in :n:`@ident`. + +Hint locality +~~~~~~~~~~~~~ + +Hints provided by the ``Hint`` commands are erased when closing a section. +Conversely, all hints of a module ``A`` that are not defined inside a +section (and not defined with option ``Local``) become available when the +module ``A`` is required (using e.g. ``Require A.``). + +As of today, hints only have a binary behavior regarding locality, as +described above: either they disappear at the end of a section scope, +or they remain global forever. This causes a scalability issue, +because hints coming from an unrelated part of the code may badly +influence another development. It can be mitigated to some extent +thanks to the :cmd:`Remove Hints` command, +but this is a mere workaround and has some limitations (for instance, external +hints cannot be removed). + +A proper way to fix this issue is to bind the hints to their module scope, as +for most of the other objects |Coq| uses. Hints should only be made available when +the module they are defined in is imported, not just required. It is very +difficult to change the historical behavior, as it would break a lot of scripts. +We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior` +option which accepts three flags allowing for a fine-grained handling of +non-imported hints. + +.. opt:: Loose Hint Behavior {| "Lax" | "Warn" | "Strict" } + :name: Loose Hint Behavior + + This option accepts three values, which control the behavior of hints w.r.t. + :cmd:`Import`: + + - "Lax": this is the default, and corresponds to the historical behavior, + that is, hints defined outside of a section have a global scope. + + - "Warn": outputs a warning when a non-imported hint is used. Note that this + is an over-approximation, because a hint may be triggered by a run that + will eventually fail and backtrack, resulting in the hint not being + actually useful for the proof. + + - "Strict": changes the behavior of an unloaded hint to a immediate fail + tactic, allowing to emulate an import-scoped hint mechanism. + +.. _tactics-implicit-automation: + +Setting implicit automation tactics +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. cmd:: Proof with @tactic + + This command may be used to start a proof. It defines a default tactic + to be used each time a tactic command ``tactic``:sub:`1` is ended by ``...``. + In this case the tactic command typed by the user is equivalent to + ``tactic``:sub:`1` ``;tactic``. + + .. seealso:: :cmd:`Proof` in :ref:`proof-editing-mode`. + + + .. cmdv:: Proof with @tactic using {+ @ident} + + Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` + + .. cmdv:: Proof using {+ @ident} with @tactic + + Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst index 3f5526dba8..ebd75ef300 100644 --- a/doc/sphinx/proofs/writing-proofs/index.rst +++ b/doc/sphinx/proofs/writing-proofs/index.rst @@ -29,6 +29,7 @@ flavors of tactics, including the SSReflect proof language. ../../proof-engine/proof-handling ../../proof-engine/tactics + rewriting ../../proof-engine/ssreflect-proof-language ../../proof-engine/detailed-tactic-examples ../../user-extensions/proof-schemes diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst new file mode 100644 index 0000000000..8e9990c45f --- /dev/null +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -0,0 +1,102 @@ +.. tacn:: cycle @integer + :name: cycle + + Reorders the selected goals so that the first :n:`@integer` goals appear after the + other selected goals. + If :n:`@integer` is negative, it puts the last :n:`@integer` goals at the + beginning of the list. + The tactic is only useful with a goal selector, most commonly `all:`. + Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent + to `all: cycle 1`. See :tacn:`… : … (goal selector)`. + +.. example:: + + .. coqtop:: none reset + + Parameter P : nat -> Prop. + + .. coqtop:: all abort + + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. + repeat split. + all: cycle 2. + all: cycle -3. + +.. tacn:: swap @integer @integer + :name: swap + + Exchanges the position of the specified goals. + Negative values for :n:`@integer` indicate counting goals + backward from the end of the list of selected goals. Goals are indexed from 1. + The tactic is only useful with a goal selector, most commonly `all:`. + Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent + to `all: swap 1 3`. See :tacn:`… : … (goal selector)`. + +.. example:: + + .. coqtop:: all abort + + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. + repeat split. + all: swap 1 3. + all: swap 1 -1. + +.. tacn:: revgoals + :name: revgoals + + Reverses the order of the selected goals. The tactic is only useful with a goal + selector, most commonly `all :`. Note that other selectors reorder goals; + `1,3: revgoals` is not equivalent to `all: revgoals`. See :tacn:`… : … (goal selector)`. + + .. example:: + + .. coqtop:: all abort + + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. + repeat split. + all: revgoals. + +.. tacn:: shelve + :name: shelve + + This tactic moves all goals under focus to a shelf. While on the + shelf, goals will not be focused on. They can be solved by + unification, or they can be called back into focus with the command + :cmd:`Unshelve`. + + .. tacv:: shelve_unifiable + :name: shelve_unifiable + + Shelves only the goals under focus that are mentioned in other goals. + Goals that appear in the type of other goals can be solved by unification. + + .. example:: + + .. coqtop:: all abort + + Goal exists n, n=0. + refine (ex_intro _ _ _). + all: shelve_unifiable. + reflexivity. + +.. cmd:: Unshelve + + This command moves all the goals on the shelf (see :tacn:`shelve`) + from the shelf into focus, by appending them to the end of the current + list of focused goals. + +.. tacn:: unshelve @tactic + :name: unshelve + + Performs :n:`@tactic`, then unshelves existential variables added to the + shelf by the execution of :n:`@tactic`, prepending them to the current goal. + +.. tacn:: give_up + :name: give_up + + This tactic removes the focused goals from the proof. They are not + solved, and cannot be solved later in the proof. As the goals are not + solved, the proof cannot be closed. + + The ``give_up`` tactic can be used while editing a proof, to choose to + write the proof script in a non-sequential order. diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst new file mode 100644 index 0000000000..040849a9ef --- /dev/null +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -0,0 +1,860 @@ +================================= +Term rewriting and simplification +================================= + +.. _rewritingexpressions: + +Rewriting expressions +--------------------- + +These tactics use the equality :g:`eq:forall A:Type, A->A->Prop` defined in +file ``Logic.v`` (see :ref:`coq-library-logic`). The notation for :g:`eq T t u` is +simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. + +.. tacn:: rewrite @term + :name: rewrite + + This tactic applies to any goal. The type of :token:`term` must have the form + + ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``), eq term``:sub:`1` ``term``:sub:`2` ``.`` + + where :g:`eq` is the Leibniz equality or a registered setoid equality. + + Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, + resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then + replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. + Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, + and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new + subgoals. + + .. exn:: The @term provided does not end with an equation. + :undocumented: + + .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. + :undocumented: + + .. tacv:: rewrite -> @term + + Is equivalent to :n:`rewrite @term` + + .. tacv:: rewrite <- @term + + Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left + + .. tacv:: rewrite @term in @goal_occurrences + + Analogous to :n:`rewrite @term` but rewriting is done following + the clause :token:`goal_occurrences`. For instance: + + + :n:`rewrite H in H'` will rewrite `H` in the hypothesis + ``H'`` instead of the current goal. + + :n:`rewrite H in H' at 1, H'' at - 2 |- *` means + :n:`rewrite H; rewrite H in H' at 1; rewrite H in H'' at - 2.` + In particular a failure will happen if any of these three simpler tactics + fails. + + :n:`rewrite H in * |-` will do :n:`rewrite H in H'` for all hypotheses + :g:`H'` different from :g:`H`. + A success will happen as soon as at least one of these simpler tactics succeeds. + + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` + that succeeds if at least one of these two tactics succeeds. + + Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. + + .. tacv:: rewrite @term at @occurrences + + Rewrite only the given :token:`occurrences` of :token:`term`. Occurrences are + specified from left to right as for pattern (:tacn:`pattern`). The rewrite is + always performed using setoid rewriting, even for Leibniz’s equality, so one + has to ``Import Setoid`` to use this variant. + + .. tacv:: rewrite @term by @tactic + + Use tactic to completely solve the side-conditions arising from the + :tacn:`rewrite`. + + .. tacv:: rewrite {+, @orientation @term} {? in @ident } + + Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one + working on the first subgoal generated by the previous one. An :production:`orientation` + ``->`` or ``<-`` can be inserted before each :token:`term` to rewrite. One + unique clause can be added at the end after the keyword in; it will then + affect all rewrite operations. + + In all forms of rewrite described above, a :token:`term` to rewrite can be + immediately prefixed by one of the following modifiers: + + + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many + times as possible (perhaps zero time). This form never fails. + + :n:`@natural?` : works similarly, except that it will do at most :token:`natural` rewrites. + + `!` : works as `?`, except that at least one rewrite should succeed, otherwise + the tactic fails. + + :n:`@natural!` (or simply :n:`@natural`) : precisely :token:`natural` rewrites of :token:`term` will be done, + leading to failure if these :token:`natural` rewrites are not possible. + + .. tacv:: erewrite @term + :name: erewrite + + This tactic works as :n:`rewrite @term` but turning + unresolved bindings into existential variables, if any, instead of + failing. It has the same variants as :tacn:`rewrite` has. + + .. flag:: Keyed Unification + + Makes higher-order unification used by :tacn:`rewrite` rely on a set of keys to drive + unification. The subterms, considered as rewriting candidates, must start with + the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments + are then unified up to full reduction. + +.. tacn:: replace @term with @term’ + :name: replace + + This tactic applies to any goal. It replaces all free occurrences of :n:`@term` + in the current goal with :n:`@term’` and generates an equality :n:`@term = @term’` + as a subgoal. This equality is automatically solved if it occurs among + the assumptions, or if its symmetric form occurs. It is equivalent to + :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. + + .. exn:: Terms do not have convertible types. + :undocumented: + + .. tacv:: replace @term with @term’ by @tactic + + This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated + subgoal :n:`@term = @term’`. + + .. tacv:: replace @term + + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` or :n:`@term’ = @term`. + + .. tacv:: replace -> @term + + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` + + .. tacv:: replace <- @term + + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term’ = @term` + + .. tacv:: replace @term {? with @term} in @goal_occurrences {? by @tactic} + replace -> @term in @goal_occurrences + replace <- @term in @goal_occurrences + + Acts as before but the replacements take place in the specified clauses + (:token:`goal_occurrences`) (see :ref:`performingcomputations`) and not + only in the conclusion of the goal. The clause argument must not contain + any ``type of`` nor ``value of``. + +.. tacn:: subst @ident + :name: subst + + This tactic applies to a goal that has :n:`@ident` in its context and (at + least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` + with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by + :g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and + clears :n:`@ident` and :g:`H` from the context. + + If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also + unfolded and cleared. + + If :n:`@ident` is a section variable it is expected to have no + indirect occurrences in the goal, i.e. that no global declarations + implicitly depending on the section variable must be present in the + goal. + + .. note:: + + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the + first one is used. + + + If :g:`H` is itself dependent in the goal, it is replaced by the proof of + reflexivity of equality. + + .. tacv:: subst {+ @ident} + + This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. + + .. tacv:: subst + + This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses of the + context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` + or :n:`@ident := t` exists, with :n:`@ident` not occurring in + ``t`` and :n:`@ident` not a section variable with indirect + dependencies in the goal. + + .. flag:: Regular Subst Tactic + + This flag controls the behavior of :tacn:`subst`. When it is + activated (it is by default), :tacn:`subst` also deals with the following corner cases: + + + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` + and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not + a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` + or :n:`u = @ident`:sub:`2`; without the flag, a second call to + subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or + `t′` respectively. + + The presence of a recursive equation which without the flag would + be a cause of failure of :tacn:`subst`. + + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` + and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the + flag would be a cause of failure of :tacn:`subst`. + + Additionally, it prevents a local definition such as :n:`@ident := t` to be + unfolded which otherwise it would exceptionally unfold in configurations + containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` + with `u′` not a variable. Finally, it preserves the initial order of + hypotheses, which without the flag it may break. + default. + + .. exn:: Cannot find any non-recursive equality over :n:`@ident`. + :undocumented: + + .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`. + Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion. + + Raised when the variable is a section variable with indirect + dependencies in the goal. + + +.. tacn:: stepl @term + :name: stepl + + This tactic is for chaining rewriting steps. It assumes a goal of the + form :n:`R @term @term` where ``R`` is a binary relation and relies on a + database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` + where `eq` is typically a setoid equality. The application of :n:`stepl @term` + then replaces the goal by :n:`R @term @term` and adds a new goal stating + :n:`eq @term @term`. + + .. cmd:: Declare Left Step @term + + Adds :n:`@term` to the database used by :tacn:`stepl`. + + This tactic is especially useful for parametric setoids which are not accepted + as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see + :ref:`Generalizedrewriting`). + + .. tacv:: stepl @term by @tactic + + This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. + + .. tacv:: stepr @term by @tactic + :name: stepr + + This behaves as :tacn:`stepl` but on the right-hand-side of the binary + relation. Lemmas are expected to be of the form + :g:`forall x y z, R x y -> eq y z -> R x z`. + + .. cmd:: Declare Right Step @term + + Adds :n:`@term` to the database used by :tacn:`stepr`. + + +.. tacn:: change @term + :name: change + + This tactic applies to any goal. It implements the rule ``Conv`` given in + :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T` + with `U` providing that `U` is well-formed and that `T` and `U` are + convertible. + + .. exn:: Not convertible. + :undocumented: + + .. tacv:: change @term with @term’ + + This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. + The term :n:`@term` and :n:`@term’` must be convertible. + + .. tacv:: change @term at {+ @natural} with @term’ + + This replaces the occurrences numbered :n:`{+ @natural}` of :n:`@term` by :n:`@term’` + in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. + + .. exn:: Too few occurrences. + :undocumented: + + .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident + + 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: + +Performing computations +--------------------------- + +.. insertprodn red_expr pattern_occ + +.. prodn:: + red_expr ::= red + | hnf + | simpl {? @delta_flag } {? @ref_or_pattern_occ } + | cbv {? @strategy_flag } + | cbn {? @strategy_flag } + | lazy {? @strategy_flag } + | compute {? @delta_flag } + | vm_compute {? @ref_or_pattern_occ } + | native_compute {? @ref_or_pattern_occ } + | unfold {+, @unfold_occ } + | fold {+ @one_term } + | pattern {+, @pattern_occ } + | @ident + delta_flag ::= {? - } [ {+ @reference } ] + strategy_flag ::= {+ @red_flag } + | @delta_flag + red_flag ::= beta + | iota + | match + | fix + | cofix + | zeta + | delta {? @delta_flag } + ref_or_pattern_occ ::= @reference {? at @occs_nums } + | @one_term {? at @occs_nums } + occs_nums ::= {+ {| @natural | @ident } } + | - {| @natural | @ident } {* @int_or_var } + int_or_var ::= @integer + | @ident + unfold_occ ::= @reference {? at @occs_nums } + pattern_occ ::= @one_term {? at @occs_nums } + +This set of tactics implements different specialized usages of the +tactic :tacn:`change`. + +All conversion tactics (including :tacn:`change`) can be parameterized by the +parts of the goal where the conversion can occur. This is done using +*goal clauses* which consists in a list of hypotheses and, optionally, +of a reference to the conclusion of the goal. For defined hypothesis +it is possible to specify if the conversion should occur on the type +part, the body part or both (default). + +Goal clauses are written after a conversion tactic (tactics :tacn:`set`, +:tacn:`rewrite`, :tacn:`replace` and :tacn:`autorewrite` also use goal +clauses) and are introduced by the keyword `in`. If no goal clause is +provided, the default is to perform the conversion only in the +conclusion. + +The syntax and description of the various goal clauses is the +following: + ++ :n:`in {+ @ident} |-` only in hypotheses :n:`{+ @ident}` ++ :n:`in {+ @ident} |- *` in hypotheses :n:`{+ @ident}` and in the + conclusion ++ :n:`in * |-` in every hypothesis ++ :n:`in *` (equivalent to in :n:`* |- *`) everywhere ++ :n:`in (type of @ident) (value of @ident) ... |-` in type part of + :n:`@ident`, in the value part of :n:`@ident`, etc. + +For backward compatibility, the notation :n:`in {+ @ident}` performs +the conversion in hypotheses :n:`{+ @ident}`. + +.. tacn:: cbv {? @strategy_flag } + lazy {? @strategy_flag } + :name: cbv; lazy + + These parameterized reduction tactics apply to any goal and perform + the normalization of the goal according to the specified flags. In + correspondence with the kinds of reduction considered in |Coq| namely + :math:`\beta` (reduction of functional application), :math:`\delta` + (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`), + :math:`\iota` (reduction of + pattern matching over a constructed term, and unfolding of :g:`fix` and + :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the + flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``, + ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix`` + and ``cofix``. The ``delta`` flag itself can be refined into + :n:`delta [ {+ @qualid} ]` or :n:`delta - [ {+ @qualid} ]`, restricting in the first + case the constants to unfold to the constants listed, and restricting in the + second case the constant to unfold to all but the ones explicitly mentioned. + Notice that the ``delta`` flag does not apply to variables bound by a let-in + construction inside the :n:`@term` itself (use here the ``zeta`` flag). In + any cases, opaque constants are not unfolded (see :ref:`vernac-controlling-the-reduction-strategies`). + + Normalization according to the flags is done by first evaluating the + head of the expression into a *weak-head* normal form, i.e. until the + evaluation is blocked by a variable (or an opaque constant, or an + axiom), as e.g. in :g:`x u1 ... un` , or :g:`match x with ... end`, or + :g:`(fix f x {struct x} := ...) x`, or is a constructed form (a + :math:`\lambda`-expression, a constructor, a cofixpoint, an inductive type, a + product type, a sort), or is a redex that the flags prevent to reduce. Once a + weak-head normal form is obtained, subterms are recursively reduced using the + same strategy. + + Reduction to weak-head normal form can be done using two strategies: + *lazy* (``lazy`` tactic), or *call-by-value* (``cbv`` tactic). The lazy + strategy is a call-by-need strategy, with sharing of reductions: the + arguments of a function call are weakly evaluated only when necessary, + and if an argument is used several times then it is weakly computed + only once. This reduction is efficient for reducing expressions with + dead code. For instance, the proofs of a proposition :g:`exists x. P(x)` + reduce to a pair of a witness :g:`t`, and a proof that :g:`t` satisfies the + predicate :g:`P`. Most of the time, :g:`t` may be computed without computing + the proof of :g:`P(t)`, thanks to the lazy strategy. + + The call-by-value strategy is the one used in ML languages: the + arguments of a function call are systematically weakly evaluated + first. Despite the lazy strategy always performs fewer reductions than + the call-by-value strategy, the latter is generally more efficient for + evaluating purely computational expressions (i.e. with little dead code). + +.. tacv:: compute + cbv + :name: compute; _ + + These are synonyms for ``cbv beta delta iota zeta``. + +.. tacv:: lazy + + This is a synonym for ``lazy beta delta iota zeta``. + +.. tacv:: compute [ {+ @qualid} ] + cbv [ {+ @qualid} ] + + These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. + +.. tacv:: compute - [ {+ @qualid} ] + cbv - [ {+ @qualid} ] + + These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. + +.. tacv:: lazy [ {+ @qualid} ] + lazy - [ {+ @qualid} ] + + These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta` + and :n:`lazy beta delta -{+ @qualid} iota zeta`. + +.. tacv:: vm_compute + :name: vm_compute + + This tactic evaluates the goal using the optimized call-by-value evaluation + bytecode-based virtual machine described in :cite:`CompiledStrongReduction`. + This algorithm is dramatically more efficient than the algorithm used for the + :tacn:`cbv` tactic, but it cannot be fine-tuned. It is especially interesting for + full evaluation of algebraic objects. This includes the case of + reflection-based tactics. + +.. tacv:: native_compute + :name: native_compute + + This tactic evaluates the goal by compilation to |OCaml| as described + in :cite:`FullReduction`. If |Coq| is running in native code, it can be + typically two to five times faster than :tacn:`vm_compute`. Note however that the + compilation cost is higher, so it is worth using only for intensive + computations. + + .. flag:: NativeCompute Timing + + This flag causes all calls to the native compiler to print + timing information for the conversion to native code, + compilation, execution, and reification phases of native + compilation. Timing is printed in units of seconds of + wall-clock time. + + .. flag:: NativeCompute Profiling + + On Linux, if you have the ``perf`` profiler installed, this flag makes + it possible to profile :tacn:`native_compute` evaluations. + + .. opt:: NativeCompute Profile Filename @string + :name: NativeCompute Profile Filename + + This option specifies the profile output; the default is + ``native_compute_profile.data``. The actual filename used + will contain extra characters to avoid overwriting an existing file; that + filename is reported to the user. + That means you can individually profile multiple uses of + :tacn:`native_compute` in a script. From the Linux command line, run ``perf report`` + on the profile file to see the results. Consult the ``perf`` documentation + for more details. + +.. flag:: Debug Cbv + + This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print + information about the constants it encounters and the unfolding decisions it + makes. + +.. tacn:: red + :name: red + + This tactic applies to a goal that has the form:: + + forall (x:T1) ... (xk:Tk), T + + with :g:`T` :math:`\beta`:math:`\iota`:math:`\zeta`-reducing to :g:`c t`:sub:`1` :g:`... t`:sub:`n` and :g:`c` a + constant. If :g:`c` is transparent then it replaces :g:`c` with its + definition (say :g:`t`) and then reduces + :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules. + +.. exn:: Not reducible. + :undocumented: + +.. exn:: No head constant to reduce. + :undocumented: + +.. tacn:: hnf + :name: hnf + + This tactic applies to any goal. It replaces the current goal with its + head normal form according to the :math:`\beta`:math:`\delta`:math:`\iota`:math:`\zeta`-reduction rules, i.e. it + reduces the head of the goal until it becomes a product or an + irreducible term. All inner :math:`\beta`:math:`\iota`-redexes are also reduced. + The behavior of both :tacn:`hnf` can be tuned using the :cmd:`Arguments` command. + + Example: The term :g:`fun n : nat => S n + S n` is not reduced by :n:`hnf`. + +.. note:: + The :math:`\delta` rule only applies to transparent constants (see :ref:`vernac-controlling-the-reduction-strategies` + on transparency and opacity). + +.. tacn:: cbn + simpl + :name: cbn; simpl + + These tactics apply to any goal. They try to reduce a term to + something still readable instead of fully normalizing it. They perform + a sort of strong normalization with two key differences: + + + They unfold a constant if and only if it leads to a :math:`\iota`-reduction, + i.e. reducing a match or unfolding a fixpoint. + + While reducing a constant unfolding to (co)fixpoints, the tactics + use the name of the constant the (co)fixpoint comes from instead of + the (co)fixpoint definition in recursive calls. + + The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + predictable replacement for :tacn:`simpl`. + + The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and + :tacn:`lazy`. The behavior of both :tacn:`simpl` and :tacn:`cbn` + can be tuned using the :cmd:`Arguments` command. + + .. todo add "See <subsection about controlling the behavior of reduction strategies>" + to TBA section + + Notice that only transparent constants whose name can be reused in the + recursive calls are possibly unfolded by :tacn:`simpl`. For instance a + constant defined by :g:`plus' := plus` is possibly unfolded and reused in + the recursive calls, but a constant such as :g:`succ := plus (S O)` is + never unfolded. This is the main difference between :tacn:`simpl` and :tacn:`cbn`. + The tactic :tacn:`cbn` reduces whenever it will be able to reuse it or not: + :g:`succ t` is reduced to :g:`S t`. + +.. tacv:: cbn [ {+ @qualid} ] + cbn - [ {+ @qualid} ] + + These are respectively synonyms of :n:`cbn beta delta [ {+ @qualid} ] iota zeta` + and :n:`cbn beta delta - [ {+ @qualid} ] iota zeta` (see :tacn:`cbn`). + +.. tacv:: simpl @pattern + + This applies :tacn:`simpl` only to the subterms matching + :n:`@pattern` in the current goal. + +.. tacv:: simpl @pattern at {+ @natural} + + This applies :tacn:`simpl` only to the :n:`{+ @natural}` occurrences of the subterms + matching :n:`@pattern` in the current goal. + + .. exn:: Too few occurrences. + :undocumented: + +.. tacv:: simpl @qualid + simpl @string + + This applies :tacn:`simpl` only to the applicative subterms whose head occurrence + is the unfoldable constant :n:`@qualid` (the constant can be referred to by + its notation using :n:`@string` if such a notation exists). + +.. tacv:: simpl @qualid at {+ @natural} + simpl @string at {+ @natural} + + This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose + head occurrence is :n:`@qualid` (or :n:`@string`). + +.. flag:: Debug RAKAM + + This flag makes :tacn:`cbn` print various debugging information. + ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. + +.. tacn:: unfold @qualid + :name: unfold + + This tactic applies to any goal. The argument qualid must denote a + defined transparent constant or local definition (see + :ref:`gallina-definitions` and + :ref:`vernac-controlling-the-reduction-strategies`). The tactic + :tacn:`unfold` applies the :math:`\delta` rule to each occurrence + of the constant to which :n:`@qualid` refers in the current goal + and then replaces it with its :math:`\beta\iota\zeta`-normal form. + Use the general reduction tactics if you want to avoid this final + reduction, for instance :n:`cbv delta [@qualid]`. + + .. exn:: Cannot coerce @qualid to an evaluable reference. + + This error is frequent when trying to unfold something that has + defined as an inductive type (or constructor) and not as a + definition. + + .. example:: + + .. coqtop:: abort all fail + + Goal 0 <= 1. + unfold le. + + This error can also be raised if you are trying to unfold + something that has been marked as opaque. + + .. example:: + + .. coqtop:: abort all fail + + Opaque Nat.add. + Goal 1 + 0 = 1. + unfold Nat.add. + + .. tacv:: unfold @qualid in @goal_occurrences + + Replaces :n:`@qualid` in hypothesis (or hypotheses) designated + by :token:`goal_occurrences` with its definition and replaces + the hypothesis with its :math:`\beta`:math:`\iota` normal form. + + .. tacv:: unfold {+, @qualid} + + Replaces :n:`{+, @qualid}` with their definitions and replaces + the current goal with its :math:`\beta`:math:`\iota` normal + form. + + .. tacv:: unfold {+, @qualid at @occurrences } + + The list :token:`occurrences` specify the occurrences of + :n:`@qualid` to be unfolded. Occurrences are located from left + to right. + + .. exn:: Bad occurrence number of @qualid. + :undocumented: + + .. exn:: @qualid does not occur. + :undocumented: + + .. tacv:: unfold @string + + If :n:`@string` denotes the discriminating symbol of a notation + (e.g. "+") or an expression defining a notation (e.g. `"_ + + _"`), and this notation denotes an application whose head symbol + is an unfoldable constant, then the tactic unfolds it. + + .. tacv:: unfold @string%@ident + + This is variant of :n:`unfold @string` where :n:`@string` gets + its interpretation from the scope bound to the delimiting key + :token:`ident` instead of its default interpretation (see + :ref:`Localinterpretationrulesfornotations`). + + .. tacv:: unfold {+, {| @qualid | @string{? %@ident } } {? at @occurrences } } {? in @goal_occurrences } + + This is the most general form. + +.. tacn:: fold @term + :name: fold + + This tactic applies to any goal. The term :n:`@term` is reduced using the + :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 abort + + Goal ~0=0. + unfold not. + Fail progress fold not. + pattern (0 = 0). + fold not. + + .. tacv:: fold {+ @term} + + Equivalent to :n:`fold @term ; ... ; fold @term`. + +.. tacn:: pattern @term + :name: pattern + + This command applies to any goal. The argument :n:`@term` must be a free + subterm of the current goal. The command pattern performs :math:`\beta`-expansion + (the inverse of :math:`\beta`-reduction) of the current goal (say :g:`T`) by + + + replacing all occurrences of :n:`@term` in :g:`T` with a fresh variable + + abstracting this variable + + applying the abstracted goal to :n:`@term` + + For instance, if the current goal :g:`T` is expressible as + :math:`\varphi`:g:`(t)` where the notation captures all the instances of :g:`t` + in :math:`\varphi`:g:`(t)`, then :n:`pattern t` transforms it into + :g:`(fun x:A =>` :math:`\varphi`:g:`(x)) t`. This tactic can be used, for + instance, when the tactic ``apply`` fails on matching. + +.. tacv:: pattern @term at {+ @natural} + + Only the occurrences :n:`{+ @natural}` of :n:`@term` are considered for + :math:`\beta`-expansion. Occurrences are located from left to right. + +.. tacv:: pattern @term at - {+ @natural} + + All occurrences except the occurrences of indexes :n:`{+ @natural }` + of :n:`@term` are considered for :math:`\beta`-expansion. Occurrences are located from + left to right. + +.. tacv:: pattern {+, @term} + + Starting from a goal :math:`\varphi`:g:`(t`:sub:`1` :g:`... t`:sub:`m`:g:`)`, + the tactic :n:`pattern t`:sub:`1`:n:`, ..., t`:sub:`m` generates the + equivalent goal + :g:`(fun (x`:sub:`1`:g:`:A`:sub:`1`:g:`) ... (x`:sub:`m` :g:`:A`:sub:`m` :g:`) =>`:math:`\varphi`:g:`(x`:sub:`1` :g:`... x`:sub:`m` :g:`)) t`:sub:`1` :g:`... t`:sub:`m`. + If :g:`t`:sub:`i` occurs in one of the generated types :g:`A`:sub:`j` these + occurrences will also be considered and possibly abstracted. + +.. tacv:: pattern {+, @term at {+ @natural}} + + This behaves as above but processing only the occurrences :n:`{+ @natural}` of + :n:`@term` starting from :n:`@term`. + +.. tacv:: pattern {+, @term {? at {? -} {+, @natural}}} + + This is the most general syntax that combines the different variants. + +.. tacn:: with_strategy @strategy_level_or_var [ {+ @reference } ] @ltac_expr3 + :name: with_strategy + + Executes :token:`ltac_expr3`, applying the alternate unfolding + behavior that the :cmd:`Strategy` command controls, but only for + :token:`ltac_expr3`. This can be useful for guarding calls to + reduction in tactic automation to ensure that certain constants are + never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to + ensure that unfolding does not fail. + + .. example:: + + .. coqtop:: all reset abort + + Opaque id. + Goal id 10 = 10. + Fail unfold id. + with_strategy transparent [id] unfold id. + + .. warning:: + + Use this tactic with care, as effects do not persist past the + end of the proof script. Notably, this fine-tuning of the + conversion strategy is not in effect during :cmd:`Qed` nor + :cmd:`Defined`, so this tactic is most useful either in + combination with :tacn:`abstract`, which will check the proof + early while the fine-tuning is still in effect, or to guard + calls to conversion in tactic automation to ensure that, e.g., + :tacn:`unfold` does not fail just because the user made a + constant :cmd:`Opaque`. + + This can be illustrated with the following example involving the + factorial function. + + .. coqtop:: in reset + + Fixpoint fact (n : nat) : nat := + match n with + | 0 => 1 + | S n' => n * fact n' + end. + + Suppose now that, for whatever reason, we want in general to + unfold the :g:`id` function very late during conversion: + + .. coqtop:: in + + Strategy 1000 [id]. + + If we try to prove :g:`id (fact n) = fact n` by + :tacn:`reflexivity`, it will now take time proportional to + :math:`n!`, because |Coq| will keep unfolding :g:`fact` and + :g:`*` and :g:`+` before it unfolds :g:`id`, resulting in a full + computation of :g:`fact n` (in unary, because we are using + :g:`nat`), which takes time :math:`n!`. We can see this cross + the relevant threshold at around :math:`n = 9`: + + .. coqtop:: all abort + + Goal True. + Time assert (id (fact 8) = fact 8) by reflexivity. + Time assert (id (fact 9) = fact 9) by reflexivity. + + Note that behavior will be the same if you mark :g:`id` as + :g:`Opaque` because while most reduction tactics refuse to + unfold :g:`Opaque` constants, conversion treats :g:`Opaque` as + merely a hint to unfold this constant last. + + We can get around this issue by using :tacn:`with_strategy`: + + .. coqtop:: all + + Goal True. + Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] reflexivity. + + However, when we go to close the proof, we will run into + trouble, because the reduction strategy changes are local to the + tactic passed to :tacn:`with_strategy`. + + .. coqtop:: all abort fail + + exact I. + Timeout 1 Defined. + + We can fix this issue by using :tacn:`abstract`: + + .. coqtop:: all + + Goal True. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity. + exact I. + Time Defined. + + On small examples this sort of behavior doesn't matter, but + because |Coq| is a super-linear performance domain in so many + places, unless great care is taken, tactic automation using + :tacn:`with_strategy` may not be robustly performant when + scaling the size of the input. + + .. warning:: + + In much the same way this tactic does not play well with + :cmd:`Qed` and :cmd:`Defined` without using :tacn:`abstract` as + an intermediary, this tactic does not play well with ``coqchk``, + even when used with :tacn:`abstract`, due to the inability of + tactics to persist information about conversion hints in the + proof term. See `#12200 + <https://github.com/coq/coq/issues/12200>`_ for more details. + +Conversion tactics applied to hypotheses +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. tacn:: @tactic in {+, @ident} + + Applies :token:`tactic` (any of the conversion tactics listed in this + section) to the hypotheses :n:`{+ @ident}`. + + If :token:`ident` is a local definition, then :token:`ident` can be replaced by + :n:`type of @ident` to address not the body but the type of the local + definition. + + Example: :n:`unfold not in (type of H1) (type of H3)`. + +.. exn:: No such hypothesis: @ident. + :undocumented: |