Changeset 3576
 Timestamp:
 Jun 19, 2015, 1:56:43 PM (4 years ago)
 Location:
 LTS
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3574 r3576 175 175 #EQ destruct @H1 >(\P EQcond) % 176 176 ] 177 qed. 177 qed. 178 179 definition DeqInstructions ≝ λp,l_p.mk_DeqSet (Instructions p l_p) (eq_instructions p l_p) ?. 180 @hide_prf #i1 #i2 @eq_instructions_elim [ #EQ destruct % //  * #H % #EQ destruct cases H %] 181 qed. 182 183 unification hint 0 ≔ p,l_p; 184 X ≟ (DeqInstructions p l_p) 185 (*  *) ⊢ 186 (Instructions p l_p) ≡ carr X. 187 188 unification hint 0 ≔ p,l_p,p1,p2; 189 X ≟ (DeqInstructions p l_p) 190 (*  *) ⊢ 191 eq_instructions p l_p p1 p2 ≡ eqb X p1 p2. 178 192 179 193 record env_params : Type[1] ≝ … … 299 313 { env : list (env_item p p' l_p) 300 314 ; main : Instructions p' l_p 315 ; initial_act : NonFunctionalLabel l_p 301 316 }. 302 317 … … 306 321 λp,p',l_p,prog. 307 322 no_duplicates … 308 (foldr …323 (foldr ? (list (CostLabel l_p)) … 309 324 (λitem,acc.((a_call … (f_lab … item)) :: get_labels_of_code … (f_body … item)) @ acc) 310 ( get_labels_of_code … (main … prog)) (env … prog)).325 ((a_non_functional_label … (initial_act … prog)) :: (get_labels_of_code … (main … prog))) (env … prog)). 311 326 312 327 lemma no_duplicates_domain_of_fun: … … 314 329 ∀f,env_it.lookup p p' l_p (env … prog) f = return env_it → 315 330 no_duplicates … (get_labels_of_code … (f_body … env_it)). 316 #p #p' #l_p * #env elim env [ #main normalize #_ #f #env_it #EQ destruct(EQ)]317 #x #xs #IH #main whd in ⊢ (% → ?); whd in match (foldr ?????); #H #f #env_it331 #p #p' #l_p * #env elim env [ #main #initial_act normalize #_ #f #env_it #EQ destruct(EQ)] 332 #x #xs #IH #main #initial_act whd in ⊢ (% → ?); whd in match (foldr ?????); #H #f #env_it 318 333 whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta 319 334 [ whd in ⊢ (? → ???% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) cases H #_ /2/ ] … … 328 343 ]. 329 344 330 definition operational_semantics : ∀p : state_params.∀p'.Program p p p → abstract_status p ≝ 331 λp,p',prog.mk_abstract_status … 345 definition lang_initial : ∀p : state_params.sem_state_params p → Program p p p → state p → bool ≝ 346 λp,p',prog,st. 347 let spec_act ≝ cost_act … (Some ? (initial_act … prog)) in 348 eq_instructions … (code … st) (EMPTY …) ∧ 349 eqb_list … (cont … st) [〈spec_act,(main … prog)〉 ; 〈spec_act,EMPTY …〉] ∧ 350 store … st == init_store … p' ∧ io_info … st. 351 352 definition lang_final : ∀p.state p → bool ≝ 353 λp,st. 354 eq_instructions … (code … st) (EMPTY …) ∧ isnilb … (cont … st). 355 356 definition operational_semantics : ∀p : state_params.sem_state_params p → Program p p p → abstract_status p ≝ 357 λp,p',prog.mk_abstract_status ? 332 358 (state p) 333 359 (execute_l ? p' (env … prog)) … … 343 369  _ ⇒ false 344 370 ]) 345 (λs.eq_instructions … (code … s) (main … prog) ∧ isnilb … (cont … s) ∧ store … s == init_store … p' ∧ io_info … s) 346 (λs.match (cont … s) with 347 [ nil ⇒ match (code … s) with 348 [ EMPTY ⇒ true 349  RETURN _ ⇒ true 350  _ ⇒ false 351 ] 352  _ ⇒ false 353 ]) 371 (lang_initial … p' … prog) 372 (lang_final p) 354 373 ???. 355 374 @hide_prf … … 1032 1051 lemma fresh_aux_ok : ∀p,p',l_p.∀prog : Program p p' l_p.∀n,m.n ⊑^{l_p} m → 1033 1052 fresh_for_prog_aux … prog n ⊑^{l_p} fresh_for_prog_aux … prog m. 1034 #p #p' #l_p * #env #main elim env // #hd #tl #IH #n #m #H whd in ⊢ (???%%);1053 #p #p' #l_p * #env #main #init_act elim env // #hd #tl #IH #n #m #H whd in ⊢ (???%%); 1035 1054 @IH whd in ⊢ (???%?); @(monotonic_magg … l_p … H) 1036 1055 qed. … … 1057 1076 let info_main ≝ (call_post_trans … (main … prog) max_all (nil ?)) in 1058 1077 let 〈t_env,n,m,keep〉 ≝ translate_env … (env … prog) (fresh … info_main) in 1059 〈mk_Program ??? t_env (t_code … info_main) ,m @ (lab_map … info_main),keep @ (lab_to_keep … info_main)〉.1078 〈mk_Program ??? t_env (t_code … info_main) (initial_act … prog),m @ (lab_map … info_main),keep @ (lab_to_keep … info_main)〉. 1060 1079 1061 1080 definition map_labels_on_trace : ∀p : label_params. … … 1187 1206 lemma is_fresh_fresh_for_prog : ∀p,p',l_p.∀prog : Program p p' l_p. 1188 1207 is_fresh_for_return … (labels_of_prog … prog) (fresh_for_prog … prog). 1189 #p #p' #l_p * #env #main whd in match fresh_for_prog; normalize nodelta whd in ⊢ (??%?);1208 #p #p' #l_p * #env #main #initial_act whd in match fresh_for_prog; normalize nodelta whd in ⊢ (??%?); 1190 1209 elim env // * #sig #cost #i #tail #IH whd in ⊢ (??%?); @fresh_append 1191 1210 [ @(fresh_keep_n_ok … IH) @fresh_aux_ok @max_1 // 1192 1211  @(fresh_keep_n_ok … (is_fresh_code … i)) whd in match fresh_for_prog_aux; normalize nodelta 1193 1212 whd in ⊢ (????%); elim tail [ @max_2 // ] #hd1 #tl1 #IH1 @(trans_po_rel … IH1) 1194 whd in ⊢ (????%); change with (fresh_for_prog_aux ??? (mk_Program ??? tl1 main ) ?) in ⊢ (???%%);1213 whd in ⊢ (????%); change with (fresh_for_prog_aux ??? (mk_Program ??? tl1 main initial_act) ?) in ⊢ (???%%); 1195 1214 @fresh_aux_ok @max_1 // 1196 1215 ] … … 1210 1229 ∀t_prog,m,keep.trans_prog … prog = 〈t_prog,m,keep〉 → 1211 1230 (cast_return_to_cost_labels l_p keep) ⊆ (labels_of_prog p p' l_p prog). 1212 #p #p' #l_p * #env #main # t_prog #m #keep whd in match trans_prog; normalize nodelta1231 #p #p' #l_p * #env #main #initial_act #t_prog #m #keep whd in match trans_prog; normalize nodelta 1213 1232 @pair_elim * #env1 #fresh * #m1 #keep1 #EQenv1 normalize nodelta #EQ destruct 1214 1233 lapply EQenv1 EQenv1 lapply keep1 keep1 lapply m1 m1 lapply fresh fresh … … 1227 1246 >memb_append_l2 // @(lab_to_keep_in_domain … H) 1228 1247  whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); 1229 change with (labels_of_prog ??? (mk_Program ??? xs ? )) in match (foldr ?????);1248 change with (labels_of_prog ??? (mk_Program ??? xs ? initial_act)) in match (foldr ?????); 1230 1249 @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail)) 1231 1250 >cast_return_append @subset_append_h1 // 1232 1251 ] 1233 1252  whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); 1234 change with (labels_of_prog ??? (mk_Program ??? xs ? )) in match (foldr ?????);1253 change with (labels_of_prog ??? (mk_Program ??? xs ? initial_act)) in match (foldr ?????); 1235 1254 @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail)) 1236 1255 >cast_return_append @subset_append_h2 // … … 1269 1288 lapply EQt_prog normalize nodelta 1270 1289 generalize in match keep0 in ⊢ (% → ? → ? → ? → ? → ??(λ_.??(λ_.?%?))); 1271 #keep1 #EQkeep1 inversion prog in EQt_prog; #env #main # EQprog1290 #keep1 #EQkeep1 inversion prog in EQt_prog; #env #main #initial_act #EQprog 1272 1291 whd in match trans_prog; normalize nodelta 1273 1292 @pair_elim 1274 cut(fresh_for_prog ??? prog ⊑^{p} fresh_for_prog ??? (mk_Program … env main )) [ >EQprog //]1293 cut(fresh_for_prog ??? prog ⊑^{p} fresh_for_prog ??? (mk_Program … env main initial_act)) [ >EQprog //] 1275 1294 generalize in match (fresh_for_prog ????) in ⊢ (????% → %); 1276 1295 lapply t_prog0 lapply m0 lapply keep0 … … 1281 1300 * #m_tail #keep_tail change with (translate_env ?????) in ⊢ (??%? → ?); #EQtail normalize nodelta #EQ1 destruct(EQ1) #EQ2 destruct(EQ2) 1282 1301 whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H) 1283 change with (no_duplicates_labels p p p (mk_Program p p p tail main )) in match1284 (no_duplicates_labels p p p (mk_Program p p p tail main )); #no_dup_tail1302 change with (no_duplicates_labels p p p (mk_Program p p p tail main initial_act)) in match 1303 (no_duplicates_labels p p p (mk_Program p p p tail main initial_act)); #no_dup_tail 1285 1304 lapply(no_duplicates_append_l … H) #no_dup_head normalize nodelta 1286 1305 #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta … … 1303 1322 normalize nodelta >get_element_append_l1 1304 1323 [2: % #ABS @(memb_no_duplicates_append … x … H) // elim tail 1305 [ whd in match (foldr ?????); @lab_map_in_domain // ] 1324 [ whd in match (foldr ?????); 1325 change with (orb ??) in match (orb ??); @orb_Prop_r 1326 @lab_map_in_domain // ] 1306 1327 #x #xs #IH whd in match (foldr ?????); @orb_Prop_r 1307 1328 >memb_append_l2 // >IH % 
LTS/Traces.ma
r3549 r3576 277 277 ] 278 278 ]. 279 280 lemma eq_ActionLabel_elim : ∀P : bool → Prop.∀p,c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) → P (eq_ActionLabel p c1 c2). 281 #P #p * [#f #lab  * [ #lab]  * [ #lab] ] * 282 [1,4,7,10,13: #f' #lab' 2,5,8,14: * [2,4,6,8: #lab'] *: * [2,4,6,8,10,12: #lab'] ] #H1 #H2 283 whd in match eq_ActionLabel; normalize nodelta 284 try(@H2 % #EQ destruct) 285 [ @eq_function_name_elim [ @eq_call_cost_lab_elim [ #H #_ lapply H H ] ]  @eq_return_cost_lab_elim   @eq_fn_label_elim ] 286 normalize nodelta 287 [1,4,6,7,9: try(#EQ destruct) try(#EQ destruct) @H1 % 288 *: * #H @H2 % #EQ destruct cases H % 289 ] 290 qed. 291 292 definition DeqActionLabel ≝ λp.mk_DeqSet (ActionLabel p) (eq_ActionLabel p) ?. 293 @hide_prf #x #y @eq_ActionLabel_elim [ #EQ destruct % //  * #H % #EQ destruct cases H %] 294 qed. 295 296 unification hint 0 ≔ p ; 297 X ≟ (DeqActionLabel p) 298 (*  *) ⊢ 299 (ActionLabel p) ≡ carr X. 300 301 unification hint 0 ≔ p,p1,p2; 302 X ≟ (DeqActionLabel p) 303 (*  *) ⊢ 304 eq_ActionLabel p p1 p2 ≡ eqb X p1 p2. 279 305 280 306 definition is_cost_label : ∀p.ActionLabel p → Prop ≝
Note: See TracChangeset
for help on using the changeset viewer.