The Coq mailing list

[Paul Tarau <paul.tarau AT gmail.com>]

Dear Coq users,

When trying to port some simple code from Haskell to Coq
I have noticed that it does not propagate what it knows
about a function ("half" in the following example) to
another function ("buggy" in the example).

Require Import Bool.

Fixpoint isEven (n: nat) {struct n} : bool :=
match n with
| 0 => true
| 1 => false
| S (S n) => isEven n
end.

Fixpoint half (n  : nat) : nat :=
  match n with
  | O => 0
  | S O => 0
  | S (S x) => S (half x)
  end.

Fixpoint buggy (n:nat) {struct n} : nat :=
match n with
| 0 => 0
| S n => if isEven n then 0 else S (buggy (half n))
end.

After graciously saying that
"half is recursively defined (decreasing on 1st argument)"
it complains that
"Recursive call to buggy has principal argument equal to
"half n0" instead of n0"

The system clearly knows that "S n" decreases to "n" and it
is also acknowledging that "half is decreasing" but it does
not seem to connect the dots and accept "half n"
as an argument in the recursive call to "buggy".

Can anyone suggest a simple workaround to the problem?

I have high hopes that it should exist, because, I guess, otherwise this would
have been fixed :-)

Paul Tarau