diff options
Diffstat (limited to 'doc')
8 files changed, 153 insertions, 35 deletions
diff --git a/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst b/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst new file mode 100644 index 0000000000..208855b4c8 --- /dev/null +++ b/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst @@ -0,0 +1,9 @@ +- **Changed:** + Int63 notations now match up with the rest of the standard library: :g:`a \% + m`, :g:`m == n`, :g:`m < n`, :g:`m <= n`, and :g:`m ≤ n` have been replaced + with :g:`a mod m`, :g:`m =? n`, :g:`m <? n`, :g:`m <=? n`, and :g:`m ≤? n`. + The old notations are still available as deprecated notations. Additionally, + there is now a ``Coq.Numbers.Cyclic.Int63.Int63.Int63Notations`` module that + users can import to get the ``Int63`` notations without unqualifying the + various primitives (`#12479 <https://github.com/coq/coq/pull/12479>`_, fixes + `#12454 <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst new file mode 100644 index 0000000000..1709cf1eae --- /dev/null +++ b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst @@ -0,0 +1,9 @@ +- **Changed:** + PrimFloat notations now match up with the rest of the standard library: :g:`m + == n`, :g:`m < n`, and :g:`m <= n` have been replaced with :g:`m =? n`, :g:`m + <? n`, and :g:`m <=? n`. The old notations are still available as deprecated + notations. Additionally, there is now a + ``Coq.Floats.PrimFloat.PrimFloatNotations`` module that users can import to + get the ``PrimFloat`` notations without unqualifying the various primitives + (`#12556 <https://github.com/coq/coq/pull/12556>`_, fixes `#12454 + <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12716-curry.rst b/doc/changelog/10-standard-library/12716-curry.rst new file mode 100644 index 0000000000..51b59e4a94 --- /dev/null +++ b/doc/changelog/10-standard-library/12716-curry.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` + (`#12716 <https://github.com/coq/coq/pull/12716>`_, + by Yishuai Li). diff --git a/doc/changelog/10-standard-library/12799-list-repeat.rst b/doc/changelog/10-standard-library/12799-list-repeat.rst new file mode 100644 index 0000000000..adfc48f67b --- /dev/null +++ b/doc/changelog/10-standard-library/12799-list-repeat.rst @@ -0,0 +1,4 @@ +- **Added:** + New lemmas about ``repeat`` in ``List`` and ``Permutation``: ``repeat_app``, ``repeat_eq_app``, ``repeat_eq_cons``, ``repeat_eq_elt``, ``Forall_eq_repeat``, ``Permutation_repeat`` + (`#12799 <https://github.com/coq/coq/pull/12799>`_, + by Olivier Laurent). diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index f9d24fde0e..c27eb216e8 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -40,7 +40,7 @@ in the |Coq| root directory; this includes the modules ``Datatypes``, ``Specif``, ``Peano``, -``Wf`` and +``Wf`` and ``Tactics``. Module ``Logic_Type`` also makes it in the initial state. @@ -175,7 +175,7 @@ Quantifiers Then we find first-order quantifiers: .. coqtop:: in - + Definition all (A:Set) (P:A -> Prop) := forall x:A, P x. Inductive ex (A: Set) (P:A -> Prop) : Prop := ex_intro (x:A) (_:P x). @@ -256,12 +256,12 @@ Finally, a few easy lemmas are provided. single: f_equal2 ... f_equal5 (term) The theorem ``f_equal`` is extended to functions with two to five -arguments. The theorem are names ``f_equal2``, ``f_equal3``, +arguments. The theorem are names ``f_equal2``, ``f_equal3``, ``f_equal4`` and ``f_equal5``. For instance ``f_equal3`` is defined the following way. .. coqtop:: in abort - + Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), @@ -324,7 +324,7 @@ Programming Note that zero is the letter ``O``, and *not* the numeral ``0``. -The predicate ``identity`` is logically +The predicate ``identity`` is logically equivalent to equality but it lives in sort ``Type``. It is mainly maintained for compatibility. @@ -367,7 +367,7 @@ infix notation ``||``), ``xorb``, ``implb`` and ``negb``. Specification ~~~~~~~~~~~~~ -The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. +The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. They are available with the syntax shown in the previous section :ref:`datatypes`. For instance, given :g:`A:Type` and :g:`P:A->Prop`, the construct @@ -393,11 +393,11 @@ provided. .. coqtop:: in Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x). - Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := + Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := exist2 (x:A) (_:P x) (_:Q x). A *strong (dependent) sum* :g:`{x:A & P x}` may be also defined, -when the predicate ``P`` is now defined as a +when the predicate ``P`` is now defined as a constructor of types in ``Type``. .. index:: @@ -556,7 +556,7 @@ section :tacn:`refine`). This scope is opened by default. Now comes the content of module ``Peano``: .. coqdoc:: - + Theorem eq_S : forall x y:nat, x = y -> S x = S y. Definition pred (n:nat) : nat := match n with @@ -628,7 +628,7 @@ induction principle. .. coqdoc:: Theorem nat_case : - forall (n:nat) (P:nat -> Prop), + forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n. Theorem nat_double_ind : forall R:nat -> nat -> Prop, @@ -640,7 +640,7 @@ induction principle. Well-founded recursion ~~~~~~~~~~~~~~~~~~~~~~ -The basic library contains the basics of well-founded recursion and +The basic library contains the basics of well-founded recursion and well-founded induction, in module ``Wf.v``. .. index:: @@ -669,7 +669,7 @@ well-founded induction, in module ``Wf.v``. forall P:A -> Prop, (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a. -The automatically generated scheme ``Acc_rect`` +The automatically generated scheme ``Acc_rect`` can be used to define functions by fixpoints using well-founded relations to justify termination. Assuming extensionality of the functional used for the recursive call, the @@ -741,7 +741,7 @@ The standard library Survey ~~~~~~ -The rest of the standard library is structured into the following +The rest of the standard library is structured into the following subdirectories: * **Logic** : Classical logic and dependent equality @@ -751,8 +751,8 @@ subdirectories: * **ZArith** : Basic relative integer arithmetic * **Numbers** : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words) * **Bool** : Booleans (basic functions and results) - * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) - * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) + * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) + * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) * **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees) * **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...) * **Floats** : Machine implementation of floating-point arithmetic (for the binary64 format) @@ -903,7 +903,7 @@ tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: discrR :name: discrR - + Proves that two real integer constants are different. .. example:: @@ -931,7 +931,7 @@ tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: split_Rmult :name: split_Rmult - + Splits a condition that a product is non null into subgoals corresponding to the condition on each operand of the product. @@ -963,7 +963,7 @@ List library single: fold_left (term) single: fold_right (term) -Some elementary operations on polymorphic lists are defined here. +Some elementary operations on polymorphic lists are defined here. They can be accessed by requiring module ``List``. It defines the following notions: @@ -1052,9 +1052,9 @@ Notation Interpretation ``_ + _`` ``add`` ``_ * _`` ``mul`` ``_ / _`` ``div`` -``_ == _`` ``eqb`` -``_ < _`` ``ltb`` -``_ <= _`` ``leb`` +``_ =? _`` ``eqb`` +``_ <? _`` ``ltb`` +``_ <=? _`` ``leb`` ``_ ?= _`` ``compare`` =========== ============== diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3b4b80ca21..4eaca8634f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1211,6 +1211,8 @@ The move tactic. :tacn:`revert`, :tacn:`rename`, :tacn:`clear` and :tacn:`pattern` tactics. +.. _the_case_tactic_ssr: + The case tactic ``````````````` @@ -1235,7 +1237,17 @@ The case tactic x = 1 -> y = 2 -> G. - Note also that the case of |SSR| performs :g:`False` elimination, even + The :tacn:`case` can generate the following warning: + + .. warn:: SSReflect: cannot obtain new equations out of ... + + The tactic was run on an equation that cannot generate simpler equations, + for example `x = 1`. + + The warning can be silenced or made fatal by using the :opt:`Warnings` option + and the `spurious-ssr-injection` key. + + Finally the :tacn:`case` tactic of |SSR| performs :g:`False` elimination, even if no branch is generated by this case operation. Hence the tactic :tacn:`case` on a goal of the form :g:`False -> G` will succeed and prove the goal. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 25c4de7389..c5fab0983f 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2227,9 +2227,6 @@ and an explanation of the underlying technique. then :n:`injection @ident` first introduces the hypothesis in the local context using :n:`intros until @ident`. - .. exn:: Not a projectable equality but a discriminable one. - :undocumented: - .. exn:: Nothing to do, it is an equality between convertible terms. :undocumented: @@ -2237,7 +2234,8 @@ and an explanation of the underlying technique. :undocumented: .. exn:: Nothing to inject. - :undocumented: + + This error is given when one side of the equality is not a constructor. .. tacv:: injection @num diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 18149a690a..9e8e5e5fa5 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -425,16 +425,98 @@ Displaying information about notations (corresponding to :token:`ltac_expr` in the documentation). - `vernac` - for :token:`command`\s - The first three of these give the precedence and associativity for each construct. - For example, these lines printed by `Print Grammar tactic` indicates that the `try` construct - is at level 3 and right-associative. `SELF` represents the `tactic_expr` nonterminal - at level 5 (the top level):: - + 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. + + The prefixes `tactic:`, `prim:`, `constr:` appearing in the output are meant to identify + what part of the grammar a nonterminal is from. If you examine nonterminal definitions + in the source code, they are identified only by the name following the colon. + + 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 + source code, edits it and inserts it into the documentation files. While the + edited grammar is equivalent to the original, for readability some nonterminals + have been renamed and others have been eliminated by substituting the nonterminal + definition where the nonterminal was referenced. This command shows the original grammar, + so it won't exactly match the documentation. + + The |Coq| parser is based on Camlp5. The documentation for + `Extensible grammars <http://camlp5.github.io/doc/htmlc/grammars.html>`_ is the + most relevant but it assumes considerable knowledge. Here are the essentials: + + Productions can contain the following elements: + + - nonterminal names - identifiers in the form `[a-zA-Z0-9_]*` + - `"…"` - a literal string that becomes a keyword and cannot be used as an :token:`ident`. + The string doesn't have to be a valid identifier; frequently the string will contain only + punctuation characters. + - `IDENT "…"` - a literal string that has the form of an :token:`ident` + - `OPT element` - optionally include `element` (e.g. a nonterminal, IDENT "…" or "…") + - `LIST1 element` - a list of one or more `element`\s + - `LIST0 element` - an optional list of `element`\s + - `LIST1 element SEP sep` - a list of `element`\s separated by `sep` + - `LIST0 element SEP sep` - an optional list of `element`\s separated by `sep` + - `[ elements1 | elements2 | … ]` - alternatives (either `elements1` or `elements2` or …) + + Nonterminals can have multiple **levels** to specify precedence and associativity + of its productions. This feature of grammars makes it simple to parse input + 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, + which applies to the productions within it, such as the `try` construct:: + + Entry tactic:tactic_expr is + [ "5" RIGHTA + [ tactic:binder_tactic ] + | "4" LEFTA + [ SELF; ";"; tactic:binder_tactic + | SELF; ";"; SELF + | SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ] | "3" RIGHTA [ IDENT "try"; SELF + : + + The interpretation of `SELF` depends on its position in the production and the + associativity of the level: + + - At the beginning of a production, `SELF` means the next level. In the + fragment shown above, the next level for `try` is "2". (This is defined by the order + of appearance in the grammar or output; the levels could just as well be + named "foo" and "bar".) + - In the middle of a production, `SELF` means the top level ("5" in the fragment) + - At the end of a production, `SELF` means the next level within + `LEFTA` levels and the current level within `RIGHTA` levels. + + `NEXT` always means the next level. `nonterminal LEVEL "…"` is a reference to the specified level + for `nonterminal`. + + `Associativity <http://camlp5.github.io/doc/htmlc/grammars.html#b:Associativity>`_ + explains `SELF` and `NEXT` in somewhat more detail. + + 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 + here is defined by a :cmd:`Reserved Notation` command in `Notations.v`:: + + | "50" LEFTA + [ SELF; "||"; NEXT + + Similarly, `Print Grammar tactic` includes :cmd:`Tactic Notation`\s, such as :tacn:`dintuition`. + + The file + `doc/tools/docgram/fullGrammar <http://github.com/coq/coq/blob/master/doc/tools/docgram/fullGrammar>`_ + in the source tree extracts the full grammar for + |Coq| (not including notations and tactic notations defined in `*.v` files nor some optionally-loaded plugins) + in a single file with minor changes to handle nonterminals using multiple levels (described in + `doc/tools/docgram/README.md <http://github.com/coq/coq/blob/master/doc/tools/docgram/README.md>`_). + This is complete and much easier to read than the grammar source files. + `doc/tools/docgram/orderedGrammar <http://github.com/coq/coq/blob/master/doc/tools/docgram/orderedGrammar>`_ + has the edited grammar that's used in the documentation. - Note that the productions printed by this command are represented in the form used by - |Coq|'s parser (coqpp), which differs from how productions are shown in the documentation. + Developer documentation for parsing is in + `dev/doc/parsing.md <http://github.com/coq/coq/blob/master/dev/doc/parsing.md>`_. .. _locating-notations: @@ -872,7 +954,7 @@ where ``x`` is any expression parsed in entry the given rule) and ``y`` is any expression parsed in entry ``expr`` at level strictly less than ``2``. -Rules associated to an entry can refer different sub-entries. The +Rules associated with an entry can refer different sub-entries. The grammar entry name ``constr`` can be used to refer to the main grammar of term as in the rule @@ -958,7 +1040,7 @@ up to the insertion of a pair of curly brackets. .. cmd:: Print Custom Grammar @ident :name: Print Custom Grammar - This displays the state of the grammar for terms associated to + This displays the state of the grammar for terms associated with the custom entry :token:`ident`. .. _NotationSyntax: |