 Timestamp:
 Jan 24, 2014, 5:38:33 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3414 r3416 462 462 463 463 definition fresh_rc_label : ℕ → ReturnPostCostLabel × ℕ ≝ 464 λx.〈a_return_cost_label x,S x〉.464 λx.〈a_return_cost_label (S x),S x〉. 465 465 466 466 record call_post_info (p : instr_params) : Type[0] ≝ … … 898 898 qed. 899 899 900 let rec is_fresh_ keep (keep : list ReturnPostCostLabel) (n : ℕ) on keep : Prop ≝900 let rec is_fresh_for_return (keep : list CostLabel) (n : ℕ) on keep : Prop ≝ 901 901 match keep with 902 902 [ nil ⇒ True 903  cons x xs ⇒ let ih ≝ is_fresh_ keepxs n in903  cons x xs ⇒ let ih ≝ is_fresh_for_return xs n in 904 904 match x with 905 [ a_return_cost_label m ⇒ m < n ∧ ih ] 905 [ a_return_post y ⇒ match y with [a_return_cost_label m ⇒ m ≤ n ∧ ih ] 906  _ ⇒ ih 907 ] 906 908 ]. 907 909 … … 917 919 918 920 lemma fresh_keep_n_ok : ∀n,m,l. 919 is_fresh_keep l n → n ≤ m → is_fresh_keep l m. 920 #n #m #l lapply n n lapply m m elim l // * #x #xs #IH #n #m 921 normalize * #H1 #H2 #H3 % /2 by transitive_le/ 922 qed. 923 924 lemma fresh_false : ∀n,l.is_fresh_keep l n → a_return_cost_label n ∈ l = false. 925 #n #l lapply n n elim l // * #x #xs #IH #n whd in ⊢ (% → ??%?); * #H1 #H2 926 whd in match (eqb ???); @eqb_elim 921 is_fresh_for_return l n → n ≤ m → is_fresh_for_return l m. 922 #n #m #l lapply n n lapply m m elim l // ** #x #xs #IH #n #m 923 normalize [2: * #H1] #H2 #H3 [ %] /2 by transitive_le/ 924 qed. 925 926 definition cast_return_to_cost_labels ≝ map … (a_return_post …). 927 coercion cast_return_to_cost_labels. 928 929 lemma fresh_false : ∀n.∀l: list ReturnPostCostLabel.is_fresh_for_return l n → 930 a_return_cost_label (S n) ∈ l = false. 931 #n #l lapply n n elim l // * #x #xs #IH #n whd in ⊢ (% → ??%?); * #H1 932 #H2 @eq_return_cost_lab_elim 927 933 [ #EQ destruct @⊥ /2 by absurd/ 928 934  #_ >IH // 929 935 ] 930 936 qed. 931 932 937 933 938 lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ. … … 938 943 same_fresh_map_on dom (lab_map … info) m → 939 944 same_to_keep_on dom (lab_to_keep … info) keep → 940 is_fresh_ keepkeep n →945 is_fresh_for_return keep n → 941 946 call_post_clean ? (t_code ? info) m keep l 942 947 = return 〈gen_labels … info,i1〉. … … 1108 1113 >(IH … (refl …)) 1109 1114 [1,6: normalize nodelta 1110 [ >fresh_false [2: /2 by fresh_keep_n_ok/ 1115 [ >fresh_false [2: /2 by fresh_keep_n_ok/] % 1111 1116  <same_keep 1112 1117 [ whd in match (memb ???); >(\b (refl …)) normalize nodelta … … 1155 1160 ] 1156 1161 ] 1157 qed. 1158 1159 1160 1161 definition trans_prog : ∀p,p'.Program p p' → 1162 (Program p p') × (associative_list DEQCostLabel CostLabel) × (list ReturnPostCostLabel)≝ 1163 λp,p',prog. 1164 let max_all ≝ foldl … (λn,i.max n (compute_max_n … (f_body … i))) O (env … prog) in 1165 let 〈t_env,n,m,keep〉 ≝ (foldr ?? 1162 qed. 1163 1164 definition fresh_for_prog : ∀p,p'.Program p p' → ℕ ≝ 1165 λp,p',prog.foldl … (λn,i.max n (compute_max_n … (f_body … i))) 1166 (compute_max_n … (main … prog)) (env … prog). 1167 1168 definition translate_env ≝ 1169 λp,p'.λenv : list (env_item p p').λmax_all.(foldr ?? 1166 1170 (λi,x.let 〈t_env,n,m,keep〉 ≝ x in 1167 1171 let info ≝ call_post_trans … (f_body … i) n (nil ?) in … … 1171 1175 fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 :: 1172 1176 ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉) 1173 (〈nil ?,max_all,nil ?,nil ?〉) (env … prog)) in 1174 〈mk_Program ?? t_env (t_code … (call_post_trans … (main … prog) n (nil ?))),m,keep〉 . 1177 (〈nil ?,max_all,nil ?,nil ?〉) env). 1178 1179 definition trans_prog : ∀p,p'.Program p p' → 1180 ((Program p p') × (associative_list DEQCostLabel CostLabel)) × ((list ReturnPostCostLabel))≝ 1181 λp,p',prog. 1182 let max_all ≝ fresh_for_prog … prog in 1183 let info_main ≝ (call_post_trans … (main … prog) max_all (nil ?)) in 1184 let 〈t_env,n,m,keep〉 ≝ translate_env … (env … prog) (fresh … info_main) in 1185 〈mk_Program ?? t_env (t_code … info_main),m @ (lab_map … info_main),keep @ (lab_to_keep … info_main)〉. 1175 1186 1176 1187 definition map_labels_on_trace : … … 1298 1309 (* aggiungere fresh_to_keep al lemma seguente??*) 1299 1310 1300 xxxxxxx 1301 1311 let rec subset (A : Type[0]) (l1,l2 : list A) on l1 : Prop ≝ 1312 match l1 with 1313 [ nil ⇒ True 1314  cons x xs ⇒ mem … x l2 ∧ subset … xs l2 1315 ]. 1316 1317 interpretation "subset" 'subseteq a b = (subset ? a b). 1318 1319 lemma subset_append_l2 : ∀A,l2,l1.subset A l2 (l1 @ l2). 1320 #A #l2 elim l2 // normalize #x #xs #IH #l1 % // @mem_append_l2 whd /2/ 1321 qed. 1322 1323 lemma refl_subset : ∀A.reflexive … (subset A). 1324 #A #l1 elim l1 // #x #xs #IH normalize % /2/ 1325 qed. 1326 1327 lemma fresh_for_subset : ∀l1,l2,n.l1 ⊆ l2 → is_fresh_for_return … l2 n → 1328 is_fresh_for_return … l1 n. 1329 #l1 elim l1 // ** #x #xs #IH #l2 #n * #H1 #H2 #H3 whd 1330 try(@IH) // % [2: @IH //] elim l2 in H1 H3; normalize [*] 1331 ** #y #ys #IH normalize 1332 [2,3: * [2,4: #H3 [2: @IH //] * #H4 #H5 @IH // 1333 *: #EQ destruct * // 1334 ]] 1335 * 1336 [ #EQ destruct ] #H3 #H4 @IH // 1337 qed. 1338 1339 lemma fresh_append : ∀n,l1,l2.is_fresh_for_return l1 n → is_fresh_for_return l2 n → 1340 is_fresh_for_return (l1@l2) n. 1341 #n #l1 lapply n n elim l1 // ** #x #xs #IH #n #l2 [2: * #H1 ] #H2 #H3 1342 [ % // @IH //] @IH // 1343 qed. 1344 1345 definition labels_of_prog : ∀p,p'.Program p p' → ? ≝ 1346 λp,p',prog.foldr … (λx,l.l @ (get_labels_of_code … (f_body … x))) [ ] (env … prog). 1347 1348 lemma cast_return_append : ∀l1,l2.cast_return_to_cost_labels … (l1 @ l2) = 1349 (cast_return_to_cost_labels … l1) @ (cast_return_to_cost_labels … l2). 1350 #l1 #l2 @(sym_eq … (map_append …)) qed. 1302 1351 1303 1352 lemma trans_env_ok : ∀p : state_params.∀ prog. … … 1305 1354 let 〈t_prog,m,keep〉 ≝ trans_prog … prog in 1306 1355 ∀f,env_it.lookup p p (env … prog) f = return env_it → 1307 let dom ≝ get_labels_of_code … (f_body … env_it) in 1308 ∃env_it',n. lookup p p (env … t_prog) f = return env_it' ∧1356 let dom ≝ get_labels_of_code … (f_body … env_it) in 1357 ∃env_it',n.is_fresh_for_return keep n ∧lookup p p (env … t_prog) f = return env_it' ∧ 1309 1358 let info ≝ call_post_trans … (f_body … env_it) n (nil ?) in 1310 1359 t_code … info = f_body … env_it' ∧ … … 1312 1361 f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it' ∧ 1313 1362 same_fresh_map_on dom m (lab_map … info) ∧ same_to_keep_on dom keep (lab_to_keep … info). 1314 #p * #env #main @pair_elim * whd in match trans_prog; normalize nodelta 1315 @pair_elim generalize in match O; elim env 1316 [ #fresh1 * #env' #fresh #x #_ #t_prog #m #keep #_ #_ #f #env_it normalize in ⊢ (% → ?); #ABS destruct] 1317 * #hd_sig #hd_lab #hd_code #tail #IH #fresh1 * #env' #fresh * #m' #keep' 1363 #p #prog inversion(trans_prog … prog) * #t_prog0 #m0 #keep0 #EQt_prog 1364 lapply EQt_prog normalize nodelta 1365 generalize in match keep0 in ⊢ (% → ? → ? → ? → ? → ??(λ_.??(λ_.?%?))); 1366 #keep1 #EQkeep1 inversion prog in EQt_prog; #env #main #EQprog 1367 whd in match trans_prog; normalize nodelta 1368 @pair_elim 1369 cut(fresh_for_prog ?? prog ≤ fresh_for_prog ?? (mk_Program … env main)) [ >EQprog //] 1370 generalize in match (fresh_for_prog ???) in ⊢ (??% → %); 1371 lapply t_prog0 lapply m0 lapply keep0 1372 elim env in ⊢ (?→ ? → ? → ? → ? → %); 1373 [ #keep #m #t_prog #n #_ * #env' #fresh * #x #y #_ #_ #_ #f #env_it normalize in ⊢ (% → ?); #ABS destruct] 1374 * #hd_sig #hd_lab #hd_code #tail #IH #keep #m #t_prog #fresh1 #Hfresh1 * #env' #fresh * #m' #keep' 1318 1375 normalize in ⊢ (% → ?); normalize nodelta @pair_elim * #env_tail #fresh_tail 1319 * #m_tail #keep_tail #EQtail normalize nodelta #EQ1 destruct(EQ1) #t_prog 1320 #m #keep #EQ2 destruct(EQ2) 1376 * #m_tail #keep_tail change with (translate_env ????) in ⊢ (??%? → ?); #EQtail normalize nodelta #EQ1 destruct(EQ1) #EQ2 destruct(EQ2) 1321 1377 whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H) 1322 1378 change with (no_duplicates_labels p p (mk_Program p p tail main)) in match … … 1327 1383 inversion (call_post_trans … hd_code fresh_tail []) 1328 1384 #gen_labs #t_hd_code #t_fresh #t_lab_map #t_lab_to_keep #EQ_trans_code 1329 %{(mk_env_item … hd_sig hd_lab t_hd_code)} %{fresh_tail} % 1330 [ whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta 1331 @eq_f cases hd_sig // ] >EQ_trans_code % [% [ % [ % [% // whd in ⊢ (??%?); >(\b (refl …)) %] % ] %  whd 1385 %{(mk_env_item … hd_sig hd_lab t_hd_code)} %{fresh_tail} % 1386 [ % 1387 [ @(fresh_keep_n_ok … fresh1) 1388 [ @(fresh_keep_n_ok … Hfresh1) 1389 @(fresh_for_subset … (labels_of_prog … prog)) 1390 cases daemon (*TODO*) 1391  cases daemon (*TODO*) 1392 ] 1393  whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta 1394 @eq_f cases hd_sig // ]] >EQ_trans_code % [% [ % [ % [% // whd in ⊢ (??%?); >(\b (refl …)) %] % ] %  whd 1332 1395 #x #Hx whd in ⊢ (??%?); >(? : (x == hd_lab) = false) 1333 1396 [2: inversion(x==hd_lab) // #EQx_hdlab cases Hhd_lab Hhd_lab #Hhd_lab cases Hhd_lab 1334 1397 >memb_append_l1 // <(\P EQx_hdlab) >Hx // ] 1335 normalize nodelta @get_element_append_l1 % #H1 1398 normalize nodelta >get_element_append_l1 1399 [2: cases daemon (*noduplicates*)] @get_element_append_l1 1400 % #H1 1336 1401 (* subproof with no nice statement *) 1337 1402 lapply H1 H1 lapply H H lapply Hhd_lab Hhd_lab lapply EQtail EQtail 1338 generalize in match (foldl ?????); lapply env_tail env_tail lapply fresh_tail1339 fresh_tail lapply m_tail m_tail lapply keep_tail keep_tail IHelim tail1403 generalize in match fresh1; lapply env_tail env_tail lapply fresh_tail 1404 fresh_tail lapply m_tail m_tail lapply keep_tail keep_tail elim tail 1340 1405 normalize nodelta 1341 1406 [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); … … 1363 1428 ] 1364 1429 ] 1365  whd #x #Hx >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … (a_return_post x) … H) 1430  whd #x #Hx >memb_append_l12 [2: cases daemon (*TODO*) ] 1431 >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … (a_return_post x) … H) 1366 1432 // @⊥ 1367 1433 (* subproof with no nice statement *) 1368 1434 lapply ABS ABS lapply H H lapply Hhd_lab Hhd_lab lapply EQtail EQtail 1369 generalize in match (foldl ?????); lapply env_tail env_tail lapply fresh_tail1370 fresh_tail lapply m_tail m_tail lapply keep_tail keep_tail IHelim tail1435 generalize in match fresh1; lapply env_tail env_tail lapply fresh_tail 1436 fresh_tail lapply m_tail m_tail lapply keep_tail keep_tail elim tail 1371 1437 normalize nodelta 1372 1438 [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); … … 1395 1461 ] 1396 1462  #Hf #Henv_it cases(IH … no_dup_tail … Henv_it) 1397 [5: >EQtail in ⊢ (??%?); % 1398 9: normalize nodelta % 1463 [9: >EQtail in ⊢ (??%?); % 1464 13: % 1465 6: assumption 1466 10: % 1399 1467 *: 1400 1468 ] 1401 #new_env_it * #new_fresh * #EQlook_new_env_it ***** #EQt_code #EQ_get_el1469 #new_env_it * #new_fresh ** #is_fresh_newfresh #EQlook_new_env_it ***** #EQt_code #EQ_get_el 1402 1470 #EQsign_env_it #EQ_f_lab #same_fresh_map #same_to_keep %{new_env_it} %{new_fresh} 1403 1471 % 1404 [ whd in ⊢ (??%?); @eq_function_name_elim [ #ABS >ABS in Hf; * #H @⊥ @H %] 1405 #_ normalize nodelta assumption ] 1406 % [2: #x #Hx <same_to_keep // @memb_append_l22 1472 [ % 1473 [ assumption 1474  whd in ⊢ (??%?); @eq_function_name_elim [ #ABS >ABS in Hf; * #H @⊥ @H %] 1475 #_ normalize nodelta assumption ]] 1476 % [2: #x #Hx <same_to_keep // >associative_append @memb_append_l22 1407 1477 inversion(memb ???) // #ABS lapply(lab_to_keep_in_domain … (eq_true_to_b … ABS)) 1408 1478 #ABS1 @(memb_no_duplicates_append … (a_return_post x) … H) // … … 1410 1480 >foldr_map_append >memb_append_l2 // >foldr_map_append >memb_append_l1 // 1411 1481 whd in match (foldr ?????); @orb_Prop_r >memb_append_l1 // >Hx % ] 1412 % [2: #x #Hx <same_fresh_map // >cons_append <associative_append @(get_element_append_r1) 1482 % [2: #x #Hx <same_fresh_map // >cons_append <associative_append 1483 <associative_append in ⊢ (??(???(??%?)?)?); >associative_append 1484 @(get_element_append_r1) 1413 1485 % >domain_of_associative_list_append #ABS cases(memb_append … ABS) 1414 1486 [ whd in match (memb ???); inversion(x==hd_lab) normalize nodelta … … 1429 1501 ] 1430 1502 ] 1431 % // % // % // <EQ_get_el >cons_append <associative_append 1503 % // % // % // <EQ_get_el >cons_append <associative_append <associative_append in ⊢ (??(???(??%?)?)?); 1504 >associative_append 1432 1505 @get_element_append_r1 % >domain_of_associative_list_append #ABS cases(memb_append … ABS) 1433 1506 [ whd in match (memb ???); inversion(a_call (f_lab … new_env_it)== a_call hd_lab) … … 1570 1643 #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ) 1571 1644 lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H 1572 cases(H … EQenv_it) H #env_it' * #fresh' * #EQenv_it' ***** #EQtrans 1645 cases(H … EQenv_it) H #env_it' * #fresh' ** #is_fresh_fresh' 1646 #EQenv_it' ***** #EQtrans 1573 1647 #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep 1574 1648 change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean; … … 1589 1663 whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta 1590 1664 % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans 1591 @(inverse_call_post_trans … fresh')1665 @(inverse_call_post_trans … is_fresh_fresh') 1592 1666 [2: % *: [2,3: /2 by / ] 1593 1667 cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
Note: See TracChangeset
for help on using the changeset viewer.