Changeset 3389 for LTS


Ignore:
Timestamp:
Oct 10, 2013, 1:07:28 PM (6 years ago)
Author:
piccolo
Message:

Ended simulation proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3388 r3389  
    6060      ∃s2',s2'',s2'''.
    6161       ∃t1: raw_trace S s2 s2'.
    62        as_execute … (call_act f l) s2' s2'' ∧
     62       bool_to_Prop (¬ is_call_post_label … s2') ∧
     63       as_execute … (call_act f l) s2' s2'' ∧ as_classify … s2' ≠ cl_jump ∧
     64       as_classify … s2'' ≠ cl_io ∧
    6365       ∃t3: raw_trace S s2'' s2'''.
    6466        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     
    6769     ∀s1,s2,s1' : S.
    6870      as_execute … (ret_act (None ?)) s1 s1' →
    69       Srel … rel s1 s2 →
     71      Srel … rel s1 s2 → as_classify … s2 ≠ cl_io ∧
    7072      ∃s2',s2'',s2'''.
    7173       ∃t1: raw_trace S s2 s2'.
    72        as_execute … (ret_act (None ?)) s2' s2''  ∧
     74       as_execute … (ret_act (None ?)) s2' s2''  ∧ as_classify … s2' ≠ cl_jump ∧
     75       as_classify … s2'' ≠ cl_io ∧
    7376       ∃t3: raw_trace S s2'' s2'''.
    7477        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
    75         ∧ Rrel … rel s2 s2''
     78        ∧ Rrel … rel s1' s2''
    7679 }.
    7780
     
    113116qed.
    114117
     118lemma pre_silent_is_premeasurable : ∀S : abstract_status.
     119∀st1,st2 : S. ∀t : raw_trace S st1 st2.as_classify … st1 ≠cl_io → pre_silent_trace … t
     120→ pre_measurable_trace … t.
     121#S #st1 #st2 #t elim t
     122[ #st #Hst #H inversion H in ⊢ ?; [ #st' #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
     123  #st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
     124-t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #Hst1 #H inversion H in ⊢ ?;
     125[ #st #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
     126#_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
     127@IH [ >Hst2' % #EQ destruct | assumption]
     128qed.
     129
     130lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
     131    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
     132    ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
     133#S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.   
     134
     135lemma append_silent_premeasurable : ∀S : abstract_status.
     136∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
     137pre_measurable_trace … t' → pre_silent_trace … t → as_classify … st1 ≠ cl_io →
     138pre_measurable_trace … (t' @ t).
     139#S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
     140[ normalize #st #Hst #r #H1 #H2 @pre_silent_is_premeasurable assumption
     141|2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
     142  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r #Hs3 [ %2 | %3 | %4 ]
     143  try ( %{x} %) try @IH try assumption % ]
     144#s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
     145#EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
     146#r #pre_r #Hs5 normalize
     147cut(∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
     148    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
     149    ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2)
     150[ @append_tind_commute ] #H >H >H >append_associative <H in ⊢ (????(??????%)); %5
     151try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
     152qed.
     153
     154
     155
    115156definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
    116157raw_trace S st1 st2 → bool ≝
     
    133174qed.
    134175
     176lemma well_formed_append : ∀S : abstract_status.
     177∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
     178well_formed_trace … (t1 @ t2) → well_formed_trace … t1 ∧ well_formed_trace … t2.
     179#S #st1 #st2 #st3 #t1 #t2 #H %
     180[ lapply H -H lapply t2 -t2 elim t1 [ //] #st1' #st2' #st3' #l #exe #tl #IH #r
     181#H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 normalize in EQ3; destruct ]
     182#st1'' #st2'' #st3'' #l' #prf' #tl' #wf_tl' [#Hst1'' | * #x #EQ destruct] #_
     183#EQ1 #EQ2 normalize in ⊢ (% → ?); #EQ3 destruct #_
     184[ %2 [ @IH assumption ] assumption | %3 [ @IH assumption ] %{x} % ]
     185]
     186lapply H lapply t2 -t2 elim t1 [ #st #r normalize //]
     187#s1 #s2 #s3 #l #prf #tl #IH #r #H inversion H in ⊢ ?;
     188[ #st #EQ1 #EQ2 normalize #EQ3 destruct ]
     189#s1' #s2' #s3' #l' #prf' #tl' #wf_tl' #Hs1' #_ normalize #EQ1 #EQ2 #EQ3 destruct
     190#_ @IH assumption
     191qed.
     192
     193
     194lemma append_well_formed : ∀S : abstract_status.
     195∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
     196well_formed_trace … t1 → well_formed_trace … t2 → well_formed_trace … (t1 @ t2).
     197#S #st1 #st2 #st3 #t1 #t2 #H lapply t2 -t2 elim H
     198[ #st #r #H1 @H1 ]
     199#s1 #s2 #s3 #l #prf #tl #wf_tl #Hs1 #IH #r #wf_r normalize [ %2 | %3]
     200try @IH assumption
     201qed.
     202
     203lemma silent_is_well_formed : ∀S : abstract_status.
     204∀st1,st2 : S.∀t : raw_trace … st1 st2.silent_trace … t → well_formed_trace … t.
     205#S #st1 #st2 #t elim t [ #st #_ %]
     206#s1 #s2 #s3 #l #prf #tl #IH * #H inversion H [ #st #EQ1 #EQ2 #EQ3 destruct]
     207#s1' #s2' #s3' #prf' #tl' #Hs2' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ #H1 %2
     208[ @IH % [2: #_ ] assumption | >(H1 I) % #EQ destruct]
     209qed.
     210
     211
    135212lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
    136213∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
     
    144221qed.
    145222
     223lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
     224∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
     225get_costlabels_of_trace … (t1 @ t2) =
     226 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
     227#S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
     228[#f * #l | * [| * #l] | *  [| #l] |] #prf #tl #IH #t2 normalize try @eq_f @IH
     229qed.
     230 
    146231(*
    147232lemma raw_trace_ind_r : ∀S : abstract_status.
     
    318403     ]
    319404   ]
    320 | cases daemon (*TODO*)
     405| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
     406  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
     407  #IH1 #IH2 #wf_all #st1' #Hst1' #REL
     408  cases(simulate_call_n … good … exe_12 … Hst1 … REL)
     409  #st1'' * #st1''' * #st2' * #tr1 **** #nps_st1'' #exe_12' #Hst1'' #Hst1''' * #tr2 *** #REL1 #sil_tr1
     410  #sil_tr2 #call_rel cases(IH1 … REL1)
     411  [2: inversion wf_all [ #st #EQ1 #EQ2 #EQ3 destruct]
     412      #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1 | * #y1 #EQ destruct(EQ) ] #_
     413      #EQ1 #EQ2 #EQ3 destruct #_ @(proj1 … (well_formed_append … wf_tl))
     414  |3: @(silent_io … (proj1 … sil_tr2)) assumption
     415  ]
     416  #st3' * #tr3 *** #pre_tr3 #wf_tr3 #EQcost_tr3 #REL2
     417  cases(simulate_ret_n … good … exe_34 … REL2) #Hst3' * #st3'' * #st4' * #st4'' *
     418  #tr4 *** #exe_34' #Hst3'' #Hst4' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3)
     419  [2: inversion wf_all in ⊢ ?; [#st #EQ1 #EQ2 destruct whd in ⊢ (????% → ?); #EQ destruct]
     420      #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1 | * #y1 #EQ destruct(EQ)] #_
     421      #EQ1 #EQ2 #EQ3 destruct #_ cases(well_formed_append … wf_tl) -wf_tl -wf_all
     422      #_ #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
     423      #z1 #z2 #z3 #w #prf' #tl' #wf_tl' [ #Hz1 | * #w1 #EQ destruct(EQ)] #_
     424      #EQ1 #EQ2 #EQ3 destruct #_ assumption
     425  |3: @(silent_io … (proj1 … sil_tr5)) assumption
     426  ]
     427  #st5' * #tr6 *** #pre_tr6 #wf_tr6 #EQcost_tr6 #REL4 %{st5'}
     428  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
     429  % [2: assumption] %
     430  [ %
     431     [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_tr1) ]
     432       %5
     433       [ @(silent_io … (proj1 … sil_tr1)) assumption
     434       | @(silent_io … (proj1 … sil_tr4)) assumption
     435       | whd %{f} %{l} %
     436       | 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)
     440       | @(RET_REL … call_rel) assumption
     441       | %
     442       ]
     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
     446       [ @append_well_formed try assumption @silent_is_well_formed assumption ]
     447       %2 [2: assumption] @append_well_formed try assumption @silent_is_well_formed
     448       assumption
     449     ]
     450  | >get_cost_label_invariant_for_append_silent_trace_l [2: @(proj1 … sil_tr1) ]
     451    whd in ⊢ (??%%); @eq_f >append_associative
     452    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
     453    [2: @(proj1 … sil_tr2) ] >append_associative
     454    >get_cost_label_append in ⊢ (???%);
     455    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
     456    [2: @(proj1 … sil_tr4) ] normalize
     457    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
     458    [2: @(proj1 …  sil_tr5) ] >get_cost_label_append in ⊢ (??%?); @eq_f2
     459    assumption
     460  ]
    321461]
    322 qed.
    323 
    324  
    325  
    326    #st3 #l #class_st1 #exe #tl * #x #EQ destruct(EQ) #pre_tl #IH
    327   #well_formed #s2 #class_s2 #REL cases(simulate_ret_l … good … exe … REL)
    328   #s2'' * #s2''' * #s2'''' * #t1 * #exe' * #t2 ** #Rs2s2'''' #t1_sil #t2_sil
    329   xxxxxxxxx
    330 
    331 
    332  #st4 #st5 #l1 #l2 * #x #EQ whd in ⊢ (% → ?);   
    333       @append_premeasurable_silent
    334    
    335     xxxxxxxxxxxxxx
    336   ]
    337 |*: cases daemon (*TODO*)
    338 ]
    339 qed.*)
     462qed.
     463
     464xxxxx
     465
    340466
    341467(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
     
    402528∀t : LR_raw_trace S.
    403529∀rel : relations S.
     530simulation_conditions … rel →
    404531measurable S t →
    405 ∀s1'.Srel … rel (LR_s1 … t) s1' →
     532∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' →
    406533∃ t' : LR_raw_trace S.
    407534measurable S t' ∧
     
    417544
    418545get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t').
    419 cases daemon (*TODO*)
     546#S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL
     547cases(simulates_pre_mesurable … (LR_t … t) … REL)
     548[2: @good |3: @pre_t |4: @wf_t |5: @Hs1' ]
     549#s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1
     550inversion(as_initial … (LR_s1 … t)) #Has_initial
     551inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry
     552inversion(as_final … (LR_s2 … t)) #Has_final
     553inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit
     554normalize nodelta
     555[ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2:
     556
     557
     558
    420559qed.
    421560
Note: See TracChangeset for help on using the changeset viewer.