diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 66 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 76 |
2 files changed, 82 insertions, 60 deletions
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 583b73e53d..e12e4d897a 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -3,6 +3,8 @@ Proof schemes =============== +.. _proofschemes-induction-principles: + Generation of induction principles with ``Scheme`` -------------------------------------------------------- @@ -10,7 +12,7 @@ The ``Scheme`` command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Its syntax follows the schema: -.. cmd:: Scheme ident := Induction for ident' Sort sort {* with ident := Induction for ident' Sort sort} +.. cmd:: Scheme @ident := Induction for @ident Sort sort {* with @ident := Induction for @ident Sort sort} where each `ident'ᵢ` is a different inductive type identifier belonging to the same package of mutual inductive definitions. This @@ -18,17 +20,17 @@ command generates the `identᵢ`s to be mutually recursive definitions. Each term `identᵢ` proves a general principle of mutual induction for objects in type `identᵢ`. -.. cmdv:: Scheme ident := Minimality for ident' Sort sort {* with ident := Minimality for ident' Sort sort} +.. cmdv:: Scheme @ident := Minimality for @ident Sort sort {* with @ident := Minimality for @ident' Sort sort} Same as before but defines a non-dependent elimination principle more natural in case of inductively defined relations. -.. cmdv:: Scheme Equality for ident +.. cmdv:: Scheme Equality for @ident Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident` involves some other inductive types, their equality has to be defined first. -.. cmdv:: Scheme Induction for ident Sort sort {* with Induction for ident Sort sort} +.. cmdv:: Scheme Induction for @ident Sort sort {* with Induction for @ident Sort sort} If you do not provide the name of the schemes, they will be automatically computed from the sorts involved (works also with Minimality). @@ -101,26 +103,34 @@ induction for objects in type `identᵢ`. Automatic declaration of schemes ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: Elimination Schemes + It is possible to deactivate the automatic declaration of the induction principles when defining a new inductive type with the ``Unset Elimination Schemes`` command. It may be reactivated at any time with ``Set Elimination Schemes``. -The types declared with the keywords ``Variant`` (see :ref:`TODO-1.3.3`) and ``Record`` -(see :ref:`Record Types <record-types>`) do not have an automatic declaration of the induction -principles. It can be activated with the command -``Set Nonrecursive Elimination Schemes``. It can be deactivated again with -``Unset Nonrecursive Elimination Schemes``. - -In addition, the ``Case Analysis Schemes`` flag governs the generation of -case analysis lemmas for inductive types, i.e. corresponding to the -pattern-matching term alone and without fixpoint. -You can also activate the automatic declaration of those Boolean -equalities (see the second variant of ``Scheme``) with respectively the -commands ``Set Boolean Equality Schemes`` and ``Set Decidable Equality -Schemes``. However you have to be careful with this option since Coq may -now reject well-defined inductive types because it cannot compute a -Boolean equality for them. +.. opt:: Nonrecursive Elimination Schemes + +This option controls whether types declared with the keywords :cmd:`Variant` and +:cmd:`Record` get an automatic declaration of the induction principles. + +.. opt:: Case Analysis Schemes + + This flag governs the generation of case analysis lemmas for inductive types, + i.e. corresponding to the pattern-matching term alone and without fixpoint. + +.. opt:: Boolean Equality Schemes + +.. opt:: Decidable Equality Schemes + +These flags control the automatic declaration of those Boolean equalities (see +the second variant of ``Scheme``). + +.. warning:: + + You have to be careful with this option since Coq may now reject well-defined + inductive types because it cannot compute a Boolean equality for them. .. opt:: Rewriting Schemes @@ -133,7 +143,7 @@ The ``Combined Scheme`` command is a tool for combining induction principles generated by the ``Scheme command``. Its syntax follows the schema : -.. cmd:: Combined Scheme ident from {+, ident} +.. cmd:: Combined Scheme @ident from {+, ident} where each identᵢ after the ``from`` is a different inductive principle that must belong to the same package of mutual inductive principle definitions. @@ -163,6 +173,8 @@ concluded by the conjunction of their conclusions. Check tree_forest_mutind. +.. _functional-scheme: + Generation of induction principles with ``Functional`` ``Scheme`` ----------------------------------------------------------------- @@ -172,7 +184,7 @@ generating automatically induction principles corresponding to available via ``Require Import FunInd``. Its syntax then follows the schema: -.. cmd:: Functional Scheme ident := Induction for ident' Sort sort {* with ident := Induction for ident' Sort sort} +.. cmd:: Functional Scheme @ident := Induction for ident' Sort sort {* with @ident := Induction for @ident Sort sort} where each `ident'ᵢ` is a different mutually defined function name (the names must be in the same order as when they were defined). This @@ -229,7 +241,7 @@ definition written by the user. simpl; auto with arith. Qed. - We can use directly the functional induction (:ref:`TODO-8.5.5`) tactic instead + We can use directly the functional induction (:tacn:`function induction`) tactic instead of the pattern/apply trick: .. coqtop:: all @@ -305,13 +317,15 @@ definition written by the user. .. coqtop:: all Check tree_size_ind2. + +.. _derive-inversion: Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- The syntax of ``Derive`` ``Inversion`` follows the schema: -.. cmd:: Derive Inversion ident with forall (x : T), I t Sort sort +.. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort This command generates an inversion principle for the `inversion … using` tactic. Let `I` be an inductive predicate and `x` the variables occurring @@ -320,17 +334,17 @@ sort `sort` corresponding to the instance `∀ (x:T), I t` with the name `ident` in the global environment. When applied, it is equivalent to having inverted the instance with the tactic `inversion`. -.. cmdv:: Derive Inversion_clear ident with forall (x:T), I t Sort sort +.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort sort When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic `inversion_clear`. -.. cmdv:: Derive Dependent Inversion ident with forall (x:T), I t Sort sort +.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion`. -.. cmdv:: Derive Dependent Inversion_clear ident with forall(x:T), I t Sort sort +.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion_clear`. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6e6d664475..c4a7121ce4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -10,12 +10,12 @@ parses and prints objects, i.e. the translations between the concrete and internal representations of terms and commands. The main commands to provide custom symbolic notations for terms are -``Notation`` and ``Infix``. They are described in section 12.1. There is also a +``Notation`` and ``Infix``. They are described in section :ref:`Notations`. There is also a variant of ``Notation`` which does not modify the parser. This provides with a form of abbreviation and it is described in Section :ref:`Abbreviations`. It is sometimes expected that the same symbolic notation has different meanings in different contexts. To achieve this form of overloading, |Coq| offers a notion -of interpretation scope. This is described in Section :ref:`scopes`. +of interpretation scope. This is described in Section :ref:`Scopes`. The main command to provide custom notations for tactics is ``Tactic Notation``. It is described in Section :ref:`TacticNotation`. @@ -24,12 +24,16 @@ It is described in Section :ref:`TacticNotation`. Set Printing Depth 50. +.. _Notations: + Notations --------- Basic notations ~~~~~~~~~~~~~~~ +.. cmd:: Notation + A *notation* is a symbolic expression denoting some term or term pattern. @@ -68,7 +72,7 @@ have to be given. .. note:: The right-hand side of a notation is interpreted at the time the notation is - given. In particular, disambiguiation of constants, implicit arguments (see + given. In particular, disambiguation of constants, implicit arguments (see Section :ref:`ImplicitArguments`), coercions (see Section :ref:`Coercions`), etc. are resolved at the time of the declaration of the notation. @@ -343,13 +347,13 @@ inductive type or a recursive constant and a notation for it. Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Thanks to reserved notations, the inductive, co-inductive, record, recursive -and corecursive definitions can benefit of customized notations. To do -this, insert a ``where`` notation clause after the definition of the -(co)inductive type or (co)recursive term (or after the definition of -each of them in case of mutual definitions). The exact syntax is given -on Figure 12.1 for inductive, co-inductive, recursive and corecursive -definitions and on Figure :ref:`record-syntax` for records. Here are examples: +Thanks to reserved notations, the inductive, co-inductive, record, recursive and +corecursive definitions can benefit of customized notations. To do this, insert +a ``where`` notation clause after the definition of the (co)inductive type or +(co)recursive term (or after the definition of each of them in case of mutual +definitions). The exact syntax is given by :token:`decl_notation` for inductive, +co-inductive, recursive and corecursive definitions and in :ref:`record-types` +for records. Here are examples: .. coqtop:: in @@ -379,23 +383,21 @@ Displaying informations about notations :opt:`Printing All` To disable other elements in addition to notations. +.. _locating-notations: + Locating notations ~~~~~~~~~~~~~~~~~~ -.. cmd:: Locate @symbol - - To know to which notations a given symbol belongs to, use the command - ``Locate symbol``, where symbol is any (composite) symbol surrounded by double - quotes. To locate a particular notation, use a string where the variables of the - notation are replaced by “_” and where possible single quotes inserted around - identifiers or tokens starting with a single quote are dropped. - - .. coqtop:: all +To know to which notations a given symbol belongs to, use the :cmd:`Locate` +command. You can call it on any (composite) symbol surrounded by double quotes. +To locate a particular notation, use a string where the variables of the +notation are replaced by “_” and where possible single quotes inserted around +identifiers or tokens starting with a single quote are dropped. - Locate "exists". - Locate "exists _ .. _ , _". +.. coqtop:: all - .. todo:: See also: Section 6.3.10. + Locate "exists". + Locate "exists _ .. _ , _". Notations and binders ~~~~~~~~~~~~~~~~~~~~~ @@ -433,8 +435,7 @@ Binders bound in the notation and parsed as patterns In the same way as patterns can be used as binders, as in :g:`fun '(x,y) => x+y` or :g:`fun '(existT _ x _) => x`, notations can be -defined so that any pattern (in the sense of the entry :n:`@pattern` of -Figure :ref:`term-syntax-aux`) can be used in place of the +defined so that any :n:`@pattern` can be used in place of the binder. Here is an example: .. coqtop:: in reset @@ -473,7 +474,7 @@ variable. Here is an example showing the difference: The default level for a ``pattern`` is 0. One can use a different level by using ``pattern at level`` :math:`n` where the scale is the same as the one for -terms (Figure :ref:`init-notations`). +terms (see :ref:`init-notations`). Binders bound in the notation and parsed as terms +++++++++++++++++++++++++++++++++++++++++++++++++ @@ -489,7 +490,7 @@ the following: This is so because the grammar also contains rules starting with :g:`{}` and followed by a term, such as the rule for the notation :g:`{ A } + { B }` for the -constant :g:`sumbool` (see Section :ref:`sumbool`). +constant :g:`sumbool` (see Section :ref:`specification`). Then, in the rule, ``x ident`` is replaced by ``x at level 99 as ident`` meaning that ``x`` is parsed as a term at level 99 (as done in the notation for @@ -689,8 +690,7 @@ side. E.g.: Summary ~~~~~~~ -Syntax of notations -~~~~~~~~~~~~~~~~~~~ +**Syntax of notations** The different syntactic variants of the command Notation are given on the following figure. The optional :token:`scope` is described in the Section 12.2. @@ -743,8 +743,7 @@ following figure. The optional :token:`scope` is described in the Section 12.2. given to some notation, say ``"{ y } & { z }"`` in fact applies to the underlying ``"{ x }"``\-free rule which is ``"y & z"``). -Persistence of notations -~~~~~~~~~~~~~~~~~~~~~~~~ +**Persistence of notations** Notations do not survive the end of sections. @@ -753,6 +752,8 @@ Notations do not survive the end of sections. Notations survive modules unless the command ``Local Notation`` is used instead of ``Notation``. +.. _Scopes: + Interpretation scopes ---------------------- @@ -827,6 +828,8 @@ lonely notations. These scopes, in opening order, are ``core_scope``, These variants survive sections. They behave as if Global were absent when not inside a section. +.. _LocalInterpretationRulesForNotations: + Local interpretation rules for notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -857,6 +860,7 @@ Binding arguments of a constant to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ .. cmd:: Arguments @qualid {+ @name%@scope} + :name: Arguments (scopes) It is possible to set in advance that some arguments of a given constant have to be interpreted in a given scope. The command is @@ -895,7 +899,7 @@ Binding arguments of a constant to an interpretation scope .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes Defines extra argument scopes, to be used in case of coercion to Funclass - (see Chapter :ref:`Coercions-full`) or with a computed type. + (see Chapter :ref:`implicitcoercions`) or with a computed type. .. cmdv:: Global Arguments @qualid {+ @name%@scope} @@ -955,7 +959,7 @@ Binding types of arguments to an interpretation scope type :g:`t` in :g:`f t a` is not recognized as an argument to be interpreted in scope ``scope``. - More generally, any coercion :n:`@class` (see Chapter :ref:`Coercions-full`) + More generally, any coercion :n:`@class` (see Chapter :ref:`implicitcoercions`) can be bound to an interpretation scope. The command to do it is :n:`Bind Scope @scope with @class` @@ -1125,6 +1129,8 @@ Displaying informations about scopes class of all the existing interpretation scopes. It also displays the lonely notations. +.. _Abbreviations: + Abbreviations -------------- @@ -1187,6 +1193,8 @@ Abbreviations denoted expression is performed at definition time. Type-checking is done only at the time of use of the abbreviation. +.. _TacticNotation: + Tactic Notations ----------------- @@ -1194,7 +1202,7 @@ Tactic notations allow to customize the syntax of the tactics of the tactic language. Tactic notations obey the following syntax: .. productionlist:: coq - tacn : [Local] Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. + tacn : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. prod_item : `string` | `tactic_argument_type`(`ident`) tactic_level : (at level `natural`) tactic_argument_type : ident | simple_intropattern | reference @@ -1205,7 +1213,7 @@ tactic language. Tactic notations obey the following syntax: : | tactic | tactic0 | tactic1 | tactic2 | tactic3 : | tactic4 | tactic5 -.. cmd:: {? Local} Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic. +.. cmd:: Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic. A tactic notation extends the parser and pretty-printer of tactics with a new rule made of the list of production items. It then evaluates into the |