Changeset 3081 for src/common
 Timestamp:
 Apr 3, 2013, 5:54:34 PM (7 years ago)
 Location:
 src/common
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FEMeasurable.ma
r3063 r3081 170 170 qed. 171 171 172 172 (* First show that the trace up to the start of the measurable subtrace (i.e., 173 the prefix of the execution) is preserved using the simulation results in 174 the meas_sim record. Note that this doesn't end cleanly  the first states 175 in the measurable subtrace may not be in the simulation relation, see the 176 comment below. *) 173 177 174 178 lemma prefix_preserved : … … 429 433 @IH @Ntl 430 434 ] qed. 435 436 (* Now show the preservation of parts of the measurable subtrace from states in 437 simulation to the end. (We'll deal with any extra steps at the start from 438 the prefix lemma in the theorem below.) The basic idea here is that having 439 broken up the simulation results into normal, call, return and cost lemmas, 440 we can match up the structure of the two executions, and in particular 441 prove the will_return_aux predicate for the target execution. *) 431 442 432 443 lemma measurable_subtrace_preserved : … … 777 788 ] qed. 778 789 779 (* TODO: move*)780 lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z.781 #x0 elim x0782 [ #y %{y} %2 %783  #x #IH *784 [ %{(S x)} %1 %785  #y cases (IH y) #z *786 [ #H %{z} %1 >H //787  #H %{z} %2 >H //788 ]789 ]790 ] qed.791 792 lemma all_append : ∀A,p,l1,l2.793 all A p (l1@l2) →794 all A p l1 ∧ all A p l2.795 #A #p #l1 elim l1796 [ //797  #h #t #IH #l2798 whd in ⊢ (?% → ?(?%?));799 cases (p h) //800 @IH801 ] qed.802 803 790 804 791 lemma ends_at_return_normal : ∀C,g,t1,t2. … … 825 812 826 813 814 (* Now put the two main lemmas above together to show that the target has a 815 [measurable] subtrace, and that the observables are the same. 816 817 To deal with the extra steps from the prefix lemma, note that they are 818 "normal" steps, and so cannot interfere with the structure. *) 827 819 828 820 theorem measured_subtrace_preserved : 
src/common/SmallstepExec.ma
r2685 r3081 235 235 qed. 236 236 237 lemma after_aux_result : ∀avs,n,s,tr,P. 238 after_aux avs n s tr P → 239 ∃tr',s'. P tr' s' ∧ after_aux avs n s tr (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉). 240 #avs #n elim n 241 [ #s #tr #P #A whd in A; %{tr} %{s} % [ @A  % ] 242  #n' #IH #s #tr #P 243 whd in ⊢ (% → ?); 244 lapply (refl ? (is_final … s)) 245 cases (is_final … s) in ⊢ (???% → %); 246 [ #F whd in ⊢ (% → ?); 247 lapply (refl ? (step … s)) 248 cases (step … s) in ⊢ (???% → %); 249 [ #o #k #_ * 250  * #tr1 #s1 #ST whd in ⊢ (% → ?); 251 cases n' in IH ⊢ %; 252 [ #_ whd in ⊢ (% → ?); #p % [2: % [2: %{p} whd >F whd >ST whd %  skip ]  skip ] 253  #n'' #IH lapply (refl ? (avs_inv avs s1)) cases (avs_inv avs s1) in ⊢ (???% → %); 254 [ #INV #AF 255 cases (IH … AF) #tr' * #s' * #p #AF' 256 % [2: % [2: %{p} whd >F whd >ST whd >INV @AF'  skip ]  skip ] 257  #_ * 258 ] 259 ] 260  #m #_ * 261 ] 262  #r #F * 263 ] 264 ] qed. 265 266 lemma after_n_result : ∀n,O,I,exec,g,s,P,inv. 267 after_n_steps n O I exec g s inv P → 268 ∃tr',s'. 269 P tr' s' ∧ 270 after_n_steps n O I exec g s inv (λtr'',s''. 〈tr'',s''〉 = 〈tr',s'〉). 271 #n #O #I #exec #g #s #P #inv #A 272 cases (after_aux_result … A) #tr * #s' * #p #A' 273 %{tr} %{s'} %{p} @A' 274 qed. 275 276 lemma after_1_of_n_steps' : ∀n,O,I,exec,g,tr,s',s. 277 after_n_steps (S n) O I exec g s (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr,s'〉) → 278 ∃tr1,tr2,s1. 279 is_final … exec g s = None ? ∧ 280 step … exec g s = Value … 〈tr1,s1〉 ∧ 281 tr = tr1⧺tr2 ∧ 282 after_n_steps n O I exec g s1 (λ_.true) (λtrx,sx. 〈trx,sx〉 = 〈tr2,s'〉). 283 #n #O #I #exec #g #tr #s' #s #A 284 cases (after_1_of_n_steps … A) 285 #tr1 * #s1 * * * #F #ST #_ #A' 286 cases (after_n_result … A') 287 #tr'' * #s'' * #E #A'' destruct 288 % [2: % [2: % [2: % [ % [% [ @F  @ST ]  % ]  @A'' ]  skip ]  skip ]  skip ] 289 qed. 290 237 291 (* A typical way to use the following: 238 292
Note: See TracChangeset
for help on using the changeset viewer.