From e9acdf4a5682cdda0044c1d2048b2c8f0a8161bd Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Mar 2018 15:13:45 +0100 Subject: [Sphinx] Move chapter 27 to new infrastructure --- Makefile.doc | 2 +- doc/refman/Reference-Manual.tex | 1 - doc/refman/Setoid.tex | 842 -------------------------- doc/sphinx/addendum/generalized-rewriting.rst | 842 ++++++++++++++++++++++++++ 4 files changed, 843 insertions(+), 844 deletions(-) delete mode 100644 doc/refman/Setoid.tex create mode 100644 doc/sphinx/addendum/generalized-rewriting.rst diff --git a/Makefile.doc b/Makefile.doc index 8dd73a153..ecc68979e 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,7 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Setoid.v.tex Universes.v.tex \ + Universes.v.tex \ Misc.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 57d867060..cfb3c625b 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -117,7 +117,6 @@ Options A and B of the licence are {\em not} elected.} %END LATEX \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% -\include{Setoid.v}% Tactique pour les setoides \include{AsyncProofs}% Paral-ITP \include{Universes.v}% Universe polymorphes \include{Misc.v} diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex deleted file mode 100644 index b7b343112..000000000 --- a/doc/refman/Setoid.tex +++ /dev/null @@ -1,842 +0,0 @@ -\newtheorem{cscexample}{Example} - -\achapter{\protect{Generalized rewriting}} -%HEVEA\cutname{setoid.html} -\aauthor{Matthieu Sozeau} -\label{setoids} - -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 the specification of -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). -The new implementation is a drop-in replacement for the old one,\footnote{Nicolas -Tabareau helped with the gluing.} hence most of the documentation still applies. - -The work is a complete rewrite of the previous implementation, based on -the type class infrastructure. It also improves on and generalizes -the previous implementation in several ways: -\begin{itemize} -\item User-extensible algorithm. The algorithm is separated in two - parts: generations of the rewriting constraints (done in ML) and - solving of these constraints using type class resolution. As type - class resolution is extensible using tactics, this allows users to define - general ways to solve morphism constraints. -\item Sub-relations. An example extension to the base algorithm is the - ability to define one relation as a subrelation of another so that - morphism declarations on one relation can be used automatically for - the other. This is done purely using tactics and type class search. -\item Rewriting under binders. It is possible to rewrite under binders - in the new implementation, if one provides the proper - morphisms. Again, most of the work is handled in the tactics. -\item First-class morphisms and signatures. Signatures and morphisms are - ordinary Coq terms, hence they can be manipulated inside Coq, put - inside structures and lemmas about them can be proved inside the - system. Higher-order morphisms are also allowed. -\item Performance. The implementation is based on a depth-first search for the first - solution to a set of constraints which can be as fast as linear in the - size of the term, and the size of the proof term is linear - in the size of the original term. Besides, the extensibility allows the - user to customize the proof search if necessary. -\end{itemize} - -\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 -expression $A$, which depends on $x_1$ \ldots $x_n$, is called the -\emph{carrier} of the relation and \texttt{R} is -said to be a relation over \texttt{A}; the list $x_1,\ldots,x_n$ -is the (possibly empty) list of parameters of the relation. - -\firstexample -\begin{cscexample}[Parametric relation] -It is possible to implement finite sets of elements of type \texttt{A} -as unordered list of elements of type \texttt{A}. The function -\texttt{set\_eq: forall (A: Type), relation (list A)} satisfied by two lists -with the same elements is a parametric relation over \texttt{(list A)} with -one parameter \texttt{A}. The type of \texttt{set\_eq} is convertible with -\texttt{forall (A: Type), list A -> list A -> Prop}. -\end{cscexample} - -An \emph{instance} of a parametric relation \texttt{R} with $n$ parameters -is any term \texttt{(R $t_1$ \ldots $t_n$)}. - -Let \texttt{R} be a relation over \texttt{A} with $n$ parameters. -A term is a parametric proof of reflexivity for \texttt{R} if it has type -\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), - reflexive (R $x_1$ \ldots $x_n$)}. Similar definitions are given for -parametric proofs of symmetry and transitivity. - -\begin{cscexample}[Parametric relation (cont.)] -The \texttt{set\_eq} relation of the previous example can be proved to be -reflexive, symmetric and transitive. -\end{cscexample} - -A parametric unary function $f$ of type -\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), $A_1$ -> $A_2$} -covariantly respects two parametric relation instances $R_1$ and $R_2$ if, -whenever $x, y$ satisfy $R_1~x~y$, their images $(f~x)$ and $(f~y)$ -satisfy $R_2~(f~x)~(f~y)$ . An $f$ that respects its input and output relations -will be called a unary covariant \emph{morphism}. We can also say that $f$ is -a monotone function with respect to $R_1$ and $R_2$. -The sequence $x_1,\ldots x_n$ represents the parameters of the morphism. - -Let $R_1$ and $R_2$ be two parametric relations. -The \emph{signature} of a parametric morphism of type -\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), $A_1$ -> $A_2$} that -covariantly respects two instances $I_{R_1}$ and $I_{R_2}$ of $R_1$ and $R_2$ is written $I_{R_1} \texttt{++>} I_{R_2}$. -Notice that the special arrow \texttt{++>}, which reminds the reader -of covariance, is placed between the two relation instances, not -between the two carriers. The signature relation instances and morphism will -be typed in a context introducing variables for the parameters. - -The previous definitions are extended straightforwardly to $n$-ary morphisms, -that are required to be simultaneously monotone on every argument. - -Morphisms can also be contravariant in one or more of their arguments. -A morphism is contravariant on an argument associated to the relation instance -$R$ if it is covariant on the same argument when the inverse relation -$R^{-1}$ (\texttt{inverse R} in Coq) is considered. -The special arrow \texttt{-{}->} is used in signatures -for contravariant morphisms. - -Functions having arguments related by symmetric relations instances are both -covariant and contravariant in those arguments. The special arrow -\texttt{==>} is used in signatures for morphisms that are both covariant -and contravariant. - -An instance of a parametric morphism $f$ with $n$ parameters is any term -\texttt{f $t_1$ \ldots $t_n$}. - -\begin{cscexample}[Morphisms] -Continuing the previous example, let -\texttt{union: forall (A: Type), list A -> list A -> list A} perform the union -of two sets by appending one list to the other. \texttt{union} is a binary -morphism parametric over \texttt{A} that respects the relation instance -\texttt{(set\_eq A)}. The latter condition is proved by showing -\texttt{forall (A: Type) (S1 S1' S2 S2': list A), set\_eq A S1 S1' -> - set\_eq A S2 S2' -> set\_eq A (union A S1 S2) (union A S1' S2')}. - -The signature of the function \texttt{union A} is -\texttt{set\_eq A ==> set\_eq A ==> set\_eq A} for all \texttt{A}. -\end{cscexample} - -\begin{cscexample}[Contravariant morphism] -The division function \texttt{Rdiv: R -> R -> R} is a morphism of -signature \texttt{le ++> le -{}-> le} where \texttt{le} is -the usual order relation over real numbers. Notice that division is -covariant in its first argument and contravariant in its second -argument. -\end{cscexample} - -Leibniz equality is a relation and every function is a -morphism that respects Leibniz equality. Unfortunately, Leibniz equality -is not always the intended equality for a given structure. - -In the next section we will describe the commands to register terms as -parametric relations and morphisms. Several tactics that deal with equality -in \Coq\ can also work with the registered relations. -The exact list of tactic will be given in Sect.~\ref{setoidtactics}. -For instance, the -tactic \texttt{reflexivity} can be used to close a goal $R~n~n$ whenever -$R$ is an instance of a registered reflexive relation. However, the tactics -that replace in a context $C[]$ one term with another one related by $R$ -must verify that $C[]$ is a morphism that respects the intended relation. -Currently the verification consists in checking whether $C[]$ is a syntactic -composition of morphism instances that respects some obvious -compatibility constraints. - -\begin{cscexample}[Rewriting] -Continuing the previous examples, suppose that the user must prove -\texttt{set\_eq int (union int (union int S1 S2) S2) (f S1 S2)} under the -hypothesis \texttt{H: set\_eq int S2 (@nil int)}. It is possible to -use the \texttt{rewrite} tactic to replace the first two occurrences of -\texttt{S2} with \texttt{@nil int} in the goal since the context -\texttt{set\_eq int (union int (union int S1 nil) nil) (f S1 S2)}, being -a composition of morphisms instances, is a morphism. However the tactic -will fail replacing the third occurrence of \texttt{S2} unless \texttt{f} -has also been declared as a morphism. -\end{cscexample} - -\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}) -can be declared with the following command: - -\comindex{Add Parametric Relation} -\begin{quote} - \texttt{Add Parametric Relation} ($x_1 : T_1$) \ldots ($x_n : T_k$) : - \textit{(A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots $t'_m$)}\\ - ~\zeroone{\texttt{reflexivity proved by} \textit{refl}}\\ - ~\zeroone{\texttt{symmetry proved by} \textit{sym}}\\ - ~\zeroone{\texttt{transitivity proved by} \textit{trans}}\\ - \texttt{~as} \textit{id}. -\end{quote} -after having required the \texttt{Setoid} module with the -\texttt{Require Setoid} command. - -The identifier \textit{id} gives a unique name to the morphism and it is -used by the command to generate fresh names for automatically provided lemmas -used internally. - -Notice that the carrier and relation parameters may refer to the context -of variables introduced at the beginning of the declaration, but the -instances need not be made only of variables. -Also notice that \textit{A} is \emph{not} required to be a term -having the same parameters as \textit{Aeq}, although that is often the -case in practice (this departs from the previous implementation). - -\comindex{Add Relation} -In case the carrier and relations are not parametric, one can use the -command \texttt{Add Relation} instead, whose syntax is the same except -there is no local context. - -The proofs of reflexivity, symmetry and transitivity can be omitted if the -relation is not an equivalence relation. The proofs must be instances of the -corresponding relation definitions: e.g. the proof of reflexivity must -have a type convertible to \texttt{reflexive (A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots - $t'_n$)}. Each proof may refer to the introduced variables as well. - -\begin{cscexample}[Parametric relation] -For Leibniz equality, we may declare: -\texttt{Add Parametric Relation (A : Type) :} \texttt{A (@eq A)}\\ -~\zeroone{\texttt{reflexivity proved by} \texttt{@refl\_equal A}}\\ -\ldots -\end{cscexample} - -Some tactics -(\texttt{reflexivity}, \texttt{symmetry}, \texttt{transitivity}) work only -on relations that respect the expected properties. The remaining tactics -(\texttt{replace}, \texttt{rewrite} and derived tactics such as -\texttt{autorewrite}) do not require any properties over the relation. -However, they are able to replace terms with related ones only in contexts -that are syntactic compositions of parametric morphism instances declared with -the following command. - -\comindex{Add Parametric Morphism} -\begin{quote} - \texttt{Add Parametric Morphism} ($x_1 : \T_1$) \ldots ($x_k : \T_k$) : - (\textit{f $t_1$ \ldots $t_n$})\\ - \texttt{~with signature} \textit{sig}\\ - \texttt{~as id}.\\ - \texttt{Proof}\\ - ~\ldots\\ - \texttt{Qed} -\end{quote} - -The command declares \textit{f} as a parametric morphism of signature -\textit{sig}. The identifier \textit{id} gives a unique name to the morphism -and it is used as the base name of the type class instance definition -and as the name of the lemma that proves the well-definedness of the morphism. -The parameters of the morphism as well as the signature may refer to the -context of variables. -The command asks the user to prove interactively that \textit{f} respects -the relations identified from the signature. - -\begin{cscexample} -We start the example by assuming a small theory over homogeneous sets and -we declare set equality as a parametric equivalence relation and -union of two sets as a parametric morphism. -\begin{coq_example*} -Require Export Setoid. -Require Export Relation_Definitions. -Set Implicit Arguments. -Parameter set: Type -> Type. -Parameter empty: forall A, set A. -Parameter eq_set: forall A, set A -> set A -> Prop. -Parameter union: forall A, set A -> set A -> set A. -Axiom eq_set_refl: forall A, reflexive _ (eq_set (A:=A)). -Axiom eq_set_sym: forall A, symmetric _ (eq_set (A:=A)). -Axiom eq_set_trans: forall A, transitive _ (eq_set (A:=A)). -Axiom empty_neutral: forall A (S: set A), eq_set (union S (empty A)) S. -Axiom union_compat: - forall (A : Type), - forall x x' : set A, eq_set x x' -> - forall y y' : set A, eq_set y y' -> - eq_set (union x y) (union x' y'). -Add Parametric Relation A : (set A) (@eq_set A) - reflexivity proved by (eq_set_refl (A:=A)) - symmetry proved by (eq_set_sym (A:=A)) - transitivity proved by (eq_set_trans (A:=A)) - as eq_set_rel. -Add Parametric Morphism A : (@union A) with -signature (@eq_set A) ==> (@eq_set A) ==> (@eq_set A) as union_mor. -Proof. exact (@union_compat A). Qed. -\end{coq_example*} - -\end{cscexample} - -It is possible to reduce the burden of specifying parameters using -(maximally inserted) implicit arguments. If \texttt{A} is always set as -maximally implicit in the previous example, one can write: - -\begin{coq_eval} -Reset Initial. -Require Export Setoid. -Require Export Relation_Definitions. -Parameter set: Type -> Type. -Parameter empty: forall {A}, set A. -Parameter eq_set: forall {A}, set A -> set A -> Prop. -Parameter union: forall {A}, set A -> set A -> set A. -Axiom eq_set_refl: forall {A}, reflexive (set A) eq_set. -Axiom eq_set_sym: forall {A}, symmetric (set A) eq_set. -Axiom eq_set_trans: forall {A}, transitive (set A) eq_set. -Axiom empty_neutral: forall A (S: set A), eq_set (union S empty) S. -Axiom union_compat: - forall (A : Type), - forall x x' : set A, eq_set x x' -> - forall y y' : set A, eq_set y y' -> - eq_set (union x y) (union x' y'). -\end{coq_eval} - -\begin{coq_example*} -Add Parametric Relation A : (set A) eq_set - reflexivity proved by eq_set_refl - symmetry proved by eq_set_sym - transitivity proved by eq_set_trans - as eq_set_rel. -Add Parametric Morphism A : (@union A) with - signature eq_set ==> eq_set ==> eq_set as union_mor. -Proof. exact (@union_compat A). Qed. -\end{coq_example*} - -We proceed now by proving a simple lemma performing a rewrite step -and then applying reflexivity, as we would do working with Leibniz -equality. Both tactic applications are accepted -since the required properties over \texttt{eq\_set} and -\texttt{union} can be established from the two declarations above. - -\begin{coq_example*} -Goal forall (S: set nat), - eq_set (union (union S empty) S) (union S S). -Proof. intros. rewrite empty_neutral. reflexivity. Qed. -\end{coq_example*} - -The tables of relations and morphisms are managed by the type class -instance mechanism. The behavior on section close is to generalize -the instances by the variables of the section (and possibly hypotheses -used in the proofs of instance declarations) but not to export them in -the rest of the development for proof search. One can use the -\texttt{Existing Instance} command to do so outside the section, -using the name of the declared morphism suffixed by \texttt{\_Morphism}, -or use the \texttt{Global} modifier for the corresponding class instance -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. - -\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. - -\begin{cscexample} -To replace \texttt{(union S empty)} with \texttt{S} in -\texttt{(union (union S empty) S) (union S S)} the rewrite tactic must -exploit the monotony of \texttt{union} (axiom \texttt{union\_compat} in -the previous example). Applying \texttt{union\_compat} by hand we are left -with the goal \texttt{eq\_set (union S S) (union S S)}. -\end{cscexample} - -When the relations associated to some arguments are not reflexive, the tactic -cannot automatically prove the reflexivity goals, that are left to the user. - -Setoids whose relation are partial equivalence relations (PER) -are useful to deal with partial functions. Let \texttt{R} be a PER. We say -that an element \texttt{x} is defined if \texttt{R x x}. A partial function -whose domain comprises all the defined elements only is declared as a -morphism that respects \texttt{R}. Every time a rewriting step is performed -the user must prove that the argument of the morphism is defined. - -\begin{cscexample} -Let \texttt{eqO} be \texttt{fun x y => x = y $\land$ ~x$\neq$ 0} (the smaller PER over -non zero elements). Division can be declared as a morphism of signature -\texttt{eq ==> eq0 ==> eq}. Replace \texttt{x} with \texttt{y} in -\texttt{div x n = div y n} opens the additional goal \texttt{eq0 n n} that -is equivalent to \texttt{n=n $\land$ n$\neq$0}. -\end{cscexample} - -\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 -every context, since the obtained goal implies the previous one if and -only if the replacement has been performed in a contravariant position. -In a similar way, replacement in an hypothesis can be performed only if -the replaced term occurs in a covariant position. - -\begin{cscexample}[Covariance and contravariance] -Suppose that division over real numbers has been defined as a -morphism of signature \texttt{Z.div: Z.lt ++> Z.lt -{}-> Z.lt} (i.e. -\texttt{Z.div} is increasing in its first argument, but decreasing on the -second one). Let \texttt{<} denotes \texttt{Z.lt}. -Under the hypothesis \texttt{H: x < y} we have -\texttt{k < x / y -> k < x / x}, but not -\texttt{k < y / x -> k < x / x}. -Dually, under the same hypothesis \texttt{k < x / y -> k < y / y} holds, -but \texttt{k < y / x -> k < y / y} does not. -Thus, if the current goal is \texttt{k < x / x}, it is possible to replace -only the second occurrence of \texttt{x} (in contravariant position) -with \texttt{y} since the obtained goal must imply the current one. -On the contrary, if \texttt{k < x / x} is -an hypothesis, it is possible to replace only the first occurrence of -\texttt{x} (in covariant position) with \texttt{y} since -the current hypothesis must imply the obtained one. -\end{cscexample} - -Contrary to the previous implementation, no specific error message will -be raised when trying to replace a term that occurs in the wrong -position. It will only fail because the rewriting constraints are not -satisfiable. However it is possible to use the \texttt{at} modifier to -specify which occurrences should be rewritten. - -As expected, composing morphisms together propagates the variance annotations by -switching the variance every time a contravariant position is traversed. -\begin{cscexample} -Let us continue the previous example and let us consider the goal -\texttt{x / (x / x) < k}. The first and third occurrences of \texttt{x} are -in a contravariant position, while the second one is in covariant position. -More in detail, the second occurrence of \texttt{x} occurs -covariantly in \texttt{(x / x)} (since division is covariant in its first -argument), and thus contravariantly in \texttt{x / (x / x)} (since division -is contravariant in its second argument), and finally covariantly in -\texttt{x / (x / x) < k} (since \texttt{<}, as every transitive relation, -is contravariant in its first argument with respect to the relation itself). -\end{cscexample} - -\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. - -\begin{cscexample} -Union over homogeneous lists can be given all the following signatures: -\texttt{eq ==> eq ==> eq} (\texttt{eq} being the equality over ordered lists) -\texttt{set\_eq ==> set\_eq ==> set\_eq} (\texttt{set\_eq} being the equality -over unordered lists up to duplicates), -\texttt{multiset\_eq ==> multiset\_eq ==> multiset\_eq} (\texttt{multiset\_eq} -being the equality over unordered lists). -\end{cscexample} - -To declare multiple signatures for a morphism, repeat the \texttt{Add Morphism} -command. - -When morphisms have multiple signatures it can be the case that a rewrite -request is ambiguous, since it is unclear what relations should be used to -perform the rewriting. Contrary to the previous implementation, the -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{Commands and tactics} -\subsection{First class setoids and morphisms} -\label{setoid:first-class} - -The implementation is based on a first-class representation of -properties of relations and morphisms as type classes. That is, -the various combinations of properties on relations and morphisms -are represented as records and instances of theses classes are put -in a hint database. -For example, the declaration: - -\begin{quote} - \texttt{Add Parametric Relation} ($x_1 : T_1$) \ldots ($x_n : T_k$) : - \textit{(A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots $t'_m$)}\\ - ~\zeroone{\texttt{reflexivity proved by} \textit{refl}}\\ - ~\zeroone{\texttt{symmetry proved by} \textit{sym}}\\ - ~\zeroone{\texttt{transitivity proved by} \textit{trans}}\\ - \texttt{~as} \textit{id}. -\end{quote} - -is equivalent to an instance declaration: - -\begin{quote} - \texttt{Instance} ($x_1 : T_1$) \ldots ($x_n : T_k$) \texttt{=>} - \textit{id} : \texttt{@Equivalence} \textit{(A $t_1$ \ldots $t_n$) (Aeq - $t'_1$ \ldots $t'_m$)} :=\\ - ~\zeroone{\texttt{Equivalence\_Reflexive :=} \textit{refl}}\\ - ~\zeroone{\texttt{Equivalence\_Symmetric :=} \textit{sym}}\\ - ~\zeroone{\texttt{Equivalence\_Transitive :=} \textit{trans}}. -\end{quote} - -The declaration itself amounts to the definition of an object of the -record type \texttt{Coq.Classes.RelationClasses.Equivalence} and a -hint added to the \texttt{typeclass\_instances} hint database. -Morphism declarations are also instances of a type class defined in -\texttt{Classes.Morphisms}. -See the documentation on type classes \ref{typeclasses} and -the theories files in \texttt{Classes} for further explanations. - -One can inform the rewrite tactic about morphisms and relations just by -using the typeclass mechanism to declare them using \texttt{Instance} -and \texttt{Context} vernacular commands. -Any object of type \texttt{Proper} (the type of morphism declarations) -in the local context will also be automatically used by the rewriting -tactic to solve constraints. - -Other representations of first class setoids and morphisms can also -be handled by encoding them as records. In the following example, -the projections of the setoid relation and of the morphism function -can be registered as parametric relations and morphisms. -\begin{cscexample}[First class setoids] - -\begin{coq_example*} -Require Import Relation_Definitions Setoid. -Record Setoid: Type := -{ car:Type; - eq:car->car->Prop; - refl: reflexive _ eq; - sym: symmetric _ eq; - trans: transitive _ eq -}. -Add Parametric Relation (s : Setoid) : (@car s) (@eq s) - reflexivity proved by (refl s) - symmetry proved by (sym s) - transitivity proved by (trans s) as eq_rel. -Record Morphism (S1 S2:Setoid): Type := -{ f:car S1 ->car S2; - compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2) }. -Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) : - (@f S1 S2 M) with signature (@eq S1 ==> @eq S2) as apply_mor. -Proof. apply (compat S1 S2 M). Qed. -Lemma test: forall (S1 S2:Setoid) (m: Morphism S1 S2) - (x y: car S1), eq S1 x y -> eq S2 (f _ _ m x) (f _ _ m y). -Proof. intros. rewrite H. reflexivity. Qed. -\end{coq_example*} -\end{cscexample} - -\subsection{Tactics enabled on user provided relations} -\label{setoidtactics} -The following tactics, all prefixed by \texttt{setoid\_}, -deal with arbitrary -registered relations and morphisms. Moreover, all the corresponding unprefixed -tactics (i.e. \texttt{reflexivity}, \texttt{symmetry}, \texttt{transitivity}, -\texttt{replace}, \texttt{rewrite}) -have been extended to fall back to their prefixed counterparts when -the relation involved is not Leibniz equality. Notice, however, that using -the prefixed tactics it is possible to pass additional arguments such as -\texttt{using relation}. -\medskip - -\tacindex{setoid\_reflexivity} -\texttt{setoid\_reflexivity} - -\tacindex{setoid\_symmetry} -\texttt{setoid\_symmetry} \zeroone{\texttt{in} \textit{ident}} - -\tacindex{setoid\_transitivity} -\texttt{setoid\_transitivity} - -\tacindex{setoid\_rewrite} -\texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term} -~\zeroone{\texttt{at} \textit{occs}} ~\zeroone{\texttt{in} \textit{ident}} - -\tacindex{setoid\_replace} -\texttt{setoid\_replace} \textit{term} \texttt{with} \textit{term} -~\zeroone{\texttt{in} \textit{ident}} -~\zeroone{\texttt{using relation} \textit{term}} -~\zeroone{\texttt{by} \textit{tactic}} -\medskip - -The \texttt{using relation} -arguments cannot be passed to the unprefixed form. The latter argument -tells the tactic what parametric relation should be used to replace -the first tactic argument with the second one. If omitted, it defaults -to the \texttt{DefaultRelation} instance on the type of the objects. -By default, it means the most recent \texttt{Equivalence} instance in -the environment, but it can be customized by declaring new -\texttt{DefaultRelation} instances. As Leibniz equality is a declared -equivalence, it will fall back to it if no other relation is declared on -a given type. - -Every derived tactic that is based on the unprefixed forms of the tactics -considered above will also work up to user defined relations. For instance, -it is possible to register hints for \texttt{autorewrite} that are -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. - -\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, -\texttt{Equivalence}s, \texttt{PreOrder}s, \texttt{PER}s, and -Morphisms (implemented as \texttt{Proper} instances). When - the rewriting tactics refuse to replace a term in a context -because the latter is not a composition of morphisms, the \texttt{Print Instances} -commands can be useful to understand what additional morphisms should be -registered. - -\subsection{Deprecated syntax and backward incompatibilities} -Due to backward compatibility reasons, the following syntax for the -declaration of setoids and morphisms is also accepted. - -\comindex{Add Setoid} -\begin{quote} - \texttt{Add Setoid} \textit{A Aeq ST} \texttt{as} \textit{ident} -\end{quote} -where \textit{Aeq} is a congruence relation without parameters, -\textit{A} is its carrier and \textit{ST} is an object of type -\texttt{(Setoid\_Theory A Aeq)} (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. - -\comindex{Add Morphism} -\begin{quote} - \texttt{Add Morphism} \textit{f}:\textit{ident}.\\ - Proof.\\ - \ldots\\ - Qed. -\end{quote} - -The latter command also is restricted to the declaration of morphisms without -parameters. It is not fully backward compatible since the property the user -is asked to prove is slightly different: for $n$-ary morphisms the hypotheses -of the property are permuted; moreover, when the morphism returns a -proposition, the property is now stated using a bi-implication in place of -a simple implication. In practice, porting an old development to the new -semantics is usually quite simple. - -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. Moreover, it is -now also possible to declare several morphisms having the same signature. -Finally, the replace and rewrite tactics can be used to replace terms in -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{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}. - -To be able to rewrite under binding constructs, one must declare -morphisms with respect to pointwise (setoid) equivalence of functions. -Example of such morphisms are the standard \texttt{all} and \texttt{ex} -combinators for universal and existential quantification respectively. -They are declared as morphisms in the \texttt{Classes.Morphisms\_Prop} -module. For example, to declare that universal quantification is a -morphism for logical equivalence: - -\begin{coq_eval} -Reset Initial. -Require Import Setoid Morphisms. -\end{coq_eval} -\begin{coq_example} -Instance all_iff_morphism (A : Type) : - Proper (pointwise_relation A iff ==> iff) (@all A). -Proof. simpl_relation. -\end{coq_example} -\begin{coq_eval} -Admitted. -\end{coq_eval} - -One then has to show that if two predicates are equivalent at every -point, their universal quantifications are equivalent. Once we have -declared such a morphism, it will be used by the setoid rewriting tactic -each time we try to rewrite under an \texttt{all} application (products -in \Prop{} are implicitly translated to such applications). - -Indeed, when rewriting under a lambda, binding variable $x$, say from -$P~x$ to $Q~x$ using the relation \texttt{iff}, the tactic will generate -a proof of \texttt{pointwise\_relation A iff (fun x => P x) (fun x => Q -x)} from the proof of \texttt{iff (P x) (Q x)} and a constraint of the -form \texttt{Proper (pointwise\_relation A iff ==> ?) m} will be -generated for the surrounding morphism \texttt{m}. - -Hence, one can add higher-order combinators as morphisms by providing -signatures using pointwise extension for the relations on the functional -arguments (or whatever subrelation of the pointwise extension). -For example, one could declare the \texttt{map} combinator on lists as -a morphism: -\begin{coq_eval} -Require Import List Setoid Morphisms. -Set Implicit Arguments. -Inductive list_equiv {A:Type} (eqA : relation A) : relation (list A) := -| eq_nil : list_equiv eqA nil nil -| eq_cons : forall x y, eqA x y -> - forall l l', list_equiv eqA l l' -> list_equiv eqA (x :: l) (y :: l'). -Generalizable All Variables. -\end{coq_eval} -\begin{coq_example*} -Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} : - Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B). -\end{coq_example*} - -where \texttt{list\_equiv} implements an equivalence on lists -parameterized by an equivalence on the elements. - -Note that when one does rewriting with a lemma under a binder -using \texttt{setoid\_rewrite}, the application of the lemma may capture -the bound variable, as the semantics are different from rewrite where -the lemma is first matched on the whole term. With the new -\texttt{setoid\_rewrite}, matching is done on each subterm separately -and in its local environment, and all matches are rewritten -\emph{simultaneously} by default. The semantics of the previous -\texttt{setoid\_rewrite} implementation can almost be recovered using -the \texttt{at 1} modifier. - -\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. -If a signature mentions a relation $R$ on the left of an arrow -\texttt{==>}, then the signature also applies for any relation $S$ that -is smaller than $R$, and the inverse applies on the right of an arrow. -One can then declare only a few morphisms instances that generate the complete set -of signatures for a particular constant. By default, the only declared -subrelation is \texttt{iff}, which is a subrelation of \texttt{impl} -and \texttt{inverse impl} (the dual of implication). That's why we can -declare only two morphisms for conjunction: -\texttt{Proper (impl ==> impl ==> impl) and} and -\texttt{Proper (iff ==> iff ==> iff) and}. This is sufficient to satisfy -any rewriting constraints arising from a rewrite using \texttt{iff}, -\texttt{impl} or \texttt{inverse impl} through \texttt{and}. - -Sub-relations are implemented in \texttt{Classes.Morphisms} and are a -prime example of a mostly user-space extension of the algorithm. - -\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}). - -\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 -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst new file mode 100644 index 000000000..b7b343112 --- /dev/null +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -0,0 +1,842 @@ +\newtheorem{cscexample}{Example} + +\achapter{\protect{Generalized rewriting}} +%HEVEA\cutname{setoid.html} +\aauthor{Matthieu Sozeau} +\label{setoids} + +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 the specification of +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). +The new implementation is a drop-in replacement for the old one,\footnote{Nicolas +Tabareau helped with the gluing.} hence most of the documentation still applies. + +The work is a complete rewrite of the previous implementation, based on +the type class infrastructure. It also improves on and generalizes +the previous implementation in several ways: +\begin{itemize} +\item User-extensible algorithm. The algorithm is separated in two + parts: generations of the rewriting constraints (done in ML) and + solving of these constraints using type class resolution. As type + class resolution is extensible using tactics, this allows users to define + general ways to solve morphism constraints. +\item Sub-relations. An example extension to the base algorithm is the + ability to define one relation as a subrelation of another so that + morphism declarations on one relation can be used automatically for + the other. This is done purely using tactics and type class search. +\item Rewriting under binders. It is possible to rewrite under binders + in the new implementation, if one provides the proper + morphisms. Again, most of the work is handled in the tactics. +\item First-class morphisms and signatures. Signatures and morphisms are + ordinary Coq terms, hence they can be manipulated inside Coq, put + inside structures and lemmas about them can be proved inside the + system. Higher-order morphisms are also allowed. +\item Performance. The implementation is based on a depth-first search for the first + solution to a set of constraints which can be as fast as linear in the + size of the term, and the size of the proof term is linear + in the size of the original term. Besides, the extensibility allows the + user to customize the proof search if necessary. +\end{itemize} + +\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 +expression $A$, which depends on $x_1$ \ldots $x_n$, is called the +\emph{carrier} of the relation and \texttt{R} is +said to be a relation over \texttt{A}; the list $x_1,\ldots,x_n$ +is the (possibly empty) list of parameters of the relation. + +\firstexample +\begin{cscexample}[Parametric relation] +It is possible to implement finite sets of elements of type \texttt{A} +as unordered list of elements of type \texttt{A}. The function +\texttt{set\_eq: forall (A: Type), relation (list A)} satisfied by two lists +with the same elements is a parametric relation over \texttt{(list A)} with +one parameter \texttt{A}. The type of \texttt{set\_eq} is convertible with +\texttt{forall (A: Type), list A -> list A -> Prop}. +\end{cscexample} + +An \emph{instance} of a parametric relation \texttt{R} with $n$ parameters +is any term \texttt{(R $t_1$ \ldots $t_n$)}. + +Let \texttt{R} be a relation over \texttt{A} with $n$ parameters. +A term is a parametric proof of reflexivity for \texttt{R} if it has type +\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), + reflexive (R $x_1$ \ldots $x_n$)}. Similar definitions are given for +parametric proofs of symmetry and transitivity. + +\begin{cscexample}[Parametric relation (cont.)] +The \texttt{set\_eq} relation of the previous example can be proved to be +reflexive, symmetric and transitive. +\end{cscexample} + +A parametric unary function $f$ of type +\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), $A_1$ -> $A_2$} +covariantly respects two parametric relation instances $R_1$ and $R_2$ if, +whenever $x, y$ satisfy $R_1~x~y$, their images $(f~x)$ and $(f~y)$ +satisfy $R_2~(f~x)~(f~y)$ . An $f$ that respects its input and output relations +will be called a unary covariant \emph{morphism}. We can also say that $f$ is +a monotone function with respect to $R_1$ and $R_2$. +The sequence $x_1,\ldots x_n$ represents the parameters of the morphism. + +Let $R_1$ and $R_2$ be two parametric relations. +The \emph{signature} of a parametric morphism of type +\texttt{forall ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), $A_1$ -> $A_2$} that +covariantly respects two instances $I_{R_1}$ and $I_{R_2}$ of $R_1$ and $R_2$ is written $I_{R_1} \texttt{++>} I_{R_2}$. +Notice that the special arrow \texttt{++>}, which reminds the reader +of covariance, is placed between the two relation instances, not +between the two carriers. The signature relation instances and morphism will +be typed in a context introducing variables for the parameters. + +The previous definitions are extended straightforwardly to $n$-ary morphisms, +that are required to be simultaneously monotone on every argument. + +Morphisms can also be contravariant in one or more of their arguments. +A morphism is contravariant on an argument associated to the relation instance +$R$ if it is covariant on the same argument when the inverse relation +$R^{-1}$ (\texttt{inverse R} in Coq) is considered. +The special arrow \texttt{-{}->} is used in signatures +for contravariant morphisms. + +Functions having arguments related by symmetric relations instances are both +covariant and contravariant in those arguments. The special arrow +\texttt{==>} is used in signatures for morphisms that are both covariant +and contravariant. + +An instance of a parametric morphism $f$ with $n$ parameters is any term +\texttt{f $t_1$ \ldots $t_n$}. + +\begin{cscexample}[Morphisms] +Continuing the previous example, let +\texttt{union: forall (A: Type), list A -> list A -> list A} perform the union +of two sets by appending one list to the other. \texttt{union} is a binary +morphism parametric over \texttt{A} that respects the relation instance +\texttt{(set\_eq A)}. The latter condition is proved by showing +\texttt{forall (A: Type) (S1 S1' S2 S2': list A), set\_eq A S1 S1' -> + set\_eq A S2 S2' -> set\_eq A (union A S1 S2) (union A S1' S2')}. + +The signature of the function \texttt{union A} is +\texttt{set\_eq A ==> set\_eq A ==> set\_eq A} for all \texttt{A}. +\end{cscexample} + +\begin{cscexample}[Contravariant morphism] +The division function \texttt{Rdiv: R -> R -> R} is a morphism of +signature \texttt{le ++> le -{}-> le} where \texttt{le} is +the usual order relation over real numbers. Notice that division is +covariant in its first argument and contravariant in its second +argument. +\end{cscexample} + +Leibniz equality is a relation and every function is a +morphism that respects Leibniz equality. Unfortunately, Leibniz equality +is not always the intended equality for a given structure. + +In the next section we will describe the commands to register terms as +parametric relations and morphisms. Several tactics that deal with equality +in \Coq\ can also work with the registered relations. +The exact list of tactic will be given in Sect.~\ref{setoidtactics}. +For instance, the +tactic \texttt{reflexivity} can be used to close a goal $R~n~n$ whenever +$R$ is an instance of a registered reflexive relation. However, the tactics +that replace in a context $C[]$ one term with another one related by $R$ +must verify that $C[]$ is a morphism that respects the intended relation. +Currently the verification consists in checking whether $C[]$ is a syntactic +composition of morphism instances that respects some obvious +compatibility constraints. + +\begin{cscexample}[Rewriting] +Continuing the previous examples, suppose that the user must prove +\texttt{set\_eq int (union int (union int S1 S2) S2) (f S1 S2)} under the +hypothesis \texttt{H: set\_eq int S2 (@nil int)}. It is possible to +use the \texttt{rewrite} tactic to replace the first two occurrences of +\texttt{S2} with \texttt{@nil int} in the goal since the context +\texttt{set\_eq int (union int (union int S1 nil) nil) (f S1 S2)}, being +a composition of morphisms instances, is a morphism. However the tactic +will fail replacing the third occurrence of \texttt{S2} unless \texttt{f} +has also been declared as a morphism. +\end{cscexample} + +\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}) +can be declared with the following command: + +\comindex{Add Parametric Relation} +\begin{quote} + \texttt{Add Parametric Relation} ($x_1 : T_1$) \ldots ($x_n : T_k$) : + \textit{(A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots $t'_m$)}\\ + ~\zeroone{\texttt{reflexivity proved by} \textit{refl}}\\ + ~\zeroone{\texttt{symmetry proved by} \textit{sym}}\\ + ~\zeroone{\texttt{transitivity proved by} \textit{trans}}\\ + \texttt{~as} \textit{id}. +\end{quote} +after having required the \texttt{Setoid} module with the +\texttt{Require Setoid} command. + +The identifier \textit{id} gives a unique name to the morphism and it is +used by the command to generate fresh names for automatically provided lemmas +used internally. + +Notice that the carrier and relation parameters may refer to the context +of variables introduced at the beginning of the declaration, but the +instances need not be made only of variables. +Also notice that \textit{A} is \emph{not} required to be a term +having the same parameters as \textit{Aeq}, although that is often the +case in practice (this departs from the previous implementation). + +\comindex{Add Relation} +In case the carrier and relations are not parametric, one can use the +command \texttt{Add Relation} instead, whose syntax is the same except +there is no local context. + +The proofs of reflexivity, symmetry and transitivity can be omitted if the +relation is not an equivalence relation. The proofs must be instances of the +corresponding relation definitions: e.g. the proof of reflexivity must +have a type convertible to \texttt{reflexive (A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots + $t'_n$)}. Each proof may refer to the introduced variables as well. + +\begin{cscexample}[Parametric relation] +For Leibniz equality, we may declare: +\texttt{Add Parametric Relation (A : Type) :} \texttt{A (@eq A)}\\ +~\zeroone{\texttt{reflexivity proved by} \texttt{@refl\_equal A}}\\ +\ldots +\end{cscexample} + +Some tactics +(\texttt{reflexivity}, \texttt{symmetry}, \texttt{transitivity}) work only +on relations that respect the expected properties. The remaining tactics +(\texttt{replace}, \texttt{rewrite} and derived tactics such as +\texttt{autorewrite}) do not require any properties over the relation. +However, they are able to replace terms with related ones only in contexts +that are syntactic compositions of parametric morphism instances declared with +the following command. + +\comindex{Add Parametric Morphism} +\begin{quote} + \texttt{Add Parametric Morphism} ($x_1 : \T_1$) \ldots ($x_k : \T_k$) : + (\textit{f $t_1$ \ldots $t_n$})\\ + \texttt{~with signature} \textit{sig}\\ + \texttt{~as id}.\\ + \texttt{Proof}\\ + ~\ldots\\ + \texttt{Qed} +\end{quote} + +The command declares \textit{f} as a parametric morphism of signature +\textit{sig}. The identifier \textit{id} gives a unique name to the morphism +and it is used as the base name of the type class instance definition +and as the name of the lemma that proves the well-definedness of the morphism. +The parameters of the morphism as well as the signature may refer to the +context of variables. +The command asks the user to prove interactively that \textit{f} respects +the relations identified from the signature. + +\begin{cscexample} +We start the example by assuming a small theory over homogeneous sets and +we declare set equality as a parametric equivalence relation and +union of two sets as a parametric morphism. +\begin{coq_example*} +Require Export Setoid. +Require Export Relation_Definitions. +Set Implicit Arguments. +Parameter set: Type -> Type. +Parameter empty: forall A, set A. +Parameter eq_set: forall A, set A -> set A -> Prop. +Parameter union: forall A, set A -> set A -> set A. +Axiom eq_set_refl: forall A, reflexive _ (eq_set (A:=A)). +Axiom eq_set_sym: forall A, symmetric _ (eq_set (A:=A)). +Axiom eq_set_trans: forall A, transitive _ (eq_set (A:=A)). +Axiom empty_neutral: forall A (S: set A), eq_set (union S (empty A)) S. +Axiom union_compat: + forall (A : Type), + forall x x' : set A, eq_set x x' -> + forall y y' : set A, eq_set y y' -> + eq_set (union x y) (union x' y'). +Add Parametric Relation A : (set A) (@eq_set A) + reflexivity proved by (eq_set_refl (A:=A)) + symmetry proved by (eq_set_sym (A:=A)) + transitivity proved by (eq_set_trans (A:=A)) + as eq_set_rel. +Add Parametric Morphism A : (@union A) with +signature (@eq_set A) ==> (@eq_set A) ==> (@eq_set A) as union_mor. +Proof. exact (@union_compat A). Qed. +\end{coq_example*} + +\end{cscexample} + +It is possible to reduce the burden of specifying parameters using +(maximally inserted) implicit arguments. If \texttt{A} is always set as +maximally implicit in the previous example, one can write: + +\begin{coq_eval} +Reset Initial. +Require Export Setoid. +Require Export Relation_Definitions. +Parameter set: Type -> Type. +Parameter empty: forall {A}, set A. +Parameter eq_set: forall {A}, set A -> set A -> Prop. +Parameter union: forall {A}, set A -> set A -> set A. +Axiom eq_set_refl: forall {A}, reflexive (set A) eq_set. +Axiom eq_set_sym: forall {A}, symmetric (set A) eq_set. +Axiom eq_set_trans: forall {A}, transitive (set A) eq_set. +Axiom empty_neutral: forall A (S: set A), eq_set (union S empty) S. +Axiom union_compat: + forall (A : Type), + forall x x' : set A, eq_set x x' -> + forall y y' : set A, eq_set y y' -> + eq_set (union x y) (union x' y'). +\end{coq_eval} + +\begin{coq_example*} +Add Parametric Relation A : (set A) eq_set + reflexivity proved by eq_set_refl + symmetry proved by eq_set_sym + transitivity proved by eq_set_trans + as eq_set_rel. +Add Parametric Morphism A : (@union A) with + signature eq_set ==> eq_set ==> eq_set as union_mor. +Proof. exact (@union_compat A). Qed. +\end{coq_example*} + +We proceed now by proving a simple lemma performing a rewrite step +and then applying reflexivity, as we would do working with Leibniz +equality. Both tactic applications are accepted +since the required properties over \texttt{eq\_set} and +\texttt{union} can be established from the two declarations above. + +\begin{coq_example*} +Goal forall (S: set nat), + eq_set (union (union S empty) S) (union S S). +Proof. intros. rewrite empty_neutral. reflexivity. Qed. +\end{coq_example*} + +The tables of relations and morphisms are managed by the type class +instance mechanism. The behavior on section close is to generalize +the instances by the variables of the section (and possibly hypotheses +used in the proofs of instance declarations) but not to export them in +the rest of the development for proof search. One can use the +\texttt{Existing Instance} command to do so outside the section, +using the name of the declared morphism suffixed by \texttt{\_Morphism}, +or use the \texttt{Global} modifier for the corresponding class instance +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. + +\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. + +\begin{cscexample} +To replace \texttt{(union S empty)} with \texttt{S} in +\texttt{(union (union S empty) S) (union S S)} the rewrite tactic must +exploit the monotony of \texttt{union} (axiom \texttt{union\_compat} in +the previous example). Applying \texttt{union\_compat} by hand we are left +with the goal \texttt{eq\_set (union S S) (union S S)}. +\end{cscexample} + +When the relations associated to some arguments are not reflexive, the tactic +cannot automatically prove the reflexivity goals, that are left to the user. + +Setoids whose relation are partial equivalence relations (PER) +are useful to deal with partial functions. Let \texttt{R} be a PER. We say +that an element \texttt{x} is defined if \texttt{R x x}. A partial function +whose domain comprises all the defined elements only is declared as a +morphism that respects \texttt{R}. Every time a rewriting step is performed +the user must prove that the argument of the morphism is defined. + +\begin{cscexample} +Let \texttt{eqO} be \texttt{fun x y => x = y $\land$ ~x$\neq$ 0} (the smaller PER over +non zero elements). Division can be declared as a morphism of signature +\texttt{eq ==> eq0 ==> eq}. Replace \texttt{x} with \texttt{y} in +\texttt{div x n = div y n} opens the additional goal \texttt{eq0 n n} that +is equivalent to \texttt{n=n $\land$ n$\neq$0}. +\end{cscexample} + +\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 +every context, since the obtained goal implies the previous one if and +only if the replacement has been performed in a contravariant position. +In a similar way, replacement in an hypothesis can be performed only if +the replaced term occurs in a covariant position. + +\begin{cscexample}[Covariance and contravariance] +Suppose that division over real numbers has been defined as a +morphism of signature \texttt{Z.div: Z.lt ++> Z.lt -{}-> Z.lt} (i.e. +\texttt{Z.div} is increasing in its first argument, but decreasing on the +second one). Let \texttt{<} denotes \texttt{Z.lt}. +Under the hypothesis \texttt{H: x < y} we have +\texttt{k < x / y -> k < x / x}, but not +\texttt{k < y / x -> k < x / x}. +Dually, under the same hypothesis \texttt{k < x / y -> k < y / y} holds, +but \texttt{k < y / x -> k < y / y} does not. +Thus, if the current goal is \texttt{k < x / x}, it is possible to replace +only the second occurrence of \texttt{x} (in contravariant position) +with \texttt{y} since the obtained goal must imply the current one. +On the contrary, if \texttt{k < x / x} is +an hypothesis, it is possible to replace only the first occurrence of +\texttt{x} (in covariant position) with \texttt{y} since +the current hypothesis must imply the obtained one. +\end{cscexample} + +Contrary to the previous implementation, no specific error message will +be raised when trying to replace a term that occurs in the wrong +position. It will only fail because the rewriting constraints are not +satisfiable. However it is possible to use the \texttt{at} modifier to +specify which occurrences should be rewritten. + +As expected, composing morphisms together propagates the variance annotations by +switching the variance every time a contravariant position is traversed. +\begin{cscexample} +Let us continue the previous example and let us consider the goal +\texttt{x / (x / x) < k}. The first and third occurrences of \texttt{x} are +in a contravariant position, while the second one is in covariant position. +More in detail, the second occurrence of \texttt{x} occurs +covariantly in \texttt{(x / x)} (since division is covariant in its first +argument), and thus contravariantly in \texttt{x / (x / x)} (since division +is contravariant in its second argument), and finally covariantly in +\texttt{x / (x / x) < k} (since \texttt{<}, as every transitive relation, +is contravariant in its first argument with respect to the relation itself). +\end{cscexample} + +\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. + +\begin{cscexample} +Union over homogeneous lists can be given all the following signatures: +\texttt{eq ==> eq ==> eq} (\texttt{eq} being the equality over ordered lists) +\texttt{set\_eq ==> set\_eq ==> set\_eq} (\texttt{set\_eq} being the equality +over unordered lists up to duplicates), +\texttt{multiset\_eq ==> multiset\_eq ==> multiset\_eq} (\texttt{multiset\_eq} +being the equality over unordered lists). +\end{cscexample} + +To declare multiple signatures for a morphism, repeat the \texttt{Add Morphism} +command. + +When morphisms have multiple signatures it can be the case that a rewrite +request is ambiguous, since it is unclear what relations should be used to +perform the rewriting. Contrary to the previous implementation, the +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{Commands and tactics} +\subsection{First class setoids and morphisms} +\label{setoid:first-class} + +The implementation is based on a first-class representation of +properties of relations and morphisms as type classes. That is, +the various combinations of properties on relations and morphisms +are represented as records and instances of theses classes are put +in a hint database. +For example, the declaration: + +\begin{quote} + \texttt{Add Parametric Relation} ($x_1 : T_1$) \ldots ($x_n : T_k$) : + \textit{(A $t_1$ \ldots $t_n$) (Aeq $t'_1$ \ldots $t'_m$)}\\ + ~\zeroone{\texttt{reflexivity proved by} \textit{refl}}\\ + ~\zeroone{\texttt{symmetry proved by} \textit{sym}}\\ + ~\zeroone{\texttt{transitivity proved by} \textit{trans}}\\ + \texttt{~as} \textit{id}. +\end{quote} + +is equivalent to an instance declaration: + +\begin{quote} + \texttt{Instance} ($x_1 : T_1$) \ldots ($x_n : T_k$) \texttt{=>} + \textit{id} : \texttt{@Equivalence} \textit{(A $t_1$ \ldots $t_n$) (Aeq + $t'_1$ \ldots $t'_m$)} :=\\ + ~\zeroone{\texttt{Equivalence\_Reflexive :=} \textit{refl}}\\ + ~\zeroone{\texttt{Equivalence\_Symmetric :=} \textit{sym}}\\ + ~\zeroone{\texttt{Equivalence\_Transitive :=} \textit{trans}}. +\end{quote} + +The declaration itself amounts to the definition of an object of the +record type \texttt{Coq.Classes.RelationClasses.Equivalence} and a +hint added to the \texttt{typeclass\_instances} hint database. +Morphism declarations are also instances of a type class defined in +\texttt{Classes.Morphisms}. +See the documentation on type classes \ref{typeclasses} and +the theories files in \texttt{Classes} for further explanations. + +One can inform the rewrite tactic about morphisms and relations just by +using the typeclass mechanism to declare them using \texttt{Instance} +and \texttt{Context} vernacular commands. +Any object of type \texttt{Proper} (the type of morphism declarations) +in the local context will also be automatically used by the rewriting +tactic to solve constraints. + +Other representations of first class setoids and morphisms can also +be handled by encoding them as records. In the following example, +the projections of the setoid relation and of the morphism function +can be registered as parametric relations and morphisms. +\begin{cscexample}[First class setoids] + +\begin{coq_example*} +Require Import Relation_Definitions Setoid. +Record Setoid: Type := +{ car:Type; + eq:car->car->Prop; + refl: reflexive _ eq; + sym: symmetric _ eq; + trans: transitive _ eq +}. +Add Parametric Relation (s : Setoid) : (@car s) (@eq s) + reflexivity proved by (refl s) + symmetry proved by (sym s) + transitivity proved by (trans s) as eq_rel. +Record Morphism (S1 S2:Setoid): Type := +{ f:car S1 ->car S2; + compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2) }. +Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) : + (@f S1 S2 M) with signature (@eq S1 ==> @eq S2) as apply_mor. +Proof. apply (compat S1 S2 M). Qed. +Lemma test: forall (S1 S2:Setoid) (m: Morphism S1 S2) + (x y: car S1), eq S1 x y -> eq S2 (f _ _ m x) (f _ _ m y). +Proof. intros. rewrite H. reflexivity. Qed. +\end{coq_example*} +\end{cscexample} + +\subsection{Tactics enabled on user provided relations} +\label{setoidtactics} +The following tactics, all prefixed by \texttt{setoid\_}, +deal with arbitrary +registered relations and morphisms. Moreover, all the corresponding unprefixed +tactics (i.e. \texttt{reflexivity}, \texttt{symmetry}, \texttt{transitivity}, +\texttt{replace}, \texttt{rewrite}) +have been extended to fall back to their prefixed counterparts when +the relation involved is not Leibniz equality. Notice, however, that using +the prefixed tactics it is possible to pass additional arguments such as +\texttt{using relation}. +\medskip + +\tacindex{setoid\_reflexivity} +\texttt{setoid\_reflexivity} + +\tacindex{setoid\_symmetry} +\texttt{setoid\_symmetry} \zeroone{\texttt{in} \textit{ident}} + +\tacindex{setoid\_transitivity} +\texttt{setoid\_transitivity} + +\tacindex{setoid\_rewrite} +\texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term} +~\zeroone{\texttt{at} \textit{occs}} ~\zeroone{\texttt{in} \textit{ident}} + +\tacindex{setoid\_replace} +\texttt{setoid\_replace} \textit{term} \texttt{with} \textit{term} +~\zeroone{\texttt{in} \textit{ident}} +~\zeroone{\texttt{using relation} \textit{term}} +~\zeroone{\texttt{by} \textit{tactic}} +\medskip + +The \texttt{using relation} +arguments cannot be passed to the unprefixed form. The latter argument +tells the tactic what parametric relation should be used to replace +the first tactic argument with the second one. If omitted, it defaults +to the \texttt{DefaultRelation} instance on the type of the objects. +By default, it means the most recent \texttt{Equivalence} instance in +the environment, but it can be customized by declaring new +\texttt{DefaultRelation} instances. As Leibniz equality is a declared +equivalence, it will fall back to it if no other relation is declared on +a given type. + +Every derived tactic that is based on the unprefixed forms of the tactics +considered above will also work up to user defined relations. For instance, +it is possible to register hints for \texttt{autorewrite} that are +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. + +\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, +\texttt{Equivalence}s, \texttt{PreOrder}s, \texttt{PER}s, and +Morphisms (implemented as \texttt{Proper} instances). When + the rewriting tactics refuse to replace a term in a context +because the latter is not a composition of morphisms, the \texttt{Print Instances} +commands can be useful to understand what additional morphisms should be +registered. + +\subsection{Deprecated syntax and backward incompatibilities} +Due to backward compatibility reasons, the following syntax for the +declaration of setoids and morphisms is also accepted. + +\comindex{Add Setoid} +\begin{quote} + \texttt{Add Setoid} \textit{A Aeq ST} \texttt{as} \textit{ident} +\end{quote} +where \textit{Aeq} is a congruence relation without parameters, +\textit{A} is its carrier and \textit{ST} is an object of type +\texttt{(Setoid\_Theory A Aeq)} (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. + +\comindex{Add Morphism} +\begin{quote} + \texttt{Add Morphism} \textit{f}:\textit{ident}.\\ + Proof.\\ + \ldots\\ + Qed. +\end{quote} + +The latter command also is restricted to the declaration of morphisms without +parameters. It is not fully backward compatible since the property the user +is asked to prove is slightly different: for $n$-ary morphisms the hypotheses +of the property are permuted; moreover, when the morphism returns a +proposition, the property is now stated using a bi-implication in place of +a simple implication. In practice, porting an old development to the new +semantics is usually quite simple. + +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. Moreover, it is +now also possible to declare several morphisms having the same signature. +Finally, the replace and rewrite tactics can be used to replace terms in +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{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}. + +To be able to rewrite under binding constructs, one must declare +morphisms with respect to pointwise (setoid) equivalence of functions. +Example of such morphisms are the standard \texttt{all} and \texttt{ex} +combinators for universal and existential quantification respectively. +They are declared as morphisms in the \texttt{Classes.Morphisms\_Prop} +module. For example, to declare that universal quantification is a +morphism for logical equivalence: + +\begin{coq_eval} +Reset Initial. +Require Import Setoid Morphisms. +\end{coq_eval} +\begin{coq_example} +Instance all_iff_morphism (A : Type) : + Proper (pointwise_relation A iff ==> iff) (@all A). +Proof. simpl_relation. +\end{coq_example} +\begin{coq_eval} +Admitted. +\end{coq_eval} + +One then has to show that if two predicates are equivalent at every +point, their universal quantifications are equivalent. Once we have +declared such a morphism, it will be used by the setoid rewriting tactic +each time we try to rewrite under an \texttt{all} application (products +in \Prop{} are implicitly translated to such applications). + +Indeed, when rewriting under a lambda, binding variable $x$, say from +$P~x$ to $Q~x$ using the relation \texttt{iff}, the tactic will generate +a proof of \texttt{pointwise\_relation A iff (fun x => P x) (fun x => Q +x)} from the proof of \texttt{iff (P x) (Q x)} and a constraint of the +form \texttt{Proper (pointwise\_relation A iff ==> ?) m} will be +generated for the surrounding morphism \texttt{m}. + +Hence, one can add higher-order combinators as morphisms by providing +signatures using pointwise extension for the relations on the functional +arguments (or whatever subrelation of the pointwise extension). +For example, one could declare the \texttt{map} combinator on lists as +a morphism: +\begin{coq_eval} +Require Import List Setoid Morphisms. +Set Implicit Arguments. +Inductive list_equiv {A:Type} (eqA : relation A) : relation (list A) := +| eq_nil : list_equiv eqA nil nil +| eq_cons : forall x y, eqA x y -> + forall l l', list_equiv eqA l l' -> list_equiv eqA (x :: l) (y :: l'). +Generalizable All Variables. +\end{coq_eval} +\begin{coq_example*} +Instance map_morphism `{Equivalence A eqA, Equivalence B eqB} : + Proper ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) (@map A B). +\end{coq_example*} + +where \texttt{list\_equiv} implements an equivalence on lists +parameterized by an equivalence on the elements. + +Note that when one does rewriting with a lemma under a binder +using \texttt{setoid\_rewrite}, the application of the lemma may capture +the bound variable, as the semantics are different from rewrite where +the lemma is first matched on the whole term. With the new +\texttt{setoid\_rewrite}, matching is done on each subterm separately +and in its local environment, and all matches are rewritten +\emph{simultaneously} by default. The semantics of the previous +\texttt{setoid\_rewrite} implementation can almost be recovered using +the \texttt{at 1} modifier. + +\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. +If a signature mentions a relation $R$ on the left of an arrow +\texttt{==>}, then the signature also applies for any relation $S$ that +is smaller than $R$, and the inverse applies on the right of an arrow. +One can then declare only a few morphisms instances that generate the complete set +of signatures for a particular constant. By default, the only declared +subrelation is \texttt{iff}, which is a subrelation of \texttt{impl} +and \texttt{inverse impl} (the dual of implication). That's why we can +declare only two morphisms for conjunction: +\texttt{Proper (impl ==> impl ==> impl) and} and +\texttt{Proper (iff ==> iff ==> iff) and}. This is sufficient to satisfy +any rewriting constraints arising from a rewrite using \texttt{iff}, +\texttt{impl} or \texttt{inverse impl} through \texttt{and}. + +Sub-relations are implemented in \texttt{Classes.Morphisms} and are a +prime example of a mostly user-space extension of the algorithm. + +\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}). + +\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 +%%% TeX-master: "Reference-Manual" +%%% End: -- cgit v1.2.3