How to check my implementation of a function which generates an infinite list?

Question

Write a function that takes the function f and the number n and returns the list [f n, f (n + 1), f (n + 2), f (n + 3), f (n + 4) ... ].

Here is my solution:

func f n = f n : func f (n+1)

But I'm not sure that it is correct. How can I check my implementation?

Answer 1

You can give a co-inductive proof. Co-inductive reasoning is similar to inductive reasoning, but it allows for "infinite" structures. It's a natural choice for reasoning about things like data streams and infinite lists.

The property you want func to have is something like

∀ f : Int -> a, ∀ n : Int, ∀ i : Int, (i >= 0 ⟹ (func f n) !! i == f (n + i))

Proving something by co-induction is similar to induction: you assume it as a co-inductive hypothesis for all substructures, and then prove it for the superstructure. Since there is only one definition for func, there is only only such proof obligation.

This means that, if you could prove

∀ f : Int -> a, ∀ n : Int, ∀ i : Int, (i ≥ 0 ⟹ (func f n) !! i == f (n + i))
⟹
∀ f : Int -> a, ∀ n : Int, ∀ i : Int, (i ≥ 0 ⟹ (f n : (func f (n + 1))) !! i == f (n + i))

then you would prove that your function definition is correct.

Since you could actually prove the above statement, your function definition is correct.