The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Notice also that you can use merge2_equation to rewrite instead of
computing (if you are trying to to prove thing on unclosed terms).

P.

2011/12/20 Jónathan Heras 
<jonathan.heras AT unirioja.es>:
> Thanks, it worked perfectly.
> Sincerely.
> Jónathan
>
> El 20/12/11 16:59, Vincent Siles escribió:
>
>> Hi Jonathan,
>> try replacing Qed with Defined. It should allow your function to evaluate.
>>
>> Cheers,
>> Vincent
>>
>>Â 2011/12/20<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.
>
>