Mercurial > cpdt > repo

annotate src/Coinductive.v @ 435:a54a4a2ea6e4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Changes while hacking on coqdoc
author Adam Chlipala <adam@chlipala.net>
date Thu, 26 Jul 2012 19:05:12 -0400
parents a730378789f5
children 5d5e44f905c7
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
adamc@202 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@422 53 CoInductive evilStream := Nil.
adam@422 54 (* end hide *)
adam@422 55
adamc@62 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.
adamc@62 57
adam@402 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.
adamc@62 59
adam@346 60 We can define a stream consisting only of zeroes.%\index{Vernacular commands!CoFixpoint}% *)
adamc@62 61
adamc@62 62 CoFixpoint zeroes : stream nat := Cons 0 zeroes.
adamc@62 63
adam@346 64 (* EX: Define a stream that alternates between [true] and [false]. *)
adam@346 65 (* begin thide *)
adam@346 66
adamc@62 67 (** We can also define a stream that alternates between [true] and [false]. *)
adamc@62 68
adam@346 69 CoFixpoint trues_falses : stream bool := Cons true falses_trues
adam@346 70 with falses_trues : stream bool := Cons false trues_falses.
adam@346 71 (* end thide *)
adamc@62 72
adamc@62 73 (** 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 74
adam@348 75 (* EX: Define a function to calculate a finite approximation of a stream, to a particular length. *)
adam@346 76 (* begin thide *)
adam@346 77
adamc@211 78 Fixpoint approx A (s : stream A) (n : nat) : list A :=
adamc@62 79 match n with
adamc@62 80 | O => nil
adamc@62 81 | S n' =>
adamc@62 82 match s with
adamc@62 83 | Cons h t => h :: approx t n'
adamc@62 84 end
adamc@62 85 end.
adamc@62 86
adamc@62 87 Eval simpl in approx zeroes 10.
adamc@211 88 (** %\vspace{-.15in}% [[
adamc@62 89 = 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: nil
adamc@62 90 : list nat
adam@302 91 ]]
adam@302 92 *)
adamc@211 93
adam@346 94 Eval simpl in approx trues_falses 10.
adamc@211 95 (** %\vspace{-.15in}% [[
adamc@62 96 = true
adamc@62 97 :: false
adamc@62 98 :: true
adamc@62 99 :: false
adamc@62 100 :: true :: false :: true :: false :: true :: false :: nil
adamc@62 101 : list bool
adam@346 102 ]]
adam@346 103 *)
adamc@62 104
adam@349 105 (* end thide *)
adamc@62 106
adam@402 107 (* begin hide *)
adam@402 108 Definition looper := 0.
adam@402 109 (* end hide *)
adam@402 110
adam@398 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.
adamc@62 112
adam@402 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.
adamc@62 114 [[
adamc@62 115 CoFixpoint looper : stream nat := looper.
adam@346 116 ]]
adamc@205 117
adam@346 118 <<
adamc@62 119 Error:
adamc@62 120 Recursive definition of looper is ill-formed.
adamc@62 121 In environment
adamc@62 122 looper : stream nat
adamc@62 123
adamc@62 124 unguarded recursive call in "looper"
adam@346 125 >>
adamc@205 126
adam@398 127 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 128
adam@346 129 Some familiar functions are easy to write in co-recursive fashion. *)
adamc@62 130
adamc@62 131 Section map.
adam@351 132 Variables A B : Type.
adamc@62 133 Variable f : A -> B.
adamc@62 134
adamc@62 135 CoFixpoint map (s : stream A) : stream B :=
adamc@62 136 match s with
adamc@62 137 | Cons h t => Cons (f h) (map t)
adamc@62 138 end.
adamc@62 139 End map.
adamc@62 140
adam@402 141 (* begin hide *)
adam@402 142 Definition filter := 0.
adam@402 143 (* end hide *)
adam@402 144
adam@402 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.
adamc@62 146
adam@398 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. *)
adamc@62 148
adamc@62 149 Section interleave.
adam@351 150 Variable A : Type.
adamc@62 151
adamc@62 152 CoFixpoint interleave (s1 s2 : stream A) : stream A :=
adamc@62 153 match s1, s2 with
adamc@62 154 | Cons h1 t1, Cons h2 t2 => Cons h1 (Cons h2 (interleave t1 t2))
adamc@62 155 end.
adamc@62 156 End interleave.
adamc@62 157
adamc@62 158 (** Now say we want to write a weird stuttering version of [map] that repeats elements in a particular way, based on interleaving. *)
adamc@62 159
adamc@62 160 Section map'.
adam@351 161 Variables A B : Type.
adamc@62 162 Variable f : A -> B.
adamc@68 163 (* begin thide *)
adamc@62 164 (** [[
adamc@62 165 CoFixpoint map' (s : stream A) : stream B :=
adamc@62 166 match s with
adam@346 167 | Cons h t => interleave (Cons (f h) (map' t)) (Cons (f h) (map' t))
adamc@68 168 end.
adamc@205 169 ]]
adamc@211 170
adam@346 171 We get another error message about an unguarded recursive call. *)
adamc@62 172
adam@346 173 End map'.
adam@346 174
adam@346 175 (** 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 176
adam@346 177 Definition tl A (s : stream A) : stream A :=
adam@346 178 match s with
adam@346 179 | Cons _ s' => s'
adam@346 180 end.
adam@346 181
adam@346 182 (** Coq rejects the following definition that uses [tl].
adam@346 183 [[
adam@346 184 CoFixpoint bad : stream nat := tl (Cons 0 bad).
adam@346 185 ]]
adam@346 186
adam@422 187 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 188
adam@346 189 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 190 [[
adam@346 191 CoFixpoint bad : stream nat := bad.
adam@346 192 ]]
adam@346 193 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 194 [[
adam@346 195 CoFixpoint map' (s : stream A) : stream B :=
adam@346 196 match s with
adam@346 197 | Cons h t => Cons (f h) (Cons (f h) (interleave (map' t) (map' t)))
adam@346 198 end.
adam@346 199 ]]
adam@346 200 Clearly in this case the [map'] calls are not immediate arguments to constructors, so we violate the guardedness condition. *)
adamc@68 201 (* end thide *)
adamc@211 202
adam@402 203 (** 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 204
adamc@63 205
adamc@63 206 (** * Infinite Proofs *)
adamc@63 207
adamc@63 208 (** 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 209
adamc@63 210 CoFixpoint ones : stream nat := Cons 1 ones.
adamc@63 211 Definition ones' := map S zeroes.
adamc@63 212
adamc@63 213 (** The obvious statement of the equality is this: *)
adamc@63 214
adamc@63 215 Theorem ones_eq : ones = ones'.
adamc@63 216
adam@422 217 (* begin hide *)
adam@422 218 Definition foo := @eq.
adam@422 219 (* end hide *)
adam@422 220
adamc@63 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. *)
adamc@68 222 (* begin thide *)
adamc@211 223
adamc@63 224 Abort.
adamc@63 225
adam@398 226 (** 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 227
adam@346 228 We are ready for our first %\index{co-inductive predicates}%co-inductive predicate. *)
adamc@63 229
adamc@63 230 Section stream_eq.
adam@351 231 Variable A : Type.
adamc@63 232
adamc@63 233 CoInductive stream_eq : stream A -> stream A -> Prop :=
adamc@63 234 | Stream_eq : forall h t1 t2,
adamc@63 235 stream_eq t1 t2
adamc@63 236 -> stream_eq (Cons h t1) (Cons h t2).
adamc@63 237 End stream_eq.
adamc@63 238
adamc@63 239 (** 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 240
adamc@63 241 We can try restating the theorem with [stream_eq]. *)
adamc@63 242
adamc@63 243 Theorem ones_eq : stream_eq ones ones'.
adamc@63 244 (** 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 245
adamc@63 246 cofix.
adamc@63 247 (** [[
adamc@63 248 ones_eq : stream_eq ones ones'
adamc@63 249 ============================
adamc@63 250 stream_eq ones ones'
adamc@211 251
adamc@211 252 ]]
adamc@63 253
adamc@211 254 It looks like this proof might be easier than we expected! *)
adamc@63 255
adamc@63 256 assumption.
adam@422 257 (** <<
adamc@211 258 Proof completed.
adam@422 259 >>
adamc@63 260
adamc@211 261 Unfortunately, we are due for some disappointment in our victory lap.
adamc@211 262 [[
adamc@63 263 Qed.
adam@346 264 ]]
adamc@63 265
adam@346 266 <<
adamc@63 267 Error:
adamc@63 268 Recursive definition of ones_eq is ill-formed.
adamc@63 269
adamc@63 270 In environment
adamc@63 271 ones_eq : stream_eq ones ones'
adamc@63 272
adamc@205 273 unguarded recursive call in "ones_eq"
adam@346 274 >>
adamc@205 275
adamc@211 276 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 277
adam@347 278 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 279 [[
adamc@63 280 Guarded.
adamc@205 281 ]]
adamc@205 282
adam@398 283 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 284
adam@281 285 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 286
adamc@63 287 Undo.
adamc@63 288 simpl.
adamc@63 289 (** [[
adamc@63 290 ones_eq : stream_eq ones ones'
adamc@63 291 ============================
adamc@63 292 stream_eq ones ones'
adamc@211 293
adamc@211 294 ]]
adamc@63 295
adamc@211 296 It turns out that we are best served by proving an auxiliary lemma. *)
adamc@211 297
adamc@63 298 Abort.
adamc@63 299
adamc@63 300 (** First, we need to define a function that seems pointless on first glance. *)
adamc@63 301
adamc@63 302 Definition frob A (s : stream A) : stream A :=
adamc@63 303 match s with
adamc@63 304 | Cons h t => Cons h t
adamc@63 305 end.
adamc@63 306
adamc@63 307 (** Next, we need to prove a theorem that seems equally pointless. *)
adamc@63 308
adamc@63 309 Theorem frob_eq : forall A (s : stream A), s = frob s.
adamc@63 310 destruct s; reflexivity.
adamc@63 311 Qed.
adamc@63 312
adamc@63 313 (** But, miraculously, this theorem turns out to be just what we needed. *)
adamc@63 314
adamc@63 315 Theorem ones_eq : stream_eq ones ones'.
adamc@63 316 cofix.
adamc@63 317
adamc@63 318 (** We can use the theorem to rewrite the two streams. *)
adamc@211 319
adamc@63 320 rewrite (frob_eq ones).
adamc@63 321 rewrite (frob_eq ones').
adamc@63 322 (** [[
adamc@63 323 ones_eq : stream_eq ones ones'
adamc@63 324 ============================
adamc@63 325 stream_eq (frob ones) (frob ones')
adamc@211 326
adamc@211 327 ]]
adamc@63 328
adamc@211 329 Now [simpl] is able to reduce the streams. *)
adamc@63 330
adamc@63 331 simpl.
adamc@63 332 (** [[
adamc@63 333 ones_eq : stream_eq ones ones'
adamc@63 334 ============================
adamc@63 335 stream_eq (Cons 1 ones)
adamc@63 336 (Cons 1
adamc@63 337 ((cofix map (s : stream nat) : stream nat :=
adamc@63 338 match s with
adamc@63 339 | Cons h t => Cons (S h) (map t)
adamc@63 340 end) zeroes))
adamc@211 341
adamc@211 342 ]]
adamc@63 343
adam@422 344 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 345
adamc@63 346 constructor.
adamc@63 347 (** [[
adamc@63 348 ones_eq : stream_eq ones ones'
adamc@63 349 ============================
adamc@63 350 stream_eq ones
adamc@63 351 ((cofix map (s : stream nat) : stream nat :=
adamc@63 352 match s with
adamc@63 353 | Cons h t => Cons (S h) (map t)
adamc@63 354 end) zeroes)
adamc@211 355
adamc@211 356 ]]
adamc@63 357
adamc@211 358 Now, modulo unfolding of the definition of [map], we have matched our assumption. *)
adamc@211 359
adamc@63 360 assumption.
adamc@63 361 Qed.
adamc@63 362
adamc@63 363 (** 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 364
adam@398 365 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 366
adamc@63 367 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 368
adamc@63 369 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 370
adamc@63 371 Theorem ones_eq' : stream_eq ones ones'.
adamc@63 372 cofix; crush.
adamc@63 373 (** [[
adamc@205 374 Guarded.
adam@302 375 ]]
adam@302 376 *)
adamc@63 377 Abort.
adam@346 378
adam@422 379 (** 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 380
adam@346 381 %\medskip%
adam@346 382
adam@402 383 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 384
adam@398 385 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 386
adam@346 387 To state a useful principle for [stream_eq], it will be useful first to define the stream head function. *)
adam@346 388
adam@346 389 Definition hd A (s : stream A) : A :=
adam@346 390 match s with
adam@346 391 | Cons x _ => x
adam@346 392 end.
adam@346 393
adam@346 394 (** 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 395
adam@346 396 Section stream_eq_coind.
adam@351 397 Variable A : Type.
adam@346 398 Variable R : stream A -> stream A -> Prop.
adam@392 399 (** This relation generalizes the theorem we want to prove, characterizing exactly which two arguments to [stream_eq] we want to consider. *)
adam@346 400
adam@346 401 Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2.
adam@346 402 Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2).
adam@422 403 (** 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 404
adam@346 405 (** 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 406
adam@346 407 Theorem stream_eq_coind : forall s1 s2, R s1 s2 -> stream_eq s1 s2.
adam@346 408 cofix; destruct s1; destruct s2; intro.
adam@346 409 generalize (Cons_case_hd H); intro Heq; simpl in Heq; rewrite Heq.
adam@346 410 constructor.
adam@346 411 apply stream_eq_coind.
adam@346 412 apply (Cons_case_tl H).
adam@346 413 Qed.
adam@346 414 End stream_eq_coind.
adam@346 415
adam@346 416 (** 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 417
adam@346 418 Print stream_eq_coind.
adam@346 419
adam@346 420 (** 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 421
adam@346 422 Theorem ones_eq'' : stream_eq ones ones'.
adam@346 423 apply (stream_eq_coind (fun s1 s2 => s1 = ones /\ s2 = ones')); crush.
adam@346 424 Qed.
adam@346 425
adam@346 426 (** 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 427
adam@346 428 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 429
adam@346 430 Section stream_eq_loop.
adam@351 431 Variable A : Type.
adam@346 432 Variables s1 s2 : stream A.
adam@346 433
adam@346 434 Hypothesis Cons_case_hd : hd s1 = hd s2.
adam@346 435 Hypothesis loop1 : tl s1 = s1.
adam@346 436 Hypothesis loop2 : tl s2 = s2.
adam@346 437
adam@346 438 (** The proof of the principle includes a choice of [R], so that we no longer need to make such choices thereafter. *)
adam@346 439
adam@346 440 Theorem stream_eq_loop : stream_eq s1 s2.
adam@346 441 apply (stream_eq_coind (fun s1' s2' => s1' = s1 /\ s2' = s2)); crush.
adam@346 442 Qed.
adam@346 443 End stream_eq_loop.
adam@346 444
adam@346 445 Theorem ones_eq''' : stream_eq ones ones'.
adam@346 446 apply stream_eq_loop; crush.
adam@346 447 Qed.
adamc@68 448 (* end thide *)
adamc@63 449
adam@435 450 (** 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 451
adam@346 452 Require Import Arith.
adam@346 453 Print fact.
adam@346 454 (** %\vspace{-.15in}%[[
adam@346 455 fact =
adam@346 456 fix fact (n : nat) : nat :=
adam@346 457 match n with
adam@346 458 | 0 => 1
adam@346 459 | S n0 => S n0 * fact n0
adam@346 460 end
adam@346 461 : nat -> nat
adam@346 462 ]]
adam@346 463 *)
adam@346 464
adam@346 465 (** The simplest way to compute the factorial stream involves calling [fact] afresh at each position. *)
adam@346 466
adam@346 467 CoFixpoint fact_slow' (n : nat) := Cons (fact n) (fact_slow' (S n)).
adam@346 468 Definition fact_slow := fact_slow' 1.
adam@346 469
adam@346 470 (** 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 471
adam@346 472 CoFixpoint fact_iter' (cur acc : nat) := Cons acc (fact_iter' (S cur) (acc * cur)).
adam@346 473 Definition fact_iter := fact_iter' 2 1.
adam@346 474
adam@346 475 (** We can verify that the streams are equal up to particular finite bounds. *)
adam@346 476
adam@346 477 Eval simpl in approx fact_iter 5.
adam@346 478 (** %\vspace{-.15in}%[[
adam@346 479 = 1 :: 2 :: 6 :: 24 :: 120 :: nil
adam@346 480 : list nat
adam@346 481 ]]
adam@346 482 *)
adam@346 483 Eval simpl in approx fact_slow 5.
adam@346 484 (** %\vspace{-.15in}%[[
adam@346 485 = 1 :: 2 :: 6 :: 24 :: 120 :: nil
adam@346 486 : list nat
adam@346 487 ]]
adam@346 488
adam@346 489 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 490
adam@346 491 (* begin thide *)
adam@346 492 Lemma fact_def : forall x n,
adam@346 493 fact_iter' x (fact n * S n) = fact_iter' x (fact (S n)).
adam@346 494 simpl; intros; f_equal; ring.
adam@346 495 Qed.
adam@346 496
adam@346 497 Hint Resolve fact_def.
adam@346 498
adam@346 499 (** 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 500
adam@346 501 Lemma fact_eq' : forall n, stream_eq (fact_iter' (S n) (fact n)) (fact_slow' n).
adam@346 502 intro; apply (stream_eq_coind (fun s1 s2 => exists n, s1 = fact_iter' (S n) (fact n)
adam@346 503 /\ s2 = fact_slow' n)); crush; eauto.
adam@346 504 Qed.
adam@346 505
adam@346 506 (** The final theorem is a direct corollary of [fact_eq']. *)
adam@346 507
adam@346 508 Theorem fact_eq : stream_eq fact_iter fact_slow.
adam@346 509 apply fact_eq'.
adam@346 510 Qed.
adam@346 511
adam@346 512 (** 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 513
adam@346 514 Section stream_eq_onequant.
adam@351 515 Variables A B : Type.
adam@346 516 (** We have the types [A], the domain of the one quantifier; and [B], the type of data found in the streams. *)
adam@346 517
adam@346 518 Variables f g : A -> stream B.
adam@346 519 (** 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 520
adam@346 521 Hypothesis Cons_case_hd : forall x, hd (f x) = hd (g x).
adam@346 522 Hypothesis Cons_case_tl : forall x, exists y, tl (f x) = f y /\ tl (g x) = g y.
adam@346 523 (** 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 524
adam@346 525 Theorem stream_eq_onequant : forall x, stream_eq (f x) (g x).
adam@346 526 intro; apply (stream_eq_coind (fun s1 s2 => exists x, s1 = f x /\ s2 = g x)); crush; eauto.
adam@346 527 Qed.
adam@346 528 End stream_eq_onequant.
adam@346 529
adam@346 530 Lemma fact_eq'' : forall n, stream_eq (fact_iter' (S n) (fact n)) (fact_slow' n).
adam@346 531 apply stream_eq_onequant; crush; eauto.
adam@346 532 Qed.
adam@346 533
adam@346 534 (** We have arrived at one of our customary automated proofs, thanks to the new principle. *)
adam@346 535 (* end thide *)
adamc@64 536
adamc@64 537
adamc@64 538 (** * Simple Modeling of Non-Terminating Programs *)
adamc@64 539
adam@402 540 (** 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 541
adam@347 542 We define a suggestive synonym for [nat], as we will consider programs with infinitely many variables, represented as [nat]s. *)
adamc@211 543
adam@347 544 Definition var := nat.
adamc@64 545
adam@347 546 (** 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 import the [Arith] module from Coq's standard library, and we use its function [beq_nat] for comparing natural numbers. *)
adamc@64 547
adam@347 548 Definition vars := var -> nat.
adam@347 549 Require Import Arith.
adam@347 550 Definition set (vs : vars) (v : var) (n : nat) : vars :=
adam@347 551 fun v' => if beq_nat v v' then n else vs v'.
adamc@67 552
adam@347 553 (** We define a simple arithmetic expression language with variables, and we give it a semantics via an interpreter. *)
adamc@67 554
adam@347 555 Inductive exp : Set :=
adam@347 556 | Const : nat -> exp
adam@347 557 | Var : var -> exp
adam@347 558 | Plus : exp -> exp -> exp.
adamc@64 559
adam@347 560 Fixpoint evalExp (vs : vars) (e : exp) : nat :=
adam@347 561 match e with
adam@347 562 | Const n => n
adam@347 563 | Var v => vs v
adam@347 564 | Plus e1 e2 => evalExp vs e1 + evalExp vs e2
adam@347 565 end.
adamc@64 566
adam@422 567 (** 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 568
adam@347 569 Inductive cmd : Set :=
adam@347 570 | Assign : var -> exp -> cmd
adam@347 571 | Seq : cmd -> cmd -> cmd
adam@347 572 | While : exp -> cmd -> cmd.
adamc@64 573
adam@398 574 (** 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. *)
adamc@67 575
adam@347 576 CoInductive evalCmd : vars -> cmd -> vars -> Prop :=
adam@347 577 | EvalAssign : forall vs v e, evalCmd vs (Assign v e) (set vs v (evalExp vs e))
adam@347 578 | EvalSeq : forall vs1 vs2 vs3 c1 c2, evalCmd vs1 c1 vs2
adam@347 579 -> evalCmd vs2 c2 vs3
adam@347 580 -> evalCmd vs1 (Seq c1 c2) vs3
adam@347 581 | EvalWhileFalse : forall vs e c, evalExp vs e = 0
adam@347 582 -> evalCmd vs (While e c) vs
adam@347 583 | EvalWhileTrue : forall vs1 vs2 vs3 e c, evalExp vs1 e <> 0
adam@347 584 -> evalCmd vs1 c vs2
adam@347 585 -> evalCmd vs2 (While e c) vs3
adam@347 586 -> evalCmd vs1 (While e c) vs3.
adam@347 587
adam@347 588 (** Having learned our lesson in the last section, before proceeding, we build a co-induction principle for [evalCmd]. *)
adam@347 589
adam@347 590 Section evalCmd_coind.
adam@347 591 Variable R : vars -> cmd -> vars -> Prop.
adam@347 592
adam@347 593 Hypothesis AssignCase : forall vs1 vs2 v e, R vs1 (Assign v e) vs2
adam@347 594 -> vs2 = set vs1 v (evalExp vs1 e).
adam@347 595
adam@347 596 Hypothesis SeqCase : forall vs1 vs3 c1 c2, R vs1 (Seq c1 c2) vs3
adam@347 597 -> exists vs2, R vs1 c1 vs2 /\ R vs2 c2 vs3.
adam@347 598
adam@347 599 Hypothesis WhileCase : forall vs1 vs3 e c, R vs1 (While e c) vs3
adam@347 600 -> (evalExp vs1 e = 0 /\ vs3 = vs1)
adam@347 601 \/ exists vs2, evalExp vs1 e <> 0 /\ R vs1 c vs2 /\ R vs2 (While e c) vs3.
adam@347 602
adam@402 603 (** 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 604
adam@347 605 Theorem evalCmd_coind : forall vs1 c vs2, R vs1 c vs2 -> evalCmd vs1 c vs2.
adam@347 606 cofix; intros; destruct c.
adam@347 607 rewrite (AssignCase H); constructor.
adam@347 608 destruct (SeqCase H) as [? [? ?]]; econstructor; eauto.
adam@347 609 destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst;
adam@347 610 [ econstructor | econstructor 4 ]; eauto.
adam@347 611 Qed.
adam@347 612 End evalCmd_coind.
adam@347 613
adam@347 614 (** 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 615
adam@347 616 Fixpoint optExp (e : exp) : exp :=
adam@347 617 match e with
adam@347 618 | Plus (Const 0) e => optExp e
adam@347 619 | Plus e1 e2 => Plus (optExp e1) (optExp e2)
adam@347 620 | _ => e
adam@347 621 end.
adam@347 622
adam@347 623 Fixpoint optCmd (c : cmd) : cmd :=
adam@347 624 match c with
adam@347 625 | Assign v e => Assign v (optExp e)
adam@347 626 | Seq c1 c2 => Seq (optCmd c1) (optCmd c2)
adam@347 627 | While e c => While (optExp e) (optCmd c)
adam@347 628 end.
adam@347 629
adam@347 630 (** 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 631
adam@347 632 (* begin thide *)
adam@347 633 Lemma optExp_correct : forall vs e, evalExp vs (optExp e) = evalExp vs e.
adam@347 634 induction e; crush;
adam@347 635 repeat (match goal with
adam@347 636 | [ |- context[match ?E with Const _ => _ | Var _ => _
adam@347 637 | Plus _ _ => _ end] ] => destruct E
adam@347 638 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
adam@347 639 end; crush).
adamc@64 640 Qed.
adamc@64 641
adam@375 642 Hint Rewrite optExp_correct .
adamc@64 643
adam@384 644 (** 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 645
adam@384 646 Ltac finisher := match goal with
adam@384 647 | [ H : evalCmd _ _ _ |- _ ] => ((inversion H; [])
adam@384 648 || (inversion H; [|])); subst
adam@384 649 end; crush; eauto 10.
adam@384 650
adam@384 651 Lemma optCmd_correct1 : forall vs1 c vs2, evalCmd vs1 c vs2
adam@347 652 -> evalCmd vs1 (optCmd c) vs2.
adam@347 653 intros; apply (evalCmd_coind (fun vs1 c' vs2 => exists c, evalCmd vs1 c vs2
adam@347 654 /\ c' = optCmd c)); eauto; crush;
adam@347 655 match goal with
adam@347 656 | [ H : _ = optCmd ?E |- _ ] => destruct E; simpl in *; discriminate
adam@347 657 || injection H; intros; subst
adam@384 658 end; finisher.
adam@384 659 Qed.
adam@384 660
adam@384 661 Lemma optCmd_correct2 : forall vs1 c vs2, evalCmd vs1 (optCmd c) vs2
adam@384 662 -> evalCmd vs1 c vs2.
adam@384 663 intros; apply (evalCmd_coind (fun vs1 c vs2 => evalCmd vs1 (optCmd c) vs2));
adam@384 664 crush; finisher.
adam@384 665 Qed.
adam@384 666
adam@384 667 Theorem optCmd_correct : forall vs1 c vs2, evalCmd vs1 (optCmd c) vs2
adam@384 668 <-> evalCmd vs1 c vs2.
adam@384 669 intuition; apply optCmd_correct1 || apply optCmd_correct2; assumption.
adam@347 670 Qed.
adam@347 671 (* end thide *)
adamc@64 672
adam@422 673 (** 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. *)