Changeset 1706


Ignore:
Timestamp:
Feb 16, 2012, 6:05:56 PM (6 years ago)
Author:
campbell
Message:

Checkpoint RTLabs structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1705 r1706  
    985985
    986986inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝
    987 | stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l (S n)
    988987| stlb_step : ∀l,n,H.
    989988    let stmt ≝ lookup_present … g l H in
    990     (∀l'. Exists label (λl0. l0 = l') (successors stmt) → steps_to_label_bound g l' n) →
     989    (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
     990          (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨
     991          steps_to_label_bound g l' n) →
    991992    steps_to_label_bound g l (steps_for_statement stmt + n).
     993
     994lemma steps_to_label_bound_inv : ∀g,l,n.
     995  steps_to_label_bound g l n →
     996  ∀H. let stmt ≝ lookup_present … g l H in
     997  ∃n'. n = steps_for_statement stmt + n' ∧
     998  (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
     999        (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨
     1000        steps_to_label_bound g l' n').
     1001#g #l0 #n0 #S inversion S #l #n #H #IH #E1 #E2 #_ destruct #H'
     1002% [2: % [ @refl | #l' #EX cases (IH l' EX) /2/ ] | skip ]
     1003qed.
    9921004   
    9931005discriminator nat.
    994 
    995 lemma steps_to_label_bound_inv_step : ∀g,l,n.
    996   steps_to_label_bound g l n →
    997   ∀H.
    998   let stmt ≝ lookup_present … g l H in
    999   ¬ (bool_to_Prop (is_cost_label stmt)) →
    1000   (∀l'. Exists label (λl0. l0 = l') (successors stmt) →
    1001     ∃n'. n = n' + steps_for_statement stmt ∧
    1002           steps_to_label_bound g l' n').
    1003 #g #l0 #n0 #H1 inversion H1
    1004 [ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4)
    1005 | #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC #l' #EX
    1006   % [2: % [ @commutative_plus | @IH // ] ]
    1007 ] qed.
    10081006
    10091007definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n.
     
    10371035[ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct
    10381036  inversion H52
    1039   [ #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
    1040   | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 normalize in H74; destruct
    1041   ]
     1037  #H68 #H69 #H70 #H71 #H72 #H73 #H74 normalize in H73; destruct
    10421038| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
    10431039| #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
     
    10751071  state_steps_to_label_bound s (S n) →
    10761072  eval_statement ge s = Value ??? 〈tr, s'〉 →
    1077   RTLabs_cost s = false →
     1073  RTLabs_cost s' = false →
    10781074  (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨
    10791075   state_steps_to_label_bound s' n.
     
    10831079  [ /3/
    10841080  | * #l * #S1 #S2 #NC %2
    1085     cases (steps_to_label_bound_inv_step … FS … l S2)
    1086     [ 2: change with (RTLabs_cost (State f fs m)) in ⊢ (?(?%)); >NC % // ]
     1081    cases (steps_to_label_bound_inv … FS ?) [2: @(next_ok f) ]
    10871082    #n'
    10881083    inversion (eval_perserves … EVAL)
    10891084    [ #ge0 #f0 #f' #fs' #m0 #m' #F #E1 #E2 #E3 #_ destruct
    1090       >(eval_steps … EVAL) * >commutative_plus #En normalize in En;
    1091       whd in S1:(??%?);
     1085      >(eval_steps … EVAL) * #En normalize in En;
    10921086      #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
    1093       %1 @H
     1087      whd in S1:(??%?); destruct
     1088      %1 cases (H l S2)
     1089      [ * #LP
     1090        change with (RTLabs_cost (State (mk_frame H1 H7 l H9 H5 H6) fs' m')) in ⊢ (?% → ?);
     1091        >NC *
     1092      | //
     1093      ]
    10941094    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
    1095       >(eval_steps … EVAL) * >commutative_plus #En normalize in En;
    1096       whd in S1:(??%?);
     1095      >(eval_steps … EVAL) * #En normalize in En;
    10971096      #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
    1098       %2 //
     1097      %2 whd lapply (H l S2)
     1098      @FS //
    10991099    | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29
    11001100      destruct
Note: See TracChangeset for help on using the changeset viewer.