Mercurial > cpdt > repo

comparison src/Coinductive.v @ 437:8077352044b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass over all formatting, after big pile of coqdoc changes
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 16:47:28 -0400
parents 5d5e44f905c7
children f923024bd284
comparison
equal deleted inserted replaced
436:5d5e44f905c7 437:8077352044b2
48 CoInductive stream : Type := 48 CoInductive stream : Type :=
49 | Cons : A -> stream -> stream. 49 | Cons : A -> stream -> stream.
50 End stream. 50 End stream.
51 51
52 (* begin hide *) 52 (* begin hide *)
53 (* begin thide *)
53 CoInductive evilStream := Nil. 54 CoInductive evilStream := Nil.
55 (* end thide *)
54 (* end hide *) 56 (* end hide *)
55 57
56 (** The definition is surprisingly simple. Starting from the definition of [list], we just need to change the keyword [Inductive] to [CoInductive]. We could have left a [Nil] constructor in our definition, but we will leave it out to force all of our streams to be infinite. 58 (** The definition is surprisingly simple. Starting from the definition of [list], we just need to change the keyword [Inductive] to [CoInductive]. We could have left a [Nil] constructor in our definition, but we will leave it out to force all of our streams to be infinite.
57 59
58 How do we write down a stream constant? Obviously simple application of constructors is not good enough, since we could only denote finite objects that way. Rather, whereas recursive definitions were necessary to _use_ values of recursive inductive types effectively, here we find that we need%\index{co-recursive definitions}% _co-recursive definitions_ to _build_ values of co-inductive types effectively. 60 How do we write down a stream constant? Obviously simple application of constructors is not good enough, since we could only denote finite objects that way. Rather, whereas recursive definitions were necessary to _use_ values of recursive inductive types effectively, here we find that we need%\index{co-recursive definitions}% _co-recursive definitions_ to _build_ values of co-inductive types effectively.
103 *) 105 *)
104 106
105 (* end thide *) 107 (* end thide *)
106 108
107 (* begin hide *) 109 (* begin hide *)
110 (* begin thide *)
108 Definition looper := 0. 111 Definition looper := 0.
112 (* end thide *)
109 (* end hide *) 113 (* end hide *)
110 114
111 (** So far, it looks like co-inductive types might be a magic bullet, allowing us to import all of the Haskeller's usual tricks. However, there are important restrictions that are dual to the restrictions on the use of inductive types. Fixpoints _consume_ values of inductive types, with restrictions on which _arguments_ may be passed in recursive calls. Dually, co-fixpoints _produce_ values of co-inductive types, with restrictions on what may be done with the _results_ of co-recursive calls. 115 (** So far, it looks like co-inductive types might be a magic bullet, allowing us to import all of the Haskeller's usual tricks. However, there are important restrictions that are dual to the restrictions on the use of inductive types. Fixpoints _consume_ values of inductive types, with restrictions on which _arguments_ may be passed in recursive calls. Dually, co-fixpoints _produce_ values of co-inductive types, with restrictions on what may be done with the _results_ of co-recursive calls.
112 116
113 The restriction for co-inductive types shows up as the%\index{guardedness condition}% _guardedness condition_. First, consider this stream definition, which would be legal in Haskell. 117 The restriction for co-inductive types shows up as the%\index{guardedness condition}% _guardedness condition_. First, consider this stream definition, which would be legal in Haskell.
137 | Cons h t => Cons (f h) (map t) 141 | Cons h t => Cons (f h) (map t)
138 end. 142 end.
139 End map. 143 End map.
140 144
141 (* begin hide *) 145 (* begin hide *)
146 (* begin thide *)
142 Definition filter := 0. 147 Definition filter := 0.
148 (* end thide *)
143 (* end hide *) 149 (* end hide *)
144 150
145 (** This code is a literal copy of that for the list [map] function, with the [nil] case removed and [Fixpoint] changed to [CoFixpoint]. Many other standard functions on lazy data structures can be implemented just as easily. Some, like [filter], cannot be implemented. Since the predicate passed to [filter] may reject every element of the stream, we cannot satisfy the guardedness condition. 151 (** This code is a literal copy of that for the list [map] function, with the [nil] case removed and [Fixpoint] changed to [CoFixpoint]. Many other standard functions on lazy data structures can be implemented just as easily. Some, like [filter], cannot be implemented. Since the predicate passed to [filter] may reject every element of the stream, we cannot satisfy the guardedness condition.
146 152
147 The implications of the condition can be subtle. To illustrate how, we start off with another co-recursive function definition that _is_ legal. The function [interleave] takes two streams and produces a new stream that alternates between their elements. *) 153 The implications of the condition can be subtle. To illustrate how, we start off with another co-recursive function definition that _is_ legal. The function [interleave] takes two streams and produces a new stream that alternates between their elements. *)
213 (** The obvious statement of the equality is this: *) 219 (** The obvious statement of the equality is this: *)
214 220
215 Theorem ones_eq : ones = ones'. 221 Theorem ones_eq : ones = ones'.
216 222
217 (* begin hide *) 223 (* begin hide *)
224 (* begin thide *)
218 Definition foo := @eq. 225 Definition foo := @eq.
226 (* end thide *)
219 (* end hide *) 227 (* end hide *)
220 228
221 (** However, faced with the initial subgoal, it is not at all clear how this theorem can be proved. In fact, it is unprovable. The [eq] predicate that we use is fundamentally limited to equalities that can be demonstrated by finite, syntactic arguments. To prove this equivalence, we will need to introduce a new relation. *) 229 (** However, faced with the initial subgoal, it is not at all clear how this theorem can be proved. In fact, it is unprovable. The [eq] predicate that we use is fundamentally limited to equalities that can be demonstrated by finite, syntactic arguments. To prove this equivalence, we will need to introduce a new relation. *)
222 (* begin thide *) 230 (* begin thide *)
223 231