diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 83 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 76 |
2 files changed, 79 insertions, 80 deletions
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 8e23e61018..abecee8459 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -8,35 +8,36 @@ Proof schemes Generation of induction principles with ``Scheme`` -------------------------------------------------------- -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 := } @scheme_kind {* with {? @ident := } @scheme_kind } -.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort @sort {* with @ident__i := Induction for @ident__j Sort @sort} + .. insertprodn scheme_kind sort_family - This command is a high-level tool for generating automatically + .. prodn:: + scheme_kind ::= Equality for @reference + | {| Induction | Minimality | Elimination | Case } for @reference Sort @sort_family + sort_family ::= Set + | Prop + | SProp + | Type + + A high-level tool for automatically generating (possibly mutual) induction principles for given types and sorts. - Each :n:`@ident__j` is a different inductive type identifier belonging to + Each :n:`@reference` is a different inductive type identifier belonging to the same package of mutual inductive definitions. - The command generates the :n:`@ident__i`\s to be mutually recursive - definitions. Each term :n:`@ident__i` proves a general principle of mutual - induction for objects in type :n:`@ident__j`. - -.. 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. + The command generates the :n:`@ident`\s as mutually recursive + definitions. Each term :n:`@ident` proves a general principle of mutual + induction for objects in type :n:`@reference`. -.. cmdv:: Scheme Equality for @ident - :name: Scheme Equality + :n:`@ident` + The name of the scheme. If not provided, the scheme name will be determined automatically + from the sorts involved. - 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. + :n:`Minimality for @reference Sort @sort_family` + Defines a non-dependent elimination principle more natural for inductively defined relations. -.. 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). + :n:`Equality for @reference` + Tries to generate a Boolean equality and a proof of the decidability of the usual equality. + If :token:`reference` involves other inductive types, their equality has to be defined first. .. example:: @@ -128,7 +129,7 @@ Automatic declaration of schemes .. warning:: - You have to be careful with these flags since Coq may now reject well-defined + You have to be careful with these flags since |Coq| may now reject well-defined inductive types because it cannot compute a Boolean equality for them. .. flag:: Rewriting Schemes @@ -138,13 +139,13 @@ Automatic declaration of schemes Combined Scheme ~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Combined Scheme @ident from {+, @ident__i} +.. cmd:: Combined Scheme @ident__def from {+, @ident } This command is a tool for combining induction principles generated by the :cmd:`Scheme` command. - Each :n:`@ident__i` is a different inductive principle that must belong + Each :n:`@ident` is a different inductive principle that must belong to the same package of mutual inductive principle definitions. - This command generates :n:`@ident` to be the conjunction of the + This command generates :n:`@ident__def` as the conjunction of the principles: it is built from the common premises of the principles and concluded by the conjunction of their conclusions. In the case where all the inductive principles used are in sort @@ -197,32 +198,30 @@ Combined Scheme Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- -.. cmd:: Derive Inversion @ident with @ident Sort @sort - Derive Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort +.. cmd:: Derive Inversion @ident with @one_term {? Sort @sort_family } - This command generates an inversion principle for the - :tacn:`inversion ... using ...` tactic. The first :token:`ident` is the name - of the generated principle. The second :token:`ident` should be an inductive - predicate, and :n:`{* @binder }` the variables occurring in the term - :token:`term`. This command generates the inversion lemma for the sort - :token:`sort` corresponding to the instance :n:`forall {* @binder }, @ident @term`. - When applied, it is equivalent to having inverted the instance with the - tactic :g:`inversion`. + Generates an inversion lemma for the + :tacn:`inversion ... using ...` tactic. :token:`ident` is the name + of the generated lemma. :token:`one_term` should be in the form + :token:`qualid` or :n:`(forall {+ @binder }, @qualid @term)` where + :token:`qualid` is the name of an inductive + predicate and :n:`{+ @binder }` binds the variables occurring in the term + :token:`term`. The lemma is generated for the sort + :token:`sort_family` corresponding to :token:`one_term`. + Applying the lemma is equivalent to inverting the instance with the + :tacn:`inversion` tactic. -.. cmdv:: Derive Inversion_clear @ident with @ident Sort @sort - Derive Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort +.. cmd:: Derive Inversion_clear @ident with @one_term {? Sort @sort_family } 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 @ident Sort @sort - Derive Dependent Inversion @ident with (forall {* @binder }, @ident @term) Sort @sort +.. cmd:: Derive Dependent Inversion @ident with @one_term Sort @sort_family When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion`. -.. cmdv:: Derive Dependent Inversion_clear @ident with @ident Sort @sort - Derive Dependent Inversion_clear @ident with (forall {* @binder }, @ident @term) Sort @sort +.. cmd:: Derive Dependent Inversion_clear @ident with @one_term Sort @sort_family 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 d6db305300..06018304ab 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -3,7 +3,7 @@ Syntax extensions and notation scopes ===================================== -In this chapter, we introduce advanced commands to modify the way Coq +In this chapter, we introduce advanced commands to modify the way |Coq| parses and prints objects, i.e. the translations between the concrete and internal representations of terms and commands. @@ -71,7 +71,7 @@ least 3 characters and starting with a simple quote must be quoted Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3). A notation binds a syntactic expression to a term. Unless the parser -and pretty-printer of Coq already know how to deal with the syntactic +and pretty-printer of |Coq| already know how to deal with the syntactic expression (such as through :cmd:`Reserved Notation` or for notations that contain only literals), explicit precedences and associativity rules have to be given. @@ -88,7 +88,7 @@ Precedences and associativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Mixing different symbolic notations in the same text may cause serious -parsing ambiguity. To deal with the ambiguity of notations, Coq uses +parsing ambiguity. To deal with the ambiguity of notations, |Coq| uses precedence levels ranging from 0 to 100 (plus one extra level numbered 200) and associativity rules. @@ -99,7 +99,7 @@ Consider for example the new notation Notation "A \/ B" := (or A B). Clearly, an expression such as :g:`forall A:Prop, True /\ A \/ A \/ False` -is ambiguous. To tell the Coq parser how to interpret the +is ambiguous. To tell the |Coq| parser how to interpret the expression, a priority between the symbols ``/\`` and ``\/`` has to be given. Assume for instance that we want conjunction to bind more than disjunction. This is expressed by assigning a precedence level to each @@ -117,7 +117,7 @@ defaults to :g:`True /\ (False /\ False)` (right associativity) or to expression is not well-formed and that parentheses are mandatory (this is a “no associativity”) [#no_associativity]_. We do not know of a special convention for the associativity of disjunction and conjunction, so let us apply -right associativity (which is the choice of Coq). +right associativity (which is the choice of |Coq|). Precedence levels and associativity rules of notations are specified with a list of parenthesized :n:`@syntax_modifier`\s. Here is how the previous examples refine: @@ -187,7 +187,7 @@ left. See the next section for more about factorization. Simple factorization rules ~~~~~~~~~~~~~~~~~~~~~~~~~~ -Coq extensible parsing is performed by *Camlp5* which is essentially a LL1 +|Coq| extensible parsing is performed by *Camlp5* which is essentially a LL1 parser: it decides which notation to parse by looking at tokens from left to right. Hence, some care has to be taken not to hide already existing rules by new rules. Some simple left factorization work has to be done. Here is an example. @@ -209,16 +209,16 @@ need to force the parsing level of ``y``, as follows. Notation "x < y" := (lt x y) (at level 70). Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level). -For the sake of factorization with Coq predefined rules, simple rules +For the sake of factorization with |Coq| predefined rules, simple rules have to be observed for notations starting with a symbol, e.g., rules starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list -of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`. +of |Coq| predefined notations can be found in the chapter on :ref:`thecoqlibrary`. Displaying symbolic notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The command :cmd:`Notation` has an effect both on the Coq parser and on the -Coq printer. For example: +The command :cmd:`Notation` has an effect both on the |Coq| parser and on the +|Coq| printer. For example: .. coqtop:: all @@ -226,7 +226,7 @@ Coq printer. For example: However, printing, especially pretty-printing, also requires some care. We may want specific indentations, line breaks, alignment if on -several lines, etc. For pretty-printing, |Coq| relies on |ocaml| +several lines, etc. For pretty-printing, |Coq| relies on |OCaml| formatting library, which provides indentation and automatic line breaks depending on page width by means of *formatting boxes*. @@ -349,12 +349,12 @@ Reserving notations .. cmd:: Reserved Notation @string {? ( {+, @syntax_modifier } ) } - A given notation may be used in different contexts. Coq expects all + A given notation may be used in different contexts. |Coq| expects all uses of the notation to be defined at the same precedence and with the same associativity. To avoid giving the precedence and associativity every time, this command declares a parsing rule (:token:`string`) in advance without giving its interpretation. Here is an example from the initial - state of Coq. + state of |Coq|. .. coqtop:: in @@ -385,8 +385,8 @@ a :token:`decl_notations` clause after the definition of the (co)inductive type (co)recursive term (or after the definition of each of them in case of mutual definitions). The exact syntax is given by :n:`@decl_notation` for inductive, co-inductive, recursive and corecursive definitions and in :ref:`record-types` -for records. Note that only syntax modifiers that do not require to add or -change a parsing rule are accepted. +for records. Note that only syntax modifiers that do not require adding or +changing a parsing rule are accepted. .. insertprodn decl_notations decl_notation @@ -444,7 +444,7 @@ Displaying information about notations This command doesn't display all nonterminals of the grammar. For example, productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` - and `tactic_then_gen` which are not shown and can't be printed. + and `for_each_goal` which are not shown and can't be printed. Most of the grammar in the documentation was updated in 8.12 to make it accurate and readable. This was done using a new developer tool that extracts the grammar from the @@ -477,16 +477,16 @@ Displaying information about notations such as `1+2*3` in the usual way as `1+(2*3)`. However, most nonterminals have a single level. For example, this output from `Print Grammar tactic` shows the first 3 levels for - `tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative, + `ltac_expr`, designated as "5", "4" and "3". Level 3 is right-associative, which applies to the productions within it, such as the `try` construct:: - Entry tactic_expr is + Entry ltac_expr is [ "5" RIGHTA [ binder_tactic ] | "4" LEFTA [ SELF; ";"; binder_tactic | SELF; ";"; SELF - | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ] + | SELF; ";"; tactic_then_locality; for_each_goal; "]" ] | "3" RIGHTA [ IDENT "try"; SELF : @@ -510,7 +510,7 @@ Displaying information about notations The output for `Print Grammar constr` includes :cmd:`Notation` definitions, which are dynamically added to the grammar at run time. - For example, in the definition for `operconstr`, the production on the second line shown + For example, in the definition for `term`, the production on the second line shown here is defined by a :cmd:`Reserved Notation` command in `Notations.v`:: | "50" LEFTA @@ -762,7 +762,7 @@ recursive patterns. The basic example is: Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). On the right-hand side, an extra construction of the form ``.. t ..`` can -be used. Notice that ``..`` is part of the Coq syntax and it must not be +be used. Notice that ``..`` is part of the |Coq| syntax and it must not be confused with the three-dots notation “``…``” used in this manual to denote a sequence of arbitrary size. @@ -942,7 +942,7 @@ Custom entries Custom entries have levels, like the main grammar of terms and grammar of patterns have. The lower level is 0 and this is the level used by default to put rules delimited with tokens on both ends. The level is -left to be inferred by Coq when using :n:`in custom @ident`. The +left to be inferred by |Coq| when using :n:`in custom @ident`. The level is otherwise given explicitly by using the syntax :n:`in custom @ident at level @natural`, where :n:`@natural` refers to the level. @@ -996,7 +996,7 @@ associated to the custom entry ``expr``. The level can be omitted, as in Notation "[ e ]" := e (e custom expr). -in which case Coq infer it. If the sub-expression is at a border of +in which case |Coq| infer it. If the sub-expression is at a border of the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is determined by the associativity. If the sub-expression is not at the border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is @@ -1097,7 +1097,7 @@ Here are the syntax elements used by the various notation commands. time. Type checking is done only at the time of use of the notation. .. note:: Some examples of Notation may be found in the files composing - the initial state of Coq (see directory :file:`$COQLIB/theories/Init`). + the initial state of |Coq| (see directory :file:`$COQLIB/theories/Init`). .. note:: The notation ``"{ x }"`` has a special status in the main grammars of terms and patterns so that @@ -1122,7 +1122,7 @@ Here are the syntax elements used by the various notation commands. .. warn:: Use of @string Notation is deprecated as it is inconsistent with pattern syntax. This warning is disabled by default to avoid spurious diagnostics - due to legacy notation in the Coq standard library. + due to legacy notation in the |Coq| standard library. It can be turned on with the ``-w disj-pattern-notation`` flag. .. _Scopes: @@ -1156,7 +1156,7 @@ Most commands use :token:`scope_name`; :token:`scope_key`\s are used within :tok .. cmd:: Declare Scope @scope_name Declares a new notation scope. Note that the initial - state of Coq declares the following notation scopes: + state of |Coq| declares the following notation scopes: ``core_scope``, ``type_scope``, ``function_scope``, ``nat_scope``, ``bool_scope``, ``list_scope``, ``int_scope``, ``uint_scope``. @@ -1308,10 +1308,10 @@ recognized to be a ``Funclass`` instance, i.e., of type :g:`forall x:A, B` or .. _notation-scopes: -Notation scopes used in the standard library of Coq -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Notation scopes used in the standard library of |Coq| +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We give an overview of the scopes used in the standard library of Coq. +We give an overview of the scopes used in the standard library of |Coq|. For a complete list of notations in each scope, use the commands :cmd:`Print Scopes` or :cmd:`Print Scope`. @@ -1377,7 +1377,7 @@ Scopes` or :cmd:`Print Scope`. ``string_scope`` This scope includes notation for strings as elements of the type string. - Special characters and escaping follow Coq conventions on strings (see + Special characters and escaping follow |Coq| conventions on strings (see :ref:`lexical-conventions`). Especially, there is no convention to visualize non printable characters of a string. The file :file:`String.v` shows an example that contains quotes, a newline and a beep (i.e. the ASCII character @@ -1478,7 +1478,7 @@ Abbreviations An abbreviation expects no precedence nor associativity, since it is parsed as an usual application. Abbreviations are used as - much as possible by the Coq printers unless the modifier ``(only + much as possible by the |Coq| printers unless the modifier ``(only parsing)`` is given. An abbreviation is bound to an absolute name as an ordinary definition is @@ -1634,7 +1634,7 @@ Number notations with :n:`(abstract after @bignat)`, this warning is emitted when parsing a number greater than or equal to :token:`bignat`. Typically, this indicates that the fully computed representation - of numbers can be so large that non-tail-recursive OCaml + of numbers can be so large that non-tail-recursive |OCaml| functions run out of stack space when trying to walk them. .. warn:: The 'abstract after' directive has no effect when the parsing function (@qualid__parse) targets an option type. @@ -1894,12 +1894,12 @@ Tactic notations allow customizing the syntax of tactics. - :tacn:`unfold`, :tacn:`with_strategy` * - ``constr`` - - :token:`term` + - :token:`one_term` - a term - :tacn:`exact` * - ``uconstr`` - - :token:`term` + - :token:`one_term` - an untyped term - :tacn:`refine` @@ -1978,9 +1978,9 @@ Tactic notations allow customizing the syntax of tactics. .. rubric:: Footnotes .. [#and_or_levels] which are the levels effectively chosen in the current - implementation of Coq + implementation of |Coq| -.. [#no_associativity] Coq accepts notations declared as nonassociative but the parser on - which Coq is built, namely Camlp5, currently does not implement ``no associativity`` and - replaces it with ``left associativity``; hence it is the same for Coq: ``no associativity`` +.. [#no_associativity] |Coq| accepts notations declared as nonassociative but the parser on + which |Coq| is built, namely Camlp5, currently does not implement ``no associativity`` and + replaces it with ``left associativity``; hence it is the same for |Coq|: ``no associativity`` is in fact ``left associativity`` for the purposes of parsing |