Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Problem with a simple proof

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with a simple proof


chronological Thread 
  • From: Pierre Casteran <pierre.casteran AT labri.fr>
  • To: Jieung Kim <gbali AT kaist.ac.kr>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Problem with a simple proof
  • Date: Thu, 07 Apr 2011 16:36:00 +0200

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




Archive powered by MhonArc 2.6.16.

Top of Page