Coq: Recursive definition of fibonacci is ill-formed

Question

I am trying to define Fibonacci numbers using coq. This is my code:

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

I met the error message:

Recursive definition of fibonacci is ill-formed. In environment fibonacci : nat -> nat n : nat n0 : nat n' : nat Recursive call to fibonacci has principal argument equal to "S n'" instead of one of the following variables: "n0" "n'". Recursive definition is: "fun n : nat => match n with | S (S n') => fibonacci (S n') + fibonacci n | _ => 1 end".

I am wondering why this is wrong. Parenthetically, in the third clause of the match, I did not define the property of n' (e.g. n': nat), what would be the default of the property of n'?

Thanks in advance!

M Soegtrop M Soegtrop · Accepted Answer · 2021-05-30T07:05:29

All arguments of a recursive call must be structurally decreasing, that is you must strip away one constructor symbol in the match. In your case the (S n') argument is in fact structurally decreasing, but Coq doesn't detect that (which is a bit silly) because you add another constructor S, which is not allowed. The second argument is wrong and should probably be n'. Besides one usually defines this such that fibonacci 0 = 0.

To get around the issue of (S n') one gives it a separate name with as as in:

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).

Coq: Recursive definition of fibonacci is ill-formed

1 Answers