[Haskell-beginners] Data.Stream interleave implementation question

[Bryan Brady]

On Wed, Feb 12, 2014 at 3:10 AM, Kim-Ee Yeoh <ky3 at atamo.com> wrote:

> I'd hazard to say that it's probably not the solution the author had in
> mind, so bonus points for novelty!
>

What solution do you think the author had in mind? He did hint to use
define and use interleaveStreams and to avoid checking divisibility
testing.


> How would you prove it correct though?
>

I haven't attempted this yet, but if I were to, I'd go for an inductive
proof. If you list the solution along with the numbers they correspond to
(divide), you get:
1 2 3 4 5 6 7 8 9 10...
0 1 0 2 0 1 0 3 0 1...

If you drop all the numbers corresponding to a 0 in the ruler function:
2 4 6 8 10...
1 2 1 3 1 ...

then drop the numbers corresponding to a 1 in the ruler function:
4 6 ...
2 3 ...

At each level, you drop every other number, and the first number of each
successive level is 1 greater than the previous level. Formalize that a bit
and you got a proof.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/beginners/attachments/20140212/263925bf/attachment.html>