The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hello,

  Adam's final remark is perfectly right :
"
(This would even lead to cleaner code that's easier to understand, which 
is not the usual case when someone hits a problem with termination 
checking. ;]) "



Even if your definition were accepted by Coq, it doesn't formalize what 
is suggested
by its name.

For instance, let's make coq accept your function through a measure 
argument.

Require Import List.
Definition natlist := list nat.


Fixpoint m (l : list nat) :=
  match l with nil => 0
             | n::l' => S n + m l'
  end.

Require Import Recdef.

Function oddmembers (l:natlist) {measure m l} : natlist :=
  match l with
    | nil =>nil
    | h :: t =>
      match h with
        | 0 => oddmembers t
        | 1 => 1 :: (oddmembers t)
        | S (S h') =>  oddmembers (h' :: t)
      end
  end.
intros.
simpl;auto with arith.
simpl;intros;auto with arith.
simpl ;intros;auto with arith.
Defined.

Eval vm_compute in oddmembers (1::3::4::5::nil).
(*
   = 1 :: 1 :: 1 :: nil
     : natlist
*)

As Adam writes, its better to separate the oddity check and the 
recursion scheme.

Pierre




Le 07/03/2010 17:55, Adam Chlipala a écrit :
> Z wrote:
> > Could you please tell me why this program has a syntax error with 
> > this message
> > "Recursive definiton ill-formed"? Maybe the syntax of recursive 
> > function in Coq is not like
> > ML etc?
> >
> > Thanks in advance.
> >
> > ------------------------
> > Fixpoint oddmembers (l:natlist) : natlist :=
> >   match l with
> >     | nil =>nil
> >     | h :: t =>
> >       match h with
> >         | 0 => oddmembers t
> >         | 1 => 1 :: (oddmembers t)
> >         | S (S h') =>  oddmembers (h' :: t)
> >       end
> >   end.
> > --------------------
>
> Your definition isn't obviously terminating; that is, the simple rule 
> of primitive recursion doesn't show that it always terminates.  All 
> Coq programs must terminate.  Therefore, to get Coq to accept your 
> definition, you would have to use an explicit termination argument.
>
> I believe this trouble is easy to avoid in your specific example, by 
> using an auxiliary recursive function for deciding evenness.  (This 
> would even lead to cleaner code that's easier to understand, which is 
> not the usual case when someone hits a problem with termination 
> checking. ;])