Start documenting new [rewrite_strat] tactic that applies rewriting

according to a given strategy.
- Enhance the hints/lemmas strategy to support "using tac" comming from
rewrite hints to solve side-conditions.  


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16558 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 159 insertions, 25 deletions

diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index c0913135c..8a293ea2b 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -1,15 +1,16 @@
 \newtheorem{cscexample}{Example}
 
-\achapter{\protect{User defined equalities and relations}}
+\achapter{\protect{Generalized rewriting}}
 \aauthor{Matthieu Sozeau}
-\tacindex{setoid\_replace}
 \label{setoid_replace}
 
-This chapter presents the extension of several equality related tactics to
-work over user-defined structures (called setoids) that are equipped with
-ad-hoc equivalence relations meant to behave as equalities.
-Actually, the tactics have also been generalized to relations weaker then
-equivalences (e.g. rewriting systems).
+This chapter presents the extension of several equality related tactics
+to work over user-defined structures (called setoids) that are equipped
+with ad-hoc equivalence relations meant to behave as equalities.
+Actually, the tactics have also been generalized to relations weaker
+then equivalences (e.g. rewriting systems). The toolbox also extends the
+automatic rewriting capabilities of the system, allowing to specify
+custom strategies for rewriting.
 
 This documentation is adapted from the previous setoid documentation by
 Claudio Sacerdoti Coen (based on previous work by Cl\'ement Renard).
@@ -43,7 +44,9 @@ the previous implementation in several ways:
   user to customize the proof-search if necessary.
 \end{itemize}
 
-\asection{Relations and morphisms}
+\asection{Introduction to generalized rewriting}
+
+\subsection{Relations and morphisms}
 
 A parametric \emph{relation} \texttt{R} is any term of type
 \texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), relation $A$}. The
@@ -162,7 +165,7 @@ will fail replacing the third occurrence of \texttt{S2} unless \texttt{f}
 has also been declared as a morphism.
 \end{cscexample}
 
-\asection{Adding new relations and morphisms}
+\subsection{Adding new relations and morphisms}
 A parametric relation
 \textit{Aeq}\texttt{: forall ($y_1 : \beta_!$ \ldots $y_m : \beta_m$), relation (A $t_1$ \ldots $t_n$)} over
 \textit{(A : $\alpha_i$ -> \ldots $\alpha_n$ -> }\texttt{Type})
@@ -329,7 +332,7 @@ declaration (see \S\ref{setoid:first-class}) at definition time.
 When loading a compiled file or importing a module,
 all the declarations of this module will be loaded.
 
-\asection{Rewriting and non reflexive relations}
+\subsection{Rewriting and non reflexive relations}
 To replace only one argument of an n-ary morphism it is necessary to prove
 that all the other arguments are related to themselves by the respective
 relation instances.
@@ -360,7 +363,7 @@ non zero elements). Division can be declared as a morphism of signature
 is equivalent to \texttt{n=n $\land$ n$\neq$0}.
 \end{cscexample}
 
-\asection{Rewriting and non symmetric relations}
+\subsection{Rewriting and non symmetric relations}
 When the user works up to relations that are not symmetric, it is no longer
 the case that any covariant morphism argument is also contravariant. As a
 result it is no longer possible to replace a term with a related one in
@@ -408,7 +411,7 @@ is contravariant in its second argument), and finally covariantly in
 is contravariant in its first argument with respect to the relation itself).
 \end{cscexample}
 
-\asection{Rewriting in ambiguous setoid contexts}
+\subsection{Rewriting in ambiguous setoid contexts}
 One function can respect several different relations and thus it can be
 declared as a morphism having multiple signatures.
 
@@ -431,7 +434,8 @@ tactic will always choose the first possible solution to the set of
 constraints generated by a rewrite and will not try to find \emph{all}
 possible solutions to warn the user about.
 
-\asection{First class setoids and morphisms}
+\asection{Commands and tactics}
+\subsection{First class setoids and morphisms}
 \label{setoid:first-class}
 
 The implementation is based on a first-class representation of
@@ -507,7 +511,7 @@ Proof. intros. rewrite H. reflexivity. Qed.
 \end{coq_example*}
 \end{cscexample}
 
-\asection{Tactics enabled on user provided relations}
+\subsection{Tactics enabled on user provided relations}
 \label{setoidtactics}
 The following tactics, all prefixed by \texttt{setoid\_}, 
 deal with arbitrary
@@ -519,20 +523,20 @@ the prefixed tactics it is possible to pass additional arguments such as
 \texttt{using relation}.
 \medskip
 
-\comindex{setoid\_reflexivity}
+\tacindex{setoid\_reflexivity}
 \texttt{setoid\_reflexivity}
 
-\comindex{setoid\_symmetry}
+\tacindex{setoid\_symmetry}
 \texttt{setoid\_symmetry} \zeroone{\texttt{in} \textit{ident}}
 
-\comindex{setoid\_transitivity}
+\tacindex{setoid\_transitivity}
 \texttt{setoid\_transitivity}
 
-\comindex{setoid\_rewrite}
+\tacindex{setoid\_rewrite}
 \texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}
 ~\zeroone{\texttt{at} \textit{occs}} ~\zeroone{\texttt{in} \textit{ident}}
 
-\comindex{setoid\_replace}
+\tacindex{setoid\_replace}
 \texttt{setoid\_replace} \textit{term} \texttt{with} \textit{term}
 ~\zeroone{\texttt{in} \textit{ident}}
 ~\zeroone{\texttt{using relation} \textit{term}}
@@ -557,7 +561,7 @@ not proof of Leibniz equalities. In particular it is possible to exploit
 \texttt{autorewrite} to simulate normalization in a term rewriting system
 up to user defined equalities.
 
-\asection{Printing relations and morphisms}
+\subsection{Printing relations and morphisms}
 The \texttt{Print Instances} command can be used to show the list of
 currently registered \texttt{Reflexive} (using \texttt{Print Instances Reflexive}),
 \texttt{Symmetric} or \texttt{Transitive} relations,
@@ -568,7 +572,7 @@ because the latter is not a composition of morphisms, the \texttt{Print Instance
 commands can be useful to understand what additional morphisms should be
 registered.
 
-\asection{Deprecated syntax and backward incompatibilities}
+\subsection{Deprecated syntax and backward incompatibilities}
 Due to backward compatibility reasons, the following syntax for the
 declaration of setoids and morphisms is also accepted.
 
@@ -607,7 +611,8 @@ contexts that were refused by the old implementation. As discussed in
 the next section, the semantics of the new \texttt{setoid\_rewrite}
 command differs slightly from the old one and \texttt{rewrite}.
 
-\asection{Rewriting under binders}
+\asection{Extensions}
+\subsection{Rewriting under binders}
 
 \textbf{Warning}: Due to compatibility issues, this feature is enabled only when calling 
 the \texttt{setoid\_rewrite} tactics directly and not \texttt{rewrite}.
@@ -678,7 +683,7 @@ and in its local environment, and all matches are rewritten
 \texttt{setoid\_rewrite} implementation can almost be recovered using
 the \texttt{at 1} modifier.
 
-\asection{Sub-relations}
+\subsection{Sub-relations}
 
 Sub-relations can be used to specify that one relation is included in
 another, so that morphisms signatures for one can be used for the other.
@@ -698,14 +703,136 @@ any rewriting constraints arising from a rewrite using \texttt{iff},
 Sub-relations are implemented in \texttt{Classes.Morphisms} and are a 
 prime example of a mostly user-space extension of the algorithm.
 
-\asection{Constant unfolding}
+\subsection{Constant unfolding}
 
 The resolution tactic is based on type classes and hence regards user-defined 
 constants as transparent by default. This may slow down the resolution
 due to a lot of unifications (all the declared \texttt{Proper}
 instances are tried at each node of the search tree).
 To speed it up, declare your constant as rigid for proof search
-using the command \texttt{Typeclasses Opaque} (see \S \ref{TypeclassesTransparency}).
+using the command \texttt{Typeclasses Opaque} (see \S
+\ref{TypeclassesTransparency}).
+
+\asection{Strategies for rewriting}
+
+\subsection{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 $\texttt{rewrite\_strat}~s$ where $s$ is a strategy
+expression. Strategies are defined inductively as described by the
+following grammar:
+
+\def\str#1{\texttt{#1}}
+
+\def\strline#1#2{& \vert & #1 & \text{#2}}
+\def\strlinea#1#2#3{& \vert & \str{#1}~#2 & \text{#3}}
+
+\[\begin{array}{lcll}
+  s, t, u & ::= & ( s ) & \text{strategy} \\
+  \strline{c}{lemma} \\
+  \strline{\str{<-}~c}{lemma, right-to-left} \\
+
+  \strline{\str{fail}}{failure} \\
+  \strline{\str{id}}{identity} \\
+  \strline{\str{refl}}{reflexivity} \\
+  \strlinea{progress}{s}{progress} \\
+  \strlinea{try}{s}{failure catch} \\
+
+  \strline{s~\str{;}~u}{composition} \\
+  \strline{\str{choice}~s~t}{left-biased choice} \\
+
+  \strlinea{repeat}{s}{iteration (+)} \\
+  \strlinea{any}{s}{iteration (*)} \\
+  
+  \strlinea{subterm}{s}{one subterm} \\
+  \strlinea{subterms}{s}{all subterms} \\
+  \strlinea{innermost}{s}{innermost first} \\
+  \strlinea{outermost}{s}{outermost first}\\
+  \strlinea{bottomup}{s}{bottom-up} \\
+  \strlinea{topdown}{s}{top-down} \\
+
+  \strlinea{hints}{hintdb}{apply hint} \\
+  \strlinea{terms}{c \ldots c}{any of the terms}\\
+  \strlinea{eval}{redexpr}{apply reduction}\\
+  \strlinea{fold}{c}{fold expression}
+\end{array}\]
+
+Actually a few of these are defined in term of the others using
+a primitive fixpoint operator:
+
+\[\begin{array}{lcl}
+  \str{try}~s & = & \str{choice}~s~\str{id} \\
+  \str{any}~s & = & \str{fix}~u. \str{try}~(s~\str{;}~u) \\
+  \str{repeat}~s & = & s~\str{;}~\str{any}~s \\
+  \str{bottomup}~s & = &
+  \str{fix}~bu. (\str{choice}~(\str{progress}~(\str{subterms}~bu))~s)~\str{;}~\str{try}~bu \\
+  \str{topdown}~s & = &
+  \str{fix}~td. (\str{choice}~s~(\str{progress}~(\str{subterms}~td)))~\str{;}~\str{try}~td \\
+  \str{innermost}~s & = &  \str{fix}~i. (\str{choice}~(\str{subterm}~i)~s) \\
+  \str{outermost}~s & = &
+  \str{fix}~o. (\str{choice}~s~(\str{subterm}~o))
+\end{array}\]
+
+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
+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 was made, while \str{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 \str{repeat} and at least 0 times using
+\str{any}.
+
+The \str{subterm} and \str{subterms} strategies apply their argument
+strategy $s$ to respectively one or all subterms of the current term
+under consideration, left-to-right. \str{subterm} stops at the first
+subterm for which $s$ made progress. The composite strategies
+\str{innermost} and \str{outermost} perform a single innermost our outermost
+rewrite using their argument strategy. Their counterparts
+\str{bottomup} and \str{topdown} perform as many rewritings as possible,
+starting from the bottom or the top of the term. 
+
+Hint databases created for \texttt{autorewrite} can also be used by
+\texttt{rewrite\_strat} using the \str{hints} strategy that applies any
+of the lemmas at the current subterm. The \str{terms} strategy takes the
+lemma names directly as arguments. The \str{eval} strategy expects a
+reduction expression (see \S\ref{Conversion-tactics}) and succeeds if it
+reduces the subterm under consideration. The \str{fold} strategy takes a
+term $c$ and tries to \emph{unify} it to the current subterm, converting
+it to $c$ on success, it is stronger than the tactic \texttt{fold}. 
+
+
+\subsection{Usage}
+\tacindex{rewrite\_strat}
+
+\texttt{rewrite\_strat}~\textit{s}~\zeroone{\texttt{in} \textit{ident}}: 
+
+  Rewrite using the strategy \textit{s} in hypothesis \textit{ident}
+  or the conclusion.
+
+  \begin{ErrMsgs}
+  \item  \errindex{Nothing to rewrite}. If the strategy failed. 
+  \item  \errindex{No progress made}. If the strategy succeeded but
+    made no progress.
+  \item  \errindex{Unable to satisfy the rewriting constraints}. 
+    If the strategy succeeded and made progress but the corresponding
+    rewriting constraints are not satisfied.
+  \end{ErrMsgs}
+  
+
+The \texttt{setoid\_rewrite}~c tactic is basically equivalent to 
+\texttt{rewrite\_strat}~(\str{outermost}~c).
+
+
+
+
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 192a96998..3715c4c79 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -786,6 +786,13 @@ of the {ML} language},
   year        = {1990}
 }
 
+@inproceedings{Luttik97specificationof,
+	Author = {Sebastiaan P. Luttik and Eelco Visser},
+	Booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing},
+	Publisher = {Springer-Verlag},
+	Title = {Specification of Rewriting Strategies},
+	Year = {1997}}
+
 @Book{MaL84,
   author      = {{P. Martin-L\"of}},
   publisher   = {Bibliopolis},