Mercurial > cpdt > repo
comparison src/Coinductive.v @ 81:f295a64bf9fd
Coinductive exercise description
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 05 Oct 2008 11:34:09 -0400 |
| parents | 943478e5a32d |
| children | cde1351d18bb |
comparison
equal
deleted
inserted
replaced
| 80:506a06118014 | 81:f295a64bf9fd |
|---|---|
| 453 End constFold_ok. | 453 End constFold_ok. |
| 454 | 454 |
| 455 (** 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. *) | 455 (** 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. *) |
| 456 | 456 |
| 457 Print constFold_ok. | 457 Print constFold_ok. |
| 458 | |
| 459 | |
| 460 (** * Exercises *) | |
| 461 | |
| 462 (** %\begin{enumerate}%#<ol># | |
| 463 | |
| 464 %\item%#<li># %\begin{enumerate}%#<ol># | |
| 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># | |
| 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 stream [falses] where every node has the value [false].#</li># | |
| 469 %\item%#<li># Define a stream [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># | |
| 471 #</ol>#%\end{enumerate}% #</li># | |
| 472 | |
| 473 #</ol>#%\end{enumerate}% *) |