Changeset 2444
 Timestamp:
 Nov 8, 2012, 6:47:04 PM (7 years ago)
 Location:
 src/common
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/IOMonad.ma
r2428 r2444 426 426 on _E:eq (IO ???) ?? to eq (res ?) ??. 427 427 428 (* and for an unreduced form *) 429 coercion io_monad_eq_from_res : 430 ∀O,I,T,e,v. ∀E:err_to_io O I T e = Value O I T v. e = OK T v ≝ io_eq_to_res 431 on _E:eq (monad (max_def (IOMonad ??)) ?) ?? to eq (res ?) ??. 432 428 433 (* Similarly for opt *) 429 434 … … 441 446 on _E:eq (IO ???) ?? to eq (option ?) ??. 442 447 443 444 448 coercion io_monad_eq_from_opt : 449 ∀O,I,T,e,m,v. ∀E:opt_to_io O I T m e = Value O I T v. e = Some T v ≝ io_eq_to_opt 450 on _E:eq (monad (max_def (IOMonad ??)) ?) ?? to eq (option ?) ??. 451 452 453 
src/common/SmallstepExec.ma
r2338 r2444 77 77 and at the end reduce with whd to get the property as the goal. 78 78 79 There's an inversionlike result to get back the information contained in 80 the proof in Executions.ma. 79 There are a few inversionlike results to get back the information contained in 80 the proof below, and other that provides all the steps in an inductive form 81 in Executions.ma. 81 82 82 83 *) … … 118 119 λn,O,I,exec,g,s,P. after_aux (mk_await_value_stuff O I exec g) n s E0 P. 119 120 121 lemma after_aux_covariant : ∀avs,P,Q,tr'. 122 (∀tr,s. P (tr'⧺tr) s → Q tr s) → 123 ∀n,s,tr. 124 after_aux avs n s (tr'⧺tr) P → 125 after_aux avs n s tr Q. 126 #avs #P #Q #tr' #H #n elim n 127 [ normalize /2/ 128  #n' #IH #s #tr 129 whd in ⊢ (% → %); cases (is_final … s) [ 2: #x * ] 130 whd in ⊢ (% → %); 131 cases (step … s) [1,3: normalize /2/ ] 132 * #tr'' #s'' 133 whd in ⊢ (% → %); >Eapp_assoc @IH 134 ] qed. 135 120 136 lemma after_n_covariant : ∀n,O,I,exec,g,P,Q. 121 137 (∀tr,s. P tr s → Q tr s) → … … 123 139 after_n_steps n O I exec g s P → 124 140 after_n_steps n O I exec g s Q. 125 #n #O #I #exec #g #P #Q #H whd in ⊢ (? → % → %); generalize in match E0; elim n 126 [ normalize /2/ 127  #n' #IH #tr #s 128 normalize cases (is_final … s) normalize [ 2: #_ * ] cases (step O I exec g s) normalize /4/ 129 ] qed. 141 normalize /3/ 142 qed. 130 143 131 144 (* for joining a couple of these together *) … … 152 165 ] qed. 153 166 167 (* Inversion lemmas. *) 168 169 lemma after_1_of_n_steps : ∀n,O,I,exec,g,P,s. 170 after_n_steps (S n) O I exec g s P → 171 ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ 172 after_n_steps n O I exec g s' (λtr'',s''. P (tr⧺tr'') s''). 173 #n #O #I #exec #g #P #s 174 whd in ⊢ (% → ?); 175 cases (is_final … s) 176 [ whd in ⊢ (% → ?); 177 cases (step … s) 178 [ #o #k * 179  * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER 180 %{tr} %{s'} % // whd @(after_aux_covariant … AFTER) 181 #tr' #s'' // 182  #m * 183 ] 184  #r * 185 ] qed. 186 187 lemma after_1_step : ∀O,I,exec,g,P,s. 188 after_n_steps 1 O I exec g s P → 189 ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ P tr s'. 190 #O #I #exec #g #P #s #AFTER 191 cases (after_1_of_n_steps … AFTER) 192 #tr * #s' * #STEP #FIN %{tr} %{s'} % // whd in FIN; >E0_right in FIN; // 193 qed. 194 195 (* A typical way to use the following: 196 197 With a hypothesis 198 EX : after_n_steps n ... (State ...) ... 199 reduce it [whd in EX;] to 200 EX : await_value ... 201 then perform inversion 202 [cases (await_value_bind_inv … EX) EX * #x * #E1 #EX] 203 x : T 204 E1 : f = return x 205 EX : await_value ... 206 *) 207 208 lemma await_value_bind_inv : ∀avs,T,f,g,P. 209 await_value avs (f »= g) P → 210 ∃x:T. (f = return x) ∧ await_value avs (g x) P. 211 #avs #T * 212 [ #o #k #g #P * 213  #x #g #P #AWAIT %{x} % // 214  #m #g #P * 215 ] qed. 154 216 155 217 (* A (possibly nonterminating) execution. *)
Note: See TracChangeset
for help on using the changeset viewer.