The Coq mailing list

[Andrew Pennebaker <andrew.pennebaker AT gmail.com>]

I rewrote fib as:

Fixpoint fib (n : nat) : nat :=
match n with

| O => O
| S O => one

| _ => plus (fib (minus n one)) (fib (minus n two))
end.

Now the error is

Error:
Recursive definition of fib is ill-formed.
In environment
fib : nat -> nat
n : nat
n0 : nat
n1 : nat
Recursive call to fibber has principal argument equal to
"minus n one" instead of one of the following variables:
"n0" "n1".
Recursive definition is:
"fun n : nat =>
 match n with
 | O => O
 | S O => S O
 | S (S _) => plus (fib (minus n one)) (fib (minus n two))
 end".

Cheers,

Andrew Pennebaker

www.yellosoft.us

On Thu, Nov 3, 2011 at 3:23 PM, Vincent Siles <vincent.siles AT ens-lyon.org> wrote:

one on the left of => is not considered as the definition you gave, it
is understood as a pattern variable.
You should have a warning "Warning: pattern one is understood as a
pattern variable".
This there is no constructor, just a variable, it will capture all the
remaining cases.
As a consequence, the last clause is redundant.

You should put S O instead of one on the left of =>.

By the way, your function is not recursive (the recursive calls are
not done on subterms of n

Best,
V.

2011/11/3 Andrew Pennebaker <andrew.pennebaker AT gmail.com>:

> I'm following the Software Foundations tutorial, and I decided to write a
> fibonacci function.
>
> Inductive nat : Set :=
> | O : nat
> | S : nat -> nat.
>
> Fixpoint plus (n m : nat) : nat :=
> match n with
> | O => m
> | S n' => S (plus n' m)
> end.
>
> Fixpoint mult (n m : nat) : nat :=
> match n with
> | O => O
> | S n' => plus m (mult n' m)
> end.
>
> Definition one : nat := S O.
> Definition two : nat := S(S O).
>
> Fixpoint minus (n m : nat) : nat :=
> match n, m with
> | O, _ => O
> | S _, O => n
> | S n', S m' => minus n' m'
> end.
>
> Fixpoint fib (n : nat) : nat :=
> match n with
> | O => O
> | one
> | _ => plus (fib (minus n one)) (fib (minus n two))
> end.
>
> When I tell CoqIDE to go forward with the fib function, it reports "Error:
> This clause is redundant", and underlines the last case in fib:
>
> _ => plus (fib (minus n one)) (fib (minus n two))
>
> What am I doing wrong?
>
> Cheers,
> Andrew Pennebaker
> www.yellosoft.us