diff options
Diffstat (limited to 'doc/sphinx/addendum/type-classes.rst')
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 380 |
1 files changed, 176 insertions, 204 deletions
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 5518da9ac..6c7258f9c 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -68,8 +68,8 @@ the remaining fields, e.g.: Defined. One has to take care that the transparency of every field is -determined by the transparency of the ``Instance`` proof. One can use -alternatively the ``Program Instance`` variant which has richer facilities +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. @@ -148,11 +148,10 @@ database. Sections and contexts --------------------- -To ease the parametrization of developments by type classes, we -provide a new way to introduce variables into section contexts, -compatible with the implicit argument mechanism. The new command works -similarly to the ``Variables`` vernacular (:ref:`TODO-1.3.2-Definitions`), except it -accepts any binding context as argument. For example: +To ease the parametrization of developments by type classes, we provide a new +way to introduce variables into section contexts, compatible with the implicit +argument mechanism. The new command works similarly to the :cmd:`Variables` +vernacular, except it accepts any binding context as argument. For example: .. coqtop:: all @@ -270,12 +269,9 @@ the Existing Instance command to achieve the same effect. Summary of the commands ----------------------- +.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } } -.. _Class: - -.. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } }. - - The ``Class`` command is used to declare a type class with parameters + The :cmd:`Class` command is used to declare a type class with parameters ``binders`` and fields the declared record fields. Variants: @@ -300,12 +296,10 @@ Variants: This variant declares a class a posteriori from a constant or inductive definition. No methods or instances are defined. -.. _Instance: - .. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } -The ``Instance`` command is used to declare a type class instance named -``ident`` of the class ``Class`` with parameters ``t1`` to ``tn`` and +The :cmd:`Instance` command is used to declare a type class instance named +``ident`` of the class :cmd:`Class` with parameters ``t1`` to ``tn`` and fields ``b1`` to ``bi``, where each field must be a declared field of the class. Missing fields must be filled in interactive proof mode. @@ -315,233 +309,235 @@ optional priority can be declared, 0 being the highest priority as for auto hints. If the priority is not specified, it defaults to the number of non-dependent binders of the instance. -Variants: - - -.. cmd:: Instance ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term +.. cmdv:: Instance @ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term This syntax is used for declaration of singleton class instances or for directly giving an explicit term of type ``forall binders, Class t1 … tn``. One need not even mention the unique field name for singleton classes. -.. cmd:: Global Instance +.. cmdv:: Global Instance One can use the ``Global`` modifier on instances declared in a section so that their generalization is automatically redeclared after the section is closed. -.. cmd:: Program Instance +.. cmdv:: Program Instance + :name: Program Instance - Switches the type-checking to Program (chapter :ref:`program`) and + Switches the type-checking to Program (chapter :ref:`programs`) and uses the obligation mechanism to manage missing fields. -.. cmd:: Declare Instance +.. cmdv:: Declare Instance + :name: Declare Instance In a Module Type, this command states that a corresponding concrete - instance should exist in any implementation of thisModule Type. This - is similar to the distinction betweenParameter vs. Definition, or - between Declare Module and Module. + instance should exist in any implementation of this Module Type. This + is similar to the distinction between :cmd:`Parameter` vs. :cmd:`Definition`, or + between :cmd:`Declare Module` and :cmd:`Module`. -Besides the ``Class`` and ``Instance`` vernacular commands, there are a +Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a few other commands related to type classes. -.. _ExistingInstance: - -Existing Instance -~~~~~~~~~~~~~~~~~ - .. cmd:: Existing Instance {+ @ident} [| priority] -This commands adds an arbitrary list of constants whose type ends with -an applied type class to the instance database with an optional -priority. It can be used for redeclaring instances at the end of -sections, or declaring structure projections as instances. This is -equivalent to ``Hint Resolve ident : typeclass_instances``, except it -registers instances for ``Print Instances``. - -.. _Context: - -Context -~~~~~~~ + This commands adds an arbitrary list of constants whose type ends with + an applied type class to the instance database with an optional + priority. It can be used for redeclaring instances at the end of + sections, or declaring structure projections as instances. This is + equivalent to ``Hint Resolve ident : typeclass_instances``, except it + registers instances for :cmd:`Print Instances`. .. cmd:: Context @binders -Declares variables according to the given binding context, which might -use :ref:`implicit-generalization`. - + Declares variables according to the given binding context, which might + use :ref:`implicit-generalization`. + +.. 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: + + + 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 + available among dependent subgoals, and shelving goals is supported. + typeclasses eauto is a multi-goal tactic. It analyses the dependencies + between subgoals to avoid backtracking on subgoals that are entirely + independent. + + + When called with no arguments, typeclasses eauto uses + the ``typeclass_instances`` database by default (instead of core). + Dependent subgoals are automatically shelved, and shelved goals can + remain after resolution ends (following the behavior of Coq 8.5). + + .. note:: + As of Coq 8.6, ``all:once (typeclasses eauto)`` faithfully + mimicks what happens during typeclass resolution when it is called + during refinement/type-inference, except that *only* declared class + subgoals are considered at the start of resolution during type + inference, while ``all`` can select non-class subgoals as well. It might + move to ``all:typeclasses eauto`` in future versions when the + refinement engine will be able to backtrack. + + + When called with specific databases (e.g. with), typeclasses eauto + allows shelved goals to remain at any point during search and treat + typeclasses goals like any other. + + + The transparency information of databases is used consistently for + all hints declared in them. It is always used when calling the + unifier. When considering the local hypotheses, we use the transparent + state of the first hint database given. Using an empty database + (created with :cmd:`Create HintDb` for example) with unfoldable variables and + constants as the first argument of typeclasses eauto hence makes + resolution with the local hypotheses use full conversion during + unification. + + + .. cmdv:: typeclasses eauto @num + + .. warning:: + The semantics for the limit :n:`@num` + is different than for auto. By default, if no limit is given the + search is unbounded. Contrary to auto, introduction steps (intro) are + counted, which might result in larger limits being necessary when + searching with typeclasses eauto than auto. + + .. cmdv:: typeclasses eauto with {+ @ident} + + This variant runs resolution with the given hint databases. It treats + typeclass subgoals the same as other subgoals (no shelving of + non-typeclass goals in particular). + +.. tacn:: autoapply @term with @ident + :name: autoapply + + The tactic autoapply applies a term using the transparency information + of the hint database ident, and does *no* typeclass resolution. This can + be used in :cmd:`Hint Extern`’s for typeclass instances (in the hint + database ``typeclass_instances``) to allow backtracking on the typeclass + subgoals created by the lemma application, rather than doing type class + resolution locally at the hint application time. -.. _typeclasses-eauto: - -``typeclasses eauto`` -~~~~~~~~~~~~~~~~~~~~~ - -The ``typeclasses eauto`` tactic uses a different resolution engine than -eauto and auto. The main differences are the following: - -+ Contrary to ``eauto`` and ``auto``, the resolution is done entirely in - the new proof engine (as of Coq v8.6), meaning that backtracking is - available among dependent subgoals, and shelving goals is supported. - typeclasses eauto is a multi-goal tactic. It analyses the dependencies - between subgoals to avoid backtracking on subgoals that are entirely - independent. - -+ When called with no arguments, typeclasses eauto uses - thetypeclass_instances database by default (instead of core). - Dependent subgoals are automatically shelved, and shelved goals can - remain after resolution ends (following the behavior ofCoq 8.5). - *Note: * As of Coq 8.6, all:once (typeclasses eauto) faithfully - mimicks what happens during typeclass resolution when it is called - during refinement/type-inference, except that *only* declared class - subgoals are considered at the start of resolution during type - inference, while “all” can select non-class subgoals as well. It might - move to ``all:typeclasses eauto`` in future versions when the - refinement engine will be able to backtrack. - -+ When called with specific databases (e.g. with), typeclasses eauto - allows shelved goals to remain at any point during search and treat - typeclasses goals like any other. - -+ The transparency information of databases is used consistently for - all hints declared in them. It is always used when calling the - unifier. When considering the local hypotheses, we use the transparent - state of the first hint database given. Using an empty database - (created with Create HintDb for example) with unfoldable variables and - constants as the first argument of typeclasses eauto hence makes - resolution with the local hypotheses use full conversion during - unification. - - -Variants: +.. _TypeclassesTransparent: -#. ``typeclasses eauto [num]`` +Typeclasses Transparent, Typclasses Opaque +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - *Warning:* The semantics for the limit num - is different than for auto. By default, if no limit is given the - search is unbounded. Contrary to auto, introduction steps (intro) are - counted, which might result in larger limits being necessary when - searching with typeclasses eauto than auto. +.. cmd:: Typeclasses Transparent {+ @ident} -#. ``typeclasses eauto with {+ @ident}`` + This command defines makes the identifiers transparent during type class + resolution. - This variant runs resolution with the given hint databases. It treats - typeclass subgoals the same as other subgoals (no shelving of - non-typeclass goals in particular). +.. cmd:: Typeclasses Opaque {+ @ident} -.. _autoapply: + Make the identifiers opaque for typeclass search. It is useful when some + constants prevent some unifications and make resolution fail. It is also + useful to declare constants which should never be unfolded during + proof-search, like fixpoints or anything which does not look like an + abbreviation. This can additionally speed up proof search as the typeclass + map can be indexed by such rigid constants (see + :ref:`thehintsdatabasesforautoandeauto`). -``autoapply term with ident`` -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +By default, all constants and local variables are considered transparent. One +should take care not to make opaque any constant that is used to abbreviate a +type, like: -The tactic autoapply applies a term using the transparency information -of the hint database ident, and does *no* typeclass resolution. This can -be used in ``Hint Extern``’s for typeclass instances (in the hint -database ``typeclass_instances``) to allow backtracking on the typeclass -subgoals created by the lemma application, rather than doing type class -resolution locally at the hint application time. +:: -.. _TypeclassesTransparent: + relation A := A -> A -> Prop. -Typeclasses Transparent, Typclasses Opaque -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. -.. cmd:: Typeclasses { Transparent | Opaque } {+ @ident} - This commands defines the transparency of the given identifiers - during type class resolution. It is useful when some constants - prevent some unifications and make resolution fail. It is also useful - to declare constants which should never be unfolded during - proof-search, like fixpoints or anything which does not look like an - abbreviation. This can additionally speed up proof search as the - typeclass map can be indexed by such rigid constants (see - :ref:`thehintsdatabasesforautoandeauto`). By default, all constants - and local variables are considered transparent. One should take care - not to make opaque any constant that is used to abbreviate a type, - like: +Options +~~~~~~~ -:: +.. opt:: Typeclasses Dependency Order - relation A := A -> A -> Prop. + This option (on by default since 8.6) respects the dependency order + between subgoals, meaning that subgoals which are depended on by other + subgoals come first, while the non-dependent subgoals were put before + the dependent ones previously (Coq 8.5 and below). This can result in + quite different performance behaviors of proof search. -This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. +.. opt:: Typeclasses Filtered Unification -Set Typeclasses Dependency Order -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + This option, available since Coq 8.6 and off by default, switches the + hint application procedure to a filter-then-unify strategy. To apply a + hint, we first check that the goal *matches* syntactically the + inferred or specified pattern of the hint, and only then try to + *unify* the goal with the conclusion of the hint. This can drastically + improve performance by calling unification less often, matching + syntactic patterns being very quick. This also provides more control + on the triggering of instances. For example, forcing a constant to + explicitely appear in the pattern will make it never apply on a goal + where there is a hole in that place. -This option (on by default since 8.6) respects the dependency order -between subgoals, meaning that subgoals which are depended on by other -subgoals come first, while the non-dependent subgoals were put before -the dependent ones previously (Coq v8.5 and below). This can result in -quite different performance behaviors of proof search. +.. opt:: Typeclasses Limit Intros -Set Typeclasses Filtered Unification -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + This option (on by default) controls the ability to apply hints while + avoiding (functional) eta-expansions in the generated proof term. It + does so by allowing hints that conclude in a product to apply to a + goal with a matching product directly, avoiding an introduction. + *Warning:* this can be expensive as it requires rebuilding hint + clauses dynamically, and does not benefit from the invertibility + status of the product introduction rule, resulting in potentially more + expensive proof-search (i.e. more useless backtracking). -This option, available since Coq 8.6 and off by default, switches the -hint application procedure to a filter-then-unify strategy. To apply a -hint, we first check that the goal *matches* syntactically the -inferred or specified pattern of the hint, and only then try to -*unify* the goal with the conclusion of the hint. This can drastically -improve performance by calling unification less often, matching -syntactic patterns being very quick. This also provides more control -on the triggering of instances. For example, forcing a constant to -explicitely appear in the pattern will make it never apply on a goal -where there is a hole in that place. +.. opt:: Typeclass Resolution For Conversion -Set Typeclasses Limit Intros -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + This option (on by default) controls the use of typeclass resolution + when a unification problem cannot be solved during elaboration/type- + inference. With this option on, when a unification fails, typeclass + resolution is tried before launching unification once again. -This option (on by default) controls the ability to apply hints while -avoiding (functional) eta-expansions in the generated proof term. It -does so by allowing hints that conclude in a product to apply to a -goal with a matching product directly, avoiding an introduction. -*Warning:* this can be expensive as it requires rebuilding hint -clauses dynamically, and does not benefit from the invertibility -status of the product introduction rule, resulting in potentially more -expensive proof-search (i.e. more useless backtracking). +.. opt:: Typeclasses Strict Resolution + Typeclass declarations introduced when this option is set have a + stricter resolution behavior (the option is off by default). When + looking for unifications of a goal with an instance of this class, we + “freeze” all the existentials appearing in the goals, meaning that + they are considered rigid during unification and cannot be + instantiated. -Set Typeclass Resolution For Conversion -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -This option (on by default) controls the use of typeclass resolution -when a unification problem cannot be solved during elaboration/type- -inference. With this option on, when a unification fails, typeclass -resolution is tried before launching unification once again. +.. opt:: Typeclasses Unique Solutions + When a typeclass resolution is launched we ensure that it has a single + solution or fail. This ensures that the resolution is canonical, but + can make proof search much more expensive. -Set Typeclasses Strict Resolution -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Typeclass declarations introduced when this option is set have a -stricter resolution behavior (the option is off by default). When -looking for unifications of a goal with an instance of this class, we -“freeze” all the existentials appearing in the goals, meaning that -they are considered rigid during unification and cannot be -instantiated. +.. opt:: Typeclasses Unique Instances + Typeclass declarations introduced when this option is set have a more + efficient resolution behavior (the option is off by default). When a + solution to the typeclass goal of this class is found, we never + backtrack on it, assuming that it is canonical. -Set Typeclasses Unique Solutions -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: Typeclasses Debug {? Verbosity @num} -When a typeclass resolution is launched we ensure that it has a single -solution or fail. This ensures that the resolution is canonical, but -can make proof search much more expensive. + These options allow to see the resolution steps of typeclasses that are + performed during search. The ``Debug`` option is synonymous to ``Debug + Verbosity 1``, and ``Debug Verbosity 2`` provides more information + (tried tactics, shelving of goals, etc…). +.. opt:: Refine Instance Mode -Set Typeclasses Unique Instances -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + This option allows to switch the behavior of instance declarations made through + the Instance command. -Typeclass declarations introduced when this option is set have a more -efficient resolution behavior (the option is off by default). When a -solution to the typeclass goal of this class is found, we never -backtrack on it, assuming that it is canonical. + + When it is on (the default), instances that have unsolved holes in + their proof-term silently open the proof mode with the remaining + obligations to prove. + + When it is off, they fail with an error instead. Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ @@ -558,27 +554,3 @@ Typeclasses eauto `:=` default) or breadth-first search. + ``depth`` This sets the depth limit of the search. - - -Set Typeclasses Debug -~~~~~~~~~~~~~~~~~~~~~ - -.. cmd:: Set Typeclasses Debug {? Verbosity @num} - -These options allow to see the resolution steps of typeclasses that are -performed during search. The ``Debug`` option is synonymous to ``Debug -Verbosity 1``, and ``Debug Verbosity 2`` provides more information -(tried tactics, shelving of goals, etc…). - - -Set Refine Instance Mode -~~~~~~~~~~~~~~~~~~~~~~~~ - -The option Refine Instance Mode allows to switch the behavior of -instance declarations made through the Instance command. - -+ When it is on (the default), instances that have unsolved holes in - their proof-term silently open the proof mode with the remaining - obligations to prove. - -+ When it is off, they fail with an error instead. |