 Timestamp:
 Dec 27, 2013, 9:09:10 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3411 r3414 469 469 ; fresh : ℕ 470 470 ; lab_map : associative_list DEQCostLabel CostLabel 471 ; lab_to_keep : list CostLabel471 ; lab_to_keep : list ReturnPostCostLabel 472 472 }. 473 473 … … 515 515 mk_call_post_info ? (nil ?) (CALL ? f act_p (Some ? lbl) (t_code … ih)) (fresh … ih) 516 516 (〈a_return_post lbl,(a_return_post lbl :: (gen_labels … ih))〉 :: (lab_map … ih)) 517 ( a_return_postlbl :: lab_to_keep … ih)517 (lbl :: lab_to_keep … ih) 518 518 ] 519 519  IO lin io lout i1 ⇒ … … 526 526 527 527 let rec call_post_clean (p : instr_params) (i : Instructions p) on i : 528 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →528 associative_list DEQCostLabel CostLabel → list ReturnPostCostLabel → list CostLabel → 529 529 option ((list CostLabel) × (Instructions p)) ≝ 530 530 λm,keep,abs. … … 559 559 match r_lb with 560 560 [ None ⇒ None ? 561  Some lbl ⇒ if ( (a_return_post lbl ∈ keep))561  Some lbl ⇒ if (lbl ∈ keep) 562 562 then if ((get_element … m lbl) == lbl :: l1) 563 563 then return 〈nil ?,CALL … f act_p (Some ? lbl) instr1〉 … … 605 605 ]. 606 606 607 definition ret_costed_abs : list CostLabel → option ReturnPostCostLabel → option CostLabel ≝607 definition ret_costed_abs : list ReturnPostCostLabel → option ReturnPostCostLabel → option CostLabel ≝ 608 608 λkeep,x. 609 609 match x with 610 [ Some lbl ⇒ if (a_return_post lbl)∈ keep then return (a_return_post lbl)610 [ Some lbl ⇒ if lbl ∈ keep then return (a_return_post lbl) 611 611 else None ? 612 612  None ⇒ None ? … … 617 617 ∀l1,l2 : list (ActionLabel × (Instructions p)). 618 618 associative_list DEQCostLabel CostLabel → 619 list CostLabel → option (Prop × (list CostLabel) × (list CostLabel)) ≝619 list ReturnPostCostLabel → option (Prop × (list CostLabel) × (list CostLabel)) ≝ 620 620 λp,cont1,cont2,m,keep. 621 621 foldr2 ??? 〈True,nil ?,nil ?〉 cont1 cont2 … … 676 676 677 677 definition state_rel : ∀p. 678 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →(list CostLabel) →678 associative_list DEQCostLabel CostLabel → list ReturnPostCostLabel → list CostLabel →(list CostLabel) → 679 679 relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2. 680 680 match check_continuations ? (cont ? st1) (cont … st2) m keep with … … 757 757 λdom,m1,m2.∀x.bool_to_Prop (x ∈ dom) → get_element … m1 x = get_element … m2 x. 758 758 759 definition same_to_keep_on : list CostLabel → relation (list CostLabel) ≝760 λdom,keep1,keep2.∀x. bool_to_Prop ( x ∈ dom) → (x ∈ keep1) = (x ∈ keep2).759 definition same_to_keep_on : list CostLabel → relation (list ReturnPostCostLabel) ≝ 760 λdom,keep1,keep2.∀x. bool_to_Prop (a_return_post x ∈ dom) → (x ∈ keep1) = (x ∈ keep2). 761 761 762 762 lemma memb_not_append : ∀D : DeqSet.∀l1,l2 : list D.∀x : D. … … 779 779 780 780 781 lemma same_to_keep_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l. 782 no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → x ∈ dom1) → 783 (∀x.x ∈ l3 → x ∈ dom3) → 781 lemma same_to_keep_on_append : ∀dom1,dom2,dom3 : list CostLabel. 782 ∀l1,l2,l3,l : list ReturnPostCostLabel. 783 no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → a_return_post x ∈ dom1) → 784 (∀x.x ∈ l3 → a_return_post x ∈ dom3) → 784 785 same_to_keep_on (dom1@dom2@dom3) (l1@l2@l3) l → 785 786 same_to_keep_on dom2 l2 l. … … 792 793  @sym_eq @memb_not_append [2: @memb_not_append //] 793 794 [ <associative_append in no_dup; #no_dup ] 794 lapply(memb_no_duplicates_append … x… no_dup) #H795 lapply(memb_no_duplicates_append … (a_return_post x) … no_dup) #H 795 796 inversion(memb ???) // #H1 cases H 796 797 [1,4: [>memb_append_l2  >memb_append_l1] // >Hx // … … 819 820 lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p. 820 821 ∀x,n,l. 821 x ∈ lab_to_keep … (call_post_trans … i n l) → x ∈ get_labels_of_code … i.822 x ∈ lab_to_keep … (call_post_trans … i n l) → a_return_post x ∈ get_labels_of_code … i. 822 823 #p #i elim i // 823 824 [ #seq #opt_l #instr #IH #x #n #l whd in match (call_post_trans ????); … … 896 897 #EQ destruct >(\b (refl …)) @I 897 898 qed. 898 899 900 let rec is_fresh_keep (keep : list ReturnPostCostLabel) (n : ℕ) on keep : Prop ≝ 901 match keep with 902 [ nil ⇒ True 903  cons x xs ⇒ let ih ≝ is_fresh_keep xs n in 904 match x with 905 [ a_return_cost_label m ⇒ m < n ∧ ih ] 906 ]. 907 908 lemma fresh_ok_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.∀l. 909 n ≤ fresh … (call_post_trans p i1 n l). 910 #p #i1 elim i1 normalize /2 by transitive_le, le_n/ 911 [ #seq * [#lbl] #i2 #IH #n #l normalize /2 by / 912  #cond #ltrue #i_true #lfalse #i_false #i2 #IH1 #IH2 #IH3 #n #l 913 @(transitive_le … (IH3 …)) [2: @(transitive_le … (IH2 …)) [2: @(transitive_le … (IH1 …)) ]] // 914  #f #act_p * [#lbl] normalize #i2 #IH /2 by le_S/ 915 ] 916 qed. 917 918 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 927 [ #EQ destruct @⊥ /2 by absurd/ 928  #_ >IH // 929 ] 930 qed. 931 932 899 933 lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ. 900 934 let dom ≝ get_labels_of_code … i1 in … … 904 938 same_fresh_map_on dom (lab_map … info) m → 905 939 same_to_keep_on dom (lab_to_keep … info) keep → 906 call_post_clean … (t_code … info) m keep l 940 is_fresh_keep keep n → 941 call_post_clean ? (t_code ? info) m keep l 907 942 = return 〈gen_labels … info,i1〉. 908 943 #p #i1 elim i1 … … 912 947 #EQ destruct(EQ) // 913 948  #seq * [#lbl] #instr #IH #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep 914 #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%%); normalize nodelta949 #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%%); normalize nodelta 915 950 >IH // 916 951 [1,4: whd whd in H2; #x #Hx @H2 whd in match (get_labels_of_code ??); // 917 @orb_Prop_r //918 952 2,5: whd whd in H1; #x #Hx [ @H1 // ] cases no_dup #H3 #_ <H1 919 953 [2: whd in match (get_labels_of_code ??); @orb_Prop_r // ] … … 929 963  #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #n normalize nodelta 930 964 #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); 931 #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%?); >IH3 //965 #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%?); >IH3 // 932 966 [2: whd in match (get_labels_of_code ??) in H2; 933 967 change with ([?;?]@?) in match (?::?) in H2; … … 964 998 4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) ] 965 999 ] 966 normalize nodelta >IH2 // 967 [2: whd in match (get_labels_of_code ??) in H2; 1000 normalize nodelta >IH2 1001 [5: % 1002 2: /2 by fresh_keep_n_ok/ 1003 3: whd in match (get_labels_of_code ??) in H2; 968 1004 change with ([?;?]@?) in match (?::?) in H2; 969 1005 <associative_append in H2; #H2 970 1006 @(same_to_keep_on_append … H2) // #x #Hx [ @orb_Prop_r @orb_Prop_r ] 971 1007 @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) 972  3: whd in match (get_labels_of_code ??) in H1;1008 4: whd in match (get_labels_of_code ??) in H1; 973 1009 change with ([?;?]@?) in match (?::?) in H1; 974 1010 change with ([?;?]@?) in match (?::?::?) in H1 : (??%?); … … 982 1018 @(lab_map_in_domain … (eq_true_to_b … H1)) 983 1019 ] 984 4: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l 1020 6: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l 1021 *: 985 1022 ] 986 >m_return_bind >IH1 // 987 [2: whd in match (get_labels_of_code ??) in H2; 1023 >m_return_bind >IH1 1024 [5: % 1025 2: /3 by fresh_keep_n_ok/ 1026 3: whd in match (get_labels_of_code ??) in H2; 988 1027 change with ([?;?]@?) in match (?::?) in H2; 989 1028 change with ([ ] @ ?) in match (lab_to_keep ??) in H2; 990 1029 >associative_append in H2 : (??%?); #H2 991 @(same_to_keep_on_append … H2) // [ #x *]#x #Hx cases(memb_append … Hx)1030 @(same_to_keep_on_append … H2) // #x #Hx cases(memb_append … Hx) 992 1031 Hx #Hx [ >memb_append_l1  >memb_append_l2] // 993 1032 @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) 994  3: whd in match (get_labels_of_code ??) in H1;1033 4: whd in match (get_labels_of_code ??) in H1; 995 1034 change with ([?;?]@?) in match (?::?) in H1; 996 1035 change with ([?;?]@?) in match (?::?::?) in H1 : (??%?); … … 998 1037 #Hx cases(memb_append … Hx) Hx #Hx [ >memb_append_l1  >memb_append_l2 ] 999 1038 // @(lab_map_in_domain … (eq_true_to_b … Hx)) 1000 4: cases no_dup #_ * #_ @no_duplicates_append_l 1039 6: cases no_dup #_ * #_ @no_duplicates_append_l 1040 *: 1001 1041 ] 1002 1042 >m_return_bind normalize nodelta whd in H1; <H1 … … 1010 1050 >(\b (refl ? (a_non_functional_label ltrue))) % ] #_ 1011 1051 whd in match (get_element ????); >(\b (refl …)) normalize nodelta 1012 >(\b (refl …)) % 1052 >(\b (refl …)) % 1013 1053  #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?); 1014 #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on 1015 whd in ⊢ (??%?); > IH21016 [ normalize nodelta > IH11054 #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on #f_k 1055 whd in ⊢ (??%?); >(IH2 … (refl …)) 1056 [ normalize nodelta >(IH1 … (refl …)) 1017 1057 [ >m_return_bind <fresh_map [2: @orb_Prop_l >(\b (refl …)) % ] 1018 1058 whd in match (get_element ????); … … 1026 1066 whd in match (get_element ????); >(\b (refl …)) normalize nodelta 1027 1067 >(\b (refl …)) % 1068  /2 by fresh_keep_n_ok/ 1028 1069  change with ([?;?]@?@?) in keep_on : (?%??); change with ((nil ?) @ ? @ ?) in keep_on : (??%?); 1029 @(same_to_keep_on_append … keep_on) // [ #x *  #x /2 by lab_to_keep_in_domain/ ]1070 @(same_to_keep_on_append … keep_on) // #x /2 by lab_to_keep_in_domain/ 1030 1071  change with ([?;?]@?@?) in fresh_map : (?%%?); @(same_fresh_map_on_append … fresh_map) 1031 1072 /2 by lab_map_in_domain/ #x whd in match (memb ???); inversion(x==lfalse) #Hlfalse … … 1035 1076 @orb_Prop_l >Hltrue % 1036 1077 ] 1037  %1038 1078  cases no_dup #_ * #_ /2/ 1039 1040 1079 ] 1080  // 1041 1081  change with ([?;?]@?@?) in keep_on : (?%??); <associative_append in keep_on; 1042 1082 <(append_nil … (?@?)) <(append_nil … (?@?)) in ⊢ (??%? → ?); … … 1062 1102 ] 1063 1103 ] 1064  %1065 1104  cases no_dup #_ * #_ /2 by no_duplicates_append_r/ 1066 1067 1105 ] 1068 1106  #f #act_p * [#r_lb] #i #IH #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?); 1069 #EQ destruct(EQ) cases daemon 1070 *: cases daemon (*TODO*) 1107 #EQ destruct(EQ) #fresh_map #same_keep #f_k whd in ⊢ (??%?); 1108 >(IH … (refl …)) 1109 [1,6: normalize nodelta 1110 [ >fresh_false [2: /2 by fresh_keep_n_ok/ ] % 1111  <same_keep 1112 [ whd in match (memb ???); >(\b (refl …)) normalize nodelta 1113 <fresh_map 1114 [ whd in match (get_element ????); >(\b (refl …)) normalize nodelta 1115 >(\b (refl …)) % 1116  whd in match (memb ???); >(\b (refl …)) % 1117 ] 1118  whd in match (memb ???); >(\b (refl …)) % 1119 ] 1120 ] 1121 2,7: // 1122 3,8: whd in match (get_labels_of_code ??) in same_keep; // #x #Hx <same_keep 1123 [2: >memb_cons // >Hx // ] cases no_dup * #ABS #_ whd in ⊢ (???%); 1124 inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) >Hx // 1125 4,9: whd in match (get_labels_of_code ??) in fresh_map; // #x #Hx <fresh_map 1126 [2: >memb_cons // >Hx //] cases no_dup * #ABS #_ whd in ⊢ (???%); 1127 inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) // 1128 5,10: [ @no_dup  cases no_dup // ] 1129 ] 1130  #lin #io #lout #i #IH #n whd in match (get_labels_of_code ??); #no_dup 1131 #m #keep #info #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #fresh_map #same_keep 1132 #f_k whd in ⊢ (??%?); >(IH … (refl …)) 1133 [ normalize nodelta <fresh_map [2: >memb_cons // >memb_hd // ] 1134 whd in match (get_element ????); >(\b (refl …)) normalize nodelta 1135 >(\b (refl …)) <fresh_map [2: >memb_hd //] whd in match (get_element ????); 1136 inversion(lin==lout) 1137 [ #ABS @⊥ cases no_dup * #ABS1 #_ @ABS1 whd in match (memb ???); >(\P ABS) 1138 >(\b (refl …)) // 1139  #H inversion (a_non_functional_label lin== ? lout) 1140 [ #ABS lapply(\P ABS) #EQ destruct >(\b (refl …)) in H; #EQ destruct 1141  #_ normalize nodelta whd in match (get_element ????); >(\b (refl …)) 1142 normalize nodelta >(\b (refl …)) % 1143 ] 1144 ] 1145  // 1146  #x #Hx >same_keep [2: >memb_cons // >memb_cons // >Hx % ] % 1147  #x #Hx <fresh_map [2: >memb_cons // >memb_cons // >Hx %] 1148 cases no_dup * #ABS1 ** #ABS2 #_ whd in ⊢ (???%); inversion(x == lout) 1149 normalize nodelta 1150 [2: #_ whd in ⊢ (???%); inversion(x==lin) normalize nodelta // 1151 #H @⊥ @ABS1 >memb_cons // <(\P H) >Hx // 1152  #H @⊥ @ABS2 <(\P H) >Hx // 1153 ] 1154  cases no_dup #_ * #_ // 1155 ] 1071 1156 ] 1072 qed. 1157 qed. 1158 1073 1159 1074 1160 1075 1161 definition trans_prog : ∀p,p'.Program p p' → 1076 (Program p p') × (associative_list DEQCostLabel CostLabel) × (list CostLabel)≝1162 (Program p p') × (associative_list DEQCostLabel CostLabel) × (list ReturnPostCostLabel)≝ 1077 1163 λp,p',prog. 1078 1164 let max_all ≝ foldl … (λn,i.max n (compute_max_n … (f_body … i))) O (env … prog) in … … 1209 1295 ] 1210 1296 qed. 1297 1298 (* aggiungere fresh_to_keep al lemma seguente??*) 1299 1300 xxxxxxx 1211 1301 1212 1302 … … 1273 1363 ] 1274 1364 ] 1275  whd #x #Hx >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … x… H)1365  whd #x #Hx >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … (a_return_post x) … H) 1276 1366 // @⊥ 1277 1367 (* subproof with no nice statement *) … … 1289 1379 #H1 #H2 #H3 cases(memb_append … H3) H3 1290 1380 [ #H3 change with ([?]@?) in match (?::?) in H2; 1291 lapply(no_duplicates_append_commute … H2) H2 * #_ #H4 @(memb_no_duplicates_append … x… H4)1381 lapply(no_duplicates_append_commute … H2) H2 * #_ #H4 @(memb_no_duplicates_append … (a_return_post x) … H4) 1292 1382 [ whd in match (append ???); >memb_append_l1 // >(lab_to_keep_in_domain … (eq_true_to_b … H3)) % 1293 1383  // … … 1316 1406 % [2: #x #Hx <same_to_keep // @memb_append_l22 1317 1407 inversion(memb ???) // #ABS lapply(lab_to_keep_in_domain … (eq_true_to_b … ABS)) 1318 #ABS1 @(memb_no_duplicates_append … x… H) //1408 #ABS1 @(memb_no_duplicates_append … (a_return_post x) … H) // 1319 1409 cases(lookup_ok_append … Henv_it) #l1 * #l2 * #EQ1 #EQ2 destruct(EQ1 EQ2) 1320 1410 >foldr_map_append >memb_append_l2 // >foldr_map_append >memb_append_l1 // … … 1522 1612 ] 1523 1613 ] 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 1529 #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 1530 destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #abs_top #abs_tail 1614  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?; 1615 [1,2,3,4,5,6,7,9: cases daemon (*assurdi*) ] 1616 #st11 #st12 #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem 1617 #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 1618 destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #t1 #t2 #H inversion H in ⊢ ?; 1619 [1,2,3,4,5,6,7,8: cases daemon (*assurdi*) ] 1620 #st41 #st42 #r_t #mem1 #new_cont #opt_l1 #cd #EQcode41 #EQcont41 #EQ destruct(EQ) 1621 #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #_ #_ 1622 #_ whd in ⊢ (?(?%) → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta 1623 inversion(opt_l) in ⊢(% → ?); normalize nodelta [2: #lbl #_ * ] #EQopt_l * 1624 #Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); #EQcont11_42 whd in ⊢ (% → ?); #EQ destruct 1625 #IH1 #IH2 #st1' #abs_top #abs_tail 1531 1626 whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1 1532 1627 #abs_top_cont #abs_tail_cont #EQcheck … … 1540 1635 [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind 1541 1636 inversion opt_l' in EQcode_st1'; [ #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta 1542 [2: inversion(memb ???) normalize nodelta #Hlbl_keep 1543 [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] 1544 #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta 1545 [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_ 1546 lapply(H1 H) H H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta 1547 [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'') 1548 #H1 #_ lapply(H1 H) H H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ 1549 #EQ destruct(EQ) 1550 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 ?)))) 1551 [2: whd >EQcont12 1552 change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????); 1553 >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l' 1554 whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta 1555 % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans 1556 @(inverse_call_post_trans … fresh') 1557 [2: % *: [2,3: /2 by / ] 1558 cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2 1559 whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append 1560 #no_dup lapply(no_duplicates_append_r … no_dup) #H1 1561 lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); H1 1562 change with ([?]@?) in match (?::?); #H1 1563 lapply(no_duplicates_append_r … H1) >append_nil // 1564 ] 1565 ] 1566 #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{abs_top'''} 1567 %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) … t')} 1568 [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %] 1569 %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%); 1570 >EQlab_env_it >associative_append whd in match (append ???); >associative_append 1571 >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%); 1572 whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons 1573 >append_nil whd in match (append ???) in ⊢ (???%); // 1574  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct(EQ) 1637 [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] cases(memb ???) normalize nodelta 1638 [ cases(?==?) normalize nodelta ] 1639 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct 1640 xxxxxxx 1641 1642 1643 1575 1644 cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_top''@abs_tail_cont) (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?)))) 1576 1645 [2: whd >EQcont12
Note: See TracChangeset
for help on using the changeset viewer.