diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 9 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 29 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 67 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 136 |
7 files changed, 147 insertions, 109 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 15f42591ce..8ec51e45ba 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -5,8 +5,6 @@ Extended pattern matching :Authors: Cristina Cornes and Hugo Herbelin -.. TODO links to figures - This section describes the full form of pattern matching in |Coq| terms. .. |rhs| replace:: right hand sides @@ -14,7 +12,7 @@ This section describes the full form of pattern matching in |Coq| terms. Patterns -------- -The full syntax of match is presented in Figures 1.1 and 1.2. +The full syntax of :g:`match` is presented in section :ref:`term`. Identifiers in patterns are either constructor names or variables. Any identifier that is not the constructor of an inductive or co-inductive type is considered to be a variable. A variable name cannot occur more @@ -496,9 +494,8 @@ We can use multiple patterns to write the proof of the lemma In the example of :g:`dec`, the first match is dependent while the second is not. -The user can also use match in combination with the tactic :tacn:`refine` (see -Section 8.2.3) to build incomplete proofs beginning with a match -construction. +The user can also use match in combination with the tactic :tacn:`refine` +to build incomplete proofs beginning with a :g:`match` construction. Pattern-matching on inductive objects involving local definitions diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index d909f98956..41b726b069 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,7 +1,7 @@ .. _extraction: -Extraction of programs in |OCaml| and Haskell -============================================= +Program extraction +================== :Authors: Jean-Christophe Filliâtre and Pierre Letouzey diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index db8c09d88f..0e8660cb0e 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,10 +1,5 @@ -.. _miscellaneousextensions: - -Miscellaneous extensions -======================== - Program derivation ------------------- +================== |Coq| comes with an extension called ``Derive``, which supports program derivation. Typically in the style of Bird and Meertens or derivations diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 549249d25c..5cffe9e435 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -98,10 +98,17 @@ coercions. .. flag:: Program Mode Enables the program mode, in which 1) typechecking allows subset coercions and - 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and - :cmd:`Program Definition` act - like Program Fixpoint/Definition, generating obligations if there are - unresolved holes after typechecking. + 2) the elaboration of pattern matching of :cmd:`Fixpoint` and + :cmd:`Definition` act as if the :attr:`program` attribute had been + used, generating obligations if there are unresolved holes after + typechecking. + +.. attr:: program + + This attribute allows to use the Program mode on a specific + definition. An alternative syntax is to use the legacy ``Program`` + prefix (cf. :n:`@legacy_attr`) as documented in the rest of this + chapter. .. _syntactic_control: @@ -155,7 +162,7 @@ Program Definition This command types the value term in Russell and generates proof obligations. Once solved using the commands shown below, it binds the - final |Coq| term to the name ``ident`` in the environment. + final |Coq| term to the name :n:`@ident` in the environment. .. exn:: @ident already exists. :name: @ident already exists. (Program Definition) @@ -163,12 +170,12 @@ Program Definition .. cmdv:: Program Definition @ident : @type := @term - It interprets the type ``type``, potentially generating proof + It interprets the type :n:`@type`, potentially generating proof obligations to be resolved. Once done with them, we have a |Coq| - type |type_0|. It then elaborates the preterm ``term`` into a |Coq| - term |term_0|, checking that the type of |term_0| is coercible to - |type_0|, and registers ``ident`` as being of type |type_0| once the - set of obligations generated during the interpretation of |term_0| + type :n:`@type__0`. It then elaborates the preterm :n:`@term` into a |Coq| + term :n:`@term__0`, checking that the type of :n:`@term__0` is coercible to + :n:`@type__0`, and registers :n:`@ident` as being of type :n:`@type__0` once the + set of obligations generated during the interpretation of :n:`@term__0` and the aforementioned coercion derivation are solved. .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ... @@ -178,7 +185,7 @@ Program Definition This is equivalent to: - :g:`Program Definition ident : forall binders, type := fun binders => term`. + :n:`Program Definition @ident : forall {* @binder }, @type := fun {* @binder } => @term`. .. TODO refer to production in alias diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 76174e32b5..2a321b5cbf 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -1,8 +1,12 @@ +.. |bdi| replace:: :math:`\beta\delta\iota` .. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}` .. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}` .. |eq| replace:: `=`:sub:`(by the main correctness theorem)` .. |re| replace:: ``(PEeval`` `v` `ap`\ ``)`` .. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))`` +.. |N| replace:: ``N`` +.. |nat| replace:: ``nat`` +.. |Z| replace:: ``Z`` .. _theringandfieldtacticfamilies: diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index af4e9051bb..bd4c276571 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -47,7 +47,7 @@ Leibniz equality on some type. An example implementation is: | tt, tt => eq_refl tt end }. -Using the attribute ``refine``, if the term is not sufficient to +Using the :attr:`refine` attribute, if the term is not sufficient to finish the definition (e.g. due to a missing field or non-inferable hole) it must be finished in proof mode. If it is sufficient a trivial proof mode with no open goals is started. @@ -77,9 +77,9 @@ remaining fields, e.g.: Defined. One has to take care that the transparency of every field is -determined by the transparency of the :cmd:`Instance` proof. One can use -alternatively the :cmd:`Program Instance` variant which has richer facilities -for dealing with obligations. +determined by the transparency of the :cmd:`Instance` proof. One can +use alternatively the :attr:`program` attribute to get richer +facilities for dealing with obligations. Binding classes @@ -174,7 +174,7 @@ For example: .. coqtop:: in - Global Program Instance option_eqb : EqDec (option A) := + #[ global, program ] Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true @@ -188,7 +188,7 @@ For example: About option_eqb. -Here the :cmd:`Global` modifier redeclares the instance at the end of the +Here the :attr:`global` attribute redeclares the instance at the end of the section, once it has been generalized by the context variables it uses. @@ -300,9 +300,11 @@ Summary of the commands The :cmd:`Class` command is used to declare a typeclass with parameters :token:`binders` and fields the declared record fields. - This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, + Like any command declaring a record, this command supports the + :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`Cumulative`, :attr:`NonCumulative` and :attr:`Private` attributes. + :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`private(matching)` attributes. .. _singleton-class: @@ -341,6 +343,25 @@ Summary of the commands :tacn:`auto` hints. If the priority :token:`num` is not specified, it defaults to the number of non-dependent binders of the instance. + This command supports the :attr:`global` attribute that can be + used on instances declared in a section so that their + generalization is automatically redeclared after the section is + closed. + + Like :cmd:`Definition`, it also supports the :attr:`program` + attribute to switch the type checking to `Program` (chapter + :ref:`programs`) and use the obligation mechanism to manage missing + fields. + + Finally, it supports the lighter :attr:`refine` attribute: + + .. attr:: refine + + This attribute can be used to leave holes or not provide all + fields in the definition of an instance and open the tactic mode + to fill them. It works exactly as if no body had been given and + the :tacn:`refine` tactic has been used first. + .. cmdv:: Instance @ident {* @binder } : forall {* @binder }, @term__0 {+ @term} {? | @num } := @term This syntax is used for declaration of singleton class instances or @@ -348,19 +369,6 @@ Summary of the commands {+ @term}`. One need not even mention the unique field name for singleton classes. - .. cmdv:: Global Instance - :name: Global Instance - - One can use the :cmd:`Global` modifier on instances declared in a - section so that their generalization is automatically redeclared - after the section is closed. - - .. cmdv:: Program Instance - :name: Program Instance - - Switches the type checking to `Program` (chapter :ref:`programs`) and - uses the obligation mechanism to manage missing fields. - .. cmdv:: Declare Instance :name: Declare Instance @@ -385,8 +393,10 @@ few other commands related to typeclasses. .. tacn:: typeclasses eauto :name: typeclasses eauto - This tactic uses a different resolution engine than :tacn:`eauto` and - :tacn:`auto`. The main differences are the following: + This proof search tactic implements the resolution engine that is run + implicitly during type-checking. This tactic uses a different resolution + engine than :tacn:`eauto` and :tacn:`auto`. The main differences are the + following: + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in the new proof engine (as of Coq 8.6), meaning that backtracking is @@ -422,6 +432,17 @@ few other commands related to typeclasses. resolution with the local hypotheses use full conversion during unification. + + The mode hints (see :cmd:`Hint Mode`) associated to a class are + taken into account by :tacn:`typeclasses eauto`. When a goal + does not match any of the declared modes for its head (if any), + instead of failing like :tacn:`eauto`, the goal is suspended and + resolution proceeds on the remaining goals. + If after one run of resolution, there remains suspended goals, + resolution is launched against on them, until it reaches a fixed + point when the set of remaining suspended goals does not change. + Using `solve [typeclasses eauto]` can be used to ensure that + no suspended goals remain. + + When considering local hypotheses, we use the union of all the modes declared in the given databases. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 0e326f45d2..a08495badd 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -122,62 +122,92 @@ in a universe strictly higher than :g:`Set`. Polymorphic, Monomorphic ------------------------- -.. cmd:: Polymorphic @definition +.. attr:: universes(polymorphic) - As shown in the examples, polymorphic definitions and inductives can be - declared using the ``Polymorphic`` prefix. + This attribute can be used to declare universe polymorphic + definitions and inductive types. There is also a legacy syntax + using the ``Polymorphic`` prefix (see :n:`@legacy_attr`) which, as + shown in the examples, is more commonly used. .. flag:: Universe Polymorphism - Once enabled, this flag will implicitly prepend ``Polymorphic`` to any - definition of the user. + This flag is off by default. When it is on, new declarations are + polymorphic unless the :attr:`universes(monomorphic)` attribute is + used. -.. cmd:: Monomorphic @definition +.. attr:: universes(monomorphic) - When the :flag:`Universe Polymorphism` flag is set, to make a definition - producing global universe constraints, one can use the ``Monomorphic`` prefix. + This attribute can be used to declare universe monomorphic + definitions and inductive types (i.e. global universe constraints + are produced), even when the :flag:`Universe Polymorphism` flag is + on. There is also a legacy syntax using the ``Monomorphic`` prefix + (see :n:`@legacy_attr`). -Many other commands support the ``Polymorphic`` flag, including: +Many other commands can be used to declare universe polymorphic or +monomorphic constants depending on whether the :flag:`Universe +Polymorphism` flag is on or the :attr:`universes(polymorphic)` or +:attr:`universes(monomorphic)` attributes are used: -.. TODO add links on each of these? +- :cmd:`Lemma`, :cmd:`Axiom`, etc. can be used to declare universe + polymorphic constants. -- ``Lemma``, ``Axiom``, and all the other “definition” keywords support - polymorphism. +- Using the :attr:`universes(polymorphic)` attribute with the + :cmd:`Section` command will locally set the polymorphism flag inside + the section. -- :cmd:`Section` will locally set the polymorphism flag inside the section. +- :cmd:`Variable`, :cmd:`Context`, :cmd:`Universe` and + :cmd:`Constraint` in a section support polymorphism. See + :ref:`universe-polymorphism-in-sections` for more details. -- ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support - polymorphism. See :ref:`universe-polymorphism-in-sections` for more details. - -- :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint - polymorphically, not at a single instance. +- Using the :attr:`universes(polymorphic)` attribute with the + :cmd:`Hint Resolve` or :cmd:`Hint Rewrite` commands will make + :tacn:`auto` / :tacn:`rewrite` use the hint polymorphically, not at + a single instance. .. _cumulative: Cumulative, NonCumulative ------------------------- -Polymorphic inductive types, coinductive types, variants and records can be -declared cumulative using the :g:`Cumulative` prefix. +.. attr:: universes(cumulative) + + Polymorphic inductive types, coinductive types, variants and + records can be declared cumulative using this attribute or the + legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as + shown in the examples, is more commonly used. -.. cmd:: Cumulative @inductive + This means that two instances of the same inductive type (family) + are convertible based on the universe variances; they do not need + to be equal. - Declares the inductive as cumulative + .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. -Alternatively, there is a :flag:`Polymorphic Inductive -Cumulativity` flag which when set, makes all subsequent *polymorphic* -inductive definitions cumulative. When set, inductive types and the -like can be enforced to be non-cumulative using the :g:`NonCumulative` -prefix. + Using this attribute requires being in a polymorphic context, + i.e. either having the :flag:`Universe Polymorphism` flag on, or + having used the :attr:`universes(polymorphic)` attribute as + well. -.. cmd:: NonCumulative @inductive + .. note:: - Declares the inductive as non-cumulative + ``#[ universes(polymorphic), universes(cumulative) ]`` can be + abbreviated into ``#[ universes(polymorphic, cumulative) ]``. .. flag:: Polymorphic Inductive Cumulativity - When this flag is on, it sets all following polymorphic inductive - types as cumulative (it is off by default). + When this flag is on (it is off by default), it makes all + subsequent *polymorphic* inductive definitions cumulative, unless + the :attr:`universes(noncumulative)` attribute is used. It has no + effect on *monomorphic* inductive definitions. + +.. attr:: universes(noncumulative) + + Declares the inductive type as non-cumulative even if the + :flag:`Polymorphic Inductive Cumulativity` flag is on. There is + also a legacy syntax using the ``NonCumulative`` prefix (see + :n:`@legacy_attr`). + + This means that two instances of the same inductive type (family) + are convertible only if all the universes are equal. Consider the examples below. @@ -220,34 +250,10 @@ The following is an example of a record with non-trivial subtyping relation: E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j -Cumulative inductive types, coinductive types, variants and records -only make sense when they are universe polymorphic. Therefore, an -error is issued whenever the user uses the :g:`Cumulative` or -:g:`NonCumulative` prefix in a monomorphic context. -Notice that this is not the case for the :flag:`Polymorphic Inductive Cumulativity` flag. -That is, this flag, when set, makes all subsequent *polymorphic* -inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used) -but has no effect on *monomorphic* inductive declarations. - -Consider the following examples. - -.. coqtop:: all reset - - Fail Monomorphic Cumulative Inductive Unit := unit. - -.. coqtop:: all reset - - Fail Monomorphic NonCumulative Inductive Unit := unit. - -.. coqtop:: all reset - - Set Polymorphic Inductive Cumulativity. - Inductive Unit := unit. - An example of a proof using cumulativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. coqtop:: in +.. coqtop:: in reset Set Universe Polymorphism. Set Polymorphic Inductive Cumulativity. @@ -368,10 +374,14 @@ to universes and explicitly instantiate polymorphic definitions. In the monorphic case, this command declares a new global universe named :g:`ident`, which can be referred to using its qualified name as well. Global universe names live in a separate namespace. The - command supports the ``Polymorphic`` flag only in sections, meaning the - universe quantification will be discharged on each section definition + command supports the :attr:`universes(polymorphic)` attribute (or + the ``Polymorphic`` prefix) only in sections, meaning the universe + quantification will be discharged on each section definition independently. + .. exn:: Polymorphic universes can only be declared inside sections, use Monomorphic Universe instead. + :undocumented: + .. cmd:: Constraint @univ_constraint Polymorphic Constraint @univ_constraint @@ -379,9 +389,10 @@ to universes and explicitly instantiate polymorphic definitions. If consistent, the constraint is then enforced in the global environment. Like :cmd:`Universe`, it can be used with the - ``Polymorphic`` prefix in sections only to declare constraints - discharged at section closing time. One cannot declare a global - constraint on polymorphic universes. + :attr:`universes(polymorphic)` attribute (or the ``Polymorphic`` + prefix) in sections only to declare constraints discharged at + section closing time. One cannot declare a global constraint on + polymorphic universes. .. exn:: Undeclared universe @ident. :undocumented: @@ -389,6 +400,9 @@ to universes and explicitly instantiate polymorphic definitions. .. exn:: Universe inconsistency. :undocumented: + .. exn:: Polymorphic universe constraints can only be declared inside sections, use Monomorphic Constraint instead + :undocumented: + Polymorphic definitions ~~~~~~~~~~~~~~~~~~~~~~~ |