Changeset 2669
 Timestamp:
 Feb 15, 2013, 11:27:58 AM (8 years ago)
 Location:
 src/common
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FEMeasurable.ma
r2668 r2669 6 6 λC,g,s. match pcs_classify C g s with [ cl_other ⇒ true  cl_jump ⇒ true  _ ⇒ false ]. 7 7 8 lemma normal_state_inv : ∀C,g,s. 9 normal_state C g s → 10 pcs_classify C g s = cl_other ∨ pcs_classify C g s = cl_jump. 11 #C #g #s whd in ⊢ (?% → ?); cases (pcs_classify C g s) /2/ * 12 qed. 13 8 14 (* A record giving the languages and simulation results necessary to show that 9 measurability is preserved. *) 15 measurability is preserved. 16 17 Note: as we're interested in measurable subtraces, we don't have to worry 18 about the execution "going wrong." 19 *) 10 20 11 21 record meas_sim : Type[2] ≝ { … … 18 28 ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (normal_state ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C2 g2 s2); 19 29 ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (pcs_labelled ms_C2 g2 s2); 30 31 (* These hold in (at least) the languages of interest for measurable subtraces *) 32 ms_labelled_normal_1 : ∀g1,s1. bool_to_Prop (pcs_labelled ms_C1 g1 s1) ↔ bool_to_Prop (normal_state ms_C1 g1 s1); 33 ms_labelled_normal_2 : ∀g2,s2. bool_to_Prop (pcs_labelled ms_C2 g2 s2) ↔ bool_to_Prop (normal_state ms_C2 g2 s2); 34 ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall; 35 20 36 sim_normal : 21 37 ∀g1,g2. 22 38 ∀INV:ms_inv g1 g2. 23 ∀s1,s1' ,s2,tr.39 ∀s1,s1'. 24 40 ms_rel g1 g2 INV s1 s1' → 25 41 normal_state ms_C1 g1 s1 → 26 42 ¬ pcs_labelled ms_C1 g1 s1 → 27 ∃n . after_n_steps (S n) … (pcs_exec ms_C1) g1 s1 (λs.normal_state ms_C1 g1 s ∧ ¬ pcs_labelled ms_C1 g1 s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →43 ∃n,s2,tr. after_n_steps (S n) … (pcs_exec ms_C1) g1 s1 (λs.normal_state ms_C1 g1 s ∧ ¬ pcs_labelled ms_C1 g1 s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) ∧ 28 44 ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'. 29 45 tr = tr' ∧ … … 33 49 ∀g1,g2. 34 50 ∀INV:ms_inv g1 g2. 35 ∀s1,s1' ,s2,tr.51 ∀s1,s1'. 36 52 ms_rel g1 g2 INV s1 s1' → 37 53 match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true  cl_return ⇒ true  _ ⇒ false] → 38 54 ¬ pcs_labelled ms_C1 g1 s1 → 39 after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) →55 ∃s2,tr. after_n_steps 1 … (pcs_exec ms_C1) g1 s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) ∧ 40 56 ∃m. after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.normal_state ms_C2 g2 s) (λtr',s2'. 41 57 tr = tr' ∧ … … 131 147 ] qed. 132 148 133 lemma stack_ labelled_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.149 lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. 134 150 exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 → 135 pcs_labelledC g s1 →151 normal_state C g s1 → 136 152 stack_after (pcs_to_cs C g stack) current trace = current. 137 153 #C #g #s1 #trace #s2 #stack #current #EXEC 138 154 cases (exec_steps_S … EXEC) 139 155 #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct 140 #CS 141 whd in ⊢ (??%?); whd in match (cs_classify ??); >CS 156 #N 157 whd in ⊢ (??%?); generalize in match (cs_stack ??); 158 whd in match (cs_classify ??); 159 cases (normal_state_inv … N) 160 #CL >CL #f % 161 qed. 162 163 lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. 164 exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 → 165 normal_state C g s1 → 166 max_stack (pcs_to_cs C g stack) current trace = current. 167 #C #g #s1 #trace #s2 #stack #current #EXEC 168 cases (exec_steps_S … EXEC) 169 #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct 170 #N 171 whd in ⊢ (??%?); generalize in match (cs_stack ??); 172 whd in match (cs_classify ??); 173 cases (normal_state_inv … N) 174 #CL >CL #f % 175 qed. 176 177 lemma exec_split : ∀C:preclassified_system.∀g,m,s1,trace,sf. 178 exec_steps m io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 → 179 ¬pcs_labelled C g s1 → 180 pcs_labelled C g sf → 181 ∀inv. (∀s. bool_to_Prop (inv s) → ¬pcs_labelled C g s) → 182 ∀n,P. after_n_steps n io_out io_in (pcs_exec … C) g s1 inv P → 183 ∃p,trace1,s2,trace2. 184 exec_steps n io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧ 185 P (gather_trace … trace1) s2 ∧ 186 exec_steps p io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉 ∧ 187 m = n + p. 188 #C #g #m elim m m 189 [ #s1 #trace #sf #EXEC whd in EXEC:(??%?); destruct 190 #NCS #CS @⊥ @(absurd … CS) @Prop_notb @NCS 191  #m #IH #s1 #trace #sf #EXEC1 #NCS1 #CS2 #inv #H * 192 [ #P #AFTER %{(S m)} %{[ ]} %{s1} %{trace} % [ % [ % [ %  @AFTER ]  @EXEC1 ] % ] 193  #n #P #AFTER 194 cases (exec_steps_S … EXEC1) 195 #NF1 * #tr1 * #s2 * #tl * * #Etrace #STEP #EXEC2 196 cases (after_1_of_n_steps … AFTER) 197 #tr1' * #s2' * * * #NF1' #STEP' #INV2 #AFTER2 198 >STEP in STEP'; #E destruct 199 cases (IH … EXEC2 … AFTER2) 200 [ #p * #trace1 * #s2 * #trace2 * * * #EXEC2' #P2 #EXEC2 #E 201 %{p} % [2: %{s2} %{trace2} % [ % [ % 202 [ @(exec_steps_join 1 … EXEC2') [2: whd in ⊢ (??%?); >NF1 in ⊢ (??%?); >STEP in ⊢ (??%?); %  skip ] 203  @P2 ] @EXEC2 ] >E % ]  skip ] 204  @H assumption 205  assumption 206  assumption 207 ] 208 ] 209 ] qed. 210 211 lemma exec_split1 : ∀C:preclassified_system.∀g,m,s1,trace,sf. 212 exec_steps (S m) io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 → 213 ∀P,inv. after_n_steps 1 io_out io_in (pcs_exec … C) g s1 inv P → 214 ∃trace1,s2,trace2. 215 exec_steps 1 io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧ 216 P (gather_trace … trace1) s2 ∧ 217 exec_steps m io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉. 218 #C #g #m #s1 #trace #sf #EXEC1 #P #inv #AFTER1 219 cases (exec_steps_S … EXEC1) 220 #NF1 * #tr * #s2 * #tl * * #E1 destruct #STEP #EXEC2 221 %{[〈s1,tr〉]} %{s2} %{tl} % [ % 222 [ whd in ⊢ (??%?); >NF1 >STEP %  whd in AFTER1; >NF1 in AFTER1; >STEP normalize 223 cases (inv s2) // * ] // ] 224 qed. 225 226 (* XXX do I need to do the max_stack reasoning here? perhaps just by preserving 227 observables? *) 142 228 143 229 … … 153 239 ∀m,prefix,sf. 154 240 exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 → 241 pcs_labelled (ms_C1 MS) g sf → 155 242 le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) 0 prefix) max_allowed_stack → 156 243 … … 160 247 161 248 ms_rel MS g g' INV sf sf'. 162 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled # sim_normal #sim_call_return #sim_cost #sim_init249 * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #labelled_normal1 #labelled_normal2 #no_tailcalls #sim_normal #sim_call_return #sim_cost #sim_init 163 250 #g #g' #INV #max #s1 #s1' #REL 164 251 #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; s1 s1' … … 166 253 @(nat_elim1 m0) 167 254 * 168 [ #_ #current_stack #s1 #s1' #REL #prefix #sf # exec whd in exec:(??%?); destruct255 [ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf 169 256 #max_ok %{0} %{[]} %{s1'} 170 257 % [ % //  // ] 171  #m #IH #current_stack #s1 #s1' #REL #prefix #sf # exec #max_ok258  #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #MAX_OK 172 259 cases (true_or_false_Prop … (pcs_labelled … s1)) 173 260 [ #CS 174 cases (exec_steps_split 1 … exec) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1261 cases (exec_steps_split 1 … EXEC) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1 175 262 lapply (sim_cost … s2 ? REL CS ?) 176 263 [ @(exec_steps_after_n_noinv … EXEC1) %  skip ] … … 178 265 cases (after_n_exec_steps … AFTER') 179 266 #prefix' * #s2' * #EXEC1' * #Etrace #R2 180 cases (IH m ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 ?) 181 [ 2: //  3: @(transitive_le … max_ok) >E1 <max_stack_append 182 183 @le_maxr 267 cut (normal_state C1 g s1) [ @(proj1 … (labelled_normal1 …)) assumption ] #N1 268 cut (normal_state C2 g' s1') [ @(proj1 … (labelled_normal2 …)) @(proj1 … (rel_labelled … REL)) assumption ] #N1' 269 cases (IH m ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?) 270 [ 2: //  3: @(transitive_le … MAX_OK) >E1 <max_stack_append 271 >(stack_normal_step … EXEC1 N1) 272 >(stack_normal_step … EXEC1' N1') 273 @max_r // 274 ] 184 275 #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R'' 185 276 %{(1+m'')} %{(prefix'@prefix'')} %{sf''} 186 % [ % [ @(exec_steps_join … EXEC1') @EXEC''  cases daemon ]  @R2 187  188 %{trace1 } 189 190 cases (exec_steps_S … exec) #notfinal * #tr' * #s' * #tl * * #E #STEP #EXEC' 191 cases (true_or_false_Prop … (pcs_labelled … s1)) 192 [ #CS lapply (sim_cost … s' tr' REL CS ?) 193 [ @(exec_steps_after_n_noinv … whd >notfinal whd >STEP whd % ] 194 #AFTER %{1} 195 [ 3: whd in match (after_n_steps ????? s1 ??); 196 >(?:is_final ???? s1 = None ?) [ whd in ⊢ ((% → ?) → ?); 197 lapply (refl ? (pcs_classify … s1)) cases (pcs_classify … s1) in ⊢ (???% → ?); 198 [ 199  #CL 277 % [ % [ @(exec_steps_join … EXEC1') @EXEC'' 278  <max_stack_append @to_max 279 [ >(max_stack_normal_step … EXEC1' N1') 280 lapply MAX_OK >E1 <max_stack_append 281 >(max_stack_normal_step … EXEC1 N1) 282 #H /2 by le_maxl/ 283  @MAX'' ] ] 284  @R'' 285 ] 286 287  #NCS 288 cases (true_or_false_Prop (normal_state C1 g s1)) 289 [ #NORMAL 290 (* XXX should set things up so that notb_Prop isn't needed *) 291 cases (sim_normal … REL NORMAL (notb_Prop … NCS)) 292 #n * #s2x * #tr * #AFTER * #n' #AFTER' 293 cases (exec_split … EXEC (notb_Prop … NCS) CSf … AFTER) 294 [ 2: #s #H cases (andb_Prop_true … H) // ] 295 #p * #trace1 * #s2 * #trace2 * * * #EXEC1 #E2 #EXEC2 #Esplit destruct 296 cases (after_n_exec_steps … AFTER') #prefix' * #s2' * #EXEC1' * #Etrace #R2 297 cases (IH p ? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?) 298 [ 2: /2/  3: cases daemon ] (* XXX *) 299 #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R'' 300 %{(n'+m'')} %{(prefix'@prefix'')} %{sf''} 301 % [ % [ @(exec_steps_join … EXEC1') @EXEC'' 302  <max_stack_append @to_max 303 [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1') 304 lapply MAX_OK >E1 <max_stack_append 305 >(max_stack_normal_step … EXEC1 N1) 306 #H /2 by le_maxl/*) 307  @MAX'' ] ] 308  @R'' 309 ] 310  #CALLRET 311 cases (sim_call_return … REL … (notb_Prop … NCS)) 312 [ 2: whd in CALLRET:(?%); whd in match (normal_state ???) in CALLRET; 313 lapply (no_tailcalls … s1) 314 cases (pcs_classify … s1) in CALLRET ⊢ %; 315 normalize * #H #H' try % try cases (H I) 316 cases H' /2/ ] 317 #s2 * #tr2 * #AFTER1 * #m' #AFTER1' 318 cases (exec_split1 … EXEC … AFTER1) 319 #trace1 * #s2x * #trace2 * * #EXEC1 #E2 #EXEC2 destruct 320 cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * #EXEC1' * #Etrace #R2 321 cases (IH ?? (stack_after (pcs_to_cs C2 … (stack … INV)) current_stack prefix') … R2 … EXEC2 CSf ?) 322 [ 2: /2/  3: cases daemon ] (* XXX *) 323 #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R'' 324 %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''} 325 % [ % [ @(exec_steps_join … EXEC1') @EXEC'' 326  <max_stack_append @to_max 327 [ cases daemon (* XXX >(max_stack_normal_step … EXEC1' N1') 328 lapply MAX_OK >E1 <max_stack_append 329 >(max_stack_normal_step … EXEC1 N1) 330 #H /2 by le_maxl/*) 331  @MAX'' ] ] 332  @R'' 333 ] 334 ] 335 ] 336 qed. 337 338 200 339 201 340 theorem measured_subtrace_preserved : 
src/common/Measurable.ma
r2668 r2669 22 22 *) 23 23 24 definition trace_is_label_to_return : ∀C. execution_prefix (cs_state … C) → Prop ≝25 λC,x. ∃tr1,s1,x',tr2,s2 ,s3. x = 〈tr1,s1〉::(x'@[〈tr2,s2〉;〈E0,s3〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.24 definition trace_is_label_to_return : ∀C. list (cs_state … C × trace) → Prop ≝ 25 λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return. 26 26 27 27 definition measure_stack_aux ≝ 28 λC. (λx. λ trs:trace × (cs_state … C).28 λC. (λx. λstr:cs_state … C × trace. 29 29 let 〈current,max_stack〉 ≝ x in 30 let 〈 tr,s〉 ≝ trsin30 let 〈s,tr〉 ≝ str in 31 31 let new ≝ 32 32 match cs_classify C s return λcl. (match cl in status_class with [_⇒?] → ?) → ? with … … 37 37 〈new, max max_stack new〉). 38 38 39 definition measure_stack : ∀C. nat → execution_prefix (cs_state … C) → nat × nat ≝39 definition measure_stack : ∀C. nat → list (cs_state … C × trace) → nat × nat ≝ 40 40 λC,current. 41 41 foldl … (measure_stack_aux C) 〈current,0〉. 42 42 43 definition stack_after : ∀C. nat → execution_prefix (cs_state … C) → nat ≝43 definition stack_after : ∀C. nat → list (cs_state … C × trace) → nat ≝ 44 44 λC,current,x. \fst (measure_stack C current x). 45 45 46 definition max_stack : ∀C. nat → execution_prefix (cs_state … C) → nat ≝46 definition max_stack : ∀C. nat → list (cs_state … C × trace) → nat ≝ 47 47 λC,current,x. \snd (measure_stack C current x). 48 48 … … 57 57 58 58 lemma max_stack_step : ∀C,a,m,a',m',tr,s. 59 measure_stack_aux C 〈a,m〉 〈 tr,s〉 = 〈a',m'〉 →59 measure_stack_aux C 〈a,m〉 〈s,tr〉 = 〈a',m'〉 → 60 60 m' = max m a'. 61 61 #C #a #m #a' #m' #tr #s … … 65 65 qed. 66 66 67 lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2', trs.68 measure_stack_aux C 〈a,m1〉 trs= 〈a1',m1'〉 →69 measure_stack_aux C 〈a,m2〉 trs= 〈a2',m2'〉 →67 lemma max_stack_step' : ∀C,a,a1',a2',m1,m1',m2,m2',str. 68 measure_stack_aux C 〈a,m1〉 str = 〈a1',m1'〉 → 69 measure_stack_aux C 〈a,m2〉 str = 〈a2',m2'〉 → 70 70 a1' = a2'. 71 #C #a #a1' #a2' #m1 #m2 #m1' #m2' * # tr #s71 #C #a #a1' #a2' #m1 #m2 #m1' #m2' * #s #tr 72 72 whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???); 73 73 generalize in match (cs_stack C s); cases (cs_classify C s) #f … … 224 224 225 225 let rec will_return_aux C (depth:nat) 226 (trace: execution_prefix (cs_state … C)) on trace : bool ≝226 (trace:list (cs_state … C × trace)) on trace : bool ≝ 227 227 match trace with 228 228 [ nil ⇒ false 229 229  cons h tl ⇒ 230 let 〈 tr,s〉 ≝ h in230 let 〈s,tr〉 ≝ h in 231 231 match cs_classify C s with 232 232 [ cl_call ⇒ will_return_aux C (S depth) tl 233 233  cl_return ⇒ 234 234 match depth with 235 (* We need to see the state after the return to build the structured 236 trace. *) 237 [ O ⇒ match tl with [ cons _ tl' ⇒ match tl' with [ nil ⇒ true  _ ⇒ false ]  _ ⇒ false ] 235 (* The state after the return will appear in the structured trace, but 236 not here because it is the second part of the pair returned by 237 exec_steps. *) 238 [ O ⇒ match tl with [ nil ⇒ true  _ ⇒ false ] 238 239  S d ⇒ will_return_aux C d tl 239 240 ] … … 241 242 ] 242 243 ]. 243 definition will_return' : ∀C. execution_prefix (cs_state … C) → bool ≝ λC. will_return_aux C O.244 definition will_return' : ∀C. list (cs_state … C × trace) → bool ≝ λC. will_return_aux C O. 244 245 245 246 (* Like classified_system, but we don't fix the global environment so that we 
src/common/SmallstepExec.ma
r2668 r2669 383 383 (* For now I'm doing this without I/O, to keep things simple. In the place I 384 384 intend to use it (the definition of measurable subtraces, and proofs using 385 that) I should allow I/O for the prefix. *) 386 387 let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (trace × (state … fx g)) × (state … fx g)) ≝ 385 that) I should allow I/O for the prefix. 386 387 If the execution has the form 388 389 s1 tr1→ s2 tr2→ … sn trn→ s' 390 391 then the function returns 392 393 〈[〈s1,tr1〉; 〈s2,tr2〉; …; 〈sn,trn〉], s'〉 394 *) 395 396 let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (state … fx g × trace) × (state … fx g)) ≝ 388 397 match n with 389 398 [ O ⇒ return 〈[ ], s〉 … … 395 404 [ Value trs ⇒ 396 405 ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs); 397 return 〈 trs::tl, s'〉406 return 〈〈s, \fst trs〉::tl, s'〉 398 407  Interact _ _ ⇒ Error … (msg UnexpectedIO) 399 408  Wrong m ⇒ Error … m … … 408 417 is_final … fx g s = None ? ∧ 409 418 ∃tr',s',tl. 410 trace = 〈 tr',s'〉::tl ∧419 trace = 〈s,tr'〉::tl ∧ 411 420 step … fx g s = Value … 〈tr',s'〉 ∧ 412 421 exec_steps n O I fx g s' = OK … 〈tl,s''〉. … … 454 463 qed. 455 464 456 let rec gather_trace S (l:list ( trace × S)) on l : trace ≝465 let rec gather_trace S (l:list (S × trace)) on l : trace ≝ 457 466 match l with 458 467 [ nil ⇒ E0 459  cons h t ⇒ (\ fsth)⧺(gather_trace S t)468  cons h t ⇒ (\snd h)⧺(gather_trace S t) 460 469 ]. 461 470 … … 474 483 lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P. 475 484 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 476 all … (λts. inv (\snd ts)) trace → 485 all ? (λstr. inv (\fst str)) (tail … trace) → 486 inv s' → 477 487 P (gather_trace ? trace) s' → 478 488 after_n_steps n O I fx g s inv P. 479 489 #n elim n 480 490 [ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct 481 #ALL # p whd @p491 #ALL #FI #p whd @p 482 492  #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC 483 493 cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS 484 494 destruct 485 #ALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all … (λts. inv (\snd ts)) tl)) 486 [ whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/ ] * #i1 #itl 487 #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?)) 495 #ALL #FALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl))) 496 [ cases m in STEPS; 497 [ whd in ⊢ (??%? → ?); #E destruct /2/ 498  #m' #STEPS cases (exec_steps_S … STEPS) #_ * #tr'' * #s'' * #tl'' * * #E #_ #_ destruct 499 whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/ 500 ] 501 ] * #i1 #itl 502 #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ??)) 488 503 [ @p 504  @FALL 489 505  whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p' 490 506 ] … … 497 513 #n #O #I #fx #g #s #trace #s' #P #EXEC #p 498 514 @(exec_steps_after_n … EXEC) // 499 elim trace /2/ 515 cases trace // #x #trace' 516 elim trace' /2/ 500 517 qed. 501 518 … … 510 527 cases (IH … AFTER') 511 528 #tl * #s' * #STEPS #p 512 %{(〈 tr1,s1〉::tl)} %{s'} %529 %{(〈s,tr1〉::tl)} %{s'} % 513 530 [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS %  // ] 514 531 ] qed. … … 526 543 cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC' 527 544 cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2 528 %{(〈 tr',s'〉::trace1)} %{trace2} %{s1}545 %{(〈s,tr'〉::trace1)} %{trace2} %{s1} 529 546 % 530 547 [ % … … 549 566 ] qed. 550 567 551 (* Show that it corresponds to split_trace … (exec_inf …) *) 568 lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'. 569 exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 → 570 s = s1. 571 #n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC 572 lapply (exec_steps_length … EXEC) #E normalize in E; destruct 573 cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct 574 % 575 qed. 576 577 (* Show that it corresponds to split_trace … (exec_inf …). 578 We need to adjust the form of trace. *) 579 580 let rec switch_trace_aux S tr (l:list (S × trace)) (s':S) on l : list (trace × S) ≝ 581 match l with 582 [ nil ⇒ [〈tr,s'〉] 583  cons h t ⇒ 〈tr,\fst h〉::(switch_trace_aux S (\snd h) t s') 584 ]. 585 586 definition switch_trace ≝ 587 λS,l,s'. match l with 588 [ nil ⇒ nil ? 589  cons h t ⇒ switch_trace_aux S (\snd h) t s' 590 ]. 552 591 553 592 lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'. 554 593 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 555 594 match is_final … s' with 556 [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈 trace, exec_inf_aux … fx g (step … s')〉557  Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈 trace, e_stop … tr' r s'〉595 [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', exec_inf_aux … fx g (step … s')〉 596  Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', e_stop … tr' r s'〉 558 597 ]. 559 598 #O #I #fx #g #n elim n … … 570 609 >exec_inf_aux_unfold normalize nodelta 571 610 cases (is_final … s') 572 [ %611 [ whd % 573 612  #r %2 %{tr''} % 574 613 ] 575  * # tr1 #s1 #tl1 #E normalize in E; destruct #Esteps614  * #s1 #tr1 #tl1 #E normalize in E; destruct #Esteps 576 615 lapply (IH … Esteps) cases (is_final … s') 577 [ normalize nodelta #IH' >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 578 >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' % 616 [ normalize nodelta #IH' >Estep <(exec_steps_first … Esteps) 617 >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 618 >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' normalize nodelta % 579 619  normalize nodelta #r * 580 620 [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct 581  * #tr'' #IH' %2 %{tr''} >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 621  * #tr'' #IH' %2 %{tr''} >Estep <(exec_steps_first … Esteps) 622 >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 582 623 >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' % 583 624 ]
Note: See TracChangeset
for help on using the changeset viewer.