The Coq mailing list

[Jieung Kim <gbali AT kaist.ac.kr>]

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