Вы можете дать коиндуктивное доказательство. Коиндуктивное мышление похоже на индуктивное мышление, но оно допускает «бесконечные» структуры. Это естественный выбор для рассуждений о вещах, таких как потоки данных и бесконечные списки.
Свойство, которое вы хотите иметь func, выглядит примерно так:
∀ f : Int -> a, ∀ n : Int, ∀ i : Int, (i >= 0 ⟹ (func f n) !! i == f (n + i))
Доказательство чего-либо путем коиндукции аналогично для индукции: вы принимаете это как коиндуктивную гипотезу для всех подструктур, а затем доказываете это для надстройки. Поскольку существует только одно определение для func, существует только такое обязательное доказательство.
Это означает, что, если бы вы могли доказать
∀ 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))
, то вы бы доказали, что определение вашей функции является правильным.
Поскольку вы действительно можете доказать приведенное выше утверждение, определение вашей функции является правильным.