Search code examples
algorithmscalastreaminductionproof-of-correctness

Inductive proof on scala stream

Can someone help me with how to reason inductively that this scala code

lazy val y : Stream[Int] = 1 #:: (y map (_ + 1))

produces a list of natural numbers from 1 onwards?

Solution

  • The value at position in 1 #:: whatever is 1, so we know y(0) = 1.

    At a greater position we have y(n+1) = whatever(n). Here whatever is y map (_+1), so y(n+1) = (y map (_+1))(n).

    We want to prove forall n. y(n) = n + 1.

    We know this is true for n = 0, y(0) = 1

    (y.map(_+1))(n) is simply y(n) + 1. This is what map does. So our formula above becomes y(n+1) = y(n) + 1.

    Then trivially, if we know y(n) = n+1, then y(n+1) = (n+1) + 1. Result true at next rank. We get our proof by induction.