Changeset 3081 for src/common


Ignore:
Timestamp:
Apr 3, 2013, 5:54:34 PM (7 years ago)
Author:
campbell
Message:

Tidy up recent work a little.

Location:
src/common
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r3063 r3081  
    170170qed.
    171171
    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. *)
    173177
    174178lemma prefix_preserved :
     
    429433  @IH @Ntl
    430434] 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. *)
    431442
    432443lemma measurable_subtrace_preserved :
     
    777788] qed.
    778789
    779 (* TODO: move*)
    780 lemma plus_split : ∀x,y:nat. ∃z. x = y + z ∨ y = x + z.
    781 #x0 elim x0
    782 [ #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 l1
    796 [ //
    797 | #h #t #IH #l2
    798   whd in ⊢ (?% → ?(?%?));
    799   cases (p h) //
    800   @IH
    801 ] qed.
    802 
    803790
    804791lemma ends_at_return_normal : ∀C,g,t1,t2.
     
    825812
    826813
     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. *)
    827819
    828820theorem measured_subtrace_preserved :
  • src/common/SmallstepExec.ma

    r2685 r3081  
    235235qed.
    236236
     237lemma 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
     266lemma 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
     272cases (after_aux_result … A) #tr * #s' * #p #A'
     273%{tr} %{s'} %{p} @A'
     274qed.
     275
     276lemma 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
     284cases (after_1_of_n_steps … A)
     285#tr1 * #s1 * * * #F #ST #_ #A'
     286cases (after_n_result … A')
     287#tr'' * #s'' * #E #A'' destruct
     288% [2: % [2: % [2: % [ % [% [ @F | @ST ] | % ] | @A'' ] | skip ] | skip ] | skip ]
     289qed.
     290
    237291(* A typical way to use the following:
    238292
Note: See TracChangeset for help on using the changeset viewer.