Отображение двух различных функций фибоначчи эквивалентно

Ответ 1

Я не мог получить доступ к вышеупомянутой статье, но их обобщенная теорема - хороший способ. Два значения 0 и 1 в f n 0 1 звучат как магические числа; однако, если вы обобщите их на числа Фибоначчи, доказательство гораздо проще провести.

Чтобы избежать путаницы при чтении доказательства, fib k записывается как F(k), а некоторые ненужные круглые скобки также удаляются. Мы имеем обобщенную теорему: forall k. fib' n F(k) F(k+1) = F(k+n) и докажем ее индукцией по n.

Базовый регистр с n = 1:

fib' 1 F(k) F(k+1) = F(k+1) // directly deduce from definition of fib'

Индуктивный шаг:

У нас есть предположение индукции где:

forall k. fib' n F(k) F(k+1) = F(k+n)

И мы должны доказать:

forall k. fib' (n+1) F(k) F(k+1) = F(k+(n+1))

Доказательство начинается с левой части:

fib' (n+1) F(k) F(k+1)
= fib' n F(k+1) (F(k) + F(k+1)) // definition of fib'
= fib' n F(k+1) F(k+2) // definition of F (or fib)
= F((k+1)+n) // induction hypothesis
= F(k+(n+1)) // arithmetic

Мы завершили обобщенное доказательство. Ваш пример также доказан, потому что это конкретный случай вышеупомянутой теоремы с k=0.

В качестве побочного примечания fib' не странно; это хвостовая рекурсивная версия fib.

Ответ 2

Проверенная машиной версия прокладки в Агда:

module fibs where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

fib : ℕ → ℕ
fib 0 = 0
fib 1 = 1
fib (suc (suc n)) = fib n + fib (suc n)

f : ℕ → ℕ → ℕ → ℕ
f 0 a b = a
f (suc n) a b = f n b (a + b)

fib' : ℕ → ℕ
fib' n = f n 0 1

-- Exactly the theorem the user `pad` proposed:
Theorem : ℕ → Set
Theorem n = ∀ k → f n (fib k) (fib (suc k)) ≡ fib (k + n)

-- Helper theorems about natural numbers:
right-identity : ∀ k → k ≡ k + 0
right-identity zero = refl
right-identity (suc n) = cong suc (right-identity n)

1+m+n≡m+1+n : ∀ n k → suc (n + k) ≡ n + suc k
1+m+n≡m+1+n zero k = refl
1+m+n≡m+1+n (suc n) k = cong suc (1+m+n≡m+1+n n k)

-- The base case. 
-- Theorem 0 by definition expands to (∀ k → fib k ≡ fib (k + 0))
-- and we prove that using the right-identity theorem.
th-base : Theorem 0
th-base k = cong fib (right-identity k)

-- The inductive step.
-- The definitions are expanded automatically, so (Theorem (suc n)) is
--   (∀ k → f n (fib (suc k)) (fib (suc (suc k))) ≡ fib (k + suc n))
-- We can apply the induction hypothesis to rewrite the LHS to 
--   (fib (suc k + n))
-- which is equal to the RHS by the 1+m+n≡m+1+n theorem.
th-step : ∀ n → Theorem n → Theorem (suc n)
th-step n hyp k = trans (hyp (suc k)) (cong fib (1+m+n≡m+1+n k n))

-- The inductive proof of Theorem using th-base and th-step.
th : ∀ n → Theorem n
th zero = th-base
th (suc n) = th-step n (th n)

-- And the final proof:
fibs-equal : ∀ n → fib' n ≡ fib n
fibs-equal n = th n 0

Ответ 3

Я считаю, что ваше доказательство будет легче распознать с помощью Сильная индукция:

... на втором шаге мы можем предположить не только, что оператор выполняется для n = m, но также и для всех n, меньших или равных m.

Вы застряли здесь:

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

.. отчасти потому, что вам нужно иметь оба шага от k+1 до k, а также от k+1 до k-1.

Извините, что это не более убедительно, прошло много лет с тех пор, как я сделал реальные доказательства.

Ответ 4

Если в документе сказано, что это эквивалентно

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

мы должны начать с доказательства этого. Ключевым моментом здесь является использование обобщенной индукции, т.е. Отслеживание ваших кванторов forall.

Сначала покажем, что

forall p, f 0 (fib p) (fib (p+1)) = fib p = fib (p + 0)

Теперь предположим, что индуктивное предположение

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

и покажите

forall p, f (n+1) (fib p) (fib (p+1)) = f n (fib (p+1)) (fib (p+1) + fib p)
                                      = f n (fib (p+1)) (fib (p + 2)) --By def of fib
                                      = fib ((p + 1) + n) --By induction hypothesis
                                      = fib (p + (n+1))

Итак, это показывает лемму.

Это позволяет легко доказать свою цель. Если у вас есть

fib' n = f n 0 1
       = f n (fib 0) (fib (0 + 1)) --by def of fib
       = fib (n + 1) --by lemma

Кстати, если вас это интересует, я предлагаю вам ознакомиться с бесплатной книгой Бенджамина Пирса "Основы программного обеспечения". Это учебник для курса по языкам программирования, в котором используется помощник Coq proof. Coq похож на уродливый, более сильный и более мощный Haskell, который позволяет вам доказывать свойства ваших функций. Это достаточно хорошо, чтобы сделать реальную математику (подтверждение четырехцветной теоремы), но наиболее естественной вещью в ней является проверенная правильная функциональная программа. Мне приятно, что компьютер проверяет мою работу. И все функции в Coq полны...

Ответ 5

Иногда неплохо начинать слишком формально. Я думаю, как только вы увидите, что рекурсивная версия хвоста просто пропускает F (n-2) и F (n-1) вокруг, чтобы избежать перерасчета на каждом шаге, это дает вам доказательную идею, которую вы затем формализуете.