The Coq mailing list

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

Dear Pierre Casteran

Thank you for your advice.

2011/4/7 Pierre Casteran <pierre.casteran AT labri.fr>

Dear Jieung Kim,

  Perhaps the first thing is to prove that "extends" is decidable (using lemmas on
lists and the decidibility of equality on nat), then prove the decidibilty of
"sub_ty"  (may be not so trivial ? ) , then proceed as your first example.

Pierre

Le 07/04/2011 15:33, Jieung Kim a écrit :

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.

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