The Coq mailing list

[jonathan.heras AT unirioja.es]

Dear all,

I would like to know if it is possible to execute a recursive function which
has been defined using the Function Command.

For instance, if we have defined the following function (which merges two
lists)

Function merge2 (p:list Z*list Z)
{measure (fun p=>(length (fst p))+(length (snd p)))} : list Z :=
match p with
| (nil,l) => l
| (l,nil) => l
| (x::xs,y::ys) => if Z_lt_ge_dec x y
then x::(merge2 (xs,y::ys))
else y::(merge2 (x::xs,ys))
end.
intros.
simpl; auto with arith.
intros.
simpl; auto with arith.
Qed.

and now we are interested in computing

Eval compute in merge2 ((1::3::5::nil),(2::4::6::nil)).

In this case, the result that I obtain is

let (v, _) :=
           merge2_terminate
             (1 :: 3 :: 5 :: Datatypes.nil, 2 :: 4 :: 6 :: Datatypes.nil) in
       v
     : list Z

when I was expecting (1::2::3::4::5::6::nil).

So, is it impossible to compute with a recursive function defined using
Function?

Thank you in advance.