diff options
Diffstat (limited to 'doc/RefMan-coi.tex')
| -rwxr-xr-x | doc/RefMan-coi.tex | 400 |
1 files changed, 400 insertions, 0 deletions
diff --git a/doc/RefMan-coi.tex b/doc/RefMan-coi.tex new file mode 100755 index 000000000..7de3e69fe --- /dev/null +++ b/doc/RefMan-coi.tex @@ -0,0 +1,400 @@ +%\documentstyle[11pt,../tools/coq-tex/coq]{article} +%\input{title} + +%\include{macros} +%\begin{document} + +%\coverpage{Co-inductive types in Coq}{Eduardo Gim\'enez} +\chapter{Co-inductive types in Coq}\label{Coinductives} + +%\begin{abstract} +{\it Co-inductive} types are types whose elements may not be well-founded. +A formal study of the Calculus of Constructions extended by +co-inductive types has been presented +in \cite{Gim94}. It is based on the notion of +{\it guarded definitions} introduced by Th. Coquand +in \cite{Coquand93}. The implementation is by E. Gim\'enez. +%\end{abstract} + +\section{A short introduction to co-inductive types} + +We assume that the reader is rather familiar with inductive types. +These types are characterized by their {\it constructors}, which can be +regarded as the basic methods from which the elements +of the type can be built up. It is implicit in the definition +of an inductive type that +its elements are the result of a {\it finite} number of +applications of its constructors. Co-inductive types arise from +relaxing this implicit condition and admitting that an element of +the type can also be introduced by a non-ending (but effective) process +of construction defined in terms of the basic methods which characterize the +type. So we could think in the wider notion of types defined by +constructors (let us call them {\it recursive types}) and classify +them into inductive and co-inductive ones, depending on whether or not +we consider non-ending methods as admissible for constructing elements +of the type. Note that in both cases we obtain a ``closed type'', all whose +elements are pre-determined in advance (by the constructors). When we +know that $a$ is an element of a recursive type (no matter if it is +inductive or co-inductive) what we know is that it is the result of applying +one of the basic forms of construction allowed for the type. +So the more primitive way of eliminating an element of a recursive type is +by case analysis, i.e. by considering through which constructor it could have +been introduced. In the case of inductive sets, the additional knowledge that +constructors can be applied only a finite number of times provide +us with a more powerful way of eliminating their elements, say, +the principle of +induction. This principle is obviously not valid for co-inductive types, +since it is just the expression of this extra knowledge attached to inductive +types. + + +An example of a co-inductive type is the type of infinite sequences formed with +elements of type $A$, or streams for shorter. In Coq, +it can be introduced using the \verb!CoInductive! command~: +\begin{coq_example} +CoInductive Set Stream [A:Set] := cons : A->(Stream A)->(Stream A). +\end{coq_example} + +The syntax of this command is the same as the +command \verb!Inductive! (cf. section +\ref{gal_Inductive_Definitions}). +Definition of mutually coinductive types are possible. + +As was already said, there are not principles of +induction for co-inductive sets, the only way of eliminating these +elements is by case analysis. +In the example of streams, this elimination principle can be +used for instance to define the well known +destructors on streams $\hd : (\Str\;A)\rightarrow A$ +and $\tl: (\Str\;A)\rightarrow (\Str\;A)$ : +\begin{coq_example} +Section Destructors. +Variable A : Set. +Definition hd := [x:(Stream A)]Cases x of (cons a s) => a end. +Definition tl := [x:(Stream A)]Cases x of (cons a s) => s end. +\end{coq_example} +\begin{coq_example*} +End Destructors. +\end{coq_example*} + +\subsection{Non-ending methods of construction} + +At this point the reader should have realized that we have left unexplained +what is a ``non-ending but effective process of +construction'' of a stream. In the widest sense, a +method is a non-ending process of construction if we can eliminate the +stream that it introduces, in other words, if we can reduce +any case analysis on it. In this sense, the following ways of +introducing a stream are not acceptable. +\begin{center} +$\zeros = (\cons\;\nat\;\nO\;(\tl\;\zeros))\;\;:\;\;(\Str\;\nat)$\\[12pt] +$\filter\;(\cons\;A\;a\;s) = \si\;\;(P\;a)\;\;\alors\;\;(\cons\;A\;a\;(\filter\;s))\;\;\sinon\;\;(\filter\;s) )\;\;:\;\;(\Str\;A)$ +\end{center} +\noindent The former it is not valid since the stream can not be eliminated +to obtain its tail. In the latter, a stream is naively defined as +the result of erasing from another (arbitrary) stream +all the elements which does not verify a certain property $P$. This +does not always makes sense, for example it does not when all the elements +of the stream verify $P$, in which case we can not eliminate it to +obtain its head\footnote{Note that there is no notion of ``the empty +stream'', a stream is always infinite and build by a \texttt{cons}.}. +On the contrary, the following definitions are acceptable methods for +constructing a stream~: +\begin{center} +$\zeros = (\cons\;\nat\;\nO\;\zeros)\;\;:\;\;(\Str\;\nat)\;\;\;(*)$\\[12pt] +$(\from\;n) = (\cons\;\nat\;n\;(\from\;(\nS\;n)))\;:\;(\Str\;\nat)$\\[12pt] +$\alter = (\cons\;\bool\;\true\;(\cons\;\bool\;\false\;\alter))\;:\;(\Str\;\bool)$. +\end{center} +\noindent The first one introduces a stream containing all the natural numbers +greater than a given one, and the second the stream which infinitely +alternates the booleans true and false. + +In general it is not evident to realise when a definition can +be accepted or not. However, there is a class of definitions that +can be easily recognised as being valid : those +where (1) all the recursive calls of the method are done +after having explicitly mentioned which is (at least) the first constructor +to start building the element, and (2) no other +functions apart from constructors are applied to recursive calls. +This class of definitions is usually +referred as {\it guarded-by-constructors} +definitions \cite{Coquand93,Gim94}. +The methods $\from$ +and $\alter$ are examples of definitions which are guarded by constructors. +The definition of function $\filter$ is not, because there is no +constructor to guard +the recursive call in the {\it else} branch. Neither is the one of +$\zeros$, since there is function applied to the recursive call +which is not a constructor. However, there is a difference between +the definition of $\zeros$ and $\filter$. The former may be seen as a +wrong way of characterising an object which makes sense, and it can +be reformulated in an admissible way using the equation (*). On the contrary, +the definition of +$\filter$ can not be patched, since is the idea itself +of traversing an infinite +construction searching for an element whose existence is not ensured +which does not make sense. + + + +Guarded definitions are exactly the kind of non-ending process of +construction which are allowed in Coq. The way of introducing +a guarded definition in Coq is using the special command +{\tt CoFixpoint}. This command verifies that the definition introduces an +element of a co-inductive type, and checks if it is guarded by constructors. +If we try to +introduce the definitions above, $\from$ and $\alter$ will be accepted, +while $\zeros$ and $\filter$ will be rejected giving some explanation +about why. +\begin{coq_example} +CoFixpoint zeros : (Stream nat) := (cons nat O (tl nat zeros)). +CoFixpoint zeros : (Stream nat) := (cons nat O zeros). +CoFixpoint from : nat->(Stream nat) := [n:nat](cons nat n (from (S n))). +\end{coq_example} + +As in the \verb!Fixpoint! command (cf. section~\ref{Fixpoint}), it is possible +to introduce a block of mutually dependent methods. The general syntax +for this case is : + +{\tt CoFixpoint {\ident$_1$} :{\term$_1$} := {\term$_1'$}\\ + with\\ + \mbox{}\hspace{0.1cm} $\ldots$ \\ + with {\ident$_m$} : {\term$_m$} := {\term$_m'$}} + + +\subsection{Non-ending methods and reduction} + +The elimination of a stream introduced by a \verb!CoFixpoint! definition +is done lazily, i.e. its definition can be expanded only when it occurs +at the head of an application which is the argument of a case expression. +Isolately it is considered as a canonical expression which +is completely evaluated. We can test this using the command \verb!Compute! +to calculate the normal forms of some terms~: +\begin{coq_example} +Eval Compute in (from O). +Eval Compute in (hd nat (from O)). +Eval Compute in (tl nat (from O)). +\end{coq_example} +\noindent Thus, the equality +$(\from\;n)\equiv(\cons\;\nat\;n\;(\from \; (\S\;n)))$ +does not hold as definitional one. Nevertheless, it can be proved +as a propositional equality, in the sense of Leibniz's equality. +The version {\it à la Leibniz} of the equality above follows from +a general lemma stating that eliminating and then re-introducing a stream +yields the same stream. +\begin{coq_example} +Lemma unfold_Stream : + (x:(Stream nat))(x=(Cases x of (cons a s) => (cons nat a s) end)). +\end{coq_example} + +\noindent The proof is immediate from the analysis of +the possible cases for $x$, which transforms +the equality in a trivial one. + +\begin{coq_example} +Destruct x. +Trivial. +\end{coq_example} +\begin{coq_eval} +Save. +\end{coq_eval} +The application of this lemma to $(\from\;n)$ puts this +constant at the head of an application which is an argument +of a case analysis, forcing its expansion. +We can test the type of this application using Coq's command \verb!Check!, +which infers the type of a given term. +\begin{coq_example} +Check [n:nat](unfold_Stream (from n)). +\end{coq_example} + \noindent Actually, The elimination of $(\from\;n)$ has actually +no effect, because it is followed by a re-introduction, +so the type of this application is in fact +definitionally equal to the +desired proposition. We can test this computing +the normal form of the application above to see its type. +\begin{coq_example} +Transparent unfold_Stream. +Eval Compute in [n:nat](unfold_Stream (from n)). +\end{coq_example} + + +\section{Reasoning about infinite objects} + +At a first sight, it might seem that +case analysis does not provide a very powerful way +of reasoning about infinite objects. In fact, what we can prove about +an infinite object using +only case analysis is just what we can prove unfolding its method +of construction a finite number of times, which is not always +enough. Consider for example the following method for appending +two streams~: +\begin{coq_example} +Variable A:Set. +CoFixpoint conc : (Stream A)->(Stream A)->(Stream A) + := [s1,s2:(Stream A)](cons A (hd A s1) (conc (tl A s1) s2)). +\end{coq_example} + +Informally speaking, we expect that for all pair of streams $s_1$ and $s_2$, +$(\conc\;s_1\;s_2)$ +defines the ``the same'' stream as $s_1$, +in the sense that if we would be able to unfold the definition +``up to the infinite'', we would obtain definitionally equal normal forms. +However, no finite unfolding of the definitions gives definitionally +equal terms. Their equality can not be proved just using case analysis. + + +The weakness of the elimination principle proposed for infinite objects +contrast with the power provided by the inductive +elimination principles, but it is not actually surprising. It just means +that we can not expect to prove very interesting things about infinite +objects doing finite proofs. To take advantage of infinite objects we +have to consider infinite proofs as well. For example, +if we want to catch up the equality between $(\conc\;s_1\;s_2)$ and +$s_1$ we have to introduce first the type of the infinite proofs +of equality between streams. This is a +co-inductive type, whose elements are build up from a +unique constructor, requiring a proof of the equality of the +heads of the streams, and an (infinite) proof of the equality +of their tails. + +\begin{coq_example} +CoInductive EqSt : (Stream A)->(Stream A)->Prop := + eqst : (s1,s2:(Stream A)) + (hd A s1)=(hd A s2)-> + (EqSt (tl A s1) (tl A s2))->(EqSt s1 s2). +\end{coq_example} +\noindent Now the equality of both streams can be proved introducing +an infinite object of type + +\noindent $(\EqSt\;s_1\;(\conc\;s_1\;s_2))$ by a \verb!CoFixpoint! +definition. +\begin{coq_example} +CoFixpoint eqproof : (s1,s2:(Stream A))(EqSt s1 (conc s1 s2)) + := [s1,s2:(Stream A)] + (eqst s1 (conc s1 s2) + (refl_equal A (hd A (conc s1 s2))) (eqproof (tl A s1) s2)). +\end{coq_example} +\begin{coq_eval} +Reset eqproof. +\end{coq_eval} +\noindent Instead of giving an explicit definition, +we can use the proof editor of Coq to help us in +the construction of the proof. +A tactic \verb!Cofix! allows to place a \verb!CoFixpoint! definition +inside a proof. +This tactic introduces a variable in the context which has +the same type as the current goal, and its application stands +for a recursive call in the construction of the proof. If no name is +specified for this variable, the name of the lemma is chosen by +default. +%\pagebreak + +\begin{coq_example} +Lemma eqproof : (s1,s2:(Stream A))(EqSt s1 (conc s1 s2)). +Cofix. +\end{coq_example} + +\noindent An easy (and wrong!) way of finishing the proof is just to apply the +variable \verb!eqproof!, which has the same type as the goal. + +\begin{coq_example} +Intros. +Apply eqproof. +\end{coq_example} + +\noindent The ``proof'' constructed in this way +would correspond to the \verb!CoFixpoint! definition +\begin{coq_example*} +CoFixpoint eqproof : (s1:(Stream A))(s2:(Stream A))(EqSt s1 (conc s1 s2)) + := eqproof. +\end{coq_example*} + +\noindent which is obviously non-guarded. This means that +we can use the proof editor to +define a method of construction which does not make sense. However, +the system will never accept to include it as part of the theory, +because the guard condition is always verified before saving the proof. + +\begin{coq_example} +Qed. +\end{coq_example} + +\noindent Thus, the user must be careful in the +construction of infinite proofs +with the tactic \verb!Cofix!. Remark that once it has been used +the application of tactics performing automatic proof search in +the environment (like for example \verb!Auto!) +could introduce unguarded recursive calls in the proof. +The command \verb!Guarded! allows to verify +if the guarded condition has been violated +during the construction of the proof. This command can be +applied even if the proof term is not complete. + + + +\begin{coq_example} +Restart. +Cofix. +Auto. +Guarded. +Undo. +Guarded. +\end{coq_example} + +\noindent To finish with this example, let us restart from the +beginning and show how to construct an admissible proof~: + +\begin{coq_example} +Restart. +Cofix. +\end{coq_example} + +%\pagebreak + +\begin{coq_example} +Intros. +Apply eqst. +Trivial. +Simpl. +Apply eqproof. +Qed. +\end{coq_example} + + +\section{Experiments with co-inductive types} + +Some examples involving co-inductive types are available with +the distributed system, in the theories library and in the contributions +of the Lyon site. Here we present a short description of their contents~: +\begin{itemize} +\item Directory \verb!theories/LISTS! : + \begin{itemize} + \item File \verb!Streams.v! : The type of streams and the +extensional equality between streams. + \end{itemize} + +\item Directory \verb!contrib/Lyon/COINDUCTIVES! : + \begin{itemize} + \item Directory \verb!ARITH! : An arithmetic where $\infty$ +is an explicit constant of the language instead of a metatheoretical notion. + \item Directory \verb!STREAM! : + \begin{itemize} + \item File \verb!Examples! : +Several examples of guarded definitions, as well as +of frequent errors in the introduction of a stream. A different +way of defining the extensional equality of two streams, +and the proofs showing that it is equivalent to the one in \verb!theories!. + \item File \verb!Alter.v! : An example showing how +an infinite proof introduced by a guarded definition can be also described +using an operator of co-recursion \cite{Gimenez95b}. + \end{itemize} +\item Directory \verb!PROCESSES! : A proof of the alternating +bit protocol based on Pra\-sad's Calculus of Broadcasting Systems \cite{Prasad93}, +and the verification of an interpreter for this calculus. +See \cite{Gimenez95b} for a complete description about this development. + \end{itemize} +\end{itemize} + +%\end{document} + +% $Id$ |