Changeset 3390 for LTS/Simulation.ma


Ignore:
Timestamp:
Oct 10, 2013, 2:53:31 PM (6 years ago)
Author:
piccolo
Message:

Patched simulation proof, changed definition of silent trace

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3389 r3390  
    112112[ assumption
    113113| %{(None ?)} %
    114 | @IH try assumption >Hclass % #EQ destruct
     114| @IH try assumption
    115115]
    116116qed.
     
    125125[ #st #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
    126126#_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
    127 @IH [ >Hst2' % #EQ destruct | assumption]
     127@IH assumption
    128128qed.
    129129
     
    158158λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
    159159
     160(*
    160161lemma append_well_formed_silent : ∀S : abstract_status.
    161162∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
    162163well_formed_trace … t → pre_silent_trace … t' →
    163 (is_trace_non_empty … t' → as_classify … st1' = cl_other) →
     164(is_trace_non_empty … t' → as_classify … st) →
    164165well_formed_trace … (t' @ t).
    165166#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
     
    172173[2: >(Hclass1 I) % #EQ destruct]
    173174@IH try assumption #_ assumption
    174 qed.
     175qed.*)
    175176
    176177lemma well_formed_append : ∀S : abstract_status.
     
    200201try @IH assumption
    201202qed.
    202 
     203(*
    203204lemma silent_is_well_formed : ∀S : abstract_status.
    204205∀st1,st2 : S.∀t : raw_trace … st1 st2.silent_trace … t → well_formed_trace … t.
     
    208209[ @IH % [2: #_ ] assumption | >(H1 I) % #EQ destruct]
    209210qed.
    210 
     211*)
    211212
    212213lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
     
    260261  #pre_measurable_tl #IH #well_formed #s2 #classify_s2 #REL
    261262  [ cases(simulate_tau … good … execute … REL) #s2'' * #t_s2'' * #RELst2s2''
    262     * #silent_ts2'' #Hclass_s2 cases(IH … RELst2s2'')
     263    ** #silent_ts2'' #Hclass_s2 #wf_ts2'' cases(IH … RELst2s2'')
    263264    [2: cases(well_formed_trace_inv … well_formed)
    264265         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
     
    276277    [ %
    277278      [ @append_premeasurable_silent assumption
    278       | @append_well_formed_silent assumption
     279      | @append_well_formed assumption
    279280      ]
    280281    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
     
    291292    ]
    292293    #s2'' * #s2''' * #s2'''' * #t_s2'' ** #exe_s2''' #CLASS' * #t_s2'''' ** #RELst2_s2''''
    293     * #sil_ts2'' #Hclass_s2 * #sil_t_s2'''' #Hclass_s2''' cases(IH … RELst2_s2'''')
     294    ** #sil_ts2'' #Hclass_s2 #wf_ts2'' ** #sil_t_s2'''' #Hclass_s2''' #wf_ts2'''' cases(IH … RELst2_s2'''')
    294295    [2: cases(well_formed_trace_inv … well_formed)
    295296         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
     
    312313        ]
    313314        @append_premeasurable_silent assumption
    314       | @append_well_formed_silent try assumption inversion(as_classify … s2'')
     315      | @append_well_formed try assumption inversion(as_classify … s2'')
    315316        #Hclass
    316317        [ %3 [2: %{c} %]
    317318        |*: %2 [2,4: >Hclass % #EQ destruct]
    318319        ]
    319         @append_well_formed_silent assumption
     320        @append_well_formed assumption
    320321      ]
    321322    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
     
    341342  #sil_t1 #sil_t2
    342343  cases(IH … wf_tl' … rel_s2_s2''')
    343   [2: @(silent_io … (proj1 … sil_t2)) assumption]
     344  [2: @(silent_io … (proj1 … (proj1 … sil_t2))) assumption]
    344345  #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL
    345346  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
    346347  % [2: whd in ⊢ (??%?);
    347         >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))
     348        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t1)))
    348349        whd in ⊢ (???%);
    349         >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))
     350        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t2)))
    350351        @eq_f assumption ]
    351352  %
    352   [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]
     353  [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_t1))]
    353354    %3
    354     [ @(silent_io … (proj1 … sil_t1)) assumption
     355    [ @(silent_io … (proj1 … (proj1 … sil_t1))) assumption
    355356    | whd %{ret_lab} %
    356     | @append_premeasurable_silent try assumption @(proj1 … sil_t2)
     357    | @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_t2))
    357358    ]
    358   | @append_well_formed_silent
    359     [ %2 try assumption @append_well_formed_silent try assumption
    360       [ @(proj1 … sil_t2)
    361       | @(proj2 … sil_t2)
    362       ]
    363     | @(proj1 … sil_t1)
    364     | @(proj2 … sil_t1)
    365     ]
     359  | @append_well_formed
     360    [ @(proj2 … sil_t1)]
     361    %2 try assumption @append_well_formed try assumption @(proj2 … sil_t2)
    366362  ]
    367363| #s2 #s2' #s2'' #l #exe_s2_s2' #tl #class_s2 whd in ⊢ (% → ?); * #f * #lab #EQ destruct
     
    379375   #s2' * #s2'' * #s2''' * #t1 **** #j_s2' #exe_s2'' #post' #io_s2'' * #t2 ** #REL #sil_t1 #sil_t2
    380376   cases(IH … wf_tl' … REL)
    381    [2: @(silent_io … (proj1 … sil_t2)) assumption ]
     377   [2: @(silent_io … (proj1 … (proj1 … sil_t2))) assumption ]
    382378   #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL1 %{s2_fin}
    383379   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
    384380   [2: whd in ⊢ (??%?);
    385         >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))
     381        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t1)))
    386382        whd in ⊢ (???%);
    387         >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))
     383        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t2)))
    388384        @eq_f assumption ]
    389385   %
    390    [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]
     386   [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_t1))]
    391387     %4 try assumption
    392      [ @(silent_io … (proj1 … sil_t1)) assumption
     388     [ @(silent_io … (proj1 … (proj1 … sil_t1))) assumption
    393389     | whd %{f} %{lab} %
    394      | @append_premeasurable_silent try assumption @(proj1 … sil_t2)
     390     | @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_t2))
    395391     ]
    396    | @append_well_formed_silent
    397      [ %2 try assumption @append_well_formed_silent try assumption
    398         [ @(proj1 … sil_t2)
    399         | @(proj2 … sil_t2)
    400         ]
    401      | @(proj1 …  sil_t1)
    402      | @(proj2 … sil_t1)
    403      ]
     392   | @append_well_formed [ @(proj2 … sil_t1) ]
     393     %2 try assumption @append_well_formed try assumption @(proj2 … sil_t2)
    404394   ]
    405395| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
     
    412402      #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1 | * #y1 #EQ destruct(EQ) ] #_
    413403      #EQ1 #EQ2 #EQ3 destruct #_ @(proj1 … (well_formed_append … wf_tl))
    414   |3: @(silent_io … (proj1 … sil_tr2)) assumption
     404  |3: @(silent_io … (proj1 … (proj1 … sil_tr2))) assumption
    415405  ]
    416406  #st3' * #tr3 *** #pre_tr3 #wf_tr3 #EQcost_tr3 #REL2
     
    423413      #z1 #z2 #z3 #w #prf' #tl' #wf_tl' [ #Hz1 | * #w1 #EQ destruct(EQ)] #_
    424414      #EQ1 #EQ2 #EQ3 destruct #_ assumption
    425   |3: @(silent_io … (proj1 … sil_tr5)) assumption
     415  |3: @(silent_io … (proj1 … (proj1 … sil_tr5))) assumption
    426416  ]
    427417  #st5' * #tr6 *** #pre_tr6 #wf_tr6 #EQcost_tr6 #REL4 %{st5'}
     
    429419  % [2: assumption] %
    430420  [ %
    431      [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_tr1) ]
     421     [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_tr1)) ]
    432422       %5
    433        [ @(silent_io … (proj1 … sil_tr1)) assumption
    434        | @(silent_io … (proj1 … sil_tr4)) assumption
     423       [ @(silent_io … (proj1 … (proj1 … sil_tr1))) assumption
     424       | @(silent_io … (proj1 … (proj1 … sil_tr4))) assumption
    435425       | whd %{f} %{l} %
    436426       | assumption
    437        | @append_premeasurable_silent try assumption [2: @(proj1 … sil_tr2)]
    438          @append_silent_premeasurable try assumption @(proj1 … sil_tr4)
    439        | @append_premeasurable_silent try assumption @(proj1 … sil_tr5)
     427       | @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_tr2))]
     428         @append_silent_premeasurable try assumption @(proj1 … (proj1 … sil_tr4))
     429       | @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_tr5))
    440430       | @(RET_REL … call_rel) assumption
    441431       | %
    442432       ]
    443      | @append_well_formed_silent [2: @(proj1 … sil_tr1) |3: @(proj2 … sil_tr1) ]
    444        %2 [2: assumption] >append_associative @append_well_formed_silent
    445        [2: @(proj1 … sil_tr2) |3: @(proj2 … sil_tr2) ] @append_well_formed
     433     | @append_well_formed [ @(proj2 … sil_tr1) ]
     434       %2 [2: assumption] >append_associative @append_well_formed
     435       [ @(proj2 … sil_tr2) ] @append_well_formed
    446436       [ @append_well_formed try assumption @silent_is_well_formed assumption ]
    447437       %2 [2: assumption] @append_well_formed try assumption @silent_is_well_formed
    448438       assumption
    449439     ]
    450   | >get_cost_label_invariant_for_append_silent_trace_l [2: @(proj1 … sil_tr1) ]
     440  | >get_cost_label_invariant_for_append_silent_trace_l [2: @(proj1 … (proj1 … sil_tr1)) ]
    451441    whd in ⊢ (??%%); @eq_f >append_associative
    452442    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    453     [2: @(proj1 … sil_tr2) ] >append_associative
     443    [2: @(proj1 … (proj1 … sil_tr2)) ] >append_associative
    454444    >get_cost_label_append in ⊢ (???%);
    455445    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    456     [2: @(proj1 … sil_tr4) ] normalize
     446    [2: @(proj1 … (proj1 … sil_tr4)) ] normalize
    457447    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    458     [2: @(proj1 …  sil_tr5) ] >get_cost_label_append in ⊢ (??%?); @eq_f2
     448    [2: @(proj1 … (proj1 … sil_tr5)) ] >get_cost_label_append in ⊢ (??%?); @eq_f2
    459449    assumption
    460450  ]
     
    462452qed.
    463453
    464 xxxxx
     454sxxxxx
    465455
    466456
Note: See TracChangeset for help on using the changeset viewer.