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/automatic-tactics/logic.rst | 293 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/proof-mode.rst | 102 |
3 files changed, 1066 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/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst new file mode 100644 index 0000000000..1312c25f63 --- /dev/null +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -0,0 +1,293 @@ +.. _decisionprocedures: + +Decision procedures +------------------- + +.. tacn:: tauto + :name: tauto + + This tactic implements a decision procedure for intuitionistic propositional + calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff + :cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an + intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and + logical equivalence but does not unfold any other definition. + +.. example:: + + The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would + fail: + + .. coqtop:: reset all + + Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. + intros. + tauto. + +Moreover, if it has nothing else to do, :tacn:`tauto` performs introductions. +Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. +:tacn:`tauto` can for instance for: + +.. example:: + + .. coqtop:: reset all + + Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x. + tauto. + +.. note:: + In contrast, :tacn:`tauto` cannot solve the following goal + :g:`Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) ->` + :g:`forall x:nat, ~ ~ (A \/ P x).` + because :g:`(forall x:nat, ~ A -> P x)` cannot be treated as atomic and + an instantiation of `x` is necessary. + +.. tacv:: dtauto + :name: dtauto + + While :tacn:`tauto` recognizes inductively defined connectives isomorphic to + the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit``, ``True``, :tacn:`dtauto` also recognizes all inductive + types with one constructor and no indices, i.e. record-style connectives. + +.. tacn:: intuition @tactic + :name: intuition + + The tactic :tacn:`intuition` takes advantage of the search-tree built by the + decision procedure involved in the tactic :tacn:`tauto`. It uses this + information to generate a set of subgoals equivalent to the original one (but + simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If + this tactic fails on some goals then :tacn:`intuition` fails. In fact, + :tacn:`tauto` is simply :g:`intuition fail`. + + .. example:: + + For instance, the tactic :g:`intuition auto` applied to the goal:: + + (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O + + internally replaces it by the equivalent one:: + + (forall (x:nat), P x), B |- P O + + and then uses :tacn:`auto` which completes the proof. + +Originally due to César Muñoz, these tactics (:tacn:`tauto` and +:tacn:`intuition`) have been completely re-engineered by David Delahaye using +mainly the tactic language (see :ref:`ltac`). The code is +now much shorter and a significant increase in performance has been noticed. +The general behavior with respect to dependent types, unfolding and +introductions has slightly changed to get clearer semantics. This may lead to +some incompatibilities. + +.. tacv:: intuition + + Is equivalent to :g:`intuition auto with *`. + +.. tacv:: dintuition + :name: dintuition + + While :tacn:`intuition` recognizes inductively defined connectives + isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` also recognizes all inductive + types with one constructor and no indices, i.e. record-style connectives. + +.. flag:: Intuition Negation Unfolding + + Controls whether :tacn:`intuition` unfolds inner negations which do not need + to be unfolded. This flag is on by default. + +.. tacn:: rtauto + :name: rtauto + + The :tacn:`rtauto` tactic solves propositional tautologies similarly to what + :tacn:`tauto` does. The main difference is that the proof term is built using a + reflection scheme applied to a sequent calculus proof of the goal. The search + procedure is also implemented using a different technique. + + Users should be aware that this difference may result in faster proof-search + but slower proof-checking, and :tacn:`rtauto` might not solve goals that + :tacn:`tauto` would be able to solve (e.g. goals involving universal + quantifiers). + + Note that this tactic is only available after a ``Require Import Rtauto``. + +.. tacn:: firstorder + :name: firstorder + + The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to + first- order reasoning, written by Pierre Corbineau. It is not restricted to + usual logical connectives but instead may reason about any first-order class + inductive definition. + +.. opt:: Firstorder Solver @tactic + :name: Firstorder Solver + + The default tactic used by :tacn:`firstorder` when no rule applies is + :g:`auto with core`, it can be reset locally or globally using this option. + + .. cmd:: Print Firstorder Solver + + Prints the default tactic used by :tacn:`firstorder` when no rule applies. + +.. tacv:: firstorder @tactic + + Tries to solve the goal with :n:`@tactic` when no logical rule may apply. + +.. tacv:: firstorder using {+ @qualid} + + .. deprecated:: 8.3 + + Use the syntax below instead (with commas). + +.. tacv:: firstorder using {+, @qualid} + + Adds lemmas :n:`{+, @qualid}` to the proof-search environment. If :n:`@qualid` + refers to an inductive type, it is the collection of its constructors which are + added to the proof-search environment. + +.. tacv:: firstorder with {+ @ident} + + Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search + environment. + +.. tacv:: firstorder @tactic using {+, @qualid} with {+ @ident} + + This combines the effects of the different variants of :tacn:`firstorder`. + +.. opt:: Firstorder Depth @natural + :name: Firstorder Depth + + This option controls the proof-search depth bound. + +.. tacn:: congruence + :name: congruence + + The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard + Nelson and Oppen congruence closure algorithm, which is a decision procedure + for ground equalities with uninterpreted symbols. It also includes + constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal + is a non-quantified equality, congruence tries to prove it with non-quantified + equalities in the context. Otherwise it tries to infer a discriminable equality + from those in the context. Alternatively, congruence tries to prove that a + hypothesis is equal to the goal or to the negation of another hypothesis. + + :tacn:`congruence` is also able to take advantage of hypotheses stating + quantified equalities, but you have to provide a bound for the number of extra + equalities generated that way. Please note that one of the sides of the + equality must contain all the quantified variables in order for congruence to + match against it. + +.. example:: + + .. coqtop:: reset all + + Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a. + intros. + congruence. + Qed. + + Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : f = pair a -> Some (f c) = Some (f d) -> c=d. + intros. + congruence. + Qed. + +.. tacv:: congruence @natural + + Tries to add at most :token:`natural` instances of hypotheses stating quantified equalities + to the problem in order to solve it. A bigger value of :token:`natural` does not make + success slower, only failure. You might consider adding some lemmas as + hypotheses using assert in order for :tacn:`congruence` to use them. + +.. tacv:: congruence with {+ @term} + :name: congruence with + + Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps + in case you have partially applied constructors in your goal. + +.. exn:: I don’t know how to handle dependent equality. + + The decision procedure managed to find a proof of the goal or of a + discriminable equality but this proof could not be built in |Coq| because of + dependently-typed functions. + +.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms. + + The decision procedure could solve the goal with the provision that additional + arguments are supplied for some partially applied constructors. Any term of an + appropriate type will allow the tactic to successfully solve the goal. Those + additional arguments can be given to congruence by filling in the holes in the + terms given in the error message, using the :tacn:`congruence with` variant described above. + +.. flag:: Congruence Verbose + + This flag makes :tacn:`congruence` print debug information. + +.. tacn:: btauto + :name: btauto + + The tactic :tacn:`btauto` implements a reflexive solver for boolean + tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are + constructed over the following grammar: + + .. prodn:: + btauto_term ::= @ident + | true + | false + | orb @btauto_term @btauto_term + | andb @btauto_term @btauto_term + | xorb @btauto_term @btauto_term + | negb @btauto_term + | if @btauto_term then @btauto_term else @btauto_term + + Whenever the formula supplied is not a tautology, it also provides a + counter-example. + + Internally, it uses a system very similar to the one of the ring + tactic. + + Note that this tactic is only available after a ``Require Import Btauto``. + + .. exn:: Cannot recognize a boolean equality. + + The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` + doesn't introduce variables into the context on its own. + +.. tacv:: field + field_simplify {* @term} + field_simplify_eq + + The field tactic is built on the same ideas as ring: this is a + reflexive tactic that solves or simplifies equations in a field + structure. The main idea is to reduce a field expression (which is an + extension of ring expressions with the inverse and division + operations) to a fraction made of two polynomial expressions. + + Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}` + replaces the provided terms by their reduced fraction. + :n:`field_simplify_eq` applies when the conclusion is an equation: it + simplifies both hand sides and multiplies so as to cancel + denominators. So it produces an equation without division nor inverse. + + All of these 3 tactics may generate a subgoal in order to prove that + denominators are different from zero. + + See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to + declare new field structures. All declared field structures can be + printed with the Print Fields command. + +.. example:: + + .. coqtop:: reset all + + Require Import Reals. + Goal forall x y:R, + (x * y > 0)%R -> + (x * (1 / x + x / (x + y)))%R = + ((- 1 / y) * y * (- x * (x / (x + y)) - 1))%R. + + intros; field. + +.. seealso:: + + File plugins/ring/RealField.v for an example of instantiation, + theory theories/Reals for many examples of use of field. 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. |