diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 155 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 48 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 105 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 9 |
4 files changed, 187 insertions, 130 deletions
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 94ab6e789c..315c9d4a80 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -713,48 +713,119 @@ 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 +combined to create custom rewriting procedures. Its set of strategies is based on the programmable rewriting strategies with generic traversals by Visser et al. :cite:`Luttik97specificationof` :cite:`Visser98`, which formed the core of the Stratego transformation language :cite:`Visser01`. Rewriting 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:: 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 `red_expr` (apply reduction) - : fold `term` (unify) - : ( `strategy` ) - -Actually a few of these are defined in term of the others using a +are applied using the tactic :n:`rewrite_strat @rewstrategy`. + +.. insertprodn rewstrategy rewstrategy + +.. prodn:: + rewstrategy ::= @one_term + | <- @one_term + | fail + | id + | refl + | progress @rewstrategy + | try @rewstrategy + | @rewstrategy ; @rewstrategy + | choice @rewstrategy @rewstrategy + | repeat @rewstrategy + | any @rewstrategy + | subterm @rewstrategy + | subterms @rewstrategy + | innermost @rewstrategy + | outermost @rewstrategy + | bottomup @rewstrategy + | topdown @rewstrategy + | hints @ident + | terms {* @one_term } + | eval @red_expr + | fold @one_term + | ( @rewstrategy ) + | old_hints @ident + +:n:`@one_term` + lemma, left to right + +:n:`<- @one_term` + lemma, right to left + +:n:`fail` + failure + +:n:`id` + identity + +:n:`refl` + reflexivity + +:n:`progress @rewstrategy` + progress + +:n:`try @rewstrategy` + try catch + +:n:`@rewstrategy ; @rewstrategy` + composition + +:n:`choice @rewstrategy @rewstrategy` + left_biased_choice + +:n:`repeat @rewstrategy` + one or more + +:n:`any @rewstrategy` + zero or more + +:n:`subterm @rewstrategy` + one subterm + +:n:`subterms @rewstrategy` + all subterms + +:n:`innermost @rewstrategy` + innermost first + +:n:`outermost @rewstrategy` + outermost first + +:n:`bottomup @rewstrategy` + bottom-up + +:n:`topdown @rewstrategy` + top-down + +:n:`hints @ident` + apply hints from hint database + +:n:`terms {* @one_term }` + any of the terms + +:n:`eval @red_expr` + apply reduction + +:n:`fold @term` + unify + +:n:`( @rewstrategy )` + to be documented + +:n:`old_hints @ident` + to be documented + + +A few of these are defined in terms of the others using a primitive fixpoint operator: -- :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))` +- :n:`try @rewstrategy := choice @rewstrategy id` +- :n:`any @rewstrategy := fix @ident. try (@rewstrategy ; @ident)` +- :n:`repeat @rewstrategy := @rewstrategy; any @rewstrategy` +- :n:`bottomup @rewstrategy := fix @ident. (choice (progress (subterms @ident)) @rewstrategy) ; try @ident` +- :n:`topdown @rewstrategy := fix @ident. (choice @rewstrategy (progress (subterms @ident))) ; try @ident` +- :n:`innermost @rewstrategy := fix @ident. (choice (subterm @ident) @rewstrategy)` +- :n:`outermost @rewstrategy := fix @ident. (choice @rewstrategy (subterm @ident))` The basic control strategy semantics are straightforward: strategies are applied to subterms of the term to rewrite, starting from the root @@ -764,18 +835,18 @@ hand-side. Composition can be used to continue rewriting on the 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 :token:`strategy` and fails if no +``progress`` tests progress of the argument :n:`@rewstrategy` 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 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 :token:`strategy` to +The ``subterm`` and ``subterms`` strategies apply their argument :n:`@rewstrategy` to respectively one or all subterms of the current term under consideration, left-to-right. ``subterm`` stops at the first subterm for -which :token:`strategy` made progress. The composite strategies ``innermost`` and ``outermost`` +which :n:`@rewstrategy` made progress. The composite strategies ``innermost`` and ``outermost`` perform a single innermost or outermost rewrite using their argument -:token:`strategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many +:n:`@rewstrategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many rewritings as possible, starting from the bottom or the top of the term. @@ -793,7 +864,7 @@ Usage ~~~~~ -.. tacn:: rewrite_strat @strategy {? in @ident } +.. tacn:: rewrite_strat @rewstrategy {? 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 b007509b2e..1f33775a01 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -37,12 +37,13 @@ In addition to these user-defined classes, we have two built-in classes: * ``Funclass``, the class of functions; its objects are all the terms with a functional type, i.e. of form :g:`forall x:A,B`. -Formally, the syntax of classes is defined as: + .. insertprodn class class + + .. prodn:: + class ::= Funclass + | Sortclass + | @smart_qualid -.. productionlist:: - class: `qualid` - : Sortclass - : Funclass Coercions @@ -186,37 +187,12 @@ Declaring Coercions This defines :token:`ident` just like :n:`Let @ident := @term {? @type }`, and then declares :token:`ident` as a coercion between it source and its target. -Assumptions can be declared as coercions at declaration time. -This extends the grammar of assumptions from -Figure :ref:`vernacular` as follows: - -.. - FIXME: - \comindex{Variable \mbox{\rm (and coercions)}} - \comindex{Axiom \mbox{\rm (and coercions)}} - \comindex{Parameter \mbox{\rm (and coercions)}} - \comindex{Hypothesis \mbox{\rm (and coercions)}} - -.. productionlist:: - assumption : `assumption_token` `assums` . - assums : `simple_assums` - : (`simple_assums`) ... (`simple_assums`) - simple_assums : `ident` ... `ident` :[>] `term` - -If the extra ``>`` is present before the type of some assumptions, these -assumptions are declared as coercions. - -Similarly, constructors of inductive types can be declared as coercions at -definition time of the inductive type. This extends and modifies the -grammar of inductive types from Figure :ref:`vernacular` as follows: - -.. - FIXME: - \comindex{Inductive \mbox{\rm (and coercions)}} - \comindex{CoInductive \mbox{\rm (and coercions)}} - -Especially, if the extra ``>`` is present in a constructor -declaration, this constructor is declared as a coercion. +Some objects can be declared as coercions when they are defined. +This applies to :ref:`assumptions<gallina-assumptions>` and +constructors of :ref:`inductive types and record fields<gallina-inductive-definitions>`. +Use :n:`:>` instead of :n:`:` before the +:n:`@type` of the assumption to do so. See :n:`@of_type`. + .. cmd:: Identity Coercion @ident : @class >-> @class diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 1098aa75da..76174e32b5 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -300,70 +300,79 @@ following property: The syntax for adding a new ring is -.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )} - - The :token:`ident` is not relevant. It is used just for error messages. The - :token:`term` is a proof that the ring signature satisfies the (semi-)ring +.. cmd:: Add Ring @ident : @one_term {? ( {+, @ring_mod } ) } + + .. insertprodn ring_mod ring_mod + + .. prodn:: + ring_mod ::= decidable @one_term + | abstract + | morphism @one_term + | constants [ @ltac_expr ] + | preprocess [ @ltac_expr ] + | postprocess [ @ltac_expr ] + | setoid @one_term @one_term + | sign @one_term + | power @one_term [ {+ @qualid } ] + | power_tac @one_term [ @ltac_expr ] + | div @one_term + | closed [ {+ @qualid } ] + + The :n:`@ident` is used only for error messages. The + :n:`@one_term` is a proof that the ring signature satisfies the (semi-)ring axioms. The optional list of modifiers is used to tailor the behavior - of the tactic. The following list describes their syntax and effects: - - .. productionlist:: coq - ring_mod : abstract | decidable `term` | morphism `term` - : setoid `term` `term` - : constants [ `tactic` ] - : preprocess [ `tactic` ] - : postprocess [ `tactic` ] - : power_tac `term` [ `tactic` ] - : sign `term` - : div `term` - - abstract + of the tactic. Here are their effects: + + :n:`abstract` declares the ring as abstract. This is the default. - decidable :n:`@term` + :n:`decidable @one_term` declares the ring as computational. The expression - :n:`@term` is the correctness proof of an equality test ``?=!`` + :n:`@one_term` is the correctness proof of an equality test ``?=!`` (which should be evaluable). Its type should be of the form ``forall x y, x ?=! y = true → x == y``. - morphism :n:`@term` + :n:`morphism @one_term` declares the ring as a customized one. The expression - :n:`@term` is a proof that there exists a morphism between a set of + :n:`@one_term` is a proof that there exists a morphism between a set of coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and ``Ring_theory.semi_morph``). - setoid :n:`@term` :n:`@term` + :n:`setoid @one_term @one_term` forces the use of given setoid. The first - :n:`@term` is a proof that the equality is indeed a setoid (see - ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the + :n:`@one_term` is a proof that the equality is indeed a setoid (see + ``Setoid.Setoid_Theory``), and the second a proof that the ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and ``Ring_theory.sring_eq_ext``). This modifier needs not be used if the setoid and morphisms have been declared. - constants [ :n:`@tactic` ] - specifies a tactic expression :n:`@tactic` that, given a + :n:`constants [ @ltac_expr ]` + specifies a tactic expression :n:`@ltac_expr` 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:`@tactic` ] - specifies a tactic :n:`@tactic` that is applied as a + :n:`preprocess [ @ltac_expr ]` + specifies a tactic :n:`@ltac_expr` 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:`@tactic` ] - specifies a tactic :n:`@tactic` that is applied as a final + :n:`postprocess [ @ltac_expr ]` + specifies a tactic :n:`@ltac_expr` 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:`@tactic` ] + :n:`power @one_term [ {+ @qualid } ]` + to be documented + + :n:`power_tac @one_term @ltac_expr ]` 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 + :math:`x^2` ). The term :n:`@one_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:`@tactic` specifies a tactic expression that, given a term, “abstracts” it into an object of type |N| whose @@ -374,22 +383,25 @@ The syntax for adding a new ring is and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic does not recognize power expressions as ring expressions. - sign :n:`@term` + :n:`sign @one_term` allows :tacn:`ring_simplify` to use a minus operation when outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The term :token:`term` is a proof that a given sign function indicates expressions that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. - div :n:`@term` + :n:`div @one_term` allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with - coefficients other than 1 in the rewriting. The term :n:`@term` is a proof + coefficients other than 1 in the rewriting. The term :n:`@one_term` is a proof that a given division function satisfies the specification of an - euclidean division function (:n:`@term` has to be a proof of + euclidean division function (:n:`@one_term` has to be a proof of ``Ring_theory.div_theory``). For example, this function is called when trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See ``plugins/setoid_ring/InitialRing.v`` for examples of div function. + :n:`closed [ {+ @qualid } ]` + to be documented + Error messages: .. exn:: Bad ring structure. @@ -653,24 +665,27 @@ zero for the correctness of the algorithm. The syntax for adding a new field is -.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )} +.. cmd:: Add Field @ident : @one_term {? ( {+, @field_mod } ) } - The :n:`@ident` is not relevant. It is used just for error - messages. :n:`@term` is a proof that the field signature satisfies the + .. insertprodn field_mod field_mod + + .. prodn:: + field_mod ::= @ring_mod + | completeness @one_term + + The :n:`@ident` is used only for error + messages. :n:`@one_term` is a proof that the field signature satisfies the (semi-)field axioms. The optional list of modifiers is used to tailor the behavior of the tactic. - .. productionlist:: coq - field_mod : `ring_mod` | completeness `term` - Since field tactics are built upon ``ring`` - tactics, all modifiers of the ``Add Ring`` apply. There is only one + tactics, all modifiers of :cmd:`Add Ring` apply. There is only one specific modifier: - completeness :n:`@term` + completeness :n:`@one_term` allows the field tactic to prove automatically that the image of nonzero coefficients are mapped to nonzero - elements of the field. :n:`@term` is a proof of + elements of the field. :n:`@one_term` is a proof of :g:`forall x y, [x] == [y] -> x ?=! y = true`, which is the completeness of equality on coefficients w.r.t. the field equality. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index c069782add..0e326f45d2 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -372,16 +372,11 @@ to universes and explicitly instantiate polymorphic definitions. universe quantification will be discharged on each section definition independently. -.. cmd:: Constraint @universe_constraint - Polymorphic Constraint @universe_constraint +.. cmd:: Constraint @univ_constraint + Polymorphic Constraint @univ_constraint 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 |