The Coq mailing list

[��ӣ <phoebezz AT 163.com>]

Hi guys,
   
  We are defined a relationship "simulation" over two traces and try  to prove the transitive property of it. But we meet some problems when proving the sim_tl case. So I wonder whether I give the proper definition on "simulation".

 

We define a simulation relation over two traces trace1 and trace2 inductively as follow:
(1) Let c c¡¯ ¡Ê cnd, e e¡¯ ¡Ê event,  (ge c e)  (ge c¡¯ e¡¯)¡Êgrdevt(GuardEvent), 
simulation   (ge c e)  (ge c¡¯ e¡¯) if bImp c c¡¯ and e = e¡¯
(2)There is a strictly increasing function ¦Ë:dom(trace1) -> dom(trace2)
Such that:
Let i,j ¡Ê grdevt(GuardEvent),
a. Forall  i¡Ê trace1 , exists j¡Ê trace2 , simulation i  (¦Ëj)
b. forall j= (ge c e) ¡Ê trace1 ,if not (j ¡Êimage(trace2)) , exists  k=(ge c¡¯ e¡¯)¡Êgrdevt and j strictly follows k in trace1 and c = c¡¯.

(The domain of a function f is denoted dom(f) and its image image(f) = { f(x) | x ¡Ê dom(f)}.)

 

Could u please give us some guidence? The related codes are in the attachment and i have added comments .

Thank you for all the help.

Attachment: example.v
Description: Binary data