diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 48 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 173 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 34 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 49 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 176 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 113 |
6 files changed, 356 insertions, 237 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 46f9826e41..b2b426ada5 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -31,10 +31,10 @@ Syntax The syntax of the tactic language is given below. See Chapter :ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used in these grammar rules. Various already defined entries will be used in this -chapter: entries :token:`natural`, :token:`integer`, :token:`ident`, +chapter: entries :token:`num`, :token:`int`, :token:`ident` :token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic` -represent respectively the natural and integer numbers, the authorized -identificators and qualified names, Coq terms and patterns and all the atomic +represent respectively natural and integer numbers, +identifiers, qualified names, Coq terms, patterns and the atomic tactics described in Chapter :ref:`tactics`. The syntax of :production:`cpattern` is @@ -127,7 +127,7 @@ mode but it can also be used in toplevel definitions as shown below. : gfail [`natural`] [`message_token` ... `message_token`] : fresh [ `component` … `component` ] : context `ident` [`term`] - : eval `redexpr` in `term` + : eval `red_expr` in `term` : type of `term` : constr : `term` : uconstr : `term` @@ -141,10 +141,10 @@ mode but it can also be used in toplevel definitions as shown below. : `atom` atom : `qualid` : () - : `integer` + : `int` : ( `ltac_expr` ) component : `string` | `qualid` - message_token : `string` | `ident` | `integer` + message_token : `string` | `ident` | `int` tacarg : `qualid` : () : ltac : `atom` @@ -159,11 +159,11 @@ mode but it can also be used in toplevel definitions as shown below. match_rule : `cpattern` => `ltac_expr` : context [`ident`] [ `cpattern` ] => `ltac_expr` : _ => `ltac_expr` - test : `integer` = `integer` - : `integer` (< | <= | > | >=) `integer` + test : `int` = `int` + : `int` (< | <= | > | >=) `int` selector : [`ident`] - : `integer` - : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) + : `int` + : (`int` | `int` - `int`), ..., (`int` | `int` - `int`) toplevel_selector : `selector` : all : par @@ -368,7 +368,7 @@ We can check if a tactic made progress with: :name: progress :n:`@ltac_expr` is evaluated to v which must be a tactic value. The tactic value ``v`` - is applied to each focued subgoal independently. If the application of ``v`` + is applied to each focused subgoal independently. If the application of ``v`` to one of the focused subgoal produced subgoals equal to the initial goals (up to syntactical equality), then an error of level 0 is raised. @@ -516,7 +516,9 @@ Coq provides a derived tactic to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr :name: assert_fails - This behaves like :n:`tryif @ltac_expr then fail 0 tac "succeeds" else idtac`. + This behaves like :tacn:`idtac` if :n:`@ltac_expr` fails, and + behaves like :n:`fail 0 @ltac_expr "succeeds"` if :n:`@ltac_expr` + has at least one success. Checking the success ~~~~~~~~~~~~~~~~~~~~ @@ -528,7 +530,7 @@ success: :name: assert_succeeds This behaves like - :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`. + :n:`tryif (assert_fails @ltac_expr) then fail 0 @ltac_expr "fails" else idtac`. Solving ~~~~~~~ @@ -858,8 +860,8 @@ We can carry out pattern matching on terms with: If the evaluation of the right-hand-side of a valid match fails, the next matching subterm is tried. If no further subterm matches, the next clause is tried. Matching subterms are considered top-bottom and from left to - right (with respect to the raw printing obtained by setting option - :flag:`Printing All`). + right (with respect to the raw printing obtained by setting the + :flag:`Printing All` flag). .. example:: @@ -984,9 +986,9 @@ Computing in a constr Evaluation of a term can be performed with: -.. tacn:: eval @redexpr in @term +.. tacn:: eval @red_expr in @term - where :n:`@redexpr` is a reduction tactic among :tacn:`red`, :tacn:`hnf`, + where :n:`@red_expr` is a reduction tactic among :tacn:`red`, :tacn:`hnf`, :tacn:`compute`, :tacn:`simpl`, :tacn:`cbv`, :tacn:`lazy`, :tacn:`unfold`, :tacn:`fold`, :tacn:`pattern`. @@ -1640,7 +1642,7 @@ Interactive debugger .. flag:: Ltac Debug - This option governs the step-by-step debugger that comes with the |Ltac| interpreter. + This flag governs the step-by-step debugger that comes with the |Ltac| interpreter. When the debugger is activated, it stops at every step of the evaluation of the current |Ltac| expression and prints information on what it is doing. @@ -1664,13 +1666,13 @@ following: .. exn:: Debug mode not available in the IDE :undocumented: -A non-interactive mode for the debugger is available via the option: +A non-interactive mode for the debugger is available via the flag: .. flag:: Ltac Batch Debug - This option has the effect of presenting a newline at every prompt, when + This flag has the effect of presenting a newline at every prompt, when the debugger is on. The debug log thus created, which does not require - user input to generate when this option is set, can then be run through + user input to generate when this flag is set, can then be run through external tools such as diff. Profiling |Ltac| tactics @@ -1689,7 +1691,7 @@ performance issue. .. flag:: Ltac Profiling - This option enables and disables the profiler. + This flag enables and disables the profiler. .. cmd:: Show Ltac Profile @@ -1773,7 +1775,7 @@ performance issue. benchmarking purposes. You can also pass the ``-profile-ltac`` command line option to ``coqc``, which -turns the :flag:`Ltac Profiling` option on at the beginning of each document, +turns the :flag:`Ltac Profiling` flag on at the beginning of each document, and performs a :cmd:`Show Ltac Profile` at the end. .. warning:: diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 3036648b08..cfdc70d50e 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -17,16 +17,16 @@ Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: - is error-prone and fragile - has an intricate implementation -Following the need of users that start developing huge projects relying +Following the need of users who are developing huge projects relying critically on Ltac, we believe that we should offer a proper modern language that features at least the following: - at least informal, predictable semantics -- a typing system -- standard programming facilities (i.e. datatypes) +- a type system +- standard programming facilities (e.g., datatypes) This new language, called Ltac2, is described in this chapter. It is still -experimental but we encourage nonetheless users to start testing it, +experimental but we nonetheless encourage users to start testing it, especially wherever an advanced tactic language is needed. The previous implementation of Ltac, described in the previous chapter, will be referred to as Ltac1. @@ -36,9 +36,9 @@ as Ltac1. General design -------------- -There are various alternatives to Ltac1, such that Mtac or Rtac for instance. -While those alternatives can be quite distinct from Ltac1, we designed -Ltac2 to be closest as reasonably possible to Ltac1, while fixing the +There are various alternatives to Ltac1, such as Mtac or Rtac for instance. +While those alternatives can be quite different from Ltac1, we designed +Ltac2 to be as close as reasonably possible to Ltac1, while fixing the aforementioned defects. In particular, Ltac2 is: @@ -47,11 +47,11 @@ In particular, Ltac2 is: * a call-by-value functional language * with effects - * together with Hindley-Milner type system + * together with the Hindley-Milner type system - a language featuring meta-programming facilities for the manipulation of Coq-side terms -- a language featuring notation facilities to help writing palatable scripts +- a language featuring notation facilities to help write palatable scripts We describe more in details each point in the remainder of this document. @@ -77,7 +77,7 @@ 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 computation will be well-typed. This is actually a design choice, motivated -by retro-compatibility with Ltac1. Instead, well-typedness is deferred to +by backward compatibility with Ltac1. Instead, well-typedness is deferred to dynamic checks, allowing many primitive functions to fail whenever they are provided with an ill-typed term. @@ -92,7 +92,7 @@ Type Syntax ~~~~~~~~~~~ At the level of terms, we simply elaborate on Ltac1 syntax, which is quite -close to e.g. the one of OCaml. Types follow the simply-typed syntax of OCaml. +close to OCaml. Types follow the simply-typed syntax of OCaml. The non-terminal :production:`lident` designates identifiers starting with a lowercase. @@ -122,7 +122,7 @@ Built-in types include: Type declarations ~~~~~~~~~~~~~~~~~ -One can define new types by the following commands. +One can define new types with the following commands. .. cmd:: Ltac2 Type {? @ltac2_typeparams } @lident :name: Ltac2 Type @@ -149,7 +149,7 @@ One can define new types by the following commands. Variants are sum types defined by constructors and eliminated by pattern-matching. They can be recursive, but the `rec` flag must be - explicitly set. Pattern-maching must be exhaustive. + explicitly set. Pattern matching must be exhaustive. Records are product types with named fields and eliminated by projection. Likewise they can be recursive if the `rec` flag is set. @@ -158,15 +158,15 @@ One can define new types by the following commands. Open variants are a special kind of variant types whose constructors are not statically defined, but can instead be extended dynamically. A typical example - is the standard `exn` type. Pattern-matching must always include a catch-all - clause. They can be extended by this command. + is the standard `exn` type. Pattern matching on open variants must always include a catch-all + clause. They can be extended with this command. Term Syntax ~~~~~~~~~~~ The syntax of the functional fragment is very close to the one of Ltac1, except that it adds a true pattern-matching feature, as well as a few standard -constructions from ML. +constructs from ML. .. productionlist:: coq ltac2_var : `lident` @@ -179,7 +179,7 @@ constructions from ML. : let `ltac2_var` := `ltac2_term` in `ltac2_term` : let rec `ltac2_var` := `ltac2_term` in `ltac2_term` : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end - : `integer` + : `int` : `string` : `ltac2_term` ; `ltac2_term` : [| `ltac2_term` ; ... ; `ltac2_term` |] @@ -202,7 +202,7 @@ constructions from ML. In practice, there is some additional syntactic sugar that allows e.g. to bind a variable and match on it at the same time, in the usual ML style. -There is a dedicated syntax for list and array literals. +There is dedicated syntax for list and array literals. .. note:: @@ -217,7 +217,7 @@ Ltac Definitions This command defines a new global Ltac2 value. For semantic reasons, the body of the Ltac2 definition must be a syntactical - value, i.e. a function, a constant or a pure constructor recursively applied to + value, that is, a function, a constant or a pure constructor recursively applied to values. If ``rec`` is set, the tactic is expanded into a recursive binding. @@ -247,7 +247,7 @@ if ever we implement native compilation. The expected equations are as follows:: (t any term, V values, C constructor) Note that call-by-value reduction is already a departure from Ltac1 which uses -heuristics to decide when evaluating an expression. For instance, the following +heuristics to decide when to evaluate an expression. For instance, the following expressions do not evaluate the same way in Ltac1. :n:`foo (idtac; let x := 0 in bar)` @@ -255,7 +255,7 @@ expressions do not evaluate the same way in Ltac1. :n:`foo (let x := 0 in bar)` Instead of relying on the :n:`idtac` idiom, we would now require an explicit thunk -not to compute the argument, and :n:`foo` would have e.g. type +to not compute the argument, and :n:`foo` would have e.g. type :n:`(unit -> unit) -> unit`. :n:`foo (fun () => let x := 0 in bar)` @@ -263,19 +263,19 @@ not to compute the argument, and :n:`foo` would have e.g. type Typing ~~~~~~ -Typing is strict and follows Hindley-Milner system. Unlike Ltac1, there +Typing is strict and follows the Hindley-Milner system. Unlike Ltac1, there are no type casts at runtime, and one has to resort to conversion functions. See notations though to make things more palatable. -In this setting, all usual argument-free tactics have type :n:`unit -> unit`, but -one can return as well a value of type :n:`t` thanks to terms of type :n:`unit -> t`, +In this setting, all the usual argument-free tactics have type :n:`unit -> unit`, but +one can return a value of type :n:`t` thanks to terms of type :n:`unit -> t`, or take additional arguments. Effects ~~~~~~~ Effects in Ltac2 are straightforward, except that instead of using the -standard IO monad as the ambient effectful world, Ltac2 is going to use the +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 @@ -288,15 +288,15 @@ Intuitively a thunk of type :n:`unit -> 'a` can do the following: - It can perform non-backtracking IO like printing and setting mutable variables - It can fail in a non-recoverable way -- It can use first-class backtrack. The proper way to figure that is that we - morally have the following isomorphism: +- It can use first-class backtracking. One way to think about this is that + thunks are isomorphic to this type: :n:`(unit -> 'a) ~ (unit -> exn + ('a * (exn -> 'a)))` i.e. thunks can produce a lazy list of results where each tail is waiting for a continuation exception. -- It can access a backtracking proof state, made out amongst other things of +- It can access a backtracking proof state, consisting among other things of the current evar assignation and the list of goals under focus. -We describe more thoroughly the various effects existing in Ltac2 hereafter. +We now describe more thoroughly the various effects in Ltac2. Standard IO +++++++++++ @@ -315,28 +315,28 @@ Fatal errors ++++++++++++ The Ltac2 language provides non-backtracking exceptions, also known as *panics*, -through the following primitive in module `Control`.:: +through the following primitive in module `Control`:: val throw : exn -> 'a Unlike backtracking exceptions from the next section, this kind of error is never caught by backtracking primitives, that is, throwing an exception -destroys the stack. This is materialized by the following equation, where `E` -is an evaluation context.:: +destroys the stack. This is codified by the following equation, where `E` +is an evaluation context:: E[throw e] ≡ throw e (e value) -There is currently no way to catch such an exception and it is a design choice. -There might be at some future point a way to catch it in a brutal way, -destroying all backtrack and return values. +There is currently no way to catch such an exception, which is a deliberate design choice. +Eventually there might be a way to catch it and +destroy all backtrack and return values. -Backtrack -+++++++++ +Backtracking +++++++++++++ In Ltac2, we have the following backtracking primitives, defined in the -`Control` module.:: +`Control` module:: Ltac2 Type 'a result := [ Val ('a) | Err (exn) ]. @@ -344,7 +344,7 @@ In Ltac2, we have the following backtracking primitives, defined in the val plus : (unit -> 'a) -> (exn -> 'a) -> 'a val case : (unit -> 'a) -> ('a * (exn -> 'a)) result -If one sees thunks as lazy lists, then `zero` is the empty list and `plus` is +If one views thunks as lazy lists, then `zero` is the empty list and `plus` is list concatenation, while `case` is pattern-matching. The backtracking is first-class, i.e. one can write @@ -376,8 +376,8 @@ represent several goals, including none. Thus, there is no such thing as *the current goal*. Goals are naturally ordered, though. It is natural to do the same in Ltac2, but we must provide a way to get access -to a given goal. This is the role of the `enter` primitive, that applies a -tactic to each currently focused goal in turn.:: +to a given goal. This is the role of the `enter` primitive, which applies a +tactic to each currently focused goal in turn:: val enter : (unit -> unit) -> unit @@ -427,6 +427,8 @@ In general, quotations can be introduced in terms using the following syntax, wh .. prodn:: ltac2_term += @ident : ( @quotentry ) +.. _ltac2_built-in-quotations: + Built-in quotations +++++++++++++++++++ @@ -439,10 +441,11 @@ The current implementation recognizes the following built-in quotations: holes at runtime (type ``Init.constr`` as well). - ``pattern``, which parses Coq patterns and produces a pattern used for term matching (type ``Init.pattern``). -- ``reference``, which parses either a :n:`@qualid` or :n:`& @ident`. Qualified names +- ``reference``, which parses either a :n:`@qualid` or :n:`&@ident`. Qualified names are globalized at internalization into the corresponding global reference, while ``&id`` is turned into ``Std.VarRef id``. This produces at runtime a - ``Std.reference``. + ``Std.reference``. There shall be no white space between the ampersand + symbol (``&``) and the identifier (:n:`@ident`). The following syntactic sugar is provided for two common cases. @@ -452,9 +455,9 @@ The following syntactic sugar is provided for two common cases. Strict vs. non-strict mode ++++++++++++++++++++++++++ -Depending on the context, quotations producing terms (i.e. ``constr`` or +Depending on the context, quotation-producing terms (i.e. ``constr`` or ``open_constr``) are not internalized in the same way. There are two possible -modes, respectively called the *strict* and the *non-strict* mode. +modes, the *strict* and the *non-strict* mode. - In strict mode, all simple identifiers appearing in a term quotation are required to be resolvable statically. That is, they must be the short name of @@ -467,7 +470,7 @@ modes, respectively called the *strict* and the *non-strict* mode. of the term at runtime will fail if there is no such variable in the dynamic context. -Strict mode is enforced by default, e.g. for all Ltac2 definitions. Non-strict +Strict mode is enforced by default, such as for all Ltac2 definitions. Non-strict mode is only set when evaluating Ltac2 snippets in interactive proof mode. The rationale is that it is cumbersome to explicitly add ``&`` interactively, while it is expected that global tactics enforce more invariants on their code. @@ -490,12 +493,12 @@ for their side-effects. Semantics +++++++++ -Interpretation of a quoted Coq term is done in two phases, internalization and +A quoted Coq term is interpreted in two phases, internalization and evaluation. -- Internalization is part of the static semantics, i.e. it is done at Ltac2 +- Internalization is part of the static semantics, that is, it is done at Ltac2 typing time. -- Evaluation is part of the dynamic semantics, i.e. it is done when +- 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 @@ -560,6 +563,20 @@ for it. - `&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 +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 +current context using the `Ltac2.Constr.pretype` function. + +.. example:: + + The following notation is essentially the identity. + + .. coqtop:: in + + Notation "[ x ]" := ltac2:(let x := Ltac2.Constr.pretype x in exact $x) (only parsing). + Dynamic semantics ***************** @@ -670,9 +687,9 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression at parsing time. Scopes are described using a form of S-expression. .. prodn:: - ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) } + ltac2_scope ::= {| @string | @int | @lident ({+, @ltac2_scope}) } -A few scopes contain antiquotation features. For sake of uniformity, all +A few scopes contain antiquotation features. For the sake of uniformity, all antiquotations are introduced by the syntax :n:`$@lident`. The following scopes are built-in. @@ -713,15 +730,15 @@ The following scopes are built-in. - :n:`self`: - + parses a Ltac2 expression at the current level and return it as is. + + parses a Ltac2 expression at the current level and returns it as is. - :n:`next`: - + parses a Ltac2 expression at the next level and return it as is. + + parses a Ltac2 expression at the next level and returns it as is. -- :n:`tactic(n = @integer)`: +- :n:`tactic(n = @int)`: - + parses a Ltac2 expression at the provided level :n:`n` and return it as is. + + parses a Ltac2 expression at the provided level :n:`n` and returns it as is. - :n:`thunk(@ltac2_scope)`: @@ -747,7 +764,7 @@ The following scopes are built-in. out of the parsed values in the same order. As an optimization, all subscopes of the form :n:`STRING` are left out of the returned tuple, instead of returning a useless unit value. It is forbidden for the various - subscopes to refer to the global entry using self or next. + subscopes to refer to the global entry using :n:`self` or :n:`next`. A few other specific scopes exist to handle Ltac1-like syntax, but their use is discouraged and they are thus not documented. @@ -758,9 +775,9 @@ planned. Notations ~~~~~~~~~ -The Ltac2 parser can be extended by syntactic notations. +The Ltac2 parser can be extended with syntactic notations. -.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term +.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @int} := @ltac2_term :name: Ltac2 Notation A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded @@ -793,10 +810,10 @@ Abbreviations .. cmdv:: Ltac2 Notation @lident := @ltac2_term - This command introduces a special kind of notations, called abbreviations, + This command introduces a special kind of notation, called an abbreviation, that is designed so that it does not add any parsing rules. It is similar in spirit to Coq abbreviations, insofar as its main purpose is to give an - absolute name to a piece of pure syntax, which can be transparently referred + absolute name to a piece of pure syntax, which can be transparently referred to by this name as if it were a proper definition. The abbreviation can then be manipulated just as a normal Ltac2 definition, @@ -850,8 +867,11 @@ a Ltac1 expression, and semantics of this quotation is the evaluation of the corresponding code for its side effects. In particular, it cannot return values, and the quotation has type :n:`unit`. +.. productionlist:: coq + ltac2_term : ltac1 : ( `ltac_expr` ) + Ltac1 **cannot** implicitly access variables from the Ltac2 scope, but this can -be done via an explicit annotation to the :n:`ltac1` quotation. +be done with an explicit annotation on the :n:`ltac1` quotation. .. productionlist:: coq ltac2_term : ltac1 : ( `ident` ... `ident` |- `ltac_expr` ) @@ -887,10 +907,19 @@ Ltac2 from Ltac1 Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation instead. -Note that the tactic expression is evaluated eagerly, if one wants to use it as -an argument to a Ltac1 function, she has to resort to the good old -:n:`idtac; ltac2:(foo)` trick. For instance, the code below will fail immediately -and won't print anything. +.. productionlist:: coq + ltac_expr : ltac2 : ( `ltac2_term` ) + : ltac2 : ( `ident` ... `ident` |- `ltac2_term` ) + +The typing rules are dual, that is, the optional identifiers are bound +with type `Ltac2.Ltac1.t` in the Ltac2 expression, which is expected to have +type unit. The value returned by this quotation is an Ltac1 function with the +same arity as the number of bound variables. + +Note that when no variables are bound, the inner tactic expression is evaluated +eagerly, if one wants to use it as an argument to a Ltac1 function, one has to +resort to the good old :n:`idtac; ltac2:(foo)` trick. For instance, the code +below will fail immediately and won't print anything. .. coqtop:: in @@ -899,11 +928,17 @@ and won't print anything. .. coqtop:: all - Ltac mytac tac := idtac "wow"; tac. + Ltac mytac tac := idtac "I am being evaluated"; tac. Goal True. Proof. + (* Doesn't print anything *) Fail mytac ltac2:(fail). + (* Prints and fails *) + Fail mytac ltac:(idtac; ltac2:(fail)). + +In any case, the value returned by the fully applied quotation is an +unspecified dummy Ltac1 closure and should not be further used. Transition from Ltac1 --------------------- @@ -923,8 +958,8 @@ Due to conflicts, a few syntactic rules have changed. - The dispatch tactical :n:`tac; [foo|bar]` is now written :n:`tac > [foo|bar]`. - Levels of a few operators have been revised. Some tacticals now parse as if - they were a normal function, i.e. one has to put parentheses around the - argument when it is complex, e.g an abstraction. List of affected tacticals: + they were normal functions. Parentheses are now required around complex + arguments, such as abstractions. The tacticals affected are: :n:`try`, :n:`repeat`, :n:`do`, :n:`once`, :n:`progress`, :n:`time`, :n:`abstract`. - :n:`idtac` is no more. Either use :n:`()` if you expect nothing to happen, :n:`(fun () => ())` if you want a thunk (see next section), or use printing @@ -1010,4 +1045,4 @@ Exception catching Ltac2 features a proper exception-catching mechanism. For this reason, the Ltac1 mechanism relying on `fail` taking integers, and tacticals decreasing it, has been removed. Now exceptions are preserved by all tacticals, and it is -your duty to catch them and reraise them depending on your use. +your duty to catch them and re-raise them as needed. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 03b30d5d97..6884b6e998 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -535,16 +535,20 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Proof + .. cmdv:: Show Proof {? Diffs {? removed } } :name: Show Proof - It displays the proof term generated by the tactics - that have been applied. If the proof is not completed, this term - contain holes, which correspond to the sub-terms which are still to be - constructed. These holes appear as a question mark indexed by an - integer, and applied to the list of variables in the context, since it - may depend on them. The types obtained by abstracting away the context - from the type of each placeholder are also printed. + 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. + + Experimental: 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_diffs`. .. cmdv:: Show Conjectures :name: Show Conjectures @@ -574,9 +578,8 @@ Requesting information .. cmdv:: Show Existentials :name: Show Existentials - It displays the set of all uninstantiated - existential variables in the current proof tree, along with the type - and the context of each variable. + Displays all open goals / existential variables in the current proof + along with the type and the context of each variable. .. cmdv:: Show Match @ident @@ -627,8 +630,11 @@ Showing differences between proof steps --------------------------------------- -Coq can automatically highlight the differences between successive proof steps and between -values in some error messages. +Coq can automatically highlight the differences between successive proof steps +and between values in some error messages. Also, as an experimental feature, +Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof` +command, but only, for now, when using coqtop and Proof General. + 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 @@ -798,7 +804,7 @@ Controlling the effect of proof editing commands .. flag:: Nested Proofs Allowed - When turned on (it is off by default), this option enables support for nested + 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` diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index ed980bd4de..853ddfd6dc 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -514,7 +514,7 @@ is a valid tactic expression. The pose tactic is also improved for the local definition of higher order terms. Local definitions of functions can use the same syntax as global ones. -For example, the tactic :tacn:`pose <pose (ssreflect)>` supoprts parameters: +For example, the tactic :tacn:`pose <pose (ssreflect)>` supports parameters: .. example:: @@ -684,7 +684,7 @@ conditions: + If this head is a projection of a canonical structure, then canonical structure equations are used for the matching. + If the head of term is *not* a constant, the subterm should have the - same structure (λ abstraction,let…in structure …). + same structure (λ abstraction, let…in structure …). + If the head of :token:`term` is a hole, the subterm should have at least as many arguments as :token:`term`. @@ -1151,7 +1151,7 @@ is basically equivalent to move: a H1 H2; tactic => a H1 H2. -with two differences: the in tactical will preserve the body of a ifa +with two differences: the in tactical will preserve the body of an if a is a defined constant, and if the ``*`` is omitted it will use a temporary abbreviation to hide the statement of the goal from ``tactic``. @@ -1513,7 +1513,7 @@ In a goal like the following:: ============= m < 5 + n -The tactic ``abstract: abs n`` first generalizes the goal with respect ton +The tactic :g:`abstract: abs n` first generalizes the goal with respect to :g:`n` (that is not visible to the abstract constant abs) and then assigns abs. The resulting goal is:: @@ -1706,7 +1706,7 @@ Intro patterns execution of tactic should thus generate exactly m subgoals, unless the ``[…]`` :token:`i_pattern` comes after an initial ``//`` or ``//=`` :token:`s_item` that closes some of the goals produced by ``tactic``, in - which case exactly m subgoals should remain after thes- item, or we have + which case exactly m subgoals should remain after the :token:`s_item`, or we have the trivial branching :token:`i_pattern` [], which always does nothing, regardless of the number of remaining subgoals. ``[`` :token:`i_item` * ``| … |`` :token:`i_item` * ``]`` @@ -2240,8 +2240,8 @@ then the tactic tactic ; last k [ tactic1 |…| tacticm ] || tacticn. -where natural denotes the integer k as above, applies tactic1 to the n -−k + 1-th goal, … tacticm to the n −k + 2 − m-th goal and tactic n +where natural denotes the integer :math:`k` as above, applies tactic1 to the +:math:`n−k+1`\-th goal, … tacticm to the :math:`n−k+2`\-th goal and tacticn to the others. .. example:: @@ -2631,7 +2631,7 @@ The :token:`i_item` and :token:`s_item` can be used to interpret the asserted hypothesis with views (see section :ref:`views_and_reflection_ssr`) or simplify the resulting goals. -The ``have`` tactic also supports a ``suff`` modifier which allows for +The :tacn:`have` tactic also supports a ``suff`` modifier which allows for asserting that a given statement implies the current goal without copying the goal itself. @@ -2651,7 +2651,7 @@ compatible with the presence of a list of binders. Generating let in context entries with have ``````````````````````````````````````````` -Since |SSR| 1.5 the ``have`` tactic supports a “transparent” modifier +Since |SSR| 1.5 the :tacn:`have` tactic supports a “transparent” modifier to generate let in context entries: the ``@`` symbol in front of the context entry name. @@ -2670,7 +2670,7 @@ context entry name. Lemma test n m (H : m + 1 < n) : True. have @i : 'I_n by apply: (Sub m); omega. -Note that the sub-term produced by ``omega`` is in general huge and +Note that the subterm produced by :tacn:`omega` is in general huge and uninteresting, and hence one may want to hide it. For this purpose the ``[: name ]`` intro pattern and the tactic ``abstract`` (see :ref:`abstract_ssr`) are provided. @@ -2764,7 +2764,7 @@ typeclass inference. .. flag:: SsrHave NoTCResolution - This option restores the behavior of |SSR| 1.4 and below (never resolve typeclasses). + This flag restores the behavior of |SSR| 1.4 and below (never resolve typeclasses). Variants: the suff and wlog tactics ``````````````````````````````````` @@ -2782,7 +2782,7 @@ The ``have`` and ``suff`` tactics are equivalent and have the same syntax but: -+ the order of the generated subgoals is inversed ++ the order of the generated subgoals is inverted + the optional clear item is still performed in the *second* branch. This means that the tactic: @@ -3756,8 +3756,11 @@ involves the following steps: the corresponding intro pattern :n:`@i_pattern__i` in each goal. 4. Then :tacn:`under` checks that the first n subgoals - are (quantified) equalities or double implications between a - term and an evar (e.g. ``m - m = ?F2 m`` in the running example). + are (quantified) Leibniz equalities, double implications or + registered relations (w.r.t. Class ``RewriteRelation``) between a + term and an evar, e.g. ``m - m = ?F2 m`` in the running example. + (This support for setoid-like relations is enabled as soon as we do + both ``Require Import ssreflect.`` and ``Require Setoid.``) 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. @@ -3769,7 +3772,10 @@ involves the following steps: by using a regular :tacn:`rewrite` tactic. 7. Interactive editing of the first n goals has to be signalled by - using the :tacn:`over` tactic or rewrite rule (see below). + using the :tacn:`over` tactic or rewrite rule (see below), which + requires that the underlying relation is reflexive. (The running + example deals with Leibniz equality, but ``PreOrder`` relations are + also supported, for example.) 8. Finally, a post-processing step is performed in the main goal to keep the name(s) for the bound variables chosen by the user in @@ -3795,6 +3801,10 @@ displayed as ``'Under[ … ]``): This is a variant of :tacn:`over` in order to close ``'Under[ … ]`` goals, relying on the ``over`` rewrite rule. +Note that a rewrite rule ``UnderE`` is available as well, if one wants +to "unprotect" the evar, without closing the goal automatically (e.g., +to instantiate it manually with another rule than reflexivity). + .. _under_one_liner: One-liner mode @@ -4061,6 +4071,7 @@ which the function is supplied: :name: congr This tactic: + + checks that the goal is a Leibniz equality; + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. @@ -4208,7 +4219,7 @@ in the second column. ``ident`` in all the occurrences of ``term2`` * - ``term1 as ident in term2`` - ``term 1`` - - in all the subterms identified by ``ident` + - in all the subterms identified by ``ident`` in all the occurrences of ``term2[term 1 /ident]`` The rewrite tactic supports two more patterns obtained prefixing the @@ -4583,7 +4594,7 @@ The ``elim/`` tactic distinguishes two cases: passed to the eliminator as the last argument (``x`` in ``foo_ind``) and ``en−1 … e1`` are used as patterns to select in the goal the occurrences that will be bound by the predicate ``P``, thus it must be possible to unify - the sub-term of the goal matched by ``en−1`` with ``pm`` , the one matched + the subterm of the goal matched by ``en−1`` with ``pm`` , the one matched by ``en−2`` with ``pm−1`` and so on. :regular eliminator: in all the other cases. Here it must be possible to unify the term matched by ``en`` with ``pm`` , the one matched by @@ -5013,7 +5024,7 @@ mechanism: Coercion is_true (b : bool) := b = true. 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 +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 to the user. @@ -5451,7 +5462,7 @@ equivalences are indeed taken into account, otherwise only single name of an open module. This command returns the list of lemmas: + whose *conclusion* contains a subterm matching the optional first - pattern. A - reverses the test, producing the list of lemmas whose + pattern. A ``-`` reverses the test, producing the list of lemmas whose conclusion does not contain any subterm matching the pattern; + whose name contains the given string. A ``-`` prefix reverses the test, producing the list of lemmas whose name does not contain the string. A diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fa6d62ffa2..62d4aa704f 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -157,10 +157,10 @@ 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:`?@ident` - generate a name that begins with :n:`@ident` -* :n:`_` - discard the matched part (unless it is required for another +* :n:`@ident` — use the specified name +* :n:`?` — let Coq choose a name +* :n:`?@ident` — generate a name that begins with :n:`@ident` +* :n:`_` — discard the matched part (unless it is required for another hypothesis) * if a disjunction pattern omits a name, such as :g:`[|H2]`, Coq will choose a name @@ -186,7 +186,7 @@ use the :tacn:`split` tactic to replace the current goal with subgoals :g:`A` an For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A`, or :tacn:`right` to replace the current goal with :g:`B`. -* :n:`( {+, @simple_intropattern}` ) - matches +* :n:`( {+, @simple_intropattern}` ) — matches a product over an inductive type with a :ref:`single constructor <intropattern_cons_note>`. If the number of patterns @@ -196,7 +196,7 @@ For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A` If the number of patterns equals the number of constructor arguments plus the number of :n:`let-ins`, the patterns are applied to the arguments and :n:`let-in` variables. -* :n:`( {+& @simple_intropattern} )` - matches a right-hand nested term that consists +* :n:`( {+& @simple_intropattern} )` — matches a right-hand nested term that consists of one or more nested binary inductive types such as :g:`a1 OP1 a2 OP2 ...` (where the :g:`OPn` are right-associative). (If the :g:`OPn` are left-associative, additional parentheses will be needed to make the @@ -207,15 +207,15 @@ For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A` :ref:`single constructor with two parameters <intropattern_cons_note>`. :ref:`Example <intropattern_ampersand_ex>` -* :n:`[ {+| @intropattern_list} ]` - splits an inductive type that has +* :n:`[ {+| @intropattern_list} ]` — splits an inductive type that has :ref:`multiple constructors <intropattern_cons_note>` such as :n:`A \/ B` into multiple subgoals. The number of :token:`intropattern_list` must be the same as the number of constructors for the matched part. -* :n:`[ {+ @intropattern} ]` - splits an inductive type that has a +* :n:`[ {+ @intropattern} ]` — splits an inductive type that has a :ref:`single constructor with multiple parameters <intropattern_cons_note>` such as :n:`A /\ B` into multiple hypotheses. Use :n:`[H1 [H2 H3]]` to match :g:`A /\ B /\ C`. -* :n:`[]` - splits an inductive type: If the inductive +* :n:`[]` — splits an inductive type: If the inductive type has multiple constructors, such as :n:`A \/ B`, create one subgoal for each constructor. If the inductive type has a single constructor with multiple parameters, such as :n:`A /\ B`, split it into multiple hypotheses. @@ -224,14 +224,14 @@ For a goal :g:`A \/ B`, use :tacn:`left` to replace the current goal with :g:`A` These patterns can be used when the hypothesis is an equality: -* :n:`->` - replaces the right-hand side of the hypothesis with the left-hand +* :n:`->` — replaces the right-hand side of the hypothesis with the left-hand side of the hypothesis in the conclusion of the goal; the hypothesis is cleared; if the left-hand side of the hypothesis is a variable, it is substituted everywhere in the context and the variable is removed. :ref:`Example <intropattern_rarrow_ex>` -* :n:`<-` - similar to :n:`->`, but replaces the left-hand side of the hypothesis +* :n:`<-` — similar to :n:`->`, but replaces the left-hand side of the hypothesis with the right-hand side of the hypothesis. -* :n:`[= {*, @intropattern} ]` - If the product is over an equality type, +* :n:`[= {*, @intropattern} ]` — If the product is over an equality type, applies either :tacn:`injection` or :tacn:`discriminate`. If :tacn:`injection` is applicable, the intropattern is used on the hypotheses generated by :tacn:`injection`. If the @@ -241,16 +241,16 @@ These patterns can be used when the hypothesis is an equality: **Other patterns** -* :n:`*` - introduces one or more quantified variables from the result +* :n:`*` — introduces one or more quantified variables from the result until there are no more quantified variables. :ref:`Example <intropattern_star_ex>` -* :n:`**` - introduces one or more quantified variables or hypotheses from the result until there are +* :n:`**` — introduces one or more quantified variables or hypotheses from the result until there are no more quantified variables or implications (:g:`->`). :g:`intros **` is equivalent to :g:`intros`. :ref:`Example <intropattern_2stars_ex>` -* :n:`@simple_intropattern_closed {* % @term}` - first applies each of the terms +* :n:`@simple_intropattern_closed {* % @term}` — first applies each of the terms with the :tacn:`apply ... in` tactic on the hypothesis to be introduced, then it uses :n:`@simple_intropattern_closed`. :ref:`Example <intropattern_injection_ex>` @@ -261,7 +261,7 @@ These patterns can be used when the hypothesis is an equality: conjunctive pattern that doesn't give enough simple patterns to match all the arguments in the constructor. If set (the default), |Coq| generates additional names to match the number of arguments. - Unsetting the option will put the additional hypotheses in the goal instead, behavior that is more + Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more similar to |SSR|'s intro patterns. .. deprecated:: 8.10 @@ -477,7 +477,7 @@ that occurrences have to be selected in the hypotheses named :token:`ident`. If no numbers are given for hypothesis :token:`ident`, then all the occurrences of :token:`term` in the hypothesis are selected. If numbers are given, they refer to occurrences of :token:`term` when the term is printed -using option :flag:`Printing All`, counting from left to right. In particular, +using the :flag:`Printing All` flag, counting from left to right. In particular, occurrences of :token:`term` in implicit arguments (see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are counted. @@ -804,11 +804,11 @@ Applying theorems component of the tuple matches the goal, it excludes components whose statement would result in applying an universal lemma of the form ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by - setting the following option: + setting the following flag: .. flag:: Universal Lemma Under Conjunction - This option, 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 @@ -1409,7 +1409,7 @@ Controlling the proof flow While the different variants of :tacn:`assert` expect that no existential variables are generated by the tactic, :tacn:`eassert` removes this constraint. - This allows not to specify the asserted statement completeley before starting + This lets you avoid specifying the asserted statement completely before starting to prove it. .. tacv:: pose proof @term {? as @simple_intropattern} @@ -1527,7 +1527,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term` but it generalizes only over the specified occurrences of :n:`@term` (counting from left to right on the - expression printed using option :flag:`Printing All`). + expression printed using the :flag:`Printing All` flag). .. tacv:: generalize @term as @ident @@ -1555,8 +1555,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. :name: instantiate The instantiate tactic refines (see :tacn:`refine`) an existential variable - :n:`@ident` with the term :n:`@term`. It is equivalent to only [ident]: - :n:`refine @term` (preferred alternative). + :n:`@ident` with the term :n:`@term`. It is equivalent to + :n:`only [ident]: refine @term` (preferred alternative). .. note:: To be able to refer to an existential variable by name, the user must have given the name explicitly (see :ref:`Existential-Variables`). @@ -2008,7 +2008,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) .. coqtop:: reset all - Lemma le_minus : forall n:nat, n < 1 -> n = 0. + Lemma lt_1_r : forall n:nat, n < 1 -> n = 0. intros n H ; induction H. Here we did not get any information on the indexes to help fulfill @@ -2020,7 +2020,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) .. coqtop:: reset all Require Import Coq.Program.Equality. - Lemma le_minus : forall n:nat, n < 1 -> n = 0. + Lemma lt_1_r : forall n:nat, n < 1 -> n = 0. intros n H ; dependent induction H. The subgoal is cleaned up as the tactic tries to automatically @@ -2300,16 +2300,16 @@ and an explanation of the underlying technique. .. flag:: Structural Injection - This option ensure that :n:`injection @term` erases the original hypothesis + This flag ensures that :n:`injection @term` erases the original hypothesis and leaves the generated equalities in the context rather than putting them as antecedents of the current goal, as if giving :n:`injection @term as` - (with an empty list of names). This option is off by default. + (with an empty list of names). This flag is off by default. .. flag:: Keep Proof Equalities By default, :tacn:`injection` only creates new equalities between :n:`@term`\s whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special - behavior for objects that are proofs of a statement in :g:`Prop`. This option + behavior for objects that are proofs of a statement in :g:`Prop`. This flag controls this behavior. .. tacn:: inversion @ident @@ -2691,7 +2691,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. 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` ``.`` + ``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. @@ -2862,26 +2862,26 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. flag:: Regular Subst Tactic - This option controls the behavior of :tacn:`subst`. When it is + 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 option, a second call to + 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 option would + + 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 - option would be a cause of failure of :tacn:`subst`. + 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 option it may break. + hypotheses, which without the flag it may break. default. @@ -3005,7 +3005,7 @@ the conversion in hypotheses :n:`{+ @ident}`. 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 + :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 @@ -3049,18 +3049,18 @@ the conversion in hypotheses :n:`{+ @ident}`. This is a synonym for ``lazy beta delta iota zeta``. -.. tacv:: compute {+ @qualid} - cbv {+ @qualid} +.. tacv:: compute [ {+ @qualid} ] + cbv [ {+ @qualid} ] These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. -.. tacv:: compute -{+ @qualid} - cbv -{+ @qualid} +.. tacv:: compute - [ {+ @qualid} ] + cbv - [ {+ @qualid} ] These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. -.. tacv:: lazy {+ @qualid} - lazy -{+ @qualid} +.. 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`. @@ -3071,7 +3071,7 @@ the conversion in hypotheses :n:`{+ @ident}`. 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 - ``cbv`` tactic, but it cannot be fine-tuned. It is specially interesting for + :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. @@ -3080,14 +3080,14 @@ the conversion in hypotheses :n:`{+ @ident}`. 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 ``vm_compute``. Note however that the + 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 Profiling - On Linux, if you have the ``perf`` profiler installed, this option makes - it possible to profile ``native_compute`` evaluations. + 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 @@ -3097,13 +3097,13 @@ the conversion in hypotheses :n:`{+ @ident}`. 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 - ``native_compute`` in a script. From the Linux command line, run ``perf report`` + :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 option makes :tacn:`cbv` (and its derivative :tacn:`compute`) print + This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print information about the constants it encounters and the unfolding decisions it makes. @@ -3153,14 +3153,15 @@ the conversion in hypotheses :n:`{+ @ident}`. use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls. - The ``cbn`` tactic is claimed to be a more principled, faster and more - predictable replacement for ``simpl``. + The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + predictable replacement for :tacn:`simpl`. - The ``cbn`` tactic accepts the same flags as ``cbv`` and ``lazy``. The - behavior of both ``simpl`` and ``cbn`` can be tuned using the - Arguments vernacular command as follows: + 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 Arguments vernacular command as follows: - + A constant can be marked to be never unfolded by ``cbn`` or ``simpl``: + + A constant can be marked to be never unfolded by :tacn:`cbn` or + :tacn:`simpl`: .. example:: @@ -3169,7 +3170,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Arguments minus n m : simpl never. After that command an expression like :g:`(minus (S x) y)` is left - untouched by the tactics ``cbn`` and ``simpl``. + untouched by the tactics :tacn:`cbn` and :tacn:`simpl`. + A constant can be marked to be unfolded only if applied to enough arguments. The number of arguments required can be specified using the @@ -3184,7 +3185,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Notation "f \o g" := (fcomp f g) (at level 50). After that command the expression :g:`(f \o g)` is left untouched by - ``simpl`` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. + :tacn:`simpl` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. The same mechanism can be used to make a constant volatile, i.e. always unfolded. @@ -3206,7 +3207,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Arguments minus !n !m. After that command, the expression :g:`(minus (S x) y)` is left untouched - by ``simpl``, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`. + by :tacn:`simpl`, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`. + A special heuristic to determine if a constant has to be unfolded can be activated with the following command: @@ -3222,25 +3223,25 @@ the conversion in hypotheses :n:`{+ @ident}`. :g:`(minus (S (S x)) (S y))` is simplified to :g:`(minus (S x) y)` even if an extra simplification is possible. - In detail, the tactic ``simpl`` first applies :math:`\beta`:math:`\iota`-reduction. Then, it - expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`- - reduction. But, when no :math:`\iota` rule is applied after unfolding then - :math:`\delta`-reductions are not applied. For instance trying to use ``simpl`` on + In detail, the tactic :tacn:`simpl` first applies :math:`\beta`:math:`\iota`-reduction. Then, it + expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`-reduction. + But, when no :math:`\iota` rule is applied after unfolding then + :math:`\delta`-reductions are not applied. For instance trying to use :tacn:`simpl` on :g:`(plus n O) = n` changes nothing. Notice that only transparent constants whose name can be reused in the - recursive calls are possibly unfolded by ``simpl``. For instance a + 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 ``simpl`` and ``cbn``. - The tactic ``cbn`` reduces whenever it will be able to reuse it or not: + 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} +.. 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`). + 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 @@ -3249,7 +3250,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @pattern at {+ @num} - This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + This applies :tacn:`simpl` only to the :n:`{+ @num}` occurrences of the subterms matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences. @@ -3265,12 +3266,12 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @qualid at {+ @num} simpl @string at {+ @num} - This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose + This applies :tacn:`simpl` only to the :n:`{+ @num}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). .. flag:: Debug RAKAM - This option makes :tacn:`cbn` print various debugging information. + This flag makes :tacn:`cbn` print various debugging information. ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. .. tacn:: unfold @qualid @@ -3547,7 +3548,7 @@ Automation Info Trivial Debug Trivial - These options enable printing of informative or debug information for + These flags enable printing of informative or debug information for the :tacn:`auto` and :tacn:`trivial` tactics. .. tacn:: eauto @@ -3575,7 +3576,7 @@ Automation The various options for :tacn:`eauto` are the same as for :tacn:`auto`. - :tacn:`eauto` also obeys the following options: + :tacn:`eauto` also obeys the following flags: .. flag:: Info Eauto Debug Eauto @@ -3719,7 +3720,7 @@ automatically created. .. cmdv:: Local Hint @hint_definition : {+ @ident} This is used to declare hints that must not be exported to the other modules - that require and import the current module. Inside a section, the option + that require and import the current module. Inside a section, the flag Local is useless since hints do not survive anyway to the closure of sections. @@ -3960,6 +3961,9 @@ At Coq startup, only the core database is nonempty and can be used. :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. @@ -4001,8 +4005,8 @@ use one or several databases specific to your development. 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 ``auto`` - hint bases and thatauto does not take them into account. + (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 @@ -4192,7 +4196,7 @@ some incompatibilities. .. flag:: Intuition Negation Unfolding Controls whether :tacn:`intuition` unfolds inner negations which do not need - to be unfolded. This option is on by default. + to be unfolded. This flag is on by default. .. tacn:: rtauto :name: rtauto @@ -4233,7 +4237,13 @@ some incompatibilities. .. tacv:: firstorder using {+ @qualid} - Adds lemmas :n:`{+ @qualid}` to the proof-search environment. If :n:`@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. @@ -4242,7 +4252,7 @@ some incompatibilities. Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident}` to the proof-search environment. -.. tacv:: firstorder @tactic using {+ @qualid} with {+ @ident} +.. tacv:: firstorder @tactic using {+, @qualid} with {+ @ident} This combines the effects of the different variants of :tacn:`firstorder`. @@ -4312,7 +4322,7 @@ some incompatibilities. .. flag:: Congruence Verbose - This option makes :tacn:`congruence` print debug information. + This flag makes :tacn:`congruence` print debug information. Checking properties of terms @@ -4549,7 +4559,7 @@ Inversion .. tacv:: functional inversion @num - This does the same thing as :n:`intros until @num` folowed by + This does the same thing as :n:`intros until @num` followed by :n:`functional inversion @ident` where :token:`ident` is the identifier for the last introduced hypothesis. @@ -4565,8 +4575,8 @@ Inversion Classical tactics ----------------- -In order to ease the proving process, when the Classical module is -loaded. A few more tactics are available. Make sure to load the module +In order to ease the proving process, when the ``Classical`` module is +loaded, a few more tactics are available. Make sure to load the module using the ``Require Import`` command. .. tacn:: classical_left @@ -4623,7 +4633,7 @@ Automating The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision procedure for Presburger arithmetic. It solves quantifier-free - formulas built with `~`, `\/`, `/\`, `->` on top of equalities, + formulas built with `~`, `\\/`, `/\\`, `->` on top of equalities, inequalities and disequalities on both the type :g:`nat` of natural numbers and :g:`Z` of binary integers. This tactic must be loaded by the command ``Require Import Omega``. See the additional documentation about omega diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 5f3e82938d..89b24ea8a3 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -195,7 +195,7 @@ Requests to the environment (see Section :ref:`invocation-of-tactics`). -.. cmd:: Eval @redexpr in @term +.. cmd:: Eval @red_expr in @term This command performs the specified reduction on :n:`@term`, and displays the resulting term with its type. The term to be reduced may depend on @@ -627,6 +627,7 @@ file is a particular case of module called *library file*. as ``Export``. .. cmdv:: From @dirpath Require @qualid + :name: From ... Require ... This command acts as :cmd:`Require`, but picks any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid` @@ -870,26 +871,6 @@ interactively, they cannot be part of a vernacular file loaded via have to undo some extra commands and end on a state :n:`@num′ ≤ @num` if necessary. - .. cmdv:: Backtrack @num @num @num - :name: Backtrack - - .. deprecated:: 8.4 - - :cmd:`Backtrack` is a *deprecated* form of - :cmd:`BackTo` which allows explicitly manipulating the proof environment. The - three numbers represent the following: - - + *first number* : State label to reach, as for :cmd:`BackTo`. - + *second number* : *Proof state number* to unbury once aborts have been done. - |Coq| will compute the number of :cmd:`Undo` to perform (see Chapter :ref:`proofhandling`). - + *third number* : Number of :cmd:`Abort` to perform, i.e. the number of currently - opened nested proofs that must be canceled (see Chapter :ref:`proofhandling`). - - .. exn:: Invalid backtrack. - - The destination state label is unknown. - - .. _quitting-and-debugging: Quitting and debugging @@ -981,7 +962,7 @@ Controlling display .. flag:: Silent - This option controls the normal displaying. + This flag controls the normal displaying. .. opt:: Warnings "{+, {? {| - | + } } @ident }" :name: Warnings @@ -996,7 +977,7 @@ Controlling display .. flag:: Search Output Name Only - This option restricts the output of search commands to identifier names; + This flag restricts the output of search commands to identifier names; turning it on causes invocations of :cmd:`Search`, :cmd:`SearchHead`, :cmd:`SearchPattern`, :cmd:`SearchRewrite` etc. to omit types from their output, printing only identifiers. @@ -1017,7 +998,7 @@ Controlling display .. flag:: Printing Compact Contexts - This option controls the compact display mode for goals contexts. When on, + This flag controls the compact display mode for goals contexts. When on, the printer tries to reduce the vertical size of goals contexts by putting several variables (even if of different types) on the same line provided it does not exceed the printing width (see :opt:`Printing Width`). At the time @@ -1025,14 +1006,15 @@ Controlling display .. flag:: Printing Unfocused - This option controls whether unfocused goals are displayed. Such goals are + This flag controls whether unfocused goals are displayed. Such goals are created by focusing other goals with bullets (see :ref:`bullets` or :ref:`curly braces <curly-braces>`). It is off by default. .. flag:: Printing Dependent Evars Line - This option controls the printing of the “(dependent evars: …)” line when - ``-emacs`` is passed. + This flag controls the printing of the “(dependent evars: …)” information + after each tactic. The information is used by the Prooftree tool in Proof + General. (https://askra.de/software/prooftree) .. _vernac-controlling-the-reduction-strategies: @@ -1164,7 +1146,7 @@ described first. Print all the currently non-transparent strategies. -.. cmd:: Declare Reduction @ident := @redexpr +.. cmd:: Declare Reduction @ident := @red_expr This command allows giving a short name to a reduction expression, for instance ``lazy beta delta [foo bar]``. This short name can then be used @@ -1176,7 +1158,7 @@ described first. functor applications will be rejected if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but nothing prevents the user from also performing a - :n:`Ltac @ident := @redexpr`. + :n:`Ltac @ident := @red_expr`. .. seealso:: :ref:`performingcomputations` @@ -1224,6 +1206,79 @@ Controlling the locality of commands occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. _controlling-typing-flags: + +Controlling Typing Flags +---------------------------- + +.. flag:: Guard Checking + + This flag can be used to enable/disable the guard checking of + fixpoints. Warning: this can break the consistency of the system, use at your + own risk. Decreasing argument can still be specified: the decrease is not checked + anymore but it still affects the reduction of the term. Unchecked fixpoints are + printed by :cmd:`Print Assumptions`. + +.. flag:: Positivity Checking + + This flag can be used to enable/disable the positivity checking of inductive + types and the productivity checking of coinductive types. Warning: this can + break the consistency of the system, use at your own risk. Unchecked + (co)inductive types are printed by :cmd:`Print Assumptions`. + +.. flag:: Universe Checking + + This flag can be used to enable/disable the checking of universes, providing a + form of "type in type". Warning: this breaks the consistency of the system, use + at your own risk. Constants relying on "type in type" are printed by + :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line + argument (see :ref:`command-line-options`). + +.. cmd:: Print Typing Flags + + Print the status of the three typing flags: guard checking, positivity checking + and universe checking. + +.. example:: + + .. coqtop:: all reset + + Unset Guard Checking. + + Print Typing Flags. + + Fixpoint f (n : nat) : False + := f n. + + Fixpoint ackermann (m n : nat) {struct m} : nat := + match m with + | 0 => S n + | S m => + match n with + | 0 => ackermann m 1 + | S n => ackermann m (ackermann (S m) n) + end + end. + + Print Assumptions ackermann. + + Note that the proper way to define the Ackermann function is to use + an inner fixpoint: + + .. coqtop:: all reset + + Fixpoint ack m := + fix ackm n := + match m with + | 0 => S n + | S m' => + match n with + | 0 => ack m' 1 + | S n' => ack m' (ackm n') + end + end. + + .. _internal-registration-commands: Internal registration commands |