Changeset 2186 for src/common
- Timestamp:
- Jul 16, 2012, 4:59:09 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/StructuredTraces.ma
r2129 r2186 334 334 qed. 335 335 336 (* an uncalling, unreturning and *unjumping*, 337 as well as unlabelled (but possibly for the first and last statuses) 338 possibly empty trace segment *) 339 inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝ 340 | taa_base : 336 (* 337 (* an trace of unlabeled and cl_other states, possibly empty *) 338 inductive trace_no_label_any (S:abstract_status) : S → S → Type[0] ≝ 339 | tna_base : 341 340 ∀start_status: S. 342 trace_any_any S start_status start_status 343 | taa_step : 341 ¬as_costed … start_status → 342 trace_no_label_any S start_status start_status 343 | tna_step : 344 344 ∀status_pre: S. 345 345 ∀status_init: S. 346 346 ∀status_end: S. 347 347 as_execute S status_pre status_init → 348 trace_any_any S status_init status_end →349 348 as_classifier S status_pre cl_other → 350 ¬as_costed … status_init → 351 trace_any_any S status_pre status_end. 352 353 let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝ 349 ¬as_costed … status_pre → 350 trace_no_label_any S status_init status_end → 351 trace_no_label_any S status_pre status_end. 352 353 let rec tna_append_tna S st1 st2 st3 (taa1 : trace_no_label_any S st1 st2) 354 on taa1 : 355 trace_no_label_any S st2 st3 → 356 trace_no_label_any S st1 st3 ≝ 357 match taa1 with 358 [ tna_base st1' H ⇒ λtaa2.taa2 359 | tna_step st1' st2' st3' H G K tl ⇒ 360 λtaa2.tna_step ???? H G K (tna_append_tna … tl taa2) 361 ]. 362 363 definition tna_non_empty ≝ λS,st1,st2.λtna : trace_no_label_any S st1 st2. 364 match tna with 365 [ tna_base _ _ ⇒ false 366 | tna_step _ _ _ _ _ _ _ ⇒ true 367 ]. 368 369 coercion tna_to_bool : ∀S,st1,st2.∀tna:trace_no_label_any S st1 st2.bool ≝ 370 tna_non_empty on _tna : trace_no_label_any ??? to bool. 371 372 lemma tna_unlabelled : ∀S,st1,st2.trace_no_label_any S st1 st2 → ¬as_costed … st1. 373 #S #st1 #st2 * [#st #H @H | #st #st' #st'' #_ #_ #H #_ @H] qed. 374 375 let rec tna_append_tal S st1 fl st2 st3 (tna : trace_no_label_any S st1 st2) 376 on tna : 377 trace_any_label S fl st2 st3 → 378 if tna then Not (as_costed … st2) else True → 379 trace_any_label S fl st1 st3 ≝ 380 match tna return λst1,st2.λx : trace_no_label_any S st1 st2. 381 ∀fl,st3. 382 trace_any_label S fl st2 st3 → 383 if x then Not (as_costed … st2) else True → 384 trace_any_label S fl st1 st3 385 with 386 [ tna_base st1' H ⇒ λfl,st3,taa2,prf.taa2 387 | tna_step st1' st2' st3' H G K tl ⇒ λfl,st3,taa2,prf. 388 tal_step_default ????? H (tna_append_tal ????? tl taa2 ?) G (tna_unlabelled … tl) 389 ] fl st3. 390 cases (tna_non_empty … tl) [@prf|%] 391 qed. 392 *) 393 394 inductive trace_any_any (S : abstract_status) : S → S → Type[0] ≝ 395 | taa_base : ∀st.trace_any_any S st st 396 | taa_step : ∀st1,st2,st3. 397 as_execute S st1 st2 → 398 as_classifier S st1 cl_other → 399 ¬as_costed S st2 → 400 trace_any_any S st2 st3 → 401 trace_any_any S st1 st3. 402 403 definition taa_non_empty ≝ λS,st1,st2.λtaa : trace_any_any S st1 st2. 354 404 match taa with 355 [ taa_base st1' ⇒ [st1']356 | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl405 [ taa_base _ ⇒ false 406 | taa_step _ _ _ _ _ _ _ ⇒ true 357 407 ]. 358 408 359 let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2) 360 on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝ 361 match taa1 362 return λst1,st2.λx : trace_any_any S st1 st2. 363 trace_any_any S st2 st3 → trace_any_any S st1 st3 364 with 365 [ taa_base _ ⇒ λtaa2.taa2 366 | taa_step st1' st2' st3' H tl G K ⇒ λtaa2. 367 taa_step … H (taa_append_taa … tl taa2) G K 368 ]. 369 370 let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2) 371 on taa : 409 coercion taa_to_bool : ∀S,st1,st2.∀taa:trace_any_any S st1 st2.bool ≝ 410 taa_non_empty on _taa : trace_any_any ??? to bool. 411 412 let rec taa_append_tal S st1 fl st2 st3 413 (taa : trace_any_any S st1 st2) on taa : 372 414 trace_any_label S fl st2 st3 → 373 415 trace_any_label S fl st1 st3 ≝ 374 match taa 375 return λst1,st2.λx : trace_any_any S st1 st2. 376 trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3 416 match taa return λst1,st2.λx : trace_any_any S st1 st2. 417 ∀fl,st3. 418 trace_any_label S fl st2 st3 → 419 trace_any_label S fl st1 st3 377 420 with 378 [ taa_base _ ⇒ λtaa2.taa2 379 | taa_step st1' st2' st3' H tl G K ⇒ λtaa2. 380 tal_step_default … H (taa_append_tal … tl taa2) G K 381 ]. 421 [ taa_base st1' ⇒ λfl,st3,tal2.tal2 422 | taa_step st1' st2' st3' H G K tl ⇒ λfl,st3,tal2. 423 tal_step_default ????? H (taa_append_tal ????? tl tal2) G K 424 ] fl st3. 425 426 interpretation "trace any any label append" 'append taa tal = (taa_append_tal ????? taa tal). 382 427 383 428 let rec tlr_rel S1 st1 st1' S2 st2 st2' … … 416 461 fl2 = doesnt_end_with_ret ∧ 417 462 ∃st2mid,taa,H,G,K. 418 tal2 ≃ taa_append_tal ? st2 ? st2mid st2'taa463 tal2 ≃ taa_append_tal ? st2 ??? taa 419 464 (tal_base_not_return ? st2mid st2' H G K) 420 465 | tal_base_return st1 st1' _ _ ⇒ … … 437 482 tal_rel … tl1 tal2 (* <- this makes it many to many *) 438 483 ]. 439 484 440 485 interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2). 441 486 interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2). 442 interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ???????? t1 t2). 443 487 interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ?????? t1 t2). 488 489 let rec taa_rel_inv S1 fl1 st1 st1mid st1' S2 fl2 st2 st2' 490 (taa1 : trace_any_any S1 st1 st1mid) on taa1 : 491 ∀tal1 : trace_any_label S1 fl1 st1mid st1'. 492 ∀tal2 : trace_any_label S2 fl2 st2 st2'. 493 tal_rel … (taa1 @ tal1) tal2 → 494 tal_rel … tal1 tal2 ≝ ?. 495 cases taa1 -taa1 496 [ -taa_rel_inv // 497 | #st #st' #st'' #H #G #K #tl #tal1 #tal2 whd in ⊢ (%→?); 498 @(taa_rel_inv … tl) 499 ] 500 qed. 501 502 let rec tlr_rel_transitive S1 st1 st1' S2 st2 st2' S3 st3 st3' 503 (tlr1 : trace_label_return S1 st1 st1') 504 (tlr2 : trace_label_return S2 st2 st2') 505 (tlr3 : trace_label_return S3 st3 st3') on tlr1 : 506 tlr_rel … tlr1 tlr2 → tlr_rel … tlr2 tlr3 → tlr_rel … tlr1 tlr3 ≝ 507 match tlr1 with 508 [ tlr_base st1' st1'' tll1 ⇒ ? 509 | tlr_step st1' st1'' st1''' tll1 tl1 ⇒ ? 510 ] 511 and tll_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3' 512 (tll1 : trace_label_label S1 fl1 st1 st1') 513 (tll2 : trace_label_label S2 fl2 st2 st2') 514 (tll3 : trace_label_label S3 fl3 st3 st3') on tll1 : 515 tll1 ≈ tll2 → tll2 ≈ tll3 → tll1 ≈ tll3 ≝ 516 match tll1 with 517 [ tll_base fl1' st1' st1'' tal1 H ⇒ ? 518 ] 519 and tal_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3' 520 (tal1 : trace_any_label S1 fl1 st1 st1') 521 (tal2 : trace_any_label S2 fl2 st2 st2') 522 (tal3 : trace_any_label S3 fl3 st3 st3') on tal1 : 523 tal1 ≈ tal2 → tal2 ≈ tal3 → tal1 ≈ tal3 ≝ 524 match tal1 with 525 [ tal_base_not_return st1' st1'' H G K ⇒ ? 526 | tal_base_return st1' st1'' H G ⇒ ? 527 | tal_base_call st1' st1'' st1''' H G K tlr1 L ⇒ ? 528 | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ? 529 | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ? 530 ]. 531 [1,2: cases tlr2 #st2' #st2'' [1,3: #tllhd2 |2,4: #st2''' #tllhd2 #tlrtl2] 532 [2,3: *] normalize in ⊢ (%→?); [ #Rhd12 | * #Rhd12 #Rtl12 ] 533 cases tlr3 #st3' #st3'' [1,3: #tllhd3 |2,4: #st3''' #tllhd3 #tlrtl3] 534 [2,3: *] normalize in ⊢ (%→?); [ #Rhd23 | * #Rhd23 #Rtl23 ] whd 535 [ @(tll_rel_transitive … Rhd12 Rhd23) | 536 %{(tll_rel_transitive … Rhd12 Rhd23)} 537 @(tlr_rel_transitive … Rtl12 Rtl23) 538 ] 539 |3: 540 cases tll2 #fl2' #st2' #st2'' #tal2 #H2 * #G2 #R12 541 cases tll3 #fl3' #st3' #st3'' #tal3 #H3 * #G3 #R23 542 %{(tal_rel_transitive … R12 R23)} // 543 |*: 544 [1,2,3: * #EQ] 545 [5: whd in ⊢ (%→?→%); @tal_rel_transitive] 546 *#st2mid *#taa2 547 [ *#H2 *#G2 *#K2 #R12 548 | *#H2 *#G2 #R12 549 | *#st2' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#R12 #R12' 550 | *#st2' *#st2'' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #R12 #R12' #R12'' 551 ] destruct #R23 lapply (taa_rel_inv … R23) [1,2: // |3: *#EQ destruct] 552 *#st3mid *#taa3 553 [ *#st3' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#R23 #R23' 554 %{(refl …)} %{st3mid} %{taa3} %{st3'} %{H3} %{G3} %{K3} %{tlr3} %{L3} 555 %{R23} @(tlr_rel_transitive … R12' R23') 556 | *#st3' *#st3'' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#tl3 ** #R23 #R23' #R23'' 557 %{st3mid} %{taa3} %{st3'} %{st3''} %{H3} %{G3} %{K3} %{tlr3} %{L3} %{tl3} 558 %{(tal_rel_transitive … R12'' R23'')} 559 %{R23} @(tlr_rel_transitive … R12' R23') 560 ] 561 ] 562 qed. 444 563 445 564 let rec flatten_trace_label_label … … 507 626 S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa : 508 627 ∀tal : trace_any_label S fl st2 st3. 509 flatten_trace_any_label … (taa _append_tal … taatal) =628 flatten_trace_any_label … (taa @ tal) = 510 629 flatten_trace_any_label … tal ≝ ?. 511 630 cases taa -st1 -st2 512 [ #st1 #tal %513 | #st_pre #st_init #st2 #H # taa #G #K#tal514 whd in match ( taa_append_tal ???????);631 [ // 632 | #st_pre #st_init #st2 #H #G #K #taa' #tal 633 whd in match (? @ ?); 515 634 whd in ⊢ (??%?); // 516 635 ] 517 qed. 518 636 qed. 519 637 520 638 let rec tll_rel_to_traces_same_flatten … … 606 724 λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ. 607 725 608 definition lift_cost_map_id : 609 ∀S_in, S_out: abstract_status. 610 (∀l. (∃pc.as_label_of_pc S_out pc = Some … l) + 611 ¬(∃pc.as_label_of_pc S_out pc = Some … l)) → 612 (as_cost_map S_out) → as_cost_map S_in ≝ λS_in,S_out,dec,m,l_sig. 613 match dec l_sig with 614 [ inl prf ⇒ m «l_sig, prf» 615 | inr _ ⇒ 0 (* labels not present in out code get 0 *) 726 definition lift_sigma_map_id : 727 ∀A,B : Type[0].∀P_in,P_out : A → Prop.B → 728 (∀a.P_out a + ¬ P_out a) → 729 ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig. 730 match dec a_sig with 731 [ inl prf ⇒ m «a_sig, prf» 732 | inr _ ⇒ dflt (* labels not present in out code get 0 *) 616 733 ]. 617 734 618 lemma lift_cost_map_id_eq : 619 ∀S_in, S_out, dec, m, l_in, l_out. 620 pi1 ?? l_in = pi1 ?? l_out → lift_cost_map_id S_in S_out dec m l_in = m l_out. 621 #S_in #S_out #dec #m #l_in * #l_out #prf #EQ 622 whd in match lift_cost_map_id; normalize nodelta 623 cases (dec l_in) normalize nodelta >EQ 624 [2: #H @⊥] /2 by refl, absurd/ 735 lemma lift_sigma_map_id_eq : 736 ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out. 737 pi1 ?? a_in = pi1 ?? a_out → 738 lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out. 739 #A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ 740 whd in match lift_sigma_map_id; normalize nodelta 741 cases (dec a_in) normalize nodelta >EQ cases a_out 742 #a #H #G [ % | @⊥ /2 by absurd/ ] 625 743 qed. 626 744 … … 631 749 with precedence 20 632 750 for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}. 751 752 definition lift_cost_map_id : 753 ∀S_in,S_out : abstract_status.? → 754 as_cost_map S_out → as_cost_map S_in 755 ≝ 756 λS_in,S_out : abstract_status. 757 lift_sigma_map_id costlabel ℕ 758 (λl.∃pc.as_label_of_pc S_in pc = Some ? l) 759 (λl.∃pc.as_label_of_pc S_out pc = Some ? l) 760 0. 633 761 634 762 lemma lift_cost_map_same_cost : … … 645 773 #EQ destruct 646 774 whd in ⊢(??%%); 647 >(lift_cost_map_id_eq … e0) 775 whd in match lift_cost_map_id; normalize nodelta 776 >(lift_sigma_map_id_eq ????????? e0) 648 777 >e0 in e1; normalize in ⊢(%→?); #EQ 649 778 >(IH … EQ) %
Note: See TracChangeset
for help on using the changeset viewer.