Changeset 2503
 Timestamp:
 Nov 29, 2012, 3:32:50 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/StructuredTraces.ma
r2423 r2503 31 31 32 32 (* temporary alias for backward compatibility *) 33 definition final_abstract_status ≝ abstract_status. 33 (* definition final_abstract_status ≝ abstract_status. *) 34 34 35 35 definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝ 36 36 λa_s,st.as_label ? st ≠ None ?. 37 38 lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) ∨ (¬as_costed S s).39 #S #s whd in match (as_costed S s);40 cases (as_label S s) [ %2 % * /2/  #c %1 % #E destruct ]41 qed.42 37 43 38 definition as_label_safe : ∀a_s : abstract_status. 44 39 (Σs : a_s.as_costed ? s) → costlabel ≝ 45 40 λa_s,st_sig.opt_safe … (pi2 … st_sig). 41 42 lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) + (¬as_costed S s). 43 #S #s whd in match (as_costed S s); 44 cases (as_label S s) [ %2 % * /2/  #c %1 % #E destruct ] 45 qed. 46 47 lemma not_costed_no_label : ∀S,st. 48 ¬as_costed S st → 49 as_label S st = None ?. 50 #S #st * normalize cases (as_label_of_pc S ?) 51 [ //  #l #H cases (H ?) % #E destruct ] 52 qed. 53 54 (* cost maps generalities *) 55 56 definition as_cost_labelled ≝ 57 λS : abstract_status. λl.∃pc.as_label_of_pc S pc = Some ? l. 58 59 definition as_cost_label ≝ 60 λS : abstract_status. Σl.as_cost_labelled S l. 61 62 definition as_cost_labels ≝ 63 λS : abstract_status. list (as_cost_label S). 64 65 definition as_cost_get_label ≝ 66 λS : abstract_status. λl_sig: as_cost_label S. pi1 … l_sig. 67 68 definition as_cost_get_labels ≝ 69 λS : abstract_status. map … (as_cost_get_label S). 70 71 definition as_cost_map ≝ 72 (* λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ. *) 73 λS : abstract_status. (as_cost_label S) → ℕ. 74 75 definition lift_sigma_map_id : 76 ∀A,B : Type[0].∀P_in,P_out : A → Prop.B → 77 (∀a.P_out a + ¬ P_out a) → 78 ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig. 79 match dec a_sig with 80 [ inl prf ⇒ m «a_sig, prf» 81  inr _ ⇒ dflt (* labels not present in out code get 0 *) 82 ]. 83 84 lemma lift_sigma_map_id_eq : 85 ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out. 86 pi1 ?? a_in = pi1 ?? a_out → 87 lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out. 88 #A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ 89 whd in match lift_sigma_map_id; normalize nodelta 90 cases (dec a_in) normalize nodelta >EQ cases a_out 91 #a #H #G [ %  @⊥ /2 by absurd/ ] 92 qed. 93 94 notation > "Σ_{ ident i ∈ l } f" 95 with precedence 20 96 for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}. 97 notation < "Σ_{ ident i ∈ l } f" 98 with precedence 20 99 for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}. 100 101 definition lift_cost_map_id : 102 ∀S_in,S_out : abstract_status.? → 103 as_cost_map S_out → as_cost_map S_in 104 ≝ 105 λS_in,S_out : abstract_status. 106 lift_sigma_map_id costlabel ℕ 107 (*λl.∃pc.as_label_of_pc S_in pc = Some ? l*) (as_cost_labelled S_in) 108 (*λl.∃pc.as_label_of_pc S_out pc = Some ? l*) (as_cost_labelled S_out) 109 0. 110 111 lemma lift_cost_map_same_cost : 112 ∀S_in, S_out, dec, m_out, trace_in, trace_out. 113 map … (pi1 ??) trace_in = map … (pi1 ??) trace_out → 114 (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) = 115 (Σ_{ l_sig ∈ trace_out } (m_out l_sig)). 116 #S_in #S_out #dec #m_out #trace_in elim trace_in 117 [2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out] 118 normalize in ⊢ (%→?); 119 [2,3: #ABS destruct(ABS) 120 4: #_ % 121 1: 122 #EQ destruct 123 whd in ⊢(??%%); 124 whd in match lift_cost_map_id; normalize nodelta 125 >(lift_sigma_map_id_eq ????????? e0) 126 >e0 in e1; normalize in ⊢(%→?); #EQ 127 >(IH … EQ) % 128 ] 129 qed. 130 131 132 (* structured traces: down to business *) 46 133 47 134 inductive trace_ends_with_ret: Type[0] ≝ … … 189 276 qed. 190 277 191 lemma not_costed_no_label : ∀S,st.192 ¬as_costed S st →193 as_label_of_pc S (as_pc_of S st) = None ?.194 #S #st * normalize cases (as_label_of_pc S ?)195 [ //  #l #H cases (H ?) % #E destruct ]196 qed.197 198 278 lemma tal_pc_list_start : ∀S,fl,s1,s2. ∀tal: trace_any_label S fl s1 s2. 199 279 ∃tl. tal_pc_list … tal = (as_pc_of S s1)::tl. … … 209 289 let rec tal_tail_not_costed S fl st1 st2 tal 210 290 (H:Not (as_costed S st1)) on tal : 211 All ? (λ l. as_label_of_pc S l= None ?) (tal_pc_list S fl st1 st2 tal) ≝ ?.291 All ? (λpc. as_label_of_pc S pc = None ?) (tal_pc_list S fl st1 st2 tal) ≝ ?. 212 292 cases tal in H ⊢ %; 213 293 [ #start #final #EX #CL #CS #CS' % // @(not_costed_no_label ?? CS') … … 624 704 (start_status: S) (final_status: S) 625 705 (the_trace: trace_label_label S trace_ends_flag start_status final_status) 626 on the_trace: list ( Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝706 on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝ 627 707 match the_trace with 628 708 [ tll_base ends_flag initial final given_trace labelled_proof ⇒ 629 709 let label ≝ 630 match as_label … initial return λx: option costlabel. x ≠ None costlabel→ ? with710 match as_label … initial return λx: option costlabel. x ≠ None ? → ? with 631 711 [ None ⇒ λabs. ⊥ 632 712  Some l ⇒ λ_. l … … 639 719 (start_status: S) (final_status: S) 640 720 (the_trace: trace_any_label S trace_ends_flag start_status final_status) 641 on the_trace: list ( Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝721 on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝ 642 722 match the_trace with 643 723 [ tal_base_not_return the_status _ _ _ _ ⇒ [ ] … … 657 737 (start_status: S) (final_status: S) 658 738 (the_trace: trace_label_return S start_status final_status) 659 on the_trace: list ( Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l) ≝739 on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝ 660 740 match the_trace with 661 741 [ tlr_base before after trace_to_lift ⇒ … … 681 761 qed. 682 762 763 (* JHM: base case now passes the termination checker *) 683 764 let rec taa_append_tal_same_flatten 684 765 S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa : … … 687 768 flatten_trace_any_label … tal ≝ ?. 688 769 cases taa st1 st2 689 [ //770 [ #st #tal normalize in ⊢ (??%?); // 690 771  #st_pre #st_init #st2 #H #G #K #taa' #tal 691 772 whd in match (? @ ?); … … 797 878 qed. 798 879 799 definition as_cost_map ≝ 800 λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ. 801 802 definition lift_sigma_map_id : 803 ∀A,B : Type[0].∀P_in,P_out : A → Prop.B → 804 (∀a.P_out a + ¬ P_out a) → 805 ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig. 806 match dec a_sig with 807 [ inl prf ⇒ m «a_sig, prf» 808  inr _ ⇒ dflt (* labels not present in out code get 0 *) 809 ]. 810 811 lemma lift_sigma_map_id_eq : 812 ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out. 813 pi1 ?? a_in = pi1 ?? a_out → 814 lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out. 815 #A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ 816 whd in match lift_sigma_map_id; normalize nodelta 817 cases (dec a_in) normalize nodelta >EQ cases a_out 818 #a #H #G [ %  @⊥ /2 by absurd/ ] 819 qed. 820 821 notation > "Σ_{ ident i ∈ l } f" 822 with precedence 20 823 for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}. 824 notation < "Σ_{ ident i ∈ l } f" 825 with precedence 20 826 for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}. 827 828 definition lift_cost_map_id : 829 ∀S_in,S_out : abstract_status.? → 830 as_cost_map S_out → as_cost_map S_in 831 ≝ 832 λS_in,S_out : abstract_status. 833 lift_sigma_map_id costlabel ℕ 834 (λl.∃pc.as_label_of_pc S_in pc = Some ? l) 835 (λl.∃pc.as_label_of_pc S_out pc = Some ? l) 836 0. 837 838 lemma lift_cost_map_same_cost : 839 ∀S_in, S_out, dec, m_out, trace_in, trace_out. 840 map … (pi1 ??) trace_in = map … (pi1 ??) trace_out → 841 (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) = 842 (Σ_{ l_sig ∈ trace_out } (m_out l_sig)). 843 #S_in #S_out #dec #m_out #trace_in elim trace_in 844 [2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out] 845 normalize in ⊢ (%→?); 846 [2,3: #ABS destruct(ABS) 847 4: #_ % 848 1: 849 #EQ destruct 850 whd in ⊢(??%%); 851 whd in match lift_cost_map_id; normalize nodelta 852 >(lift_sigma_map_id_eq ????????? e0) 853 >e0 in e1; normalize in ⊢(%→?); #EQ 854 >(IH … EQ) % 855 ] 856 qed. 880 (* cost maps specifics: summing over flattened traces *) 857 881 858 882 lemma lift_cost_map_same_cost_tal :
Note: See TracChangeset
for help on using the changeset viewer.