Changeset 3416


Ignore:
Timestamp:
Jan 24, 2014, 5:38:33 PM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3414 r3416  
    462462
    463463definition fresh_rc_label : ℕ → ReturnPostCostLabel × ℕ ≝
    464 λx.〈a_return_cost_label x,S x〉.
     464λx.〈a_return_cost_label (S x),S x〉.
    465465
    466466record call_post_info (p : instr_params) : Type[0] ≝
     
    898898qed.
    899899
    900 let rec is_fresh_keep (keep : list ReturnPostCostLabel) (n : ℕ) on keep : Prop ≝
     900let rec is_fresh_for_return (keep : list CostLabel) (n : ℕ) on keep : Prop ≝
    901901match keep with
    902902[ nil ⇒ True
    903 | cons x xs ⇒ let ih ≝ is_fresh_keep xs n in
     903| cons x xs ⇒ let ih ≝ is_fresh_for_return xs n in
    904904              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              ]
    906908].
    907909
     
    917919
    918920lemma 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
     921is_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
     923normalize [2: * #H1] #H2 #H3 [ %] /2 by transitive_le/
     924qed.
     925
     926definition cast_return_to_cost_labels ≝ map … (a_return_post …).
     927coercion cast_return_to_cost_labels.
     928
     929lemma fresh_false : ∀n.∀l: list ReturnPostCostLabel.is_fresh_for_return l n →
     930a_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
    927933[ #EQ destruct @⊥ /2 by absurd/
    928934| #_ >IH //
    929935]
    930936qed.
    931 
    932937
    933938lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
     
    938943same_fresh_map_on dom (lab_map … info) m →
    939944same_to_keep_on dom (lab_to_keep … info) keep →
    940 is_fresh_keep keep n →
     945is_fresh_for_return keep n →
    941946call_post_clean ? (t_code ? info) m keep l
    942947 = return 〈gen_labels … info,i1〉.
     
    11081113  >(IH … (refl …))
    11091114  [1,6: normalize nodelta
    1110      [ >fresh_false [2: /2 by fresh_keep_n_ok/ ] %
     1115     [ >fresh_false [2: /2 by fresh_keep_n_ok/] %
    11111116     | <same_keep
    11121117       [ whd in match (memb ???); >(\b (refl …)) normalize nodelta
     
    11551160  ]
    11561161]
    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 ??
     1162qed.
     1163
     1164definition 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
     1168definition translate_env ≝
     1169λp,p'.λenv : list (env_item p p').λmax_all.(foldr ??
    11661170           (λi,x.let 〈t_env,n,m,keep〉 ≝ x in
    11671171           let info ≝ call_post_trans … (f_body … i) n (nil ?) in
     
    11711175                     fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 ::
    11721176                                     ((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
     1179definition trans_prog : ∀p,p'.Program p p' →
     1180((Program p p') × (associative_list DEQCostLabel CostLabel)) × ((list ReturnPostCostLabel))≝
     1181λp,p',prog.
     1182let max_all ≝ fresh_for_prog … prog in
     1183let info_main ≝ (call_post_trans … (main … prog) max_all (nil ?)) in
     1184let 〈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)〉.
    11751186
    11761187definition map_labels_on_trace :
     
    12981309(* aggiungere fresh_to_keep al lemma seguente??*)
    12991310
    1300 xxxxxxx
    1301 
     1311let rec subset (A : Type[0]) (l1,l2 : list A) on l1 : Prop ≝
     1312match l1 with
     1313[ nil ⇒ True
     1314| cons x xs ⇒ mem … x l2 ∧ subset … xs l2
     1315].
     1316
     1317interpretation "subset" 'subseteq a b = (subset ? a b).
     1318
     1319lemma 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/
     1321qed.
     1322
     1323lemma refl_subset : ∀A.reflexive … (subset A).
     1324#A #l1 elim l1 // #x #xs #IH normalize % /2/
     1325qed.
     1326
     1327lemma fresh_for_subset : ∀l1,l2,n.l1 ⊆ l2 → is_fresh_for_return … l2 n →
     1328is_fresh_for_return … l1 n.
     1329#l1 elim l1 // ** #x #xs #IH #l2 #n * #H1 #H2 #H3 whd
     1330try(@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 //
     1337qed.
     1338
     1339lemma fresh_append : ∀n,l1,l2.is_fresh_for_return l1 n → is_fresh_for_return l2 n →
     1340is_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 //
     1343qed.
     1344
     1345definition 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
     1348lemma 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.
    13021351
    13031352lemma trans_env_ok : ∀p : state_params.∀ prog.
     
    13051354let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
    13061355∀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' ∧
     1356let 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' ∧
    13091358let info ≝ call_post_trans … (f_body … env_it) n (nil ?) in
    13101359t_code … info = f_body … env_it' ∧
     
    13121361f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it' ∧
    13131362same_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
     1364lapply EQt_prog normalize nodelta
     1365generalize in match keep0 in ⊢ (% → ? → ? → ? → ? → ??(λ_.??(λ_.?%?)));
     1366#keep1 #EQkeep1 inversion prog in EQt_prog; #env #main #EQprog
     1367whd in match trans_prog; normalize nodelta
     1368@pair_elim
     1369cut(fresh_for_prog ?? prog ≤ fresh_for_prog ?? (mk_Program … env main)) [ >EQprog //]
     1370generalize in match (fresh_for_prog ???) in ⊢ (??% → %);
     1371lapply t_prog0 lapply m0 lapply keep0
     1372elim 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'
    13181375normalize 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)
    13211377whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H)
    13221378change with (no_duplicates_labels p p (mk_Program p p tail main)) in match
     
    13271383  inversion (call_post_trans … hd_code fresh_tail [])
    13281384  #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
    13321395    #x #Hx whd in ⊢ (??%?); >(? : (x == hd_lab) = false)
    13331396    [2: inversion(x==hd_lab) // #EQx_hdlab cases Hhd_lab -Hhd_lab #Hhd_lab cases Hhd_lab
    13341397        >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 
    13361401    (* subproof with no nice statement *)
    13371402    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_tail
    1339     -fresh_tail lapply m_tail -m_tail lapply keep_tail -keep_tail -IH elim tail
     1403    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
    13401405    normalize nodelta
    13411406    [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?);
     
    13631428    ]
    13641429    ]
    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)
    13661432    // @⊥
    13671433    (* subproof with no nice statement *)
    13681434    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_tail
    1370     -fresh_tail lapply m_tail -m_tail lapply keep_tail -keep_tail -IH elim tail
     1435    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
    13711437    normalize nodelta
    13721438    [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?);
     
    13951461  ]
    13961462| #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: %
    13991467  |*:
    14001468  ]
    1401   #new_env_it * #new_fresh * #EQlook_new_env_it ***** #EQt_code #EQ_get_el
     1469  #new_env_it * #new_fresh ** #is_fresh_newfresh #EQlook_new_env_it ***** #EQt_code #EQ_get_el
    14021470  #EQsign_env_it #EQ_f_lab #same_fresh_map #same_to_keep %{new_env_it} %{new_fresh}
    14031471  %
    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
    14071477        inversion(memb ???) // #ABS lapply(lab_to_keep_in_domain … (eq_true_to_b … ABS))
    14081478        #ABS1 @(memb_no_duplicates_append … (a_return_post x) … H) //
     
    14101480        >foldr_map_append >memb_append_l2 // >foldr_map_append >memb_append_l1 //
    14111481        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)
    14131485         % >domain_of_associative_list_append #ABS cases(memb_append … ABS)
    14141486         [ whd in match (memb ???); inversion(x==hd_lab) normalize nodelta
     
    14291501         ]
    14301502     ] 
    1431    % // % // % // <EQ_get_el >cons_append <associative_append
     1503   % // % // % // <EQ_get_el >cons_append <associative_append  <associative_append in ⊢ (??(???(??%?)?)?);
     1504   >associative_append
    14321505   @get_element_append_r1 % >domain_of_associative_list_append #ABS cases(memb_append … ABS)
    14331506         [ whd in match (memb ???); inversion(a_call (f_lab … new_env_it)== a_call hd_lab)
     
    15701643    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
    15711644    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
    15731647    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
    15741648    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
     
    15891663            whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
    15901664            % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans
    1591             @(inverse_call_post_trans … fresh')
     1665            @(inverse_call_post_trans … is_fresh_fresh')
    15921666            [2: % |*: [2,3: /2 by / ]
    15931667                cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
Note: See TracChangeset for help on using the changeset viewer.