Mercurial > cpdt > repo

annotate src/Coinductive.v @ 487:8bfb27cf0121

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add explicit warning that Coq 8.4 or later is required
author Adam Chlipala <adam@chlipala.net>
date Mon, 07 Jan 2013 15:23:16 -0500
parents f02b698aadb1
children ed829eaa91b2
rev   line source
adam@398 1 (* Copyright (c) 2008-2012, 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
adam@422 15 Definition bad : unit := tt.
adam@402 16
adamc@62 17 Set Implicit Arguments.
adamc@62 18 (* end hide *)
adamc@62 19
adamc@62 20
adamc@62 21 (** %\chapter{Infinite Data and Proofs}% *)
adamc@62 22
adam@395 23 (** In lazy functional programming languages like %\index{Haskell}%Haskell, infinite data structures are everywhere%~\cite{whyfp}%. 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 24
adam@346 25 %\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 26
adam@398 27 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 _inconsistent_. For an arbitrary proposition [P], we could write:
adamc@202 28 [[
adamc@202 29 Fixpoint bad (u : unit) : P := bad u.
adamc@205 30 ]]
adamc@205 31
adam@442 32 This would leave us with [bad tt] as a proof of [P].
adamc@62 33
adamc@62 34 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 35
adam@422 36 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; several such approaches are surveyed in Chapter 7. This is a heavyweight solution, and so we would like to avoid it whenever possible.
adamc@62 37
adam@402 38 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}% _co-inductive types_, is the subject of this chapter. *)
adamc@62 39
adamc@62 40
adamc@62 41 (** * Computing with Infinite Data *)
adamc@62 42
adam@398 43 (** Let us begin with the most basic type of infinite data, _streams_, or lazy lists.%\index{Vernacular commands!CoInductive}% *)
adamc@62 44
adamc@62 45 Section stream.
adam@351 46 Variable A : Type.
adamc@62 47
adam@351 48 CoInductive stream : Type :=
adamc@62 49 | Cons : A -> stream -> stream.
adamc@62 50 End stream.
adamc@62 51
adam@422 52 (* begin hide *)
adam@437 53 (* begin thide *)
adam@422 54 CoInductive evilStream := Nil.
adam@437 55 (* end thide *)
adam@422 56 (* end hide *)
adam@422 57
adamc@62 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.
adamc@62 59
adam@471 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.
adamc@62 61
adam@346 62 We can define a stream consisting only of zeroes.%\index{Vernacular commands!CoFixpoint}% *)
adamc@62 63
adamc@62 64 CoFixpoint zeroes : stream nat := Cons 0 zeroes.
adamc@62 65
adam@346 66 (* EX: Define a stream that alternates between [true] and [false]. *)
adam@346 67 (* begin thide *)
adam@346 68
adamc@62 69 (** We can also define a stream that alternates between [true] and [false]. *)
adamc@62 70
adam@346 71 CoFixpoint trues_falses : stream bool := Cons true falses_trues
adam@346 72 with falses_trues : stream bool := Cons false trues_falses.
adam@346 73 (* end thide *)
adamc@62 74
adamc@62 75 (** 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 76
adam@348 77 (* EX: Define a function to calculate a finite approximation of a stream, to a particular length. *)
adam@346 78 (* begin thide *)
adam@346 79
adamc@211 80 Fixpoint approx A (s : stream A) (n : nat) : list A :=
adamc@62 81 match n with
adamc@62 82 | O => nil
adamc@62 83 | S n' =>
adamc@62 84 match s with
adamc@62 85 | Cons h t => h :: approx t n'
adamc@62 86 end
adamc@62 87 end.
adamc@62 88
adamc@62 89 Eval simpl in approx zeroes 10.
adamc@211 90 (** %\vspace{-.15in}% [[
adamc@62 91 = 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: nil
adamc@62 92 : list nat
adam@302 93 ]]
adam@302 94 *)
adamc@211 95
adam@346 96 Eval simpl in approx trues_falses 10.
adamc@211 97 (** %\vspace{-.15in}% [[
adamc@62 98 = true
adamc@62 99 :: false
adamc@62 100 :: true
adamc@62 101 :: false
adamc@62 102 :: true :: false :: true :: false :: true :: false :: nil
adamc@62 103 : list bool
adam@346 104 ]]
adam@346 105 *)
adamc@62 106
adam@349 107 (* end thide *)
adamc@62 108
adam@402 109 (* begin hide *)
adam@437 110 (* begin thide *)
adam@402 111 Definition looper := 0.
adam@437 112 (* end thide *)
adam@402 113 (* end hide *)
adam@402 114
adam@398 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.
adamc@62 116
adam@402 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.
adamc@62 118 [[
adamc@62 119 CoFixpoint looper : stream nat := looper.
adam@346 120 ]]
adamc@205 121
adam@346 122 <<
adamc@62 123 Error:
adamc@62 124 Recursive definition of looper is ill-formed.
adamc@62 125 In environment
adamc@62 126 looper : stream nat
adamc@62 127
adamc@62 128 unguarded recursive call in "looper"
adam@346 129 >>
adamc@205 130
adam@398 131 The rule we have run afoul of here is that _every co-recursive call must be guarded by a constructor_; 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 132
adam@346 133 Some familiar functions are easy to write in co-recursive fashion. *)
adamc@62 134
adamc@62 135 Section map.
adam@351 136 Variables A B : Type.
adamc@62 137 Variable f : A -> B.
adamc@62 138
adamc@62 139 CoFixpoint map (s : stream A) : stream B :=
adamc@62 140 match s with
adamc@62 141 | Cons h t => Cons (f h) (map t)
adamc@62 142 end.
adamc@62 143 End map.
adamc@62 144
adam@402 145 (* begin hide *)
adam@437 146 (* begin thide *)
adam@402 147 Definition filter := 0.
adam@437 148 (* end thide *)
adam@402 149 (* end hide *)
adam@402 150
adam@402 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.
adamc@62 152
adam@398 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. *)
adamc@62 154
adamc@62 155 Section interleave.
adam@351 156 Variable A : Type.
adamc@62 157
adamc@62 158 CoFixpoint interleave (s1 s2 : stream A) : stream A :=
adamc@62 159 match s1, s2 with
adamc@62 160 | Cons h1 t1, Cons h2 t2 => Cons h1 (Cons h2 (interleave t1 t2))
adamc@62 161 end.
adamc@62 162 End interleave.
adamc@62 163
adamc@62 164 (** Now say we want to write a weird stuttering version of [map] that repeats elements in a particular way, based on interleaving. *)
adamc@62 165
adamc@62 166 Section map'.
adam@351 167 Variables A B : Type.
adamc@62 168 Variable f : A -> B.
adamc@68 169 (* begin thide *)
adam@440 170 (** %\vspace{-.15in}%[[
adamc@62 171 CoFixpoint map' (s : stream A) : stream B :=
adamc@62 172 match s with
adam@346 173 | Cons h t => interleave (Cons (f h) (map' t)) (Cons (f h) (map' t))
adamc@68 174 end.
adamc@205 175 ]]
adam@440 176 %\vspace{-.15in}%We get another error message about an unguarded recursive call. *)
adamc@62 177
adam@346 178 End map'.
adam@346 179
adam@475 180 (** 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 by defining a standard function for taking the tail of a stream. Since streams are infinite, this operation is total. *)
adam@346 181
adam@346 182 Definition tl A (s : stream A) : stream A :=
adam@346 183 match s with
adam@346 184 | Cons _ s' => s'
adam@346 185 end.
adam@346 186
adam@346 187 (** Coq rejects the following definition that uses [tl].
adam@346 188 [[
adam@346 189 CoFixpoint bad : stream nat := tl (Cons 0 bad).
adam@346 190 ]]
adam@346 191
adam@422 192 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 193
adam@471 194 Coq's complete rule for co-recursive definitions includes not just the basic guardedness condition, but also a requirement about where co-recursive calls may occur. In particular, a co-recursive call must be a direct argument to a constructor, _nested only inside of other constructor calls or [fun] or [match] expressions_. In the definition of [bad], we erroneously nested the co-recursive call inside a call to [tl], and we nested inside a call to [interleave] in the definition of [map'].
adam@471 195
adam@471 196 Coq helps the user out a little by performing the guardedness check after using computation to simplify terms. For instance, any co-recursive function definition can be expanded by inserting extra calls to an identity function, and this change preserves guardedness. However, in other cases computational simplification can reveal why definitions are dangerous. Consider what happens when we inline the definition of [tl] in [bad]:
adam@346 197 [[
adam@346 198 CoFixpoint bad : stream nat := bad.
adam@346 199 ]]
adam@471 200 This is the same looping definition we rejected earlier. A similar inlining process reveals an alternate view on our failed definition of [map']:
adam@346 201 [[
adam@346 202 CoFixpoint map' (s : stream A) : stream B :=
adam@346 203 match s with
adam@346 204 | Cons h t => Cons (f h) (Cons (f h) (interleave (map' t) (map' t)))
adam@346 205 end.
adam@346 206 ]]
adam@346 207 Clearly in this case the [map'] calls are not immediate arguments to constructors, so we violate the guardedness condition. *)
adamc@68 208 (* end thide *)
adamc@211 209
adam@402 210 (** 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}% _productivity_ 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 211
adamc@63 212
adamc@63 213 (** * Infinite Proofs *)
adamc@63 214
adamc@63 215 (** 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 216
adamc@63 217 CoFixpoint ones : stream nat := Cons 1 ones.
adamc@63 218 Definition ones' := map S zeroes.
adamc@63 219
adamc@63 220 (** The obvious statement of the equality is this: *)
adamc@63 221
adamc@63 222 Theorem ones_eq : ones = ones'.
adamc@63 223
adam@422 224 (* begin hide *)
adam@437 225 (* begin thide *)
adam@422 226 Definition foo := @eq.
adam@437 227 (* end thide *)
adam@422 228 (* end hide *)
adam@422 229
adamc@63 230 (** 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 231 (* begin thide *)
adamc@211 232
adamc@63 233 Abort.
adamc@63 234
adam@398 235 (** Co-inductive datatypes make sense by analogy from Haskell. What we need now is a _co-inductive proposition_. 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 236
adam@346 237 We are ready for our first %\index{co-inductive predicates}%co-inductive predicate. *)
adamc@63 238
adamc@63 239 Section stream_eq.
adam@351 240 Variable A : Type.
adamc@63 241
adamc@63 242 CoInductive stream_eq : stream A -> stream A -> Prop :=
adamc@63 243 | Stream_eq : forall h t1 t2,
adamc@63 244 stream_eq t1 t2
adamc@63 245 -> stream_eq (Cons h t1) (Cons h t2).
adamc@63 246 End stream_eq.
adamc@63 247
adamc@63 248 (** 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 249
adamc@63 250 We can try restating the theorem with [stream_eq]. *)
adamc@63 251
adamc@63 252 Theorem ones_eq : stream_eq ones ones'.
adamc@63 253 (** 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 254
adamc@63 255 cofix.
adamc@63 256 (** [[
adamc@63 257 ones_eq : stream_eq ones ones'
adamc@63 258 ============================
adamc@63 259 stream_eq ones ones'
adamc@211 260
adamc@211 261 ]]
adamc@63 262
adamc@211 263 It looks like this proof might be easier than we expected! *)
adamc@63 264
adamc@63 265 assumption.
adam@422 266 (** <<
adamc@211 267 Proof completed.
adam@422 268 >>
adamc@63 269
adamc@211 270 Unfortunately, we are due for some disappointment in our victory lap.
adamc@211 271 [[
adamc@63 272 Qed.
adam@346 273 ]]
adamc@63 274
adam@346 275 <<
adamc@63 276 Error:
adamc@63 277 Recursive definition of ones_eq is ill-formed.
adamc@63 278
adamc@63 279 In environment
adamc@63 280 ones_eq : stream_eq ones ones'
adamc@63 281
adamc@205 282 unguarded recursive call in "ones_eq"
adam@346 283 >>
adamc@205 284
adamc@211 285 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 286
adam@347 287 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 commands!Guarded}%
adamc@63 288 [[
adamc@63 289 Guarded.
adamc@205 290 ]]
adamc@205 291
adam@398 292 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 _before_ we think we are ready to run [Qed].
adamc@63 293
adam@281 294 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 295
adamc@63 296 Undo.
adamc@63 297 simpl.
adamc@63 298 (** [[
adamc@63 299 ones_eq : stream_eq ones ones'
adamc@63 300 ============================
adamc@63 301 stream_eq ones ones'
adamc@211 302
adamc@211 303 ]]
adamc@63 304
adamc@211 305 It turns out that we are best served by proving an auxiliary lemma. *)
adamc@211 306
adamc@63 307 Abort.
adamc@63 308
adam@450 309 (** First, we need to define a function that seems pointless at first glance. *)
adamc@63 310
adamc@63 311 Definition frob A (s : stream A) : stream A :=
adamc@63 312 match s with
adamc@63 313 | Cons h t => Cons h t
adamc@63 314 end.
adamc@63 315
adamc@63 316 (** Next, we need to prove a theorem that seems equally pointless. *)
adamc@63 317
adamc@63 318 Theorem frob_eq : forall A (s : stream A), s = frob s.
adamc@63 319 destruct s; reflexivity.
adamc@63 320 Qed.
adamc@63 321
adamc@63 322 (** But, miraculously, this theorem turns out to be just what we needed. *)
adamc@63 323
adamc@63 324 Theorem ones_eq : stream_eq ones ones'.
adamc@63 325 cofix.
adamc@63 326
adamc@63 327 (** We can use the theorem to rewrite the two streams. *)
adamc@211 328
adamc@63 329 rewrite (frob_eq ones).
adamc@63 330 rewrite (frob_eq ones').
adamc@63 331 (** [[
adamc@63 332 ones_eq : stream_eq ones ones'
adamc@63 333 ============================
adamc@63 334 stream_eq (frob ones) (frob ones')
adamc@211 335
adamc@211 336 ]]
adamc@63 337
adamc@211 338 Now [simpl] is able to reduce the streams. *)
adamc@63 339
adamc@63 340 simpl.
adamc@63 341 (** [[
adamc@63 342 ones_eq : stream_eq ones ones'
adamc@63 343 ============================
adamc@63 344 stream_eq (Cons 1 ones)
adamc@63 345 (Cons 1
adamc@63 346 ((cofix map (s : stream nat) : stream nat :=
adamc@63 347 match s with
adamc@63 348 | Cons h t => Cons (S h) (map t)
adamc@63 349 end) zeroes))
adamc@211 350
adamc@211 351 ]]
adamc@63 352
adam@422 353 Note the [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 354
adamc@63 355 constructor.
adamc@63 356 (** [[
adamc@63 357 ones_eq : stream_eq ones ones'
adamc@63 358 ============================
adamc@63 359 stream_eq ones
adamc@63 360 ((cofix map (s : stream nat) : stream nat :=
adamc@63 361 match s with
adamc@63 362 | Cons h t => Cons (S h) (map t)
adamc@63 363 end) zeroes)
adamc@211 364
adamc@211 365 ]]
adamc@63 366
adamc@211 367 Now, modulo unfolding of the definition of [map], we have matched our assumption. *)
adamc@211 368
adamc@63 369 assumption.
adamc@63 370 Qed.
adamc@63 371
adamc@63 372 (** 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 373
adam@398 374 Fixpoints only reduce when enough is known about the _definitions_ of their arguments. Dually, co-fixpoints only reduce when enough is known about _how their results will be used_. 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 375
adamc@63 376 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 377
adamc@63 378 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 379
adamc@63 380 Theorem ones_eq' : stream_eq ones ones'.
adamc@63 381 cofix; crush.
adam@440 382 (** %\vspace{-.25in}%[[
adamc@205 383 Guarded.
adam@302 384 ]]
adam@440 385 %\vspace{-.25in}%
adam@302 386 *)
adamc@63 387 Abort.
adam@346 388
adam@471 389 (** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness. A correct proof strategy for a theorem like this usually starts 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 390
adam@346 391 %\medskip%
adam@346 392
adam@402 393 Must we always be cautious with automation in proofs by co-induction? Induction seems to have dual versions of 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}% _co-induction principles_. Let us take that tack here, so that we can arrive at an [induction x; crush]-style proof for [ones_eq'].
adam@346 394
adam@398 395 An induction principle is parameterized over a predicate characterizing what we mean to prove, _as a function of the inductive fact that we already know_. Dually, a co-induction principle ought to be parameterized over a predicate characterizing what we mean to prove, _as a function of the arguments to the co-inductive predicate that we are trying to prove_.
adam@346 396
adam@346 397 To state a useful principle for [stream_eq], it will be useful first to define the stream head function. *)
adam@346 398
adam@346 399 Definition hd A (s : stream A) : A :=
adam@346 400 match s with
adam@346 401 | Cons x _ => x
adam@346 402 end.
adam@346 403
adam@346 404 (** 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 405
adam@346 406 Section stream_eq_coind.
adam@351 407 Variable A : Type.
adam@346 408 Variable R : stream A -> stream A -> Prop.
adam@475 409
adam@471 410 (** This relation generalizes the theorem we want to prove, defining a set of pairs of streams that we must eventually prove contains the particular pair we care about. *)
adam@346 411
adam@346 412 Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2.
adam@346 413 Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2).
adam@475 414
adam@422 415 (** 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 an [R] stream pair passes on "[R]-ness" to its tails. An established technical term for such a relation is%\index{bisimulation}% _bisimulation_. *)
adam@346 416
adam@346 417 (** 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@392 418
adam@346 419 Theorem stream_eq_coind : forall s1 s2, R s1 s2 -> stream_eq s1 s2.
adam@346 420 cofix; destruct s1; destruct s2; intro.
adam@346 421 generalize (Cons_case_hd H); intro Heq; simpl in Heq; rewrite Heq.
adam@346 422 constructor.
adam@346 423 apply stream_eq_coind.
adam@346 424 apply (Cons_case_tl H).
adam@346 425 Qed.
adam@346 426 End stream_eq_coind.
adam@346 427
adam@346 428 (** 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@392 429
adam@346 430 Print stream_eq_coind.
adam@346 431
adam@346 432 (** 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 433
adam@346 434 Theorem ones_eq'' : stream_eq ones ones'.
adam@346 435 apply (stream_eq_coind (fun s1 s2 => s1 = ones /\ s2 = ones')); crush.
adam@346 436 Qed.
adam@346 437
adam@346 438 (** 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 439
adam@346 440 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 441
adam@346 442 Section stream_eq_loop.
adam@351 443 Variable A : Type.
adam@346 444 Variables s1 s2 : stream A.
adam@346 445
adam@346 446 Hypothesis Cons_case_hd : hd s1 = hd s2.
adam@346 447 Hypothesis loop1 : tl s1 = s1.
adam@346 448 Hypothesis loop2 : tl s2 = s2.
adam@346 449
adam@346 450 (** The proof of the principle includes a choice of [R], so that we no longer need to make such choices thereafter. *)
adam@346 451
adam@346 452 Theorem stream_eq_loop : stream_eq s1 s2.
adam@346 453 apply (stream_eq_coind (fun s1' s2' => s1' = s1 /\ s2' = s2)); crush.
adam@346 454 Qed.
adam@346 455 End stream_eq_loop.
adam@346 456
adam@346 457 Theorem ones_eq''' : stream_eq ones ones'.
adam@346 458 apply stream_eq_loop; crush.
adam@346 459 Qed.
adamc@68 460 (* end thide *)
adamc@63 461
adam@435 462 (** Let us put [stream_eq_coind] 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 463
adam@346 464 Require Import Arith.
adam@346 465 Print fact.
adam@346 466 (** %\vspace{-.15in}%[[
adam@346 467 fact =
adam@346 468 fix fact (n : nat) : nat :=
adam@346 469 match n with
adam@346 470 | 0 => 1
adam@346 471 | S n0 => S n0 * fact n0
adam@346 472 end
adam@346 473 : nat -> nat
adam@346 474 ]]
adam@346 475 *)
adam@346 476
adam@346 477 (** The simplest way to compute the factorial stream involves calling [fact] afresh at each position. *)
adam@346 478
adam@346 479 CoFixpoint fact_slow' (n : nat) := Cons (fact n) (fact_slow' (S n)).
adam@346 480 Definition fact_slow := fact_slow' 1.
adam@346 481
adam@346 482 (** 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 483
adam@346 484 CoFixpoint fact_iter' (cur acc : nat) := Cons acc (fact_iter' (S cur) (acc * cur)).
adam@346 485 Definition fact_iter := fact_iter' 2 1.
adam@346 486
adam@346 487 (** We can verify that the streams are equal up to particular finite bounds. *)
adam@346 488
adam@346 489 Eval simpl in approx fact_iter 5.
adam@346 490 (** %\vspace{-.15in}%[[
adam@346 491 = 1 :: 2 :: 6 :: 24 :: 120 :: nil
adam@346 492 : list nat
adam@346 493 ]]
adam@346 494 *)
adam@346 495 Eval simpl in approx fact_slow 5.
adam@346 496 (** %\vspace{-.15in}%[[
adam@346 497 = 1 :: 2 :: 6 :: 24 :: 120 :: nil
adam@346 498 : list nat
adam@346 499 ]]
adam@346 500
adam@471 501 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]. (I intentionally skip explaining its proof at this point.) *)
adam@346 502
adam@346 503 (* begin thide *)
adam@346 504 Lemma fact_def : forall x n,
adam@346 505 fact_iter' x (fact n * S n) = fact_iter' x (fact (S n)).
adam@346 506 simpl; intros; f_equal; ring.
adam@346 507 Qed.
adam@346 508
adam@346 509 Hint Resolve fact_def.
adam@346 510
adam@346 511 (** 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 512
adam@346 513 Lemma fact_eq' : forall n, stream_eq (fact_iter' (S n) (fact n)) (fact_slow' n).
adam@346 514 intro; apply (stream_eq_coind (fun s1 s2 => exists n, s1 = fact_iter' (S n) (fact n)
adam@346 515 /\ s2 = fact_slow' n)); crush; eauto.
adam@346 516 Qed.
adam@346 517
adam@346 518 (** The final theorem is a direct corollary of [fact_eq']. *)
adam@346 519
adam@346 520 Theorem fact_eq : stream_eq fact_iter fact_slow.
adam@346 521 apply fact_eq'.
adam@346 522 Qed.
adam@346 523
adam@346 524 (** 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 525
adam@346 526 Section stream_eq_onequant.
adam@351 527 Variables A B : Type.
adam@346 528 (** We have the types [A], the domain of the one quantifier; and [B], the type of data found in the streams. *)
adam@346 529
adam@346 530 Variables f g : A -> stream B.
adam@346 531 (** 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 532
adam@346 533 Hypothesis Cons_case_hd : forall x, hd (f x) = hd (g x).
adam@346 534 Hypothesis Cons_case_tl : forall x, exists y, tl (f x) = f y /\ tl (g x) = g y.
adam@346 535 (** 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 536
adam@346 537 Theorem stream_eq_onequant : forall x, stream_eq (f x) (g x).
adam@346 538 intro; apply (stream_eq_coind (fun s1 s2 => exists x, s1 = f x /\ s2 = g x)); crush; eauto.
adam@346 539 Qed.
adam@346 540 End stream_eq_onequant.
adam@346 541
adam@346 542 Lemma fact_eq'' : forall n, stream_eq (fact_iter' (S n) (fact n)) (fact_slow' n).
adam@346 543 apply stream_eq_onequant; crush; eauto.
adam@346 544 Qed.
adam@346 545
adam@346 546 (** We have arrived at one of our customary automated proofs, thanks to the new principle. *)
adam@346 547 (* end thide *)
adamc@64 548
adamc@64 549
adamc@64 550 (** * Simple Modeling of Non-Terminating Programs *)
adamc@64 551
adam@402 552 (** 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 imperative programming language and use that semantics to prove the correctness of a trivial optimization that removes spurious additions by 0. We follow the technique of%\index{co-inductive big-step operational semantics}% _co-inductive big-step operational semantics_ %\cite{BigStep}%.
adamc@64 553
adam@471 554 We define a suggestive synonym for [nat], as we will consider programs over infinitely many variables, represented as [nat]s. *)
adamc@211 555
adam@347 556 Definition var := nat.
adamc@64 557
adam@436 558 (** We define a type [vars] of maps from variables to values. To define a function [set] for setting a variable's value in a map, we use the standard library function [beq_nat] for comparing natural numbers. *)
adamc@64 559
adam@347 560 Definition vars := var -> nat.
adam@347 561 Definition set (vs : vars) (v : var) (n : nat) : vars :=
adam@347 562 fun v' => if beq_nat v v' then n else vs v'.
adamc@67 563
adam@347 564 (** We define a simple arithmetic expression language with variables, and we give it a semantics via an interpreter. *)
adamc@67 565
adam@347 566 Inductive exp : Set :=
adam@347 567 | Const : nat -> exp
adam@347 568 | Var : var -> exp
adam@347 569 | Plus : exp -> exp -> exp.
adamc@64 570
adam@347 571 Fixpoint evalExp (vs : vars) (e : exp) : nat :=
adam@347 572 match e with
adam@347 573 | Const n => n
adam@347 574 | Var v => vs v
adam@347 575 | Plus e1 e2 => evalExp vs e1 + evalExp vs e2
adam@347 576 end.
adamc@64 577
adam@422 578 (** Finally, we define a language of commands. It includes variable assignment, sequencing, and a <<while>> form that repeats as long as its test expression evaluates to a nonzero value. *)
adamc@64 579
adam@347 580 Inductive cmd : Set :=
adam@347 581 | Assign : var -> exp -> cmd
adam@347 582 | Seq : cmd -> cmd -> cmd
adam@347 583 | While : exp -> cmd -> cmd.
adamc@64 584
adam@471 585 (** We could define an inductive relation to characterize the results of command evaluation. However, such a relation would not capture _nonterminating_ executions. With a co-inductive relation, we can capture both cases. The parameters of the relation are an initial state, a command, and a final state. A program that does not terminate in a particular initial state is related to _any_ final state. For more realistic languages than this one, it is often possible for programs to _crash_, in which case a semantics would generally relate their executions to no final states; so relating safely non-terminating programs to all final states provides a crucial distinction. *)
adamc@67 586
adam@347 587 CoInductive evalCmd : vars -> cmd -> vars -> Prop :=
adam@347 588 | EvalAssign : forall vs v e, evalCmd vs (Assign v e) (set vs v (evalExp vs e))
adam@347 589 | EvalSeq : forall vs1 vs2 vs3 c1 c2, evalCmd vs1 c1 vs2
adam@347 590 -> evalCmd vs2 c2 vs3
adam@347 591 -> evalCmd vs1 (Seq c1 c2) vs3
adam@347 592 | EvalWhileFalse : forall vs e c, evalExp vs e = 0
adam@347 593 -> evalCmd vs (While e c) vs
adam@347 594 | EvalWhileTrue : forall vs1 vs2 vs3 e c, evalExp vs1 e <> 0
adam@347 595 -> evalCmd vs1 c vs2
adam@347 596 -> evalCmd vs2 (While e c) vs3
adam@347 597 -> evalCmd vs1 (While e c) vs3.
adam@347 598
adam@347 599 (** Having learned our lesson in the last section, before proceeding, we build a co-induction principle for [evalCmd]. *)
adam@347 600
adam@347 601 Section evalCmd_coind.
adam@347 602 Variable R : vars -> cmd -> vars -> Prop.
adam@347 603
adam@347 604 Hypothesis AssignCase : forall vs1 vs2 v e, R vs1 (Assign v e) vs2
adam@347 605 -> vs2 = set vs1 v (evalExp vs1 e).
adam@347 606
adam@347 607 Hypothesis SeqCase : forall vs1 vs3 c1 c2, R vs1 (Seq c1 c2) vs3
adam@347 608 -> exists vs2, R vs1 c1 vs2 /\ R vs2 c2 vs3.
adam@347 609
adam@347 610 Hypothesis WhileCase : forall vs1 vs3 e c, R vs1 (While e c) vs3
adam@347 611 -> (evalExp vs1 e = 0 /\ vs3 = vs1)
adam@347 612 \/ exists vs2, evalExp vs1 e <> 0 /\ R vs1 c vs2 /\ R vs2 (While e c) vs3.
adam@347 613
adam@402 614 (** The proof is routine. We make use of a form of %\index{tactics!destruct}%[destruct] that takes an%\index{intro pattern}% _intro pattern_ in an [as] clause. These patterns control how deeply we break apart the components of an inductive value, and we refer the reader to the Coq manual for more details. *)
adam@347 615
adam@347 616 Theorem evalCmd_coind : forall vs1 c vs2, R vs1 c vs2 -> evalCmd vs1 c vs2.
adam@347 617 cofix; intros; destruct c.
adam@347 618 rewrite (AssignCase H); constructor.
adam@347 619 destruct (SeqCase H) as [? [? ?]]; econstructor; eauto.
adam@478 620 destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; econstructor; eauto.
adam@347 621 Qed.
adam@347 622 End evalCmd_coind.
adam@347 623
adam@347 624 (** Now that we have a co-induction principle, we should use it to prove something! Our example is a trivial program optimizer that finds places to replace [0 + e] with [e]. *)
adam@347 625
adam@347 626 Fixpoint optExp (e : exp) : exp :=
adam@347 627 match e with
adam@347 628 | Plus (Const 0) e => optExp e
adam@347 629 | Plus e1 e2 => Plus (optExp e1) (optExp e2)
adam@347 630 | _ => e
adam@347 631 end.
adam@347 632
adam@347 633 Fixpoint optCmd (c : cmd) : cmd :=
adam@347 634 match c with
adam@347 635 | Assign v e => Assign v (optExp e)
adam@347 636 | Seq c1 c2 => Seq (optCmd c1) (optCmd c2)
adam@347 637 | While e c => While (optExp e) (optCmd c)
adam@347 638 end.
adam@347 639
adam@347 640 (** Before proving correctness of [optCmd], we prove a lemma about [optExp]. This is where we have to do the most work, choosing pattern match opportunities automatically. *)
adam@347 641
adam@347 642 (* begin thide *)
adam@347 643 Lemma optExp_correct : forall vs e, evalExp vs (optExp e) = evalExp vs e.
adam@347 644 induction e; crush;
adam@347 645 repeat (match goal with
adam@478 646 | [ |- context[match ?E with Const _ => _ | _ => _ end] ] => destruct E
adam@347 647 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
adam@347 648 end; crush).
adamc@64 649 Qed.
adamc@64 650
adam@478 651 Hint Rewrite optExp_correct.
adamc@64 652
adam@384 653 (** The final theorem is easy to establish, using our co-induction principle and a bit of Ltac smarts that we leave unexplained for now. Curious readers can consult the Coq manual, or wait for the later chapters of this book about proof automation. At a high level, we show inclusions between behaviors, going in both directions between original and optimized programs. *)
adamc@64 654
adam@384 655 Ltac finisher := match goal with
adam@384 656 | [ H : evalCmd _ _ _ |- _ ] => ((inversion H; [])
adam@384 657 || (inversion H; [|])); subst
adam@384 658 end; crush; eauto 10.
adam@384 659
adam@384 660 Lemma optCmd_correct1 : forall vs1 c vs2, evalCmd vs1 c vs2
adam@347 661 -> evalCmd vs1 (optCmd c) vs2.
adam@347 662 intros; apply (evalCmd_coind (fun vs1 c' vs2 => exists c, evalCmd vs1 c vs2
adam@347 663 /\ c' = optCmd c)); eauto; crush;
adam@347 664 match goal with
adam@347 665 | [ H : _ = optCmd ?E |- _ ] => destruct E; simpl in *; discriminate
adam@347 666 || injection H; intros; subst
adam@384 667 end; finisher.
adam@384 668 Qed.
adam@384 669
adam@384 670 Lemma optCmd_correct2 : forall vs1 c vs2, evalCmd vs1 (optCmd c) vs2
adam@384 671 -> evalCmd vs1 c vs2.
adam@384 672 intros; apply (evalCmd_coind (fun vs1 c vs2 => evalCmd vs1 (optCmd c) vs2));
adam@384 673 crush; finisher.
adam@384 674 Qed.
adam@384 675
adam@384 676 Theorem optCmd_correct : forall vs1 c vs2, evalCmd vs1 (optCmd c) vs2
adam@384 677 <-> evalCmd vs1 c vs2.
adam@384 678 intuition; apply optCmd_correct1 || apply optCmd_correct2; assumption.
adam@347 679 Qed.
adam@347 680 (* end thide *)
adamc@64 681
adam@422 682 (** In this form, the theorem tells us that the optimizer preserves observable behavior of both terminating and nonterminating programs, but we did not have to do more work than for the case of terminating programs alone. We merely took the natural inductive definition for terminating executions, made it co-inductive, and applied the appropriate co-induction principle. Curious readers might experiment with adding command constructs like <<if>>; the same proof script should continue working, after the co-induction principle is extended to the new evaluation rules. *)