The Coq mailing list

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

Dear all,

First, thank you so much, Pierre Casteran.

I have one more question about a proof.

How can I solve such proof when I cannot use Peano_dec.

For example, In this case, I think I cannot prove 

Lemma sub_ty_same_or_not: forall t1 t2, (sub_ty t1 t2) \/ ~(sub_ty t1 t2).

Therefore, I cannot use the same approach for Lemma subtyset_ex

Is there any way to prove Lemma subtyset_ex?

Or, Do I have to change subtyset definition?

Thanks.

Definition ty := nat.

Notation tytable := (list (ty * ty)).

Parameter TT : tytable.

Definition extends (t1: ty) (t2: ty) : Prop :=

   In (t1, t2) TT.

Inductive sub_ty : ty -> ty -> Prop :=

    | sub_refl : forall t, sub_ty t t

    | sub_trans : forall t1 t2 t3, sub_ty t1 t2 -> sub_ty t2 t3 -> sub_ty t1 t3

    | sub_tapp : forall t1 t2, extends t1 t2 -> sub_ty t1 t2.

Inductive subtyset : ty -> list ty -> list ty -> Prop :=

    | subtysetnil : forall t, subtyset t nil nil

    | subtysetnoadd: forall t t' ts1 ts2,

          subtyset t ts1 ts2 ->

          ~(sub_ty t' t) ->

          subtyset t (t'::ts1) ts2

    | subtysetadd: forall t t' ts1 ts2,

           subtyset t ts1 ts2 ->

           sub_ty t' t ->

           subtyset t (t'::ts1) (t'::ts2).

Lemma subtyset_ex: forall t ts1,

    exists ts2, subtyset t ts1 ts2.

Proof.

  induction ts1.

  exists nil. constructor 1.

  destruct IHts1 as (ts2, H).

  .......

2011/4/7 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

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