Mercurial > cpdt > repo

comparison src/Coinductive.v @ 64:739c2818d6e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Co-inductive evaluation example
author Adam Chlipala <adamc@hcoop.net>
date Tue, 30 Sep 2008 17:47:59 -0400
parents fe7d37dfbd26
children 21bb59c56b98
comparison
equal deleted inserted replaced
63:fe7d37dfbd26 64:739c2818d6e2
303 303
304 Guarded. *) 304 Guarded. *)
305 Abort. 305 Abort.
306 306
307 (** 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. *) 307 (** 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. *)
308
309
310 (** * Simple Modeling of Non-Terminating Programs *)
311
312 (** 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 a type of instructions. *)
313
314 Inductive reg : Set := R1 | R2.
315 Definition label := nat.
316
317 Inductive instrs : Set :=
318 | Const : reg -> nat -> instrs -> instrs
319 | Add : reg -> reg -> reg -> instrs -> instrs
320 | Halt : reg -> instrs
321 | Jeq : reg -> reg -> label -> instrs -> instrs.
322
323 Definition program := list instrs.
324
325 Section regmap.
326 Variable A : Set.
327
328 Record regmap : Set := Regmap {
329 VR1 : A;
330 VR2 : A
331 }.
332
333 Definition empty v : regmap := Regmap v v.
334 Definition get (rm : regmap) (r : reg) : A :=
335 match r with
336 | R1 => VR1 rm
337 | R2 => VR2 rm
338 end.
339 Definition set (rm : regmap) (r : reg) (v : A) : regmap :=
340 match r with
341 | R1 => Regmap v (VR2 rm)
342 | R2 => Regmap (VR1 rm) v
343 end.
344 End regmap.
345
346 Section run.
347 Variable prog : program.
348
349 CoInductive run : regmap nat -> instrs -> nat -> Prop :=
350 | RConst : forall rm r n is v,
351 run (set rm r n) is v
352 -> run rm (Const r n is) v
353 | RAdd : forall rm r r1 r2 is v,
354 run (set rm r (get rm r1 + get rm r2)) is v
355 -> run rm (Add r r1 r2 is) v
356 | RHalt : forall rm r,
357 run rm (Halt r) (get rm r)
358 | RJeq_eq : forall rm r1 r2 l is is' v,
359 get rm r1 = get rm r2
360 -> nth_error prog l = Some is'
361 -> run rm is' v
362 -> run rm (Jeq r1 r2 l is) v
363 | RJeq_neq : forall rm r1 r2 l is v,
364 get rm r1 <> get rm r2
365 -> run rm is v
366 -> run rm (Jeq r1 r2 l is) v.
367 End run.
368
369 Fixpoint constFold (rm : regmap (option nat)) (is : instrs) {struct is} : instrs :=
370 match is with
371 | Const r n is => Const r n (constFold (set rm r (Some n)) is)
372 | Add r r1 r2 is =>
373 match get rm r1, get rm r2 with
374 | Some n1, Some n2 => Const r (n1 + n2) (constFold (set rm r (Some (n1 + n2))) is)
375 | _, _ => Add r r1 r2 (constFold (set rm r None) is)
376 end
377 | Halt _ => is
378 | Jeq r1 r2 l is => Jeq r1 r2 l (constFold rm is)
379 end.
380
381 Definition regmapCompat (rm : regmap nat) (rm' : regmap (option nat)) :=
382 forall r, match get rm' r with
383 | None => True
384 | Some v => get rm r = v
385 end.
386
387 Ltac compat := unfold regmapCompat in *; crush;
388 match goal with
389 | [ |- match get _ ?R with Some _ => _ | None => _ end ] => destruct R; crush
390 end.
391
392 Lemma regmapCompat_set_None : forall rm rm' r n,
393 regmapCompat rm rm'
394 -> regmapCompat (set rm r n) (set rm' r None).
395 destruct r; compat.
396 Qed.
397
398 Lemma regmapCompat_set_Some : forall rm rm' r n,
399 regmapCompat rm rm'
400 -> regmapCompat (set rm r n) (set rm' r (Some n)).
401 destruct r; compat.
402 Qed.
403
404 Require Import Arith.
405
406 Section constFold_ok.
407 Variable prog : program.
408
409 Theorem constFold_ok : forall rm is v,
410 run prog rm is v
411 -> forall rm', regmapCompat rm rm'
412 -> run prog rm (constFold rm' is) v.
413 Hint Resolve regmapCompat_set_None regmapCompat_set_Some.
414 Hint Constructors run.
415
416 cofix.
417 destruct 1; crush; eauto;
418 repeat match goal with
419 | [ H : regmapCompat _ _ |- run _ _ (match get ?RM ?R with Some _ => _ | None => _ end) _ ] =>
420 generalize (H R); destruct (get RM R); crush
421 end.
422 Qed.
423 End constFold_ok.
424
425 Print constFold_ok.