Changeset 3411 for LTS/Language.ma


Ignore:
Timestamp:
Dec 23, 2013, 6:46:07 PM (6 years ago)
Author:
piccolo
Message:

new statement of correctness theorem in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3410 r3411  
    265265
    266266
    267 definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.True.
     267definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.cont … s1 = cont … s2.
    268268(* bisognerebbe confrontare la coda dell'istruzione corrente e la parte di stack fino alla prima label.
    269269 match (code … s1) with
     
    13661366∀s1,s2,s1' : state p.∀abs_top,abs_tail.
    13671367∀t : raw_trace (operational_semantics … p' prog) s1 s2.
     1368pre_measurable_trace … t →
    13681369state_rel … m keep abs_top abs_tail s1 s1' →
    13691370∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
     
    13731374 len … t = len … t'.
    13741375#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_tail
    1376 -abs_tail lapply s1' -s1' elim t
    1377 [ #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 …)}
    13781379  % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
    13791380  @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
    14041444    ]
    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*)
    14451446(*     
    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
    14471450  #EQ destruct(EQ) #Hio_st11 #Hio_st12 #EQ destruct(EQ) #EQ1 #EQ2 destruct(EQ1 EQ2)
    14481451  #EQ destruct(EQ) #tl #IH #st3 #l1 whd in ⊢ (% → ?);
     
    14541457  #seq1 #opt_l #i1 #_ #EQcode_st3 change with (m_bind ?????) in ⊢ (??%? → ?);
    14551458  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
     15268:
     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
    14571529    #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
    14581530    destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #abs_top #abs_tail
     
    15181590          ]
    15191591          #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen
    1520           %{([a_return_post lbl'] @ abs_top''')}
     1592          %{abs_top'''}
    15211593          %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
    15221594          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %]
     
    15241596          >EQlab_env_it >associative_append >associative_append
    15251597          >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
     1598          >EQopt_l' in t'; #t'
    15261599          whd in match (map_labels_on_trace ??); >EQgen_labels
    15271600          whd in match (foldr ?????); >append_nil
     1601          whd in match (get_costlabels_of_trace ????);
    15281602           @is_permutation_cons
    15291603          >append_nil whd in match (append ???) in ⊢ (???%); //
Note: See TracChangeset for help on using the changeset viewer.