diff options
Diffstat (limited to 'doc/sphinx/language/core')
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/language/core/coinductive.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/language/core/index.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 24 | ||||
| -rw-r--r-- | doc/sphinx/language/core/modules.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/language/core/primitive.rst | 28 | ||||
| -rw-r--r-- | doc/sphinx/language/core/records.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/language/core/sections.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/variants.rst | 1 |
11 files changed, 82 insertions, 56 deletions
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 41e1c30f0d..a38282d41a 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -117,7 +117,7 @@ Assumptions Assumptions extend the environment with axioms, parameters, hypotheses or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted -by Coq if and only if this :n:`@type` is a correct type in the environment +by |Coq| if and only if this :n:`@type` is a correct type in the environment preexisting the declaration and if :n:`@ident` was not previously defined in the same module. This :n:`@type` is considered to be the type (or specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident` @@ -141,8 +141,8 @@ has type :n:`@type`. of_type ::= {| : | :> } @type These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in - the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence - of an object of this type) is accepted as a postulate. + the global context. The fact asserted by :n:`@type` (or, equivalently, the existence + of an object of this type) is accepted as a postulate. They accept the :attr:`program` attribute. :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms are equivalent. They can take the :attr:`local` :term:`attribute`, @@ -155,6 +155,10 @@ has type :n:`@type`. is closed, the :n:`@ident`\(s) become undefined and every object depending on them will be explicitly parameterized (i.e., the variables are *discharged*). See Section :ref:`section-mechanism`. + :n:`:>` + If specified, :token:`ident_decl` is automatically + declared as a coercion to the class of its type. See :ref:`coercions`. + The :n:`Inline` clause is only relevant inside functors. See :cmd:`Module`. .. example:: Simple assumptions diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 45bdc019ac..29a2b40162 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -134,7 +134,7 @@ Numbers hexdigit ::= {| 0 .. 9 | a .. f | A .. F } :n:`@integer` and :n:`@natural` are limited to the range that fits - into an OCaml integer (63-bit integers on most architectures). + into an |OCaml| integer (63-bit integers on most architectures). :n:`@bigint` and :n:`@bignat` have no range limitation. The :ref:`standard library <thecoqlibrary>` provides some @@ -152,8 +152,8 @@ Strings :token:`string`. Keywords - The following character sequences are keywords defined in the main Coq grammar - that cannot be used as identifiers (even when starting Coq with the `-noinit` + The following character sequences are keywords defined in the main |Coq| grammar + that cannot be used as identifiers (even when starting |Coq| with the `-noinit` command-line flag):: _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop @@ -168,11 +168,11 @@ Keywords keywords. Other tokens - The following character sequences are tokens defined in the main Coq grammar - (even when starting Coq with the `-noinit` command-line flag):: + The following character sequences are tokens defined in the main |Coq| grammar + (even when starting |Coq| with the `-noinit` command-line flag):: ! #[ % & ' ( () ) * + , - -> - . .( .. ... / : ::= := :> :>> ; < <+ <- <: + . .( .. ... / : ::= := :> ; < <+ <- <: <<: <= = => > >-> >= ? @ @{ [ ] _ `( `{ { {| | } @@ -325,10 +325,10 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types boldface label "Command:". Commands are listed in the :ref:`command_index`. Example: - .. cmd:: Comments {* @string } + .. cmd:: Comments {* {| @one_term | @string | @natural } } - This command prints "Comments ok" and does not change anything - to the state of the document. + Prints "Comments ok" and does not change + the state of the document. tactic diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index c034b7f302..2e5dff42ac 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -28,8 +28,8 @@ More information on co-inductive definitions can be found in This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, :attr:`universes(template)`, :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(noncumulative)`, :attr:`private(matching)` + and :attr:`using` attributes. .. example:: @@ -76,7 +76,7 @@ propositional η-equality, which itself would require full η-conversion for subject reduction to hold, but full η-conversion is not acceptable as it would make type checking undecidable. -Since the introduction of primitive records in Coq 8.5, an alternative +Since the introduction of primitive records in |Coq| 8.5, an alternative presentation is available, called *negative co-inductive types*. This consists in defining a co-inductive type as a primitive record type through its projections. Such a technique is akin to the *co-pattern* style that can be @@ -115,7 +115,7 @@ equality: Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2. -As of Coq 8.9, it is now advised to use negative co-inductive types rather than +As of |Coq| 8.9, it is now advised to use negative co-inductive types rather than their positive counterparts. .. seealso:: @@ -195,7 +195,7 @@ Top-level definitions of co-recursive functions As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously defining several mutual cofixpoints. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 42203d9d65..1681eee6e7 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -87,10 +87,10 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`program` and - :attr:`canonical` attributes. + :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`), + :attr:`canonical` and :attr:`using` attributes. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. @@ -135,11 +135,13 @@ Chapter :ref:`Tactics`. The basic assertion command is: | Proposition | Property - After the statement is asserted, Coq needs a proof. Once a proof of + After the statement is asserted, |Coq| needs a proof. Once a proof of :n:`@type` under the assumptions represented by :n:`@binder`\s is given and validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and the theorem is bound to the name :n:`@ident` in the environment. + These commands accept the :attr:`program` attribute. See :ref:`program_lemma`. + Forms using the :n:`with` clause are useful for theorems that are proved by simultaneous induction over a mutually inductive assumption, or that assert mutually dependent statements in some mutual co-inductive type. It is equivalent to @@ -157,6 +159,8 @@ Chapter :ref:`Tactics`. The basic assertion command is: correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. + This command accepts the :attr:`using` attribute. + .. exn:: The term @term has type @type which should be Set, Prop or Type. :undocumented: @@ -172,7 +176,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: This feature, called nested proofs, is disabled by default. To activate it, turn the :flag:`Nested Proofs Allowed` flag on. -Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode +Proofs start with the keyword :cmd:`Proof`. Then |Coq| enters the proof editing mode until the proof is completed. In proof editing mode, the user primarily enters tactics, which are described in chapter :ref:`Tactics`. The user may also enter commands to manage the proof editing mode. They are described in Chapter diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst index de780db267..c7b1df28db 100644 --- a/doc/sphinx/language/core/index.rst +++ b/doc/sphinx/language/core/index.rst @@ -4,7 +4,7 @@ Core language ============= -At the heart of the Coq proof assistant is the Coq kernel. While +At the heart of the |Coq| proof assistant is the |Coq| kernel. While users have access to a language with many convenient features such as :ref:`notations <syntax-extensions-and-notation-scopes>`, :ref:`implicit arguments <ImplicitArguments>`, etc. (presented in the diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 39b154de8d..1642482bb1 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -17,7 +17,7 @@ Inductive types constructor ::= @ident {* @binder } {? @of_type } This command defines one or more - inductive types and its constructors. Coq generates destructors + inductive types and its constructors. |Coq| generates destructors depending on the universe that the inductive type belongs to. The destructors are named :n:`@ident`\ ``_rect``, :n:`@ident`\ ``_ind``, @@ -342,9 +342,9 @@ Recursive functions: fix .. insertprodn term_fix fixannot .. prodn:: - term_fix ::= let fix @fix_body in @term - | fix @fix_body {? {+ with @fix_body } for @ident } - fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term + term_fix ::= let fix @fix_decl in @term + | fix @fix_decl {? {+ with @fix_decl } for @ident } + fix_decl ::= @ident {* @binder } {? @fixannot } {? : @type } := @term fixannot ::= %{ struct @ident %} | %{ wf @one_term @ident %} | %{ measure @one_term {? @ident } {? @one_term } %} @@ -361,7 +361,11 @@ syntax: :n:`let fix @ident {* @binder } := @term in` stands for Some options of :n:`@fixannot` are only supported in specific constructs. :n:`fix` and :n:`let fix` only support the :n:`struct` option, while :n:`wf` and :n:`measure` are only supported in -commands such as :cmd:`Function` and :cmd:`Program Fixpoint`. +commands such as :cmd:`Fixpoint` (with the :attr:`program` attribute) and :cmd:`Function`. + +.. todo explanation of struct: see text above at the Fixpoint command, also + see https://github.com/coq/coq/pull/12936#discussion_r510716268 and above. + Consider whether to move the grammar for fixannot elsewhere .. _Fixpoint: @@ -379,7 +383,7 @@ constructions. .. prodn:: fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations } - This command allows defining functions by pattern matching over inductive + Allows defining functions by pattern matching over inductive objects using a fixed point construction. The meaning of this declaration is to define :n:`@ident` as a recursive function with arguments specified by the :n:`@binder`\s such that :n:`@ident` applied to arguments @@ -388,6 +392,8 @@ constructions. consequently :n:`forall {* @binder }, @type` and its value is equivalent to :n:`fun {* @binder } => @term`. + This command accepts the :attr:`program` attribute. + To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical constraints on a special argument called the decreasing argument. They are needed to ensure that the :cmd:`Fixpoint` definition always terminates. @@ -399,17 +405,19 @@ constructions. that satisfies the decreasing condition. :cmd:`Fixpoint` without the :attr:`program` attribute does not support the - :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. + :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. See :ref:`program_fixpoint`. The :n:`with` clause allows simultaneously defining several mutual fixpoints. It is especially useful when defining functions over mutually defined inductive types. Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. + This command accepts the :attr:`using` attribute. + .. note:: + Some fixpoints may have several arguments that fit as decreasing diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 866104d5d1..1309a47ff4 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -1001,12 +1001,12 @@ of the ``Require`` command can be used to bypass the implicit shortening by providing an absolute root to the required file (see :ref:`compiled-files`). There also exists another independent loadpath mechanism attached to -OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object -files as described above. The OCaml loadpath is managed using -the option ``-I`` `path` (in the OCaml world, there is neither a +|OCaml| object files (``.cmo`` or ``.cmxs``) rather than |Coq| object +files as described above. The |OCaml| loadpath is managed using +the option ``-I`` `path` (in the |OCaml| world, there is neither a notion of logical name prefix nor a way to access files in subdirectories of path). See the command :cmd:`Declare ML Module` in -:ref:`compiled-files` to understand the need of the OCaml loadpath. +:ref:`compiled-files` to understand the need of the |OCaml| loadpath. See :ref:`command-line-options` for a more general view over the |Coq| command line options. diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst index 48647deeff..17f569ca2a 100644 --- a/doc/sphinx/language/core/primitive.rst +++ b/doc/sphinx/language/core/primitive.rst @@ -45,13 +45,13 @@ applications of these primitive operations. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63` -module can be used when extracting to OCaml: it maps the Coq primitives to types -and functions of a :g:`Uint63` module. Said OCaml module is not produced by +module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types +and functions of a :g:`Uint63` module. That |OCaml| module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of Coq. +can be taken from the kernel of |Coq|. -Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values +Literal values (at type :g:`Int63.int`) are extracted to literal |OCaml| values wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on 64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the function :g:`Uint63.compile` from the kernel). @@ -94,13 +94,13 @@ to comply with the IEEE 754 standard for floating-point arithmetic. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlFloats` -module can be used when extracting to OCaml: it maps the Coq primitives to types -and functions of a :g:`Float64` module. Said OCaml module is not produced by +module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types +and functions of a :g:`Float64` module. Said |OCaml| module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of Coq. +can be taken from the kernel of |Coq|. -Literal values (of type :g:`Float64.t`) are extracted to literal OCaml +Literal values (of type :g:`Float64.t`) are extracted to literal |OCaml| values (of type :g:`float`) written in hexadecimal notation and wrapped into the :g:`Float64.of_float` constructor, e.g.: :g:`Float64.of_float (0x1p+0)`. @@ -144,19 +144,19 @@ operations. The extraction of these primitives can be customized similarly to the extraction of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlPArray` -module can be used when extracting to OCaml: it maps the Coq primitives to types -and functions of a :g:`Parray` module. Said OCaml module is not produced by +module can be used when extracting to |OCaml|: it maps the |Coq| primitives to types +and functions of a :g:`Parray` module. Said |OCaml| module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module -can be taken from the kernel of Coq (see ``kernel/parray.ml``). +can be taken from the kernel of |Coq| (see ``kernel/parray.ml``). -Coq's primitive arrays are persistent data structures. Semantically, a set operation +|Coq|'s primitive arrays are persistent data structures. Semantically, a set operation ``t.[i <- a]`` represents a new array that has the same values as ``t``, except at position ``i`` where its value is ``a``. The array ``t`` still exists, can still be used and its values were not modified. Operationally, the implementation -of Coq's primitive arrays is optimized so that the new array ``t.[i <- a]`` does not +of |Coq|'s primitive arrays is optimized so that the new array ``t.[i <- a]`` does not copy all of ``t``. The details are in section 2.3 of :cite:`ConchonFilliatre07wml`. -In short, the implementation keeps one version of ``t`` as an OCaml native array and +In short, the implementation keeps one version of ``t`` as an |OCaml| native array and other versions as lists of modifications to ``t``. Accesses to the native array version are constant time operations. However, accesses to versions where all the cells of the array are modified have O(n) access time, the same as a list. The version that is kept as the native array diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index b2099b8636..e6df3ee9f5 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -18,7 +18,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. insertprodn record_definition field_def .. prodn:: - record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } {? ; } %} {? @decl_notations } + record_definition ::= {? > } @ident_decl {* @binder } {? : @sort } {? := {? @ident } %{ {*; @record_field } {? ; } %} } record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations } field_body ::= {* @binder } @of_type | {* @binder } @of_type := @term @@ -26,19 +26,28 @@ expressions. In this sense, the :cmd:`Record` construction allows defining term_record ::= %{%| {*; @field_def } {? ; } %|%} field_def ::= @qualid {* @binder } := @term - Each :n:`@record_definition` defines a record named by :n:`@ident_decl`. The constructor name is given by :n:`@ident`. If the constructor name is not specified, then the default name :n:`Build_@ident` is used, where :n:`@ident` is the record name. - If :n:`@type` is - omitted, the default type is :math:`\Type`. The identifiers inside the brackets are the field names. - The type of each field :n:`@ident` is :n:`forall {* @binder }, @type`. + If :token:`sort` is omitted, the default sort is Type. Notice that the type of an identifier can depend on a previously-given identifier. Thus the order of the fields is important. :n:`@binder` parameters may be applied to the record as a whole or to individual fields. + .. todo + "Record foo2:Prop := { a }." gives the error "Cannot infer this placeholder of type "Type", + while "Record foo2:Prop := { a:Type }." gives the output "foo2 is defined. + a cannot be defined because it is informative and foo2 is not." + Your thoughts? + + :n:`{? > }` + If provided, the constructor name is automatically declared as + a coercion from the class of the last field type to the record name + (this may fail if the uniform inheritance condition is not + satisfied). See :ref:`coercions`. + Notations can be attached to fields using the :n:`@decl_notations` annotation. :cmd:`Record` and :cmd:`Structure` are synonyms. @@ -76,7 +85,7 @@ Let us now see the work done by the ``Record`` macro. First the macro generates a variant type definition with just one constructor: :n:`Variant @ident {* @binder } : @sort := @ident__0 {* @binder }`. -To build an object of type :token:`ident`, one should provide the constructor +To build an object of type :token:`ident`, provide the constructor :n:`@ident__0` with the appropriate number of terms filling the fields of the record. .. example:: diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index df50dbafe3..c70f7a347b 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -84,7 +84,7 @@ Sections create local contexts which can be shared across multiple definitions. will be wrapped with a :n:`@term_let` with the same declaration. As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, - if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + if :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index 2904250e41..645986be9c 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -29,6 +29,7 @@ Private (matching) inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. attr:: private(matching) + :name: private(matching); Private This attribute can be used to forbid the use of the :g:`match` construct on objects of this inductive type outside of the module |