The Coq mailing list

[Cedric Auger <Cedric.Auger AT lri.fr>]

Here is an awful way to do it using tactics.
You can also write it as in caml with Fixpoint and then prove it separately.
My function also provides witness in success case.
By extraction, you get a:

type sublist_result = Is_sublist of (a list * a list) | Is_not_sublist

But you need to instantiate A or generalize it.


Require Import List.

Parameter A : Set.
Parameter A_dec : forall (a b : A), { a = b } + { a <> b }.

Inductive sublist_result (l1 l2 : list A) : Set :=
| Is_sublist : forall a b, l1 = a ++ l2 ++ b -> sublist_result l1 l2
| Is_not_sublist : (forall a b, ~ l1 = a ++ l2 ++ b) -> sublist_result 
l1 l2.

Inductive prefix_result (l1 l2 : list A) : Set :=
| Is_prefix : forall b, l1 = l2 ++ b -> prefix_result l1 l2
| Is_not_prefix : (forall b, ~ l1 = l2 ++ b) -> prefix_result l1 l2.

Lemma prefix : forall l2 l1, prefix_result l1 l2.
Proof.
 induction l2.
   (*l2 is nil*)
     intro l1.
     apply Is_prefix with l1.
     simpl.
     reflexivity.
   (*l2->a::l2*)
     intro l1.
     destruct l1 as [| b l].
       (*l1 is nil*)
         apply Is_not_prefix.
         intro b.
         simpl.
         intro absurd.
         discriminate absurd.
       (*l1->b::l*)
         destruct (A_dec b a).
           (*a=b*)
             destruct (IHl2 l) as [ m Hm | H].
               (*is_prefix*)
                 apply Is_prefix with m.
                 rewrite Hm; rewrite e; simpl.
                 reflexivity.
               (*is_not_prefix*)
                 apply Is_not_prefix.
                 intro c.
                 simpl.
                 intro absurd.
                 inversion absurd.
                 destruct (H c H2).
           (*a<>b*)
             apply Is_not_prefix.
             simpl; intros c absurd.
             inversion absurd.
             destruct (n H0).
Defined.

Lemma sublist : forall l1 l2, sublist_result l1 l2.
Proof.
 induction l1.
   (*l1 is nil*)
     intro l2.
     destruct l2.
       apply Is_sublist with nil nil; auto.
       apply Is_not_sublist.
       simpl; intros; destruct a0; simpl; intro absurd; inversion absurd.
   (*l1->a::l1*)
     intro l2; destruct (IHl1 l2) as [ a0 b0 Hab | H ].
       apply Is_sublist with (a::a0) b0; simpl; rewrite Hab; auto.
       destruct l2.
         apply Is_sublist with (a::nil) l1; simpl; auto.
         destruct (prefix (a0::l2) (a::l1)).
           apply Is_sublist with nil b; simpl in *; auto.
           apply Is_not_sublist.
             intros a1 b absurd; simpl in *.
             destruct a1; simpl in *.
               exact (n b absurd).
               inversion absurd.
                 exact (H a2 b H2).
Defined.
silviu andrica a écrit :
> 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


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay