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

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)

我尝试了各种操作，在正确的时间替换假设等等，但我就是无法让 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

我无法访问上述论文，但他们的广义定理是一个很好的方法。 fn 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

我相信使用强归纳你的证明会更容易识别：

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

我们应该从证明这一点开始。这里的关键是使用广义归纳法，即跟踪所有量词。

首先我们展示

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) 以避免在每个步骤中重新计算，这就会为您提供一个证明想法，然后将其形式化。