diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 121 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 24 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 24 |
5 files changed, 85 insertions, 95 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index e882ce6e88..b568160356 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -21,10 +21,10 @@ type is considered to be a variable. A variable name cannot occur more than once in a given pattern. It is recommended to start variable names by a lowercase letter. -If a pattern has the form ``(c x)`` where ``c`` is a constructor symbol and x +If a pattern has the form ``c x`` where ``c`` is a constructor symbol and x is a linear vector of (distinct) variables, it is called *simple*: it is the kind of pattern recognized by the basic version of match. On -the opposite, if it is a variable ``x`` or has the form ``(c p)`` with ``p`` not +the opposite, if it is a variable ``x`` or has the form ``c p`` with ``p`` not only made of variables, the pattern is called *nested*. A variable pattern matches any value, and the identifier is bound to @@ -216,7 +216,8 @@ Here is an example: end. -Here is another example using disjunctive subpatterns. +Nested disjunctive patterns are allowed, inside parentheses, with the +notation :n:`({+| @pattern})`, as in: .. coqtop:: in diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 68f6d4008a..2ea0861e47 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -528,7 +528,7 @@ pass additional arguments such as ``using relation``. .. tacv:: setoid_reflexivity setoid_symmetry {? in @ident} setoid_transitivity - setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident} + setoid_rewrite {? @orientation} @term {? at @occurrences} {? in @ident} setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic} :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; setoid_replace @@ -563,17 +563,18 @@ Printing relations and morphisms of morphisms, the :cmd:`Print Instances` command can be useful to understand what additional morphisms should be registered. +.. _deprecated_syntax_for_generalized_rewriting: Deprecated syntax and backward incompatibilities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Add Setoid @A @Aeq @ST as @ident +.. cmd:: Add Setoid @qualid__1 @qualid__2 @qualid__3 as @ident This command for declaring setoids and morphisms is also accepted due to backward compatibility reasons. - Here ``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 + Here :n:`@qualid__2` is a congruence relation without parameters, :n:`@qualid__1` is its carrier + and :n:`@qualid__3` is an object of type (:n:`Setoid_Theory @qualid__1 @qualid__2`) (i.e. a record packing together the reflexivity, symmetry and transitivity lemmas). Notice that the syntax is not completely backward compatible since the identifier was not required. @@ -589,6 +590,12 @@ Deprecated syntax and backward incompatibilities bi-implication in place of a simple implication. In practice, porting an old development to the new semantics is usually quite simple. +.. cmd:: Declare Morphism @ident : @ident + :name: Declare Morphism + + This commands is to be used in a module type to declare a parameter that + is a morphism. + Notice that several limitations of the old implementation have been lifted. In particular, it is now possible to declare several relations with the same carrier and several signatures for the same morphism. @@ -708,91 +715,65 @@ Definitions The generalized rewriting tactic is based on a set of strategies that can be combined to obtain custom rewriting procedures. Its set of strategies is based on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting -strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a +strategies are applied using the tactic :n:`rewrite_strat @strategy` where :token:`strategy` is a strategy expression. Strategies are defined inductively as described by the following grammar: -.. productionlist:: rewriting - s, t, u : `strategy` - : `lemma` - : `lemma_right_to_left` - : `failure` - : `identity` - : `reflexivity` - : `progress` - : `failure_catch` - : `composition` - : `left_biased_choice` - : `iteration_one_or_more` - : `iteration_zero_or_more` - : `one_subterm` - : `all_subterms` - : `innermost_first` - : `outermost_first` - : `bottom_up` - : `top_down` - : `apply_hint` - : `any_of_the_terms` - : `apply_reduction` - : `fold_expression` - -.. productionlist:: rewriting - strategy : ( `s` ) - lemma : `c` - lemma_right_to_left : <- `c` - failure : fail - identity : id - reflexivity : refl - progress : progress `s` - failure_catch : try `s` - composition : `s` ; `u` - left_biased_choice : choice `s` `t` - iteration_one_or_more : repeat `s` - iteration_zero_or_more : any `s` - one_subterm : subterm `s` - all_subterms : subterms `s` - innermost_first : innermost `s` - outermost_first : outermost `s` - bottom_up : bottomup `s` - top_down : topdown `s` - apply_hint : hints `hintdb` - any_of_the_terms : terms (`c`)+ - apply_reduction : eval `redexpr` - fold_expression : fold `c` - +.. productionlist:: coq + strategy : `qualid` (lemma, left to right) + : <- `qualid` (lemma, right to left) + : fail (failure) + : id (identity) + : refl (reflexivity) + : progress `strategy` (progress) + : try `strategy` (try catch) + : `strategy` ; `strategy` (composition) + : choice `strategy` `strategy` (left_biased_choice) + : repeat `strategy` (one or more) + : any `strategy` (zero or more) + : subterm `strategy` (one subterm) + : subterms `strategy` (all subterms) + : innermost `strategy` (innermost first) + : outermost `strategy` (outermost first) + : bottomup `strategy` (bottom-up) + : topdown `strategy` (top-down) + : hints `ident` (apply hints from hint database) + : terms `term` ... `term` (any of the terms) + : eval `redexpr` (apply reduction) + : fold `term` (unify) + : ( `strategy` ) Actually a few of these are defined in term of the others using a primitive fixpoint operator: -.. productionlist:: rewriting - try `s` : choice `s` `id` - any `s` : fix `u`. try (`s` ; `u`) - repeat `s` : `s` ; any `s` - bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu - topdown s : fix `td`. (choice s (progress (subterms td))) ; try td - innermost s : fix `i`. (choice (subterm i) s) - outermost s : fix `o`. (choice s (subterm o)) +- :n:`try @strategy := choice @strategy id` +- :n:`any @strategy := fix @ident. try (@strategy ; @ident)` +- :n:`repeat @strategy := @strategy; any @strategy` +- :n:`bottomup @strategy := fix @ident. (choice (progress (subterms @ident)) @strategy) ; try @ident` +- :n:`topdown @strategy := fix @ident. (choice @strategy (progress (subterms @ident))) ; try @ident` +- :n:`innermost @strategy := fix @ident. (choice (subterm @ident) @strategy)` +- :n:`outermost @strategy := fix @ident. (choice @strategy (subterm @ident))` The basic control strategy semantics are straightforward: strategies are applied to subterms of the term to rewrite, starting from the root of the term. The lemma strategies unify the left-hand-side of the lemma with the current subterm and on success rewrite it to the right- hand-side. Composition can be used to continue rewriting on the -current subterm. The fail strategy always fails while the identity +current subterm. The ``fail`` strategy always fails while the identity strategy succeeds without making progress. The reflexivity strategy succeeds, making progress using a reflexivity proof of rewriting. -Progress tests progress of the argument strategy and fails if no +``progress`` tests progress of the argument :token:`strategy` and fails if no progress was made, while ``try`` always succeeds, catching failures. -Choice is left-biased: it will launch the first strategy and fall back +``choice`` is left-biased: it will launch the first strategy and fall back on the second one in case of failure. One can iterate a strategy at least 1 time using ``repeat`` and at least 0 times using ``any``. -The ``subterm`` and ``subterms`` strategies apply their argument strategy ``s`` to +The ``subterm`` and ``subterms`` strategies apply their argument :token:`strategy` to respectively one or all subterms of the current term under consideration, left-to-right. ``subterm`` stops at the first subterm for -which ``s`` made progress. The composite strategies ``innermost`` and ``outermost`` +which :token:`strategy` made progress. The composite strategies ``innermost`` and ``outermost`` perform a single innermost or outermost rewrite using their argument -strategy. Their counterparts ``bottomup`` and ``topdown`` perform as many +:token:`strategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many rewritings as possible, starting from the bottom or the top of the term. @@ -802,15 +783,15 @@ lemmas at the current subterm. The ``terms`` strategy takes the lemma names directly as arguments. The ``eval`` strategy expects a reduction expression (see :ref:`performingcomputations`) and succeeds if it reduces the subterm under consideration. The ``fold`` strategy takes -a term ``c`` and tries to *unify* it to the current subterm, converting it to ``c`` -on success, it is stronger than the tactic ``fold``. +a :token:`term` and tries to *unify* it to the current subterm, converting it to :token:`term` +on success. It is stronger than the tactic ``fold``. Usage ~~~~~ -.. tacn:: rewrite_strat @s {? in @ident } +.. tacn:: rewrite_strat @strategy {? in @ident } :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 22ddcae584..45c74ab02a 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -299,9 +299,9 @@ optional tactic is replaced by the default one if not specified. Displays all remaining obligations. -.. cmd:: Obligation num {? of @ident} +.. cmd:: Obligation @num {? of @ident} - Start the proof of obligation num. + Start the proof of obligation :token:`num`. .. cmd:: Next Obligation {? of @ident} diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 3b350d5dc0..3f4d5cc784 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -310,10 +310,10 @@ The syntax for adding a new ring is .. productionlist:: coq ring_mod : abstract | decidable `term` | morphism `term` : setoid `term` `term` - : constants [`ltac`] - : preprocess [`ltac`] - : postprocess [`ltac`] - : power_tac `term` [`ltac`] + : constants [ `tactic` ] + : preprocess [ `tactic` ] + : postprocess [ `tactic` ] + : power_tac `term` [ `tactic` ] : sign `term` : div `term` @@ -341,31 +341,31 @@ The syntax for adding a new ring is This modifier needs not be used if the setoid and morphisms have been declared. - constants [ :n:`@ltac` ] - specifies a tactic expression :n:`@ltac` that, given a + constants [ :n:`@tactic` ] + specifies a tactic expression :n:`@tactic` that, given a term, returns either an object of the coefficient set that is mapped to the expression via the morphism, or returns ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1 to their counterpart in the coefficient set. This is generally not desirable for non trivial computational rings. - preprocess [ :n:`@ltac` ] - specifies a tactic :n:`@ltac` that is applied as a + preprocess [ :n:`@tactic` ] + specifies a tactic :n:`@tactic` that is applied as a preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to transform a goal so that it is better recognized. For instance, ``S n`` can be changed to ``plus 1 n``. - postprocess [ :n:`@ltac` ] - specifies a tactic :n:`@ltac` that is applied as a final + postprocess [ :n:`@tactic` ] + specifies a tactic :n:`@tactic` that is applied as a final step for :tacn:`ring_simplify`. For instance, it can be used to undo modifications of the preprocessor. - power_tac :n:`@term` [ :n:`@ltac` ] + power_tac :n:`@term` [ :n:`@tactic` ] allows :tacn:`ring` and :tacn:`ring_simplify` to recognize power expressions with a constant positive integer exponent (example: :math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies the specification of a power function (term has to be a proof of - ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression + ``Ring_theory.power_theory``) and :n:`@tactic` specifies a tactic expression that, given a term, “abstracts” it into an object of type |N| whose interpretation via ``Cp_phi`` (the evaluation function of power coefficient) is the original term, or returns ``InitialRing.NotConstant`` diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 1aa2111816..395b5ce2d3 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -366,24 +366,32 @@ The syntax has been extended to allow users to explicitly bind names to universes and explicitly instantiate polymorphic definitions. .. cmd:: Universe @ident + Polymorphic Universe @ident 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 + command supports the ``Polymorphic`` flag only in sections, meaning the universe quantification will be discharged on each section definition independently. One cannot mix polymorphic and monomorphic declarations in the same section. -.. cmd:: Constraint @ident @ord @ident +.. cmd:: Constraint @universe_constraint + Polymorphic Constraint @universe_constraint - This command declares a new constraint between named universes. The - order relation :n:`@ord` can be one of :math:`<`, :math:`≤` or :math:`=`. If consistent, the constraint - is then enforced in the global environment. Like ``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. + This command declares a new constraint between named universes. + + .. productionlist:: coq + universe_constraint : `qualid` < `qualid` + : `qualid` <= `qualid` + : `qualid` = `qualid` + + 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. .. exn:: Undeclared universe @ident. :undocumented: |