comparison src/Coinductive.v @ 370:549d604c3d16

Move exercises out of mainline book
author Adam Chlipala <adam@chlipala.net>
date Fri, 02 Mar 2012 09:58:00 -0500
parents dc99dffdf20a
children d1276004eec9
comparison
equal deleted inserted replaced
369:4550dedad73a 370:549d604c3d16
636 end; crush; eauto 10. 636 end; crush; eauto 10.
637 Qed. 637 Qed.
638 (* end thide *) 638 (* end thide *)
639 639
640 (** 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 %\texttt{%#<tt>#if#</tt>#%}%; the same proof should continue working, after the co-induction principle is extended to the new evaluation rules. *) 640 (** 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 %\texttt{%#<tt>#if#</tt>#%}%; the same proof should continue working, after the co-induction principle is extended to the new evaluation rules. *)
641
642
643 (** * Exercises *)
644
645 (** %\begin{enumerate}%#<ol>#
646
647 %\item%#<li># %\begin{enumerate}%#<ol>#
648 %\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>#
649 %\item%#<li># Define a function [everywhere] for building a tree with the same data value at every node.#</li>#
650 %\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>#
651 %\item%#<li># Define a tree [falses] where every node has the value [false].#</li>#
652 %\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>#
653 %\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>#
654 #</ol>#%\end{enumerate}% #</li>#
655
656 #</ol>#%\end{enumerate}% *)