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

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