Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] connecting the dots between Fixpoint definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] connecting the dots between Fixpoint definitions


chronological Thread 
  • From: julien forest <forest AT ensiie.fr>
  • To: Paul Tarau <paul.tarau AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] connecting the dots between Fixpoint definitions
  • Date: Sun, 11 Jul 2010 23:25:48 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:date:from:to:cc:subject:message-id:in-reply-to:references :x-mailer:mime-version:content-type:content-transfer-encoding; b=M/O987L6vDZuoFPWIe26KszIR5BOqukj/oLP7HIryjZsod9VrRKCyMwhkd7hTXrj+a XxWbnlCoSb7hwh0/bFeEacx/o+rPTAo2MePtb9iOudLxPL0GLm1z+hakAhwcDkU+qtD4 g9Oo7YBMnMs2j05QfFtQhdqEnzg2ELMHTm+F0=

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




Archive powered by MhonArc 2.6.16.

Top of Page