Changeset 3411
- Timestamp:
- Dec 23, 2013, 6:46:07 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Language.ma
r3410 r3411 265 265 266 266 267 definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2. True.267 definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.cont … s1 = cont … s2. 268 268 (* bisognerebbe confrontare la coda dell'istruzione corrente e la parte di stack fino alla prima label. 269 269 match (code … s1) with … … 1366 1366 ∀s1,s2,s1' : state p.∀abs_top,abs_tail. 1367 1367 ∀t : raw_trace (operational_semantics … p' prog) s1 s2. 1368 pre_measurable_trace … t → 1368 1369 state_rel … m keep abs_top abs_tail s1 s1' → 1369 1370 ∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'. … … 1373 1374 len … t = len … t'. 1374 1375 #p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans 1375 #s1 #s2 #s1' #abs_top #abs_tail #t lapply abs_top -abs_top lapply abs_tail1376 -abs_tail lapply s1' -s1' elim t1377 [ #st # s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)}1376 #s1 #s2 #s1' #abs_top #abs_tail #t #Hpre lapply abs_top -abs_top lapply abs_tail 1377 -abs_tail lapply s1' -s1' elim Hpre 1378 [ #st #_ #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)} 1378 1379 % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil 1379 1380 @is_permutation_eq 1380 ] 1381 #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12 1382 [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore 1383 #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #IH #s1' #abs_tail #abs_top 1384 whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?); 1385 whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????); 1386 inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1' 1387 normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????); 1388 inversion(check_continuations ?????) [ #_ *] ** #H1 #l2 #ll2 #EQHl2 1389 >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ ***** ] 1390 * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta 1391 cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta 1392 [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) ***** 1393 | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1; 1394 normalize * /2/ ] * 1395 [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ) 1396 #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1') 1397 [ 1398 | #x 1399 | #seq #lbl #i #_ 1400 | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ 1401 | #cond #ltrue #i1 #lfalse #i2 #_ #_ 1402 | #f #act_p #ret_post #i #_ 1403 | #l_in #io #l_out #i #_ 1381 | #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12 1382 [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore 1383 #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #_ * #opt_l #EQ destruct(EQ) 1384 #pre_tl #IH #s1' #abs_tail #abs_top whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?); 1385 whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????); 1386 inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1' 1387 normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????); 1388 inversion(check_continuations ?????) [ #_ *] ** #H1 #l2 #ll2 #EQHl2 1389 >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ ***** ] 1390 * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta 1391 cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta 1392 [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) ***** 1393 | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1; 1394 normalize * /2/ ] * 1395 [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ) 1396 #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1') 1397 [ 1398 | #x 1399 | #seq #lbl #i #_ 1400 | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ 1401 | #cond #ltrue #i1 #lfalse #i2 #_ #_ 1402 | #f #act_p #ret_post #i #_ 1403 | #l_in #io #l_out #i #_ 1404 ] 1405 [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)] 1406 cases(call_post_clean ?????) normalize nodelta 1407 [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ] 1408 #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ) 1409 cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …) 1410 [2: whd whd in match check_continuations; normalize nodelta 1411 change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2 1412 normalize nodelta % // % // % // % // @EQcode_c_st12 ] 1413 #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen 1414 %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) … t')} 1415 [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉) 1416 [3: assumption |4: assumption |*:] /3 by nmk/ ] 1417 % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts 1418 | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ) 1419 #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?); 1420 inversion(code … s1') 1421 [ 1422 | #x 1423 | #seq #lbl #i #_ 1424 | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ 1425 | #cond #ltrue #i1 #lfalse #i2 #_ #_ 1426 | #f #act_p #ret_post #i #_ 1427 | #l_in #io #l_out #i #_ 1428 ] 1429 [|*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ] 1430 #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ) 1431 cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …) 1432 [2: whd whd in match check_continuations; normalize nodelta 1433 change with (check_continuations ?????) in match (foldr2 ???????); 1434 >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]); 1435 normalize nodelta % // % // % // % // @EQcode_c_st12 ] 1436 #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen 1437 %{abs_top'} %{abs_tail'} %{st3'} 1438 %{(t_ind … (cost_act (Some ? lbl)) … t')} 1439 [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉) 1440 [3: assumption |4: assumption |*:] /3 by nmk/ ] 1441 % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append 1442 whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el 1443 @is_permutation_cons assumption 1404 1444 ] 1405 [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)] 1406 cases(call_post_clean ?????) normalize nodelta 1407 [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ] 1408 #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ) 1409 cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …) 1410 [2: whd whd in match check_continuations; normalize nodelta 1411 change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2 1412 normalize nodelta % // % // % // % // @EQcode_c_st12 ] 1413 #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen 1414 %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) … t')} 1415 [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉) 1416 [3: assumption |4: assumption |*:] /3 by nmk/ ] 1417 % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts 1418 | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ) 1419 #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?); 1420 inversion(code … s1') 1421 [ 1422 | #x 1423 | #seq #lbl #i #_ 1424 | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ 1425 | #cond #ltrue #i1 #lfalse #i2 #_ #_ 1426 | #f #act_p #ret_post #i #_ 1427 | #l_in #io #l_out #i #_ 1428 ] 1429 [|*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ] 1430 #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ) 1431 cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …) 1432 [2: whd whd in match check_continuations; normalize nodelta 1433 change with (check_continuations ?????) in match (foldr2 ???????); 1434 >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]); 1435 normalize nodelta % // % // % // % // @EQcode_c_st12 ] 1436 #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen 1437 %{abs_top'} %{abs_tail'} %{st3'} 1438 %{(t_ind … (cost_act (Some ? lbl)) … t')} 1439 [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉) 1440 [3: assumption |4: assumption |*:] /3 by nmk/ ] 1441 % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append 1442 whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el 1443 @is_permutation_cons assumption 1444 ] 1445 | cases daemon (*TODO*) 1445 1446 (* 1446 | #seq #i #store * [| #lbl] #EQcode11 #EQstore #EQ destruct(EQ) #EQcont 1447 | 1448 #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12 1449 #seq #i #store * [| #lbl] #EQcode11 #EQstore #EQ destruct(EQ) #EQcont 1447 1450 #EQ destruct(EQ) #Hio_st11 #Hio_st12 #EQ destruct(EQ) #EQ1 #EQ2 destruct(EQ1 EQ2) 1448 1451 #EQ destruct(EQ) #tl #IH #st3 #l1 whd in ⊢ (% → ?); … … 1454 1457 #seq1 #opt_l #i1 #_ #EQcode_st3 change with (m_bind ?????) in ⊢ (??%? → ?); 1455 1458 cases daemon *) 1456 |8: #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem 1459 | cases daemon (*TODO*) 1460 | cases daemon (*TODO*) 1461 | cases daemon (*TODO*) 1462 | cases daemon (*TODO*) 1463 | cases daemon (*TODO*) 1464 | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 1465 #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ) 1466 | cases daemon (*TODO absurd as above*) 1467 ] 1468 | cases daemon (*TODO*) 1469 | #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12 1470 [1,2,3,4,5,6,7,9: cases daemon (*absurd!*) 1471 | #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem 1472 #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 1473 destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #_ #_ whd in ⊢ (?% → ?); >EQcode11 in ⊢ (% → ?); 1474 normalize nodelta cases opt_l in EQcode11 EQcont12; normalize nodelta [ #x #y *] 1475 #lbl #EQcode11 #EQcont12 * #pre_tl #IH #st1' #abs_top #abs_tail 1476 whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1 1477 #abs_top_cont #abs_tail_cont #EQcheck 1478 normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1') 1479 [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_ 1480 #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ) 1481 lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H 1482 cases(H … EQenv_it) -H #env_it' * #fresh' * #EQenv_it' ***** #EQtrans 1483 #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep 1484 change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean; 1485 [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind 1486 inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta 1487 [2: inversion(memb ???) normalize nodelta #Hlbl_keep 1488 [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] 1489 #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta 1490 [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_ 1491 lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta 1492 [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'') 1493 #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ 1494 #EQ destruct(EQ) 1495 cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_tail_cont) (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?)))) 1496 [2: whd >EQcont12 1497 change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????); 1498 >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l' 1499 whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta 1500 % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans 1501 @(inverse_call_post_trans … fresh') 1502 [2: % |*: [2,3: /2 by / ] 1503 cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2 1504 whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append 1505 #no_dup lapply(no_duplicates_append_r … no_dup) #H1 1506 lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1 1507 change with ([?]@?) in match (?::?); #H1 1508 lapply(no_duplicates_append_r … H1) >append_nil // 1509 ] 1510 ] 1511 #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{abs_top'''} 1512 %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) … t')} 1513 [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %] 1514 %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%); 1515 >EQlab_env_it >associative_append whd in match (append ???); >associative_append 1516 >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%); 1517 whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons 1518 >append_nil whd in match (append ???) in ⊢ (???%); // 1519 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 1520 ] 1521 | whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1522 ] 1523 ] 1524 | 1525 1526 8: 1527 #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12 1528 #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem 1457 1529 #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 1458 1530 destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #abs_top #abs_tail … … 1518 1590 ] 1519 1591 #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen 1520 %{ ([a_return_post lbl'] @ abs_top''')}1592 %{abs_top'''} 1521 1593 %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) … t')} 1522 1594 [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %] … … 1524 1596 >EQlab_env_it >associative_append >associative_append 1525 1597 >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%); 1598 >EQopt_l' in t'; #t' 1526 1599 whd in match (map_labels_on_trace ??); >EQgen_labels 1527 1600 whd in match (foldr ?????); >append_nil 1601 whd in match (get_costlabels_of_trace ????); 1528 1602 @is_permutation_cons 1529 1603 >append_nil whd in match (append ???) in ⊢ (???%); //
Note: See TracChangeset
for help on using the changeset viewer.