# HG changeset patch # User Adam Chlipala # Date 1223815463 14400 # Node ID 32a5ad6e2bb0d6e57b3293b53da5b26b4c7ba0c7 # Parent 22f111d5cda2dfb8cfc8c3c5c023594ecd34bd06 s/stream/tree diff -r 22f111d5cda2 -r 32a5ad6e2bb0 src/Coinductive.v --- a/src/Coinductive.v Wed Oct 08 14:22:47 2008 -0400 +++ b/src/Coinductive.v Sun Oct 12 08:44:23 2008 -0400 @@ -465,8 +465,8 @@ %\item%#
  • # 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.#
  • # %\item%#
  • # Define a function [everywhere] for building a tree with the same data value at every node.#
  • # %\item%#
  • # 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.#
  • # - %\item%#
  • # Define a stream [falses] where every node has the value [false].#
  • # - %\item%#
  • # 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.#
  • # + %\item%#
  • # Define a tree [falses] where every node has the value [false].#
  • # + %\item%#
  • # 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.#
  • # %\item%#
  • # 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.#
  • # ##%\end{enumerate}% ##