From 8f4d4c66134804bbf2d2fe65c893b68387272d31 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 10 Jul 2010 15:57:24 +0100 Subject: Remove non-DFSG contents --- doc/refman/RefMan-coi.tex | 406 ---------------------------------------------- 1 file changed, 406 deletions(-) delete mode 100644 doc/refman/RefMan-coi.tex (limited to 'doc/refman/RefMan-coi.tex') diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex deleted file mode 100644 index b0f0212e..00000000 --- a/doc/refman/RefMan-coi.tex +++ /dev/null @@ -1,406 +0,0 @@ -%\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]{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 Stream (A:Set) : 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) := match x with - | cons a s => a - end. -Definition tl (x:Stream A) := match x with - | 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 0%N (tl nat zeros). -CoFixpoint zeros : Stream nat := cons nat 0%N zeros. -CoFixpoint from (n:nat) : Stream nat := cons nat n (from (S n)). -\end{coq_example} - -As in the \verb!Fixpoint! command (see 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 0). -Eval compute in (hd nat (from 0)). -Eval compute in (tl nat (from 0)). -\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 : - forall x:Stream nat, x = match x with - | 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} -olddestruct x. -trivial. -\end{coq_example} -\begin{coq_eval} -Qed. -\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 (fun 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 (fun 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 (s1 s2:Stream A) : 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 : - forall 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) := - eqst s1 (conc s1 s2) (refl_equal (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 : forall 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 : forall s1 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: RefMan-coi.tex 10421 2008-01-05 14:06:51Z herbelin $ -- cgit v1.2.3