Changeset 2670 for src/common
 Timestamp:
 Feb 15, 2013, 11:27:59 AM (7 years ago)
 Location:
 src/common
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FEMeasurable.ma
r2669 r2670 78 78 79 79 (* TODO: obs eq *) 80 81 definition trace_starts : ∀S. execution S io_out io_in → S → Prop ≝82 λS,t,s. match t with [ e_step _ s' _ ⇒ s = s'  _ ⇒ False ].83 84 (* TODO: too many of these lemmas, slim it down*)85 86 lemma split_trace_S : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.87 split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S n) = Some ? 〈a,b〉 →88 ∃a'. a = 〈tr,s〉::a' ∧89 ((is_final … fx g s = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s)) n = Some ? 〈a',b〉) ∨90 (∃r. is_final … fx g s = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s)).91 #fx #g #tr #s #n #a #b92 >exec_inf_aux_unfold whd in ⊢ (??(????%?)? → ?);93 cases (is_final … s)94 [ whd in ⊢ (??%? → ?); cases (split_trace ?????)95 [ #E whd in E:(??%%); destruct96  * #a' #b' #E whd in E:(??%%); destruct97 %{a'} %{(refl ??)} %1 %{(refl ??)} %98 ]99  #r cases n [2:#n'] whd in ⊢ (??%? → ?); #E destruct100 %{[ ]} %{(refl ??)} %2 %{r} /4/101 ] qed.102 103 lemma split_trace_S' : ∀fx:trans_system io_out io_in. ∀g,s,n,a,b.104 split_trace … (exec_inf_aux ?? fx g (step … fx g s)) (S n) = Some ? 〈a,b〉 →105 ∃tr,s'. step … fx g s = Value … 〈tr,s'〉 ∧106 ∃a'. a = 〈tr,s'〉::a' ∧107 ((is_final … fx g s' = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s')) n = Some ? 〈a',b〉) ∨108 (∃r. is_final … fx g s' = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s')).109 #fx #g #s #n #a #b110 cases (step … fx g s)111 [ #o #i whd in ⊢ (??%? → ?); #E destruct112  * #tr #s' #split %{tr} %{s'} %{(refl …)} @split_trace_S @split113  #err #E whd in E:(??%%); destruct114 ] qed.115 116 lemma split_trace_1 : ∀fx:trans_system io_out io_in. ∀g,tr,s,a,b.117 split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) 1 = Some ? 〈a,b〉 →118 a = [〈tr,s〉] ∧119 ((is_final … fx g s = None ? ∧ b = exec_inf_aux ?? fx g (step … fx g s)) ∨120 (∃r. is_final … fx g s = Some ? r ∧ b = e_stop … tr r s)).121 #fx #g #tr #s #a #b #split122 cases (split_trace_S … split)123 #a' * #E1 *124 [ * #notfinal #split' whd in split':(??%?); destruct %{(refl ??)}125 %1 %{notfinal} %126  * #r * * * #final #_ #E2 #E3 destruct %{(refl ??)}127 %2 %{r} %{final} %128 ] qed.129 130 131 lemma split_trace_SS : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.132 split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S (S n)) = Some ? 〈a,b〉 →133 ∃a'. a = 〈tr,s〉::a' ∧134 is_final … fx g s = None ? ∧135 ∃tr',s'. step … fx g s = Value … 〈tr',s'〉 ∧136 split_trace … (exec_inf_aux ?? fx g (Value … 〈tr',s'〉)) (S n) = Some ? 〈a',b〉.137 #fx #g #tr #s #n #a #b #splitSS138 cases (split_trace_S … splitSS)139 #a' * #E1 *140 [ * #notfinal #splitS %{a'} % [ %{E1} @notfinal ]141 cases (step … s) in splitS ⊢ %;142 [ #o #i #E whd in E:(??%%); destruct143  * #tr' #s' #splitS %{tr'} %{s'} %{(refl ??)} @splitS144  #m #E whd in E:(??%%); destruct145 ]146  * #r * * * #final #En #Ea #Eb destruct147 ] qed.148 80 149 81 lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. … … 344 276 measurable (ms_C1 MS) p1 m n stack_cost max → 345 277 ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max. 346 * #C1 #C2 #compiled #inv #rel #sim_normal #sim_call_return #sim_cost #sim_init 347 #p1 #p2 #m #n #stack_cost #max #compiled 348 whd in ⊢ (% → ?); letin C1' ≝ (mk_classified_system C1 ????) letin g1 ≝ (make_global ?? C1 ?) 349 * #prefix * #suffix * #subtrace * #remainder 350 * * * * #split1 #split2 #subtrace_ok #terminates #max_ok 351 352 *) 278 
src/common/Measurable.ma
r2669 r2670 77 77 qed. 78 78 79 (* TODO: move*)80 lemma max_O_n : ∀n. max O n = n.81 * //82 qed.83 84 lemma max_n_O : ∀n. max n O = n.85 * //86 qed.87 88 lemma associative_max : associative nat max.89 #n #m #o normalize90 @(leb_elim n m)91 [ normalize @(leb_elim m o) normalize #H1 #H292 [ >(le_to_leb_true n o) /2/93  >(le_to_leb_true n m) //94 ]95  normalize @(leb_elim m o) normalize #H1 #H296 [ %97  >(not_le_to_leb_false … H2)98 >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/99 ]100 ] qed.101 102 79 103 80 lemma max_stack_steps : ∀C,trace,a,m. … … 116 93 ] qed. 117 94 118 (*119 lemma max_stack_step : ∀C,a,m,tr,s.120 m ≤ \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉).121 #C #a #m #tr #s122 whd in match (measure_stack_aux ???);123 generalize in match (cs_stack C s); cases (cs_classify C s) normalize124 #f @(leb_elim m) normalize #H /2/125 qed.126 127 lemma max_stack_steps : ∀C. ∀am. ∀trace.128 \snd am ≤ \snd (foldl … (measure_stack_aux C) am trace).129 #C * #a #m #trace130 @foldl_inv131 [ * #a' #m' * #tr #s #H @(transitive_le … H) @max_stack_step132  //133 ] qed.134 135 lemma max_stack_step' : ∀C,a,m,a',m',tr,s.136 a ≤ a' → m ≤ m' →137 \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \snd (measure_stack_aux C 〈a',m'〉 〈tr,s〉).138 #C #a #m #a' #m' #tr #s #H1 #H2139 whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???);140 generalize in match (cs_stack C s); cases (cs_classify C s) #f141 whd in ⊢ (?(??%)(??%));142 [ @to_max [ @(transitive_le … m') /2/  @(transitive_le … (a'f I)) /2/ ]143  2,4,5: @to_max /2 by max_r, max_l/144  @to_max [ @(transitive_le … m') /2/  @(transitive_le … (a'+f I)) /2/ ]145 ] qed.146 147 lemma max_stack_step'' : ∀C,a,m,a',m',tr,s.148 a ≤ a' →149 \fst (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \fst (measure_stack_aux C 〈a',m'〉 〈tr,s〉).150 #C #a #m #a' #m' #tr #s #H1151 whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???);152 generalize in match (cs_stack C s); cases (cs_classify C s) #f153 whd in ⊢ (?%%); /2/154 qed.155 156 lemma max_stack_steps' : ∀C. ∀trace,am,am'.157 \fst am ≤ \fst am' → \snd am ≤ \snd am' →158 \snd (foldl … (measure_stack_aux C) am trace) ≤ \snd (foldl … (measure_stack_aux C) am' trace).159 #C #trace elim trace160 [ * #a #m * #a' #m' #H1 #H2 @H2161  * #tr #s #tl #IH * #a #m * #a' #m' #H1 #H2 @IH [ @max_stack_step'' //  @max_stack_step' // ]162 ] qed.163 164 lemma max_stack_append_l : ∀C,ex1,ex2.165 max_stack C ex1 ≤ max_stack C (ex1@ex2).166 #C #ex1 #ex2 whd in ⊢ (??%);167 whd in match (measure_stack ? (ex1@ex2));168 >foldl_append169 @max_stack_steps170 qed.171 172 lemma max_stack_append_r : ∀C,ex1,ex2.173 max_stack C ex2 ≤ max_stack C (ex1@ex2).174 #C #ex1 #ex2 whd in ⊢ (??%);175 whd in match (measure_stack ? (ex1@ex2));176 >foldl_append177 @max_stack_steps' //178 qed.179 *)(*180 lemma max_stack_append : ∀C,ex1,ex2.181 max (max_stack C ex1) (max_stack C ex2) = max_stack C (ex1@ex2).182 #C #ex1 #ex2183 whd in match (max_stack ??); whd in match (max_stack ? (ex1@ex2));184 whd in match (measure_stack ??); whd in match (measure_stack ? (ex1@ex2));185 generalize in match 〈O,O〉; elim ex1186 [ * #a #m whd in ⊢ (??(?%?)%); >max_stack_steps187 188 elim ex1189 [ #ex2 >max_O_n %190  * #tr #s #tl #IH #ex2191 whd in match (max_stack ??); whd in match (measure_stack ??);192 lapply (refl ? (measure_stack_aux C 〈O,O〉 〈tr,s〉))193 cases (measure_stack_aux ???) in ⊢ (???% → %);194 #a #m #M195 196 #ex2197 @le_to_le_to_eq198 [ @to_max //199 200 whd in ⊢ (???%);201 202 whd in match (measure_stack ? (ex1@ex2));203 >foldl_append204 @max_stack_steps' //205 *)206 95 lemma max_stack_append : ∀C,c1,ex1,ex2. 207 96 max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2).
Note: See TracChangeset
for help on using the changeset viewer.