# Changeset 3389 for LTS/Simulation.ma

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

Ended simulation proof

File:
1 edited

Unmodified
Added
Removed
• ## LTS/Simulation.ma

 r3388 ∃s2',s2'',s2'''. ∃t1: raw_trace S s2 s2'. as_execute … (call_act f l) s2' s2'' ∧ bool_to_Prop (¬ is_call_post_label … s2') ∧ as_execute … (call_act f l) s2' s2'' ∧ as_classify … s2' ≠ cl_jump ∧ as_classify … s2'' ≠ cl_io ∧ ∃t3: raw_trace S s2'' s2'''. Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 ∀s1,s2,s1' : S. as_execute … (ret_act (None ?)) s1 s1' → Srel … rel s1 s2 → Srel … rel s1 s2 → as_classify … s2 ≠ cl_io ∧ ∃s2',s2'',s2'''. ∃t1: raw_trace S s2 s2'. as_execute … (ret_act (None ?)) s2' s2''  ∧ as_execute … (ret_act (None ?)) s2' s2''  ∧ as_classify … s2' ≠ cl_jump ∧ as_classify … s2'' ≠ cl_io ∧ ∃t3: raw_trace S s2'' s2'''. Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 ∧ Rrel … rel s2 s2'' ∧ Rrel … rel s1' s2'' }. qed. lemma pre_silent_is_premeasurable : ∀S : abstract_status. ∀st1,st2 : S. ∀t : raw_trace S st1 st2.as_classify … st1 ≠cl_io → pre_silent_trace … t → pre_measurable_trace … t. #S #st1 #st2 #t elim t [ #st #Hst #H inversion H in ⊢ ?; [ #st' #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ] #st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ] -t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #Hst1 #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ] @IH [ >Hst2' % #EQ destruct | assumption] qed. lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l. ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3. ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2. #S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed. lemma append_silent_premeasurable : ∀S : abstract_status. ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1. pre_measurable_trace … t' → pre_silent_trace … t → as_classify … st1 ≠ cl_io → pre_measurable_trace … (t' @ t). #S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht' [ normalize #st #Hst #r #H1 #H2 @pre_silent_is_premeasurable assumption |2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r #Hs3 [ %2 | %3 | %4 ] try ( %{x} %) try @IH try assumption % ] #s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1' #EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2 #r #pre_r #Hs5 normalize cut(∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l. ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3. ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2) [ @append_tind_commute ] #H >H >H >append_associative (H1 I) % #EQ destruct] qed. lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status. ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. qed. lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S. ∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3. get_costlabels_of_trace … (t1 @ t2) = append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2). #S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' * [#f * #l | * [| * #l] | *  [| #l] |] #prf #tl #IH #t2 normalize try @eq_f @IH qed. (* lemma raw_trace_ind_r : ∀S : abstract_status. ] ] | cases daemon (*TODO*) | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 * #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct #IH1 #IH2 #wf_all #st1' #Hst1' #REL cases(simulate_call_n … good … exe_12 … Hst1 … REL) #st1'' * #st1''' * #st2' * #tr1 **** #nps_st1'' #exe_12' #Hst1'' #Hst1''' * #tr2 *** #REL1 #sil_tr1 #sil_tr2 #call_rel cases(IH1 … REL1) [2: inversion wf_all [ #st #EQ1 #EQ2 #EQ3 destruct] #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1 | * #y1 #EQ destruct(EQ) ] #_ #EQ1 #EQ2 #EQ3 destruct #_ @(proj1 … (well_formed_append … wf_tl)) |3: @(silent_io … (proj1 … sil_tr2)) assumption ] #st3' * #tr3 *** #pre_tr3 #wf_tr3 #EQcost_tr3 #REL2 cases(simulate_ret_n … good … exe_34 … REL2) #Hst3' * #st3'' * #st4' * #st4'' * #tr4 *** #exe_34' #Hst3'' #Hst4' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: inversion wf_all in ⊢ ?; [#st #EQ1 #EQ2 destruct whd in ⊢ (????% → ?); #EQ destruct] #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1 | * #y1 #EQ destruct(EQ)] #_ #EQ1 #EQ2 #EQ3 destruct #_ cases(well_formed_append … wf_tl) -wf_tl -wf_all #_ #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct] #z1 #z2 #z3 #w #prf' #tl' #wf_tl' [ #Hz1 | * #w1 #EQ destruct(EQ)] #_ #EQ1 #EQ2 #EQ3 destruct #_ assumption |3: @(silent_io … (proj1 … sil_tr5)) assumption ] #st5' * #tr6 *** #pre_tr6 #wf_tr6 #EQcost_tr6 #REL4 %{st5'} %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))} % [2: assumption] % [ % [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_tr1) ] %5 [ @(silent_io … (proj1 … sil_tr1)) assumption | @(silent_io … (proj1 … sil_tr4)) assumption | whd %{f} %{l} % | assumption | @append_premeasurable_silent try assumption [2: @(proj1 … sil_tr2)] @append_silent_premeasurable try assumption @(proj1 … sil_tr4) | @append_premeasurable_silent try assumption @(proj1 … sil_tr5) | @(RET_REL … call_rel) assumption | % ] | @append_well_formed_silent [2: @(proj1 … sil_tr1) |3: @(proj2 … sil_tr1) ] %2 [2: assumption] >append_associative @append_well_formed_silent [2: @(proj1 … sil_tr2) |3: @(proj2 … sil_tr2) ] @append_well_formed [ @append_well_formed try assumption @silent_is_well_formed assumption ] %2 [2: assumption] @append_well_formed try assumption @silent_is_well_formed assumption ] | >get_cost_label_invariant_for_append_silent_trace_l [2: @(proj1 … sil_tr1) ] whd in ⊢ (??%%); @eq_f >append_associative >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); [2: @(proj1 … sil_tr2) ] >append_associative >get_cost_label_append in ⊢ (???%); >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); [2: @(proj1 … sil_tr4) ] normalize >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); [2: @(proj1 …  sil_tr5) ] >get_cost_label_append in ⊢ (??%?); @eq_f2 assumption ] ] qed. #st3 #l #class_st1 #exe #tl * #x #EQ destruct(EQ) #pre_tl #IH #well_formed #s2 #class_s2 #REL cases(simulate_ret_l … good … exe … REL) #s2'' * #s2''' * #s2'''' * #t1 * #exe' * #t2 ** #Rs2s2'''' #t1_sil #t2_sil xxxxxxxxx #st4 #st5 #l1 #l2 * #x #EQ whd in ⊢ (% → ?); @append_premeasurable_silent xxxxxxxxxxxxxx ] |*: cases daemon (*TODO*) ] qed.*) qed. xxxxx (* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio ∀t : LR_raw_trace S. ∀rel : relations S. simulation_conditions … rel → measurable S t → ∀s1'.Srel … rel (LR_s1 … t) s1' → ∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' → ∃ t' : LR_raw_trace S. measurable S t' ∧ ∧ get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t'). cases daemon (*TODO*) #S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL cases(simulates_pre_mesurable … (LR_t … t) … REL) [2: @good |3: @pre_t |4: @wf_t |5: @Hs1' ] #s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1 inversion(as_initial … (LR_s1 … t)) #Has_initial inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry inversion(as_final … (LR_s2 … t)) #Has_final inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit normalize nodelta [ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2: qed.
Note: See TracChangeset for help on using the changeset viewer.