The Coq mailing list

[Julien Forest <forest AT ensiie.fr>]

Happy new year to all of you. 

Dear Ashish, you can use Function to define your function: 

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 := *)
Require Import Recdef.
Function snarf (acc:list Z) (l1_l2: list Z * list Z){measure lsum l1_l2}:list 
Z
:=
  match l1_l2 with
    | (nil,_) => acc
    | (_,nil) => acc
    | ((x::xs),(y::ys)) => 
      match Z_eq_dec x y with
        | left _ => snarf (x::acc) (xs,ys)  
        | right _ => 
          match Z_le_gt_dec x y with
            | left _ => snarf (x::acc) (xs,y::ys)
            | right _ => snarf acc (x::xs, ys)
      end
  end
end.
Proof.
  abstract(intros; simpl;omega).
  abstract(intros; simpl;omega).
  abstract(intros; simpl;omega).
Defined.


On Wed, 31 Dec 2008 15:14:20 -0800
Taral 
<taralx AT gmail.com>
 wrote:

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