From 3e96002677226c0cdaa8f355938a76cfb37a722a Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 14 Oct 2010 17:51:11 +0200
Subject: Imported Upstream version 8.3

---
 doc/refman/Setoid.tex | 714 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 714 insertions(+)
 create mode 100644 doc/refman/Setoid.tex

(limited to 'doc/refman/Setoid.tex')

diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
new file mode 100644
index 00000000..20c8c02b
--- /dev/null
+++ b/doc/refman/Setoid.tex
@@ -0,0 +1,714 @@
+\newtheorem{cscexample}{Example}
+
+\achapter{\protect{User defined equalities and relations}}
+\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 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{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}
+
+\asection{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_!$) \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}
+
+Is 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.
+
+\asection{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}
+
+\asection{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{Zdiv: Zlt ++> Zlt -{}-> Zlt} (i.e.
+\texttt{Zdiv} is increasing in its first argument, but decreasing on the
+second one). Let \texttt{<} denotes \texttt{Zlt}. 
+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}
+
+\asection{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{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}
+
+\asection{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, symmetry, transitivity, replace, 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
+
+\comindex{setoid\_reflexivity}
+\texttt{setoid\_reflexivity}
+
+\comindex{setoid\_symmetry}
+\texttt{setoid\_symmetry} \zeroone{\texttt{in} \textit{ident}}
+
+\comindex{setoid\_transitivity}
+\texttt{setoid\_transitivity}
+
+\comindex{setoid\_rewrite}
+\texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}
+~\zeroone{\texttt{at} \textit{occs}} ~\zeroone{\texttt{in} \textit{ident}}
+
+\comindex{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.
+
+\asection{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.
+
+\asection{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{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.
+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').
+\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.
+
+\asection{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.
+
+\asection{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}).
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% compile-command: "make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
+%%% End: 
-- 
cgit v1.2.3