Changeset 2417
 Timestamp:
 Oct 25, 2012, 4:36:07 PM (7 years ago)
 Location:
 src
 Files:

 1 added
 3 edited
Legend:
 Unmodified
 Added
 Removed

src/common/StructuredTraces.ma
r2413 r2417 10 10  cl_return: status_class 11 11  cl_jump: status_class 12  cl_call: ident →status_class12  cl_call: status_class 13 13  cl_other: status_class. 14 14 … … 21 21 ; as_classifier : as_status → status_class → Prop 22 22 ; as_label_of_pc : as_pc → option costlabel 23 ; as_after_return : (Σs:as_status. ∃f.as_classifier s (cl_call f)) → as_status → Prop23 ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop 24 24 ; as_final: as_status → Prop 25 25 }. … … 90 90 ∀status_final: S. 91 91 as_execute S status_pre_fun_call status_start_fun_call → 92 ∀ f.∀H:as_classifier S status_pre_fun_call (cl_call f).93 as_after_return S (mk_Sig ?? status_pre_fun_call (ex_intro ?? f H))status_final →92 ∀H:as_classifier S status_pre_fun_call cl_call. 93 as_after_return S «status_pre_fun_call, H» status_final → 94 94 trace_label_return S status_start_fun_call status_final → 95 95 as_costed S status_final → … … 103 103 ∀status_final: S. 104 104 as_execute S status_pre_fun_call status_start_fun_call → 105 ∀ f.∀H:as_classifier S status_pre_fun_call (cl_call f).106 as_after_return S (mk_Sig ?? status_pre_fun_call (ex_intro ?? f H))status_after_fun_call →105 ∀H:as_classifier S status_pre_fun_call cl_call. 106 as_after_return S «status_pre_fun_call, H» status_after_fun_call → 107 107 trace_label_return S status_start_fun_call status_after_fun_call → 108 108 ¬ as_costed S status_after_fun_call → … … 123 123 on tal : list (as_pc S) ≝ 124 124 match tal with 125 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ _tl ⇒ as_pc_of … pre :: tal_pc_list … tl125 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl 126 126  tal_step_default fl' pre st1' st2' _ tl _ _ ⇒ as_pc_of … pre :: tal_pc_list … tl 127 127  tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre] 128 128  tal_base_return pre _ _ _ ⇒ [as_pc_of … pre] 129  tal_base_call pre _ _ _ _ _ _ _ _⇒ [as_pc_of … pre]129  tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre] 130 130 ]. 131 131 … … 155 155 and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝ 156 156 match tal with 157 [ tal_step_call fl st1 st2 st3 st4 _ _ _ _tlr _ tl ⇒157 [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒ 158 158 bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧ 159 159 tal_unrepeating … tl ∧ … … 162 162 bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧ 163 163 tal_unrepeating … tl 164  tal_base_call pre _ _ _ _ _ _trace _ ⇒ tlr_unrepeating … trace164  tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace 165 165  _ ⇒ True 166 166 ]. … … 182 182 cases tal // 183 183 #fl' #st1' [#st_fun] #st2' #st3' #H 184 [ # f #H0 #H1 #tlr #G #tal  #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*184 [ #H0 #H1 #tlr #G #tal  #tal #H0 #G ] whd in ⊢ (% → ?%); [*]* 185 185 #A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption 186 186 qed. … … 198 198 [ #s1 #s2 #EX #CL #CS 199 199  #s1 #s2 #EX #CL 200  #s1 #s2 #s3 #EX # f #CL #AF #tlr #CS201  #fl #s1 #s2 #s3 #s4 #EX # f #CL #AF #tlr #CS #tal200  #s1 #s2 #s3 #EX #CL #AF #tlr #CS 201  #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal 202 202  #fl #s1 #s2 #s3 #EX #tal #CL #CS 203 203 ] whd in ⊢ (??(λ_.??%?)); % [ 2,4,6,8,10: %  *: skip ] … … 210 210 [ #start #final #EX #CL #CS #CS' % // @(not_costed_no_label ?? CS') 211 211  #start #final #EX #CL #CS % // @(not_costed_no_label ?? CS) 212  #pre #start #final #EX # f #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')213  #fl' #pre #start #after #final #EX # f #CL #AF #tlr #CS #tal' #CS'212  #pre #start #final #EX #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS') 213  #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal' #CS' 214 214 cases (tal_pc_list_start … tal') 215 215 #hd #E >E … … 225 225  tac_base: 226 226 ∀status: S. 227 (∃f.as_classifier S status (cl_call f))→227 as_classifier S status cl_call → 228 228 trace_any_call S status status 229 229  tac_step_call: … … 233 233 ∀status_start_fun_call: S. 234 234 as_execute S status_pre_fun_call status_start_fun_call → 235 ∀H: ∃f.as_classifier S status_pre_fun_call (cl_call f).235 ∀H:as_classifier S status_pre_fun_call cl_call. 236 236 as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call → 237 237 trace_label_return S status_start_fun_call status_after_fun_call → … … 278 278 trace_label_call S status_initial status_pre_fun_call → 279 279 as_execute S status_pre_fun_call status_start_fun_call → 280 ∀H: ∃f.as_classifier S status_pre_fun_call (cl_call f).280 ∀H:as_classifier S status_pre_fun_call cl_call. 281 281 trace_label_diverges S status_start_fun_call → 282 282 trace_label_diverges S status_initial. … … 303 303 trace_label_call S status_initial status_pre_fun_call → 304 304 as_execute S status_pre_fun_call status_start_fun_call → 305 ∀H: ∃f.as_classifier S status_pre_fun_call (cl_call f).305 ∀H:as_classifier S status_pre_fun_call cl_call. 306 306 trace_label_diverges_exists S status_start_fun_call → 307 307 trace_label_diverges_exists S status_initial. … … 312 312 ∀status_start_fun: S. 313 313 ∀status_final: S. 314 (∃f.as_classifier S status_initial (cl_call f))→314 as_classifier S status_initial cl_call → 315 315 as_execute S status_initial status_start_fun → 316 316 trace_label_return S status_start_fun status_final → … … 320 320 ∀status_initial: S. 321 321 ∀status_start_fun: S. 322 (∃f.as_classifier S status_initial (cl_call f))→322 as_classifier S status_initial cl_call → 323 323 as_execute S status_initial status_start_fun → 324 324 trace_label_diverges S status_start_fun → … … 331 331 ∀status_start_fun: S. 332 332 ∀status_final: S. 333 (∃f.as_classifier S status_initial (cl_call f))→333 as_classifier S status_initial cl_call → 334 334 as_execute S status_initial status_start_fun → 335 335 trace_label_return S status_start_fun status_final → … … 339 339 ∀status_initial: S. 340 340 ∀status_start_fun: S. 341 (∃f.as_classifier S status_initial (cl_call f))→341 as_classifier S status_initial cl_call → 342 342 as_execute S status_initial status_start_fun → 343 343 trace_label_diverges_exists S status_start_fun → … … 350 350 [ tal_base_not_return start final _ _ C ⇒ C 351 351  tal_base_return _ _ _ _ ⇒ I 352  tal_base_call _ _ _ _ _ _ _ _C ⇒ C353  tal_step_call f pre start after final X fC RET LR C' tr' ⇒ trace_any_label_label … tr'352  tal_base_call _ _ _ _ _ _ _ C ⇒ C 353  tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr' 354 354  tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr' 355 355 ]. … … 371 371 372 372 lemma trace_any_call_call : ∀S,s,s'. 373 trace_any_call S s s' → ∃f.as_classifier S s' (cl_call f).373 trace_any_call S s s' → as_classifier S s' cl_call. 374 374 #S #s #s' #T elim T [1,3: //] 375 375 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 // … … 517 517 tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa 518 518 (tal_base_return ? st2mid st2' H G) 519  tal_base_call st1 st1' st1'' _ _ _ _tlr1 _ ⇒519  tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ 520 520 fl2 = doesnt_end_with_ret ∧ 521 521 ∃st2mid.∃taa : trace_any_any ? st2 st2mid.∃st2mid',H. … … 524 524 we cannot use trace_any_any as it disallows labels in the end as soon 525 525 as it is nonempty) *) 526 (∃ f,G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.527 tal2 ≃ taa @ (tal_base_call … H fG K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨528 ∃st2mid'', f,G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.526 (∃G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L. 527 tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨ 528 ∃st2mid'',G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L. 529 529 ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'. 530 tal2 ≃ taa @ (tal_step_call … H fG K tlr2 L tl2) ∧530 tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧ 531 531 tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2 532  tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ _tlr1 _ tl1 ⇒532  tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ 533 533 ∃st2mid.∃taa : trace_any_any ? st2 st2mid.∃st2mid',H. 534 (fl2 = doesnt_end_with_ret ∧ ∃ f,G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.535 tal2 ≃ taa @ tal_base_call … H fG K tlr2 L ∧534 (fl2 = doesnt_end_with_ret ∧ ∃G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L. 535 tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧ 536 536 tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨ 537 ∃st2mid'', f,G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.537 ∃st2mid'',G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L. 538 538 ∃tl2 : trace_any_label ? fl2 st2mid'' st2'. 539 tal2 ≃ taa @ (tal_step_call … H fG K tlr2 L tl2) ∧539 tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧ 540 540 tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2 541 541  tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ … … 552 552 cases tal1 fl1 s1 s1' // 553 553 [ #s1 #s1' #H #I * 554  #s1 #s1' #s1'' #s1''' #s1'''' #H # f #I #J #tlr #K #tl *554  #s1 #s1' #s1'' #s1''' #s1'''' #H #I #J #tlr #K #tl * 555 555  #fl1 #s1 #s1' #s1'' #H #tl #I #J @(tal_collapsable_eq_fl … tl) 556 556 ] … … 563 563 [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ? 564 564  tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ? 565  tal_base_call st1 st1' st1'' _ _ _ _tlr1 _ ⇒ let BASE_C ≝ 0 in ?566  tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ _tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?565  tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ? 566  tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ? 567 567  tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ? 568 568 ]. … … 570 570 [1,2,3: tal_rel_eq_fl #tal2 * // 571 571  #tal2 * #s2_mid * #taa2 * #s2' *#H2 * 572 [ * #EQ1 *# f *#G2 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) //573  * #s2_mid' *# f *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_572 [ * #EQ1 *#G2 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) // 573  * #s2_mid' *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_ 574 574 @(tal_rel_eq_fl … step) 575 575 ] … … 603 603 [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ? 604 604  tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ? 605  tal_base_call st1 st1' st1'' _ _ _ _tlr1 _ ⇒ let BASE_C ≝ 0 in ?606  tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ _tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?605  tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ? 606  tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ? 607 607  tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ? 608 608 ]. … … 637 637 match the_trace with 638 638 [ tal_base_not_return the_status _ _ _ _ ⇒ [ ] 639  tal_base_call pre_fun_call start_fun_call final _ _ _ _call_trace _ ⇒639  tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ 640 640 flatten_trace_label_return … call_trace 641 641  tal_base_return the_status _ _ _ ⇒ [ ] 642 642  tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final 643 _ _ _ _call_trace _ final_trace ⇒643 _ _ _ call_trace _ final_trace ⇒ 644 644 let call_cost_trace ≝ flatten_trace_label_return … call_trace in 645 645 let final_cost_trace ≝ flatten_trace_any_label … end_flag … final_trace in … … 730 730 [ tal_base_not_return st1 st1' H G K ⇒ ? 731 731  tal_base_return st1 st1' H G ⇒ ? 732  tal_base_call st1 st1' st1'' H fG K tlr1 L ⇒ ?733  tal_step_call fl1 st1 st1' st1'' st1''' H fG K tlr1 L tl1 ⇒ ?732  tal_base_call st1 st1' st1'' H G K tlr1 L ⇒ ? 733  tal_step_call fl1 st1 st1' st1'' st1''' H G K tlr1 L tl1 ⇒ ? 734 734  tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ? 735 735 ] … … 760 760 [ *#H' *#G' *#K' #EQ 761 761  *#H' *#G' #EQ 762  *#st_mid' *#H' * [*#st2_mid''] *# f' *#G' *#K' *#tlr2 *#L'762  *#st_mid' *#H' * [*#st2_mid''] *#G' *#K' *#tlr2 *#L' 763 763 [*#tl2 *] * #EQ #H_tlr [ #H_tl] 764 764  *#st_fun *#H' * 765 [*#fl_EQ destruct(fl_EQ) * #st2_mid ] *# f' *#G' *#K' *#tlr2 *#L'765 [*#fl_EQ destruct(fl_EQ) * #st2_mid ] *#G' *#K' *#tlr2 *#L' 766 766 [ *#tl2] ** #EQ #H_tl #H_tlr 767 767 ] >EQ >taa_append_tal_same_flatten 
src/joint/Joint_jaap.ma
r2398 r2417 175 175 [ step_seq s ⇒ 176 176 match s with 177 [ CALL_ID l _ _ ⇒ cl_calll178  extension_call _ ⇒ cl_call ? (* pointer stuff not yet implemented, it seems *)177 [ CALL_ID _ _ _ ⇒ cl_call 178  extension_call _ ⇒ cl_call 179 179  _ ⇒ cl_other 180 180 ] 181 181  COND _ _ ⇒ cl_jump 182 182 ]. 183 cases daemon184 qed.185 183 186 184 record stmt_params : Type[1] ≝ 
src/joint/stacksize.ma
r2398 r2417 47 47 [ tal_base_not_return s1 s2 ex cl co ⇒ res 48 48  tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res 49  tal_base_call s1p s1s s2 ex f clar tlr co ⇒49  tal_base_call s1p s1s s2 ex cl f ca ar tlr co ⇒ 50 50 extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) 51  tal_step_call end s1p s1s s1a s2 ex f clar tlr co tal ⇒51  tal_step_call end s1p s1s s1a s2 ex cl f ca ar tlr co tal ⇒ 52 52 let res' ≝ extract_list_from_tlr … lg f … tlr (up ?? (lg f)::res) in 53 53 extract_list_from_tal … lg top_f … tal res' … … 81 81 ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res = 82 82 extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝ 83 match t1 with 84 [ tal_base_not_return st1 st1' ex cl co ⇒ ? 85  tal_base_return st1 st1' ex cl ⇒ ? 86  tal_base_call st1p st1s st1' ex cl f ca ar tlr1 co ⇒ ? 87  tal_step_call end st1p st1s st1 st1' ex cl f ca ar tlr1 co tal1 ⇒ ? 88  tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? 89 ]. 90 [ cases t2 91 [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim) 92  #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs 93 ] 94  cases t2 95 [ #st2 #st2' #tll2 normalize #abs cases abs 96  #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res 97 >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res) 98 @(tlr_rel_extract_equal … (proj2 ?? Hsim)) 99 ] 100  cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2 101 @(tal_rel_extract_equal … H2) 102  cases t2 103 [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res % 104  #st2 #st2' #ex' #cl' * #abs destruct (abs) 105  #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #H1 * #st2mid * 106 #taa * #H * #G * #K inversion taa in ⊢ ?; 107 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 108  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 109 normalize #abs destruct (abs) 110 ] 111  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 normalize * 112 #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?; 113 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 114  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 115 normalize #abs destruct (abs) 116 ] 117  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa 118 * #H * #G * #K inversion taa in ⊢ ?; 119 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 120  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 121 destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *) 122 ] 123 ] 124  cases t2 125 [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs) 126  #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % 127  #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #abs destruct (abs) 128  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 129 normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?; 130 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 131  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 132 normalize #abs destruct (abs) 133 ] 134  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid 135 * #taa * #H * #G inversion taa in ⊢ ?; 136 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 137  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 138 destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *) 139 ] 140 ] 141  cases t2 142 [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #taa 143 * #st2mid' * #H * * [2: #st2mid'' *] #J * #f' * #G * #K * #tlr2 * #L * #H1 144 [ * * #H3 #H2 #H4  #H2 ] 145 inversion taa in ⊢ ?; 146 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3) 147  #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 148 normalize in H3; destruct (H3) 149  #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1) 150  #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 151 normalize in H1; destruct (H1) 152 ] 153  #st2 #st2' #ex' #cl' normalize * #abs destruct (abs) 154  #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #_ * #st2mid * 155 #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f'' * #G * #K * #tlr2' * #L 156 inversion taa in ⊢ ?; 157 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #tal2 * * #H1 destruct (H1) 158  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 159 destruct normalize * #tal2 * * #H1 destruct (H1) 160  #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res 161 >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *) 162  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 163 destruct normalize * #abs destruct (abs) 164 ] 165  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 166 normalize * #H1 * #st2mid * #taa * #st2mid' * #H * * [2: #st2mid'' *] #J * #f 167 * #G * #K * #tlr2' * #L 168 inversion taa in ⊢ ?; 169 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 #H2 #H3 #res 170 cases daemon 171  #st2p' #st2p'' #st2mid'; #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 172 destruct normalize * #tal2' * * #H1 destruct (H1) 173  #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs) 174  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 175 destruct normalize * #abs destruct (abs) 176 ] 177  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * 178 #taa * #st2mid' * #H * * [2: #stmid'' * ] #J * #f * #G * #K * #tlr2 * #L 179 inversion taa in ⊢ ?; 180 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #tal2' * * #H1 destruct (H1) 181  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 182 destruct normalize * #tal2' * * #H1 #H2 #H3 #res cases daemon 183  #st2mid''' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs) 184  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 185 destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *) 186 ] 187 ] 188  cases t2 189 [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun * 190 #st2_after_fun * * [#H  #st2mid'] * #J * #f' * #G * #K * #tlr2 * #L [2: * #tl2] 191 inversion taa in ⊢ ?; 192 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1) 193  #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 194 normalize * * #H1 destruct (H1) 195  #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 196  #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 197 normalize * * #abs destruct (abs) 198 ] 199  #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2mid' * #H * 200 [ * #abs destruct (abs)  * #st2mid'' * #J * #f' * #G * #K * #tlr2 * #L * #tl2 201 inversion taa in ⊢ ?; 202 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 203  #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 204 normalize * * #abs destruct (abs) 205 ] 206 ] 207  #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize * #st2mid * #taa 208 * #st2mid' * #H * * [ #_  #st2mid'' ] * #J * #f'' * #G * #K * #tlr2' * #L [2: * #tl2] 209 inversion taa in ⊢ ?; 210 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 211  #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 212 destruct normalize * * #abs destruct (abs) 213  #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 cases daemon 214  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 215 destruct normalize * * #abs destruct (abs) 216 ] 217  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 218 normalize * #st2mid * #taa * #st2mid' * #ex'' * * [ #_  #st2mid''] * #J * 219 #f'' * #G * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?; 220 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res 221 cases daemon (* injectivity needed again *) 222  #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 223 destruct normalize * * #abs destruct (abs) 224  #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) cases daemon 225 (* huh? *) 226  #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 227 destruct normalize * * #abs destruct (abs) cases daemon (* huh2? *) 228 ] 229  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa * 230 #st2mid' * #H * * [ #He  #st2mid'' ] * #J * #f' * #G * #K * #tlr2' * #L 231 [2: * #tl2] inversion taa in ⊢ ?; 232 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 233  #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 234 destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *) 235  #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 236  #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 237 destruct normalize * * #H1 #H2 #H3 #res cases daemon 238 ] 239 ] 240  cases t2 241 [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res 242 @(tal_rel_extract_equal p g lg top_f … Hsim) 243  #ss #fs #ex' #cl' normalize #Hsim #res 244 @(tal_rel_extract_equal p g lg top_f … Hsim) 245  #st2p #st2s #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' normalize #Hsim #res 246 @(tal_rel_extract_equal p g lg top_f … Hsim) 247  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #f' #ca' #ar' #tlr2 #co' #tal2 248 normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim) 249  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res 250 @(tal_rel_extract_equal p g lg top_f … Hsim) 251 ] 252 ] 253 qed. 254 255 (* let rec tlr_rel_max_equal (p: params) (g: list ident) 256 (lg: ident → joint_internal_function p g) (top_f: ident) 257 S1 S2 s1 s1' s2 s2' t1 t2 on t1: 258 tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 → 259 max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) = 260 max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝ 261 match t1 with 262 [ tlr_base st1 st1' tll1 ⇒ ? 263  tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ? 264 ] 265 and tll_rel_extract_equal (p: params) (g: list ident) 266 (lg: ident → joint_internal_function p g) (top_f: ident) 267 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: 268 t1 ≈ t2 → 269 max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) = 270 max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝ 271 match t1 with 272 [ tll_base ends st1 st1' tal1 co ⇒ ? 273 ] 274 and tal_rel_extract_equal (p: params) (g: list ident) 275 (lg: ident → joint_internal_function p g) (top_f: ident) 276 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: 277 t1 ≈ t2 → 278 max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) = 279 max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝ 83 280 match t1 with 84 281 [ tal_base_not_return st1 st1' ex cl co ⇒ ? … … 88 285  tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? 89 286 ]. 90 [ cases t291 [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim)92  #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs93 ]94  cases t295 [ #st2 #st2' #tll2 normalize #abs cases abs96  #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res97 >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res)98 @(tlr_rel_extract_equal … (proj2 ?? Hsim))99 ]100  cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2101 @(tal_rel_extract_equal … H2)102  cases t2103 [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res %104  #st2 #st2' #ex' #cl' * #abs destruct (abs)105  #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid *106 #taa * #H * #G * #K inversion taa in ⊢ ?;107 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)108  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct109 normalize #abs destruct (abs)110 ]111  #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2 normalize *112 #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?;113 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)114  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct115 normalize #abs destruct (abs)116 ]117  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa118 * #H * #G * #K inversion taa in ⊢ ?;119 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)120  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3121 destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)122 ]123 ]124  cases t2125 [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs)126  #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res %127  #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs)128  #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2129 normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?;130 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)131  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct132 normalize #abs destruct (abs)133 ]134  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid135 * #taa * #H * #G inversion taa in ⊢ ?;136 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs)137  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3138 destruct normalize #Hsim cases daemon (* use injectivity from Hsim? *)139 ]140 ]141  cases t2142 [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #taa143 * #st2mid' * #H * #f' * #G * #K * #tlr2 * #L * #H1 #H2 inversion taa in ⊢ ?;144 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1)145  #st2'' #st2''' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct146 normalize in H1; destruct (H1)147 ]148  #st2 #st2' #ex' #cl' normalize * #abs destruct (abs)149  #st2p #st2s #st2' #ex' #f' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid *150 #taa * #st2mid' * #H * #f'' * #G * #K * #tlr2' * #L inversion taa in ⊢ ?;151 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res152 >(tlr_rel_extract_equal p g lg f … H2) cases daemon (* use injectivity and H1? *)153  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3154 destruct normalize * #abs destruct (abs)155 ]156  #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2157 normalize * #H1 * #st2mid * #taa * #st2mid' * #H * #f * #G * #K * #tlr2' * #L158 inversion taa in ⊢ ?;159 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)160  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3161 destruct normalize * #abs destruct (abs)162 ]163  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid *164 #taa * #st2mid' * #H * #f * #G * #K * #tlr2 * #L inversion taa in ⊢ ?;165 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #abs destruct (abs)166  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3167 destruct normalize * #H1 #H2 #res cases daemon (* do something with H1 and H2 *)168 ]169 ]170  cases t2171 [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun172 * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;173 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)174  #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct175 normalize * * #abs destruct (abs)176 ]177  #st2 #st2' #ex' #cl' normalize * #st2mid * #taa * #st2_fun * #st2_after_fun178 * #H * #f' * #G * #K * #tlr2 * #L * #tl2 inversion taa in ⊢ ?;179 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)180  #st2p #st2p' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct181 normalize * * #abs destruct (abs)182 ]183  #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize * #st2mid * #taa184 * #st2_fun * #st2_after_fun * #H' * #f'' * #G * #K * #tlr2' * #L * #tl2185 inversion taa in ⊢ ?;186 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)187  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3188 destruct normalize * * #abs destruct (abs)189 ]190  #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2191 normalize * #st2mid * #taa * #st2_fun * #st2_after_fun * #H * #f'' *192 #G * #K * #tlr2' * #L * #tl2 inversion taa in ⊢ ?;193 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res194 >(tlr_rel_extract_equal … H2) cases daemon (* injectivity needed again *)195  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3196 destruct normalize * * #abs destruct (abs)197 ]198  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #taa *199 #st2_fun * #st2_after_fun * #H * #f' * #G * #K * #tlr2' * #L * #tl2200 inversion taa in ⊢ ?;201 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs)202  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3203 destruct normalize * * #H1 #H2 #H3 #res cases daemon (* look into this *)204 ]205 ]206  cases t2207 [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res208 @(tal_rel_extract_equal p g lg top_f … Hsim)209  #ss #fs #ex' #cl' normalize #Hsim #res210 @(tal_rel_extract_equal p g lg top_f … Hsim)211  #st2p #st2s #st2' #ex' #f' #H #ar' #tlr2 #co' normalize #Hsim #res212 @(tal_rel_extract_equal p g lg top_f … Hsim)213  #ends' #st2p #st2s #st2 #st2' #ex' #f' #cl' #ar' #tlr2 #co' #tal2214 normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim)215  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize #Hsim #res216 @(tal_rel_extract_equal p g lg top_f … Hsim)217 ]218 ]219 qed.220 221 let rec tlr_rel_max_equal (p: params) (g: list ident)222 (lg: ident → joint_internal_function p g) (top_f: ident)223 S1 S2 s1 s1' s2 s2' t1 t2 on t1:224 tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 →225 max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) =226 max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝227 match t1 with228 [ tlr_base st1 st1' tll1 ⇒ ?229  tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ?230 ]231 and tll_rel_extract_equal (p: params) (g: list ident)232 (lg: ident → joint_internal_function p g) (top_f: ident)233 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:234 t1 ≈ t2 →235 max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) =236 max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝237 match t1 with238 [ tll_base ends st1 st1' tal1 co ⇒ ?239 ]240 and tal_rel_extract_equal (p: params) (g: list ident)241 (lg: ident → joint_internal_function p g) (top_f: ident)242 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1:243 t1 ≈ t2 →244 max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) =245 max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝246 match t1 with247 [ tal_base_not_return st1 st1' ex cl co ⇒ ?248  tal_base_return st1 st1' ex cl ⇒ ?249  tal_base_call st1p st1s st1' ex f cl ar tlr1 co ⇒ ?250  tal_step_call end st1p st1s st1 st1' ex f cl ar tlr1 co tal1 ⇒ ?251  tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ?252 ].253 287 cases daemon (* next proof *) 254 qed. 288 qed. *) 255 289 256 290
Note: See TracChangeset
for help on using the changeset viewer.