Changeset 2668 for src/common


Ignore:
Timestamp:
Feb 15, 2013, 11:27:56 AM (7 years ago)
Author:
campbell
Message:

Intermediate measurable proof check-in before I change its traces again.

Location:
src/common
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/common/ErrorMessages.ma

    r2646 r2668  
    6464 | FinalState : ErrorMessage
    6565 | EmptyStack: ErrorMessage
    66  | OutOfBounds: ErrorMessage.
     66 | OutOfBounds: ErrorMessage
     67 | UnexpectedIO : ErrorMessage
     68 | TerminatedEarly : ErrorMessage.
  • src/common/FEMeasurable.ma

    r2644 r2668  
    1616  ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat);
    1717  ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop;
     18  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  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);
    1820  sim_normal :
    1921    ∀g1,g2.
     
    129131] qed.
    130132
    131 (* WIP commented out
     133lemma stack_labelled_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
     134  exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 →
     135  pcs_labelled C g s1 →
     136  stack_after (pcs_to_cs C g stack) current trace = current.
     137#C #g #s1 #trace #s2 #stack #current #EXEC
     138cases (exec_steps_S … EXEC)
     139#NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct
     140#CS
     141whd in ⊢ (??%?); whd in match (cs_classify ??); >CS
     142
     143
     144(* WIP commented out*)
    132145lemma prefix_preserved :
    133146  ∀MS:meas_sim.
    134   ∀g1,g2.
    135   ∀INV:ms_inv MS g1 g2.
     147  ∀g,g'.
     148  ∀INV:ms_inv MS g g'.
    136149  ∀max_allowed_stack.
    137   ∀s1,s1',tr,tr'.
    138   ms_rel MS g1 g2 INV s1 s1' →
     150  ∀s1,s1'.
     151  ms_rel MS g g' INV s1 s1' →
     152
     153  ∀m,prefix,sf.
     154  exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 →
     155  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) 0 prefix) max_allowed_stack →
     156
     157  ∃m',prefix',sf'.
     158    exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧
     159    le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) 0 prefix') max_allowed_stack ∧
    139160 
    140   let trace ≝ (exec_inf_aux ?? (pcs_exec … (ms_C1 MS)) g1 (Value … 〈tr,s1〉)) in
    141   let trace' ≝ (exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr',s1'〉)) in
    142  
    143   ∀m,prefix,suffix.
    144   split_trace … trace m = Some ? 〈prefix,suffix〉 →
    145   le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) prefix) max_allowed_stack →
    146 
    147   ∃m',prefix',suffix'.
    148     split_trace … trace' m' = Some ? 〈prefix',suffix'〉 ∧
    149     le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧
    150  
    151   ∃s2,s2',tr2,tr2'.
    152     suffix = exec_inf_aux ?? (pcs_exec …  (ms_C1 MS)) g1 (Value … 〈tr2,s2〉) ∧
    153     suffix' = exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr2',s2'〉) ∧
    154     ms_rel MS g1 g2 INV s2 s2'.
    155 * #C1 #C2 #compiled #inv #stack #rel #sim_normal #sim_call_return #sim_cost #sim_init
    156 #g1 #g2 #INV #max #s1 #s1' #tr #tr' #REL
    157 letin trace ≝ (exec_inf_aux ?????)
    158 letin trace' ≝ (exec_inf_aux ?????)
    159 #m0
     161    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_init
     163#g #g' #INV #max #s1 #s1' #REL
     164#m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1'
     165generalize in match 0; (* current stack level *)
    160166@(nat_elim1 m0)
    161167*
    162 [ #_ #prefix #suffix #split whd in split:(??%?); destruct
    163   #max_ok %{0} %{[]} %{trace'}
    164   % [ % // | %{s1} %{s1'} %{tr} %{tr'} /3/ ]
    165 | *
    166   [ (* m = 1; just extracts the current state *)
    167     #_ #prefix #suffix #split #max_ok
    168     cases (split_trace_1 … split) #E1 #foo
    169     %{1} %{[〈tr',s1'〉]} %{(exec_inf_aux … (step … s1'))}
    170     % [ %
    171  #m #IH #prefix #suffix #split #max_ok
    172   (* clean up first step? *)
     168[ #_ #current_stack #s1 #s1' #REL #prefix #sf #exec whd in exec:(??%?); destruct
     169  #max_ok %{0} %{[]} %{s1'}
     170  % [ % // | // ]
     171| #m #IH #current_stack #s1 #s1' #REL #prefix #sf #exec #max_ok
    173172  cases (true_or_false_Prop … (pcs_labelled … s1))
    174   [ #CS cases (split_trace_S … split) #trace1 * #Etrace *
    175     [ * #notfinal #split1
    176     lapply (sim_cost … REL CS)
     173  [ #CS
     174    cases (exec_steps_split 1 … exec) #trace1 * #trace2 * #s2 * * #EXEC1 #EXEC2 #E1
     175    lapply (sim_cost … s2 ? REL CS ?)
     176    [ @(exec_steps_after_n_noinv … EXEC1) % | skip ]
     177    #AFTER'
     178    cases (after_n_exec_steps … AFTER')
     179    #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
     184    #m'' * #prefix'' * #sf'' * * #EXEC'' #MAX'' #R''
     185    %{(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}
    177195    [ 3: whd in match (after_n_steps ????? s1 ??);
    178196      >(?:is_final ???? s1 = None ?) [ whd in ⊢ ((% → ?) → ?);
  • src/common/Measurable.ma

    r2618 r2668  
    2525λ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.
    2626
    27 definition measure_stack : ∀C. execution_prefix (cs_state … C) → nat × nat ≝
    28 λC.
    29   foldl … (λx, trs.
     27definition measure_stack_aux ≝
     28λC. (λx. λtrs:trace × (cs_state … C).
    3029    let 〈current,max_stack〉 ≝ x in
    3130    let 〈tr,s〉 ≝ trs in
     
    3635      | _ ⇒ λ_. current
    3736      ] (cs_stack C s) in
    38     〈new, max max_stack new〉) 〈0,0〉.
    39 
    40 definition stack_after : ∀C. execution_prefix (cs_state … C) → nat ≝
    41 λC,x. \fst (measure_stack C x).
    42 
    43 definition max_stack : ∀C. execution_prefix (cs_state … C) → nat ≝
    44 λC,x. \snd (measure_stack C x).
     37    〈new, max max_stack new〉).
     38
     39definition measure_stack : ∀C. nat → execution_prefix (cs_state … C) → nat × nat ≝
     40λC,current.
     41  foldl … (measure_stack_aux C) 〈current,0〉.
     42
     43definition stack_after : ∀C. nat → execution_prefix (cs_state … C) → nat ≝
     44λC,current,x. \fst (measure_stack C current x).
     45
     46definition max_stack : ∀C. nat → execution_prefix (cs_state … C) → nat ≝
     47λC,current,x. \snd (measure_stack C current x).
     48
     49lemma foldl_inv : ∀A,B. ∀P:A → Prop. ∀f.
     50  (∀acc,el. P acc → P (f acc el)) →
     51  ∀l,acc. P acc →
     52  P (foldl A B f acc l).
     53#A #B #P #f #IH #l elim l
     54[ //
     55| #h #t #IH' #acc #H @IH' @IH @H
     56] qed.
     57
     58lemma max_stack_step : ∀C,a,m,a',m',tr,s.
     59  measure_stack_aux C 〈a,m〉 〈tr,s〉 = 〈a',m'〉 →
     60  m' = max m a'.
     61#C #a #m #a' #m' #tr #s
     62whd in match (measure_stack_aux ???);
     63generalize in match (cs_stack C s); cases (cs_classify C s) #f
     64normalize nodelta #E destruct //
     65qed.
     66
     67lemma 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'〉 →
     70  a1' = a2'.
     71#C #a #a1' #a2' #m1 #m2 #m1' #m2' * #tr #s
     72whd in match (measure_stack_aux ???); whd in match (measure_stack_aux ???);
     73generalize in match (cs_stack C s); cases (cs_classify C s) #f
     74normalize nodelta
     75#E1 #E2 destruct
     76%
     77qed.
     78
     79(* TODO: move*)
     80lemma max_O_n : ∀n. max O n = n.
     81* //
     82qed.
     83
     84lemma max_n_O : ∀n. max n O = n.
     85* //
     86qed.
     87
     88lemma associative_max : associative nat max.
     89#n #m #o normalize
     90@(leb_elim n m)
     91[ normalize @(leb_elim m o) normalize #H1 #H2
     92  [ >(le_to_leb_true n o) /2/
     93  | >(le_to_leb_true n m) //
     94  ]
     95| normalize @(leb_elim m o) normalize #H1 #H2
     96  [ %
     97  | >(not_le_to_leb_false … H2)
     98    >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/
     99  ]
     100] qed.
     101
     102
     103lemma max_stack_steps : ∀C,trace,a,m.
     104  \snd (foldl … (measure_stack_aux C) 〈a,m〉 trace) =
     105  max m (\snd (foldl … (measure_stack_aux C) 〈a,0〉 trace)).
     106#C #trace elim trace
     107[ #a #m >max_n_O %
     108| * #tr #s #tl #IH #a #m
     109  whd in match (foldl ?????);
     110  letin x ≝ (measure_stack_aux ???) lapply (refl ? x) cases x in ⊢ (???% → %); #a' #m' #M
     111  whd in match (foldl ??? 〈a,O〉 ?);
     112  letin y ≝ (measure_stack_aux ? 〈a,O〉 ?) lapply (refl ? y) cases y in ⊢ (???% → %); #a'' #m'' #M'
     113  >(IH a'') >IH
     114  >(max_stack_step … M)
     115  >(max_stack_step … M') >max_O_n >(max_stack_step' … M M') >associative_max %
     116] qed.
     117
     118(*
     119lemma max_stack_step : ∀C,a,m,tr,s.
     120  m ≤ \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉).
     121#C #a #m #tr #s
     122whd in match (measure_stack_aux ???);
     123generalize in match (cs_stack C s); cases (cs_classify C s) normalize
     124#f @(leb_elim m) normalize #H /2/
     125qed.
     126
     127lemma max_stack_steps : ∀C. ∀am. ∀trace.
     128  \snd am ≤ \snd (foldl … (measure_stack_aux C) am trace).
     129#C * #a #m #trace
     130@foldl_inv
     131[ * #a' #m' * #tr #s #H @(transitive_le … H) @max_stack_step
     132| //
     133] qed.
     134
     135lemma max_stack_step' : ∀C,a,m,a',m',tr,s.
     136  a ≤ a' → m ≤ m' →
     137  \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \snd (measure_stack_aux C 〈a',m'〉 〈tr,s〉).
     138#C #a #m #a' #m' #tr #s #H1 #H2
     139whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???);
     140generalize in match (cs_stack C s); cases (cs_classify C s) #f
     141whd in ⊢ (?(??%)(??%));
     142[ @to_max [ @(transitive_le … m') /2/ | @(transitive_le … (a'-f I)) /2/ ]
     143| 2,4,5: @to_max /2 by max_r, max_l/
     144| @to_max [ @(transitive_le … m') /2/ | @(transitive_le … (a'+f I)) /2/ ]
     145] qed.
     146
     147lemma max_stack_step'' : ∀C,a,m,a',m',tr,s.
     148  a ≤ a' →
     149  \fst (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \fst (measure_stack_aux C 〈a',m'〉 〈tr,s〉).
     150#C #a #m #a' #m' #tr #s #H1
     151whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???);
     152generalize in match (cs_stack C s); cases (cs_classify C s) #f
     153whd in ⊢ (?%%); /2/
     154qed.
     155
     156lemma max_stack_steps' : ∀C. ∀trace,am,am'.
     157  \fst am ≤ \fst am' → \snd am ≤ \snd am' →
     158  \snd (foldl … (measure_stack_aux C) am trace) ≤ \snd (foldl … (measure_stack_aux C) am' trace).
     159#C #trace elim trace
     160[ * #a #m * #a' #m' #H1 #H2 @H2
     161| * #tr #s #tl #IH * #a #m * #a' #m' #H1 #H2 @IH [ @max_stack_step'' // | @max_stack_step' // ]
     162] qed.
     163
     164lemma max_stack_append_l : ∀C,ex1,ex2.
     165  max_stack C ex1 ≤ max_stack C (ex1@ex2).
     166#C #ex1 #ex2 whd in ⊢ (??%);
     167whd in match (measure_stack ? (ex1@ex2));
     168>foldl_append
     169@max_stack_steps
     170qed.
     171
     172lemma max_stack_append_r : ∀C,ex1,ex2.
     173  max_stack C ex2 ≤ max_stack C (ex1@ex2).
     174#C #ex1 #ex2 whd in ⊢ (??%);
     175whd in match (measure_stack ? (ex1@ex2));
     176>foldl_append
     177@max_stack_steps' //
     178qed.
     179*)(*
     180lemma max_stack_append : ∀C,ex1,ex2.
     181  max (max_stack C ex1) (max_stack C ex2) = max_stack C (ex1@ex2).
     182#C #ex1 #ex2
     183whd in match (max_stack ??); whd in match (max_stack ? (ex1@ex2));
     184whd in match (measure_stack ??); whd in match (measure_stack ? (ex1@ex2));
     185generalize in match 〈O,O〉; elim ex1
     186[ * #a #m whd in ⊢ (??(?%?)%); >max_stack_steps
     187
     188elim ex1
     189[ #ex2 >max_O_n %
     190| * #tr #s #tl #IH #ex2
     191  whd in match (max_stack ??); whd in match (measure_stack ??);
     192  lapply (refl ? (measure_stack_aux C 〈O,O〉 〈tr,s〉))
     193  cases (measure_stack_aux ???) in ⊢ (???% → %);
     194  #a #m #M
     195 
     196 #ex2
     197@le_to_le_to_eq
     198[ @to_max //
     199|
     200 whd in ⊢ (???%);
     201
     202whd in match (measure_stack ? (ex1@ex2));
     203>foldl_append
     204@max_stack_steps' //
     205*)
     206lemma max_stack_append : ∀C,c1,ex1,ex2.
     207  max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2).
     208#C #c1 #ex1 #ex2
     209whd in match (max_stack ???); whd in match (stack_after ???);
     210whd in match (max_stack ?? (ex1@ex2));
     211whd in match (measure_stack ???); whd in match (measure_stack ?? (ex1@ex2));
     212generalize in match O; generalize in match c1; elim ex1
     213[ #c #m whd in ⊢ (??(?%?)%); >max_stack_steps %
     214| * #tr #s #tl #IH #c #m
     215  whd in match (foldl ?????); whd in ⊢ (???(???%));
     216  lapply (refl ? (measure_stack_aux C 〈c1,m〉 〈tr,s〉))
     217  cases (measure_stack_aux ???) in ⊢ (???% → %); #a' #m' #M
     218  >IH %
     219] qed.
     220 
    45221
    46222(* Check that the trace ends with the return from the starting function and one
     
    90266  (ident → nat) (* stack cost *) →
    91267  nat → Prop ≝
    92 λC,p,m,n,stack_cost,max_allowed_stack.  ∃prefix,suffix,interesting,remainder.
    93   let C' ≝ pcs_to_cs C (make_global … p) stack_cost in
    94   let cl_trace ≝ exec_inf … (cs_exec … C') p in
    95   split_trace … cl_trace m = Some ? 〈prefix,suffix〉 ∧
    96   split_trace … suffix n = Some ? 〈interesting,remainder〉 ∧
     268λC,p,m,n,stack_cost,max_allowed_stack.  ∃s0,prefix,s1,interesting,s2.
     269  let g ≝ make_global … (pcs_exec … C) p in
     270  let C' ≝ pcs_to_cs C g stack_cost in
     271  make_initial_state … p = OK ? s0 ∧
     272  exec_steps m ?? (cs_exec … C') g s0 = OK ? 〈prefix,s1〉 ∧
     273  exec_steps n ?? (cs_exec … C') g s1 = OK ? 〈interesting,s2〉 ∧
    97274  trace_is_label_to_return C' interesting ∧
    98275  bool_to_Prop (will_return' C' interesting) ∧
    99   le (max_stack C' (prefix@interesting)) max_allowed_stack.
    100 
    101 (* TODO: probably ought to be elsewhere
     276  le (max_stack C' 0 (prefix@interesting)) max_allowed_stack.
     277
     278(* TODO: probably ought to be elsewhere; use exec_steps instead
    102279
    103280   Note that this does not include stack space
  • src/common/SmallstepExec.ma

    r2618 r2668  
    183183lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s.
    184184  after_n_steps (S n) O I exec g s inv P →
    185   ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧
     185  ∃tr,s'.
     186  is_final … exec g s = None ? ∧
     187  step … exec g s = Value … 〈tr,s'〉 ∧
    186188  bool_to_Prop (inv s') ∧
    187189  after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s'').
     
    193195  [ #o #k *
    194196  | * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER
    195     %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /2/ cases AFTER
     197    %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /3/ cases AFTER
    196198  | #m *
    197199  ]
     
    201203lemma after_1_step : ∀O,I,exec,g,inv,P,s.
    202204  after_n_steps 1 O I exec g s inv P →
    203   ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ bool_to_Prop (inv s') ∧ P tr s'.
     205  ∃tr,s'. is_final … exec g s = None ? ∧
     206    step ?? exec g s = Value … 〈tr,s'〉 ∧
     207    bool_to_Prop (inv s') ∧ P tr s'.
    204208#O #I #exec #g #inv #P #s #AFTER
    205209cases (after_1_of_n_steps … AFTER)
    206 #tr * #s' * * #STEP #INV #FIN %{tr} %{s'} % [%] // whd in FIN; >E0_right in FIN; //
     210#tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [%[%]] // whd in FIN; >E0_right in FIN; //
    207211qed.
    208212
     
    377381].
    378382
    379 
     383(* For now I'm doing this without I/O, to keep things simple.  In the place I
     384   intend to use it (the definition of measurable subtraces, and proofs using
     385   that) I should allow I/O for the prefix. *)
     386
     387let 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)) ≝
     388match n with
     389[ O ⇒ return 〈[ ], s〉
     390| S m ⇒
     391  match is_final … fx g s with
     392  [ Some r ⇒ Error … (msg TerminatedEarly)
     393  | None ⇒
     394    match step … fx g s with
     395    [ Value trs ⇒
     396        ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs);
     397        return 〈trs::tl, s'〉
     398    | Interact _ _ ⇒ Error … (msg UnexpectedIO)
     399    | Wrong m ⇒ Error … m
     400    ]
     401  ]
     402].
     403
     404(* Show that it's nice. *)
     405
     406lemma exec_steps_S : ∀O,I,fx,g,n,s,trace,s''.
     407  exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 →
     408  is_final … fx g s = None ? ∧
     409  ∃tr',s',tl.
     410    trace = 〈tr',s'〉::tl ∧
     411    step … fx g s = Value … 〈tr',s'〉 ∧
     412    exec_steps n O I fx g s' = OK … 〈tl,s''〉.
     413#O #I #fx #g #n #s #trace #s''
     414whd in ⊢ (??%? → ?);
     415cases (is_final … s)
     416[ whd in ⊢ (??%? → ?);
     417  cases (step … s)
     418  [ #o #i #EX whd in EX:(??%?); destruct
     419  | * #tr' #s' whd in ⊢ (??%? → ?); #EX %{(refl ??)}
     420    %{tr'} %{s'} cases (exec_steps … g s') in EX ⊢ %;
     421    [ * #tl #s'' #EX whd in EX:(??%?); destruct %{tl} /3/
     422    | #m #EX whd in EX:(??%?); destruct
     423    ]
     424  | #m #EX whd in EX:(??%?); destruct
     425  ]
     426| #r #EX whd in EX:(??%?); destruct
     427] qed.
     428
     429lemma exec_steps_length : ∀O,I,fx,g,n,s,trace,s'.
     430  exec_steps n O I fx g s = OK … 〈trace,s'〉 →
     431  n = |trace|.
     432#O #I #fx #g #n elim n
     433[ #s #trace #s' #EX whd in EX:(??%?); destruct %
     434| #m #IH #s #trace #s' #EX
     435  cases (exec_steps_S … EX) #notfinal * #tr' * #s'' * #tl * * #Etl #Estep #steps
     436  >(IH … steps) >Etl %
     437] qed.
     438
     439lemma exec_steps_nonterm : ∀O,I,fx,g,n,s,h,t,s'.
     440  exec_steps n O I fx g s = OK … 〈h::t,s'〉 →
     441  is_final … s = None ?.
     442#O #I #fx #g #n #s #h #t #s' #EX
     443lapply (exec_steps_length … EX)
     444#Elen destruct whd in EX:(??%?);
     445cases (is_final … s) in EX ⊢ %;
     446[ //
     447| #r #EX whd in EX:(??%?); destruct
     448] qed.
     449
     450lemma exec_steps_nonterm' : ∀O,I,fx,g,n,s,h,t,s'.
     451  exec_steps n O I fx g s = OK … 〈h@[t], s'〉 →
     452  is_final … s = None ?.
     453#O #I #fx #g #n #s * [2: #h1 #h2] #t #s' @exec_steps_nonterm
     454qed.
     455
     456let rec gather_trace S (l:list (trace × S)) on l : trace ≝
     457match l with
     458[ nil ⇒ E0
     459| cons h t ⇒ (\fst h)⧺(gather_trace S t)
     460].
     461
     462lemma exec_steps_after_n_simple : ∀n,O,I,fx,g,s,trace,s'.
     463  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
     464  after_n_steps n O I fx g s (λ_. true) (λtr,s''. 〈tr,s''〉 = 〈gather_trace ? trace,s'〉).
     465#n elim n
     466[ #O #I #fx #g #s #trace #s' #EXEC whd in EXEC:(??%?); destruct
     467  whd %
     468| #m #IH #O #I #fx #g #s #trace #s' #EXEC
     469  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
     470  @(after_n_m 1 … (IH … STEPS))
     471  whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct %
     472] qed.
     473
     474lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P.
     475  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
     476  all … (λts. inv (\snd ts)) trace →
     477  P (gather_trace ? trace) s' →
     478  after_n_steps n O I fx g s inv P.
     479#n elim n
     480[ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct
     481  #ALL #p whd @p
     482| #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC
     483  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
     484  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 ?))
     488  [ @p
     489  | whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p'
     490  ]
     491] qed.
     492
     493lemma exec_steps_after_n_noinv : ∀n,O,I,fx,g,s,trace,s',P.
     494  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
     495  P (gather_trace ? trace) s' →
     496  after_n_steps n O I fx g s (λ_.true) P.
     497#n #O #I #fx #g #s #trace #s' #P #EXEC #p
     498@(exec_steps_after_n … EXEC) //
     499elim trace /2/
     500qed.
     501
     502lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P.
     503  after_n_steps n O I fx g s inv P →
     504  ∃trace,s'. exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ P (gather_trace ? trace) s'.
     505#n elim n
     506[ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} %{(refl ??)} @AFTER
     507| #m #IH #O #I #fx #g #s #inv #P #AFTER
     508  cases (after_1_of_n_steps … AFTER)
     509  #tr1 * #s1 * * * #NF #STEP #INV #AFTER'
     510  cases (IH … AFTER')
     511  #tl * #s' * #STEPS #p
     512  %{(〈tr1,s1〉::tl)} %{s'} %
     513  [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % | // ]
     514] qed.
     515
     516lemma exec_steps_split : ∀n,m,O,I,fx,g,s,trace,s'.
     517  exec_steps (n+m) O I fx g s = OK ? 〈trace,s'〉 →
     518  ∃trace1,trace2,s1.
     519    exec_steps n O I fx g s = OK ? 〈trace1,s1〉 ∧
     520    exec_steps m O I fx g s1 = OK ? 〈trace2,s'〉 ∧   
     521    trace = trace1 @ trace2.
     522#n elim n
     523[ #m #O #I #fx #g #s #trace #s' #EXEC
     524  %{[ ]} %{trace} %{s} /3/
     525| #n' #IH #m #O #I #fx #g #s #trace #s' #EXEC
     526  cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC'
     527  cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2
     528  %{(〈tr',s'〉::trace1)} %{trace2} %{s1}
     529  %
     530  [ %
     531    [ whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >EXEC1 %
     532    | @EXEC2
     533    ]
     534  | destruct %
     535  ]
     536] qed.
     537
     538lemma exec_steps_join : ∀n,m,O,I,fx,g,s1,trace1,s2,trace2,s3.
     539  exec_steps n O I fx g s1 = OK ? 〈trace1,s2〉 →
     540  exec_steps m O I fx g s2 = OK ? 〈trace2,s3〉 →
     541  exec_steps (n+m) O I fx g s1 = OK ? 〈trace1@trace2,s3〉.
     542#n elim n
     543[ #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
     544  whd in EXEC1:(??%?); destruct @EXEC2
     545| #n' #IH #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
     546  cases (exec_steps_S … EXEC1) #NF * #tr' * #s' * #tl' * * #E1 #STEP #EXEC'
     547  whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >(IH … EXEC' EXEC2)
     548  destruct %
     549] qed.
     550
     551(* Show that it corresponds to split_trace … (exec_inf …) *)
     552
     553lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'.
     554  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
     555  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'〉
     558  ].
     559#O #I #fx #g #n elim n
     560[ #s #trace #s' #EX whd in EX:(??%%); destruct
     561  cases (is_final … s') [ % | #r %1 % ]
     562| #m #IH #s #trace #s' #EX
     563  cases (exec_steps_S … EX)
     564  #notfinal * #tr'' * #s'' * #tl * * #Etrace #Estep #Esteps
     565  cases tl in Etrace Esteps ⊢ %;
     566  [ #E destruct #Esteps
     567    lapply (exec_steps_length … Esteps) #Elen normalize in Elen; destruct
     568    whd in Esteps:(??%?); destruct
     569    >Estep
     570    >exec_inf_aux_unfold normalize nodelta
     571    cases (is_final … s')
     572    [ %
     573    | #r %2 %{tr''} %
     574    ]
     575  | * #tr1 #s1 #tl1 #E normalize in E; destruct #Esteps
     576    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' %
     579    | normalize nodelta #r *
     580      [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct
     581      | * #tr'' #IH' %2 %{tr''} >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
     582        >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' %
     583      ]
     584    ]
     585  ]
     586] qed.
Note: See TracChangeset for help on using the changeset viewer.