Ignore:
Timestamp:
Feb 21, 2013, 11:38:36 AM (7 years ago)
Author:
campbell
Message:

Progress on measurable trace preservation: prefix preserves observable
intensional events (costs and calls).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r2682 r2685  
    540540qed.
    541541
     542lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'.
     543  exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 →
     544  s = s1.
     545#n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC
     546lapply (exec_steps_length … EXEC) #E normalize in E; destruct
     547cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct
     548%
     549qed.
     550
    542551lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P.
    543552  after_n_steps n O I fx g s inv P →
    544   ∃trace,s'. exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ P (gather_trace ? trace) s'.
     553  ∃trace,s'.
     554    exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧
     555    bool_to_Prop (all ? (λstr. inv (\fst str)) (tail … trace)) ∧
     556    P (gather_trace ? trace) s'.
    545557#n elim n
    546 [ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} %{(refl ??)} @AFTER
     558[ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} % [ %{(refl ??)} % | @AFTER ]
    547559| #m #IH #O #I #fx #g #s #inv #P #AFTER
    548560  cases (after_1_of_n_steps … AFTER)
    549561  #tr1 * #s1 * * * #NF #STEP #INV #AFTER'
    550562  cases (IH … AFTER')
    551   #tl * #s' * #STEPS #p
     563  #tl * #s' * * #STEPS #INV' #p
    552564  %{(〈s,tr1〉::tl)} %{s'} %
    553   [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % | // ]
     565  [ %
     566    [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS %
     567    | cases tl in STEPS INV INV' ⊢ %; [ // | * #sx #trx #t #STEPS #INV #INV'
     568      <(exec_steps_first … STEPS) whd in ⊢ (?%); >INV //
     569      >(exec_steps_length … STEPS) %
     570      ]
     571    ]
     572  | // ]
    554573] qed.
    555574
     
    588607  destruct %
    589608] qed.
    590 
    591 lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'.
    592   exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 →
    593   s = s1.
    594 #n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC
    595 lapply (exec_steps_length … EXEC) #E normalize in E; destruct
    596 cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct
    597 %
    598 qed.
    599609
    600610(* Show that it corresponds to split_trace … (exec_inf …).
Note: See TracChangeset for help on using the changeset viewer.