Changeset 1964 for src/common/StructuredTraces.ma
 Timestamp:
 May 17, 2012, 12:06:34 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/StructuredTraces.ma
r1949 r1964 20 20 ; as_pc_of : as_status → as_pc 21 21 ; as_classifier : as_status → status_class → Prop 22 ; as_label : as_status→ option costlabel22 ; as_label_of_pc : as_pc → option costlabel 23 23 ; as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop 24 24 ; as_final: as_status → Prop 25 25 }. 26 27 definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc … (as_pc_of … s). 26 28 27 29 (* temporary alias for backward compatibility *) … … 435 437 tal_rel … tl1 tal2 (* < this makes it many to many *) 436 438 ]. 439 440 interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2). 441 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 437 444 438 445 let rec flatten_trace_label_label … … 440 447 (start_status: S) (final_status: S) 441 448 (the_trace: trace_label_label S trace_ends_flag start_status final_status) 442 on the_trace: list (Σl: costlabel. ∃ s. as_label S s= Some … l) ≝449 on the_trace: list (Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝ 443 450 match the_trace with 444 451 [ tll_base ends_flag initial final given_trace labelled_proof ⇒ … … 455 462 (start_status: S) (final_status: S) 456 463 (the_trace: trace_any_label S trace_ends_flag start_status final_status) 457 on the_trace: list (Σl: costlabel. ∃s. as_label … s= Some … l) ≝464 on the_trace: list (Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝ 458 465 match the_trace with 459 466 [ tal_base_not_return the_status _ _ _ _ ⇒ [ ] … … 473 480 (start_status: S) (final_status: S) 474 481 (the_trace: trace_label_return S start_status final_status) 475 on the_trace: list (Σl: costlabel. ∃s. as_label … s= Some … l) ≝482 on the_trace: list (Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝ 476 483 match the_trace with 477 484 [ tlr_base before after trace_to_lift ⇒ … … 485 492 cases abs abs #abs @abs % 486 493 1: 487 %{initial} whd in match label; 494 %{(as_pc_of … initial)} whd in match label; 495 change with (as_label ?? = ?) 488 496 generalize in match labelled_proof; whd in ⊢ (% → ?); 489 497 cases (as_label S initial) … … 595 603 qed. 596 604 605 definition as_cost_map ≝ 606 λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ. 607 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 *) 616 ]. 617 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/ 625 qed. 626 627 notation > "Σ_{ ident i ∈ l } f" 628 with precedence 20 629 for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}. 630 notation < "Σ_{ ident i ∈ l } f" 631 with precedence 20 632 for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}. 633 634 definition as_cost_of_trace_any_label : 635 ∀S : abstract_status. 636 ∀fl, start, end. 637 as_cost_map S → 638 trace_any_label S fl start end → ℕ ≝ 639 λS,fl,start,end,m,the_trace. 640 Σ_{ l_sig ∈ flatten_trace_any_label … the_trace } (m l_sig). 641 642 definition as_cost_of_trace_label_label : 643 ∀S : abstract_status. 644 ∀fl, start, end. 645 as_cost_map S → 646 trace_label_label S fl start end → ℕ ≝ 647 λS,fl,start,end,m,the_trace. 648 Σ_{ l_sig ∈ flatten_trace_label_label … the_trace } (m l_sig). 649 650 definition as_cost_of_trace_label_return : 651 ∀S : abstract_status. 652 ∀start, end. 653 as_cost_map S → 654 trace_label_return S start end → ℕ ≝ 655 λS,start,end,m,the_trace. 656 Σ_{ l_sig ∈ flatten_trace_label_return … the_trace } (m l_sig). 657 658 lemma lift_cost_map_same_cost : 659 ∀S_in, S_out, dec, m_out, trace_in, trace_out. 660 map … (pi1 ??) trace_in = map … (pi1 ??) trace_out → 661 (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) = 662 (Σ_{ l_sig ∈ trace_out } (m_out l_sig)). 663 #S_in #S_out #dec #m_out #trace_in elim trace_in 664 [2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out] 665 normalize in ⊢ (%→?); 666 [2,3: #ABS destruct(ABS) 667 4: #_ % 668 1: 669 #EQ destruct 670 whd in ⊢(??%%); 671 >(lift_cost_map_id_eq … e0) 672 >e0 in e1; normalize in ⊢(%→?); #EQ 673 >(IH … EQ) % 674 ] 675 qed. 676 677 lemma lift_cost_map_same_cost_tal : 678 ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out. 679 ∀the_trace_in : trace_any_label S_in f_in start_in end_in. 680 ∀the_trace_out : trace_any_label S_out f_out start_out end_out. 681 tal_rel … the_trace_in the_trace_out → 682 as_cost_of_trace_any_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in = 683 as_cost_of_trace_any_label … m_out the_trace_out. 684 #S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out 685 #tal_in #tal_out #H_tal 686 @(lift_cost_map_same_cost … (tal_rel_to_traces_same_flatten … H_tal)) 687 qed. 688 689 lemma lift_cost_map_same_cost_tll : 690 ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out. 691 ∀the_trace_in : trace_label_label S_in f_in start_in end_in. 692 ∀the_trace_out : trace_label_label S_out f_out start_out end_out. 693 tll_rel … the_trace_in the_trace_out → 694 as_cost_of_trace_label_label … (lift_cost_map_id S_in S_out dec m_out) the_trace_in = 695 as_cost_of_trace_label_label … m_out the_trace_out. 696 #S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out 697 #tll_in #tll_out #H_tll 698 @(lift_cost_map_same_cost … (tll_rel_to_traces_same_flatten … H_tll)) 699 qed. 700 701 lemma lift_cost_map_same_cost_tlr : 702 ∀S_in, S_out, dec, m_out, start_in, start_out, end_in, end_out. 703 ∀the_trace_in : trace_label_return S_in start_in end_in. 704 ∀the_trace_out : trace_label_return S_out start_out end_out. 705 tlr_rel … the_trace_in the_trace_out → 706 as_cost_of_trace_label_return … (lift_cost_map_id S_in S_out dec m_out) the_trace_in = 707 as_cost_of_trace_label_return … m_out the_trace_out. 708 #S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out 709 #tlr_in #tlr_out #H_tlr 710 @(lift_cost_map_same_cost … (tlr_rel_to_traces_same_flatten … H_tlr)) 711 qed.
Note: See TracChangeset
for help on using the changeset viewer.