[700] | 1 | include "utilities/extralib.ma". |
---|
| 2 | include "common/IOMonad.ma". |
---|
| 3 | include "common/Integers.ma". |
---|
| 4 | include "common/Events.ma". |
---|
[24] | 5 | |
---|
[1233] | 6 | record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝ |
---|
| 7 | { global : Type[1] |
---|
[1231] | 8 | ; state : global → Type[0] |
---|
| 9 | ; is_final : ∀g. state g → option int |
---|
| 10 | ; step : ∀g. state g → IO outty inty (trace×(state g)) |
---|
[24] | 11 | }. |
---|
| 12 | |
---|
[1231] | 13 | let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:trans_system outty inty) |
---|
| 14 | (g:global ?? exec) (s:state ?? exec g) |
---|
| 15 | : IO outty inty (trace × (state ?? exec g)) ≝ |
---|
[24] | 16 | match n with |
---|
[25] | 17 | [ O ⇒ Value ??? 〈E0, s〉 |
---|
[731] | 18 | | S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s; |
---|
[2338] | 19 | ! 〈tn,sn〉 ← repeat n' ?? exec g s1; |
---|
| 20 | Value ??? 〈t1⧺tn,sn〉 |
---|
[24] | 21 | ]. |
---|
| 22 | |
---|
[2203] | 23 | (* We take care here to check that we're not at the final state. It is not |
---|
| 24 | necessarily the case that a success step guarantees this (e.g., because |
---|
| 25 | there may be no way to stop a processor, so an infinite loop is used |
---|
| 26 | instead). *) |
---|
| 27 | inductive plus (O) (I) (TS:trans_system O I) (ge:global … TS) : state … TS ge → trace → state … TS ge → Prop ≝ |
---|
| 28 | | plus_one : ∀s1,tr,s2. |
---|
| 29 | is_final … TS ge s1 = None ? → |
---|
| 30 | step … TS ge s1 = OK … 〈tr,s2〉 → |
---|
| 31 | plus … ge s1 tr s2 |
---|
| 32 | | plus_succ : ∀s1,tr,s2,tr',s3. |
---|
| 33 | is_final … TS ge s1 = None ? → |
---|
| 34 | step … TS ge s1 = OK … 〈tr,s2〉 → |
---|
| 35 | plus … ge s2 tr' s3 → |
---|
| 36 | plus … ge s1 (tr⧺tr') s3. |
---|
| 37 | |
---|
| 38 | lemma plus_not_final : ∀O,I,FE. ∀gl,s,tr,s'. |
---|
| 39 | plus O I FE gl s tr s' → |
---|
| 40 | is_final … FE gl s = None ?. |
---|
| 41 | #O #I #FE #gl #s0 #tr0 #s0' * // |
---|
| 42 | qed. |
---|
| 43 | |
---|
[751] | 44 | let rec trace_map (A,B:Type[0]) (f:A → res (trace × B)) |
---|
| 45 | (l:list A) on l : res (trace × (list B)) ≝ |
---|
| 46 | match l with |
---|
| 47 | [ nil ⇒ OK ? 〈E0, [ ]〉 |
---|
| 48 | | cons h t ⇒ |
---|
| 49 | do 〈tr,h'〉 ← f h; |
---|
| 50 | do 〈tr',t'〉 ← trace_map … f t; |
---|
| 51 | OK ? 〈tr ⧺ tr',h'::t'〉 |
---|
| 52 | ]. |
---|
| 53 | |
---|
[2338] | 54 | (* A third version of making several steps (!) |
---|
| 55 | |
---|
| 56 | The idea here is to have a computational definition of reducing serveral |
---|
| 57 | steps then showing some property about the resulting trace and state. By |
---|
| 58 | careful use of let rec we can ensure that reduction stops in a sensible |
---|
| 59 | way whenever the number of steps or the step currently being executed is |
---|
| 60 | not (reducible to) a value. |
---|
[2487] | 61 | |
---|
[2682] | 62 | An invariant is also asserted on every intermediate state (i.e., everything |
---|
| 63 | other than the first and last states). |
---|
[2338] | 64 | |
---|
| 65 | For example, we state a property to prove by something like |
---|
| 66 | |
---|
[2487] | 67 | ∃n. after_n_steps n … clight_exec ge s inv (λtr,s'. <some property>) |
---|
[2338] | 68 | |
---|
| 69 | then start reducing by giving the number of steps and reducing the |
---|
| 70 | definition |
---|
| 71 | |
---|
| 72 | %{3} whd |
---|
| 73 | |
---|
| 74 | and then whenever the reduction gets stuck, the currently reducing step is |
---|
| 75 | the third subterm, which we can reduce and unblock with (for example) |
---|
| 76 | rewriting |
---|
| 77 | |
---|
| 78 | whd in ⊢ (??%?); >EXe' |
---|
| 79 | |
---|
| 80 | and at the end reduce with whd to get the property as the goal. |
---|
| 81 | |
---|
[2444] | 82 | There are a few inversion-like results to get back the information contained in |
---|
| 83 | the proof below, and other that provides all the steps in an inductive form |
---|
| 84 | in Executions.ma. |
---|
[2338] | 85 | |
---|
| 86 | *) |
---|
| 87 | |
---|
| 88 | record await_value_stuff : Type[2] ≝ { |
---|
| 89 | avs_O : Type[0]; |
---|
| 90 | avs_I : avs_O → Type[0]; |
---|
| 91 | avs_exec : trans_system avs_O avs_I; |
---|
[2487] | 92 | avs_g : global ?? avs_exec; |
---|
| 93 | avs_inv : state ?? avs_exec avs_g → bool |
---|
[2338] | 94 | }. |
---|
| 95 | |
---|
| 96 | let rec await_value (avs:await_value_stuff) |
---|
| 97 | (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs)))) |
---|
| 98 | (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝ |
---|
| 99 | match v with |
---|
| 100 | [ Value ts ⇒ P (\fst ts) (\snd ts) |
---|
| 101 | | _ ⇒ False |
---|
| 102 | ]. |
---|
| 103 | |
---|
[2487] | 104 | let rec assert (b:bool) (P:Prop) on b ≝ |
---|
| 105 | if b then P else False. |
---|
| 106 | |
---|
[2682] | 107 | let rec assert_nz (n:nat) (b:bool) (P:Prop) on n ≝ |
---|
| 108 | match n with |
---|
| 109 | [ O ⇒ P |
---|
| 110 | | _ ⇒ assert b P |
---|
| 111 | ]. |
---|
| 112 | |
---|
[2338] | 113 | let rec after_aux (avs:await_value_stuff) |
---|
| 114 | (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace) |
---|
| 115 | (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) |
---|
| 116 | on n : Prop ≝ |
---|
| 117 | match n with |
---|
| 118 | [ O ⇒ P tr s |
---|
| 119 | | S n' ⇒ |
---|
| 120 | match is_final … s with |
---|
| 121 | [ None ⇒ |
---|
| 122 | await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s. |
---|
[2682] | 123 | assert_nz n' (avs_inv avs s) (after_aux avs n' s (tr ⧺ tr') P)) |
---|
[2338] | 124 | | _ ⇒ False |
---|
| 125 | ] |
---|
| 126 | ]. |
---|
| 127 | |
---|
[2682] | 128 | lemma assert_nz_lift : ∀n,b,P,Q. |
---|
| 129 | (P → Q) → |
---|
| 130 | assert_nz n b P → |
---|
| 131 | assert_nz n b Q. |
---|
| 132 | * [ /2/ | #n * [ normalize /2/ | #P #Q #_ * ] ] |
---|
| 133 | qed. |
---|
| 134 | |
---|
[2338] | 135 | definition after_n_steps : nat → |
---|
| 136 | ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec. |
---|
| 137 | state ?? exec g → |
---|
[2487] | 138 | (state ?? exec g → bool) → |
---|
[2338] | 139 | (trace → state ?? exec g → Prop) → Prop ≝ |
---|
[2487] | 140 | λn,O,I,exec,g,s,inv,P. after_aux (mk_await_value_stuff O I exec g inv) n s E0 P. |
---|
[2338] | 141 | |
---|
[2444] | 142 | lemma after_aux_covariant : ∀avs,P,Q,tr'. |
---|
| 143 | (∀tr,s. P (tr'⧺tr) s → Q tr s) → |
---|
| 144 | ∀n,s,tr. |
---|
| 145 | after_aux avs n s (tr'⧺tr) P → |
---|
| 146 | after_aux avs n s tr Q. |
---|
| 147 | #avs #P #Q #tr' #H #n elim n |
---|
| 148 | [ normalize /2/ |
---|
| 149 | | #n' #IH #s #tr |
---|
| 150 | whd in ⊢ (% → %); cases (is_final … s) [ 2: #x * ] |
---|
| 151 | whd in ⊢ (% → %); |
---|
| 152 | cases (step … s) [1,3: normalize /2/ ] |
---|
| 153 | * #tr'' #s'' |
---|
[2487] | 154 | whd in ⊢ (% → %); |
---|
[2682] | 155 | @assert_nz_lift |
---|
[2487] | 156 | >Eapp_assoc @IH |
---|
[2444] | 157 | ] qed. |
---|
| 158 | |
---|
[2487] | 159 | lemma after_n_covariant : ∀n,O,I,exec,g,P,inv,Q. |
---|
[2338] | 160 | (∀tr,s. P tr s → Q tr s) → |
---|
| 161 | ∀s. |
---|
[2487] | 162 | after_n_steps n O I exec g s inv P → |
---|
| 163 | after_n_steps n O I exec g s inv Q. |
---|
[2444] | 164 | normalize /3/ |
---|
| 165 | qed. |
---|
[2338] | 166 | |
---|
| 167 | (* for joining a couple of these together *) |
---|
| 168 | |
---|
[2487] | 169 | lemma after_n_m : ∀n,m,O,I,exec,g,inv,P,Q,s,s'. |
---|
| 170 | after_n_steps m O I exec g s' inv Q → |
---|
[2682] | 171 | (notb (eqb m 0) → inv s') → |
---|
[2487] | 172 | after_n_steps n O I exec g s inv (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) → |
---|
| 173 | after_n_steps (n+m) O I exec g s inv P. |
---|
[2682] | 174 | #n #m #O #I #exec #g #inv #P #Q whd in ⊢ (? → ? → ? → ? → % → %); generalize in match E0; elim n |
---|
| 175 | [ #tr #s #s' #H #INVs' whd in ⊢ (% → %); * #E destruct #H2 |
---|
[2338] | 176 | whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %; |
---|
| 177 | generalize in match s; -s |
---|
| 178 | elim m |
---|
| 179 | [ #s #tr' whd in ⊢ (% → %); @H2 |
---|
| 180 | | #m' #IH #s #tr' whd in ⊢ (% → %); |
---|
| 181 | cases (is_final … s) [2: #r * ] |
---|
| 182 | whd in ⊢ (% → %); |
---|
[2487] | 183 | cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %); |
---|
[2682] | 184 | @assert_nz_lift |
---|
[2487] | 185 | >Eapp_assoc @IH ] |
---|
[2682] | 186 | | #n' #IH #tr #s #s' #H #INVs' whd in ⊢ (% → %); |
---|
[2338] | 187 | cases (is_final … s) [2: #r * ] |
---|
| 188 | whd in ⊢ (% → %); |
---|
| 189 | cases (step O I exec g s) [1,3: normalize // ] |
---|
[2487] | 190 | * #tr1 #s1 whd in ⊢ (% → %); |
---|
[2682] | 191 | cases n' in IH H ⊢ %; [ cases m in INVs' ⊢ %; |
---|
| 192 | [ #Is' #IH #H @IH [ // | * #H cases (H (refl ??)) ] |
---|
| 193 | | #m' #Is' #IH #H * #E destruct >Is' [ #X @(IH … H) [ @Is' | % // @X ] | % #E destruct ] ] ] |
---|
| 194 | #n'' #IH #H |
---|
[2487] | 195 | cases (inv s1) [2:*] |
---|
[2682] | 196 | @IH assumption |
---|
[2338] | 197 | ] qed. |
---|
| 198 | |
---|
[2444] | 199 | (* Inversion lemmas. *) |
---|
[2338] | 200 | |
---|
[2682] | 201 | lemma assert_nz_inv : ∀n,b,P. |
---|
| 202 | assert_nz n b P → |
---|
| 203 | (n = 0 ∨ bool_to_Prop b) ∧ P. |
---|
| 204 | * [ /3/ | #n * [ #P #p % /2/ @p | #P * ] ] |
---|
| 205 | qed. |
---|
| 206 | |
---|
[2487] | 207 | lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s. |
---|
| 208 | after_n_steps (S n) O I exec g s inv P → |
---|
[2668] | 209 | ∃tr,s'. |
---|
| 210 | is_final … exec g s = None ? ∧ |
---|
| 211 | step … exec g s = Value … 〈tr,s'〉 ∧ |
---|
[2682] | 212 | (notb (eqb n 0) → bool_to_Prop (inv s')) ∧ |
---|
[2487] | 213 | after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s''). |
---|
| 214 | #n #O #I #exec #g #inv #P #s |
---|
[2444] | 215 | whd in ⊢ (% → ?); |
---|
| 216 | cases (is_final … s) |
---|
| 217 | [ whd in ⊢ (% → ?); |
---|
| 218 | cases (step … s) |
---|
| 219 | [ #o #k * |
---|
[2682] | 220 | | * #tr #s' whd in ⊢ (% → ?); #ASSERT cases (assert_nz_inv … ASSERT) * #H #AFTER |
---|
| 221 | %{tr} %{s'} % [1,3: % [1,3: /2/ | *: >H /4 by notb_Prop, absurd, nmk, I/ ] |*: /2/ ] |
---|
[2444] | 222 | | #m * |
---|
| 223 | ] |
---|
| 224 | | #r * |
---|
| 225 | ] qed. |
---|
| 226 | |
---|
[2487] | 227 | lemma after_1_step : ∀O,I,exec,g,inv,P,s. |
---|
| 228 | after_n_steps 1 O I exec g s inv P → |
---|
[2668] | 229 | ∃tr,s'. is_final … exec g s = None ? ∧ |
---|
| 230 | step ?? exec g s = Value … 〈tr,s'〉 ∧ |
---|
[2682] | 231 | P tr s'. |
---|
[2487] | 232 | #O #I #exec #g #inv #P #s #AFTER |
---|
[2444] | 233 | cases (after_1_of_n_steps … AFTER) |
---|
[2682] | 234 | #tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [%] // whd in FIN; >E0_right in FIN; // |
---|
[2444] | 235 | qed. |
---|
| 236 | |
---|
[3081] | 237 | lemma 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 | |
---|
| 266 | lemma 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 |
---|
| 272 | cases (after_aux_result … A) #tr * #s' * #p #A' |
---|
| 273 | %{tr} %{s'} %{p} @A' |
---|
| 274 | qed. |
---|
| 275 | |
---|
| 276 | lemma 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 |
---|
| 284 | cases (after_1_of_n_steps … A) |
---|
| 285 | #tr1 * #s1 * * * #F #ST #_ #A' |
---|
| 286 | cases (after_n_result … A') |
---|
| 287 | #tr'' * #s'' * #E #A'' destruct |
---|
| 288 | % [2: % [2: % [2: % [ % [% [ @F | @ST ] | % ] | @A'' ] | skip ] | skip ] | skip ] |
---|
| 289 | qed. |
---|
| 290 | |
---|
[2444] | 291 | (* A typical way to use the following: |
---|
| 292 | |
---|
| 293 | With a hypothesis |
---|
| 294 | EX : after_n_steps n ... (State ...) ... |
---|
| 295 | reduce it [whd in EX;] to |
---|
| 296 | EX : await_value ... |
---|
| 297 | then perform inversion |
---|
| 298 | [cases (await_value_bind_inv … EX) -EX * #x * #E1 #EX] |
---|
| 299 | x : T |
---|
| 300 | E1 : f = return x |
---|
| 301 | EX : await_value ... |
---|
| 302 | *) |
---|
| 303 | |
---|
| 304 | lemma await_value_bind_inv : ∀avs,T,f,g,P. |
---|
[2459] | 305 | await_value avs (m_bind … f g) P → |
---|
[2444] | 306 | ∃x:T. (f = return x) ∧ await_value avs (g x) P. |
---|
| 307 | #avs #T * |
---|
| 308 | [ #o #k #g #P * |
---|
| 309 | | #x #g #P #AWAIT %{x} % // |
---|
| 310 | | #m #g #P * |
---|
| 311 | ] qed. |
---|
| 312 | |
---|
[693] | 313 | (* A (possibly non-terminating) execution. *) |
---|
| 314 | coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝ |
---|
[1213] | 315 | | e_stop : trace → int → state → execution state output input |
---|
[693] | 316 | | e_step : trace → state → execution state output input → execution state output input |
---|
[797] | 317 | | e_wrong : errmsg → execution state output input |
---|
[693] | 318 | | e_interact : ∀o:output. (input o → execution state output input) → execution state output input. |
---|
| 319 | |
---|
| 320 | (* This definition is slightly awkward because of the need to provide resumptions. |
---|
| 321 | It records the last trace/state passed in, then recursively processes the next |
---|
| 322 | state. *) |
---|
| 323 | |
---|
[731] | 324 | let corec exec_inf_aux (output:Type[0]) (input:output → Type[0]) |
---|
[1231] | 325 | (exec:trans_system output input) (g:global ?? exec) |
---|
| 326 | (s:IO output input (trace×(state ?? exec g))) |
---|
[693] | 327 | : execution ??? ≝ |
---|
| 328 | match s with |
---|
[797] | 329 | [ Wrong m ⇒ e_wrong ??? m |
---|
[1599] | 330 | | Value v ⇒ let 〈t,s'〉 ≝ v in |
---|
[1231] | 331 | match is_final ?? exec g s' with |
---|
[1213] | 332 | [ Some r ⇒ e_stop ??? t r s' |
---|
[1599] | 333 | | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] |
---|
[1231] | 334 | | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v)) |
---|
[693] | 335 | ]. |
---|
| 336 | |
---|
[731] | 337 | lemma execution_cases: ∀o,i,s.∀e:execution s o i. |
---|
[693] | 338 | e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m |
---|
| 339 | | e_step tr s e ⇒ e_step ??? tr s e |
---|
[797] | 340 | | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ]. |
---|
[1181] | 341 | #o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E % |
---|
| 342 | | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto |
---|
| 343 | here, used reflexivity instead *) |
---|
[693] | 344 | |
---|
[1231] | 345 | axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s = |
---|
[693] | 346 | match s with |
---|
[797] | 347 | [ Wrong m ⇒ e_wrong ??? m |
---|
[1599] | 348 | | Value v ⇒ let 〈t,s'〉 ≝ v in |
---|
[1231] | 349 | match is_final ?? exec g s' with |
---|
[1213] | 350 | [ Some r ⇒ e_stop ??? t r s' |
---|
[1599] | 351 | | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ] |
---|
[1231] | 352 | | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v)) |
---|
[693] | 353 | ]. |
---|
| 354 | (* |
---|
| 355 | #exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s |
---|
| 356 | [ #o #k |
---|
| 357 | | #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *) |
---|
| 358 | | ] |
---|
| 359 | whd in ⊢ (??%%); //; |
---|
| 360 | qed. |
---|
| 361 | *) |
---|
| 362 | |
---|
[2118] | 363 | lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r. |
---|
| 364 | exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' → |
---|
| 365 | step … ge s = Value … 〈tr, s'〉 ∧ |
---|
| 366 | is_final … s' = Some ? r. |
---|
| 367 | #O #I #TS #ge #s #s' #tr #r |
---|
| 368 | >exec_inf_aux_unfold |
---|
| 369 | cases (step … ge s) |
---|
| 370 | [ 1,3: normalize #H1 #H2 try #H3 destruct |
---|
| 371 | | * #tr' #s'' |
---|
| 372 | whd in ⊢ (??%? → ?); |
---|
| 373 | lapply (refl ? (is_final … s'')) |
---|
| 374 | cases (is_final … s'') in ⊢ (???% → %); |
---|
| 375 | [ #_ whd in ⊢ (??%? → ?); #E destruct |
---|
| 376 | | #r' #E1 #E2 whd in E2:(??%?); destruct % // |
---|
| 377 | ] |
---|
| 378 | ] qed. |
---|
| 379 | |
---|
| 380 | lemma extract_step : ∀O,I,TS,ge,s,s',tr,e. |
---|
| 381 | exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e → |
---|
| 382 | step … ge s = Value … 〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s'). |
---|
| 383 | #O #I #TS #ge #s #s' #tr #e |
---|
| 384 | >exec_inf_aux_unfold |
---|
| 385 | cases (step … s) |
---|
| 386 | [ 1,3: normalize #H1 #H2 try #H3 destruct |
---|
| 387 | | * #tr' #s'' |
---|
| 388 | whd in ⊢ (??%? → ?); |
---|
| 389 | cases (is_final … s'') |
---|
| 390 | [ #E normalize in E; destruct /2/ |
---|
| 391 | | #r #E normalize in E; destruct |
---|
| 392 | ] |
---|
| 393 | ] qed. |
---|
| 394 | |
---|
[2145] | 395 | lemma extract_interact : ∀O,I,TS,ge,s,o,k. |
---|
| 396 | exec_inf_aux O I TS ge (step … ge s) = e_interact … o k → |
---|
| 397 | ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)). |
---|
| 398 | #O #I #TS #ge #s #o #k >exec_inf_aux_unfold |
---|
| 399 | cases (step … s) |
---|
| 400 | [ #o' #k' normalize #E destruct %{k'} /2/ |
---|
| 401 | | * #x #y normalize cases (is_final ?????) normalize |
---|
| 402 | #X try #Y destruct |
---|
| 403 | | normalize #m #E destruct |
---|
| 404 | ] qed. |
---|
| 405 | |
---|
[2118] | 406 | lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e. |
---|
| 407 | exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e → |
---|
| 408 | is_final … s' = None ?. |
---|
| 409 | #O #I #TS #ge #s #s' #tr #e |
---|
| 410 | >exec_inf_aux_unfold |
---|
| 411 | cases (step … s) |
---|
| 412 | [ 1,3: normalize #H1 #H2 try #H3 destruct |
---|
| 413 | | * #tr' #s'' |
---|
| 414 | whd in ⊢ (??%? → ?); |
---|
| 415 | lapply (refl ? (is_final … s'')) |
---|
| 416 | cases (is_final … s'') in ⊢ (???% → %); |
---|
| 417 | [ #F whd in ⊢ (??%? → ?); #E destruct @F |
---|
| 418 | | #r' #_ #E whd in E:(??%?); destruct |
---|
| 419 | ] |
---|
| 420 | ] qed. |
---|
| 421 | |
---|
| 422 | |
---|
| 423 | |
---|
[1233] | 424 | record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝ |
---|
[1231] | 425 | { program : Type[0] |
---|
| 426 | ; es1 :> trans_system outty inty |
---|
| 427 | ; make_global : program → global ?? es1 |
---|
| 428 | ; make_initial_state : ∀p:program. res (state ?? es1 (make_global p)) |
---|
[702] | 429 | }. |
---|
[693] | 430 | |
---|
[1231] | 431 | definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝ |
---|
[731] | 432 | λo,i,fx,p. |
---|
| 433 | match make_initial_state ?? fx p with |
---|
[1231] | 434 | [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉) |
---|
[797] | 435 | | Error m ⇒ e_wrong ??? m |
---|
[731] | 436 | ]. |
---|
[693] | 437 | |
---|
[731] | 438 | |
---|
[2618] | 439 | |
---|
| 440 | |
---|
| 441 | definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state). |
---|
| 442 | |
---|
| 443 | let rec split_trace O I (state:Type[0]) (x:execution state O I) (n:nat) on n : option (execution_prefix state × (execution state O I)) ≝ |
---|
| 444 | match n with |
---|
| 445 | [ O ⇒ Some ? 〈[ ], x〉 |
---|
| 446 | | S n' ⇒ |
---|
| 447 | match x with |
---|
| 448 | [ e_step tr s x' ⇒ |
---|
| 449 | ! 〈pre,x''〉 ← split_trace ?? state x' n'; |
---|
| 450 | Some ? 〈〈tr,s〉::pre,x''〉 |
---|
| 451 | (* Necessary for a measurable trace at the end of the program *) |
---|
| 452 | | e_stop tr r s ⇒ |
---|
| 453 | match n' with |
---|
| 454 | [ O ⇒ Some ? 〈[〈tr,s〉], x〉 |
---|
| 455 | | _ ⇒ None ? |
---|
| 456 | ] |
---|
| 457 | | _ ⇒ None ? |
---|
| 458 | ] |
---|
| 459 | ]. |
---|
| 460 | |
---|
[2668] | 461 | (* For now I'm doing this without I/O, to keep things simple. In the place I |
---|
| 462 | intend to use it (the definition of measurable subtraces, and proofs using |
---|
[2669] | 463 | that) I should allow I/O for the prefix. |
---|
| 464 | |
---|
| 465 | If the execution has the form |
---|
| 466 | |
---|
| 467 | s1 -tr1→ s2 -tr2→ … sn -trn→ s' |
---|
| 468 | |
---|
| 469 | then the function returns |
---|
| 470 | |
---|
| 471 | 〈[〈s1,tr1〉; 〈s2,tr2〉; …; 〈sn,trn〉], s'〉 |
---|
| 472 | *) |
---|
[2618] | 473 | |
---|
[2669] | 474 | let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (state … fx g × trace) × (state … fx g)) ≝ |
---|
[2668] | 475 | match n with |
---|
| 476 | [ O ⇒ return 〈[ ], s〉 |
---|
| 477 | | S m ⇒ |
---|
| 478 | match is_final … fx g s with |
---|
| 479 | [ Some r ⇒ Error … (msg TerminatedEarly) |
---|
| 480 | | None ⇒ |
---|
| 481 | match step … fx g s with |
---|
| 482 | [ Value trs ⇒ |
---|
| 483 | ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs); |
---|
[2669] | 484 | return 〈〈s, \fst trs〉::tl, s'〉 |
---|
[2668] | 485 | | Interact _ _ ⇒ Error … (msg UnexpectedIO) |
---|
| 486 | | Wrong m ⇒ Error … m |
---|
| 487 | ] |
---|
| 488 | ] |
---|
| 489 | ]. |
---|
| 490 | |
---|
| 491 | (* Show that it's nice. *) |
---|
| 492 | |
---|
| 493 | lemma exec_steps_S : ∀O,I,fx,g,n,s,trace,s''. |
---|
| 494 | exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 → |
---|
| 495 | is_final … fx g s = None ? ∧ |
---|
| 496 | ∃tr',s',tl. |
---|
[2669] | 497 | trace = 〈s,tr'〉::tl ∧ |
---|
[2668] | 498 | step … fx g s = Value … 〈tr',s'〉 ∧ |
---|
| 499 | exec_steps n O I fx g s' = OK … 〈tl,s''〉. |
---|
| 500 | #O #I #fx #g #n #s #trace #s'' |
---|
| 501 | whd in ⊢ (??%? → ?); |
---|
| 502 | cases (is_final … s) |
---|
| 503 | [ whd in ⊢ (??%? → ?); |
---|
| 504 | cases (step … s) |
---|
| 505 | [ #o #i #EX whd in EX:(??%?); destruct |
---|
| 506 | | * #tr' #s' whd in ⊢ (??%? → ?); #EX %{(refl ??)} |
---|
| 507 | %{tr'} %{s'} cases (exec_steps … g s') in EX ⊢ %; |
---|
| 508 | [ * #tl #s'' #EX whd in EX:(??%?); destruct %{tl} /3/ |
---|
| 509 | | #m #EX whd in EX:(??%?); destruct |
---|
| 510 | ] |
---|
| 511 | | #m #EX whd in EX:(??%?); destruct |
---|
| 512 | ] |
---|
| 513 | | #r #EX whd in EX:(??%?); destruct |
---|
| 514 | ] qed. |
---|
| 515 | |
---|
| 516 | lemma exec_steps_length : ∀O,I,fx,g,n,s,trace,s'. |
---|
| 517 | exec_steps n O I fx g s = OK … 〈trace,s'〉 → |
---|
| 518 | n = |trace|. |
---|
| 519 | #O #I #fx #g #n elim n |
---|
| 520 | [ #s #trace #s' #EX whd in EX:(??%?); destruct % |
---|
| 521 | | #m #IH #s #trace #s' #EX |
---|
| 522 | cases (exec_steps_S … EX) #notfinal * #tr' * #s'' * #tl * * #Etl #Estep #steps |
---|
| 523 | >(IH … steps) >Etl % |
---|
| 524 | ] qed. |
---|
| 525 | |
---|
| 526 | lemma exec_steps_nonterm : ∀O,I,fx,g,n,s,h,t,s'. |
---|
| 527 | exec_steps n O I fx g s = OK … 〈h::t,s'〉 → |
---|
| 528 | is_final … s = None ?. |
---|
| 529 | #O #I #fx #g #n #s #h #t #s' #EX |
---|
| 530 | lapply (exec_steps_length … EX) |
---|
| 531 | #Elen destruct whd in EX:(??%?); |
---|
| 532 | cases (is_final … s) in EX ⊢ %; |
---|
| 533 | [ // |
---|
| 534 | | #r #EX whd in EX:(??%?); destruct |
---|
| 535 | ] qed. |
---|
| 536 | |
---|
| 537 | lemma exec_steps_nonterm' : ∀O,I,fx,g,n,s,h,t,s'. |
---|
| 538 | exec_steps n O I fx g s = OK … 〈h@[t], s'〉 → |
---|
| 539 | is_final … s = None ?. |
---|
| 540 | #O #I #fx #g #n #s * [2: #h1 #h2] #t #s' @exec_steps_nonterm |
---|
| 541 | qed. |
---|
| 542 | |
---|
[2669] | 543 | let rec gather_trace S (l:list (S × trace)) on l : trace ≝ |
---|
[2668] | 544 | match l with |
---|
| 545 | [ nil ⇒ E0 |
---|
[2669] | 546 | | cons h t ⇒ (\snd h)⧺(gather_trace S t) |
---|
[2668] | 547 | ]. |
---|
| 548 | |
---|
| 549 | lemma exec_steps_after_n_simple : ∀n,O,I,fx,g,s,trace,s'. |
---|
| 550 | exec_steps n O I fx g s = OK ? 〈trace,s'〉 → |
---|
| 551 | after_n_steps n O I fx g s (λ_. true) (λtr,s''. 〈tr,s''〉 = 〈gather_trace ? trace,s'〉). |
---|
| 552 | #n elim n |
---|
| 553 | [ #O #I #fx #g #s #trace #s' #EXEC whd in EXEC:(??%?); destruct |
---|
| 554 | whd % |
---|
| 555 | | #m #IH #O #I #fx #g #s #trace #s' #EXEC |
---|
| 556 | cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS |
---|
[2682] | 557 | @(after_n_m 1 … (IH … STEPS)) // |
---|
[2668] | 558 | whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct % |
---|
| 559 | ] qed. |
---|
| 560 | |
---|
| 561 | lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P. |
---|
| 562 | exec_steps n O I fx g s = OK ? 〈trace,s'〉 → |
---|
[2669] | 563 | all ? (λstr. inv (\fst str)) (tail … trace) → |
---|
[2668] | 564 | P (gather_trace ? trace) s' → |
---|
| 565 | after_n_steps n O I fx g s inv P. |
---|
| 566 | #n elim n |
---|
| 567 | [ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct |
---|
[2682] | 568 | #ALL #p whd @p |
---|
[2668] | 569 | | #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC |
---|
| 570 | cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS |
---|
| 571 | destruct |
---|
[2682] | 572 | #ALL cut ((notb (eqb m 0) → bool_to_Prop (inv s1)) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl))) |
---|
[2669] | 573 | [ cases m in STEPS; |
---|
[2682] | 574 | [ whd in ⊢ (??%? → ?); #E destruct % [ * #H cases (H (refl ??)) | /2/ ] |
---|
[2669] | 575 | | #m' #STEPS cases (exec_steps_S … STEPS) #_ * #tr'' * #s'' * #tl'' * * #E #_ #_ destruct |
---|
[2682] | 576 | whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; [ /2/ | * ] |
---|
[2669] | 577 | ] |
---|
| 578 | ] * #i1 #itl |
---|
[2682] | 579 | #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?)) |
---|
[2668] | 580 | [ @p |
---|
[2682] | 581 | | @i1 |
---|
| 582 | | whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #p' @p' |
---|
[2668] | 583 | ] |
---|
| 584 | ] qed. |
---|
| 585 | |
---|
| 586 | lemma exec_steps_after_n_noinv : ∀n,O,I,fx,g,s,trace,s',P. |
---|
| 587 | exec_steps n O I fx g s = OK ? 〈trace,s'〉 → |
---|
| 588 | P (gather_trace ? trace) s' → |
---|
| 589 | after_n_steps n O I fx g s (λ_.true) P. |
---|
| 590 | #n #O #I #fx #g #s #trace #s' #P #EXEC #p |
---|
| 591 | @(exec_steps_after_n … EXEC) // |
---|
[2669] | 592 | cases trace // #x #trace' |
---|
| 593 | elim trace' /2/ |
---|
[2668] | 594 | qed. |
---|
| 595 | |
---|
[2685] | 596 | lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'. |
---|
| 597 | exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 → |
---|
| 598 | s = s1. |
---|
| 599 | #n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC |
---|
| 600 | lapply (exec_steps_length … EXEC) #E normalize in E; destruct |
---|
| 601 | cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct |
---|
| 602 | % |
---|
| 603 | qed. |
---|
| 604 | |
---|
[2668] | 605 | lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P. |
---|
| 606 | after_n_steps n O I fx g s inv P → |
---|
[2685] | 607 | ∃trace,s'. |
---|
| 608 | exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ |
---|
| 609 | bool_to_Prop (all ? (λstr. inv (\fst str)) (tail … trace)) ∧ |
---|
| 610 | P (gather_trace ? trace) s'. |
---|
[2668] | 611 | #n elim n |
---|
[2685] | 612 | [ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} % [ %{(refl ??)} % | @AFTER ] |
---|
[2668] | 613 | | #m #IH #O #I #fx #g #s #inv #P #AFTER |
---|
| 614 | cases (after_1_of_n_steps … AFTER) |
---|
| 615 | #tr1 * #s1 * * * #NF #STEP #INV #AFTER' |
---|
| 616 | cases (IH … AFTER') |
---|
[2685] | 617 | #tl * #s' * * #STEPS #INV' #p |
---|
[2669] | 618 | %{(〈s,tr1〉::tl)} %{s'} % |
---|
[2685] | 619 | [ % |
---|
| 620 | [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % |
---|
| 621 | | cases tl in STEPS INV INV' ⊢ %; [ // | * #sx #trx #t #STEPS #INV #INV' |
---|
| 622 | <(exec_steps_first … STEPS) whd in ⊢ (?%); >INV // |
---|
| 623 | >(exec_steps_length … STEPS) % |
---|
| 624 | ] |
---|
| 625 | ] |
---|
| 626 | | // ] |
---|
[2668] | 627 | ] qed. |
---|
| 628 | |
---|
| 629 | lemma exec_steps_split : ∀n,m,O,I,fx,g,s,trace,s'. |
---|
| 630 | exec_steps (n+m) O I fx g s = OK ? 〈trace,s'〉 → |
---|
| 631 | ∃trace1,trace2,s1. |
---|
| 632 | exec_steps n O I fx g s = OK ? 〈trace1,s1〉 ∧ |
---|
| 633 | exec_steps m O I fx g s1 = OK ? 〈trace2,s'〉 ∧ |
---|
| 634 | trace = trace1 @ trace2. |
---|
| 635 | #n elim n |
---|
| 636 | [ #m #O #I #fx #g #s #trace #s' #EXEC |
---|
| 637 | %{[ ]} %{trace} %{s} /3/ |
---|
| 638 | | #n' #IH #m #O #I #fx #g #s #trace #s' #EXEC |
---|
| 639 | cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC' |
---|
| 640 | cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2 |
---|
[2669] | 641 | %{(〈s,tr'〉::trace1)} %{trace2} %{s1} |
---|
[2668] | 642 | % |
---|
| 643 | [ % |
---|
| 644 | [ whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >EXEC1 % |
---|
| 645 | | @EXEC2 |
---|
| 646 | ] |
---|
| 647 | | destruct % |
---|
| 648 | ] |
---|
| 649 | ] qed. |
---|
| 650 | |
---|
| 651 | lemma exec_steps_join : ∀n,m,O,I,fx,g,s1,trace1,s2,trace2,s3. |
---|
| 652 | exec_steps n O I fx g s1 = OK ? 〈trace1,s2〉 → |
---|
| 653 | exec_steps m O I fx g s2 = OK ? 〈trace2,s3〉 → |
---|
| 654 | exec_steps (n+m) O I fx g s1 = OK ? 〈trace1@trace2,s3〉. |
---|
| 655 | #n elim n |
---|
| 656 | [ #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2 |
---|
| 657 | whd in EXEC1:(??%?); destruct @EXEC2 |
---|
| 658 | | #n' #IH #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2 |
---|
| 659 | cases (exec_steps_S … EXEC1) #NF * #tr' * #s' * #tl' * * #E1 #STEP #EXEC' |
---|
| 660 | whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >(IH … EXEC' EXEC2) |
---|
| 661 | destruct % |
---|
| 662 | ] qed. |
---|
| 663 | |
---|
[2669] | 664 | (* Show that it corresponds to split_trace … (exec_inf …). |
---|
| 665 | We need to adjust the form of trace. *) |
---|
| 666 | |
---|
| 667 | let rec switch_trace_aux S tr (l:list (S × trace)) (s':S) on l : list (trace × S) ≝ |
---|
| 668 | match l with |
---|
| 669 | [ nil ⇒ [〈tr,s'〉] |
---|
| 670 | | cons h t ⇒ 〈tr,\fst h〉::(switch_trace_aux S (\snd h) t s') |
---|
| 671 | ]. |
---|
| 672 | |
---|
| 673 | definition switch_trace ≝ |
---|
| 674 | λS,l,s'. match l with |
---|
| 675 | [ nil ⇒ nil ? |
---|
| 676 | | cons h t ⇒ switch_trace_aux S (\snd h) t s' |
---|
| 677 | ]. |
---|
| 678 | |
---|
[2668] | 679 | lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'. |
---|
| 680 | exec_steps n O I fx g s = OK ? 〈trace,s'〉 → |
---|
| 681 | match is_final … s' with |
---|
[2669] | 682 | [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', exec_inf_aux … fx g (step … s')〉 |
---|
| 683 | | Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', e_stop … tr' r s'〉 |
---|
[2668] | 684 | ]. |
---|
| 685 | #O #I #fx #g #n elim n |
---|
| 686 | [ #s #trace #s' #EX whd in EX:(??%%); destruct |
---|
| 687 | cases (is_final … s') [ % | #r %1 % ] |
---|
| 688 | | #m #IH #s #trace #s' #EX |
---|
| 689 | cases (exec_steps_S … EX) |
---|
| 690 | #notfinal * #tr'' * #s'' * #tl * * #Etrace #Estep #Esteps |
---|
| 691 | cases tl in Etrace Esteps ⊢ %; |
---|
| 692 | [ #E destruct #Esteps |
---|
| 693 | lapply (exec_steps_length … Esteps) #Elen normalize in Elen; destruct |
---|
| 694 | whd in Esteps:(??%?); destruct |
---|
| 695 | >Estep |
---|
| 696 | >exec_inf_aux_unfold normalize nodelta |
---|
| 697 | cases (is_final … s') |
---|
[2669] | 698 | [ whd % |
---|
[2668] | 699 | | #r %2 %{tr''} % |
---|
| 700 | ] |
---|
[2669] | 701 | | * #s1 #tr1 #tl1 #E normalize in E; destruct #Esteps |
---|
[2668] | 702 | lapply (IH … Esteps) cases (is_final … s') |
---|
[2669] | 703 | [ normalize nodelta #IH' >Estep <(exec_steps_first … Esteps) |
---|
| 704 | >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); |
---|
| 705 | >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' normalize nodelta % |
---|
[2668] | 706 | | normalize nodelta #r * |
---|
| 707 | [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct |
---|
[2669] | 708 | | * #tr'' #IH' %2 %{tr''} >Estep <(exec_steps_first … Esteps) |
---|
| 709 | >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); |
---|
[2668] | 710 | >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' % |
---|
| 711 | ] |
---|
| 712 | ] |
---|
| 713 | ] |
---|
| 714 | ] qed. |
---|