Две разные функции Фибоначчи эквивалентны

я пытаюсь точно понять, что значит доказать правильность программы. Начинаю с нуля и зацикливаюсь на первых шагах / введении в тему.

В этой статье по полному функциональному программированию даны два определения функции Фибоначчи. Традиционная:

fib 0 = 0
fib 1 = 1
fib n = fib (n-1) + fib (n-2)
--fib (n+2) = fib (n+1) + fib (n+2) --The definition as given in the paper 
                                    --It seems incorrect to me. Typo?

и хвостовая рекурсивная версия, которую я никогда раньше не видел:

fib' n = f n 0 1
f 0 a b = a
f n a b = f (n-1) b (a+b)

Затем в статье утверждалось, что «просто» доказать по индукции, что обе функции возвращают один и тот же результат для всех положительных целых чисел n. Я впервые подумал об анализе подобных программ. Довольно интересно думать, что вы можете доказать, что две программы эквивалентны, поэтому я сразу же попытался провести это доказательство по индукции. Либо мои математические навыки заржавели, либо задача на самом деле не так проста.

Я доказал для n = 1

fib' 1 = f 1 0 1
       = f 0 1 1
       = 1
fib 1  = 1 (By definition)
therefore
fib' n = fib n for n = 1

Я сделал предположение о n = k

fib' k  = fib k
f k 0 1 = fib k

Я начинаю пытаться доказать, что если предположение верно, то функции также эквивалентны для n = k + 1 (и, следовательно, они эквивалентны для всех n> = 1 QED)

fib' (k+1)  = fib (k+1)
f (k+1) 0 1 = fib k + fib (k-1)

Я пробовал различные манипуляции, заменяя предположение в нужное время и так далее, но я просто не могу заставить LHS равняться RHS и, следовательно, доказать, что функции / программы эквивалентны.Что мне не хватает? В статье упоминается, что эта задача эквивалентна доказательству

f n (fib p) (fib (p+1)) = fib (p+n)

по индукции для произвольного p. Но я вообще не понимаю, как это правда. Как авторы пришли к этому уравнению? Это действительное преобразование уравнения, только если p = 0 . Я не понимаю, как это работает для произвольного p. Чтобы доказать это для произвольного p, вам потребуется пройти еще один уровень индукции. Конечно, правильная формула, которую нужно доказать, была бы

fib' (n+p)  = fib (n+p)
f (n+p) 0 1 = fib (n+p)

Пока это тоже не помогло. Может ли кто-нибудь показать мне, как будет проводиться индукция? Или ссылку на страницу, которая показывает доказательство (я искал, ничего не нашел).