annotate src/Coinductive.v @ 321:a9edc6ecd904

Publish this repo publicly
author Adam Chlipala <adam@chlipala.net>
date Wed, 14 Sep 2011 14:04:08 -0400
parents d5787b70cf48
children 5d85de065540
rev   line source
adam@281 1 (* Copyright (c) 2008-2010, Adam Chlipala
adamc@62 2 *
adamc@62 3 * This work is licensed under a
adamc@62 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@62 5 * Unported License.
adamc@62 6 * The license text is available at:
adamc@62 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@62 8 *)
adamc@62 9
adamc@62 10 (* begin hide *)
adamc@62 11 Require Import List.
adamc@62 12
adam@314 13 Require Import CpdtTactics.
adamc@62 14
adamc@62 15 Set Implicit Arguments.
adamc@62 16 (* end hide *)
adamc@62 17
adamc@62 18
adamc@62 19 (** %\chapter{Infinite Data and Proofs}% *)
adamc@62 20
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 Fixpoint bad (u : unit) : P := bad u.
adamc@211 29
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@292 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. This is a heavyweight solution, and so we would like to avoid it whenever possible.
adamc@62 37
adamc@62 38 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 39
adamc@62 40
adamc@62 41 (** * Computing with Infinite Data *)
adamc@62 42
adamc@62 43 (** Let us begin with the most basic type of infinite data, %\textit{%#<i>#streams#</i>#%}%, or lazy lists. *)
adamc@62 44
adamc@62 45 Section stream.
adamc@62 46 Variable A : Set.
adamc@62 47
adamc@62 48 CoInductive stream : Set :=
adamc@62 49 | Cons : A -> stream -> stream.
adamc@62 50 End stream.
adamc@62 51
adamc@62 52 (** 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 53
adamc@62 54 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 55
adamc@62 56 We can define a stream consisting only of zeroes. *)
adamc@62 57
adamc@62 58 CoFixpoint zeroes : stream nat := Cons 0 zeroes.
adamc@62 59
adamc@62 60 (** We can also define a stream that alternates between [true] and [false]. *)
adamc@62 61
adamc@62 62 CoFixpoint trues : stream bool := Cons true falses
adamc@62 63 with falses : stream bool := Cons false trues.
adamc@62 64
adamc@62 65 (** 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 66
adamc@211 67 Fixpoint approx A (s : stream A) (n : nat) : list A :=
adamc@62 68 match n with
adamc@62 69 | O => nil
adamc@62 70 | S n' =>
adamc@62 71 match s with
adamc@62 72 | Cons h t => h :: approx t n'
adamc@62 73 end
adamc@62 74 end.
adamc@62 75
adamc@62 76 Eval simpl in approx zeroes 10.
adamc@211 77 (** %\vspace{-.15in}% [[
adamc@62 78 = 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: nil
adamc@62 79 : list nat
adam@302 80 ]]
adam@302 81 *)
adamc@211 82
adamc@62 83 Eval simpl in approx trues 10.
adamc@211 84 (** %\vspace{-.15in}% [[
adamc@62 85 = true
adamc@62 86 :: false
adamc@62 87 :: true
adamc@62 88 :: false
adamc@62 89 :: true :: false :: true :: false :: true :: false :: nil
adamc@62 90 : list bool
adamc@211 91
adamc@211 92 ]]
adamc@62 93
adamc@211 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@62 101 Error:
adamc@62 102 Recursive definition of looper is ill-formed.
adamc@62 103 In environment
adamc@62 104 looper : stream nat
adamc@62 105
adamc@62 106 unguarded recursive call in "looper"
adamc@211 107
adamc@205 108 ]]
adamc@205 109
adamc@211 110 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 111
adamc@62 112 The second rule of guardedness is easiest to see by first introducing a more complicated, but legal, co-fixpoint. *)
adamc@62 113
adamc@62 114 Section map.
adamc@62 115 Variables A B : Set.
adamc@62 116 Variable f : A -> B.
adamc@62 117
adamc@62 118 CoFixpoint map (s : stream A) : stream B :=
adamc@62 119 match s with
adamc@62 120 | Cons h t => Cons (f h) (map t)
adamc@62 121 end.
adamc@62 122 End map.
adamc@62 123
adamc@62 124 (** 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 125
adamc@211 126 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 [interleave] takes two streams and produces a new stream that alternates between their elements. *)
adamc@62 127
adamc@62 128 Section interleave.
adamc@62 129 Variable A : Set.
adamc@62 130
adamc@62 131 CoFixpoint interleave (s1 s2 : stream A) : stream A :=
adamc@62 132 match s1, s2 with
adamc@62 133 | Cons h1 t1, Cons h2 t2 => Cons h1 (Cons h2 (interleave t1 t2))
adamc@62 134 end.
adamc@62 135 End interleave.
adamc@62 136
adamc@62 137 (** Now say we want to write a weird stuttering version of [map] that repeats elements in a particular way, based on interleaving. *)
adamc@62 138
adamc@62 139 Section map'.
adamc@62 140 Variables A B : Set.
adamc@62 141 Variable f : A -> B.
adamc@68 142 (* begin thide *)
adamc@62 143 (** [[
adamc@62 144 CoFixpoint map' (s : stream A) : stream B :=
adamc@62 145 match s with
adam@281 146 | Cons h t => interleave (Cons (f h) (map' t) (Cons (f h) (map' t))
adamc@68 147 end.
adamc@211 148
adamc@205 149 ]]
adamc@211 150
adamc@211 151 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 152
adam@281 153 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' t] from within [Cons (f h) (map' t)]. Next it might try a [match] on this retrieved value, which amounts to deconstructing [map' t]. To figure out how this [match] turns out, we need to know the top-level structure of [map' t], 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 154 (* end thide *)
adamc@211 155
adamc@62 156 End map'.
adamc@62 157
adamc@63 158
adamc@63 159 (** * Infinite Proofs *)
adamc@63 160
adamc@63 161 (** 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 162
adamc@63 163 CoFixpoint ones : stream nat := Cons 1 ones.
adamc@63 164 Definition ones' := map S zeroes.
adamc@63 165
adamc@63 166 (** The obvious statement of the equality is this: *)
adamc@63 167
adamc@63 168 Theorem ones_eq : ones = ones'.
adamc@63 169
adamc@63 170 (** 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 171 (* begin thide *)
adamc@211 172
adamc@63 173 Abort.
adamc@63 174
adamc@63 175 (** 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 176
adamc@63 177 We are ready for our first co-inductive predicate. *)
adamc@63 178
adamc@63 179 Section stream_eq.
adamc@63 180 Variable A : Set.
adamc@63 181
adamc@63 182 CoInductive stream_eq : stream A -> stream A -> Prop :=
adamc@63 183 | Stream_eq : forall h t1 t2,
adamc@63 184 stream_eq t1 t2
adamc@63 185 -> stream_eq (Cons h t1) (Cons h t2).
adamc@63 186 End stream_eq.
adamc@63 187
adamc@63 188 (** 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 189
adamc@63 190 We can try restating the theorem with [stream_eq]. *)
adamc@63 191
adamc@63 192 Theorem ones_eq : stream_eq ones ones'.
adamc@63 193 (** 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 194
adamc@63 195 cofix.
adamc@63 196 (** [[
adamc@63 197 ones_eq : stream_eq ones ones'
adamc@63 198 ============================
adamc@63 199 stream_eq ones ones'
adamc@211 200
adamc@211 201 ]]
adamc@63 202
adamc@211 203 It looks like this proof might be easier than we expected! *)
adamc@63 204
adamc@63 205 assumption.
adamc@63 206 (** [[
adamc@211 207 Proof completed.
adamc@211 208
adamc@211 209 ]]
adamc@63 210
adamc@211 211 Unfortunately, we are due for some disappointment in our victory lap.
adamc@205 212
adamc@211 213 [[
adamc@63 214 Qed.
adamc@63 215
adamc@63 216 Error:
adamc@63 217 Recursive definition of ones_eq is ill-formed.
adamc@63 218
adamc@63 219 In environment
adamc@63 220 ones_eq : stream_eq ones ones'
adamc@63 221
adamc@205 222 unguarded recursive call in "ones_eq"
adamc@211 223
adamc@211 224 ]]
adamc@205 225
adamc@211 226 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 227
adamc@211 228 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 229
adamc@63 230 [[
adamc@63 231 Guarded.
adamc@63 232
adamc@205 233 ]]
adamc@205 234
adamc@63 235 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 236
adam@281 237 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 238
adamc@63 239 Undo.
adamc@63 240 simpl.
adamc@63 241 (** [[
adamc@63 242 ones_eq : stream_eq ones ones'
adamc@63 243 ============================
adamc@63 244 stream_eq ones ones'
adamc@211 245
adamc@211 246 ]]
adamc@63 247
adamc@211 248 It turns out that we are best served by proving an auxiliary lemma. *)
adamc@211 249
adamc@63 250 Abort.
adamc@63 251
adamc@63 252 (** First, we need to define a function that seems pointless on first glance. *)
adamc@63 253
adamc@63 254 Definition frob A (s : stream A) : stream A :=
adamc@63 255 match s with
adamc@63 256 | Cons h t => Cons h t
adamc@63 257 end.
adamc@63 258
adamc@63 259 (** Next, we need to prove a theorem that seems equally pointless. *)
adamc@63 260
adamc@63 261 Theorem frob_eq : forall A (s : stream A), s = frob s.
adamc@63 262 destruct s; reflexivity.
adamc@63 263 Qed.
adamc@63 264
adamc@63 265 (** But, miraculously, this theorem turns out to be just what we needed. *)
adamc@63 266
adamc@63 267 Theorem ones_eq : stream_eq ones ones'.
adamc@63 268 cofix.
adamc@63 269
adamc@63 270 (** We can use the theorem to rewrite the two streams. *)
adamc@211 271
adamc@63 272 rewrite (frob_eq ones).
adamc@63 273 rewrite (frob_eq ones').
adamc@63 274 (** [[
adamc@63 275 ones_eq : stream_eq ones ones'
adamc@63 276 ============================
adamc@63 277 stream_eq (frob ones) (frob ones')
adamc@211 278
adamc@211 279 ]]
adamc@63 280
adamc@211 281 Now [simpl] is able to reduce the streams. *)
adamc@63 282
adamc@63 283 simpl.
adamc@63 284 (** [[
adamc@63 285 ones_eq : stream_eq ones ones'
adamc@63 286 ============================
adamc@63 287 stream_eq (Cons 1 ones)
adamc@63 288 (Cons 1
adamc@63 289 ((cofix map (s : stream nat) : stream nat :=
adamc@63 290 match s with
adamc@63 291 | Cons h t => Cons (S h) (map t)
adamc@63 292 end) zeroes))
adamc@211 293
adamc@211 294 ]]
adamc@63 295
adamc@211 296 Since we have exposed the [Cons] structure of each stream, we can apply the constructor of [stream_eq]. *)
adamc@63 297
adamc@63 298 constructor.
adamc@63 299 (** [[
adamc@63 300 ones_eq : stream_eq ones ones'
adamc@63 301 ============================
adamc@63 302 stream_eq ones
adamc@63 303 ((cofix map (s : stream nat) : stream nat :=
adamc@63 304 match s with
adamc@63 305 | Cons h t => Cons (S h) (map t)
adamc@63 306 end) zeroes)
adamc@211 307
adamc@211 308 ]]
adamc@63 309
adamc@211 310 Now, modulo unfolding of the definition of [map], we have matched our assumption. *)
adamc@211 311
adamc@63 312 assumption.
adamc@63 313 Qed.
adamc@63 314
adamc@63 315 (** 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 316
adamc@63 317 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 318
adamc@63 319 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 320
adamc@63 321 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 322
adamc@63 323 Theorem ones_eq' : stream_eq ones ones'.
adamc@63 324 cofix; crush.
adamc@63 325 (** [[
adamc@205 326 Guarded.
adamc@205 327
adam@302 328 ]]
adam@302 329 *)
adamc@63 330 Abort.
adamc@68 331 (* end thide *)
adamc@63 332
adam@292 333 (** 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. *)
adamc@64 334
adamc@64 335
adamc@64 336 (** * Simple Modeling of Non-Terminating Programs *)
adamc@64 337
adamc@211 338 (** We close the chapter with a quick motivating example for more complex uses of co-inductive types. We will define a co-inductive semantics for a simple assembly language and use that semantics to prove that assembly programs always run forever. This basic technique can be combined with typing judgments for more advanced languages, where some ill-typed programs can go wrong, but no well-typed programs go wrong.
adamc@64 339
adamc@211 340 We define suggestive synonyms for [nat], for cases where we use natural numbers as registers or program labels. That is, we consider our idealized machine to have infinitely many registers and infinitely many code addresses. *)
adamc@211 341
adamc@211 342 Definition reg := nat.
adamc@64 343 Definition label := nat.
adamc@64 344
adamc@211 345 (** Our instructions are loading of a constant into a register, copying from one register to another, unconditional jump, and conditional jump based on whether the value in a register is not zero. *)
adamc@64 346
adamc@211 347 Inductive instr : Set :=
adamc@211 348 | Imm : reg -> nat -> instr
adamc@211 349 | Copy : reg -> reg -> instr
adamc@211 350 | Jmp : label -> instr
adamc@211 351 | Jnz : reg -> label -> instr.
adamc@67 352
adam@281 353 (** We define a type [regs] of maps from registers to values. To define a function [set] for setting a register's value in a map, we import the [Arith] module from Coq's standard library, and we use its function [beq_nat] for comparing natural numbers. *)
adamc@67 354
adamc@211 355 Definition regs := reg -> nat.
adamc@211 356 Require Import Arith.
adamc@211 357 Definition set (rs : regs) (r : reg) (v : nat) : regs :=
adam@281 358 fun r' => if beq_nat r r' then v else rs r'.
adamc@64 359
adamc@211 360 (** An inductive [exec] judgment captures the effect of an instruction on the program counter and register bank. *)
adamc@64 361
adamc@211 362 Inductive exec : label -> regs -> instr -> label -> regs -> Prop :=
adamc@211 363 | E_Imm : forall pc rs r n, exec pc rs (Imm r n) (S pc) (set rs r n)
adamc@211 364 | E_Copy : forall pc rs r1 r2, exec pc rs (Copy r1 r2) (S pc) (set rs r1 (rs r2))
adamc@211 365 | E_Jmp : forall pc rs pc', exec pc rs (Jmp pc') pc' rs
adamc@211 366 | E_JnzF : forall pc rs r pc', rs r = 0 -> exec pc rs (Jnz r pc') (S pc) rs
adamc@211 367 | E_JnzT : forall pc rs r pc' n, rs r = S n -> exec pc rs (Jnz r pc') pc' rs.
adamc@64 368
adamc@211 369 (** We prove that [exec] represents a total function. In our proof script, we use a [match] tactic with a [context] pattern. This particular example finds an occurrence of a pattern [Jnz ?r _] anywhere in the current subgoal's conclusion. We use a Coq library tactic [case_eq] to do case analysis on whether the current value [rs r] of the register [r] is zero or not. [case_eq] differs from [destruct] in saving an equality relating the old variable to the new form we deduce for it. *)
adamc@64 370
adamc@211 371 Lemma exec_total : forall pc rs i,
adamc@211 372 exists pc', exists rs', exec pc rs i pc' rs'.
adamc@211 373 Hint Constructors exec.
adamc@67 374
adamc@211 375 destruct i; crush; eauto;
adamc@211 376 match goal with
adamc@211 377 | [ |- context[Jnz ?r _] ] => case_eq (rs r)
adamc@211 378 end; eauto.
adamc@64 379 Qed.
adamc@64 380
adam@281 381 (** We are ready to define a co-inductive judgment capturing the idea that a program runs forever. We define the judgment in terms of a program [prog], represented as a function mapping each label to the instruction found there. That is, to simplify the proof, we consider only infinitely-long programs. *)
adamc@64 382
adamc@211 383 Section safe.
adamc@211 384 Variable prog : label -> instr.
adamc@64 385
adamc@211 386 CoInductive safe : label -> regs -> Prop :=
adamc@211 387 | Step : forall pc r pc' r',
adamc@211 388 exec pc r (prog pc) pc' r'
adamc@211 389 -> safe pc' r'
adamc@211 390 -> safe pc r.
adamc@64 391
adam@292 392 (** Now we can prove that any starting address and register bank lead to safe infinite execution. Recall that proofs of existentially-quantified formulas are all built with a single constructor of the inductive type [ex]. This means that we can use [destruct] to %``%#"#open up#"#%''% such proofs. In the proof below, we want to perform this opening up on an appropriate use of the [exec_total] lemma. This lemma's conclusion begins with two existential quantifiers, so we want to tell [destruct] that it should not stop at the first quantifier. We accomplish our goal by using an %\textit{%#<i>#intro pattern#</i>#%}% with [destruct]. Consult the Coq manual for the details of intro patterns; the specific pattern [[? [? ?]]] that we use here accomplishes our goal of destructing both quantifiers at once. *)
adamc@211 393
adamc@211 394 Theorem always_safe : forall pc rs,
adamc@211 395 safe pc rs.
adamc@211 396 cofix; intros;
adamc@211 397 destruct (exec_total pc rs (prog pc)) as [? [? ?]];
adamc@211 398 econstructor; eauto.
adamc@64 399 Qed.
adamc@211 400 End safe.
adamc@64 401
adamc@67 402 (** 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 403
adamc@211 404 Print always_safe.
adamc@81 405
adamc@81 406
adamc@81 407 (** * Exercises *)
adamc@81 408
adamc@81 409 (** %\begin{enumerate}%#<ol>#
adamc@81 410
adamc@81 411 %\item%#<li># %\begin{enumerate}%#<ol>#
adamc@81 412 %\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 413 %\item%#<li># Define a function [everywhere] for building a tree with the same data value at every node.#</li>#
adamc@81 414 %\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 415 %\item%#<li># Define a tree [falses] where every node has the value [false].#</li>#
adamc@104 416 %\item%#<li># Define a tree [true_false] where the root node has value [true], its children have value [false], all nodes at the next have the value [true], and so on, alternating boolean values from level to level.#</li>#
adam@292 417 %\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 418 #</ol>#%\end{enumerate}% #</li>#
adamc@81 419
adamc@81 420 #</ol>#%\end{enumerate}% *)