diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 11:04:08 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 11:04:08 +0200 |
commit | d2533da244f770261478ae829167cb3a8ad38038 (patch) | |
tree | 0d70bcf3c5614e8750af006d95105e088022d1f3 /doc/sphinx/proof-engine | |
parent | 8a570b6830d5f42c29c36df13c10a8550120641b (diff) | |
parent | a75914f098a66bd628b162e6d9e8614451c9c8aa (diff) |
Merge PR #7508: Improve rewrite section in tactic chapter.
Diffstat (limited to 'doc/sphinx/proof-engine')
-rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 266 |
1 files changed, 127 insertions, 139 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 3835524f0..da4c3f9d7 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2398,35 +2398,35 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacn:: rewrite @term :name: rewrite -This tactic applies to any goal. The type of :n:`@term` must have the form + This tactic applies to any goal. The type of :token:`term` must have the form -``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``). eq term``:sub:`1` ``term``:sub:`2` ``.`` + ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``). eq term``:sub:`1` ``term``:sub:`2` ``.`` -where :g:`eq` is the Leibniz equality or a registered setoid equality. + where :g:`eq` is the Leibniz equality or a registered setoid equality. -Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, -resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then -replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. -Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, -and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new -subgoals. + Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, + resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then + replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. + Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, + and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new + subgoals. -.. exn:: The @term provided does not end with an equation. + .. exn:: The @term provided does not end with an equation. -.. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. + .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. -.. tacv:: rewrite -> @term + .. tacv:: rewrite -> @term - Is equivalent to :n:`rewrite @term` + Is equivalent to :n:`rewrite @term` -.. tacv:: rewrite <- @term + .. tacv:: rewrite <- @term - Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left + Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left -.. tacv:: rewrite @term in clause + .. tacv:: rewrite @term in clause - Analogous to :n:`rewrite @term` but rewriting is done following clause - (similarly to :ref:`performing computations <performingcomputations>`). For instance: + Analogous to :n:`rewrite @term` but rewriting is done following clause + (similarly to :ref:`performing computations <performingcomputations>`). For instance: + :n:`rewrite H in H`:sub:`1` will rewrite `H` in the hypothesis `H`:sub:`1` instead of the current goal. @@ -2440,136 +2440,128 @@ subgoals. + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` that succeeds if at least one of these two tactics succeeds. - Orientation :g:`->` or :g:`<-` can be inserted before the :n:`@term` to rewrite. + Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. -.. tacv:: rewrite @term at occurrences + .. tacv:: rewrite @term at occurrences - Rewrite only the given occurrences of :n:`@term`. Occurrences are - specified from left to right as for pattern (:tacn:`pattern`). The rewrite is - always performed using setoid rewriting, even for Leibniz’s equality, so one - has to ``Import Setoid`` to use this variant. + Rewrite only the given occurrences of :token:`term`. Occurrences are + specified from left to right as for pattern (:tacn:`pattern`). The rewrite is + always performed using setoid rewriting, even for Leibniz’s equality, so one + has to ``Import Setoid`` to use this variant. -.. tacv:: rewrite @term by tactic + .. tacv:: rewrite @term by tactic - Use tactic to completely solve the side-conditions arising from the - :tacn:`rewrite`. + Use tactic to completely solve the side-conditions arising from the + :tacn:`rewrite`. -.. tacv:: rewrite {+ @term} + .. tacv:: rewrite {+, @term} - Is equivalent to the `n` successive tactics :n:`{+ rewrite @term}`, each one - working on the first subgoal generated by the previous one. Orientation - :g:`->` or :g:`<-` can be inserted before each :n:`@term` to rewrite. One - unique clause can be added at the end after the keyword in; it will then - affect all rewrite operations. + Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one + working on the first subgoal generated by the previous one. Orientation + :g:`->` or :g:`<-` can be inserted before each :token:`term` to rewrite. One + unique clause can be added at the end after the keyword in; it will then + affect all rewrite operations. - In all forms of rewrite described above, a :n:`@term` to rewrite can be - immediately prefixed by one of the following modifiers: + In all forms of rewrite described above, a :token:`term` to rewrite can be + immediately prefixed by one of the following modifiers: - + `?` : the tactic rewrite :n:`?@term` performs the rewrite of :n:`@term` as many - times as possible (perhaps zero time). This form never fails. - + `n?` : works similarly, except that it will do at most `n` rewrites. - + `!` : works as ?, except that at least one rewrite should succeed, otherwise - the tactic fails. - + `n!` (or simply `n`) : precisely `n` rewrites of :n:`@term` will be done, - leading to failure if these n rewrites are not possible. + + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many + times as possible (perhaps zero time). This form never fails. + + :n:`@num?` : works similarly, except that it will do at most :token:`num` rewrites. + + `!` : works as `?`, except that at least one rewrite should succeed, otherwise + the tactic fails. + + :n:`@num!` (or simply :n:`@num`) : precisely :token:`num` rewrites of :token:`term` will be done, + leading to failure if these :token:`num` rewrites are not possible. -.. tacv:: erewrite @term - :name: erewrite + .. tacv:: erewrite @term + :name: erewrite - This tactic works as :n:`rewrite @term` but turning - unresolved bindings into existential variables, if any, instead of - failing. It has the same variants as :tacn:`rewrite` has. + This tactic works as :n:`rewrite @term` but turning + unresolved bindings into existential variables, if any, instead of + failing. It has the same variants as :tacn:`rewrite` has. -.. tacn:: replace @term with @term +.. tacn:: replace @term with @term’ :name: replace This tactic applies to any goal. It replaces all free occurrences of :n:`@term` - in the current goal with :n:`@term` and generates the equality :n:`@term = - @term` as a subgoal. This equality is automatically solved if it occurs among - the assumption, or if its symmetric form occurs. It is equivalent to - :n:`cut @term = @term; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. + in the current goal with :n:`@term’` and generates an equality :n:`@term = @term’` + as a subgoal. This equality is automatically solved if it occurs among + the assumptions, or if its symmetric form occurs. It is equivalent to + :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. -.. exn:: @terms do not have convertible types. + .. exn:: Terms do not have convertible types. -.. tacv:: replace @term with @term by tactic + .. tacv:: replace @term with @term’ by @tactic - This acts as :n:`replace @term` with :n:`@term` but applies tactic to solve the generated - subgoal :n:`@term = @term`. + This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated + subgoal :n:`@term = @term’`. -.. tacv:: replace @term + .. tacv:: replace @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` or :n:`@term’ = @term`. + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` or :n:`@term’ = @term`. -.. tacv:: replace -> @term + .. tacv:: replace -> @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` -.. tacv:: replace <- @term + .. tacv:: replace <- @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term’ = @term` + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term’ = @term` -.. tacv:: replace @term with @term in clause -.. tacv:: replace @term with @term in clause by tactic -.. tacv:: replace @term in clause replace -> @term in clause -.. tacv:: replace <- @term in clause + .. tacv:: replace @term {? with @term} in clause {? by @tactic} + .. tacv:: replace -> @term in clause + .. tacv:: replace <- @term in clause - Acts as before but the replacements take place inclause (see - :ref:`performingcomputations`) and not only in the conclusion of the goal. The - clause argument must not contain any type of nor value of. + Acts as before but the replacements take place in the specified clause (see + :ref:`performingcomputations`) and not only in the conclusion of the goal. The + clause argument must not contain any ``type of`` nor ``value of``. -.. tacv:: cutrewrite <- (@term = @term) - :cutrewrite: + .. tacv:: cutrewrite <- (@term = @term’) + :name: cutrewrite - This tactic is deprecated. It acts like :n:`replace @term with @term`, or, - equivalently as :n:`enough (@term = @term) as <-`. + This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as <-`. -.. tacv:: cutrewrite -> (@term = @term) + .. tacv:: cutrewrite -> (@term = @term’) - This tactic is deprecated. It can be replaced by enough :n:`(@term = @term) as ->`. + This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as ->`. .. tacn:: subst @ident :name: subst + This tactic applies to a goal that has :n:`@ident` in its context and (at + least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` + with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by + :g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and + clears :n:`@ident` and :g:`H` from the context. -This tactic applies to a goal that has :n:`@ident` in its context and (at -least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` -with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by -:g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and -clears :n:`@ident` and :g:`H` from the context. - -If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also -unfolded and cleared. - - -.. note:: - When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the - first one is used. - - -.. note:: - If `H` is itself dependent in the goal, it is replaced by the proof of - reflexivity of equality. + If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also + unfolded and cleared. + .. note:: + + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the + first one is used. -.. tacv:: subst {+ @ident} + + If :g:`H` is itself dependent in the goal, it is replaced by the proof of + reflexivity of equality. - This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. + .. tacv:: subst {+ @ident} -.. tacv:: subst + This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. - This applies subst repeatedly from top to bottom to all identifiers of the - context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` - or :n:`@ident := t` exists, with :n:`@ident` not occurring in `t`. + .. tacv:: subst + This applies subst repeatedly from top to bottom to all identifiers of the + context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` + or :n:`@ident := t` exists, with :n:`@ident` not occurring in ``t``. .. opt:: Regular Subst Tactic This option controls the behavior of :tacn:`subst`. When it is - activated, :tacn:`subst` also deals with the following corner cases: + activated (it is by default), :tacn:`subst` also deals with the following corner cases: + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not @@ -2587,41 +2579,40 @@ unfolded and cleared. unfolded which otherwise it would exceptionally unfold in configurations containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` with `u′` not a variable. Finally, it preserves the initial order of - hypotheses, which without the option it may break. The option is on by + hypotheses, which without the option it may break. default. .. tacn:: stepl @term :name: stepl + This tactic is for chaining rewriting steps. It assumes a goal of the + form :n:`R @term @term` where ``R`` is a binary relation and relies on a + database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` + where `eq` is typically a setoid equality. The application of :n:`stepl @term` + then replaces the goal by :n:`R @term @term` and adds a new goal stating + :n:`eq @term @term`. -This tactic is for chaining rewriting steps. It assumes a goal of the -form :n:`R @term @term` where `R` is a binary relation and relies on a -database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` -where `eq` is typically a setoid equality. The application of :n:`stepl @term` -then replaces the goal by :n:`R @term @term` and adds a new goal stating -:n:`eq @term @term`. + .. cmd:: Declare Left Step @term -.. cmd:: Declare Left Step @term + Adds :n:`@term` to the database used by :tacn:`stepl`. - Adds :n:`@term` to the database used by :tacn:`stepl`. + The tactic is especially useful for parametric setoids which are not accepted + as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see + :ref:`Generalizedrewriting`). -The tactic is especially useful for parametric setoids which are not accepted -as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see -:ref:`Generalizedrewriting`). + .. tacv:: stepl @term by @tactic -.. tacv:: stepl @term by tactic + This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. - This applies :n:`stepl @term` then applies tactic to the second goal. + .. tacv:: stepr @term stepr @term by tactic + :name: stepr -.. tacv:: stepr @term stepr @term by tactic - :name: stepr + This behaves as :tacn:`stepl` but on the right-hand-side of the binary + relation. Lemmas are expected to be of the form + :g:`forall x y z, R x y -> eq y z -> R x z`. - This behaves as :tacn:`stepl` but on the right-hand-side of the binary - relation. Lemmas are expected to be of the form :g:`forall x y z, R x y -> eq - y z -> R x z`. - - .. cmd:: Declare Right Step @term + .. cmd:: Declare Right Step @term Adds :n:`@term` to the database used by :tacn:`stepr`. @@ -2634,28 +2625,25 @@ as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see with `U` providing that `U` is well-formed and that `T` and `U` are convertible. -.. exn:: Not convertible. - + .. exn:: Not convertible. -.. tacv:: change @term with @term + .. tacv:: change @term with @term’ - This replaces the occurrences of :n:`@term` by :n:`@term` in the current goal. - The term :n:`@term` and :n:`@term` must be convertible. + This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. + The term :n:`@term` and :n:`@term’` must be convertible. -.. tacv:: change @term at {+ @num} with @term + .. tacv:: change @term at {+ @num} with @term’ - This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term by @term` - in the current goal. The terms :n:`@term` and :n:`@term` must be convertible. + This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term` by :n:`@term’` + in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. -.. exn:: Too few occurrences. + .. exn:: Too few occurrences. -.. tacv:: change @term in @ident -.. tacv:: change @term with @term in @ident -.. tacv:: change @term at {+ @num} with @term in @ident + .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident - This applies the change tactic not to the goal but to the hypothesis :n:`@ident`. + This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. -See also: :ref:`Performing computations <performingcomputations>` + .. seealso:: :ref:`Performing computations <performingcomputations>` .. _performingcomputations: @@ -3434,7 +3422,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Adds each :n:`Hint Unfold @ident`. .. cmdv:: Hint %( Transparent %| Opaque %) @qualid - :name: Hint %( Transparent %| Opaque %) + :name: Hint ( Transparent | Opaque ) This adds a transparency hint to the database, making :n:`@qualid` a transparent or opaque constant during resolution. This information is used |