The Coq mailing list

[julien forest <forest AT ensiie.fr>]

Dear Paul, 

On Sun, 11 Jul 2010 14:28:39 -0500
Paul Tarau 
<paul.tarau AT gmail.com>
 wrote:

> 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)"
At this point, this probably only means that coq found that n is the
only POSSIBLE decreasing 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".
No, for structural induction coq (mostly) only accepts recursive
definitions which recurse only on syntactically smaller arguments. Here
buggy can only recurse on n. 

The fact that (half n) is smaller than n is not so obvious and in fact
needs an inductive proof. Coq cannot guess this for you and thus you
cannot use structural fixpoint to define such a function. 

You can use non structural induction to define buggy (Function or
Program Fixpoint). 

For example, the following code will work fine and define the
function (I added a call to functionnal induction to show the
advantages on using Function):
 
Require Import Bool.

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

Function half (n  : nat) : nat :=
  match n with
  | O => 0
  | S O => 0
  | S (S x) => S (half x)
  end.
Require Import Recdef.
Require Import Arith.

Lemma half_decrease : 
  forall n, half n <= n. 
Proof.
  intros n.
  functional induction (half n);
  auto with arith.
Qed.

Function buggy (n:nat) {measure (fun n => n) n} : nat :=
match n with
| 0 => 0
| S n => if isEven n then 0 else S (buggy (half n))
end.
Proof.
  intros n n' H1 H2.
  apply le_lt_trans with n'.
  apply half_decrease.
  auto with arith.
Qed.


> 
> Can anyone suggest a simple workaround to the problem?
> 

Hope this help,
Regards, 
Julien