Coq：斐波那契的递归定义是病态的答案

【问题标题】：Coq: Recursive definition of fibonacci is ill-formedCoq：斐波那契的递归定义是病态的
【发布时间】：2021-05-30 05:52:39
【问题描述】：

我正在尝试使用 coq 定义斐波那契数。这是我的代码：

Fixpoint fibonacci (n:nat) : nat :=
       match n with
         | O => 1
         | S O => 1
         | S (S n') => fibonacci (S n') + fibonacci n
       end.

我遇到了错误信息：

斐波那契的递归定义格式不正确。在环境中 fibonacci : nat -> nat n : nat n0 : nat n' : nat 递归调用 fibonacci 的主要参数等于“S n'”，而不是其中之一以下变量：“n0”“n'”。递归定义是：“fun n : nat => 匹配 n 与 | S (S n') => 斐波那契 (S n') + 斐波那契 n | _ => 1 结束”。

我想知道为什么这是错误的。顺便说一句，在匹配的第三个子句中，我没有定义n'的属性（例如n'：nat），那么n'的属性的默认值是什么？

提前致谢！

【问题讨论】：

标签： coq fibonacci

【解决方案1】：

递归调用的所有参数在结构上必须是递减的，也就是说，您必须在匹配中去掉一个构造函数符号。在您的情况下， (S n') 参数实际上在结构上是递减的，但 Coq 没有检测到这一点（这有点傻），因为您添加了另一个构造函数 S，这是不允许的。第二个参数是错误的，应该是n'。除此之外，通常会这样定义fibonacci 0 = 0。

为了解决(S n') 的问题，可以使用as 给它一个单独的名称，如下所示：

Require Import List.

Fixpoint fibonacci (n:nat) : nat :=
       match n with
         | O => 0
         | S O => 1
         | S (S O) => 1
         | S ((S n'') as n')=> fibonacci n' + fibonacci n''
       end.

Eval cbv in map fibonacci (seq 0 10).

【讨论】：

为什么需要S (S 0) => 1 子句？这不是多余的吗？
确实是多余的，去掉也没什么损失。
对我（个人而言）它会失去一些清晰性，因为对我来说，斐波那契数列定义为fib(1)=1、fib(2)=1、fib(n)=fib(n-1)+fib(n-2)，而0 是一种可以添加额外的案例（或必须为 Coq nat 添加）。这可能是一代人的事情——我看到今天很多人将斐波那契数列定义为从 0 开始。所以我会考虑将这种情况作为一种技术优化来掩盖定义，但我认为这是值得商榷的。