Индуктивный доказательство на лестницу потока

Question

Может кто-то помочь мне с тем, как рассуждать индуктивно, что этот код Scala

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

производит список натуральных чисел от 1 года?

Answer 1

Величина в позиции 1 #:: whatever составляет 1, поэтому мы знаем y(0) = 1.

В большем положении у нас есть y(n+1) = whatever(n). Здесь whatever - y map (_+1), поэтому y(n+1) = (y map (_+1))(n).

Мы хотим доказать forall n. y(n) = n + 1.

Мы знаем, что это верно для n = 0, y(0) = 1

(y.map(_+1))(n) просто y(n) + 1. Это то, что делает карта. Таким образом, наша формула выше y(n+1) = y(n) + 1.

Тогда тривиально, если мы знаем y(n) = n+1, то y(n+1) = (n+1) + 1. Результат true в следующем ранге. Получим наше доказательство по индукции.