diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 45 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 64 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 184 |
5 files changed, 150 insertions, 156 deletions
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index d60387f4f6..e4dea34874 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -537,14 +537,19 @@ Notice, however, that using the prefixed tactics it is possible to pass additional arguments such as ``using relation``. .. tacv:: setoid_reflexivity + :name: setoid_reflexivity .. tacv:: setoid_symmetry [in @ident] + :name: setoid_symmetry .. tacv:: setoid_transitivity + :name: setoid_transitivity .. tacv:: setoid_rewrite [@orientation] @term [at @occs] [in @ident] + :name: setoid_rewrite .. tacv:: setoid_replace @term with @term [in @ident] [using relation @term] [by @tactic] + :name: setoid_replace The ``using relation`` arguments cannot be passed to the unprefixed form. @@ -583,7 +588,7 @@ Deprecated syntax and backward incompatibilities Due to backward compatibility reasons, the following syntax for the declaration of setoids and morphisms is also accepted. -.. tacv:: Add Setoid @A @Aeq @ST as @ident +.. cmd:: Add Setoid @A @Aeq @ST as @ident where ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record @@ -818,7 +823,8 @@ Usage ~~~~~ -.. tacv:: rewrite_strat @s [in @ident] +.. tacn:: rewrite_strat @s [in @ident] + :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index ec1b942e02..c48c2d7ce1 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -138,7 +138,7 @@ Declaration of Coercions .. exn:: @qualid does not respect the uniform inheritance condition .. exn:: Found target class ... instead of ... - .. warn:: Ambigous path: + .. warn:: Ambiguous path When the coercion `qualid` is added to the inheritance graph, non valid coercion paths are ignored; they are signaled by a warning @@ -218,6 +218,7 @@ declaration, this constructor is declared as a coercion. Idem but locally to the current section. .. cmdv:: SubClass @ident := @type. + :name: SubClass If `type` is a class `ident'` applied to some arguments then `ident` is defined and an identity coercion of name @@ -255,17 +256,16 @@ Displaying Available Coercions Activating the Printing of Coercions ------------------------------------- -.. cmd:: Set Printing Coercions. +.. opt:: Printing Coercions - This command forces all the coercions to be printed. - Conversely, to skip the printing of coercions, use - ``Unset Printing Coercions``. By default, coercions are not printed. + When on, this option forces all the coercions to be printed. + By default, coercions are not printed. -.. cmd:: Add Printing Coercion @qualid. +.. cmd:: Add Printing Coercion @qualid - This command forces coercion denoted by `qualid` to be printed. - To skip the printing of coercion `qualid`, use - ``Remove Printing Coercion`` `qualid`. By default, a coercion is never printed. + This command forces coercion denoted by :n:`@qualid` to be printed. To skip + the printing of coercion :n:`@qualid`, use :cmd:`Remove Printing Coercion`. By + default, a coercion is never printed. .. _coercions-classes-as-records: @@ -291,12 +291,10 @@ by extending the existing :cmd:`Record` macro. Its new syntax is: (this may fail if the uniform inheritance condition is not satisfied). -.. note:: +.. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }. + :name: Structure - The keyword ``Structure`` is a synonym of ``Record``. - -.. - FIXME: \comindex{Structure} + This is a synonym of :cmd:`Record`. Coercions and Sections @@ -312,20 +310,17 @@ coercions which do not verify the uniform inheritance condition any longer are also forgotten. Coercions and Modules ---------------------= - -From |Coq| version 8.3, the coercions present in a module are activated -only when the module is explicitly imported. Formerly, the coercions -were activated as soon as the module was required, whatever it was -imported or not. - -To recover the behavior of the versions of |Coq| prior to 8.3, use the -following command: +--------------------- -.. cmd:: Set Automatic Coercions Import. +.. opt:: Automatic Coercions Import -To cancel the effect of the option, use instead ``Unset Automatic Coercions Import``. + Since |Coq| version 8.3, the coercions present in a module are activated + only when the module is explicitly imported. Formerly, the coercions + were activated as soon as the module was required, whatever it was + imported or not. + This option makes it possible to recover the behavior of the versions of + |Coq| prior to 8.3. Examples -------- diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index e850587c8a..4f8cc34d4a 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -13,20 +13,19 @@ tactics for solving arithmetic goals over :math:`\mathbb{Z}`, :math:`\mathbb{Q}` It also possible to get the tactics for integers by a ``Require Import Lia``, rationals ``Require Import Lqa`` and reals ``Require Import Lra``. -+ ``lia`` is a decision procedure for linear integer arithmetic (see Section :ref:`lia <lia>`); -+ ``nia`` is an incomplete proof procedure for integer non-linear - arithmetic (see Section :ref:`nia <nia>`); -+ ``lra`` is a decision procedure for linear (real or rational) arithmetic - (see Section :ref:`lra <lra>`); -+ ``nra`` is an incomplete proof procedure for non-linear (real or - rational) arithmetic (see Section :ref:`nra <nra>`); -+ ``psatz D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and ++ :tacn:`lia` is a decision procedure for linear integer arithmetic; ++ :tacn:`nia` is an incomplete proof procedure for integer non-linear + arithmetic; ++ :tacn:`lra` is a decision procedure for linear (real or rational) arithmetic; ++ :tacn:`nra` is an incomplete proof procedure for non-linear (real or + rational) arithmetic; ++ :tacn:`psatz` ``D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and ``n`` is an optional integer limiting the proof search depth is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison’s HOL Light driver to the external prover `csdp` [#]_. Note that the `csdp` driver is generating a *proof cache* which makes it possible to rerun scripts - even without `csdp` (see Section :ref:`psatz <psatz>`). + even without `csdp`. The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}. @@ -91,12 +90,13 @@ For each conjunct :math:`C_i`, the tactic calls a oracle which searches for expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`) and checked to be :math:`-1`. -.. _lra: - `lra`: a decision procedure for linear real and rational arithmetic ------------------------------------------------------------------- -The `lra` tactic is searching for *linear* refutations using Fourier +.. tacn:: lra + :name: lra + +This tactic is searching for *linear* refutations using Fourier elimination [#]_. As a result, this tactic explores a subset of the *Cone* defined as @@ -107,16 +107,17 @@ The deductive power of `lra` is the combined deductive power of tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`. -.. _lia: - `lia`: a tactic for linear integer arithmetic --------------------------------------------- -The tactic lia offers an alternative to the omega and romega tactic -(see :ref:`omega`). Roughly speaking, the deductive power of lia is -the combined deductive power of `ring_simplify` and `omega`. However, it -solves linear goals that `omega` and `romega` do not solve, such as the -following so-called *omega nightmare* :cite:`TheOmegaPaper`. +.. tacn:: lia + :name: lia + +This tactic offers an alternative to the :tacn:`omega` and :tac:`romega` +tactics. Roughly speaking, the deductive power of lia is the combined deductive +power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear +goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following +so-called *omega nightmare* :cite:`TheOmegaPaper`. .. coqtop:: in @@ -124,8 +125,8 @@ following so-called *omega nightmare* :cite:`TheOmegaPaper`. 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x - 9 * y <= 4 -> False. -The estimation of the relative efficiency of `lia` *vs* `omega` and `romega` -is under evaluation. +The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and +:tacn:`romega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -182,12 +183,13 @@ Our current oracle tries to find an expression :math:`e` with a small range with an equation :math:`e = i` for :math:`i \in [c_1,c_2]` and recursively search for a proof. -.. _nra: - `nra`: a proof procedure for non-linear arithmetic -------------------------------------------------- -The `nra` tactic is an *experimental* proof procedure for non-linear +.. tacn:: nra + :name: nra + +This tactic is an *experimental* proof procedure for non-linear arithmetic. The tactic performs a limited amount of non-linear reasoning before running the linear prover of `lra`. This pre-processing does the following: @@ -202,21 +204,23 @@ does the following: After this pre-processing, the linear prover of `lra` searches for a proof by abstracting monomials by variables. -.. _nia: - `nia`: a proof procedure for non-linear integer arithmetic ---------------------------------------------------------- -The `nia` tactic is a proof procedure for non-linear integer arithmetic. +.. tacn:: nia + :name: nia + +This tactic is a proof procedure for non-linear integer arithmetic. It performs a pre-processing similar to `nra`. The obtained goal is solved using the linear integer prover `lia`. -.. _psatz: - `psatz`: a proof procedure for non-linear arithmetic ---------------------------------------------------- -The `psatz` tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the +.. tacn:: psatz + :name: psatz + +This tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the depth parameter :math:`n`. In theory, such a proof search is complete – if the goal is provable the search eventually stops. Unfortunately, the external oracle is using numeric (approximate) optimization techniques diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 1c3fdeb430..be30d1bc4a 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -151,7 +151,7 @@ Program Definition obligations. Once solved using the commands shown below, it binds the final |Coq| term to the name ``ident`` in the environment. - .. exn:: ident already exists + .. exn:: @ident already exists (Program Definition) .. cmdv:: Program Definition @ident : @type := @term @@ -276,6 +276,7 @@ obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. .. cmd:: {? Local|Global} Obligation Tactic := @tactic + :name: Obligation Tactic Sets the default obligation solving tactic applied to all obligations automatically, whether to solve them or when starting to prove one, diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 8861cac8af..3e95bd8c45 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -314,28 +314,25 @@ 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 Switches the type-checking to Program (chapter :ref:`programs`) and uses the obligation mechanism to manage missing fields. -.. cmd:: Declare Instance +..cmdv:: Declare Instance In a Module Type, this command states that a corresponding concrete instance should exist in any implementation of thisModule Type. This @@ -370,14 +367,10 @@ Context Declares variables according to the given binding context, which might use :ref:`implicit-generalization`. +.. tacn:: typeclasses eauto -.. _typeclasses-eauto: - -``typeclasses eauto`` -~~~~~~~~~~~~~~~~~~~~~ - -The ``typeclasses eauto`` tactic uses a different resolution engine than -eauto and auto. The main differences are the following: +This tactic uses a different resolution engine than :tacn:`eauto` and +:tacn:`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 @@ -428,118 +421,114 @@ Variants: typeclass subgoals the same as other subgoals (no shelving of non-typeclass goals in particular). -.. _autoapply: - -``autoapply term with ident`` -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. 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 ``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. + 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. .. _TypeclassesTransparent: Typeclasses Transparent, Typclasses Opaque ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Typeclasses { Transparent | Opaque } {+ @ident} +.. cmd:: Typeclasses Transparent {+ @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: + This command defines makes the identifiers transparent during type class + resolution. -:: + .. cmdv:: Typeclasses Opaque {+ @ident} + :name: Typeclasses Opaque + + 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`). + + 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: - relation A := A -> A -> Prop. + :: -This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. + relation A := A -> A -> Prop. + This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. -Set Typeclasses Dependency Order -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -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 Dependency Order + 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. -Set Typeclasses Filtered Unification -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -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:: Typeclasses Filtered Unification + 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. -Set Typeclasses Limit Intros -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: Typeclasses Limit Intros -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 (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). -Set Typeclass Resolution For Conversion -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: 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. + 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. -Set Typeclasses Strict Resolution -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. 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. + 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 Typeclasses Unique Solutions -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. 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. + 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 Unique Instances -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. 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. + 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. Typeclasses eauto `:=` @@ -562,7 +551,7 @@ Typeclasses eauto `:=` Set Typeclasses Debug ~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Set Typeclasses Debug {? Verbosity @num} +.. opt:: 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 @@ -570,11 +559,10 @@ Verbosity 1``, and ``Debug Verbosity 2`` provides more information (tried tactics, shelving of goals, etc…). -Set Refine Instance Mode -~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: Refine Instance Mode -The option Refine Instance Mode allows to switch the behavior of -instance declarations made through the Instance command. +This options 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 |