1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
|
%\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{Co-inductives}}
%\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 co-inductive 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) (eq_refl (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 placing 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! verifies
that the guarded condition has been not 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}
|