The Coq mailing list

[Ashish Darbari <ashish_darbariuk AT yahoo.co.uk>]

Thank you all, for educating me in different ways of handling

the same problem. The problem I really had was being unable to

specify the measure function such that it can be called in snarf, the 

idea of specifying lsum on a product as opposed to currying was

the key for me. I ended up using Function  this morning although 

Program Fixpoint works out as well.

But the way Muad showed how to use Definition looks really cool!

Unless this example is already in some tutorial or notes, I think it might be a good

idea to include this function definition in some tutorial and show how many different ways

there are to define this kind of recursive functions.  Also Matthieu's notes in his

email on the usage of Function and Program Fixpoint would help being in the tutorial.

Thanks once again and a Happy New Year to all.

Ashish

---

From: muad <muad.dib.space AT gmail.com>
To: coq-club AT pauillac.inria.fr
Sent: Thursday, 1 January, 2009 17:55:06
Subject: Re: [Coq-Club] Defining recursive functions


Sometimes with a structural/lexicographic recursion like that, you can split
the recursion into two levels, (in the same way as Conors mgu algorithm).

Definition snarf (l1 l2: list Z) (acc:list Z):list Z.
refine (fix snarf_l1 (l1 :list Z):list Z -> list Z -> list Z := _).
refine (fix snarf_l2 (l2: list Z):list Z -> list Z := _).
refine (
  fun acc =>
    match l1, l2 with
      | nil, _ => acc
      | _, nil => acc
      | x::xs, y::ys =>
        if Z_eq_dec x y
          then snarf_l1 xs ys (x::acc)
          else if Z_le_gt_dec x y
            then snarf_l1 xs (y::ys) (x::acc)
            else snarf_l2 ys acc
    end).
Defined.

I hope this is useful,
--
View this message in context: http://www.nabble.com/Defining-recursive-functions-tp21237063p21237515.html
Sent from the Coq mailing list archive at Nabble.com.

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club