Nettoyage de l'archive doc et restructuration avant intégration à l'archive

principale de Coq et publication des sources (HH)


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

1 files changed, 0 insertions, 158 deletions

diff --git a/doc/Setoid.tex b/doc/Setoid.tex
deleted file mode 100644
index 867d603669..0000000000
--- a/doc/Setoid.tex
+++ /dev/null
@@ -1,158 +0,0 @@
-\achapter{\protect{The \texttt{setoid$\_$replace} tactic}}
-\aauthor{Cl\'ement Renard}
-\label{setoid_replace}
-\tacindex{setoid\_replace}
-
-This chapter presents  the \texttt{setoid\_replace} tactic.
-
-\asection{Description of \texttt{setoid$\_$replace}}
-
-Working on user-defined structures in \Coq\ is not very easy if
-Leibniz equality does not denote the intended equality. For example
-using lists to denote finite sets drive to difficulties since two
-non convertible terms can denote the same set.
-
-We present here a \Coq\ module, {\tt setoid\_replace}, which allows to
-structure and automate some parts of the work. In particular, if
-everything has been registered a simple
-tactic can do replacement just as if the two terms were equal.
-
-\asection{Adding new setoid or morphisms}
-
-Under the toplevel
-load the \texttt{setoid\_replace} files with the command:
-
-\begin{coq_example*}
-  Require Setoid.
-\end{coq_example*}
-
-A setoid is just a type \verb+A+ and an equivalence relation on \verb+A+.
-
-The specification of a setoid can be found in the file
-
-\begin{quotation}
-\begin{verbatim}
-theories/Setoids/Setoid.v
-\end{verbatim}
-\end{quotation}
-
-It looks like :
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Section Setoid.
-
-Variable A : Type.
-Variable Aeq : A -> A -> Prop.
-
-Record Setoid_Theory : Prop :=
-{ Seq_refl : (x:A) (Aeq x x);
-  Seq_sym : (x,y:A) (Aeq x y) -> (Aeq y x);
-  Seq_trans : (x,y,z:A) (Aeq x y) -> (Aeq y z) -> (Aeq x z)
-}.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-To define a setoid structure on \verb+A+, you must provide a relation
-\verb|Aeq| on \verb+A+ and prove that \verb|Aeq| is an equivalence
-relation. That is, you have to define an object of type
-\verb|(Setoid_Theory A Aeq)|.
-
-Finally to register a setoid the syntax is:
-
-\comindex{Add Setoid}
-\begin{quotation}
-  \texttt{Add Setoid} \textit{ A Aeq ST}
-\end{quotation}
-
-\noindent where \textit{Aeq} is a term of type \texttt{A->A->Prop} and
-\textit{ST} is a term of type 
-\texttt{(Setoid\_Theory }\textit{A Aeq}\texttt{)}.
-
-\begin{ErrMsgs}
-\item \errindex{Not a valid setoid theory}.\\ 
-  That happens when the typing condition does not hold.
-\item \errindex{A Setoid Theory is already declared for \textit{A}}.\\
-  That happens when you try to declare a second setoid theory for the
-  same type.
-\end{ErrMsgs}
-
-Currently, only one setoid structure
-may be declared for a given type.
-This allows automatic detection of the theory used to achieve the
-replacement.
-
-The table of setoid theories is compatible with the \Coq\ 
-sectioning mechanism. If you declare a setoid inside a section, the
-declaration will be thrown away when closing the section.
-And when you load a compiled file, all the \texttt{Add Setoid}
-commands of this file that are not inside a section will be loaded.
-
-\Warning Only the setoid on \texttt{Prop} is loaded by default with the
-\texttt{setoid\_replace} module. The equivalence relation used is
-\texttt{iff} {\it i.e.} the logical equivalence.
-
-\asection{Adding new morphisms}
-
-A morphism is nothing else than a function compatible with the
-equivalence relation. 
-You can only replace a term by an equivalent in position of argument
-of a morphism. That's why each morphism has to be
-declared to the system, which will ask you to prove the accurate
-compatibility lemma.
-
-The syntax is the following :
-\comindex{Add Morphism}
-\begin{quotation}
-  \texttt{Add Morphism} \textit{ f }:\textit{ ident}
-\end{quotation}
-
-\noindent where f is the name of a term which type is a non dependent
-product (the term you want to declare as a morphism) and
-\textit{ident} is a new identifier which will denote the
-compatibility lemma.
-
-\begin{ErrMsgs}
-\item \errindex{The term \term \ is already declared as a morphism}
-\item \errindex{The term \term \ is not a product}
-\item \errindex{The term \term \ should not be a dependent product}
-\end{ErrMsgs}
-
-The compatibility lemma generated depends on the setoids already
-declared.
-
-\asection{The tactic itself}
-\tacindex{setoid\_replace}
-\tacindex{setoid\_rewrite}
-
-After having registered all the setoids and morphisms you need, you can
-use the tactic called \texttt{setoid\_replace}. The syntax is
-
-\begin{quotation}
-\texttt{setoid\_replace} $ term_1$ with $term_2$
-\end{quotation}
-
-The effect is similar to the one of \texttt{replace}.
-
-You also have a tactic called \texttt{setoid\_rewrite} which is the
-equivalent of \texttt{rewrite} for setoids. The syntax is 
-
-\begin{quotation}
-\texttt{setoid\_rewrite} \term
-\end{quotation}
-
-\begin{Variants}
- \item \texttt{setoid\_rewrite ->} \term
- \item \texttt{setoid\_rewrite <-} \term
-\end{Variants}
-
-The arrow tells the system in which direction the rewriting has to be
-done. Moreover, you can use \texttt{rewrite} for setoid
-rewriting. In that case the system will check if the term you give is
-an equality or a setoid equivalence and do the appropriate work.
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: