diff options
Diffstat (limited to 'doc/refman/Setoid.tex')
| -rw-r--r-- | doc/refman/Setoid.tex | 559 |
1 files changed, 0 insertions, 559 deletions
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex deleted file mode 100644 index 030400e5..00000000 --- a/doc/refman/Setoid.tex +++ /dev/null @@ -1,559 +0,0 @@ -\newtheorem{cscexample}{Example} - -\achapter{\protect{User defined equalities and relations}} -\aauthor{Claudio Sacerdoti Coen\footnote{Based on previous work by -Cl\'ement Renard}} -\label{setoid_replace} -\tacindex{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). - -The work generalizes, and is partially based on, a previous implementation of -the \texttt{setoid\_replace} tactic by Cl\'ement Renard. - -\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 $m, n$ 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 parametric relations that are instances of -$R_1$ and $R_2$ is written $R_1 \texttt{++>} R_2$. -Notice that the special arrow \texttt{++>}, which reminds the reader -of covariance, is placed between the two parametric relations, not -between the two carriers or the two relation instances. - -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}$ 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} is -\texttt{set\_eq ==> set\_eq ==> set\_eq}. -\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} - -Notice that Leibniz equality is a relation and that 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 ($x_1$:$T_1$) \ldots ($x_n$:$T_n$), - relation (A $x_1$ \ldots $x_n$)} over \textit{(A $x_1$ \ldots $x_n$)} -can be declared with the following command - -\comindex{Add Relation} -\begin{verse} - \texttt{Add Relation} \textit{A Aeq}\\ - ~\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{verse} -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 \textit{A} is required to be a term having the same parameters -of \textit{Aeq}. This is a limitation of the tactic that is often unproblematic -in practice. - -The proofs of reflexivity, symmetry and transitivity can be omitted if the -relation is not an equivalence relation. - -If \textit{Aeq} is a transitive relation, then the command also generates -a lemma of type: -\begin{quote} -\texttt{forall ($x_1$:$T_1$)\ldots($x_n$:$T_n$) - (x y x' y': (A $x_1$ \ldots $x_n$))\\ - Aeq $x_1$ \ldots $x_n$ x' x -> Aeq $x_1$ \ldots $x_n$ y y' ->\\ - (Aeq $x_1$ \ldots $x_n$ x y -> Aeq $x_1$ \ldots $x_n$ x' y')} -\end{quote} -that is used to declare \textit{Aeq} as a parametric morphism of signature -\texttt{Aeq -{}-> Aeq ++> impl} where \texttt{impl} is logical implication -seen as a parametric relation over \texttt{Aeq}. - -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 Morphism} -\begin{verse} - \texttt{Add Morphism} \textit{f}\\ - \texttt{~with signature} \textit{sig}\\ - \texttt{~as id}.\\ - \texttt{Proof}\\ - ~\ldots\\ - \texttt{Qed} -\end{verse} - -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 by the command to generate fresh names for automatically -provided lemmas used internally. The number of parameters for \textit{f} -is inferred by comparing its type with the provided signature. -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{verbatim} -Require Export Relation_Definitions. -Require Export Setoid. -Set Implicit Arguments. -Set Contextual Implicit. -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) 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 Relation set 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 Morphism union - with signature eq_set ==> eq_set ==> eq_set - as union_mor. -Proof. - exact union_compat. -Qed. -\end{verbatim} - -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{verbatim} -Goal forall (S: set nat), - eq_set (union (union S empty) S) (union S S). -Proof. - intros. - rewrite (@empty_neutral). - reflexivity. -Qed. -\end{verbatim} -\end{cscexample} - -The tables of relations and morphisms are compatible with the \Coq\ -sectioning mechanism. If you declare a relation or a morphism inside a section, -the declaration will be thrown away when closing the section. -And when you load a compiled file, all the declarations -of this file that were not inside a section 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} - -An error message will be raised by the \texttt{rewrite} and \texttt{replace} -tactics when the user is trying to replace a term that occurs in the -wrong position. - -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. When non reflexive relations are involved, different -choices lead to different sets of new goals to prove. In this case the -tactic automatically picks one choice, but raises a warning describing the -set of alternative new goals. To force one particular choice, the user -can switch to the following alternative syntax for rewriting: - -\comindex{setoid\_rewrite} -\begin{verse} - \texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term} - \zeroone{\texttt{in} \textit{ident}}\\ - \texttt{~generate side conditions} - \textit{term}$_1$ \ldots \textit{term}$_n$\\ -\end{verse} -Up to the \texttt{generate side conditions} part, the syntax is -equivalent to the -one of the \texttt{rewrite} tactic. Additionally, the user can specify a list -of new goals that the tactic must generate. The tactic will prune out from -the alternative choices those choices that do not open at least the user -proposed goals. Thus, providing enough side conditions, the user can restrict -the tactic to at most one choice. - -\begin{cscexample} -Let \texttt{[=]+} and \texttt{[=]-} be the smaller partial equivalence -relations over positive (resp. negative) integers. Integer multiplication -can be declared as a morphism with the following signatures: -\texttt{Zmult: Zlt ++> [=]+ ==> Zlt} (multiplication with a positive number -is increasing) and -\texttt{Zmult: Zlt -{}-> [=]- ==> Zlt} (multiplication with a negative number -is decreasing). -Given the hypothesis \texttt{H: x < y} and the goal -\texttt{(x * n) * m < 0} the tactic \texttt{rewrite H} proposes -two alternative sets of goals that correspond to proving that \texttt{n} -and \texttt{m} are both positive or both negative. -\begin{itemize} - \item \texttt{\ldots $\vdash$ (y * n) * m < 0}\\ - \texttt{\ldots $\vdash$ n [=]+ n}\\ - \texttt{\ldots $\vdash$ m [=]+ m}\\ - \item \texttt{\ldots $\vdash$ (y * n) * m < 0}\\ - \texttt{\ldots $\vdash$ n [=]- n} \\ - \texttt{\ldots $\vdash$ m [=]- m} -\end{itemize} -Remember that \texttt{n [=]+ n} is equivalent to \texttt{n=n $\land$ n > 0}. - -To pick the second set of goals it is sufficient to use -\texttt{setoid\_rewrite H generate side conditions (m [=]- m)} -since the side condition \texttt{m [=]- m} is contained only in the second set -of goals. -\end{cscexample} - -\asection{First class setoids and morphisms} -First class setoids and morphisms can also be handled by encoding them -as records. The projections of the setoid relation and of the morphism -function can be registered as parametric relations and morphisms, as -illustrated by the following example. -\begin{cscexample}[First class setoids] -\begin{verbatim} -Require Export Relation_Definitions. -Require Setoid. - -Record Setoid: Type := -{ car:Type; - eq:car->car->Prop; - refl: reflexive _ eq; - sym: symmetric _ eq; - trans: transitive _ eq -}. - -Add Relation car eq - reflexivity proved by refl - symmetry proved by symm - transitivity proved by trans -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 Morphism f with signature eq ==> eq as apply_mor. -Proof. - intros S1 S2 m. - 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{verbatim} -\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{generate side conditions} or \texttt{using relation}. - -\comindex{setoid\_reflexivity} -\begin{verse} - \texttt{setoid\_reflexivity} -\end{verse} - -\comindex{setoid\_symmetry} -\begin{verse} - \texttt{setoid\_symmetry} - \zeroone{\texttt{in} \textit{ident}}\\ -\end{verse} - -\comindex{setoid\_transitivity} -\begin{verse} - \texttt{setoid\_transitivity} -\end{verse} - -\comindex{setoid\_rewrite} -\begin{verse} - \texttt{setoid\_rewrite} \zeroone{\textit{orientation}} \textit{term}\\ - ~\zeroone{\texttt{in} \textit{ident}}\\ - ~\zeroone{\texttt{generate side conditions} - \textit{term}$_1$ \ldots \textit{term}$_n$}\\ -\end{verse} - -The \texttt{generate side conditions} argument cannot be passed to the -unprefixed form. - -\comindex{setoid\_replace} -\begin{verse} - \texttt{setoid\_replace} \textit{term} \texttt{with} \textit{term} - ~\zeroone{\texttt{in} \textit{ident}}\\ - ~\zeroone{\texttt{using relation} \textit{term}}\\ - ~\zeroone{\texttt{generate side conditions} - \textit{term}$_1$ \ldots \textit{term}$_n$}\\ - ~\zeroone{\texttt{by} \textit{tactic}} -\end{verse} - -The \texttt{generate side conditions} and \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 Leibniz equality. - -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 Setoids} command shows the list of currently registered -parametric relations and morphisms. For each morphism its signature is also -given. When the rewriting tactics refuse to replace a term in a context -because the latter is not a composition of morphisms, the \texttt{Print Setoids} -command is 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{verse} - \texttt{Add Setoid} \textit{A Aeq ST} \texttt{as} \textit{ident} -\end{verse} -where \textit{Aeq} is a congruence relation without parameters, -\textit{A} is its carrier and \textit{ST} is an object of type -\verb|(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{verse} - \texttt{Add Morphism} \textit{ f }:\textit{ ident}.\\ - Proof.\\ - \ldots\\ - Qed. -\end{verse} - -The latter command 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. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: |