comparison src/Coinductive.v @ 200:df289eb8ef76

Small fixes while reading student solutions
author Adam Chlipala <adamc@hcoop.net>
date Fri, 02 Jan 2009 08:57:25 -0500
parents 32a5ad6e2bb0
children 8caa3b3f8fc0
comparison
equal deleted inserted replaced
199:cadeb49dc1ef 200:df289eb8ef76
465 %\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># 465 %\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>#
466 %\item%#<li># Define a function [everywhere] for building a tree with the same data value at every node.#</li># 466 %\item%#<li># Define a function [everywhere] for building a tree with the same data value at every node.#</li>#
467 %\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># 467 %\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>#
468 %\item%#<li># Define a tree [falses] where every node has the value [false].#</li># 468 %\item%#<li># Define a tree [falses] where every node has the value [false].#</li>#
469 %\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># 469 %\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>#
470 %\item%#<li># Prove that [true_falses] 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># 470 %\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>#
471 #</ol>#%\end{enumerate}% #</li># 471 #</ol>#%\end{enumerate}% #</li>#
472 472
473 #</ol>#%\end{enumerate}% *) 473 #</ol>#%\end{enumerate}% *)