The Coq mailing list

[silviu andrica <silviu_andrica AT yahoo.com>]

Hello,
  yes you are right. I want to generate an OCaml piece of code that when given two lists returns yes or no. It might be simpler to implement it in OCaml, but I want it to be "correct", thus I want to use Coq.

Best regards,
  Silviu

---

From: Adam Chlipala <adamc AT hcoop.net>
To: silviu andrica <silviu_andrica AT yahoo.com>
Cc: coq-club AT pauillac.inria.fr
Sent: Thursday, February 19, 2009 7:31:54 PM
Subject: Re: [Coq-Club] Simple example

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.

--------------------------------------------------------
Bug reports: http://logical.saclay.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