The Coq mailing list

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