The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Dear Jieung Kim,

  You can proceed to an induction on l1', which is used to build l2' step by step.

Require Import Peano_dec.

 Lemma LC_subset: forall n l1 l2 l1',
        LessCollection n l1 l2 ->
        exists l2', LessCollection n (l1'++l1) (l2'++l2).
 Proof.
      induction l1';   simpl.
      exists nil;simpl;auto.
     intro H;  destruct (IHl1' H) as [l2' H2];  case (Lt.le_or_lt n a).
     intro H3;exists (a::l2');constructor 3;simpl;auto.
     intro H3;exists l2';constructor 2;simpl;auto with arith.
Qed.
    
In fact, you can use the same kind of argument to prove also the simpler lemma:


   Lemma LesCollection_ex : forall n l1, exists l2, LessCollection n l1 l2.


The best,

Pierre


Le 07/04/2011 08:49, Jieung Kim a écrit :

Dear all,

I'm trying to prove the Lemma LC_subset, and I tried to do an induction on list l1.

However, I cannot find a way to prove second subgoal and think additional lemma to prove it.

Could you tell me the way to prove such a lemma?

Thanks.

Require Import List.

Inductive LessCollection: nat -> list nat -> list nat -> Prop :=

    | LCnil: forall n, LessCollection n nil nil

    | LCnoadd: forall n l1 l2 n',

        LessCollection n l1 l2 ->

        ~(le n n') ->

        LessCollection n (n'::l1) l2

    | LCadd: forall n l1 l2 n',

        LessCollection n l1 l2 ->

        le n n' ->

        LessCollection n (n'::l1) (n'::l2).

Lemma LC_subset: forall n l1 l2 l1',

    LessCollection n l1 l2 ->

    exists l2', LessCollection n (l1'++l1) (l2'++l2).

Proof.

--
Jieung Kim ( 김지응 )
Programming Language Research Group, KAIST
E-mail : gbali at kaist.ac.kr
            je1004k at gmail.com
Homepage : plrg.kaist.ac.kr/kje