The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

silviu andrica wrote:
>   Today is my first day of Coq and I want to write a function in Coq 
> that checks if a list is a sublist of another list. I was thinking 
> somewhat around the lines of
>
> Definition sublist ( big_list sub_list : list ) := (exists a : list, b 
> : list) -> a++sub_list++b = big_list .
>
> And afterwards have this exported to OCaml.

Logical formulas cannot be exported to OCaml.  Extraction erases them 
systematically.  Perhaps you meant that you would like to export a 
decision procedure for that class of formulas?

> But I cannot do, can some one help?

If you've only been using Coq for a day, it's probably a bad idea to 
assume that you will be able to implement this example without more 
study.  I hope you're following a textbook or tutorial; if so, you 
should keep reading through it in order, doing a fair sample of the 
selected exercises for each chapter.