The Coq mailing list

[Pablo.Argon AT lan10.ec-nantes.fr (Pablo ARGON)]

Hello all,
        I have a rather "classical" problem defining a Fixpoint: 
a not well-formed error.

Because of the syntactical constraint of fixpoint definition, I can
define a recursive function which decreases sometimes one argument,
sometimes other one at each call, i.e. I know that it eventually ends.
A well-known example of such an algorithm is list merge (of two sorted
list).

My question is: there some "general transformation" to make this
class of algorithms acceptable by Coq ?

At the end of this mail you will find my problematic AuxDeCode function with
some extra definitions.

NB: I tried to transform my function using a recipe given by 
Christine Paulin for the ackerman function 
(cf. coq-list, Subject: Re: Fixpoint vs Recursive Definition)
but I didn't success...

Thanks in advance!
        Pablo Argon

Miscelaneous question: 
---quotation-----------------------------------------------------------------

>From 
>Benjamin.Werner AT inria.fr
>  Tue May  5 22:02:33 1998
Date: Tue, 5 May 1998 18:56:37 +0200 (MET DST)

The Reference Manual for Coq V6.2 has been updated and reorganised,
the chapters concerning syntactic extensions and customized
tactics have been completely rewritten. The documentation is also=20
available in html format. Both versions of the documentation are still
in draft format. =20
-----------------------------------------------------------------------------

Where can I find the html format documentation ?

>>>COQ code (6.2)<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
Require PolyList.

Inductive Alphabet :Set := a : Alphabet | b : Alphabet.
Record Descriptor : Set := mkD { l : (list nat) ; na : nat;
                             nb : nat ; m : (list Alphabet)}.

Fixpoint Equal_nat [m:nat; n:nat]: bool :=
 Cases m of
   O=> Cases n of
        O   => true
        | _ => false
       end
  | (S pm)=> Cases n of
        O   => false
        |(S pn)=>(Equal_nat pm pn)
           end
end.

Fixpoint AuxDeCode [l:(list nat);na,nb:nat] : (list Alphabet)-> Descriptor :=
  [m:(list Alphabet)]
  Cases l of
        nil           => (mkD l na nb (rev m))
       |(cons x rl)   => Cases (Equal_nat x nb) of
                           true  => (AuxDeCode rl (pred na) nb        (cons a 
m))
                          |false =>  Cases nb of
                                          O=> (mkD l na nb (rev m))
                                         |(S pnb)=> (AuxDeCode l  na   pnb  
(cons b m))
                                     end
                         end
      end.
>>>end COQ code<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<