Changeset 2869


Ignore:
Timestamp:
Mar 14, 2013, 3:40:01 PM (4 years ago)
Author:
tranquil
Message:

some reorganization of definitions, and a new taaf_append_taaf

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/StatusSimulation.ma

    r2799 r2869  
    5353                 call_rel ?? R s1_pre s2_pre →
    5454                 as_after_return S2 s2_pre s2_ret.
    55 
    56 (* the equivalent of a collapsable trace_any_label where we do not force
    57    costedness of the lookahead status *)
    58 inductive trace_any_any_free (S : abstract_status) : S → S → Type[0] ≝
    59 | taaf_base : ∀s.trace_any_any_free S s s
    60 | taaf_step : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
    61   as_classifier S s2 cl_other →
    62   trace_any_any_free S s1 s3
    63 | taaf_step_jump : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
    64   as_classifier S s2 cl_jump →
    65   as_costed S s3 →
    66   trace_any_any_free S s1 s3.
    67 
    68 definition taaf_non_empty ≝ λS,s1,s2.λtaaf : trace_any_any_free S s1 s2.
    69 match taaf with
    70 [ taaf_base _ ⇒ false
    71 | _ ⇒ true
    72 ].
    7355
    7456(* the base property we ask for simulation to work depends on the status_class
     
    172154(* some useful lemmas *)
    173155
    174 let rec taa_append_taa S st1 st2 st3
    175   (taa : trace_any_any S st1 st2) on taa :
    176   trace_any_any S st2 st3 →
    177   trace_any_any S st1 st3 ≝
    178   match taa
    179   with
    180   [ taa_base st1' ⇒ λst3,taa2.taa2
    181   | taa_step st1' st2' st3' H I J tl ⇒ λst3,taa2.
    182     taa_step ???? H I J (taa_append_taa … tl taa2)
    183   ] st3.
    184 
    185 definition taaf_to_taa : ∀S : abstract_status.∀s1,s2,taaf.
    186 if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
    187 trace_any_any S s1 s2 ≝
    188 λS,s1,s2,taaf.
    189 match taaf return λs1,s2,taaf.if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
    190   trace_any_any S s1 s2 with
    191 [ taaf_base s ⇒ λ_.taa_base …
    192 | taaf_step s1 s2 s3 taa ex cl ⇒ λncost.
    193   taa_append_taa … taa (taa_step … ex cl ncost (taa_base …))
    194 | taaf_step_jump s1 s2 s3 taa ex cl cost ⇒ λncost.Ⓧ(absurd … cost ncost)
    195 ].
    196 
    197 lemma associative_taa_append_tal : ∀S,s1,s2,fl,s3,s4.
    198   ∀taa1 : trace_any_any S s1 s2.
    199   ∀taa2 : trace_any_any S s2 s3.
    200   ∀tal : trace_any_label S fl s3 s4.
    201   (taa_append_taa … taa1 taa2) @ tal = taa1 @ taa2 @ tal.
    202 #S #s1 #s2 #fl #s3 #s4 #taa1 elim taa1 -s1 -s2
    203 [ #s1 #taa2 #tal %
    204 | #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
    205   normalize >IH %
    206 ]
    207 qed.
    208 
    209 lemma associative_taa_append_taa : ∀S,s1,s2,s3,s4.
    210   ∀taa1 : trace_any_any S s1 s2.
    211   ∀taa2 : trace_any_any S s2 s3.
    212   ∀taa3 : trace_any_any S s3 s4.
    213   taa_append_taa … (taa_append_taa … taa1 taa2) taa3 =
    214   taa_append_taa … taa1 (taa_append_taa … taa2 taa3).
    215 #S #s1 #s2 #s3 #s4 #taa1 elim taa1 -s1 -s2
    216 [ #s1 #taa2 #tal %
    217 | #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
    218   normalize >IH %
    219 ]
    220 qed.
    221 
    222156let rec taa_append_tal_rel S1 fl1 st1 st1'
    223157  (tal1 : trace_any_label S1 fl1 st1 st1')
     
    343277%[|%[|%[|%[|%[| % ]]]]]
    344278qed.
    345 
    346 definition taaf_append_tal : ∀S,st1,fl,st2,st3.
    347   ∀taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
    348   trace_any_label S fl st1 st3 ≝ λS,st1,fl,st2,st3,taaf.
    349   match taaf return λst1,st2,taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
    350   trace_any_label S fl st1 st3 with
    351   [ taaf_base s ⇒ λ_.λtal.tal
    352   | taaf_step s1 s2 s3 hd H I ⇒ λJ,tal.hd @ tal_step_default ????? H tal I J
    353   | taaf_step_jump _ _ s3 _ _ _ K ⇒ λJ.Ⓧ(absurd … K J)
    354   ]. 
    355279
    356280lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
  • src/common/StructuredTraces.ma

    r2824 r2869  
    11221122@(tll_rel_to_traces_same_observables … H_tlr) %
    11231123qed.
     1124
     1125(* the equivalent of a collapsable trace_any_label where we do not force
     1126   costedness of the lookahead status *)
     1127inductive trace_any_any_free (S : abstract_status) : S → S → Type[0] ≝
     1128| taaf_base : ∀s.trace_any_any_free S s s
     1129| taaf_step : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
     1130  as_classifier S s2 cl_other →
     1131  trace_any_any_free S s1 s3
     1132| taaf_step_jump : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
     1133  as_classifier S s2 cl_jump →
     1134  as_costed S s3 →
     1135  trace_any_any_free S s1 s3.
     1136
     1137definition taaf_non_empty ≝ λS,s1,s2.λtaaf : trace_any_any_free S s1 s2.
     1138match taaf with
     1139[ taaf_base _ ⇒ false
     1140| _ ⇒ true
     1141].
     1142
     1143(* utilities on taa and taaf *)
     1144
     1145let rec taa_append_taa S st1 st2 st3
     1146  (taa : trace_any_any S st1 st2) on taa :
     1147  trace_any_any S st2 st3 →
     1148  trace_any_any S st1 st3 ≝
     1149  match taa
     1150  with
     1151  [ taa_base st1' ⇒ λst3,taa2.taa2
     1152  | taa_step st1' st2' st3' H I J tl ⇒ λst3,taa2.
     1153    taa_step ???? H I J (taa_append_taa … tl taa2)
     1154  ] st3.
     1155
     1156definition taaf_to_taa : ∀S : abstract_status.∀s1,s2,taaf.
     1157if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
     1158trace_any_any S s1 s2 ≝
     1159λS,s1,s2,taaf.
     1160match taaf return λs1,s2,taaf.if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
     1161  trace_any_any S s1 s2 with
     1162[ taaf_base s ⇒ λ_.taa_base …
     1163| taaf_step s1 s2 s3 taa ex cl ⇒ λncost.
     1164  taa_append_taa … taa (taa_step … ex cl ncost (taa_base …))
     1165| taaf_step_jump s1 s2 s3 taa ex cl cost ⇒ λncost.Ⓧ(absurd … cost ncost)
     1166].
     1167
     1168lemma associative_taa_append_tal : ∀S,s1,s2,fl,s3,s4.
     1169  ∀taa1 : trace_any_any S s1 s2.
     1170  ∀taa2 : trace_any_any S s2 s3.
     1171  ∀tal : trace_any_label S fl s3 s4.
     1172  (taa_append_taa … taa1 taa2) @ tal = taa1 @ taa2 @ tal.
     1173#S #s1 #s2 #fl #s3 #s4 #taa1 elim taa1 -s1 -s2
     1174[ #s1 #taa2 #tal %
     1175| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
     1176  normalize >IH %
     1177]
     1178qed.
     1179
     1180lemma associative_taa_append_taa : ∀S,s1,s2,s3,s4.
     1181  ∀taa1 : trace_any_any S s1 s2.
     1182  ∀taa2 : trace_any_any S s2 s3.
     1183  ∀taa3 : trace_any_any S s3 s4.
     1184  taa_append_taa … (taa_append_taa … taa1 taa2) taa3 =
     1185  taa_append_taa … taa1 (taa_append_taa … taa2 taa3).
     1186#S #s1 #s2 #s3 #s4 #taa1 elim taa1 -s1 -s2
     1187[ #s1 #taa2 #tal %
     1188| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
     1189  normalize >IH %
     1190]
     1191qed.
     1192
     1193definition taaf_append_tal : ∀S,st1,fl,st2,st3.
     1194  ∀taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
     1195  trace_any_label S fl st1 st3 ≝ λS,st1,fl,st2,st3,taaf,prf.
     1196  taa_append_tal … (taaf_to_taa … prf).
     1197
     1198definition taaf_append_taa : ∀S,st1,st2,st3.
     1199  ∀taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_any S st2 st3 →
     1200  trace_any_any S st1 st3 ≝ λS,st1,st2,st3,taaf,prf.
     1201  taa_append_taa … (taaf_to_taa … prf).
     1202
     1203definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3.
     1204  as_execute S s1 s2 →
     1205  as_classifier … s1 cl_other →
     1206  ∀taaf : trace_any_any_free S s2 s3.
     1207  (if taaf_non_empty … taaf then ¬as_costed … s2 else True) →
     1208  trace_any_any_free S s1 s3 ≝
     1209λS,s1,s2,s3,H,I,tl.
     1210match tl return λs2,s3,tl.
     1211  as_execute … s1 s2 →
     1212  if taaf_non_empty … tl then ¬as_costed … s2 else True →
     1213  trace_any_any_free S s1 s3
     1214with
     1215[ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I
     1216| taaf_step s2 s3 s4 taa H' I' ⇒
     1217  λH,J.taaf_step … (taa_step … H I J taa) H' I'
     1218| taaf_step_jump s2 s3 s4 taa H' I' K' ⇒
     1219  λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K'
     1220] H.
     1221
     1222lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J.
     1223bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)).
     1224#S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl
     1225[ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ]
     1226qed.
     1227
     1228definition taaf_append_taaf :
     1229  ∀S,st1,st2,st3.
     1230  ∀taaf1 : trace_any_any_free S st1 st2.
     1231  ∀taaf2 : trace_any_any_free S st2 st3.
     1232  if taaf_non_empty … taaf2 ∧ taaf_non_empty … taaf1 then ¬as_costed … st2 else True →
     1233  trace_any_any_free S st1 st3 ≝
     1234λS,st1,st2,st3,taaf1,taaf2.
     1235match taaf2 return λst2,st3,taaf2.
     1236  ∀taaf1 : trace_any_any_free S st1 st2.
     1237  if taaf_non_empty … taaf2 ∧ taaf_non_empty … taaf1 then ¬as_costed … st2 else True →
     1238  trace_any_any_free S st1 st3 with
     1239[ taaf_base s1 ⇒ λtaaf1.λ_.taaf1
     1240| taaf_step s1 s2 s3 taa H' I' ⇒ λtaaf1,prf.
     1241  taaf_step … (taaf_append_taa … taaf1 ? taa) H' I'
     1242| taaf_step_jump s2 s3 s4 taa H' I' K' ⇒ λtaaf1,prf.
     1243  taaf_step_jump … (taaf_append_taa … taaf1 ? taa) H' I' K'
     1244] taaf1. @prf qed.
  • src/joint/semantics_blocks.ma

    r2817 r2869  
    1414  λp : evaluation_params.λcurr_id.
    1515  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id).
    16 
    17 definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3.
    18   as_execute S s1 s2 →
    19   as_classifier … s1 cl_other →
    20   ∀taaf : trace_any_any_free S s2 s3.
    21   (if taaf_non_empty … taaf then ¬as_costed … s2 else True) →
    22   trace_any_any_free S s1 s3 ≝
    23 λS,s1,s2,s3,H,I,tl.
    24 match tl return λs2,s3,tl.
    25   as_execute … s1 s2 →
    26   if taaf_non_empty … tl then ¬as_costed … s2 else True →
    27   trace_any_any_free S s1 s3
    28 with
    29 [ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I
    30 | taaf_step s2 s3 s4 taa H' I' ⇒
    31   λH,J.taaf_step … (taa_step … H I J taa) H' I'
    32 | taaf_step_jump s2 s3 s4 taa H' I' K' ⇒
    33   λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K'
    34 ] H.
    35 
    36 lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J.
    37 bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)).
    38 #S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl
    39 [ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ]
    40 qed.
    4116
    4217lemma produce_step_trace :
Note: See TracChangeset for help on using the changeset viewer.