diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 44 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 104 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 902 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 95 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 1965 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 129 |
6 files changed, 208 insertions, 3031 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 8663ac646b..6464f085b8 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -8,7 +8,7 @@ This chapter documents the tactic language |Ltac|. We start by giving the syntax followed by the informal semantics. To learn more about the language and especially about its foundations, please refer to :cite:`Del00`. -(Note the examples in the paper won't work as-is; |Coq| has evolved +(Note the examples in the paper won't work as-is; Coq has evolved since the paper was written.) .. example:: Basic tactic macros @@ -41,7 +41,7 @@ higher precedence than `+`. Usually `a/b/c` is given the :gdef:`left associativ interpretation `(a/b)/c` rather than the :gdef:`right associative` interpretation `a/(b/c)`. -In |Coq|, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4` +In Coq, the expression :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; @tactic__4` is interpreted as :n:`(try (repeat (@tactic__1 || @tactic__2)); @tactic__3); @tactic__4` because `||` is part of :token:`ltac_expr2`, which has higher precedence than :tacn:`try` and :tacn:`repeat` (at the level of :token:`ltac_expr3`), which @@ -60,7 +60,7 @@ The constructs in :token:`ltac_expr` are :term:`left associative`. ltac_expr3 ::= @l3_tactic | @ltac_expr2 ltac_expr2 ::= @ltac_expr1 + {| @ltac_expr2 | @binder_tactic } - | @ltac_expr1 || {| @ltac_expr2 | @binder_tactic } + | @ltac_expr1 %|| {| @ltac_expr2 | @binder_tactic } | @l2_tactic | @ltac_expr1 ltac_expr1 ::= @tactic_value @@ -729,7 +729,7 @@ First tactic to make progress: || Yet another way of branching without backtracking is the following structure: -.. tacn:: @ltac_expr1 || {| @ltac_expr2 | @binder_tactic } +.. tacn:: @ltac_expr1 %|| {| @ltac_expr2 | @binder_tactic } :name: || (first tactic making progress) :n:`@ltac_expr1 || @ltac_expr2` is @@ -784,7 +784,7 @@ single success: Checking for a single success: exactly_once ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| provides an experimental way to check that a tactic has *exactly +Coq provides an experimental way to check that a tactic has *exactly one* success: .. tacn:: exactly_once @ltac_expr3 @@ -813,7 +813,7 @@ one* success: Checking for failure: assert_fails ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: +Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr3 :name: assert_fails @@ -859,7 +859,7 @@ Checking for failure: assert_fails Checking for success: assert_succeeds ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one* +Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at least one* success: .. tacn:: assert_succeeds @ltac_expr3 @@ -905,7 +905,7 @@ Failing See the example for a comparison of the two constructs. - Note that if |Coq| terms have to be + Note that if Coq terms have to be printed as part of the failure, term construction always forces the tactic into the goals, meaning that if there are no goals when it is evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed. @@ -990,7 +990,7 @@ amount of time: timeout with some other tacticals. This tactical is hence proposed only for convenience during debugging or other development phases, we strongly advise you to not leave any timeout in final scripts. Note also that - this tactical isn’t available on the native Windows port of |Coq|. + this tactical isn’t available on the native Windows port of Coq. Timing a tactic ~~~~~~~~~~~~~~~ @@ -1353,8 +1353,8 @@ Pattern matching on goals and hypotheses: match goal .. insertprodn goal_pattern match_hyp .. prodn:: - goal_pattern ::= {*, @match_hyp } |- @match_pattern - | [ {*, @match_hyp } |- @match_pattern ] + goal_pattern ::= {*, @match_hyp } %|- @match_pattern + | [ {*, @match_hyp } %|- @match_pattern ] | _ match_hyp ::= @name : @match_pattern | @name := @match_pattern @@ -1523,7 +1523,7 @@ produce subgoals but generates a term to be used in tactic expressions: Generating fresh hypothesis names ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Tactics sometimes need to generate new names for hypothesis. Letting |Coq| +Tactics sometimes need to generate new names for hypothesis. Letting Coq choose a name with the intro tactic is not so good since it is very awkward to retrieve that name. The following expression returns an identifier: @@ -1730,6 +1730,8 @@ Defining |Ltac| symbols |Ltac| toplevel definitions are made as follows: +.. index:: ::= + .. cmd:: Ltac @tacdef_body {* with @tacdef_body } :name: Ltac @@ -1754,10 +1756,15 @@ Defining |Ltac| symbols Defines a user-defined symbol, but gives an error if the symbol has already been defined. -.. todo apparent inconsistency: "Ltac intros := idtac" seems like it redefines/hides an existing tactic, - but in fact it creates a tactic which can only be called by it's qualified name. This is true in general - of tactic notations. The only way to overwrite most primitive tactics, and any user-defined tactic - notation, is with another tactic notation. + .. todo apparent inconsistency: + + "Ltac intros := idtac" seems like it redefines/hides an + existing tactic, but in fact it creates a tactic which can + only be called by its qualified name. This is true in + general of tactic notations. The only way to overwrite most + primitive tactics, and any user-defined tactic notation, is + with another tactic notation. + .. exn:: There is already an Ltac named @qualid :undocumented: @@ -1767,7 +1774,8 @@ Defining |Ltac| symbols do not count as user-defined tactics for `::=`. If :attr:`local` is not specified, the redefinition applies across module boundaries. - .. exn: There is no Ltac named @qualid + .. exn:: There is no Ltac named @qualid + :undocumented: :n:`{* with @tacdef_body }` Permits definition of mutually recursive tactics. @@ -1885,7 +1893,7 @@ Proving that a list is a permutation of a second list From Section :ref:`ltac-syntax` we know that Ltac has a primitive notion of integers, but they are only used as arguments for primitive tactics and we cannot make computations with them. Thus, - instead, we use |Coq|'s natural number type :g:`nat`. + instead, we use Coq's natural number type :g:`nat`. .. coqtop:: in diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 64fc1133f0..a46f4fb894 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -4,7 +4,7 @@ Ltac2 ===== The |Ltac| tactic language is probably one of the ingredients of the success of -|Coq|, yet it is at the same time its Achilles' heel. Indeed, |Ltac|: +Coq, yet it is at the same time its Achilles' heel. Indeed, |Ltac|: - has often unclear semantics - is very non-uniform due to organic growth @@ -30,7 +30,7 @@ as Ltac1. Current limitations include: - There are a number of tactics that are not yet supported in Ltac2 because - the interface |OCaml| and/or Ltac2 notations haven't been written. See + the interface OCaml and/or Ltac2 notations haven't been written. See :ref:`defining_tactics`. - Missing usability features such as: @@ -38,7 +38,6 @@ Current limitations include: - Printing functions are limited and awkward to use. Only a few data types are printable. - Deep pattern matching and matching on tuples don't work. - - If statements on Ltac2 boolean values - A convenient way to build terms with casts through the low-level API. Because the cast type is opaque, building terms with casts currently requires an awkward construction like the following, which also incurs extra overhead to repeat typechecking for each @@ -90,7 +89,7 @@ In particular, Ltac2 is: * together with the Hindley-Milner type system - a language featuring meta-programming facilities for the manipulation of - |Coq|-side terms + Coq-side terms - a language featuring notation facilities to help write palatable scripts We describe these in more detail in the remainder of this document. @@ -108,14 +107,14 @@ that ML constitutes a sweet spot in PL design, as it is relatively expressive while not being either too lax (unlike dynamic typing) nor too strict (unlike, say, dependent types). -The main goal of Ltac2 is to serve as a meta-language for |Coq|. As such, it +The main goal of Ltac2 is to serve as a meta-language for Coq. As such, it naturally fits in the ML lineage, just as the historical ML was designed as the tactic language for the LCF prover. It can also be seen as a general-purpose -language, by simply forgetting about the |Coq|-specific features. +language, by simply forgetting about the Coq-specific features. Sticking to a standard ML type system can be considered somewhat weak for a -meta-language designed to manipulate |Coq| terms. In particular, there is no -way to statically guarantee that a |Coq| term resulting from an Ltac2 +meta-language designed to manipulate Coq terms. In particular, there is no +way to statically guarantee that a Coq term resulting from an Ltac2 computation will be well-typed. This is actually a design choice, motivated by backward compatibility with Ltac1. Instead, well-typedness is deferred to dynamic checks, allowing many primitive functions to fail whenever they are @@ -138,7 +137,7 @@ Type Syntax ~~~~~~~~~~~ At the level of terms, we simply elaborate on Ltac1 syntax, which is quite -close to |OCaml|. Types follow the simply-typed syntax of |OCaml|. +close to OCaml. Types follow the simply-typed syntax of OCaml. .. insertprodn ltac2_type ltac2_typevar @@ -160,7 +159,7 @@ declarations such as algebraic datatypes and records. Built-in types include: -- ``int``, machine integers (size not specified, in practice inherited from |OCaml|) +- ``int``, machine integers (size not specified, in practice inherited from OCaml) - ``string``, mutable strings - ``'a array``, mutable arrays - ``exn``, exceptions @@ -201,7 +200,7 @@ One can define new types with the following commands. :token:`tac2typ_knd` should be in the form :n:`[ {? {? %| } {+| @tac2alg_constructor } } ]`. Without :n:`{| := | ::= }` - Defines an abstract type for use representing data from |OCaml|. Not for + Defines an abstract type for use representing data from OCaml. Not for end users. :n:`with @tac2typ_def` @@ -227,9 +226,9 @@ One can define new types with the following commands. .. cmd:: Ltac2 @ external @ident : @ltac2_type := @string @string :name: Ltac2 external - Declares abstract terms. Frequently, these declare |OCaml| functions - defined in |Coq| and give their type information. They can also declare - data structures from |OCaml|. This command has no use for the end user. + Declares abstract terms. Frequently, these declare OCaml functions + defined in Coq and give their type information. They can also declare + data structures from OCaml. This command has no use for the end user. APIs ~~~~ @@ -345,12 +344,10 @@ Ltac2 Definitions .. coqtop:: all - Ltac2 mutable rec f b := match b with true => 0 | _ => f true end. - Ltac2 Set f := fun b => - match b with true => 1 | _ => f true end. + Ltac2 mutable rec f b := if b then 0 else f true. + Ltac2 Set f := fun b => if b then 1 else f true. Ltac2 Eval (f false). - Ltac2 Set f as oldf := fun b => - match b with true => 2 | _ => oldf false end. + Ltac2 Set f as oldf := fun b => if b then 2 else oldf false. Ltac2 Eval (f false). In the definition, the `f` in the body is resolved statically @@ -363,7 +360,7 @@ Reduction ~~~~~~~~~ We use the usual ML call-by-value reduction, with an otherwise unspecified -evaluation order. This is a design choice making it compatible with |OCaml|, +evaluation order. This is a design choice making it compatible with OCaml, if ever we implement native compilation. The expected equations are as follows:: (fun x => t) V ≡ t{x := V} (βv) @@ -407,7 +404,7 @@ standard IO monad as the ambient effectful world, Ltac2 is has a tactic monad. Note that the order of evaluation of application is *not* specified and is -implementation-dependent, as in |OCaml|. +implementation-dependent, as in OCaml. We recall that the `Proofview.tactic` monad is essentially a IO monad together with backtracking state representing the proof state. @@ -538,7 +535,7 @@ is a proper one or referring to something in the Ltac context. Likewise, in Ltac1, constr parsing is implicit, so that ``foo 0`` is not ``foo`` applied to the Ltac integer expression ``0`` (|Ltac| does have a -notion of integers, though it is not first-class), but rather the |Coq| term +notion of integers, though it is not first-class), but rather the Coq term :g:`Datatypes.O`. The implicit parsing is confusing to users and often gives unexpected results. @@ -565,16 +562,16 @@ Built-in quotations | ltac1 : ( @ltac1_expr_in_env ) | ltac1val : ( @ltac1_expr_in_env ) ltac1_expr_in_env ::= @ltac_expr - | {* @ident } |- @ltac_expr + | {* @ident } %|- @ltac_expr The current implementation recognizes the following built-in quotations: - ``ident``, which parses identifiers (type ``Init.ident``). -- ``constr``, which parses |Coq| terms and produces an-evar free term at runtime +- ``constr``, which parses Coq terms and produces an-evar free term at runtime (type ``Init.constr``). -- ``open_constr``, which parses |Coq| terms and produces a term potentially with +- ``open_constr``, which parses Coq terms and produces a term potentially with holes at runtime (type ``Init.constr`` as well). -- ``pattern``, which parses |Coq| patterns and produces a pattern used for term +- ``pattern``, which parses Coq patterns and produces a pattern used for term matching (type ``Init.pattern``). - ``reference`` Qualified names are globalized at internalization into the corresponding global reference, @@ -617,7 +614,7 @@ Term Antiquotations Syntax ++++++ -One can also insert Ltac2 code into |Coq| terms, similar to what is possible in +One can also insert Ltac2 code into Coq terms, similar to what is possible in Ltac1. .. prodn:: @@ -629,7 +626,7 @@ for their side-effects. Semantics +++++++++ -A quoted |Coq| term is interpreted in two phases, internalization and +A quoted Coq term is interpreted in two phases, internalization and evaluation. - Internalization is part of the static semantics, that is, it is done at Ltac2 @@ -637,17 +634,17 @@ evaluation. - Evaluation is part of the dynamic semantics, that is, it is done when a term gets effectively computed by Ltac2. -Note that typing of |Coq| terms is a *dynamic* process occurring at Ltac2 +Note that typing of Coq terms is a *dynamic* process occurring at Ltac2 evaluation time, and not at Ltac2 typing time. Static semantics **************** -During internalization, |Coq| variables are resolved and antiquotations are -type checked as Ltac2 terms, effectively producing a ``glob_constr`` in |Coq| +During internalization, Coq variables are resolved and antiquotations are +type checked as Ltac2 terms, effectively producing a ``glob_constr`` in Coq implementation terminology. Note that although it went through the type checking of **Ltac2**, the resulting term has not been fully computed and -is potentially ill-typed as a runtime **|Coq|** term. +is potentially ill-typed as a runtime **Coq** term. .. example:: @@ -669,7 +666,7 @@ of the corresponding term expression. let x := '0 in constr:(1 + ltac2:(exact x)) Beware that the typing environment of antiquotations is **not** -expanded by the |Coq| binders from the term. +expanded by the Coq binders from the term. .. example:: @@ -692,17 +689,17 @@ as follows. `constr:(fun x : nat => ltac2:(exact (hyp @x)))` -This pattern is so common that we provide dedicated Ltac2 and |Coq| term notations +This pattern is so common that we provide dedicated Ltac2 and Coq term notations for it. - `&x` as an Ltac2 expression expands to `hyp @x`. -- `&x` as a |Coq| constr expression expands to +- `&x` as a Coq constr expression expands to `ltac2:(Control.refine (fun () => hyp @x))`. -In the special case where Ltac2 antiquotations appear inside a |Coq| term +In the special case where Ltac2 antiquotations appear inside a Coq term notation, the notation variables are systematically bound in the body of the tactic expression with type `Ltac2.Init.preterm`. Such a type represents -untyped syntactic |Coq| expressions, which can by typed in the +untyped syntactic Coq expressions, which can by typed in the current context using the `Ltac2.Constr.pretype` function. .. example:: @@ -748,9 +745,9 @@ the notation section. .. prodn:: term += $@lident -In a |Coq| term, writing :g:`$x` is semantically equivalent to +In a Coq term, writing :g:`$x` is semantically equivalent to :g:`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to -insert in a concise way an Ltac2 variable of type :n:`constr` into a |Coq| term. +insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term. Match over terms ~~~~~~~~~~~~~~~~ @@ -981,7 +978,7 @@ Match over goals .. prodn:: goal_match_list ::= {? %| } {+| @gmatch_rule } gmatch_rule ::= @gmatch_pattern => @ltac2_expr - gmatch_pattern ::= [ {*, @gmatch_hyp_pattern } |- @ltac2_match_pattern ] + gmatch_pattern ::= [ {*, @gmatch_hyp_pattern } %|- @ltac2_match_pattern ] gmatch_hyp_pattern ::= @name : @ltac2_match_pattern Matches over goals, similar to Ltac1 :tacn:`match goal`. @@ -1129,7 +1126,7 @@ Match on values .. tacn:: match @ltac2_expr5 with {? @ltac2_branches } end :name: match (Ltac2) - Matches a value, akin to the |OCaml| `match` construct. By itself, it doesn't cause backtracking + Matches a value, akin to the OCaml `match` construct. By itself, it doesn't cause backtracking as do the `*match*!` and `*match*! goal` constructs. .. insertprodn ltac2_branches atomic_tac2pat @@ -1149,6 +1146,13 @@ Match on values | @tac2pat1 , {*, @tac2pat1 } | @tac2pat1 +.. tacn:: if @ltac2_expr5__test then @ltac2_expr5__then else @ltac2_expr5__else + :name: if-then-else (Ltac2) + + Equivalent to a :tacn:`match <match (Ltac2)>` on a boolean value. If the + :n:`@ltac2_expr5__test` evaluates to true, :n:`@ltac2_expr5__then` + is evaluated. Otherwise :n:`@ltac2_expr5__else` is evaluated. + .. note:: For now, deep pattern matching is not implemented. @@ -1182,7 +1186,7 @@ Notations into the right-hand side. The right-hand side is typechecked when the notation is used, not when it is defined. In the following example, `x` is the formal parameter name and `constr` is its :ref:`syntactic class<syntactic_classes>`. `print` and `of_constr` are - functions provided by |Coq| through `Message.v`. + functions provided by Coq through `Message.v`. .. todo "print" doesn't seem to pay attention to "Set Printing All" @@ -1254,7 +1258,7 @@ Abbreviations Introduces a special kind of notation, called an abbreviation, that does not add any parsing rules. It is similar in - spirit to |Coq| abbreviations (see :cmd:`Notation (abbreviation)`, + spirit to Coq abbreviations (see :cmd:`Notation (abbreviation)`, insofar as its main purpose is to give an absolute name to a piece of pure syntax, which can be transparently referred to by this name as if it were a proper definition. @@ -1281,7 +1285,7 @@ Abbreviations Defining tactics ~~~~~~~~~~~~~~~~ -Built-in tactics (those defined in |OCaml| code in the |Coq| executable) and Ltac1 tactics, +Built-in tactics (those defined in OCaml code in the Coq executable) and Ltac1 tactics, which are defined in `.v` files, must be defined through notations. (Ltac2 tactics can be defined with :cmd:`Ltac2`. @@ -1289,7 +1293,7 @@ Notations for many but not all built-in tactics are defined in `Notations.v`, wh loaded with Ltac2. The Ltac2 syntax for these tactics is often identical or very similar to the tactic syntax described in other chapters of this documentation. These notations rely on tactic functions declared in `Std.v`. Functions corresponding to some built-in tactics may not yet be defined in the -|Coq| executable or declared in `Std.v`. Adding them may require code changes to |Coq| or defining +Coq executable or declared in `Std.v`. Adding them may require code changes to Coq or defining workarounds through Ltac1 (described below). Two examples of syntax differences: @@ -1321,7 +1325,7 @@ Syntactic classes ~~~~~~~~~~~~~~~~~ The simplest syntactic classes in Ltac2 notations represent individual nonterminals -from the |Coq| grammar. Only a few selected nonterminals are available as syntactic classes. +from the Coq grammar. Only a few selected nonterminals are available as syntactic classes. In addition, there are metasyntactic operations for describing more complex syntax, such as making an item optional or representing a list of items. When parsing, each syntactic class expression returns a value that's bound to a name in the @@ -1598,8 +1602,8 @@ Here is the syntax for the :n:`q_*` nonterminals: ltac2_clause ::= in @ltac2_in_clause | at @ltac2_occs_nums ltac2_in_clause ::= * {? @ltac2_occs } - | * |- {? @ltac2_concl_occ } - | {*, @ltac2_hypident_occ } {? |- {? @ltac2_concl_occ } } + | * %|- {? @ltac2_concl_occ } + | {*, @ltac2_hypident_occ } {? %|- {? @ltac2_concl_occ } } .. insertprodn q_occurrences ltac2_hypident @@ -1629,7 +1633,7 @@ Here is the syntax for the :n:`q_*` nonterminals: .. insertprodn ltac2_oriented_rewriter ltac2_rewriter .. prodn:: - ltac2_oriented_rewriter ::= {| -> | <- } @ltac2_rewriter + ltac2_oriented_rewriter ::= {? {| -> | <- } } @ltac2_rewriter ltac2_rewriter ::= {? @natural } {? {| ? | ! } } @ltac2_constr_with_bindings .. insertprodn ltac2_for_each_goal ltac2_goal_tactics @@ -1795,7 +1799,7 @@ Transition from Ltac1 Owing to the use of a lot of notations, the transition should not be too difficult. In particular, it should be possible to do it incrementally. That said, we do *not* guarantee it will be a blissful walk either. -Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with |Coq| +Hopefully, owing to the fact Ltac2 is typed, the interactive dialogue with Coq will help you. We list the major changes and the transition strategies hereafter. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index b09d6146d8..7f5aacbfdb 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -1,901 +1,5 @@ -.. _proofhandling: +:orphan: -------------------- - Proof handling -------------------- +.. raw:: html -In |Coq|’s proof editing mode all top-level commands documented in -Chapter :ref:`vernacularcommands` remain available and the user has access to specialized -commands dealing with proof development pragmas documented in this -section. They can also use some other specialized commands called -*tactics*. They are the very tools allowing the user to deal with -logical reasoning. They are documented in Chapter :ref:`tactics`. - -|Coq| user interfaces usually have a way of marking whether the user has -switched to proof editing mode. For instance, in coqtop the prompt ``Coq <`` is changed into -:n:`@ident <` where :token:`ident` is the declared name of the theorem currently edited. - -At each stage of a proof development, one has a list of goals to -prove. Initially, the list consists only in the theorem itself. After -having applied some tactics, the list of goals contains the subgoals -generated by the tactics. - -To each subgoal is associated a number of hypotheses called the *local context* -of the goal. Initially, the local context contains the local variables and -hypotheses of the current section (see Section :ref:`gallina-assumptions`) and -the local variables and hypotheses of the theorem statement. It is enriched by -the use of certain tactics (see e.g. :tacn:`intro`). - -When a proof is completed, the message ``Proof completed`` is displayed. -One can then register this proof as a defined constant in the -environment. Because there exists a correspondence between proofs and -terms of λ-calculus, known as the *Curry-Howard isomorphism* -:cite:`How80,Bar81,Gir89,H89`, |Coq| stores proofs as terms of |Cic|. Those -terms are called *proof terms*. - - -.. exn:: No focused proof. - - |Coq| raises this error message when one attempts to use a proof editing command - out of the proof editing mode. - -.. _proof-editing-mode: - -Entering and leaving proof editing mode ---------------------------------------- - -The proof editing mode is entered by asserting a statement, which typically is -the assertion of a theorem using an assertion command like :cmd:`Theorem`. The -list of assertion commands is given in :ref:`Assertions`. The command -:cmd:`Goal` can also be used. - -.. cmd:: Goal @type - - This is intended for quick assertion of statements, without knowing in - advance which name to give to the assertion, typically for quick - testing of the provability of a statement. If the proof of the - statement is eventually completed and validated, the statement is then - bound to the name ``Unnamed_thm`` (or a variant of this name not already - used for another statement). - -.. cmd:: Qed - - This command is available in interactive editing proof mode when the - proof is completed. Then :cmd:`Qed` extracts a proof term from the proof - script, switches back to |Coq| top-level and attaches the extracted - proof term to the declared name of the original goal. The name is - added to the environment as an opaque constant. - - .. exn:: Attempt to save an incomplete proof. - :undocumented: - - .. note:: - - Sometimes an error occurs when building the proof term, because - tactics do not enforce completely the term construction - constraints. - - The user should also be aware of the fact that since the - proof term is completely rechecked at this point, one may have to wait - a while when the proof is large. In some exceptional cases one may - even incur a memory overflow. - -.. cmd:: Save @ident - :name: Save - - Saves a completed proof with the name :token:`ident`, which - overrides any name provided by the :cmd:`Theorem` command or - its variants. - -.. cmd:: Defined {? @ident } - - Similar to :cmd:`Qed` and :cmd:`Save`, except the proof is made *transparent*, which means - that its content can be explicitly used for type checking and that it can be - unfolded in conversion tactics (see :ref:`performingcomputations`, - :cmd:`Opaque`, :cmd:`Transparent`). If :token:`ident` is specified, - the proof is defined with the given name, which overrides any name - provided by the :cmd:`Theorem` command or its variants. - -.. cmd:: Admitted - - This command is available in interactive editing mode to give up - the current proof and declare the initial goal as an axiom. - -.. cmd:: Abort {? {| All | @ident } } - - Cancels the current proof development, switching back to - the previous proof development, or to the |Coq| toplevel if no other - proof was being edited. - - :n:`@ident` - Aborts editing the proof named :n:`@ident` for use when you have - nested proofs. See also :flag:`Nested Proofs Allowed`. - - :n:`All` - Aborts all current proofs. - - .. exn:: No focused proof (No proof-editing in progress). - :undocumented: - -.. cmd:: Proof @term - :name: Proof `term` - - This command applies in proof editing mode. It is equivalent to - :n:`exact @term. Qed.` - That is, you have to give the full proof in one gulp, as a - proof term (see Section :ref:`applyingtheorems`). - - .. warning:: - - Use of this command is discouraged. In particular, it - doesn't work in Proof General because it must - immediately follow the command that opened proof mode, but - Proof General inserts :cmd:`Unset` :flag:`Silent` before it (see - `Proof General issue #498 - <https://github.com/ProofGeneral/PG/issues/498>`_). - -.. cmd:: Proof - - Is a no-op which is useful to delimit the sequence of tactic commands - which start a proof, after a :cmd:`Theorem` command. It is a good practice to - use :cmd:`Proof` as an opening parenthesis, closed in the script with a - closing :cmd:`Qed`. - - .. seealso:: :cmd:`Proof with` - -.. cmd:: Proof using @section_var_expr {? with @ltac_expr } - - .. insertprodn section_var_expr starred_ident_ref - - .. prodn:: - section_var_expr ::= {* @starred_ident_ref } - | {? - } @section_var_expr50 - section_var_expr50 ::= @section_var_expr0 - @section_var_expr0 - | @section_var_expr0 + @section_var_expr0 - | @section_var_expr0 - section_var_expr0 ::= @starred_ident_ref - | ( @section_var_expr ) {? * } - starred_ident_ref ::= @ident {? * } - | Type {? * } - | All - - Opens proof editing mode, declaring the set of - section variables (see :ref:`gallina-assumptions`) used by the proof. - At :cmd:`Qed` time, the - system verifies that the set of section variables used in - the proof is a subset of the declared one. - - The set of declared variables is closed under type dependency. For - example, if ``T`` is a variable and ``a`` is a variable of type - ``T``, then the commands ``Proof using a`` and ``Proof using T a`` - are equivalent. - - The set of declared variables always includes the variables used by - the statement. In other words ``Proof using e`` is equivalent to - ``Proof using Type + e`` for any declaration expression ``e``. - - :n:`- @section_var_expr50` - Use all section variables except those specified by :n:`@section_var_expr50` - - :n:`@section_var_expr0 + @section_var_expr0` - Use section variables from the union of both collections. - See :ref:`nameaset` to see how to form a named collection. - - :n:`@section_var_expr0 - @section_var_expr0` - Use section variables which are in the first collection but not in the - second one. - - :n:`{? * }` - Use the transitive closure of the specified collection. - - :n:`Type` - Use only section variables occurring in the statement. Specifying :n:`*` - uses the forward transitive closure of all the section variables occurring - in the statement. For example, if the variable ``H`` has type ``p < 5`` then - ``H`` is in ``p*`` since ``p`` occurs in the type of ``H``. - - :n:`All` - Use all section variables. - - .. seealso:: :ref:`tactics-implicit-automation` - -Proof using options -``````````````````` - -The following options modify the behavior of ``Proof using``. - - -.. opt:: Default Proof Using "@section_var_expr" - :name: Default Proof Using - - Use :n:`@section_var_expr` as the default ``Proof using`` value. E.g. ``Set Default - Proof Using "a b"`` will complete all ``Proof`` commands not followed by a - ``using`` part with ``using a b``. - - -.. flag:: Suggest Proof Using - - When :cmd:`Qed` is performed, suggest a ``using`` annotation if the user did not - provide one. - -.. _`nameaset`: - -Name a set of section hypotheses for ``Proof using`` -```````````````````````````````````````````````````` - -.. cmd:: Collection @ident := @section_var_expr - - This can be used to name a set of section - hypotheses, with the purpose of making ``Proof using`` annotations more - compact. - - .. example:: - - Define the collection named ``Some`` containing ``x``, ``y`` and ``z``:: - - Collection Some := x y z. - - Define the collection named ``Fewer`` containing only ``x`` and ``y``:: - - Collection Fewer := Some - z - - Define the collection named ``Many`` containing the set union or set - difference of ``Fewer`` and ``Some``:: - - Collection Many := Fewer + Some - Collection Many := Fewer - Some - - Define the collection named ``Many`` containing the set difference of - ``Fewer`` and the unnamed collection ``x y``:: - - Collection Many := Fewer - (x y) - - - -.. cmd:: Existential @natural {? : @type } := @term - - This command instantiates an existential variable. :token:`natural` is an index in - the list of uninstantiated existential variables displayed by :cmd:`Show Existentials`. - - This command is intended to be used to instantiate existential - variables when the proof is completed but some uninstantiated - existential variables remain. To instantiate existential variables - during proof edition, you should use the tactic :tacn:`instantiate`. - -.. cmd:: Grab Existential Variables - - This command can be run when a proof has no more goal to be solved but - has remaining uninstantiated existential variables. It takes every - uninstantiated existential variable and turns it into a goal. - -Proof modes -``````````` - -When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`, -|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes -shipped in the standard |Coq| installation, and furthermore some plugins define -their own proof modes. The default proof mode used when opening a proof can -be changed using the following option. - -.. opt:: Default Proof Mode @string - - Select the proof mode to use when starting a proof. Depending on the proof - mode, various syntactic constructs are allowed when writing an interactive - proof. All proof modes support vernacular commands; the proof mode determines - which tactic language and set of tactic definitions are available. The - possible option values are: - - `"Classic"` - Activates the |Ltac| language and the tactics with the syntax documented - in this manual. - Some tactics are not available until the associated plugin is loaded, - such as `SSR` or `micromega`. - This proof mode is set when the :term:`prelude` is loaded. - - `"Noedit"` - No tactic - language is activated at all. This is the default when the :term:`prelude` - is not loaded, e.g. through the `-noinit` option for `coqc`. - - `"Ltac2"` - Activates the Ltac2 language and the Ltac2-specific variants of the documented - tactics. - This value is only available after :cmd:`Requiring <Require>` Ltac2. - :cmd:`Importing <Import>` Ltac2 sets this mode. - - Some external plugins also define their own proof mode, which can be - activated with this command. - -Navigation in the proof tree --------------------------------- - -.. cmd:: Undo {? {? To } @natural } - - Cancels the effect of the last :token:`natural` commands or tactics. - The :n:`To @natural` form goes back to the specified state number. - If :token:`natural` is not specified, the command goes back one command or tactic. - -.. cmd:: Restart - - Restores the proof editing process to the original goal. - - .. exn:: No focused proof to restart. - :undocumented: - -.. cmd:: Focus {? @natural } - - Focuses the attention on the first subgoal to prove or, if :token:`natural` is - specified, the :token:`natural`\-th. The - printing of the other subgoals is suspended until the focused subgoal - is solved or unfocused. - - .. deprecated:: 8.8 - - Prefer the use of bullets or focusing brackets with a goal selector (see below). - -.. cmd:: Unfocus - - This command restores to focus the goal that were suspended by the - last :cmd:`Focus` command. - - .. deprecated:: 8.8 - -.. cmd:: Unfocused - - Succeeds if the proof is fully unfocused, fails if there are some - goals out of focus. - -.. _curly-braces: - -.. index:: { - } - -.. todo: :name: "{"; "}" doesn't work, nor does :name: left curly bracket; right curly bracket, - hence the verbose names - -.. tacn:: {? {| @natural | [ @ident ] } : } %{ - %} - - .. todo - See https://github.com/coq/coq/issues/12004 and - https://github.com/coq/coq/issues/12825. - - ``{`` (without a terminating period) focuses on the first - goal. The subproof can only be - unfocused when it has been fully solved (*i.e.*, when there is no - focused goal left). Unfocusing is then handled by ``}`` (again, without a - terminating period). See also an example in the next section. - - Note that when a focused goal is proved a message is displayed - together with a suggestion about the right bullet or ``}`` to unfocus it - or focus the next one. - - :n:`@natural:` - Focuses on the :token:`natural`\-th subgoal to prove. - - :n:`[ @ident ]: %{` - Focuses on the named goal :token:`ident`. - - .. note:: - - Goals are just existential variables and existential variables do not - get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. - You may also wrap this in an Ltac-definition like: - - .. coqtop:: in - - Ltac name_goal name := refine ?[name]. - - .. seealso:: :ref:`existential-variables` - - .. example:: - - This first example uses the Ltac definition above, and the named goals - only serve for documentation. - - .. coqtop:: all - - Goal forall n, n + 0 = n. - Proof. - induction n; [ name_goal base | name_goal step ]. - [base]: { - - .. coqtop:: all - - reflexivity. - - .. coqtop:: in - - } - - .. coqtop:: all - - [step]: { - - .. coqtop:: all - - simpl. - f_equal. - assumption. - } - Qed. - - This can also be a way of focusing on a shelved goal, for instance: - - .. coqtop:: all - - Goal exists n : nat, n = n. - eexists ?[x]. - reflexivity. - [x]: exact 0. - Qed. - - .. exn:: This proof is focused, but cannot be unfocused this way. - - You are trying to use ``}`` but the current subproof has not been fully solved. - - .. exn:: No such goal (@natural). - :undocumented: - - .. exn:: No such goal (@ident). - :undocumented: - - .. exn:: Brackets do not support multi-goal selectors. - - Brackets are used to focus on a single goal given either by its position - or by its name if it has one. - - .. seealso:: The error messages for bullets below. - -.. _bullets: - -Bullets -``````` - -Alternatively, proofs can be structured with bullets instead of ``{`` and ``}``. The -use of a bullet ``b`` for the first time focuses on the first goal ``g``, the -same bullet cannot be used again until the proof of ``g`` is completed, -then it is mandatory to focus the next goal with ``b``. The consequence is -that ``g`` and all goals present when ``g`` was focused are focused with the -same bullet ``b``. See the example below. - -Different bullets can be used to nest levels. The scope of bullet does -not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further -nesting levels provided they are delimited by these. Bullets are made of -repeated ``-``, ``+`` or ``*`` symbols: - -.. prodn:: bullet ::= {| {+ - } | {+ + } | {+ * } } - -Note again that when a focused goal is proved a message is displayed -together with a suggestion about the right bullet or ``}`` to unfocus it -or focus the next one. - -.. note:: - - In Proof General (``Emacs`` interface to |Coq|), you must use - bullets with the priority ordering shown above to have a correct - indentation. For example ``-`` must be the outer bullet and ``**`` the inner - one in the example below. - -The following example script illustrates all these features: - -.. example:: - - .. coqtop:: all - - Goal (((True /\ True) /\ True) /\ True) /\ True. - Proof. - split. - - split. - + split. - ** { split. - - trivial. - - trivial. - } - ** trivial. - + trivial. - - assert True. - { trivial. } - assumption. - Qed. - -.. exn:: Wrong bullet @bullet__1: Current bullet @bullet__2 is not finished. - - Before using bullet :n:`@bullet__1` again, you should first finish proving - the current focused goal. - Note that :n:`@bullet__1` and :n:`@bullet__2` may be the same. - -.. exn:: Wrong bullet @bullet__1: Bullet @bullet__2 is mandatory here. - - You must put :n:`@bullet__2` to focus on the next goal. No other bullet is - allowed here. - -.. exn:: No such goal. Focus next goal with bullet @bullet. - - You tried to apply a tactic but no goals were under focus. - Using :n:`@bullet` is mandatory here. - -.. FIXME: the :noindex: below works around a Sphinx issue. - (https://github.com/sphinx-doc/sphinx/issues/4979) - It should be removed once that issue is fixed. - -.. exn:: No such goal. Try unfocusing with %}. - :noindex: - - You just finished a goal focused by ``{``, you must unfocus it with ``}``. - -Mandatory Bullets -````````````````` - -Using :opt:`Default Goal Selector` with the ``!`` selector forces -tactic scripts to keep focus to exactly one goal (e.g. using bullets) -or use explicit goal selectors. - -Set Bullet Behavior -``````````````````` -.. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } - :name: Bullet Behavior - - This option controls the bullet behavior and can take two possible values: - - - "None": this makes bullets inactive. - - "Strict Subproofs": this makes bullets active (this is the default behavior). - -.. _requestinginformation: - -Requesting information ----------------------- - - -.. cmd:: Show {? {| @ident | @natural } } - - Displays the current goals. - - :n:`@natural` - Display only the :token:`natural`\-th subgoal. - - :n:`@ident` - Displays the named goal :token:`ident`. This is useful in - particular to display a shelved goal but only works if the - corresponding existential variable has been named by the user - (see :ref:`existential-variables`) as in the following example. - - .. example:: - - .. coqtop:: all abort - - Goal exists n, n = 0. - eexists ?[n]. - Show n. - - .. exn:: No focused proof. - :undocumented: - - .. exn:: No such goal. - :undocumented: - -.. cmd:: Show Proof {? Diffs {? removed } } - - Displays the proof term generated by the tactics - that have been applied so far. If the proof is incomplete, the term - will contain holes, which correspond to subterms which are still to be - constructed. Each hole is an existential variable, which appears as a - question mark followed by an identifier. - - Specifying “Diffs” highlights the difference between the - current and previous proof step. By default, the command shows the - output once with additions highlighted. Including “removed” shows - the output twice: once showing removals and once showing additions. - It does not examine the :opt:`Diffs` option. See :ref:`showing_proof_diffs`. - -.. cmd:: Show Conjectures - - Prints the names of all the - theorems that are currently being proved. As it is possible to start - proving a previous lemma during the proof of a theorem, there may - be multiple names. - -.. cmd:: Show Intro - - If the current goal begins by at least one product, - prints the name of the first product as it would be - generated by an anonymous :tacn:`intro`. The aim of this command is to ease - the writing of more robust scripts. For example, with an appropriate - Proof General macro, it is possible to transform any anonymous :tacn:`intro` - into a qualified one such as ``intro y13``. In the case of a non-product - goal, it prints nothing. - -.. cmd:: Show Intros - - Similar to the previous command. - Simulates the naming process of :tacn:`intros`. - -.. cmd:: Show Existentials - - Displays all open goals / existential variables in the current proof - along with the type and the context of each variable. - -.. cmd:: Show Match @qualid - - Displays a template of the Gallina :token:`match<term_match>` - construct with a branch for each constructor of the type - :token:`qualid`. This is used internally by - `company-coq <https://github.com/cpitclaudel/company-coq>`_. - - .. example:: - - .. coqtop:: all - - Show Match nat. - - .. exn:: Unknown inductive type. - :undocumented: - -.. cmd:: Show Universes - - Displays the set of all universe constraints and - its normalized form at the current stage of the proof, useful for - debugging universe inconsistencies. - -.. cmd:: Show Goal @natural at @natural - - Available in coqtop. Displays a goal at a - proof state using the goal ID number and the proof state ID number. - It is primarily for use by tools such as Prooftree that need to fetch - goal history in this way. Prooftree is a tool for visualizing a proof - as a tree that runs in Proof General. - -.. cmd:: Guarded - - Some tactics (e.g. :tacn:`refine`) allow to build proofs using - fixpoint or co-fixpoint constructions. Due to the incremental nature - of interactive proof construction, the check of the termination (or - guardedness) of the recursive calls in the fixpoint or cofixpoint - constructions is postponed to the time of the completion of the proof. - - The command :cmd:`Guarded` allows checking if the guard condition for - fixpoint and cofixpoint is violated at some time of the construction - of the proof without having to wait the completion of the proof. - -.. _showing_diffs: - -Showing differences between proof steps ---------------------------------------- - -|Coq| can automatically highlight the differences between successive proof steps -and between values in some error messages. |Coq| can also highlight differences -in the proof term. -For example, the following screenshots of |CoqIDE| and coqtop show the application -of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. -The conclusion is entirely in pale green because although it’s changed, no tokens were added -to it. The second screenshot uses the "removed" option, so it shows the conclusion a -second time with the old text, with deletions marked in red. Also, since the hypotheses are -new, no line of old text is shown for them. - -.. comment screenshot produced with: - Inductive ev : nat -> Prop := - | ev_0 : ev 0 - | ev_SS : forall n : nat, ev n -> ev (S (S n)). - - Fixpoint double (n:nat) := - match n with - | O => O - | S n' => S (S (double n')) - end. - - Goal forall n, ev n -> exists k, n = double k. - intros n E. - -.. - - .. image:: ../_static/diffs-coqide-on.png - :alt: |CoqIDE| with Set Diffs on - -.. - - .. image:: ../_static/diffs-coqide-removed.png - :alt: |CoqIDE| with Set Diffs removed - -.. - - .. image:: ../_static/diffs-coqtop-on3.png - :alt: coqtop with Set Diffs on - -This image shows an error message with diff highlighting in |CoqIDE|: - -.. - - .. image:: ../_static/diffs-error-message.png - :alt: |CoqIDE| error message with diffs - -How to enable diffs -``````````````````` - -.. opt:: Diffs {| "on" | "off" | "removed" } - :name: Diffs - - The “on” setting highlights added tokens in green, while the “removed” setting - additionally reprints items with removed tokens in red. Unchanged tokens in - modified items are shown with pale green or red. Diffs in error messages - use red and green for the compared values; they appear regardless of the setting. - (Colors are user-configurable.) - -For coqtop, showing diffs can be enabled when starting coqtop with the -``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option -within |Coq|. You will need to provide the ``-color on|auto`` command-line option when -you start coqtop in either case. - -Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment -variable. See section :ref:`customization-by-environment-variables`. Diffs -use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``. - -In |CoqIDE|, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` -command in |CoqIDE|. You can change the background colors shown for diffs from the -``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``, -``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags. This panel also -lets you control other attributes of the highlights, such as the foreground -color, bold, italic, underline and strikeout. - -Proof General can also display |Coq|-generated proof diffs automatically. -Please see the PG documentation section -"`Showing Proof Diffs" <https://proofgeneral.github.io/doc/master/userman/Coq-Proof-General#Showing-Proof-Diffs>`_) -for details. - -How diffs are calculated -```````````````````````` - -Diffs are calculated as follows: - -1. Select the old proof state to compare to, which is the proof state before - the last tactic that changed the proof. Changes that only affect the view - of the proof, such as ``all: swap 1 2``, are ignored. - -2. For each goal in the new proof state, determine what old goal to compare - it to—the one it is derived from or is the same as. Match the hypotheses by - name (order is ignored), handling compacted items specially. - -3. For each hypothesis and conclusion (the “items”) in each goal, pass - them as strings to the lexer to break them into tokens. Then apply the - Myers diff algorithm :cite:`Myers` on the tokens and add appropriate highlighting. - -Notes: - -* Aside from the highlights, output for the "on" option should be identical - to the undiffed output. -* Goals completed in the last proof step will not be shown even with the - "removed" setting. - -.. comment The following screenshots show diffs working with multiple goals and with compacted - hypotheses. In the first one, notice that the goal ``P 1`` is not highlighted at - all after the split because it has not changed. - - .. todo: Use this script and remove the screenshots when COQ_COLORS - works for coqtop in sphinx - .. coqtop:: none - - Set Diffs "on". - Parameter P : nat -> Prop. - Goal P 1 /\ P 2 /\ P 3. - - .. coqtop:: out - - split. - - .. coqtop:: all abort - - 2: split. - - .. - - .. coqtop:: none - - Set Diffs "on". - Goal forall n m : nat, n + m = m + n. - Set Diffs "on". - - .. coqtop:: out - - intros n. - - .. coqtop:: all abort - - intros m. - -This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal -with 2 goals. Notice that the goal ``P 1`` is not highlighted at all after -the split because it has not changed. - -.. - - .. image:: ../_static/diffs-coqide-multigoal.png - :alt: coqide with Set Diffs on with multiple goals - -Diffs may appear like this after applying a :tacn:`intro` tactic that results -in a compacted hypotheses: - -.. - - .. image:: ../_static/diffs-coqide-compacted.png - :alt: coqide with Set Diffs on with compacted hypotheses - -.. _showing_proof_diffs: - -"Show Proof" differences -```````````````````````` - -To show differences in the proof term: - -- In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command. - -- In |CoqIDE|, position the cursor on or just after a tactic to compare the proof term - after the tactic with the proof term before the tactic, then select - `View / Show Proof` from the menu or enter the associated key binding. - Differences will be shown applying the current `Show Diffs` setting - from the `View` menu. If the current setting is `Don't show diffs`, diffs - will not be shown. - - Output with the "added and removed" option looks like this: - - .. - - .. image:: ../_static/diffs-show-proof.png - :alt: coqide with Set Diffs on with compacted hypotheses - -Controlling the effect of proof editing commands ------------------------------------------------- - - -.. opt:: Hyps Limit @natural - :name: Hyps Limit - - This option controls the maximum number of hypotheses displayed in goals - after the application of a tactic. All the hypotheses remain usable - in the proof development. - When unset, it goes back to the default mode which is to print all - available hypotheses. - - -.. flag:: Nested Proofs Allowed - - When turned on (it is off by default), this flag enables support for nested - proofs: a new assertion command can be inserted before the current proof is - finished, in which case |Coq| will temporarily switch to the proof of this - *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed` - or :cmd:`Defined`), its statement will be made available (as if it had been - proved before starting the previous proof) and |Coq| will switch back to the - proof of the previous assertion. - -.. flag:: Printing Goal Names - - When turned on, the name of the goal is printed in interactive - proof mode, which can be useful in cases of cross references - between goals. - -Controlling memory usage ------------------------- - -.. cmd:: Print Debug GC - - Prints heap usage statistics, which are values from the `stat` type of the `Gc` module - described - `here <https://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#TYPEstat>`_ - in the |OCaml| documentation. - The `live_words`, `heap_words` and `top_heap_words` values give the basic information. - Words are 8 bytes or 4 bytes, respectively, for 64- and 32-bit executables. - -When experiencing high memory usage the following commands can be used -to force |Coq| to optimize some of its internal data structures. - -.. cmd:: Optimize Proof - - Shrink the data structure used to represent the current proof. - - -.. cmd:: Optimize Heap - - Perform a heap compaction. This is generally an expensive operation. - See: `|OCaml| Gc.compact <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ - There is also an analogous tactic :tacn:`optimize_heap`. - -Memory usage parameters can be set through the :ref:`OCAMLRUNPARAM <OCAMLRUNPARAM>` -environment variable. + <meta http-equiv="refresh" content="0;URL=../proofs/writing-proofs/proof-mode.html"> diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index cdbae8ade1..07c2d268c6 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -13,12 +13,12 @@ Introduction This chapter describes a set of tactics known as |SSR| originally designed to provide support for the so-called *small scale reflection* proof methodology. Despite the original purpose this set of tactic is -of general interest and is available in |Coq| starting from version 8.7. +of general interest and is available in Coq starting from version 8.7. |SSR| was developed independently of the tactics described in Chapter :ref:`tactics`. Indeed the scope of the tactics part of |SSR| largely overlaps with the standard set of tactics. Eventually the overlap will -be reduced in future releases of |Coq|. +be reduced in future releases of Coq. Proofs written in |SSR| typically look quite different from the ones written using only tactics as per Chapter :ref:`tactics`. We try to @@ -112,7 +112,7 @@ Compatibility issues ~~~~~~~~~~~~~~~~~~~~ Requiring the above modules creates an environment which is mostly -compatible with the rest of |Coq|, up to a few discrepancies: +compatible with the rest of Coq, up to a few discrepancies: + New keywords (``is``) might clash with variable, constant, tactic or @@ -124,11 +124,11 @@ compatible with the rest of |Coq|, up to a few discrepancies: + Identifiers with both leading and trailing ``_``, such as ``_x_``, are reserved by |SSR| and cannot appear in scripts. + The extensions to the :tacn:`rewrite` tactic are partly incompatible with those - available in current versions of |Coq|; in particular: ``rewrite .. in + available in current versions of Coq; in particular: ``rewrite .. in (type of k)`` or ``rewrite .. in *`` or any other variant of :tacn:`rewrite` will not work, and the |SSR| syntax and semantics for occurrence selection and rule chaining is different. Use an explicit rewrite direction - (``rewrite <- …`` or ``rewrite -> …``) to access the |Coq| rewrite tactic. + (``rewrite <- …`` or ``rewrite -> …``) to access the Coq rewrite tactic. + New symbols (``//``, ``/=``, ``//=``) might clash with adjacent existing symbols. This can be avoided by inserting white spaces. @@ -158,34 +158,34 @@ compatible with the rest of |Coq|, up to a few discrepancies: generalized form, turn off the |SSR| Boolean ``if`` notation using the command: ``Close Scope boolean_if_scope``. + The following flags can be unset to make |SSR| more compatible with - parts of |Coq|: + parts of Coq: .. flag:: SsrRewrite Controls whether the incompatible rewrite syntax is enabled (the default). - Disabling the flag makes the syntax compatible with other parts of |Coq|. + Disabling the flag makes the syntax compatible with other parts of Coq. .. flag:: SsrIdents Controls whether tactics can refer to |SSR|-generated variables that are in the form _xxx_. Scripts with explicit references to such variables are fragile; they are prone to failure if the proof is later modified or - if the details of variable name generation change in future releases of |Coq|. + if the details of variable name generation change in future releases of Coq. The default is on, which gives an error message when the user tries to create such identifiers. Disabling the flag generates a warning instead, - increasing compatibility with other parts of |Coq|. + increasing compatibility with other parts of Coq. -|Gallina| extensions +Gallina extensions -------------------- Small-scale reflection makes an extensive use of the programming -subset of |Gallina|, |Coq|’s logical specification language. This subset +subset of Gallina, Coq’s logical specification language. This subset is quite suited to the description of functions on representations, because it closely follows the well-established design of the ML programming language. The |SSR| extension provides three additions -to |Gallina|, for pattern assignment, pattern testing, and polymorphism; -these mitigate minor but annoying discrepancies between |Gallina| and +to Gallina, for pattern assignment, pattern testing, and polymorphism; +these mitigate minor but annoying discrepancies between Gallina and ML. @@ -199,7 +199,7 @@ irrefutable pattern matching, that is, destructuring assignment: term += let: @pattern := @term in @term Note the colon ``:`` after the ``let`` keyword, which avoids any ambiguity -with a function definition or |Coq|’s basic destructuring let. The let: +with a function definition or Coq’s basic destructuring let. The let: construct differs from the latter in that @@ -237,7 +237,7 @@ construct differs from the latter in that The ``let:`` construct is just (more legible) notation for the primitive -|Gallina| expression :n:`match @term with @pattern => @term end`. +Gallina expression :n:`match @term with @pattern => @term end`. The |SSR| destructuring assignment supports all the dependent match annotations; the full syntax is @@ -294,10 +294,10 @@ example, the null and all list function(al)s can be defined as follows: The pattern conditional also provides a notation for destructuring assignment with a refutable pattern, adapted to the pure functional -setting of |Gallina|, which lacks a ``Match_Failure`` exception. +setting of Gallina, which lacks a ``Match_Failure`` exception. Like ``let:`` above, the ``if…is`` construct is just (more legible) notation -for the primitive |Gallina| expression +for the primitive Gallina expression :n:`match @term with @pattern => @term | _ => @term end`. Similarly, it will always be displayed as the expansion of this form @@ -355,15 +355,15 @@ Note that :token:`pattern` eventually binds variables in the third Parametric polymorphism ~~~~~~~~~~~~~~~~~~~~~~~ -Unlike ML, polymorphism in core |Gallina| is explicit: the type +Unlike ML, polymorphism in core Gallina is explicit: the type parameters of polymorphic functions must be declared explicitly, and -supplied at each point of use. However, |Coq| provides two features to +supplied at each point of use. However, Coq provides two features to suppress redundant parameters: + Sections are used to provide (possibly implicit) parameters for a set of definitions. -+ Implicit arguments declarations are used to tell |Coq| to use type ++ Implicit arguments declarations are used to tell Coq to use type inference to deduce some parameters from the context at each point of call. @@ -392,11 +392,11 @@ expressions such as Definition all_null (s : list T) := all (@null T) s. Unfortunately, such higher-order expressions are quite frequent in -representation functions, especially those which use |Coq|'s +representation functions, especially those which use Coq's ``Structures`` to emulate Haskell typeclasses. -Therefore, |SSR| provides a variant of |Coq|’s implicit argument -declaration, which causes |Coq| to fill in some implicit parameters at +Therefore, |SSR| provides a variant of Coq’s implicit argument +declaration, which causes Coq to fill in some implicit parameters at each point of use, e.g., the above definition can be written: .. example:: @@ -432,7 +432,7 @@ The syntax of the new declaration is As these prenex implicit arguments are ubiquitous and have often large display strings, it is strongly recommended to change the default - display settings of |Coq| so that they are not printed (except after + display settings of Coq so that they are not printed (except after a ``Set Printing All`` command). All |SSR| library files thus start with the incantation @@ -957,7 +957,7 @@ context. This is essential in the context of an interactive development environment (IDE), because it facilitates navigating the proof, allowing to instantly "jump back" to the point at which a questionable assumption was added, and to find relevant assumptions by -browsing the pruned context. While novice or casual |Coq| users may find +browsing the pruned context. While novice or casual Coq users may find the automatic name selection feature convenient, the usage of such a feature severely undermines the readability and maintainability of proof scripts, much like automatic variable declaration in programming @@ -973,7 +973,7 @@ the foundation of the |SSR| proof language. Bookkeeping ~~~~~~~~~~~ -During the course of a proof |Coq| always present the user with a +During the course of a proof Coq always present the user with a *sequent* whose general form is:: ci : Ti @@ -1015,7 +1015,7 @@ are *ordered*, but *unnamed*: the display names of variables may change at any time because of α-conversion. Similarly, basic deductive steps such as apply can only operate on the -goal because the |Gallina| terms that control their action (e.g., the +goal because the Gallina terms that control their action (e.g., the type of the lemma used by ``apply``) only provide unnamed bound variables. [#2]_ Since the proof script can only refer directly to the context, it must constantly shift declarations from the goal to the context and @@ -1083,7 +1083,7 @@ simultaneously renames ``m`` and ``le_m_n`` into ``p`` and ``le_n_p``, respectively, by first turning them into unnamed variables, then turning these variables back into constants and facts. -Furthermore, |SSR| redefines the basic |Coq| tactics ``case``, ``elim``, +Furthermore, |SSR| redefines the basic Coq tactics ``case``, ``elim``, and ``apply`` so that they can take better advantage of ``:`` and ``=>``. In there |SSR| variants, these tactic operate on the first variable or @@ -1421,7 +1421,7 @@ Therefore this tactic changes any goal ``G`` into forall n n0 : nat, n = n0 -> G. -where the name ``n0`` is picked by the |Coq| display function, and assuming +where the name ``n0`` is picked by the Coq display function, and assuming ``n`` appeared only in ``G``. Finally, note that a discharge operation generalizes defined constants @@ -1647,7 +1647,10 @@ Notations can be used to name tactics, for example Notation "'myop'" := (ltac:(my ltac code)) : ssripat_scope. lets one write just ``/myop`` in the intro pattern. Note the scope -annotation: views are interpreted opening the ``ssripat`` scope. +annotation: views are interpreted opening the ``ssripat`` scope. We +provide the following ltac views: ``/[dup]`` to duplicate the top of +the stack, ``/[swap]`` to swap the two first elements and ``/[apply]`` +to apply the top of the stack to the next. Intro patterns `````````````` @@ -1927,7 +1930,7 @@ When the top assumption of a goal has an inductive type, two specific operations are possible: the case analysis performed by the :tacn:`case` tactic, and the application of an induction principle, performed by the :tacn:`elim` tactic. When this top assumption has an inductive type, which -is moreover an instance of a type family, |Coq| may need help from the +is moreover an instance of a type family, Coq may need help from the user to specify which occurrences of the parameters of the type should be substituted. @@ -2055,7 +2058,7 @@ Control flow Indentation and bullets ~~~~~~~~~~~~~~~~~~~~~~~ -A linear development of |Coq| scripts gives little information on the +A linear development of Coq scripts gives little information on the structure of the proof. In addition, replaying a proof after some changes in the statement to be proved will usually not display information to distinguish between the various branches of case @@ -3391,7 +3394,7 @@ rewrite operations prescribed by the rules on the current goal. Indeed rule ``eqab`` is the first to apply among the ones gathered in the tuple passed to the rewrite tactic. This multirule - ``(eqab, eqac)`` is actually a |Coq| term and we can name it with a + ``(eqab, eqac)`` is actually a Coq term and we can name it with a definition: .. coqtop:: all @@ -3529,11 +3532,11 @@ Anyway this tactic is *not* equivalent to lemma that was used, while the latter requires you prove the quantified form. -When |SSR| rewrite fails on standard |Coq| licit rewrite +When |SSR| rewrite fails on standard Coq licit rewrite ```````````````````````````````````````````````````````` In a few cases, the |SSR| rewrite tactic fails rewriting some -redexes which standard |Coq| successfully rewrites. There are two main +redexes which standard Coq successfully rewrites. There are two main cases: @@ -3550,7 +3553,7 @@ cases: Lemma fubar (x : unit) : (let u := x in u) = tt. -+ The standard rewrite tactic provided by |Coq| uses a different algorithm ++ The standard rewrite tactic provided by Coq uses a different algorithm to find instances of the rewrite rule. .. example:: @@ -3953,7 +3956,7 @@ together with “term tagging” operations. The first one uses auxiliary definitions to introduce a provably equal copy of any term t. However this copy is (on purpose) *not -convertible* to t in the |Coq| system [#8]_. The job is done by the +convertible* to t in the Coq system [#8]_. The job is done by the following construction: .. coqdoc:: @@ -4542,7 +4545,7 @@ is a synonym for: elim x using V; clear x; intro y. where ``x`` is a variable in the context, ``y`` a fresh name and ``V`` -any second order lemma; |SSR| relaxes the syntactic restrictions of the |Coq| +any second order lemma; |SSR| relaxes the syntactic restrictions of the Coq ``elim``. The first pattern following ``:`` can be a ``_`` wildcard if the conclusion of the view ``V`` specifies a pattern for its last argument (e.g., if ``V`` is a functional induction lemma generated by the @@ -4590,7 +4593,7 @@ generation (see section :ref:`generation_of_equations_ssr`). elim/last_ind_list E : l=> [| u v]; last first. -User-provided eliminators (potentially generated with |Coq|’s ``Function`` +User-provided eliminators (potentially generated with Coq’s ``Function`` command) can be combined with the type family switches described in section :ref:`type_families_ssr`. Consider an eliminator ``foo_ind`` of type: @@ -4982,8 +4985,8 @@ distinction between logical propositions and boolean values. On the one hand, logical propositions are objects of *sort* ``Prop`` which is the carrier of intuitionistic reasoning. Logical connectives in ``Prop`` are *types*, which give precise information on the structure -of their proofs; this information is automatically exploited by |Coq| -tactics. For example, |Coq| knows that a proof of ``A \/ B`` is +of their proofs; this information is automatically exploited by Coq +tactics. For example, Coq knows that a proof of ``A \/ B`` is either a proof of ``A`` or a proof of ``B``. The tactics ``left`` and ``right`` change the goal ``A \/ B`` to ``A`` and ``B``, respectively; dually, the tactic ``case`` reduces the goal ``A \/ B => G`` to two @@ -5042,7 +5045,7 @@ mechanism: Coercion is_true (b : bool) := b = true. -This allows any boolean formula ``b`` to be used in a context where |Coq| +This allows any boolean formula ``b`` to be used in a context where Coq would expect a proposition, e.g., after ``Lemma … :``. It is then interpreted as ``(is_true b)``, i.e., the proposition ``b = true``. Coercions are elided by the pretty-printer, so they are essentially transparent @@ -5077,9 +5080,9 @@ proposition ``b1 /\ b2`` hides two coercions. The conjunction of Expressing logical equivalences through this family of inductive types makes possible to take benefit from *rewritable equations* associated -to the case analysis of |Coq|’s inductive types. +to the case analysis of Coq’s inductive types. -Since the equivalence predicate is defined in |Coq| as: +Since the equivalence predicate is defined in Coq as: .. coqdoc:: @@ -5573,7 +5576,7 @@ Natural number .. prodn:: nat_or_ident ::= {| @natural | @ident } -where :token:`ident` is an Ltac variable denoting a standard |Coq| number +where :token:`ident` is an Ltac variable denoting a standard Coq number (should not be the name of a tactic which can be followed by a bracket ``[``, like ``do``, ``have``,…) @@ -5823,6 +5826,6 @@ Settings .. [#8] This is an implementation feature: there is no such obstruction in the metatheory .. [#9] The current state of the proof shall be displayed by the Show - Proof command of |Coq| proof mode. + Proof command of Coq proof mode. .. [#10] A simple proof context entry is a naked identifier (i.e. not between parentheses) designating a context entry that is not a section variable. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fe9a31e220..26a56005c1 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -167,11 +167,11 @@ The :n:`eqn:` construct in various tactics uses :n:`@naming_intropattern`. Use these elementary patterns to specify a name: * :n:`@ident` — use the specified name -* :n:`?` — let |Coq| choose a name +* :n:`?` — let Coq choose a name * :n:`?@ident` — generate a name that begins with :n:`@ident` * :n:`_` — discard the matched part (unless it is required for another hypothesis) -* if a disjunction pattern omits a name, such as :g:`[|H2]`, |Coq| will choose a name +* if a disjunction pattern omits a name, such as :g:`[|H2]`, Coq will choose a name **Splitting patterns** @@ -268,7 +268,7 @@ These patterns can be used when the hypothesis is an equality: For :n:`intros @intropattern_list`, controls how to handle a conjunctive pattern that doesn't give enough simple patterns to match - all the arguments in the constructor. If set (the default), |Coq| generates + all the arguments in the constructor. If set (the default), Coq generates additional names to match the number of arguments. Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more similar to |SSR|'s intro patterns. @@ -843,7 +843,7 @@ Applying theorems .. flag:: Universal Lemma Under Conjunction - This flag, which preserves compatibility with versions of |Coq| prior to + This flag, which preserves compatibility with versions of Coq prior to 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply … in`). .. tacn:: apply @term in @ident @@ -1293,7 +1293,7 @@ Managing the local context .. tacv:: set @term {? in @goal_occurrences } This behaves as :n:`set (@ident := @term) {? in @goal_occurrences }` - but :token:`ident` is generated by |Coq|. + but :token:`ident` is generated by Coq. .. tacv:: eset (@ident {* @binder } := @term) {? in @goal_occurrences } eset @term {? in @goal_occurrences } @@ -1338,7 +1338,7 @@ Managing the local context .. tacv:: pose @term This behaves as :n:`pose (@ident := @term)` but :token:`ident` is - generated by |Coq|. + generated by Coq. .. tacv:: epose (@ident {* @binder } := @term) epose @term @@ -1400,7 +1400,7 @@ Controlling the proof flow .. tacv:: assert @type This behaves as :n:`assert (@ident : @type)` but :n:`@ident` is - generated by |Coq|. + generated by Coq. .. tacv:: assert @type by @tactic @@ -1480,7 +1480,7 @@ Controlling the proof flow .. tacv:: enough @type This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of - the hypothesis generated by |Coq|. + the hypothesis generated by Coq. .. tacv:: enough @type as @simple_intropattern @@ -1605,7 +1605,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. must have given the name explicitly (see :ref:`Existential-Variables`). .. note:: When you are referring to hypotheses which you did not name - explicitly, be aware that |Coq| may make a different decision on how to + explicitly, be aware that Coq may make a different decision on how to name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors. @@ -1759,7 +1759,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) between :token:`term` and the value that it takes in each of the possible cases. The name of the equation is specified by :token:`naming_intropattern` (see :tacn:`intros`), - in particular ``?`` can be used to let |Coq| generate a fresh name. + in particular ``?`` can be used to let Coq generate a fresh name. .. tacv:: destruct @term with @bindings @@ -2353,7 +2353,7 @@ and an explanation of the underlying technique. ``inversion`` generally behaves in a slightly more expectable way than ``inversion`` (no artificial duplication of some hypotheses referring to other hypotheses). To take benefit of these improvements, it is enough to use - ``inversion ... as []``, letting the names being finally chosen by |Coq|. + ``inversion ... as []``, letting the names being finally chosen by Coq. .. example:: @@ -2663,1760 +2663,6 @@ and an explanation of the underlying technique. simultaneously proved are respectively :g:`forall binder ... binder, type` The identifiers :n:`@ident` are the names of the coinduction hypotheses. -.. _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: - - -.. _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` - -.. _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. - Checking properties of terms ---------------------------- @@ -4647,189 +2893,6 @@ using the ``Require Import`` command. Use :tacn:`classical_right` to prove the right part of the disjunction with the assumption that the negation of left part holds. -.. _tactics-automating: - -Automating ------------- - - -.. 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. - -Non-logical tactics ------------------------- - - -.. 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. - Delaying solving unification constraints ---------------------------------------- @@ -4849,14 +2912,14 @@ Proof maintenance *Experimental.* Many tactics, such as :tacn:`intros`, can automatically generate names, such as "H0" or "H1" for a new hypothesis introduced from a goal. Subsequent proof steps -may explicitly refer to these names. However, future versions of |Coq| may not assign +may explicitly refer to these names. However, future versions of Coq may not assign names exactly the same way, which could cause the proof to fail because the new names don't match the explicit references in the proof. The following "Mangle Names" settings let users find all the places where proofs rely on automatically generated names, which can then be named explicitly to avoid any incompatibility. These -settings cause |Coq| to generate different names, producing errors for +settings cause Coq to generate different names, producing errors for references to automatically generated names. .. flag:: Mangle Names @@ -4878,7 +2941,7 @@ Performance-oriented tactic variants For advanced usage. Similar to :tacn:`change` :n:`@term`, but as an optimization, it skips checking that :n:`@term` is convertible to the goal. - Recall that the |Coq| kernel typechecks proofs again when they are concluded to + Recall that the Coq kernel typechecks proofs again when they are concluded to ensure safety. Hence, using :tacn:`change` checks convertibility twice overall, while :tacn:`change_no_check` can produce ill-typed terms, but checks convertibility only once. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 301559d69d..86d1d25745 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -133,7 +133,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). .. prodn:: search_item ::= {? {| head | hyp | concl | headhyp | headconcl } : } @string {? % @scope_key } - | {? {| head | hyp | concl | headhyp | headconcl } : } @one_term + | {? {| head | hyp | concl | headhyp | headconcl } : } @one_pattern | is : @logical_kind Searched objects can be filtered by patterns, by the constants they @@ -141,9 +141,9 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). names. The location of the pattern or constant within a term - :n:`@one_term` + :n:`@one_pattern` Search for objects whose type contains a subterm matching the - pattern :n:`@one_term`. Holes of the pattern are indicated by + pattern :n:`@one_pattern`. Holes of the pattern are indicated by `_` or :n:`?@ident`. If the same :n:`?@ident` occurs more than once in the pattern, all occurrences in the subterm must be identical. See :ref:`this example <search-pattern>`. @@ -312,7 +312,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). Search is:Instance [ Reflexive | Symmetric ]. -.. cmd:: SearchHead @one_term {? {| inside | outside } {+ @qualid } } +.. cmd:: SearchHead @one_pattern {? {| inside | outside } {+ @qualid } } .. deprecated:: 8.12 @@ -320,8 +320,8 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context that have the - form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_term` - matches a subterm of `C` in head position. For example, a :n:`@one_term` of `f _ b` + form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_pattern` + matches a subterm of `C` in head position. For example, a :n:`@one_pattern` of `f _ b` matches `f a b`, which is a subterm of `C` in head position when `C` is `f a b c`. See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. @@ -337,12 +337,12 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). SearchHead le. SearchHead (@eq bool). -.. cmd:: SearchPattern @one_term {? {| inside | outside } {+ @qualid } } +.. cmd:: SearchPattern @one_pattern {? {| inside | outside } {+ @qualid } } Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context ending with :n:`{? forall {* @binder }, } {* P__i -> } C` that match the pattern - :n:`@one_term`. + :n:`@one_pattern`. See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. @@ -362,11 +362,11 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). SearchPattern (?X1 + _ = _ + ?X1). -.. cmd:: SearchRewrite @one_term {? {| inside | outside } {+ @qualid } } +.. cmd:: SearchRewrite @one_pattern {? {| inside | outside } {+ @qualid } } Displays the name and type of all hypotheses of the selected goal (if any) and theorems of the current context that have the form - :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_term` + :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_pattern` matches either `LHS` or `RHS`. See :cmd:`Search` for an explanation of the `inside`/`outside` clauses. @@ -433,7 +433,7 @@ Requests to the environment reference ::= @qualid | @string {? % @scope_key } - Displays the full name of objects from |Coq|'s various qualified namespaces such as terms, + Displays the full name of objects from Coq's various qualified namespaces such as terms, modules and Ltac, thereby showing the module they are defined in. It also displays notation definitions. :n:`@qualid` @@ -491,7 +491,7 @@ Printing flags .. flag:: Fast Name Printing - When turned on, |Coq| uses an asymptotically faster algorithm for the + When turned on, Coq uses an asymptotically faster algorithm for the generation of unambiguous names of bound variables while printing terms. While faster, it is also less clever and results in a typically less elegant display, e.g. it will generate more names rather than reusing certain names @@ -504,12 +504,12 @@ Printing flags Loading files ----------------- -|Coq| offers the possibility of loading different parts of a whole +Coq offers the possibility of loading different parts of a whole development stored in separate files. Their contents will be loaded as if they were entered from the keyboard. This means that the loaded -files are text files containing sequences of commands for |Coq|’s -toplevel. This kind of file is called a *script* for |Coq|. The standard -(and default) extension of |Coq|’s script files is .v. +files are text files containing sequences of commands for Coq’s +toplevel. This kind of file is called a *script* for Coq. The standard +(and default) extension of Coq’s script files is .v. .. cmd:: Load {? Verbose } {| @string | @ident } @@ -521,7 +521,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard If :n:`@string` is specified, it must specify a complete filename. `~` and .. abbreviations are - allowed as well as shell variables. If no extension is specified, |Coq| + allowed as well as shell variables. If no extension is specified, Coq will use the default extension ``.v``. Files loaded this way can't leave proofs open, nor can :cmd:`Load` @@ -531,7 +531,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard :cmd:`Require` loads `.vo` files that were previously compiled from `.v` files. - :n:`Verbose` displays the |Coq| output for each command and tactic + :n:`Verbose` displays the Coq output for each command and tactic in the loaded file, as if the commands and tactics were entered interactively. .. exn:: Can’t find file @ident on loadpath. @@ -556,14 +556,14 @@ file is a particular case of a module called a *library file*. .. cmd:: Require {? {| Import | Export } } {+ @qualid } :name: Require; Require Import; Require Export - Loads compiled modules into the |Coq| environment. For each :n:`@qualid`, which has the form + Loads compiled modules into the Coq environment. For each :n:`@qualid`, which has the form :n:`{* @ident__prefix . } @ident`, the command searches for the logical name represented by the :n:`@ident__prefix`\s and loads the compiled file :n:`@ident.vo` from the associated filesystem directory. The process is applied recursively to all the loaded files; if they contain :cmd:`Require` commands, those commands are executed as well. - The compiled files must have been compiled with the same version of |Coq|. + The compiled files must have been compiled with the same version of Coq. The compiled files are neither replayed nor rechecked. * :n:`Import` - additionally does an :cmd:`Import` on the loaded module, making components defined @@ -606,15 +606,15 @@ file is a particular case of a module called a *library file*. The command tried to load library file :n:`@ident`.vo that depends on some specific version of library :n:`@qualid` which is not the - one already loaded in the current |Coq| session. Probably :n:`@ident.v` was + one already loaded in the current Coq session. Probably :n:`@ident.v` was not properly recompiled with the last version of the file containing module :token:`qualid`. .. exn:: Bad magic number. The file :n:`@ident.vo` was found but either it is not a - |Coq| compiled module, or it was compiled with an incompatible - version of |Coq|. + Coq compiled module, or it was compiled with an incompatible + version of Coq. .. exn:: The file @ident.vo contains library @qualid__1 and not library @qualid__2. @@ -633,15 +633,16 @@ file is a particular case of a module called a *library file*. .. cmd:: Print Libraries This command displays the list of library files loaded in the - current |Coq| session. + current Coq session. .. cmd:: Declare ML Module {+ @string } - This commands dynamically loads |OCaml| compiled code from + This commands dynamically loads OCaml compiled code from a :n:`.mllib` file. It is used to load plugins dynamically. The - files must be accessible in the current |OCaml| loadpath (see the - command :cmd:`Add ML Path`). The :n:`.mllib` suffix may be omitted. + files must be accessible in the current OCaml loadpath (see + :ref:`command line option <command-line-options>` :n:`-I` and command :cmd:`Add ML Path`). The + :n:`.mllib` suffix may be omitted. This command is reserved for plugin developers, who should provide a .v file containing the command. Users of the plugins will then generally @@ -656,7 +657,7 @@ file is a particular case of a module called a *library file*. .. cmd:: Print ML Modules - This prints the name of all |OCaml| modules loaded with :cmd:`Declare ML Module`. + This prints the name of all OCaml modules loaded with :cmd:`Declare ML Module`. To know from where these module were loaded, the user should use the command :cmd:`Locate File`. @@ -666,7 +667,7 @@ file is a particular case of a module called a *library file*. Loadpath ------------ -Loadpaths are preferably managed using |Coq| command line options (see +Loadpaths are preferably managed using Coq command line options (see Section :ref:`libraries-and-filesystem`) but there remain vernacular commands to manage them for practical purposes. Such commands are only meant to be issued in the toplevel, and using them in source files is discouraged. @@ -703,33 +704,35 @@ the toplevel, and using them in source files is discouraged. This command is equivalent to the command line option :n:`-R @string @dirpath`. It adds the physical directory string and all its - subdirectories to the current |Coq| loadpath. + subdirectories to the current Coq loadpath. .. cmd:: Remove LoadPath @string - This command removes the path :n:`@string` from the current |Coq| loadpath. + This command removes the path :n:`@string` from the current Coq loadpath. .. cmd:: Print LoadPath {? @dirpath } - This command displays the current |Coq| loadpath. If :n:`@dirpath` is specified, + This command displays the current Coq loadpath. If :n:`@dirpath` is specified, displays only the paths that extend that prefix. .. cmd:: Add ML Path @string - This command adds the path :n:`@string` to the current |OCaml| - loadpath (cf. :cmd:`Declare ML Module`). - + Equivalent to the :ref:`command line option <command-line-options>` + :n:`-I @string`. Adds the path :n:`@string` to the current OCaml + loadpath (cf. :cmd:`Declare ML Module`). It is for + convenience, such as for use in an interactive session, and it + is not exported to compiled files. For separation of concerns with + respect to the relocability of files, we recommend using + :n:`-I @string`. .. cmd:: Print ML Path - This command displays the current |OCaml| loadpath. This - command makes sense only under the bytecode version of ``coqtop``, i.e. - using option ``-byte`` - (cf. :cmd:`Declare ML Module`). - + Displays the current OCaml loadpath, as provided by + the :ref:`command line option <command-line-options>` :n:`-I @string` or by the command :cmd:`Add + ML Path` `@string` (cf. :cmd:`Declare ML Module`). .. _backtracking_subsection: @@ -789,25 +792,25 @@ Quitting and debugging .. cmd:: Quit - Causes |Coq| to exit. Valid only in coqtop. + Causes Coq to exit. Valid only in coqtop. .. cmd:: Drop - This command temporarily enters the |OCaml| toplevel. - It is a debug facility used by |Coq|’s implementers. Valid only in the + This command temporarily enters the OCaml toplevel. + It is a debug facility used by Coq’s implementers. Valid only in the bytecode version of coqtop. - The |OCaml| command: + The OCaml command: :: #use "include";; adds the right loadpaths and loads some toplevel printers for all - abstract types of |Coq|- section_path, identifiers, terms, judgments, …. + abstract types of Coq- section_path, identifiers, terms, judgments, …. You can also use the file base_include instead, that loads only the pretty-printers for section_paths and identifiers. You can return back - to |Coq| with the command: + to Coq with the command: :: @@ -815,9 +818,9 @@ Quitting and debugging .. warning:: - #. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`, + #. It only works with the bytecode version of Coq (i.e. `coqtop.byte`, see Section `interactive-use`). - #. You must have compiled |Coq| from the source package and set the + #. You must have compiled Coq from the source package and set the environment variable COQTOP to the root of your copy of the sources (see Section `customization-by-environment-variables`). @@ -961,7 +964,7 @@ Controlling the reduction strategies and the conversion algorithm ---------------------------------------------------------------------- -|Coq| provides reduction strategies that the tactics can invoke and two +Coq provides reduction strategies that the tactics can invoke and two different algorithms to check the convertibility of types. The first conversion algorithm lazily compares applicative terms while the other is a brute-force but efficient algorithm that first normalizes the @@ -985,16 +988,11 @@ described first. constants in the :n:`@reference` sequence in tactics using δ-conversion (unfolding a constant is replacing it by its definition). - :cmd:`Opaque` has also an effect on the conversion algorithm of |Coq|, telling - it to delay the unfolding of a constant as much as possible when |Coq| + :cmd:`Opaque` has also an effect on the conversion algorithm of Coq, telling + it to delay the unfolding of a constant as much as possible when Coq has to check the conversion (see Section :ref:`conversion-rules`) of two distinct applied constants. - .. seealso:: - - Sections :ref:`performingcomputations`, :ref:`tactics-automating`, - :ref:`proof-editing-mode` - .. cmd:: Transparent {+ @reference } This command accepts the :attr:`global` attribute. By default, the scope @@ -1015,10 +1013,7 @@ described first. There is no constant named :n:`@qualid` in the environment. - .. seealso:: - - Sections :ref:`performingcomputations`, - :ref:`tactics-automating`, :ref:`proof-editing-mode` +.. seealso:: :ref:`performingcomputations` and :ref:`proof-editing-mode` .. _vernac-strategy: @@ -1230,15 +1225,15 @@ in support libraries of plug-ins. .. _exposing-constants-to-ocaml-libraries: -Exposing constants to |OCaml| libraries +Exposing constants to OCaml libraries ``````````````````````````````````````` .. cmd:: Register @qualid__1 as @qualid__2 - Makes the constant :n:`@qualid__1` accessible to |OCaml| libraries under + Makes the constant :n:`@qualid__1` accessible to OCaml libraries under the name :n:`@qualid__2`. The constant can then be dynamically located - in |OCaml| code by - calling :n:`Coqlib.lib_ref "@qualid__2"`. The |OCaml| code doesn't need + in OCaml code by + calling :n:`Coqlib.lib_ref "@qualid__2"`. The OCaml code doesn't need to know where the constant is defined (what file, module, library, etc.). As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`, @@ -1267,9 +1262,9 @@ Registering primitive operations .. cmd:: Primitive @ident_decl {? : @term } := #@ident - Makes the primitive type or primitive operator :n:`#@ident` defined in |OCaml| - accessible in |Coq| commands and tactics. - For internal use by implementors of |Coq|'s standard library or standard library + Makes the primitive type or primitive operator :n:`#@ident` defined in OCaml + accessible in Coq commands and tactics. + For internal use by implementors of Coq's standard library or standard library replacements. No space is allowed after the `#`. Invalid values give a syntax error. |