diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 59 |
3 files changed, 56 insertions, 11 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 3bd85d29c8..5d471c695c 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -31,9 +31,11 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, .. flag:: Simplex + .. deprecated:: 8.14 + This flag (set by default) instructs the decision procedures to - use the Simplex method for solving linear goals. If it is not set, - the decision procedures are using Fourier elimination. + use the Simplex method for solving linear goals instead of the + deprecated Fourier elimination. .. opt:: Dump Arith diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index 8dbc1626ba..7566996ef6 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -9,7 +9,7 @@ Binders .. insertprodn open_binders binder .. prodn:: - open_binders ::= {+ @name } : @term + open_binders ::= {+ @name } : @type | {+ @binder } name ::= _ | @ident diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 663337bc64..f286533d78 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -44,11 +44,14 @@ Rewriting with Leibniz and setoid equality oriented_rewriter ::= {? {| -> | <- } } {? @natural } {? {| ? | ! } } @one_term_with_bindings one_term_with_bindings ::= {? > } @one_term {? with @bindings } - Rewrites terms based on equalities. The type of :n:`@one_term` must have the form: + Replaces subterms with other subterms that have been proven to be equal. + The type of :n:`@one_term` must have the form: :n:`{? forall {+ (x__i: A__i) } , } EQ @term__1 @term__2` - where :g:`EQ` is the Leibniz equality `eq` or a registered setoid equality. + .. todo :term:`Leibniz equality` does not work with Sphinx 2.3.1. It does with Sphinx 3.0.3. + + where :g:`EQ` is the Leibniz equality `eq` or a registered :term:`setoid equality`. Note that :n:`eq @term__1 @term__2` is typically written with the infix notation :n:`@term__1 = @term__2`. You must `Require Setoid` to use the tactic with a setoid equality or with :ref:`setoid rewriting <generalizedrewriting>`. @@ -61,7 +64,7 @@ Rewriting with Leibniz and setoid equality Some of the variables :g:`x`\ :sub:`i` are solved by unification, and some of the types :n:`A__1, ..., A__n` may become new subgoals. :tacn:`rewrite` won't find occurrences inside `forall` that refer - to variables bound by the `forall`; use :tacn:`setoid_rewrite` + to variables bound by the `forall`; use the more advanced :tacn:`setoid_rewrite` if you want to find such occurrences. :n:`{+, @oriented_rewriter }` @@ -90,15 +93,55 @@ Rewriting with Leibniz and setoid equality any of them can be rewritten. If not specified, only the first occurrence in the conclusion is replaced. - If :n:`at @occs_nums` is specified, rewriting is always done with - :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality, - which means that you must `Require Setoid` to use that form. - However, note that :tacn:`rewrite` (even when using setoid rewriting) and - :tacn:`setoid_rewrite` don't behave identically (as already mentioned above). + .. note:: + + If :n:`at @occs_nums` is specified, rewriting is always done + with :ref:`setoid rewriting <generalizedrewriting>`, even for + Leibniz equality, which means that you must `Require + Setoid` to use that form. However, note that :tacn:`rewrite` + (even when using setoid rewriting) and :tacn:`setoid_rewrite` + don't behave identically (as is noted above and below). :n:`by @ltac_expr3` If specified, is used to resolve all side conditions generated by the tactic. + .. note:: + + For each selected hypothesis and/or the conclusion, + :tacn:`rewrite` finds the first matching subterm in + depth-first search order. Only subterms identical to + that first matched subterm are rewritten. If the `at` clause is specified, + only these subterms are considered when counting occurrences. + To select a different set of matching subterms, you can + specify how some or all of the free variables are bound by + using a `with` clause (see :n:`@one_term_with_bindings`). + + For instance, if we want to rewrite the right-hand side in the + following goal, this will not work: + + .. coqtop:: none + + Require Import Arith. + + .. coqtop:: out + + Lemma example x y : x + y = y + x. + + .. coqtop:: all fail + + rewrite Nat.add_comm at 2. + + One can explicitly specify how some variables are bound to match + a different subterm: + + .. coqtop:: all abort + + rewrite Nat.add_comm with (m := x). + + Note that the more advanced :tacn:`setoid_rewrite` tactic + behaves differently, and thus the number of occurrences + available to rewrite may differ between the two tactics. + .. exn:: Tactic failure: Setoid library not loaded. :undocumented: |