## Mercurial > cpdt > repo

### comparison src/Coinductive.v @ 478:f02b698aadb1

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Batch of changes based on proofreader feedback

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Sun, 11 Nov 2012 18:17:23 -0500 |

parents | 1fd4109f7b31 |

children | ed829eaa91b2 |

comparison

equal
deleted
inserted
replaced

477:6769ef9688f2 | 478:f02b698aadb1 |
---|---|

615 | 615 |

616 Theorem evalCmd_coind : forall vs1 c vs2, R vs1 c vs2 -> evalCmd vs1 c vs2. | 616 Theorem evalCmd_coind : forall vs1 c vs2, R vs1 c vs2 -> evalCmd vs1 c vs2. |

617 cofix; intros; destruct c. | 617 cofix; intros; destruct c. |

618 rewrite (AssignCase H); constructor. | 618 rewrite (AssignCase H); constructor. |

619 destruct (SeqCase H) as [? [? ?]]; econstructor; eauto. | 619 destruct (SeqCase H) as [? [? ?]]; econstructor; eauto. |

620 destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; | 620 destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; econstructor; eauto. |

621 [ econstructor | econstructor 4 ]; eauto. | |

622 Qed. | 621 Qed. |

623 End evalCmd_coind. | 622 End evalCmd_coind. |

624 | 623 |

625 (** 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]. *) | 624 (** Now that we have a co-induction principle, we should use it to prove something! Our example is a trivial program optimizer that finds places to replace [0 + e] with [e]. *) |

626 | 625 |

642 | 641 |

643 (* begin thide *) | 642 (* begin thide *) |

644 Lemma optExp_correct : forall vs e, evalExp vs (optExp e) = evalExp vs e. | 643 Lemma optExp_correct : forall vs e, evalExp vs (optExp e) = evalExp vs e. |

645 induction e; crush; | 644 induction e; crush; |

646 repeat (match goal with | 645 repeat (match goal with |

647 | [ |- context[match ?E with Const _ => _ | Var _ => _ | 646 | [ |- context[match ?E with Const _ => _ | _ => _ end] ] => destruct E |

648 | Plus _ _ => _ end] ] => destruct E | |

649 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E | 647 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E |

650 end; crush). | 648 end; crush). |

651 Qed. | 649 Qed. |

652 | 650 |

653 Hint Rewrite optExp_correct . | 651 Hint Rewrite optExp_correct. |

654 | 652 |

655 (** 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. *) | 653 (** The final theorem is easy to establish, using our co-induction principle and a bit of Ltac smarts that we leave unexplained for now. Curious readers can consult the Coq manual, or wait for the later chapters of this book about proof automation. At a high level, we show inclusions between behaviors, going in both directions between original and optimized programs. *) |

656 | 654 |

657 Ltac finisher := match goal with | 655 Ltac finisher := match goal with |

658 | [ H : evalCmd _ _ _ |- _ ] => ((inversion H; []) | 656 | [ H : evalCmd _ _ _ |- _ ] => ((inversion H; []) |