The Coq mailing list

[Taral <taralx AT gmail.com>]

On Wed, Dec 31, 2008 at 1:09 PM, Ashish Darbari
<ashish_darbariuk AT yahoo.co.uk>
 wrote:
> Is there a way to define functions like these (using Fixpoint) by
> providing a measure function like (length l1 + length l2) which will
> decrease in each call.

You want Program Fixpoint. But you still have to merge the recursive 
arguments:

Definition lsum (l : list Z * list Z) := match l with (l1, l2) =>
length l1 + length l2 end.

Program Fixpoint snarf (l: list Z * list Z) (acc:list Z) {measure lsum
l} : list Z :=
  match l with
    | (nil,_) => (acc)
    | (_,nil) => (acc)
    | ((x::xs),(y::ys)) =>
      match Z_eq_dec x y with
        | left _ => snarf (xs, ys) (x::acc)
        | right _ =>
          match Z_le_gt_dec x y with
            | left _ => snarf (xs, y::ys) (x::acc)
            | right _ => snarf (x::xs, ys) acc
      end
  end
end.

(Does anyone know why this breaks if the arguments are in the original
order? It appears to be a bug in Program.)

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown