The Coq mailing list

[ldou AT cs.ecnu.edu.cn]

Hi  all, I write the following codes in Coq:
========================
Require Export String Bool ListSet List Arith Compare_dec Omega Ascii.

Open Scope nat_scope.
Open Scope type_scope.
Open Scope string_scope.
Open Scope list_scope.

(*=========Definition============*)
Inductive K:Set:=
|Send:K
|Receive:K.
Definition O:=string.
Definition L:=string.
Definition E:=K*O*L*L.
Definition T:=list E.
Definition G:=set T.

(*===========Decidable equality============*)
Definition K_dec : forall (a b:K), {a = b} + {a <> b}.
    intros;destruct a;destruct b;intuition;auto;
    right; intros; inversion H. 
Qed.

Definition O_dec:forall (a b:O) ,{a = b} + {a <> b}.
   exact string_dec.
Qed.

Definition L_dec:forall (a b:L) ,{a = b} + {a <> b}.
   exact string_dec.
Qed.

Definition E_dec:forall (a b:E) ,{a = b} + {a <> b}.

Admitted.

Definition T_dec:forall (a b:E) ,{a = b} + {a <> b}.
Admitted.

Definition G_dec:forall (a b:G) ,{a = b} + {a <> b}.
Admitted.

Eval compute in set_mem K_dec Send (Send::nil).
================================
the question is how to prove  E_dec ,T_dec and G_dec.
what's more, i find K_dec doesn't work when "Eval compute ",
it just return:

=if Kind_dec Send Send then true else false
:bool

How can i get the exact answer  (ture or false)?
----------------
===========================================================
Best regards!
 
Lisa Dou
(Department of Computer Science, East China Normal University)

E-mail:ldou AT cs.ecnu.edu.cn   
 
===========================================================