The Coq mailing list

[Bruno Barras <Bruno.Barras AT inria.fr>]

Hi Pablo,

> 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 ?


The order you need is a lexicographic order on (l,nb). Your definition
requires two embedded fixpoints, one on l, the other one on nb (note
the new syntax of Fix):

Fixpoint AuxDeCode [l:(list nat)] : nat->nat->(list Alphabet)-> Descriptor :=
 Fix ADC{ADC [na,nb:nat]: (list Alphabet)->Descriptor :=
  [m]
  Cases l of
    nil           => (mkD l na nb (rev m))
  | (cons x rl)   =>
       if (Equal_nat x nb) then (AuxDeCode rl (pred na) nb (cons a m))
       else Cases nb of
              O       => (mkD l na nb (rev m))
            | (S pnb) => (ADC na pnb (cons b m))
            end
  end}.


You can also put the fixpoint deeper, to allow Case reductions on l,
when nb is not in constructor form, but you have to take care that m
changes along the recursives calls (while na changes only when l
does). You have to abstract and apply both nb and m:

Fixpoint AuxDeCode [l:(list nat)] : nat->nat->(list Alphabet)-> Descriptor :=
 [na;nb;m]
  Cases l of
    nil           => (mkD l na nb (rev m))
  | (cons x rl)   =>
    (Fix ADC{ADC [nb:nat]: (list Alphabet)->Descriptor :=
      [m]if (Equal_nat x nb) then (AuxDeCode rl (pred na) nb (cons a m))
         else Cases nb of
                O       => (mkD l na nb (rev m))
              | (S pnb) => (ADC pnb (cons b m))
              end} nb m)
  end.

In both case, you can prove the fixpoint equation you wanted initially:

Goal (l:(list nat))(na,nb:nat)(m:(list Alphabet))
 (AuxDeCode l na nb m)
 =(Cases l of
     nil           => (mkD l na nb (rev m))
   | (cons x rl)   =>
        if (Equal_nat x nb) then (AuxDeCode rl (pred na) nb (cons a m))
        else
           Cases nb of
             O       => (mkD l na nb (rev m))
           | (S pnb) => (AuxDeCode l na pnb (cons b m))
           end
   end).
Destruct l; Destruct nb; Reflexivity.
Save.

Since nb is used in (Equal_nat x nb), you cannot put the second Fix
deeper. This one is wrong, and you cannot prove the equation:

Fixpoint AuxDeCode [l:(list nat)] : nat->nat->(list Alphabet)-> Descriptor :=
 [na;nb;m]
  Cases l of
    nil           => (mkD l na nb (rev m))
  | (cons x rl)   =>
      if (Equal_nat x nb) then (AuxDeCode rl (pred na) nb (cons a m))
      else (Fix ADC{ADC [nb:nat]: (list Alphabet)->Descriptor :=
            [m]Cases nb of
                O       => (mkD l na nb (rev m))
              | (S pnb) => (ADC pnb (cons b m))
              end} nb m)
  end.



Bruno Barras.

-- 
  Projet Coq - INRIA Rocquencourt
  tel : +33 1 39 63 53 16
  
mailto:Bruno.Barras AT inria.fr
  http://pauillac.inria.fr/~barras