%\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$