annotate src/Coinductive.v @ 346:5d85de065540

Pass through Coinductive up to PL example
author Adam Chlipala <adam@chlipala.net>
date Sun, 23 Oct 2011 13:33:46 -0400
parents d5787b70cf48
children 36a08cad9245
rev   line source
adam@346 1 (* Copyright (c) 2008-2011, Adam Chlipala
adamc@62 2 *
adamc@62 3 * This work is licensed under a
adamc@62 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@62 5 * Unported License.
adamc@62 6 * The license text is available at:
adamc@62 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@62 8 *)
adamc@62 9
adamc@62 10 (* begin hide *)
adamc@62 11 Require Import List.
adamc@62 12
adam@314 13 Require Import CpdtTactics.
adamc@62 14
adamc@62 15 Set Implicit Arguments.
adamc@62 16 (* end hide *)
adamc@62 17
adamc@62 18
adamc@62 19 (** %\chapter{Infinite Data and Proofs}% *)
adamc@62 20
adam@346 21 (** In lazy functional programming languages like %\index{Haskell}%Haskell, infinite data structures are everywhere. Infinite lists and more exotic datatypes provide convenient abstractions for communication between parts of a program. Achieving similar convenience without infinite lazy structures would, in many cases, require acrobatic inversions of control flow.
adamc@62 22
adam@346 23 %\index{laziness}%Laziness is easy to implement in Haskell, where all the definitions in a program may be thought of as mutually recursive. In such an unconstrained setting, it is easy to implement an infinite loop when you really meant to build an infinite list, where any finite prefix of the list should be forceable in finite time. Haskell programmers learn how to avoid such slip-ups. In Coq, such a laissez-faire policy is not good enough.
adamc@62 24
adam@346 25 We spent some time in the last chapter discussing the %\index{Curry-Howard correspondence}%Curry-Howard isomorphism, where proofs are identified with functional programs. In such a setting, infinite loops, intended or otherwise, are disastrous. If Coq allowed the full breadth of definitions that Haskell did, we could code up an infinite loop and use it to prove any proposition vacuously. That is, the addition of general recursion would make CIC %\textit{%#<i>#inconsistent#</i>#%}%. For an arbitrary proposition [P], we could write:
adamc@202 26 [[
adamc@202 27 Fixpoint bad (u : unit) : P := bad u.
adamc@205 28 ]]
adamc@205 29
adamc@202 30 This would leave us with [bad tt] as a proof of [P].
adamc@62 31
adamc@62 32 There are also algorithmic considerations that make universal termination very desirable. We have seen how tactics like [reflexivity] compare terms up to equivalence under computational rules. Calls to recursive, pattern-matching functions are simplified automatically, with no need for explicit proof steps. It would be very hard to hold onto that kind of benefit if it became possible to write non-terminating programs; we would be running smack into the halting problem.
adamc@62 33
adam@292 34 One solution is to use types to contain the possibility of non-termination. For instance, we can create a %``%#"#non-termination monad,#"#%''% inside which we must write all of our general-recursive programs. This is a heavyweight solution, and so we would like to avoid it whenever possible.
adamc@62 35
adam@346 36 Luckily, Coq has special support for a class of lazy data structures that happens to contain most examples found in Haskell. That mechanism, %\index{co-inductive types}\textit{%#<i>#co-inductive types#</i>#%}%, is the subject of this chapter. *)
adamc@62 37
adamc@62 38
adamc@62 39 (** * Computing with Infinite Data *)
adamc@62 40
adam@346 41 (** Let us begin with the most basic type of infinite data, %\textit{%#<i>#streams#</i>#%}%, or lazy lists.%\index{Vernacular commands!CoInductive}% *)
adamc@62 42
adamc@62 43 Section stream.
adamc@62 44 Variable A : Set.
adamc@62 45
adamc@62 46 CoInductive stream : Set :=
adamc@62 47 | Cons : A -> stream -> stream.
adamc@62 48 End stream.
adamc@62 49
adamc@62 50 (** 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.
adamc@62 51
adam@346 52 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 %\textit{%#<i>#use#</i>#%}% values of recursive inductive types effectively, here we find that we need %\index{co-recursive definitions}\textit{%#<i>#co-recursive definitions#</i>#%}% to %\textit{%#<i>#build#</i>#%}% values of co-inductive types effectively.
adamc@62 53
adam@346 54 We can define a stream consisting only of zeroes.%\index{Vernacular commands!CoFixpoint}% *)
adamc@62 55
adamc@62 56 CoFixpoint zeroes : stream nat := Cons 0 zeroes.
adamc@62 57
adam@346 58 (* EX: Define a stream that alternates between [true] and [false]. *)
adam@346 59 (* begin thide *)
adam@346 60
adamc@62 61 (** We can also define a stream that alternates between [true] and [false]. *)
adamc@62 62
adam@346 63 CoFixpoint trues_falses : stream bool := Cons true falses_trues
adam@346 64 with falses_trues : stream bool := Cons false trues_falses.
adam@346 65 (* end thide *)
adamc@62 66
adamc@62 67 (** Co-inductive values are fair game as arguments to recursive functions, and we can use that fact to write a function to take a finite approximation of a stream. *)
adamc@62 68
adam@346 69 (* EX: Defint a function to calculate a finite approximation of a stream, to a particular length. *)
adam@346 70 (* begin thide *)
adam@346 71
adamc@211 72 Fixpoint approx A (s : stream A) (n : nat) : list A :=
adamc@62 73 match n with
adamc@62 74 | O => nil
adamc@62 75 | S n' =>
adamc@62 76 match s with
adamc@62 77 | Cons h t => h :: approx t n'
adamc@62 78 end
adamc@62 79 end.
adamc@62 80
adamc@62 81 Eval simpl in approx zeroes 10.
adamc@211 82 (** %\vspace{-.15in}% [[
adamc@62 83 = 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: nil
adamc@62 84 : list nat
adam@302 85 ]]
adam@302 86 *)
adamc@211 87
adam@346 88 Eval simpl in approx trues_falses 10.
adamc@211 89 (** %\vspace{-.15in}% [[
adamc@62 90 = true
adamc@62 91 :: false
adamc@62 92 :: true
adamc@62 93 :: false
adamc@62 94 :: true :: false :: true :: false :: true :: false :: nil
adamc@62 95 : list bool
adam@346 96 ]]
adam@346 97 *)
adamc@62 98
adam@346 99 (* end thide *)
adamc@62 100
adam@346 101 (** 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 %\textit{%#<i>#consume#</i>#%}% values of inductive types, with restrictions on which %\textit{%#<i>#arguments#</i>#%}% may be passed in recursive calls. Dually, co-fixpoints %\textit{%#<i>#produce#</i>#%}% values of co-inductive types, with restrictions on what may be done with the %\textit{%#<i>#results#</i>#%}% of co-recursive calls.
adamc@62 102
adam@346 103 The restriction for co-inductive types shows up as the %\index{guardedness condition}\textit{%#<i>#guardedness condition#</i>#%}%, and it can be broken into two parts. First, consider this stream definition, which would be legal in Haskell.
adamc@62 104 [[
adamc@62 105 CoFixpoint looper : stream nat := looper.
adam@346 106 ]]
adamc@205 107
adam@346 108 <<
adamc@62 109 Error:
adamc@62 110 Recursive definition of looper is ill-formed.
adamc@62 111 In environment
adamc@62 112 looper : stream nat
adamc@62 113
adamc@62 114 unguarded recursive call in "looper"
adam@346 115 >>
adamc@205 116
adamc@211 117 The rule we have run afoul of here is that %\textit{%#<i>#every co-recursive call must be guarded by a constructor#</i>#%}%; that is, every co-recursive call must be a direct argument to a constructor of the co-inductive type we are generating. It is a good thing that this rule is enforced. If the definition of [looper] were accepted, our [approx] function would run forever when passed [looper], and we would have fallen into inconsistency.
adamc@62 118
adam@346 119 Some familiar functions are easy to write in co-recursive fashion. *)
adamc@62 120
adamc@62 121 Section map.
adamc@62 122 Variables A B : Set.
adamc@62 123 Variable f : A -> B.
adamc@62 124
adamc@62 125 CoFixpoint map (s : stream A) : stream B :=
adamc@62 126 match s with
adamc@62 127 | Cons h t => Cons (f h) (map t)
adamc@62 128 end.
adamc@62 129 End map.
adamc@62 130
adam@346 131 (** 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.
adamc@62 132
adam@346 133 The implications of the condition can be subtle. To illustrate how, we start off with another co-recursive function definition that %\textit{%#<i>#is#</i>#%}% legal. The function [interleave] takes two streams and produces a new stream that alternates between their elements. *)
adamc@62 134
adamc@62 135 Section interleave.
adamc@62 136 Variable A : Set.
adamc@62 137
adamc@62 138 CoFixpoint interleave (s1 s2 : stream A) : stream A :=
adamc@62 139 match s1, s2 with
adamc@62 140 | Cons h1 t1, Cons h2 t2 => Cons h1 (Cons h2 (interleave t1 t2))
adamc@62 141 end.
adamc@62 142 End interleave.
adamc@62 143
adamc@62 144 (** Now say we want to write a weird stuttering version of [map] that repeats elements in a particular way, based on interleaving. *)
adamc@62 145
adamc@62 146 Section map'.
adamc@62 147 Variables A B : Set.
adamc@62 148 Variable f : A -> B.
adamc@68 149 (* begin thide *)
adamc@62 150 (** [[
adamc@62 151 CoFixpoint map' (s : stream A) : stream B :=
adamc@62 152 match s with
adam@346 153 | Cons h t => interleave (Cons (f h) (map' t)) (Cons (f h) (map' t))
adamc@68 154 end.
adamc@205 155 ]]
adamc@211 156
adam@346 157 We get another error message about an unguarded recursive call. *)
adamc@62 158
adam@346 159 End map'.
adam@346 160
adam@346 161 (** What is going wrong here? Imagine that, instead of [interleave], we had called some other, less well-behaved function on streams. Here is one simpler example demonstrating the essential pitfall. We start defining a standard function for taking the tail of a stream. Since streams are infinite, this operation is total. *)
adam@346 162
adam@346 163 Definition tl A (s : stream A) : stream A :=
adam@346 164 match s with
adam@346 165 | Cons _ s' => s'
adam@346 166 end.
adam@346 167
adam@346 168 (** Coq rejects the following definition that uses [tl].
adam@346 169 [[
adam@346 170 CoFixpoint bad : stream nat := tl (Cons 0 bad).
adam@346 171 ]]
adam@346 172
adam@346 173 Imagine that Coq had accepted our definition, and consider how we might evaluate [approx bad 1]. We would be trying to calculate the first element in the stream [bad]. However, it is not hard to see that the definition of [bad] %``%#"#begs the question#"#%''%: unfolding the definition of [tl], we see that we essentially say %``%#"#define [bad] to equal itself#"#%''%! Of course such an equation admits no single well-defined solution, which does not fit well with the determinism of Gallina reduction.
adam@346 174
adam@346 175 Since Coq can be considered to check definitions after inlining and simplification of previously defined identifiers, the basic guardedness condition rules out our definition of [bad]. Such an inlining reduces [bad] to:
adam@346 176 [[
adam@346 177 CoFixpoint bad : stream nat := bad.
adam@346 178 ]]
adam@346 179 This is the same looping definition we rejected earlier. A similar inlining process reveals the way that Coq saw our failed definition of [map']:
adam@346 180 [[
adam@346 181 CoFixpoint map' (s : stream A) : stream B :=
adam@346 182 match s with
adam@346 183 | Cons h t => Cons (f h) (Cons (f h) (interleave (map' t) (map' t)))
adam@346 184 end.
adam@346 185 ]]
adam@346 186 Clearly in this case the [map'] calls are not immediate arguments to constructors, so we violate the guardedness condition. *)
adamc@68 187 (* end thide *)
adamc@211 188
adam@346 189 (** A more interesting question is why that condition is the right one. We can make an intuitive argument that the original [map'] definition is perfectly reasonable and denotes a well-understood transformation on streams, such that every output would behave properly with [approx]. The guardedness condition is an example of a syntactic check for %\index{productivity}\emph{%#<i>#productivity#</i>#%}% of co-recursive definitions. A productive definition can be thought of as one whose outputs can be forced in finite time to any finite approximation level, as with [approx]. If we replaced the guardedness condition with more involved checks, we might be able to detect and allow a broader range of productive definitions. However, mistakes in these checks could cause inconsistency, and programmers would need to understand the new, more complex checks. Coq's design strikes a balance between consistency and simplicity with its choice of guard condition, though we can imagine other worthwhile balances being struck, too. *)
adamc@62 190
adamc@63 191
adamc@63 192 (** * Infinite Proofs *)
adamc@63 193
adamc@63 194 (** Let us say we want to give two different definitions of a stream of all ones, and then we want to prove that they are equivalent. *)
adamc@63 195
adamc@63 196 CoFixpoint ones : stream nat := Cons 1 ones.
adamc@63 197 Definition ones' := map S zeroes.
adamc@63 198
adamc@63 199 (** The obvious statement of the equality is this: *)
adamc@63 200
adamc@63 201 Theorem ones_eq : ones = ones'.
adamc@63 202
adamc@63 203 (** 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. *)
adamc@68 204 (* begin thide *)
adamc@211 205
adamc@63 206 Abort.
adamc@63 207
adamc@63 208 (** Co-inductive datatypes make sense by analogy from Haskell. What we need now is a %\textit{%#<i>#co-inductive proposition#</i>#%}%. That is, we want to define a proposition whose proofs may be infinite, subject to the guardedness condition. The idea of infinite proofs does not show up in usual mathematics, but it can be very useful (unsurprisingly) for reasoning about infinite data structures. Besides examples from Haskell, infinite data and proofs will also turn out to be useful for modelling inherently infinite mathematical objects, like program executions.
adamc@63 209
adam@346 210 We are ready for our first %\index{co-inductive predicates}%co-inductive predicate. *)
adamc@63 211
adamc@63 212 Section stream_eq.
adamc@63 213 Variable A : Set.
adamc@63 214
adamc@63 215 CoInductive stream_eq : stream A -> stream A -> Prop :=
adamc@63 216 | Stream_eq : forall h t1 t2,
adamc@63 217 stream_eq t1 t2
adamc@63 218 -> stream_eq (Cons h t1) (Cons h t2).
adamc@63 219 End stream_eq.
adamc@63 220
adamc@63 221 (** We say that two streams are equal if and only if they have the same heads and their tails are equal. We use the normal finite-syntactic equality for the heads, and we refer to our new equality recursively for the tails.
adamc@63 222
adamc@63 223 We can try restating the theorem with [stream_eq]. *)
adamc@63 224
adamc@63 225 Theorem ones_eq : stream_eq ones ones'.
adamc@63 226 (** Coq does not support tactical co-inductive proofs as well as it supports tactical inductive proofs. The usual starting point is the [cofix] tactic, which asks to structure this proof as a co-fixpoint. *)
adamc@211 227
adamc@63 228 cofix.
adamc@63 229 (** [[
adamc@63 230 ones_eq : stream_eq ones ones'
adamc@63 231 ============================
adamc@63 232 stream_eq ones ones'
adamc@211 233
adamc@211 234 ]]
adamc@63 235
adamc@211 236 It looks like this proof might be easier than we expected! *)
adamc@63 237
adamc@63 238 assumption.
adamc@63 239 (** [[
adamc@211 240 Proof completed.
adamc@211 241 ]]
adamc@63 242
adamc@211 243 Unfortunately, we are due for some disappointment in our victory lap.
adamc@211 244 [[
adamc@63 245 Qed.
adam@346 246 ]]
adamc@63 247
adam@346 248 <<
adamc@63 249 Error:
adamc@63 250 Recursive definition of ones_eq is ill-formed.
adamc@63 251
adamc@63 252 In environment
adamc@63 253 ones_eq : stream_eq ones ones'
adamc@63 254
adamc@205 255 unguarded recursive call in "ones_eq"
adam@346 256 >>
adamc@205 257
adamc@211 258 Via the Curry-Howard correspondence, the same guardedness condition applies to our co-inductive proofs as to our co-inductive data structures. We should be grateful that this proof is rejected, because, if it were not, the same proof structure could be used to prove any co-inductive theorem vacuously, by direct appeal to itself!
adamc@63 259
adam@346 260 Thinking about how Coq would generate a proof term from the proof script above, we see that the problem is that we are violating the guardedness condition. During our proofs, Coq can help us check whether we have yet gone wrong in this way. We can run the command [Guarded] in any context to see if it is possible to finish the proof in a way that will yield a properly guarded proof term.%\index{Vernacular command!Guarded}%
adamc@63 261 [[
adamc@63 262 Guarded.
adamc@205 263 ]]
adamc@205 264
adamc@63 265 Running [Guarded] here gives us the same error message that we got when we tried to run [Qed]. In larger proofs, [Guarded] can be helpful in detecting problems %\textit{%#<i>#before#</i>#%}% we think we are ready to run [Qed].
adamc@63 266
adam@281 267 We need to start the co-induction by applying [stream_eq]'s constructor. To do that, we need to know that both arguments to the predicate are [Cons]es. Informally, this is trivial, but [simpl] is not able to help us. *)
adamc@63 268
adamc@63 269 Undo.
adamc@63 270 simpl.
adamc@63 271 (** [[
adamc@63 272 ones_eq : stream_eq ones ones'
adamc@63 273 ============================
adamc@63 274 stream_eq ones ones'
adamc@211 275
adamc@211 276 ]]
adamc@63 277
adamc@211 278 It turns out that we are best served by proving an auxiliary lemma. *)
adamc@211 279
adamc@63 280 Abort.
adamc@63 281
adamc@63 282 (** First, we need to define a function that seems pointless on first glance. *)
adamc@63 283
adamc@63 284 Definition frob A (s : stream A) : stream A :=
adamc@63 285 match s with
adamc@63 286 | Cons h t => Cons h t
adamc@63 287 end.
adamc@63 288
adamc@63 289 (** Next, we need to prove a theorem that seems equally pointless. *)
adamc@63 290
adamc@63 291 Theorem frob_eq : forall A (s : stream A), s = frob s.
adamc@63 292 destruct s; reflexivity.
adamc@63 293 Qed.
adamc@63 294
adamc@63 295 (** But, miraculously, this theorem turns out to be just what we needed. *)
adamc@63 296
adamc@63 297 Theorem ones_eq : stream_eq ones ones'.
adamc@63 298 cofix.
adamc@63 299
adamc@63 300 (** We can use the theorem to rewrite the two streams. *)
adamc@211 301
adamc@63 302 rewrite (frob_eq ones).
adamc@63 303 rewrite (frob_eq ones').
adamc@63 304 (** [[
adamc@63 305 ones_eq : stream_eq ones ones'
adamc@63 306 ============================
adamc@63 307 stream_eq (frob ones) (frob ones')
adamc@211 308
adamc@211 309 ]]
adamc@63 310
adamc@211 311 Now [simpl] is able to reduce the streams. *)
adamc@63 312
adamc@63 313 simpl.
adamc@63 314 (** [[
adamc@63 315 ones_eq : stream_eq ones ones'
adamc@63 316 ============================
adamc@63 317 stream_eq (Cons 1 ones)
adamc@63 318 (Cons 1
adamc@63 319 ((cofix map (s : stream nat) : stream nat :=
adamc@63 320 match s with
adamc@63 321 | Cons h t => Cons (S h) (map t)
adamc@63 322 end) zeroes))
adamc@211 323
adamc@211 324 ]]
adamc@63 325
adam@346 326 Note that [cofix] notation for anonymous co-recursion, which is analogous to the [fix] notation we have already seen for recursion. Since we have exposed the [Cons] structure of each stream, we can apply the constructor of [stream_eq]. *)
adamc@63 327
adamc@63 328 constructor.
adamc@63 329 (** [[
adamc@63 330 ones_eq : stream_eq ones ones'
adamc@63 331 ============================
adamc@63 332 stream_eq ones
adamc@63 333 ((cofix map (s : stream nat) : stream nat :=
adamc@63 334 match s with
adamc@63 335 | Cons h t => Cons (S h) (map t)
adamc@63 336 end) zeroes)
adamc@211 337
adamc@211 338 ]]
adamc@63 339
adamc@211 340 Now, modulo unfolding of the definition of [map], we have matched our assumption. *)
adamc@211 341
adamc@63 342 assumption.
adamc@63 343 Qed.
adamc@63 344
adamc@63 345 (** Why did this silly-looking trick help? The answer has to do with the constraints placed on Coq's evaluation rules by the need for termination. The [cofix]-related restriction that foiled our first attempt at using [simpl] is dual to a restriction for [fix]. In particular, an application of an anonymous [fix] only reduces when the top-level structure of the recursive argument is known. Otherwise, we would be unfolding the recursive definition ad infinitum.
adamc@63 346
adamc@63 347 Fixpoints only reduce when enough is known about the %\textit{%#<i>#definitions#</i>#%}% of their arguments. Dually, co-fixpoints only reduce when enough is known about %\textit{%#<i>#how their results will be used#</i>#%}%. In particular, a [cofix] is only expanded when it is the discriminee of a [match]. Rewriting with our superficially silly lemma wrapped new [match]es around the two [cofix]es, triggering reduction.
adamc@63 348
adamc@63 349 If [cofix]es reduced haphazardly, it would be easy to run into infinite loops in evaluation, since we are, after all, building infinite objects.
adamc@63 350
adamc@63 351 One common source of difficulty with co-inductive proofs is bad interaction with standard Coq automation machinery. If we try to prove [ones_eq'] with automation, like we have in previous inductive proofs, we get an invalid proof. *)
adamc@63 352
adamc@63 353 Theorem ones_eq' : stream_eq ones ones'.
adamc@63 354 cofix; crush.
adamc@63 355 (** [[
adamc@205 356 Guarded.
adam@302 357 ]]
adam@302 358 *)
adamc@63 359 Abort.
adam@346 360
adam@346 361 (** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness. One usually starts a proof like this by [destruct]ing some parameter and running a custom tactic to figure out the first proof rule to apply for each case. Alternatively, there are tricks that can be played with %``%#"#hiding#"#%''% the co-inductive hypothesis.
adam@346 362
adam@346 363 %\medskip%
adam@346 364
adam@346 365 Must we always be cautious with automation in proofs by co-induction? Induction seems to have dual versions the same pitfalls inherent in it, and yet we avoid those pitfalls by encapsulating safe Curry-Howard recursion schemes inside named induction principles. It turns out that we can usually do the same with %\index{co-induction principles}\emph{%#<i>#co-induction principles#</i>#%}%. Let us take that tack here, so that we can arrive at an [induction x; crush]-style proof for [ones_eq'].
adam@346 366
adam@346 367 An induction principle is parameterized over a predicate characterizing what we mean to prove, %\emph{%#<i>#as a function of the inductive fact that we already know#</i>#%}%. Dually, a co-induction principle ought to be parameterized over a predicate characterizing what we mean to prove, %\emph{%#<i>#as a function of the arguments to the co-inductive predicate that we are trying to prove#</i>#%}%.
adam@346 368
adam@346 369 To state a useful principle for [stream_eq], it will be useful first to define the stream head function. *)
adam@346 370
adam@346 371 Definition hd A (s : stream A) : A :=
adam@346 372 match s with
adam@346 373 | Cons x _ => x
adam@346 374 end.
adam@346 375
adam@346 376 (** Now we enter a section for the co-induction principle, based on %\index{Park's principle}%Park's principle as introduced in a tutorial by Gim%\'%enez%~\cite{IT}%. *)
adam@346 377
adam@346 378 Section stream_eq_coind.
adam@346 379 Variable A : Set.
adam@346 380 Variable R : stream A -> stream A -> Prop.
adam@346 381 (** This relation generalizes the theorem we want to prove, characterizinge exactly which two arguments to [stream_eq] we want to consider. *)
adam@346 382
adam@346 383 Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2.
adam@346 384 Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2).
adam@346 385 (** Two hypotheses characterize what makes a good choice of [R]: it enforces equality of stream heads, and it is %``%#<i>#hereditary#</i>#%''% in the sense that a [R] stream pair passes on %``%#"#[R]-ness#"#%''% to its tails. An established technical term for such a relation is %\index{bisimulation}\emph{%#<i>#bisimulation#</i>#%}%. *)
adam@346 386
adam@346 387 (** Now it is straightforward to prove the principle, which says that any stream pair in [R] is equal. The reader may wish to step through the proof script to see what is going on. *)
adam@346 388 Theorem stream_eq_coind : forall s1 s2, R s1 s2 -> stream_eq s1 s2.
adam@346 389 cofix; destruct s1; destruct s2; intro.
adam@346 390 generalize (Cons_case_hd H); intro Heq; simpl in Heq; rewrite Heq.
adam@346 391 constructor.
adam@346 392 apply stream_eq_coind.
adam@346 393 apply (Cons_case_tl H).
adam@346 394 Qed.
adam@346 395 End stream_eq_coind.
adam@346 396
adam@346 397 (** To see why this proof is guarded, we can print it and verify that the one co-recursive call is an immediate argument to a constructor. *)
adam@346 398 Print stream_eq_coind.
adam@346 399
adam@346 400 (** We omit the output and proceed to proving [ones_eq''] again. The only bit of ingenuity is in choosing [R], and in this case the most restrictive predicate works. *)
adam@346 401
adam@346 402 Theorem ones_eq'' : stream_eq ones ones'.
adam@346 403 apply (stream_eq_coind (fun s1 s2 => s1 = ones /\ s2 = ones')); crush.
adam@346 404 Qed.
adam@346 405
adam@346 406 (** Note that this proof achieves the proper reduction behavior via [hd] and [tl], rather than [frob] as in the last proof. All three functions pattern match on their arguments, catalyzing computation steps.
adam@346 407
adam@346 408 Compared to the inductive proofs that we are used to, it still seems unsatisfactory that we had to write out a choice of [R] in the last proof. An alternate is to capture a common pattern of co-recursion in a more specialized co-induction principle. For the current example, that pattern is: prove [stream_eq s1 s2] where [s1] and [s2] are defined as their own tails. *)
adam@346 409
adam@346 410 Section stream_eq_loop.
adam@346 411 Variable A : Set.
adam@346 412 Variables s1 s2 : stream A.
adam@346 413
adam@346 414 Hypothesis Cons_case_hd : hd s1 = hd s2.
adam@346 415 Hypothesis loop1 : tl s1 = s1.
adam@346 416 Hypothesis loop2 : tl s2 = s2.
adam@346 417
adam@346 418 (** The proof of the principle includes a choice of [R], so that we no longer need to make such choices thereafter. *)
adam@346 419
adam@346 420 Theorem stream_eq_loop : stream_eq s1 s2.
adam@346 421 apply (stream_eq_coind (fun s1' s2' => s1' = s1 /\ s2' = s2)); crush.
adam@346 422 Qed.
adam@346 423 End stream_eq_loop.
adam@346 424
adam@346 425 Theorem ones_eq''' : stream_eq ones ones'.
adam@346 426 apply stream_eq_loop; crush.
adam@346 427 Qed.
adamc@68 428 (* end thide *)
adamc@63 429
adam@346 430 (** Let us put [stream_eq_ind] through its paces a bit more, considering two different ways to compute infinite streams of all factorial values. First, we import the [fact] factorial function from the standard library. *)
adam@346 431
adam@346 432 Require Import Arith.
adam@346 433 Print fact.
adam@346 434 (** %\vspace{-.15in}%[[
adam@346 435 fact =
adam@346 436 fix fact (n : nat) : nat :=
adam@346 437 match n with
adam@346 438 | 0 => 1
adam@346 439 | S n0 => S n0 * fact n0
adam@346 440 end
adam@346 441 : nat -> nat
adam@346 442 ]]
adam@346 443 *)
adam@346 444
adam@346 445 (** The simplest way to compute the factorial stream involves calling [fact] afresh at each position. *)
adam@346 446
adam@346 447 CoFixpoint fact_slow' (n : nat) := Cons (fact n) (fact_slow' (S n)).
adam@346 448 Definition fact_slow := fact_slow' 1.
adam@346 449
adam@346 450 (** A more clever, optimized method maintains an accumulator of the previous factorial, so that each new entry can be computed with a single multiplication. *)
adam@346 451
adam@346 452 CoFixpoint fact_iter' (cur acc : nat) := Cons acc (fact_iter' (S cur) (acc * cur)).
adam@346 453 Definition fact_iter := fact_iter' 2 1.
adam@346 454
adam@346 455 (** We can verify that the streams are equal up to particular finite bounds. *)
adam@346 456
adam@346 457 Eval simpl in approx fact_iter 5.
adam@346 458 (** %\vspace{-.15in}%[[
adam@346 459 = 1 :: 2 :: 6 :: 24 :: 120 :: nil
adam@346 460 : list nat
adam@346 461 ]]
adam@346 462 *)
adam@346 463 Eval simpl in approx fact_slow 5.
adam@346 464 (** %\vspace{-.15in}%[[
adam@346 465 = 1 :: 2 :: 6 :: 24 :: 120 :: nil
adam@346 466 : list nat
adam@346 467 ]]
adam@346 468
adam@346 469 Now, to prove that the two versions are equivalent, it is helpful to prove (and add as a proof hint) a quick lemma about the computational behavior of [fact]. *)
adam@346 470
adam@346 471 (* begin thide *)
adam@346 472 Lemma fact_def : forall x n,
adam@346 473 fact_iter' x (fact n * S n) = fact_iter' x (fact (S n)).
adam@346 474 simpl; intros; f_equal; ring.
adam@346 475 Qed.
adam@346 476
adam@346 477 Hint Resolve fact_def.
adam@346 478
adam@346 479 (** With the hint added, it is easy to prove an auxiliary lemma relating [fact_iter'] and [fact_slow']. The key bit of ingenuity is introduction of an existential quantifier for the shared parameter [n]. *)
adam@346 480
adam@346 481 Lemma fact_eq' : forall n, stream_eq (fact_iter' (S n) (fact n)) (fact_slow' n).
adam@346 482 intro; apply (stream_eq_coind (fun s1 s2 => exists n, s1 = fact_iter' (S n) (fact n)
adam@346 483 /\ s2 = fact_slow' n)); crush; eauto.
adam@346 484 Qed.
adam@346 485
adam@346 486 (** The final theorem is a direct corollary of [fact_eq']. *)
adam@346 487
adam@346 488 Theorem fact_eq : stream_eq fact_iter fact_slow.
adam@346 489 apply fact_eq'.
adam@346 490 Qed.
adam@346 491
adam@346 492 (** As in the case of [ones_eq'], we may be unsatisfied that we needed to write down a choice of [R] that seems to duplicate information already present in a lemma statement. We can facilitate a simpler proof by defining a co-induction principle specialized to goals that begin with single universal quantifiers, and the strategy can be extended in a straightforward way to principles for other counts of quantifiers. (Our [stream_eq_loop] principle is effectively the instantiation of this technique to zero quantifiers.) *)
adam@346 493
adam@346 494 Section stream_eq_onequant.
adam@346 495 Variables A B : Set.
adam@346 496 (** We have the types [A], the domain of the one quantifier; and [B], the type of data found in the streams. *)
adam@346 497
adam@346 498 Variables f g : A -> stream B.
adam@346 499 (** The two streams we compare must be of the forms [f x] and [g x], for some shared [x]. Note that this falls out naturally when [x] is a shared universally quantified variable in a lemma statement. *)
adam@346 500
adam@346 501 Hypothesis Cons_case_hd : forall x, hd (f x) = hd (g x).
adam@346 502 Hypothesis Cons_case_tl : forall x, exists y, tl (f x) = f y /\ tl (g x) = g y.
adam@346 503 (** These conditions are inspired by the bisimulation requirements, with a more general version of the [R] choice we made for [fact_eq'] inlined into the hypotheses of [stream_eq_coind]. *)
adam@346 504
adam@346 505 Theorem stream_eq_onequant : forall x, stream_eq (f x) (g x).
adam@346 506 intro; apply (stream_eq_coind (fun s1 s2 => exists x, s1 = f x /\ s2 = g x)); crush; eauto.
adam@346 507 Qed.
adam@346 508 End stream_eq_onequant.
adam@346 509
adam@346 510 Lemma fact_eq'' : forall n, stream_eq (fact_iter' (S n) (fact n)) (fact_slow' n).
adam@346 511 apply stream_eq_onequant; crush; eauto.
adam@346 512 Qed.
adam@346 513
adam@346 514 (** We have arrived at one of our customary automated proofs, thanks to the new principle. *)
adam@346 515 (* end thide *)
adamc@64 516
adamc@64 517
adamc@64 518 (** * Simple Modeling of Non-Terminating Programs *)
adamc@64 519
adamc@211 520 (** We close the chapter with a quick motivating example for more complex uses of co-inductive types. We will define a co-inductive semantics for a simple assembly language and use that semantics to prove that assembly programs always run forever. This basic technique can be combined with typing judgments for more advanced languages, where some ill-typed programs can go wrong, but no well-typed programs go wrong.
adamc@64 521
adamc@211 522 We define suggestive synonyms for [nat], for cases where we use natural numbers as registers or program labels. That is, we consider our idealized machine to have infinitely many registers and infinitely many code addresses. *)
adamc@211 523
adamc@211 524 Definition reg := nat.
adamc@64 525 Definition label := nat.
adamc@64 526
adamc@211 527 (** Our instructions are loading of a constant into a register, copying from one register to another, unconditional jump, and conditional jump based on whether the value in a register is not zero. *)
adamc@64 528
adamc@211 529 Inductive instr : Set :=
adamc@211 530 | Imm : reg -> nat -> instr
adamc@211 531 | Copy : reg -> reg -> instr
adamc@211 532 | Jmp : label -> instr
adamc@211 533 | Jnz : reg -> label -> instr.
adamc@67 534
adam@281 535 (** We define a type [regs] of maps from registers to values. To define a function [set] for setting a register's value in a map, we import the [Arith] module from Coq's standard library, and we use its function [beq_nat] for comparing natural numbers. *)
adamc@67 536
adamc@211 537 Definition regs := reg -> nat.
adamc@211 538 Require Import Arith.
adamc@211 539 Definition set (rs : regs) (r : reg) (v : nat) : regs :=
adam@281 540 fun r' => if beq_nat r r' then v else rs r'.
adamc@64 541
adamc@211 542 (** An inductive [exec] judgment captures the effect of an instruction on the program counter and register bank. *)
adamc@64 543
adamc@211 544 Inductive exec : label -> regs -> instr -> label -> regs -> Prop :=
adamc@211 545 | E_Imm : forall pc rs r n, exec pc rs (Imm r n) (S pc) (set rs r n)
adamc@211 546 | E_Copy : forall pc rs r1 r2, exec pc rs (Copy r1 r2) (S pc) (set rs r1 (rs r2))
adamc@211 547 | E_Jmp : forall pc rs pc', exec pc rs (Jmp pc') pc' rs
adamc@211 548 | E_JnzF : forall pc rs r pc', rs r = 0 -> exec pc rs (Jnz r pc') (S pc) rs
adamc@211 549 | E_JnzT : forall pc rs r pc' n, rs r = S n -> exec pc rs (Jnz r pc') pc' rs.
adamc@64 550
adamc@211 551 (** We prove that [exec] represents a total function. In our proof script, we use a [match] tactic with a [context] pattern. This particular example finds an occurrence of a pattern [Jnz ?r _] anywhere in the current subgoal's conclusion. We use a Coq library tactic [case_eq] to do case analysis on whether the current value [rs r] of the register [r] is zero or not. [case_eq] differs from [destruct] in saving an equality relating the old variable to the new form we deduce for it. *)
adamc@64 552
adamc@211 553 Lemma exec_total : forall pc rs i,
adamc@211 554 exists pc', exists rs', exec pc rs i pc' rs'.
adamc@211 555 Hint Constructors exec.
adamc@67 556
adamc@211 557 destruct i; crush; eauto;
adamc@211 558 match goal with
adamc@211 559 | [ |- context[Jnz ?r _] ] => case_eq (rs r)
adamc@211 560 end; eauto.
adamc@64 561 Qed.
adamc@64 562
adam@346 563 (** We are ready to define a co-inductive judgment capturing the idea that a program runs forever. We define the judgment in terms of a program [prog], represented as a function mapping each label to the instruction found there. That is, to simplify the proof, we consider only infinitely long programs. *)
adamc@64 564
adamc@211 565 Section safe.
adamc@211 566 Variable prog : label -> instr.
adamc@64 567
adamc@211 568 CoInductive safe : label -> regs -> Prop :=
adamc@211 569 | Step : forall pc r pc' r',
adamc@211 570 exec pc r (prog pc) pc' r'
adamc@211 571 -> safe pc' r'
adamc@211 572 -> safe pc r.
adamc@64 573
adam@346 574 (** Now we can prove that any starting address and register bank lead to safe infinite execution. Recall that proofs of existentially quantified formulas are all built with a single constructor of the inductive type [ex]. This means that we can use [destruct] to %``%#"#open up#"#%''% such proofs. In the proof below, we want to perform this opening up on an appropriate use of the [exec_total] lemma. This lemma's conclusion begins with two existential quantifiers, so we want to tell [destruct] that it should not stop at the first quantifier. We accomplish our goal by using an %\textit{%#<i>#intro pattern#</i>#%}% with [destruct]. Consult the Coq manual for the details of intro patterns; the specific pattern [[? [? ?]]] that we use here accomplishes our goal of destructing both quantifiers at once. *)
adamc@211 575
adamc@211 576 Theorem always_safe : forall pc rs,
adamc@211 577 safe pc rs.
adamc@211 578 cofix; intros;
adamc@211 579 destruct (exec_total pc rs (prog pc)) as [? [? ?]];
adamc@211 580 econstructor; eauto.
adamc@64 581 Qed.
adamc@211 582 End safe.
adamc@64 583
adamc@67 584 (** If we print the proof term that was generated, we can verify that the proof is structured as a [cofix], with each co-recursive call properly guarded. *)
adamc@67 585
adamc@211 586 Print always_safe.
adamc@81 587
adamc@81 588
adamc@81 589 (** * Exercises *)
adamc@81 590
adamc@81 591 (** %\begin{enumerate}%#<ol>#
adamc@81 592
adamc@81 593 %\item%#<li># %\begin{enumerate}%#<ol>#
adamc@81 594 %\item%#<li># Define a co-inductive type of infinite trees carrying data of a fixed parameter type. Each node should contain a data value and two child trees.#</li>#
adamc@81 595 %\item%#<li># Define a function [everywhere] for building a tree with the same data value at every node.#</li>#
adamc@81 596 %\item%#<li># Define a function [map] for building an output tree out of two input trees by traversing them in parallel and applying a two-argument function to their corresponding data values.#</li>#
adamc@104 597 %\item%#<li># Define a tree [falses] where every node has the value [false].#</li>#
adamc@104 598 %\item%#<li># Define a tree [true_false] where the root node has value [true], its children have value [false], all nodes at the next have the value [true], and so on, alternating boolean values from level to level.#</li>#
adam@292 599 %\item%#<li># Prove that [true_false] is equal to the result of mapping the boolean %``%#"#or#"#%''% function [orb] over [true_false] and [falses]. You can make [orb] available with [Require Import Bool.]. You may find the lemma [orb_false_r] from the same module helpful. Your proof here should not be about the standard equality [=], but rather about some new equality relation that you define.#</li>#
adamc@81 600 #</ol>#%\end{enumerate}% #</li>#
adamc@81 601
adamc@81 602 #</ol>#%\end{enumerate}% *)