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

Question

我正在尝试确切地了解证明程序正确的含义。我从头开始，一直忙于第一步/主题介绍。

在关于总函数式编程的this paper 中，给出了斐波那契函数的两个定义。传统的：

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)

到目前为止，这也没有帮助。谁能告诉我如何进行感应？或链接到显示证明的页面（我搜索过，找不到任何东西）。

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

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 的尾递归版本。

Answer 3

我相信使用Strong Induction 会更容易识别您的证明：

...在第二步中，我们不仅可以假设该陈述对 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。

抱歉，这不是更有说服力，我已经 年 做了真正的证明。

Answer 4

如果论文说它相当于

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

我们应该从证明这一点开始。这里的关键是使用 generalized 归纳，即跟踪你的 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

顺便说一句，如果您对这类事情感兴趣，我建议您查看 Benjamin Pierce 关于“软件基础”的免费书籍。它是使用 Coq 证明助手的编程语言课程的教科书。 Coq 就像一个更丑、更卑鄙、更强大的 Haskell，它可以让你证明你的函数的属性。做真正的数学（证明四色定理）已经足够了，但最自然的事情是证明正确的函数程序。我觉得让电脑检查我的工作真是太好了。而且，Coq 中的所有函数都是总的......

Answer 5

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