Changeset 3549 for LTS/Simulation.ma


Ignore:
Timestamp:
Apr 2, 2015, 3:44:19 PM (5 years ago)
Author:
piccolo
Message:

added paolo's trick

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3531 r3549  
    44discriminator option.
    55
    6 record relations (S1,S2 : abstract_status) : Type[0] ≝
     6record relations (p : label_params) (S1,S2 : abstract_status p) : Type[0] ≝
    77 { Srel: S1 → S2 → Prop
    88 ; Crel: S1 → S2 → Prop
    99 }.
    1010
    11 definition Rrel ≝ λS1,S2 : abstract_status.λrel : relations S1 S2.λs,s'.
    12  ∀s1,s1'. as_syntactical_succ S1 s1 s → Crel … rel s1 s1' → as_syntactical_succ S2 s1' s'.
    13 
    14 record simulation_conditions (S1,S2 : abstract_status) (rel : relations S1 S2) : Prop ≝
     11definition Rrel ≝ λp.λS1,S2 : abstract_status p.λrel : relations … S1 S2.λs,s'.
     12 ∀s1,s1'. as_syntactical_succ … S1 s1 s → Crel … rel s1 s1' → as_syntactical_succ … S2 s1' s'.
     13
     14record simulation_conditions (p : label_params) (S1,S2 : abstract_status p)
     15(rel : relations …S1 S2) : Prop ≝
    1516 { initial_is_initial :
    1617   ∀s1,s2.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2))
     
    2122 ; simulate_tau:
    2223     ∀s1:S1.∀s2:S2.∀s1':S1.
    23       as_execute … (cost_act (None ?))  s1 s1'→
     24      as_execute … (cost_act (None ?))  s1 s1'→
    2425      Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    25       ∃s2'. ∃t: raw_trace S2 s2 s2'.
     26      ∃s2'. ∃t: raw_trace S2 s2 s2'.
    2627        Srel … rel s1' s2' ∧ silent_trace … t
    2728 ; simulate_label:
    2829     ∀s1:S1.∀s2:S2.∀l.∀s1':S1.
    29       as_execute S1 (cost_act (Some ? l)) s1 s1' →
     30      as_execute … S1 (cost_act … (Some ? l)) s1 s1' →
    3031      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    3132      Srel … rel s1 s2 →
    3233      ∃s2',s2'',s2'''.
    33        ∃t1: raw_trace S2 s2 s2'.
    34        as_execute … (cost_act (Some ? l)) s2' s2'' ∧
     34       ∃t1: raw_trace S2 s2 s2'.
     35       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
    3536       ∃t3: raw_trace … s2'' s2'''.
    3637        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
     
    3839     ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
    3940      is_call_post_label … s1 →
    40       as_execute … (call_act f l) s1 s1' →
     41      as_execute … (call_act f l) s1 s1' →
    4142      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    4243      Srel … rel s1 s2 →
    4344      ∃s2',s2'',s2'''.
    44        ∃t1: raw_trace S2 s2 s2'.
    45        as_execute … (call_act f l) s2' s2'' ∧
     45       ∃t1: raw_trace S2 s2 s2'.
     46       as_execute … (call_act f l) s2' s2'' ∧
    4647       bool_to_Prop(is_call_post_label … s2') ∧
    47        ∃t3: raw_trace S2 s2'' s2'''.
     48       ∃t3: raw_trace S2 s2'' s2'''.
    4849        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    4950 ; simulate_ret_l:
    5051     ∀s1:S1.∀s2:S2.∀s1':S1.∀l.
    51       as_execute S1 (ret_act (Some ? l)) s1 s1' →
     52      as_execute … S1 (ret_act … (Some ? l)) s1 s1' →
    5253      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    5354      Srel  … rel s1 s2 →
    5455      ∃s2',s2'',s2'''.
    55        ∃t1: raw_trace S2 s2 s2'.
    56        as_execute … (ret_act (Some ? l)) s2' s2'' ∧
    57        ∃t3: raw_trace S2 s2'' s2'''.
     56       ∃t1: raw_trace S2 s2 s2'.
     57       as_execute p S2 (ret_act p (Some ? l)) s2' s2'' ∧
     58       ∃t3: raw_trace S2 s2'' s2'''.
    5859        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    5960 ; simulate_call_n:
    6061     ∀s1:S1.∀s2:S2.∀s1':S1.∀f,l.
    61       as_execute … (call_act f l) s1 s1' →
     62      as_execute … (call_act f l) s1 s1' →
    6263      ¬ is_call_post_label … s1 →
    6364      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    6465      Srel … rel s1 s2 →
    6566      ∃s2',s2'',s2'''.
    66        ∃t1: raw_trace S2 s2 s2'.
     67       ∃t1: raw_trace S2 s2 s2'.
    6768       bool_to_Prop (¬ is_call_post_label … s2') ∧
    68        as_execute … (call_act f l) s2' s2'' ∧
    69        ∃t3: raw_trace S2 s2'' s2'''.
     69       as_execute … (call_act f l) s2' s2'' ∧
     70       ∃t3: raw_trace S2 s2'' s2'''.
    7071        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    7172        ∧ Crel … rel s1 s2'
    7273 ; simulate_ret_n:
    7374     ∀s1:S1.∀s2:S2.∀s1':S1.
    74       as_execute … (ret_act (None ?)) s1 s1' →
     75      as_execute … (ret_act (None ?)) s1 s1' →
    7576      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    7677      Srel … rel s1 s2 →
    7778      ∃s2',s2'',s2''': S2.
    78        ∃t1: raw_trace S2 s2 s2'.
    79        as_execute … (ret_act (None ?)) s2' s2''  ∧
    80        ∃t3: raw_trace S2 s2'' s2'''.
     79       ∃t1: raw_trace S2 s2 s2'.
     80       as_execute … (ret_act (None ?)) s2' s2''  ∧
     81       ∃t3: raw_trace S2 s2'' s2'''.
    8182        Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3
    8283        ∧ Rrel … rel s1' s2''
     
    104105qed.
    105106
    106 lemma simulate_labelled_action : ∀S1,S2 : abstract_status.
    107 ∀rel : relations S1 S2.
     107lemma simulate_labelled_action : ∀p.∀S1,S2 : abstract_status p.
     108∀rel : relations S1 S2.
    108109∀s1,s2 : S1.∀s1' : S2.
    109 ∀l : ActionLabel.
     110∀l : ActionLabel p.
    110111simulation_conditions … rel →
    111 is_costlabelled_act l →
    112 (is_call_act l → is_call_post_label … s1) →
     112is_costlabelled_act l →
     113(is_call_act l → is_call_post_label … s1) →
    113114as_execute … l s1 s2 →
    114115Srel … rel s1 s1' →
     
    119120silent_trace … t_pre ∧ silent_trace … t_post ∧
    120121as_execute … l pre_em post_em ∧
    121 (is_call_act l → is_call_post_label … pre_em) ∧
     122(is_call_act l → is_call_post_label … pre_em) ∧
    122123Srel … rel s2 s2'.
    123 #S1 #S2 #rel #s1 #s2 #s1' *
     124#p #S1 #S2 #rel #s1 #s2 #s1' *
    124125[ #f #c | * [|#lbl] | * [|#lbl]]
    125126#sim * #Hcall #prf #REL * #Hio
     
    162163
    163164
    164 theorem simulates_pre_mesurable:
    165  ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
    166  ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
     165theorem simulates_pre_mesurable: ∀p.
     166 ∀S1,S2 : abstract_status p.∀rel : relations … S1 S2.
     167 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
    167168  simulation_conditions … rel →
    168169  pre_measurable_trace … t1 →
     
    175176    (measurable_suffix … t1 → measurable_suffix … t2) ∧
    176177    (silent_trace … t1 → silent_trace … t2).
    177 #S1 #S2 #rel #s1 #s1' #t1 #sim #H elim H -t1 -s1 -s1'
     178#p #S1 #S2 #rel #s1 #s1' #t1 #sim #H elim H -t1 -s1 -s1'
    178179[ #st #Hst #s2 #Hs2 #Rsts2 %{s2} %{(t_base …)} %
    179180 [ % [ % // % // % //] * #s_em ** [ #sx | #x1 #x2 #x3 #l1 #prf1 #tl1] * #t_pre * #s_post * #t_post * #sil_tpost
     
    243244    | #Hsuff cases(measurable_suffix_tind … Hsuff)
    244245      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s2''} %{t_s2''} %{s2'''} %{(t_s2'''' @ t_s3)}
    245       % [ /3 by or_introl, append_silent/ ] %{(cost_act (Some ? lbl))} %{(exe_s2''')} % // % // * #f * #c #EQ destruct
    246       | #H @measurable_suffix_append change with ((t_ind ?????? t_s2'''')@t_s3) in ⊢ (????%);
     246      % [ /3 by or_introl, append_silent/ ] %{(cost_act (Some ? lbl))} %{(exe_s2''')} % // % // * #f * #c #EQ destruct
     247      | #H @measurable_suffix_append change with ((t_ind ??????? t_s2'''')@t_s3) in ⊢ (?????%);
    247248        @measurable_suffix_append /2/
    248249      ]
     
    279280 |  #Hsuff cases(measurable_suffix_tind … Hsuff)
    280281      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{st1} %{t1} %{st2} %{(t2 @ t_fin)}
    281       % [ /3 by or_introl, append_silent/ ] %{(ret_act (Some ? ret_lab))} %{(exe_s2'')} % // % // * #f * #c #EQ destruct
    282       | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
     282      % [ /3 by or_introl, append_silent/ ] %{(ret_act (Some ? ret_lab))} %{(exe_s2'')} % // % // * #f * #c #EQ destruct
     283      | #H @measurable_suffix_append change with ((t_ind ??????? t2)@t_fin) in ⊢ (?????%);
    283284        @measurable_suffix_append /2/
    284285      ]
     
    317318   | #Hsuff cases(measurable_suffix_tind … Hsuff)
    318319      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s'} %{t1} %{s2''} %{(t2 @ t_fin)}
    319       % [ /3 by or_introl, append_silent/ ] %{(call_act f lab)} %{(exe_s2'')} % // % //
    320       | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
     320      % [ /3 by or_introl, append_silent/ ] %{(call_act f lab)} %{(exe_s2'')} % // % //
     321      | #H @measurable_suffix_append change with ((t_ind ??????? t2)@t_fin) in ⊢ (?????%);
    321322        @measurable_suffix_append /2/
    322323      ]
     
    381382     #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    382383     #ABS1 >ABS1 in Hst1; [2: /3 by ex_intro/] *
    383    | #Hsuff @measurable_suffix_append change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append
    384      change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append @Hm2
     384   | #Hsuff @measurable_suffix_append change with (t_ind ???????? @ ?) in ⊢ (?????%); @measurable_suffix_append
     385     change with (t_ind ???????? @ ?) in ⊢ (?????%); @measurable_suffix_append @Hm2
    385386     cases(measurable_suffix_append_case … Hsuff)
    386387     [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
     
    403404qed.
    404405
    405 lemma silent_in_silent : ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
    406  ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
     406lemma silent_in_silent : ∀p.∀S1,S2 : abstract_status p.∀rel : relations … S1 S2.
     407 ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
    407408  simulation_conditions … rel →
    408409  ∀s2 : S2.Srel … rel s1 s2 →
     
    411412    silent_trace … t2 ∧
    412413    Srel … rel s1' s2'.
     414    #p
    413415#S1 #S2 #rel #s1 #s1' #t1 #sim #s2 #REL *
    414416[ #pre_sil_ti0 cases(simulates_pre_mesurable … sim … (pre_silent_is_premeasurable … pre_sil_ti0) … REL)
     
    423425qed.
    424426
    425 lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status.
     427lemma tail_of_premeasurable_is_not_io : ∀p.∀S : abstract_status p.
    426428∀s1,s2 : S.∀t : raw_trace … s1 s2.
    427429pre_measurable_trace … t →
    428 as_classify … s2 ≠ cl_io.
     430as_classify … s2 ≠ cl_io. #p
    429431#S #s1 #s2 #t #H elim H //
    430432qed.
    431433
    432434theorem simulates_measurable:
    433  ∀S1,S2: abstract_status.
    434  
    435  ∀rel: relations S1 S2. simulation_conditions … rel →
     435 ∀p.
     436 ∀S1,S2: abstract_status p.
     437 
     438 ∀rel: relations … S1 S2. simulation_conditions … rel →
    436439 
    437440 ∀si,sn: S1. ∀t: raw_trace … si sn.
     
    451454 
    452455 ∃s1',s2'. measurable … s1' s2' … t'.
    453 #S1 #S2 #rel #sim_rel #si #sn #t #s1 #s3 #Hmeas #s1' #Hclass #Rsi_si'
     456#p #S1 #S2 #rel #sim_rel #si #sn #t #s1 #s3 #Hmeas #s1' #Hclass #Rsi_si'
    454457cases Hmeas -Hmeas #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 *******
    455458#pre_t12 #EQ destruct #Hl1 #Hl2 #Hcall_fin #sil_ti0 #sil_t3n #Hcall_init
     
    469472#sn' * #t_3n' * #sil_t3n' #Rsn_sn' %{sn'}
    470473%{(ti0'@ t_s0'' @ (t_ind … prf1' (t_s1''@t12' @ t_s2'' @ (t_ind … prf2' (t_s3'' @ t_3n')))))}
    471 % [ % // cases daemon (*TODO*) ]
     474% [ % // >(get_cost_label_invariant_for_append_silent_trace_l … sil_ti0)
     475    >(get_cost_label_invariant_for_append_silent_trace_l … sil_ti0')
     476    >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts0'')
     477    whd in ⊢ (??%%); @eq_f2 //
     478    >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts1'')
     479    >get_cost_label_append >get_cost_label_append in ⊢ (???%); @eq_f2 //
     480    >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts2'')
     481    whd in ⊢ (??%%); @eq_f2 //
     482    >(get_cost_label_invariant_for_append_silent_trace_l … sil_ts3'')
     483    >(get_cost_label_silent_is_empty … sil_t3n') >(get_cost_label_silent_is_empty … sil_t3n) % ]
    472484%{s1''} %{s3''} whd %{s0''} %{s2''} %{(ti0' @t_s0'')} %{(t_s1'' @ t12' @ t_s2'')}
    473485%{(t_s3'' @ t_3n')} %{l1} %{l2} %{prf1'} %{prf2'} % [2: /2/]
    474486% [2: /2 by append_silent/] % [2: /2 by append_silent/] % [2: /2/] % // % // % //
    475487@append_premeasurable_silent /2/
    476 qed. 
    477 
    478 
     488qed.
     489
     490
Note: See TracChangeset for help on using the changeset viewer.