annotate src/Coinductive.v @ 206:3f4576f15130

Revising for 8.2 through first big example
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 16:44:06 -0500
parents f05514cc6c0d
children d06726f49bc6
rev   line source
adamc@62 1 (* Copyright (c) 2008, 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
adamc@62 13 Require Import Tactics.
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
adamc@62 21 (** In lazy functional programming languages like 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
adamc@62 23 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
adamc@202 25 We spent some time in the last chapter discussing the 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 [[
adamc@202 28
adamc@202 29 Fixpoint bad (u : unit) : P := bad u.
adamc@202 30
adamc@205 31 ]]
adamc@205 32
adamc@202 33 This would leave us with [bad tt] as a proof of [P].
adamc@62 34
adamc@62 35 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 36
adamc@62 37 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. In later chapters, we will spend some time on this idea and its applications. For now, we will just say that it is a heavyweight solution, and so we would like to avoid it whenever possible.
adamc@62 38
adamc@62 39 Luckily, Coq has special support for a class of lazy data structures that happens to contain most examples found in Haskell. That mechanism, %\textit{%#<i>#co-inductive types#</i>#%}%, is the subject of this chapter. *)
adamc@62 40
adamc@62 41
adamc@62 42 (** * Computing with Infinite Data *)
adamc@62 43
adamc@62 44 (** Let us begin with the most basic type of infinite data, %\textit{%#<i>#streams#</i>#%}%, or lazy lists. *)
adamc@62 45
adamc@62 46 Section stream.
adamc@62 47 Variable A : Set.
adamc@62 48
adamc@62 49 CoInductive stream : Set :=
adamc@62 50 | Cons : A -> stream -> stream.
adamc@62 51 End stream.
adamc@62 52
adamc@62 53 (** 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 54
adamc@62 55 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 %\textit{%#<i>#co-recursive definitions#</i>#%}% to %\textit{%#<i>#build#</i>#%}% values of co-inductive types effectively.
adamc@62 56
adamc@62 57 We can define a stream consisting only of zeroes. *)
adamc@62 58
adamc@62 59 CoFixpoint zeroes : stream nat := Cons 0 zeroes.
adamc@62 60
adamc@62 61 (** We can also define a stream that alternates between [true] and [false]. *)
adamc@62 62
adamc@62 63 CoFixpoint trues : stream bool := Cons true falses
adamc@62 64 with falses : stream bool := Cons false trues.
adamc@62 65
adamc@62 66 (** 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 67
adamc@62 68 Fixpoint approx A (s : stream A) (n : nat) {struct n} : list A :=
adamc@62 69 match n with
adamc@62 70 | O => nil
adamc@62 71 | S n' =>
adamc@62 72 match s with
adamc@62 73 | Cons h t => h :: approx t n'
adamc@62 74 end
adamc@62 75 end.
adamc@62 76
adamc@62 77 Eval simpl in approx zeroes 10.
adamc@62 78 (** [[
adamc@62 79
adamc@62 80 = 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: nil
adamc@62 81 : list nat
adamc@62 82 ]] *)
adamc@62 83 Eval simpl in approx trues 10.
adamc@62 84 (** [[
adamc@62 85
adamc@62 86 = true
adamc@62 87 :: false
adamc@62 88 :: true
adamc@62 89 :: false
adamc@62 90 :: true :: false :: true :: false :: true :: false :: nil
adamc@62 91 : list bool
adamc@62 92 ]] *)
adamc@62 93
adamc@62 94 (** 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 95
adamc@62 96 The restriction for co-inductive types shows up as the %\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 97
adamc@62 98 [[
adamc@62 99 CoFixpoint looper : stream nat := looper.
adamc@205 100
adamc@205 101 ]]
adamc@205 102
adamc@62 103 [[
adamc@62 104 Error:
adamc@62 105 Recursive definition of looper is ill-formed.
adamc@62 106 In environment
adamc@62 107 looper : stream nat
adamc@62 108
adamc@62 109 unguarded recursive call in "looper"
adamc@205 110 ]]
adamc@205 111
adamc@62 112 *)
adamc@202 113
adamc@62 114
adamc@62 115 (** 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 116
adamc@62 117 The second rule of guardedness is easiest to see by first introducing a more complicated, but legal, co-fixpoint. *)
adamc@62 118
adamc@62 119 Section map.
adamc@62 120 Variables A B : Set.
adamc@62 121 Variable f : A -> B.
adamc@62 122
adamc@62 123 CoFixpoint map (s : stream A) : stream B :=
adamc@62 124 match s with
adamc@62 125 | Cons h t => Cons (f h) (map t)
adamc@62 126 end.
adamc@62 127 End map.
adamc@62 128
adamc@62 129 (** 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 even the first guardedness condition.
adamc@62 130
adamc@62 131 The second condition is subtler. To illustrate it, we start off with another co-recursive function definition that %\textit{%#<i>#is#</i>#%}% legal. The function [interleaves] takes two streams and produces a new stream that alternates between their elements. *)
adamc@62 132
adamc@62 133 Section interleave.
adamc@62 134 Variable A : Set.
adamc@62 135
adamc@62 136 CoFixpoint interleave (s1 s2 : stream A) : stream A :=
adamc@62 137 match s1, s2 with
adamc@62 138 | Cons h1 t1, Cons h2 t2 => Cons h1 (Cons h2 (interleave t1 t2))
adamc@62 139 end.
adamc@62 140 End interleave.
adamc@62 141
adamc@62 142 (** Now say we want to write a weird stuttering version of [map] that repeats elements in a particular way, based on interleaving. *)
adamc@62 143
adamc@62 144 Section map'.
adamc@62 145 Variables A B : Set.
adamc@62 146 Variable f : A -> B.
adamc@62 147
adamc@68 148 (* begin thide *)
adamc@62 149 (** [[
adamc@62 150
adamc@62 151 CoFixpoint map' (s : stream A) : stream B :=
adamc@62 152 match s with
adamc@62 153 | Cons h t => interleave (Cons (f h) (map' s)) (Cons (f h) (map' s))
adamc@68 154 end.
adamc@205 155
adamc@205 156 ]]
adamc@68 157 *)
adamc@62 158
adamc@62 159 (** We get another error message about an unguarded recursive call. This is because we are violating the second guardedness condition, which says that, not only must co-recursive calls be arguments to constructors, there must also %\textit{%#<i>#not be anything but [match]es and calls to constructors of the same co-inductive type#</i>#%}% wrapped around these immediate uses of co-recursive calls. The actual implemented rule for guardedness is a little more lenient than what we have just stated, but you can count on the illegality of any exception that would enhance the expressive power of co-recursion.
adamc@62 160
adamc@62 161 Why enforce a rule like this? Imagine that, instead of [interleave], we had called some other, less well-behaved function on streams. Perhaps this other function might be defined mutually with [map']. It might deconstruct its first argument, retrieving [map' s] from within [Cons (f h) (map' s)]. Next it might try a [match] on this retrieved value, which amounts to deconstructing [map' s]. To figure out how this [match] turns out, we need to know the top-level structure of [map' s], but this is exactly what we started out trying to determine! We run into a loop in the evaluation process, and we have reached a witness of inconsistency if we are evaluating [approx (map' s) 1] for any [s]. *)
adamc@68 162 (* end thide *)
adamc@62 163 End map'.
adamc@62 164
adamc@63 165
adamc@63 166 (** * Infinite Proofs *)
adamc@63 167
adamc@63 168 (** 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 169
adamc@63 170 CoFixpoint ones : stream nat := Cons 1 ones.
adamc@63 171 Definition ones' := map S zeroes.
adamc@63 172
adamc@63 173 (** The obvious statement of the equality is this: *)
adamc@63 174
adamc@63 175 Theorem ones_eq : ones = ones'.
adamc@63 176
adamc@63 177 (** 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 178 (* begin thide *)
adamc@63 179 Abort.
adamc@63 180
adamc@63 181 (** 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 182
adamc@63 183 We are ready for our first co-inductive predicate. *)
adamc@63 184
adamc@63 185 Section stream_eq.
adamc@63 186 Variable A : Set.
adamc@63 187
adamc@63 188 CoInductive stream_eq : stream A -> stream A -> Prop :=
adamc@63 189 | Stream_eq : forall h t1 t2,
adamc@63 190 stream_eq t1 t2
adamc@63 191 -> stream_eq (Cons h t1) (Cons h t2).
adamc@63 192 End stream_eq.
adamc@63 193
adamc@63 194 (** 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 195
adamc@63 196 We can try restating the theorem with [stream_eq]. *)
adamc@63 197
adamc@63 198 Theorem ones_eq : stream_eq ones ones'.
adamc@63 199 (** 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@63 200 cofix.
adamc@63 201 (** [[
adamc@63 202
adamc@63 203 ones_eq : stream_eq ones ones'
adamc@63 204 ============================
adamc@63 205 stream_eq ones ones'
adamc@63 206 ]] *)
adamc@63 207
adamc@63 208 (** It looks like this proof might be easier than we expected! *)
adamc@63 209
adamc@63 210 assumption.
adamc@63 211 (** [[
adamc@63 212
adamc@205 213 Proof completed.
adamc@205 214
adamc@205 215 ]] *)
adamc@63 216
adamc@63 217 (** Unfortunately, we are due for some disappointment in our victory lap. *)
adamc@63 218
adamc@63 219 (** [[
adamc@63 220 Qed.
adamc@63 221
adamc@63 222 Error:
adamc@63 223 Recursive definition of ones_eq is ill-formed.
adamc@63 224
adamc@63 225 In environment
adamc@63 226 ones_eq : stream_eq ones ones'
adamc@63 227
adamc@205 228 unguarded recursive call in "ones_eq"
adamc@205 229
adamc@205 230 ]] *)
adamc@63 231
adamc@63 232 (** 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 233
adamc@63 234 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 first part of 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.
adamc@63 235
adamc@63 236 [[
adamc@63 237 Guarded.
adamc@63 238
adamc@205 239 ]]
adamc@205 240
adamc@63 241 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 242
adamc@63 243 We need to start the co-induction by applying one of [stream_eq]'s constructors. 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 244
adamc@63 245 Undo.
adamc@63 246 simpl.
adamc@63 247 (** [[
adamc@63 248
adamc@63 249 ones_eq : stream_eq ones ones'
adamc@63 250 ============================
adamc@63 251 stream_eq ones ones'
adamc@63 252 ]] *)
adamc@63 253
adamc@63 254 (** It turns out that we are best served by proving an auxiliary lemma. *)
adamc@63 255 Abort.
adamc@63 256
adamc@63 257 (** First, we need to define a function that seems pointless on first glance. *)
adamc@63 258
adamc@63 259 Definition frob A (s : stream A) : stream A :=
adamc@63 260 match s with
adamc@63 261 | Cons h t => Cons h t
adamc@63 262 end.
adamc@63 263
adamc@63 264 (** Next, we need to prove a theorem that seems equally pointless. *)
adamc@63 265
adamc@63 266 Theorem frob_eq : forall A (s : stream A), s = frob s.
adamc@63 267 destruct s; reflexivity.
adamc@63 268 Qed.
adamc@63 269
adamc@63 270 (** But, miraculously, this theorem turns out to be just what we needed. *)
adamc@63 271
adamc@63 272 Theorem ones_eq : stream_eq ones ones'.
adamc@63 273 cofix.
adamc@63 274
adamc@63 275 (** We can use the theorem to rewrite the two streams. *)
adamc@63 276 rewrite (frob_eq ones).
adamc@63 277 rewrite (frob_eq ones').
adamc@63 278 (** [[
adamc@63 279
adamc@63 280 ones_eq : stream_eq ones ones'
adamc@63 281 ============================
adamc@63 282 stream_eq (frob ones) (frob ones')
adamc@63 283 ]] *)
adamc@63 284
adamc@63 285 (** Now [simpl] is able to reduce the streams. *)
adamc@63 286
adamc@63 287 simpl.
adamc@63 288 (** [[
adamc@63 289
adamc@63 290 ones_eq : stream_eq ones ones'
adamc@63 291 ============================
adamc@63 292 stream_eq (Cons 1 ones)
adamc@63 293 (Cons 1
adamc@63 294 ((cofix map (s : stream nat) : stream nat :=
adamc@63 295 match s with
adamc@63 296 | Cons h t => Cons (S h) (map t)
adamc@63 297 end) zeroes))
adamc@63 298 ]] *)
adamc@63 299
adamc@63 300 (** Since we have exposed the [Cons] structure of each stream, we can apply the constructor of [stream_eq]. *)
adamc@63 301
adamc@63 302 constructor.
adamc@63 303 (** [[
adamc@63 304
adamc@63 305 ones_eq : stream_eq ones ones'
adamc@63 306 ============================
adamc@63 307 stream_eq ones
adamc@63 308 ((cofix map (s : stream nat) : stream nat :=
adamc@63 309 match s with
adamc@63 310 | Cons h t => Cons (S h) (map t)
adamc@63 311 end) zeroes)
adamc@63 312 ]] *)
adamc@63 313
adamc@63 314 (** Now, modulo unfolding of the definition of [map], we have matched our assumption. *)
adamc@63 315 assumption.
adamc@63 316 Qed.
adamc@63 317
adamc@63 318 (** 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 319
adamc@63 320 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 321
adamc@63 322 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 323
adamc@63 324 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 325
adamc@63 326 Theorem ones_eq' : stream_eq ones ones'.
adamc@63 327 cofix; crush.
adamc@63 328 (** [[
adamc@63 329
adamc@205 330 Guarded.
adamc@205 331
adamc@205 332 ]] *)
adamc@63 333 Abort.
adamc@68 334 (* end thide *)
adamc@63 335
adamc@63 336 (** 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. We will see examples of effective co-inductive proving in later chapters. *)
adamc@64 337
adamc@64 338
adamc@64 339 (** * Simple Modeling of Non-Terminating Programs *)
adamc@64 340
adamc@67 341 (** 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 an optimization function is sound. We start by defining types of registers, program labels, and instructions. *)
adamc@64 342
adamc@64 343 Inductive reg : Set := R1 | R2.
adamc@64 344 Definition label := nat.
adamc@64 345
adamc@64 346 Inductive instrs : Set :=
adamc@64 347 | Const : reg -> nat -> instrs -> instrs
adamc@64 348 | Add : reg -> reg -> reg -> instrs -> instrs
adamc@64 349 | Halt : reg -> instrs
adamc@64 350 | Jeq : reg -> reg -> label -> instrs -> instrs.
adamc@64 351
adamc@67 352 (** [Const] stores a constant in a register; [Add] stores in the first register the sum of the values in the second two; [Halt] ends the program, returning the value of its register argument; and [Jeq] jumps to a label if the values in two registers are equal. Each instruction but [Halt] takes an [instrs], which can be read as "list of instructions," as the normal continuation of control flow.
adamc@67 353
adamc@67 354 We can define a program as a list of lists of instructions, where labels will be interpreted as indexing into such a list. *)
adamc@67 355
adamc@64 356 Definition program := list instrs.
adamc@64 357
adamc@67 358 (** We define a polymorphic map type for register keys, with its associated operations. *)
adamc@64 359 Section regmap.
adamc@64 360 Variable A : Set.
adamc@64 361
adamc@64 362 Record regmap : Set := Regmap {
adamc@64 363 VR1 : A;
adamc@64 364 VR2 : A
adamc@64 365 }.
adamc@64 366
adamc@67 367 Definition empty (v : A) : regmap := Regmap v v.
adamc@64 368 Definition get (rm : regmap) (r : reg) : A :=
adamc@64 369 match r with
adamc@64 370 | R1 => VR1 rm
adamc@64 371 | R2 => VR2 rm
adamc@64 372 end.
adamc@64 373 Definition set (rm : regmap) (r : reg) (v : A) : regmap :=
adamc@64 374 match r with
adamc@64 375 | R1 => Regmap v (VR2 rm)
adamc@64 376 | R2 => Regmap (VR1 rm) v
adamc@64 377 end.
adamc@64 378 End regmap.
adamc@64 379
adamc@202 380 (** Now comes the interesting part. We define a co-inductive semantics for programs. The definition itself is not surprising. We could change [CoInductive] to [Inductive] and arrive at a valid semantics that only covers terminating program executions. Using [CoInductive] admits infinite derivations for infinite executions. An application [run rm is v] means that, when we run the instructions [is] starting with register map [rm], either execution terminates with result [v] or execution runs safely forever. (That is, the choice of [v] is immaterial for non-terminating executions.) *)
adamc@67 381
adamc@64 382 Section run.
adamc@64 383 Variable prog : program.
adamc@64 384
adamc@64 385 CoInductive run : regmap nat -> instrs -> nat -> Prop :=
adamc@64 386 | RConst : forall rm r n is v,
adamc@64 387 run (set rm r n) is v
adamc@64 388 -> run rm (Const r n is) v
adamc@64 389 | RAdd : forall rm r r1 r2 is v,
adamc@64 390 run (set rm r (get rm r1 + get rm r2)) is v
adamc@64 391 -> run rm (Add r r1 r2 is) v
adamc@64 392 | RHalt : forall rm r,
adamc@64 393 run rm (Halt r) (get rm r)
adamc@64 394 | RJeq_eq : forall rm r1 r2 l is is' v,
adamc@64 395 get rm r1 = get rm r2
adamc@64 396 -> nth_error prog l = Some is'
adamc@64 397 -> run rm is' v
adamc@64 398 -> run rm (Jeq r1 r2 l is) v
adamc@64 399 | RJeq_neq : forall rm r1 r2 l is v,
adamc@64 400 get rm r1 <> get rm r2
adamc@64 401 -> run rm is v
adamc@64 402 -> run rm (Jeq r1 r2 l is) v.
adamc@64 403 End run.
adamc@64 404
adamc@67 405 (** We can write a function which tracks known register values to attempt to constant fold a sequence of instructions. We track register values with a [regmap (option nat)], where a mapping to [None] indicates no information, and a mapping to [Some n] indicates that the corresponding register is known to have value [n]. *)
adamc@67 406
adamc@64 407 Fixpoint constFold (rm : regmap (option nat)) (is : instrs) {struct is} : instrs :=
adamc@64 408 match is with
adamc@64 409 | Const r n is => Const r n (constFold (set rm r (Some n)) is)
adamc@64 410 | Add r r1 r2 is =>
adamc@64 411 match get rm r1, get rm r2 with
adamc@67 412 | Some n1, Some n2 =>
adamc@67 413 Const r (n1 + n2) (constFold (set rm r (Some (n1 + n2))) is)
adamc@64 414 | _, _ => Add r r1 r2 (constFold (set rm r None) is)
adamc@64 415 end
adamc@64 416 | Halt _ => is
adamc@64 417 | Jeq r1 r2 l is => Jeq r1 r2 l (constFold rm is)
adamc@64 418 end.
adamc@64 419
adamc@67 420 (** We characterize when the two types of register maps we are using agree with each other. *)
adamc@67 421
adamc@64 422 Definition regmapCompat (rm : regmap nat) (rm' : regmap (option nat)) :=
adamc@64 423 forall r, match get rm' r with
adamc@64 424 | None => True
adamc@64 425 | Some v => get rm r = v
adamc@64 426 end.
adamc@64 427
adamc@67 428 (** We prove two lemmas about how register map modifications affect compatibility. A tactic [compat] abstracts the common structure of the two proofs. *)
adamc@67 429
adamc@67 430 (** remove printing * *)
adamc@64 431 Ltac compat := unfold regmapCompat in *; crush;
adamc@64 432 match goal with
adamc@88 433 | [ H : _ |- match get _ ?R with Some _ => _ | None => _ end ] => generalize (H R); destruct R; crush
adamc@64 434 end.
adamc@64 435
adamc@64 436 Lemma regmapCompat_set_None : forall rm rm' r n,
adamc@64 437 regmapCompat rm rm'
adamc@64 438 -> regmapCompat (set rm r n) (set rm' r None).
adamc@64 439 destruct r; compat.
adamc@64 440 Qed.
adamc@64 441
adamc@64 442 Lemma regmapCompat_set_Some : forall rm rm' r n,
adamc@64 443 regmapCompat rm rm'
adamc@64 444 -> regmapCompat (set rm r n) (set rm' r (Some n)).
adamc@64 445 destruct r; compat.
adamc@64 446 Qed.
adamc@64 447
adamc@67 448 (** Finally, we can prove the main theorem. *)
adamc@64 449
adamc@64 450 Section constFold_ok.
adamc@64 451 Variable prog : program.
adamc@64 452
adamc@64 453 Theorem constFold_ok : forall rm is v,
adamc@64 454 run prog rm is v
adamc@64 455 -> forall rm', regmapCompat rm rm'
adamc@64 456 -> run prog rm (constFold rm' is) v.
adamc@64 457 Hint Resolve regmapCompat_set_None regmapCompat_set_Some.
adamc@64 458 Hint Constructors run.
adamc@64 459
adamc@65 460 cofix;
adamc@65 461 destruct 1; crush; eauto;
adamc@65 462 repeat match goal with
adamc@67 463 | [ H : regmapCompat _ _
adamc@67 464 |- run _ _ (match get ?RM ?R with
adamc@67 465 | Some _ => _
adamc@67 466 | None => _
adamc@67 467 end) _ ] =>
adamc@65 468 generalize (H R); destruct (get RM R); crush
adamc@65 469 end.
adamc@64 470 Qed.
adamc@64 471 End constFold_ok.
adamc@64 472
adamc@67 473 (** 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 474
adamc@64 475 Print constFold_ok.
adamc@81 476
adamc@81 477
adamc@81 478 (** * Exercises *)
adamc@81 479
adamc@81 480 (** %\begin{enumerate}%#<ol>#
adamc@81 481
adamc@81 482 %\item%#<li># %\begin{enumerate}%#<ol>#
adamc@81 483 %\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 484 %\item%#<li># Define a function [everywhere] for building a tree with the same data value at every node.#</li>#
adamc@81 485 %\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 486 %\item%#<li># Define a tree [falses] where every node has the value [false].#</li>#
adamc@104 487 %\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>#
adamc@200 488 %\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 489 #</ol>#%\end{enumerate}% #</li>#
adamc@81 490
adamc@81 491 #</ol>#%\end{enumerate}% *)