展示两个不同的斐波那契函数是等价的。

Question

我正在尝试学习证明程序正确的确切含义。我从零开始，但在第一步/主题介绍上遇到了困难。

在这篇关于完全函数式编程的论文中，给出了斐波那契函数的两个定义。传统的定义如下：

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)

我尝试了各种操作，适时替换假设等，但我就是无法使左边等于右边，从而证明这些函数/程序是等价的。我错过了什么？论文提到这个任务等同于证明

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)

到目前为止，这并没有起到帮助的作用。有人可以向我展示如何进行归纳吗？或者链接到一个显示证明的页面（我搜索过，但找不到任何信息）。

- TheIronKnuckle

---

fib (n+2) = fib (n+1) + fib (n+2) 显然是个打字错误，他们可能想表达的是 fib (n+2) = fib (n+1) + fib n ，这是数学上正确的，但将被从有效的 Haskell 中移除。http://hackage.haskell.org/trac/haskell-prime/wiki/RemoveNPlusK - Philip JF

你可能会对这个感兴趣：http://www.ats-lang.org/EXAMPLE/#FIBexample -- 这是一个使用定理证明编程的例子（用于斐波那契函数）。还要注意，在那里给出的Fib规范是归纳的，但实现是尾递归的，并且被证明符合规范。 - Artyom Shalkhakov

Answer 1

在Agda中，pad证明的机器检查版本：

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

- Rotsor

Answer 2

我无法访问上述论文，但他们的广义定理是一种不错的方法。在 f n 0 1 中使用数字 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 的尾递归版本。

- pad

Answer 3

我相信使用强归纳法会更容易理解：

... 在第二步中，我们不仅可以假设该命题对于n=m成立，还可以假设该命题对于所有小于或等于m的n都成立。

您在这里卡住了：

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

部分原因是你需要同时拥有从k+1到k的步骤，以及k+1到k-1的步骤。

很抱歉这并不太令人信服，我已经好几年没有做过真正的证明了。

- sarnold

Answer 4

如果这篇论文说它相当于

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

我们首先需要证明这一点。关键在于使用广义归纳法，即要注意你的全称量词。

首先我们展示：

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证明助手。 Coq像Haskell，但更强大，可以证明函数的属性。 它足以进行实际数学（四色定理的证明），但最自然的事情是证明正确的函数程序。 我发现让计算机检查我的工作很好。 而且，Coq中的所有函数都是完全的...

- Philip JF

Answer 5

有时候不太正式的开始可能是个好主意。我认为，一旦你看到尾递归版本只是简单地在每一步中传递F(n-2)和F(n-1)以避免重新计算，这就给了你一个证明的想法，然后你可以将其形式化。

- Ingo