[700] | 1 | include "Clight/CexecComplete.ma". |
---|
| 2 | include "Clight/CexecSound.ma". |
---|
| 3 | include "utilities/extralib.ma". |
---|
[398] | 4 | |
---|
[487] | 5 | include "basics/jmeq.ma". |
---|
[399] | 6 | |
---|
[398] | 7 | (* A "single execution" - where all of the input values are made explicit. *) |
---|
[487] | 8 | coinductive s_execution : Type[0] ≝ |
---|
[398] | 9 | | se_stop : trace → int → mem → s_execution |
---|
| 10 | | se_step : trace → state → s_execution → s_execution |
---|
| 11 | | se_wrong : s_execution |
---|
[700] | 12 | | se_interact : ∀o:io_out. (io_in o → execution state io_out io_in) → io_in o → s_execution → s_execution. |
---|
[398] | 13 | |
---|
[700] | 14 | coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝ |
---|
| 15 | | seo_stop : ∀tr,r,m. single_exec_of (e_stop ??? tr r m) (se_stop tr r m) |
---|
[398] | 16 | | seo_step : ∀tr,s,e,se. |
---|
| 17 | single_exec_of e se → |
---|
[700] | 18 | single_exec_of (e_step ??? tr s e) (se_step tr s se) |
---|
| 19 | | seo_wrong : single_exec_of (e_wrong ???) se_wrong |
---|
[398] | 20 | | seo_interact : ∀o,k,i,se. |
---|
| 21 | single_exec_of (k i) se → |
---|
[700] | 22 | single_exec_of (e_interact ??? o k) (se_interact o k i se). |
---|
[398] | 23 | |
---|
| 24 | (* starting after state s, zero or more steps of execution e reach state s' |
---|
| 25 | after which comes e'. *) |
---|
[487] | 26 | inductive execution_isteps : trace → state → s_execution → state → s_execution → Prop ≝ |
---|
[398] | 27 | | isteps_none : ∀s,e. execution_isteps E0 s e s e |
---|
| 28 | | isteps_one : ∀e,e',tr,tr',s,s',s0. |
---|
| 29 | execution_isteps tr' s e s' e' → |
---|
| 30 | execution_isteps (tr⧺tr') s0 (se_step tr s e) s' e' |
---|
| 31 | | isteps_interact : ∀e,e',o,k,i,s,s',s0,tr,tr'. |
---|
| 32 | execution_isteps tr' s e s' e' → |
---|
| 33 | execution_isteps (tr⧺tr') s0 (se_interact o k i (se_step tr s e)) s' e'. |
---|
| 34 | |
---|
[487] | 35 | lemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3. |
---|
[398] | 36 | execution_isteps tr1 s1 e1 s2 e2 → |
---|
| 37 | execution_isteps tr2 s2 e2 s3 e3 → |
---|
| 38 | execution_isteps (tr1⧺tr2) s1 e1 s3 e3. |
---|
[487] | 39 | #tr1 #tr2 #s1 #s2 #s3 #e1 #e2 #e3 #H1 elim H1; |
---|
| 40 | [ #s #e //; |
---|
| 41 | | #e #e' #tr #tr' #s1' #s2' #s3' #H1 #H2 #H3 |
---|
| 42 | >(Eapp_assoc …) |
---|
| 43 | @isteps_one |
---|
| 44 | @H2 @H3 |
---|
| 45 | | #e #e' #o #k #i #s1' #s2' #s3' #tr #tr' #H1 #H2 #H3 |
---|
| 46 | >(Eapp_assoc …) |
---|
| 47 | @isteps_interact |
---|
[398] | 48 | /2/ |
---|
[487] | 49 | ] qed. |
---|
[398] | 50 | |
---|
[702] | 51 | lemma is_final_elim: ∀s.∀P:option int → Type[0]. |
---|
| 52 | (∀r. final_state s r → P (Some ? r)) → |
---|
| 53 | ((¬∃r.final_state s r) → P (None ?)) → |
---|
[732] | 54 | P (is_final ?? clight_exec s). |
---|
| 55 | #s #P #F #NF lapply (refl ? (is_final ?? clight_exec s)) |
---|
| 56 | cases (is_final ?? clight_exec s) in ⊢ (???% → %) |
---|
[708] | 57 | [ #E @NF % * #r #H > (is_final_complete … H) in E #H destruct |
---|
| 58 | | #r #E @F @is_final_sound @E |
---|
[702] | 59 | ] qed. |
---|
| 60 | |
---|
| 61 | lemma exec_e_step: ∀ge,x,tr,s,e. |
---|
[732] | 62 | exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e → |
---|
| 63 | exec_inf_aux ?? clight_exec ge (exec_step ge s) = e. |
---|
[702] | 64 | #ge #x #tr #s #e |
---|
[487] | 65 | >(exec_inf_aux_unfold …) cases x; |
---|
| 66 | [ #o #k #EXEC whd in EXEC:(??%?); destruct |
---|
[708] | 67 | | #y cases y #tr' #s' whd in ⊢ (??%? → ?) |
---|
[702] | 68 | @is_final_elim |
---|
| 69 | [ #r #FINAL | #FINAL ] |
---|
[708] | 70 | #EXEC whd in EXEC:(??%?); destruct @refl |
---|
[487] | 71 | | #EXEC whd in EXEC:(??%?); destruct |
---|
| 72 | ] qed. |
---|
[398] | 73 | |
---|
[487] | 74 | lemma exec_e_step_inv: ∀ge,x,tr,s,e. |
---|
[732] | 75 | exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e → |
---|
[398] | 76 | x = Value ??? 〈tr,s〉. |
---|
[487] | 77 | #ge #x #tr #s #e |
---|
| 78 | >(exec_inf_aux_unfold …) cases x; |
---|
| 79 | [ #o #k #EXEC whd in EXEC:(??%?); destruct |
---|
| 80 | | #y cases y; #tr' #s' whd in ⊢ (??%? → ?); |
---|
[702] | 81 | @is_final_elim |
---|
[708] | 82 | [ #r ] #FINAL #EXEC whd in EXEC:(??%?); |
---|
| 83 | destruct @refl |
---|
[487] | 84 | | #EXEC whd in EXEC:(??%?); destruct |
---|
| 85 | ] qed. |
---|
[398] | 86 | |
---|
[487] | 87 | lemma exec_e_step_inv2: ∀ge,x,tr,s,e. |
---|
[732] | 88 | exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e → |
---|
[398] | 89 | ¬∃r.final_state s r. |
---|
[487] | 90 | #ge #x #tr #s #e |
---|
| 91 | >(exec_inf_aux_unfold …) cases x; |
---|
| 92 | [ #o #k #EXEC whd in EXEC:(??%?); destruct |
---|
[702] | 93 | | #y cases y; #tr' #s' whd in ⊢ (??%? → ?) |
---|
[708] | 94 | @is_final_elim [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F |
---|
[487] | 95 | | #EXEC whd in EXEC:(??%?); destruct |
---|
| 96 | ] qed. |
---|
[398] | 97 | |
---|
[487] | 98 | definition exec_from : genv → state → s_execution → Prop ≝ |
---|
[732] | 99 | λge,s,se. single_exec_of (exec_inf_aux ?? clight_exec ge (exec_step ge s)) se. |
---|
[398] | 100 | |
---|
[702] | 101 | lemma se_step_eq : ∀tr,s,e,tr',s',e'. |
---|
| 102 | se_step tr s e = se_step tr' s' e' → |
---|
| 103 | tr = tr' ∧ s = s' ∧ e = e'. |
---|
[708] | 104 | #tr #s #e #tr' #s' #e' #E destruct |
---|
| 105 | % try % @refl qed. |
---|
[702] | 106 | |
---|
[487] | 107 | lemma exec_from_step : ∀ge,s,tr,s',e. |
---|
[398] | 108 | exec_from ge s (se_step tr s' e) → |
---|
| 109 | exec_step ge s = Value ??? 〈tr,s'〉 ∧ exec_from ge s' e. |
---|
[487] | 110 | #ge #s0 #tr0 #s0' #e0 #H inversion H; |
---|
| 111 | [ #tr #r #m #E1 #E2 destruct |
---|
[708] | 112 | | #tr #s #e #se #H1 #H2 #E (* destruct (E) ;*) |
---|
| 113 | cases (se_step_eq … E) * #E1 #E2 #E3 >E1 >E2 >E3 |
---|
[487] | 114 | >(exec_e_step_inv … H2) |
---|
| 115 | <(exec_e_step … H2) in H1 #H1 % // |
---|
| 116 | | #_ #E destruct |
---|
| 117 | | #o #k #i #se #H1 #H2 #E destruct |
---|
| 118 | ] qed. |
---|
[398] | 119 | |
---|
[708] | 120 | lemma exec_from_interact : ∀ge,s,o,k,i,tr,s',e. |
---|
[398] | 121 | exec_from ge s (se_interact o k i (se_step tr s' e)) → |
---|
| 122 | step ge s tr s' ∧ |
---|
| 123 | (*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e. |
---|
[487] | 124 | #ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H; |
---|
| 125 | [ #tr #r #m #E1 #E2 destruct |
---|
| 126 | | #tr #s #e #se #H1 #H2 #E destruct (E) |
---|
| 127 | | #_ #E destruct |
---|
[708] | 128 | | #o #k #i #se #H1 #H2 #E destruct (E); |
---|
[487] | 129 | lapply (exec_step_sound ge s0); |
---|
| 130 | cases (exec_step ge s0) in H2 ⊢ %; |
---|
| 131 | [ #o' #k' >(exec_inf_aux_unfold …) |
---|
| 132 | #E' whd in E':(??%?); destruct (E'); |
---|
| 133 | #STEP |
---|
| 134 | inversion H1; |
---|
| 135 | [ #tr #r #m #E1 #E2 destruct |
---|
| 136 | | #tr' #s' #e' #se' #H2 #H3 #E2 destruct (E2); |
---|
[708] | 137 | <(exec_e_step … H3) in H2 #H2 % [ 2: @H2 ] |
---|
[487] | 138 | lapply (STEP i); |
---|
| 139 | >(exec_e_step_inv … H3) |
---|
| 140 | #S @S |
---|
| 141 | | #_ #E destruct |
---|
| 142 | | #o #k #i #se #H1 #H2 #E destruct |
---|
| 143 | ] |
---|
| 144 | | #x cases x; #tr' #s' >(exec_inf_aux_unfold …) |
---|
[708] | 145 | whd in ⊢ (??%? → ?); @is_final_elim |
---|
| 146 | [ #r ] #F #E whd in E:(??%?); destruct |
---|
[487] | 147 | | >(exec_inf_aux_unfold …) |
---|
| 148 | #E' whd in E':(??%?); destruct (E'); |
---|
| 149 | ] |
---|
[708] | 150 | ] qed. |
---|
[398] | 151 | |
---|
[708] | 152 | lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m. |
---|
[398] | 153 | exec_from ge s (se_interact o k i (se_stop tr r m)) → |
---|
| 154 | step ge s tr (Returnstate (Vint r) Kstop m). |
---|
[487] | 155 | #ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H; |
---|
| 156 | [ #tr #r #m #E1 #E2 destruct |
---|
| 157 | | #tr #s #e #se #H1 #H2 #E destruct (E) |
---|
| 158 | | #_ #E destruct |
---|
| 159 | | #o #k #i #se #H1 #H2 #E destruct (E); |
---|
| 160 | lapply (exec_step_sound ge s0); |
---|
| 161 | >(exec_inf_aux_unfold …) in H2; |
---|
| 162 | cases (exec_step ge s0); |
---|
| 163 | [ #o' #k' |
---|
| 164 | #E' whd in E':(??%?); destruct (E'); |
---|
| 165 | #STEP |
---|
| 166 | inversion H1; |
---|
| 167 | [ #tr #r #m #E1 #E2 lapply (STEP i); destruct; |
---|
| 168 | >(exec_inf_aux_unfold …) in E1; |
---|
| 169 | cases (k' i); |
---|
| 170 | [ #o2 #k2 #E whd in E:(??%?); destruct (E) |
---|
| 171 | | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?); |
---|
[708] | 172 | @is_final_elim |
---|
| 173 | [ #r' #FINAL #E whd in E:(??%?); |
---|
[487] | 174 | destruct (E); |
---|
| 175 | inversion FINAL; |
---|
| 176 | #r'' #m'' #E1 #E2 destruct (E1 E2); //; |
---|
| 177 | | #NF #E whd in E:(??%?); destruct (E) |
---|
| 178 | ] |
---|
| 179 | | #E whd in E:(??%?); destruct (E) |
---|
| 180 | ] |
---|
| 181 | | #tr #s #e #e' #H #EXEC #E destruct (E) |
---|
| 182 | | #EXEC #E destruct (E) |
---|
| 183 | | #o2 #k2 #i2 #e2 #H #EXEC #E destruct (E) |
---|
| 184 | ] |
---|
| 185 | | #x cases x; #tr #s whd in ⊢ (??%? → ?); |
---|
[708] | 186 | @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct (E) |
---|
[487] | 187 | | #E whd in E:(??%?); destruct (E) |
---|
| 188 | ] |
---|
[708] | 189 | ] qed. |
---|
[398] | 190 | |
---|
| 191 | (* NB: the E0 in the execs are irrelevant. *) |
---|
[487] | 192 | lemma several_steps: ∀ge,tr,e,e',s,s'. |
---|
[398] | 193 | execution_isteps tr s e s' e' → |
---|
| 194 | exec_from ge s e → |
---|
| 195 | star (mk_transrel … step) ge s tr s' ∧ |
---|
| 196 | exec_from ge s' e'. |
---|
[487] | 197 | #ge #tr0 #e0 #e0' #s0 #s0' #H |
---|
| 198 | elim H; |
---|
| 199 | [ #s #e #EXEC % //; |
---|
| 200 | | #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #STEPS #IH #EXEC |
---|
| 201 | elim (exec_from_step … EXEC); #EXEC3 #EXEC1 |
---|
| 202 | elim (IH EXEC1); |
---|
| 203 | #STAR12 #EXEC2 % //; |
---|
| 204 | lapply (exec_step_sound ge s3); |
---|
| 205 | >EXEC3 #STEP3 |
---|
| 206 | @(star_step (mk_transrel ?? step) … STEP3 STAR12) |
---|
| 207 | @refl |
---|
| 208 | | #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #STEPS #IH #EXEC |
---|
| 209 | elim (exec_from_interact … EXEC); |
---|
| 210 | #STEP3 #EXEC1 |
---|
| 211 | elim (IH EXEC1); #STAR #EXEC2 |
---|
| 212 | % |
---|
| 213 | [ @(star_step (mk_transrel ?? step) … STEP3 STAR) |
---|
| 214 | @refl |
---|
| 215 | | // |
---|
| 216 | ] |
---|
| 217 | ] qed. |
---|
[398] | 218 | |
---|
[487] | 219 | inductive execution_terminates : trace → state → s_execution → int → mem → Prop ≝ |
---|
[398] | 220 | | terminates : ∀s,s',tr,tr',r,e,m. |
---|
| 221 | execution_isteps tr s e s' (se_stop tr' r m) → |
---|
| 222 | execution_terminates (tr⧺tr') s (se_step E0 s e) r m |
---|
| 223 | (* We should only be able to get to here if main is an external function, which is silly. *) |
---|
| 224 | | annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i. |
---|
| 225 | execution_isteps tr s e s' (se_interact o k i (se_stop tr' r m)) → |
---|
| 226 | execution_terminates (tr⧺tr') s (se_step E0 s e) r m. |
---|
| 227 | |
---|
[487] | 228 | coinductive execution_diverging : s_execution → Prop ≝ |
---|
[398] | 229 | | diverging_step : ∀s,e. execution_diverging e → execution_diverging (se_step E0 s e). |
---|
| 230 | |
---|
| 231 | (* Makes a finite number of interactions (including cost labels) before diverging. *) |
---|
[487] | 232 | inductive execution_diverges : trace → state → s_execution → Prop ≝ |
---|
[398] | 233 | | diverges_diverging: ∀tr,s,s',e,e'. |
---|
| 234 | execution_isteps tr s e s' e' → |
---|
| 235 | execution_diverging e' → |
---|
| 236 | execution_diverges tr s (se_step E0 s e). |
---|
| 237 | |
---|
| 238 | (* NB: "reacting" includes hitting a cost label. *) |
---|
[487] | 239 | coinductive execution_reacting : traceinf → state → s_execution → Prop ≝ |
---|
[398] | 240 | | reacting: ∀tr,tr',s,s',e,e'. |
---|
| 241 | execution_reacting tr' s' e' → |
---|
| 242 | execution_isteps tr s e s' e' → |
---|
| 243 | tr ≠ E0 → |
---|
| 244 | execution_reacting (tr⧻tr') s e. |
---|
| 245 | |
---|
[487] | 246 | inductive execution_reacts : traceinf → state → s_execution → Prop ≝ |
---|
[398] | 247 | | reacts: ∀tr,s,e. |
---|
| 248 | execution_reacting tr s e → |
---|
| 249 | execution_reacts tr s (se_step E0 s e). |
---|
| 250 | |
---|
[487] | 251 | inductive execution_goes_wrong: trace → state → s_execution → state → Prop ≝ |
---|
[398] | 252 | | go_wrong: ∀tr,s,s',e. |
---|
| 253 | execution_isteps tr s e s' se_wrong → |
---|
| 254 | execution_goes_wrong tr s (se_step E0 s e) s'. |
---|
| 255 | |
---|
[487] | 256 | let corec silent_sound ge s e |
---|
[398] | 257 | (H0:execution_diverging e) |
---|
| 258 | (EXEC:exec_from ge s e) |
---|
| 259 | : forever_silent (mk_transrel ?? step) … ge s ≝ ?. |
---|
[487] | 260 | cut (∃s2.∃e2.And (And (execution_diverging e2) (step ge s E0 s2)) (exec_from ge s2 e2)); |
---|
| 261 | [ cases H0 in EXEC ⊢ %; #s1 #e1 #H1 #EXEC |
---|
| 262 | elim (exec_from_step … EXEC); |
---|
| 263 | #EXEC0 #EXEC1 |
---|
| 264 | %{ s1} %{ e1} % //; % //; |
---|
| 265 | lapply (exec_step_sound ge s); >EXEC0 whd in ⊢ (% → ?); #H @H |
---|
| 266 | | *; #s2 *; #e2 *; *; #H2 #STEP2 #EXEC2 |
---|
| 267 | @(forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 e2 ??)) |
---|
[398] | 268 | //; |
---|
[487] | 269 | ] qed. |
---|
[398] | 270 | |
---|
[708] | 271 | lemma final_step: ∀ge,tr,r,m,s. |
---|
[398] | 272 | exec_from ge s (se_stop tr r m) → |
---|
| 273 | step ge s tr (Returnstate (Vint r) Kstop m). |
---|
[487] | 274 | #ge #tr #r #m #s #EXEC |
---|
| 275 | whd in EXEC; |
---|
| 276 | inversion EXEC; |
---|
| 277 | [ #tr' #r' #m' #EXEC' #E destruct (E); |
---|
| 278 | lapply (exec_step_sound ge s); |
---|
| 279 | >(exec_inf_aux_unfold …) in EXEC'; |
---|
| 280 | cases (exec_step ge s); |
---|
| 281 | [ #o #k #EXEC' whd in EXEC':(??%?); destruct (EXEC'); |
---|
| 282 | | #x cases x; #tr'' #s' whd in ⊢ (??%? → ?); |
---|
[708] | 283 | @is_final_elim [ #r'' #FINAL | #F ] |
---|
[487] | 284 | #EXEC' whd in EXEC':(??%?); destruct (EXEC'); |
---|
| 285 | | #EXEC' whd in EXEC':(??%?); destruct (EXEC'); |
---|
| 286 | ] |
---|
| 287 | inversion FINAL; #r''' #m' #E1 #E2 #H destruct (E1 E2); |
---|
| 288 | @H |
---|
| 289 | | #tr' #s' #e' #se' #H #EXEC' #E destruct |
---|
| 290 | | #EXEC' #E destruct |
---|
| 291 | | #o #k #i #e #H #EXEC #E destruct |
---|
[708] | 292 | ] qed. |
---|
[398] | 293 | |
---|
| 294 | |
---|
[487] | 295 | lemma e_stop_inv: ∀ge,x,tr,r,m. |
---|
[732] | 296 | exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r m → |
---|
[398] | 297 | x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉. |
---|
[487] | 298 | #ge #x #tr #r #m |
---|
| 299 | >(exec_inf_aux_unfold …) cases x; |
---|
| 300 | [ #o #k #EXEC whd in EXEC:(??%?); destruct; |
---|
[702] | 301 | | #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim |
---|
| 302 | [ #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?); |
---|
[487] | 303 | destruct (EXEC); @refl |
---|
| 304 | | #F #EXEC whd in EXEC:(??%?); destruct (EXEC); |
---|
| 305 | ] |
---|
| 306 | | #EXEC whd in EXEC:(??%?); destruct (EXEC); |
---|
| 307 | ] qed. |
---|
[398] | 308 | |
---|
[487] | 309 | lemma terminates_sound: ∀ge,tr,s,r,m,e. |
---|
[398] | 310 | execution_terminates tr s (se_step E0 s e) r m → |
---|
| 311 | exec_from ge s e → |
---|
| 312 | star (mk_transrel … step) ge s tr (Returnstate (Vint r) Kstop m). |
---|
[487] | 313 | #ge #tr0 #s0 #r #m #e0 #H inversion H; |
---|
| 314 | [ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC |
---|
| 315 | destruct (E1 E2 E3 E4 E5); |
---|
| 316 | cases (several_steps … ESTEPS EXEC); #STARs' #EXECs' |
---|
| 317 | @(star_right … STARs') |
---|
| 318 | [ 2: @(final_step ge tr' r m s' … EXECs') |
---|
| 319 | | skip |
---|
| 320 | | @refl |
---|
| 321 | ] |
---|
| 322 | | #s #s' #tr #tr' #r #e #m #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC |
---|
| 323 | destruct; |
---|
| 324 | cases (several_steps … ESTEPS EXEC); #STARs' #EXECs' |
---|
| 325 | @(star_right … STARs') |
---|
| 326 | [ @tr' |
---|
| 327 | | @(exec_from_interact_stop … EXECs') |
---|
| 328 | | @refl |
---|
| 329 | ] |
---|
| 330 | ] qed. |
---|
[398] | 331 | |
---|
[487] | 332 | let corec reacts_sound ge tr s e |
---|
[398] | 333 | (REACTS:execution_reacting tr s e) |
---|
| 334 | (EXEC:exec_from ge s e) : |
---|
| 335 | forever_reactive (mk_transrel … step) ge s tr ≝ ?. |
---|
[487] | 336 | cut (∃s'.∃e'.∃tr'.∃tr''.(And (And (And (execution_reacting tr'' s' e') (execution_isteps tr' s e s' e')) (tr' ≠ E0)) (tr = tr'⧻tr''))); |
---|
| 337 | [ inversion REACTS; |
---|
| 338 | #tr0 #tr' #s0 #s' #e0 #e' #EREACTS #ESTEPS #REACTED #E1 #E2 #E3 destruct (E2 E3); |
---|
| 339 | %{ s'} %{ e'} %{ tr0} %{ tr'} % [ % [ % //; | @REACTED ] | @refl ] |
---|
| 340 | | *; #s' *; #e' *; #tr' *; #tr'' |
---|
| 341 | *; *; *; #REACTS' #ESTEPS #REACTED #APPTR |
---|
| 342 | (* >APPTR *) |
---|
| 343 | @(match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ]) |
---|
| 344 | % |
---|
| 345 | cases (several_steps … ESTEPS EXEC); #STEPS #EXEC' |
---|
| 346 | [ 2: @STEPS |
---|
| 347 | | skip |
---|
| 348 | | @REACTED |
---|
| 349 | | @reacts_sound |
---|
| 350 | [ 2: @REACTS' |
---|
| 351 | | skip |
---|
| 352 | | @EXEC' |
---|
| 353 | ] |
---|
| 354 | ] |
---|
| 355 | qed. |
---|
[399] | 356 | |
---|
[487] | 357 | lemma exec_from_wrong: ∀ge,s. |
---|
[399] | 358 | exec_from ge s se_wrong → |
---|
| 359 | exec_step ge s = Wrong ???. |
---|
[487] | 360 | #ge #s #H whd in H; |
---|
| 361 | inversion H; |
---|
| 362 | [ #tr #r #m #EXEC #E destruct (E) |
---|
| 363 | | #tr #s' #e #e' #H #EXEC #E destruct (E) |
---|
| 364 | | >(exec_inf_aux_unfold …) |
---|
| 365 | cases (exec_step ge s); |
---|
| 366 | [ #o #k #EXEC whd in EXEC:(??%?); destruct |
---|
[702] | 367 | | #x cases x; #tr #s' whd in ⊢ (??%? → ?) @is_final_elim |
---|
| 368 | [ #r ] #F #EXEC whd in EXEC:(??%?); destruct |
---|
[487] | 369 | | // |
---|
| 370 | ] |
---|
| 371 | | #o #k #i #e #H #EXEC #E destruct |
---|
| 372 | ] qed. |
---|
[399] | 373 | |
---|
[487] | 374 | lemma exec_from_step_notfinal: ∀ge,s,tr,s',e. |
---|
[399] | 375 | exec_from ge s (se_step tr s' e) → |
---|
| 376 | ¬(∃r. final_state s' r). |
---|
[487] | 377 | #ge #s #tr #s' #e #H whd in H; inversion H; |
---|
| 378 | [ #tr' #r #m #EXEC #E destruct |
---|
| 379 | | #tr' #s'' #e' #e'' #H #EXEC #E destruct (E); |
---|
| 380 | >(exec_inf_aux_unfold …) in EXEC; |
---|
| 381 | cases (exec_step ge s); |
---|
| 382 | [ #o #k #EXEC whd in EXEC:(??%?); destruct |
---|
[702] | 383 | | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim |
---|
[708] | 384 | [ #r ] #F #E whd in E:(??%?); destruct @F |
---|
[487] | 385 | | #E whd in E:(??%?); destruct |
---|
| 386 | ] |
---|
| 387 | | #EXEC #E destruct |
---|
| 388 | | #o #k #i #e' #H #EXEC #E destruct |
---|
| 389 | ] qed. |
---|
[399] | 390 | |
---|
[487] | 391 | lemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e. |
---|
[399] | 392 | exec_from ge s (se_interact o k i (se_step tr s' e)) → |
---|
| 393 | ¬(∃r. final_state s' r). |
---|
[487] | 394 | #ge #s #o #k #i #tr #s' #e #H |
---|
| 395 | % *; #r #F cases F in H; #r' #m #H |
---|
| 396 | inversion H; |
---|
| 397 | [ #tr' #r #m #EXEC #E destruct |
---|
| 398 | | #tr' #s'' #e' #e'' #H #EXEC #E destruct (E); |
---|
| 399 | | #EXEC #E destruct |
---|
| 400 | | #o' #k' #i' #e' #H #EXEC #E destruct; |
---|
| 401 | >(exec_inf_aux_unfold …) in EXEC; |
---|
| 402 | cases (exec_step ge s); |
---|
| 403 | [ #o1 #k1 #EXEC1 whd in EXEC1:(??%?); destruct (EXEC1); |
---|
| 404 | inversion H; |
---|
| 405 | [ #tr1 #r1 #m1 #EXECK #E destruct (E); |
---|
| 406 | | #tr1 #s1 #e1 #e2 #H1 #EXECK #E destruct (E); |
---|
| 407 | >(exec_inf_aux_unfold …) in EXECK; |
---|
| 408 | cases (k1 i'); |
---|
| 409 | [ #o2 #k2 #EXECK whd in EXECK:(??%?); destruct |
---|
| 410 | | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?); |
---|
[708] | 411 | @is_final_elim [ #r ] #F #EXECK |
---|
[487] | 412 | whd in EXECK:(??%?); destruct; |
---|
| 413 | @(absurd ?? F) |
---|
| 414 | %{ r'} //; |
---|
| 415 | | #E whd in E:(??%?); destruct |
---|
| 416 | ] |
---|
| 417 | | #EXECK #E whd in E:(??%?); destruct |
---|
| 418 | | #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct |
---|
| 419 | ] |
---|
| 420 | | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?); |
---|
[708] | 421 | @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct; |
---|
[487] | 422 | | #E whd in E:(??%?); destruct |
---|
| 423 | ] |
---|
| 424 | ] qed. |
---|
[399] | 425 | |
---|
[487] | 426 | lemma wrong_sound: ∀ge,tr,s,s',e. |
---|
[399] | 427 | execution_goes_wrong tr s (se_step E0 s e) s' → |
---|
| 428 | exec_from ge s e → |
---|
| 429 | (¬∃r. final_state s r) → |
---|
| 430 | star (mk_transrel … step) ge s tr s' ∧ |
---|
| 431 | nostep (mk_transrel … step) ge s' ∧ |
---|
| 432 | (¬∃r. final_state s' r). |
---|
[487] | 433 | #ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG; |
---|
| 434 | #tr #s #s' #e #ESTEPS #E1 #E2 #E3 #E4 #EXEC #NOTFINAL destruct (E1 E2 E3 E4); |
---|
| 435 | cases (several_steps … ESTEPS EXEC); |
---|
| 436 | #STAR #EXEC' % |
---|
| 437 | [ % [ @STAR |
---|
| 438 | | #badtr #bads % #badSTEP |
---|
| 439 | lapply (step_complete … badSTEP); |
---|
| 440 | >(exec_from_wrong … EXEC') |
---|
[399] | 441 | //; |
---|
[487] | 442 | ] |
---|
| 443 | | % |
---|
| 444 | elim ESTEPS in NOTFINAL EXEC ⊢ %; |
---|
| 445 | [ #s1 #e1 #NF #EX #F @(absurd ? F NF) |
---|
| 446 | | #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #ESTEPS1 #IH #NF #EXEC |
---|
| 447 | cases (exec_from_step … EXEC); #EXEC3 #EXEC1 |
---|
| 448 | @(IH … EXEC1) |
---|
| 449 | @(exec_from_step_notfinal … EXEC) |
---|
| 450 | | #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #ESTEPS1 #IH #NF #EXEC |
---|
| 451 | @IH |
---|
| 452 | [ @(exec_from_interact_step_notfinal … EXEC) |
---|
[708] | 453 | | cases (exec_from_interact … EXEC) #STEP #EF1 @EF1 |
---|
[487] | 454 | ] |
---|
| 455 | ] |
---|
| 456 | ] qed. |
---|
[399] | 457 | |
---|
[487] | 458 | inductive execution_characterisation : state → s_execution → Prop ≝ |
---|
[399] | 459 | | ec_terminates: ∀s,r,m,e,tr. |
---|
| 460 | execution_terminates tr s e r m → |
---|
| 461 | execution_characterisation s e |
---|
| 462 | | ec_diverges: ∀s,e,tr. |
---|
| 463 | execution_diverges tr s e → |
---|
| 464 | execution_characterisation s e |
---|
| 465 | | ec_reacts: ∀s,e,tr. |
---|
| 466 | execution_reacts tr s e → |
---|
| 467 | execution_characterisation s e |
---|
| 468 | | ec_wrong: ∀e,s,s',tr. |
---|
| 469 | execution_goes_wrong tr s e s' → |
---|
| 470 | execution_characterisation s e. |
---|
| 471 | |
---|
| 472 | (* bit of a hack to avoid inability to reduce term in match *) |
---|
[487] | 473 | definition interact_prop : ∀A:Type[0].(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝ |
---|
[399] | 474 | λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ]. |
---|
| 475 | |
---|
[487] | 476 | lemma err_does_not_interact: ∀A,B,P,e1,e2. |
---|
[399] | 477 | (∀x:B.interact_prop A P (e2 x)) → |
---|
| 478 | interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2). |
---|
[487] | 479 | #A #B #P #e1 #e2 #H |
---|
| 480 | cases e1; //; qed. |
---|
[399] | 481 | |
---|
[487] | 482 | lemma err2_does_not_interact: ∀A,B,C,P,e1,e2. |
---|
[399] | 483 | (∀x,y.interact_prop A P (e2 x y)) → |
---|
| 484 | interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2). |
---|
[487] | 485 | #A #B #C #P #e1 #e2 #H |
---|
| 486 | cases e1; [ #z cases z; ] //; qed. |
---|
[399] | 487 | |
---|
[487] | 488 | lemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2. |
---|
[399] | 489 | (∀x.interact_prop A P (e2 x)) → |
---|
[487] | 490 | interact_prop A P (bindIO ?? (Sig B Q) A (err_to_io_sig ??? Q e1) e2). |
---|
| 491 | #A #B #P #Q #e1 #e2 #H |
---|
| 492 | cases e1; //; qed. |
---|
[399] | 493 | |
---|
[487] | 494 | lemma opt_does_not_interact: ∀A,B,P,e1,e2. |
---|
[399] | 495 | (∀x:B.interact_prop A P (e2 x)) → |
---|
| 496 | interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2). |
---|
[487] | 497 | #A #B #P #e1 #e2 #H |
---|
| 498 | cases e1; //; qed. |
---|
[399] | 499 | |
---|
[487] | 500 | lemma exec_step_interaction: |
---|
[399] | 501 | ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s). |
---|
[487] | 502 | #ge #s cases s; |
---|
| 503 | [ #f #st #kk #e #m cases st; |
---|
| 504 | [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ] |
---|
| 505 | [ 4,6,8,9: @I ] |
---|
| 506 | whd in ⊢ (???%); |
---|
| 507 | [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%); |
---|
| 508 | cases (type_eq_dec (fn_return f) Tvoid); #x //; @err2_does_not_interact // ] |
---|
| 509 | | cases (find_label a (fn_body f) (call_cont kk)); [ @I | #z cases z #x #y @I ] |
---|
| 510 | | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I |
---|
| 511 | | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I |
---|
| 512 | | @err2_does_not_interact #x1 #x2 cases x1; //; |
---|
| 513 | | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @err_does_not_interact #x6 cases a; |
---|
| 514 | [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ] |
---|
| 515 | | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I |
---|
| 516 | | @I ] |
---|
| 517 | | cases kk; [ 1,8: cases (fn_return f); //; | 2,3,5,6,7: //; |
---|
| 518 | | #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I ] |
---|
| 519 | | cases kk; //; |
---|
| 520 | | cases kk; [ 4: #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I |
---|
| 521 | | *: // ] |
---|
| 522 | ] |
---|
| 523 | | #f #args #kk #m cases f; |
---|
| 524 | [ #f' whd in ⊢ (???%); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f')) |
---|
| 525 | #x1 #x2 whd in ⊢ (???%) @err_does_not_interact // |
---|
[399] | 526 | (* This is the only case that actually matters! *) |
---|
[487] | 527 | | #fn #argtys #rty whd in ⊢ (???%); |
---|
| 528 | @err_does_not_interact #x1 |
---|
| 529 | whd; #i % [ 2: % [ 2: % [ % whd in ⊢ (??%?); @refl |
---|
| 530 | | % #E whd in E:(??%%); destruct (E); ] ] ] |
---|
| 531 | ] |
---|
| 532 | | #v #kk #m whd in ⊢ (???%); cases kk; |
---|
| 533 | [ 8: #x1 #x2 #x3 #x4 cases x1; |
---|
| 534 | [ whd in ⊢ (???%); cases v; // | #x5 whd in ⊢ (???%); cases x5; |
---|
| 535 | #x6 #x7 @opt_does_not_interact // ] |
---|
| 536 | | *: // ] |
---|
| 537 | ] qed. |
---|
[399] | 538 | |
---|
| 539 | |
---|
| 540 | (* Some classical logic (roughly like a fragment of Coq's library) *) |
---|
[487] | 541 | lemma classical_doubleneg: |
---|
[399] | 542 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 543 | ∀P:Prop. ¬ (¬ P) → P. |
---|
[487] | 544 | #classic #P *; #H |
---|
| 545 | cases (classic P); |
---|
| 546 | [ // | #H' @False_ind /2/; ] |
---|
| 547 | qed. |
---|
[399] | 548 | |
---|
[487] | 549 | lemma classical_not_all_not_ex: |
---|
[399] | 550 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 551 | ∀A:Type[0].∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x. |
---|
| 552 | #classic #A #P *; #H |
---|
| 553 | @(classical_doubleneg classic) % *; #H' |
---|
| 554 | @H #x % #H'' @H' %{x} @H'' |
---|
| 555 | qed. |
---|
[399] | 556 | |
---|
[487] | 557 | lemma classical_not_all_ex_not: |
---|
[399] | 558 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 559 | ∀A:Type[0].∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x. |
---|
| 560 | #classic #A #P *; #H |
---|
| 561 | @(classical_not_all_not_ex classic A (λx.¬ P x)) |
---|
| 562 | % #H' @H #x @(classical_doubleneg classic) |
---|
| 563 | @H' |
---|
| 564 | qed. |
---|
[399] | 565 | |
---|
[487] | 566 | lemma not_ex_all_not: |
---|
| 567 | ∀A:Type[0].∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x. |
---|
| 568 | #A #P *; #H #x % #H' |
---|
| 569 | @H %{ x} @H' |
---|
| 570 | qed. |
---|
[399] | 571 | |
---|
[487] | 572 | lemma not_imply_elim: |
---|
[399] | 573 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 574 | ∀P,Q:Prop. ¬ (P → Q) → P. |
---|
[487] | 575 | #classic #P #Q *; #H |
---|
| 576 | @(classical_doubleneg classic) % *; #H' |
---|
| 577 | @H #H'' @False_ind @H' @H'' |
---|
| 578 | qed. |
---|
[399] | 579 | |
---|
[487] | 580 | lemma not_imply_elim2: |
---|
[399] | 581 | ∀P,Q:Prop. ¬ (P → Q) → ¬ Q. |
---|
[487] | 582 | #P #Q *; #H % #H' |
---|
| 583 | @H #_ @H' |
---|
| 584 | qed. |
---|
[399] | 585 | |
---|
[487] | 586 | lemma imply_to_and: |
---|
[399] | 587 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 588 | ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q. |
---|
[487] | 589 | #classic #P #Q #H % |
---|
| 590 | [ @(not_imply_elim classic P Q H) |
---|
| 591 | | @(not_imply_elim2 P Q H) |
---|
| 592 | ] qed. |
---|
[399] | 593 | |
---|
[487] | 594 | lemma not_and_to_imply: |
---|
[399] | 595 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
| 596 | ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q. |
---|
[487] | 597 | #classic #P #Q *; #H #H' |
---|
| 598 | % #H'' @H % //; |
---|
| 599 | qed. |
---|
[399] | 600 | |
---|
[487] | 601 | inductive execution_not_over : s_execution → Prop ≝ |
---|
[399] | 602 | | eno_step: ∀tr,s,e. execution_not_over (se_step tr s e) |
---|
| 603 | | eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)). |
---|
| 604 | |
---|
[487] | 605 | lemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False. |
---|
| 606 | #tr0 #r0 #m0 #H inversion H; |
---|
| 607 | [ #tr #s #e #E destruct |
---|
| 608 | | #o #k #tr #s #e #i #E destruct |
---|
| 609 | ] qed. |
---|
[399] | 610 | |
---|
[487] | 611 | lemma eno_wrong: execution_not_over se_wrong → False. |
---|
| 612 | #H inversion H; |
---|
| 613 | [ #tr #s #e #E destruct |
---|
| 614 | | #o #k #tr #s #e #i #E destruct |
---|
| 615 | ] qed. |
---|
[399] | 616 | |
---|
[487] | 617 | let corec show_divergence s e |
---|
[399] | 618 | (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 → |
---|
| 619 | execution_not_over e1) |
---|
| 620 | (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0) |
---|
[487] | 621 | (CONTINUES:∀tr2,s2,o,k,i,e'. execution_isteps tr2 s e s2 (se_interact o k i e') → ∃tr3.∃s3.∃e3. And (e' = se_step tr3 s3 e3) (tr3 ≠ E0)) |
---|
[399] | 622 | : execution_diverging e ≝ ?. |
---|
[487] | 623 | lapply (NONTERMINATING E0 s e ?); //; |
---|
| 624 | cases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %; |
---|
| 625 | [ #tr #i #m #_ #_ #_ #ENO elim (eno_stop … ENO); |
---|
| 626 | | #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?); |
---|
| 627 | [ <(E0_right tr) in ⊢ (?%????) |
---|
| 628 | @isteps_one @isteps_none |
---|
| 629 | | #TR @(match sym_eq ??? TR with [ refl ⇒ ? ]) (* >TR in UNREACTIVE ⊢ % *) |
---|
| 630 | #NONTERMINATING #CONTINUES #_ % |
---|
| 631 | @(show_divergence s') |
---|
| 632 | [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1) |
---|
| 633 | change in ⊢ (?%????) with (Eapp E0 tr1); @isteps_one |
---|
| 634 | @S |
---|
| 635 | | #tr2 #s2 #e2 #S >TR in UNREACTIVE #UNREACTIVE @(UNREACTIVE tr2 s2 e2) |
---|
| 636 | change in ⊢ (?%????) with (Eapp E0 tr2); |
---|
| 637 | @isteps_one @S |
---|
| 638 | | #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i) |
---|
| 639 | change in ⊢ (?%????) with (Eapp E0 tr2); |
---|
| 640 | @(isteps_one … S) |
---|
| 641 | ] |
---|
| 642 | ] |
---|
| 643 | | #_ #_ #_ #ENO elim (eno_wrong … ENO); |
---|
| 644 | | #o #k #i #e' #UNREACTIVE #NONTERMINATING #CONTINUES #_ |
---|
| 645 | lapply (CONTINUES E0 s o k i e' (isteps_none …)); |
---|
| 646 | *; #tr' *; #s' *; #e' *; #EXEC #NOTSILENT |
---|
| 647 | @False_ind @(absurd ?? NOTSILENT) |
---|
| 648 | @(UNREACTIVE … s' e') |
---|
| 649 | <(E0_right tr') in ⊢ (?%????) |
---|
| 650 | >EXEC |
---|
| 651 | @isteps_interact //; |
---|
| 652 | ] qed. |
---|
[399] | 653 | |
---|
[487] | 654 | (* XXX == > jmeq notation and coercion *) |
---|
| 655 | |
---|
| 656 | lemma jmeq_to_eq : ∀A:Type[0].∀a,b:A.jmeq A a A b → a = b. |
---|
| 657 | #A #a #b #E @gral @jm_to_eq_sigma @E |
---|
| 658 | qed. |
---|
| 659 | |
---|
| 660 | coercion jmeq_to_eq : ∀A:Type[0].∀a,b:A.∀p:jmeq A a A b.a = b ≝ |
---|
| 661 | jmeq_to_eq on _p: jmeq ???? to eq ???. |
---|
| 662 | |
---|
| 663 | notation > "hvbox(a break ≃ b)" |
---|
| 664 | non associative with precedence 45 |
---|
| 665 | for @{ 'jmeq ? $a ? $b }. |
---|
| 666 | |
---|
| 667 | notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)" |
---|
| 668 | non associative with precedence 45 |
---|
| 669 | for @{ 'jmeq $t $a $u $b }. |
---|
| 670 | |
---|
| 671 | interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y). |
---|
| 672 | |
---|
| 673 | (* XXX < == *) |
---|
| 674 | |
---|
| 675 | lemma se_inv: ∀e1,e2. |
---|
[399] | 676 | single_exec_of e1 e2 → |
---|
| 677 | match e1 with |
---|
| 678 | [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m' | _ ⇒ False ] |
---|
| 679 | | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ] |
---|
| 680 | | e_wrong ⇒ match e2 with [ se_wrong ⇒ True | _ ⇒ False ] |
---|
| 681 | | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ] |
---|
| 682 | ]. |
---|
[487] | 683 | #e01 #e02 #H |
---|
| 684 | cases H; |
---|
| 685 | [ #tr #r #m whd; % [ % ] // |
---|
| 686 | | #tr #s #e1' #e2' #H' whd; % [ % ] // |
---|
| 687 | | whd; // |
---|
| 688 | | #o #k #i #e #H' whd; % [ % ] // |
---|
| 689 | ] qed. |
---|
[399] | 690 | |
---|
[487] | 691 | lemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e. |
---|
[399] | 692 | exec_from ge s (se_interact o k i (se_step tr s' e)) → |
---|
| 693 | tr ≠ E0. |
---|
[487] | 694 | #ge #o #k #i #tr #s #s' #e whd in ⊢ (% → ?); >(exec_inf_aux_unfold …) |
---|
| 695 | lapply (exec_step_interaction ge s); |
---|
| 696 | cases (exec_step ge s); |
---|
| 697 | [ #o' #k' ; whd in ⊢ (% → ?%? → ?); #H #K cases (se_inv … K); |
---|
| 698 | *; #E1 #E2 #H1 destruct (E1); |
---|
| 699 | lapply (H i); *; #tr' *; #s'' *; #K' #TR |
---|
| 700 | >E2 in H1 #H1 whd in H1:(?%?); >K' in H1 |
---|
| 701 | >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?); |
---|
[708] | 702 | @is_final_elim |
---|
| 703 | [ #r #F whd in ⊢ (?%? → ?); #S |
---|
[487] | 704 | @False_ind @(absurd ? S) cases (se_inv … S) |
---|
| 705 | | #NF #S whd in S:(?%?); cases (se_inv … S); |
---|
| 706 | *; #E1 #E2 #S' <E1 @TR |
---|
| 707 | ] |
---|
[708] | 708 | | #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?) |
---|
| 709 | @is_final_elim [ #r ] #F #E whd in E:(?%?); |
---|
[487] | 710 | inversion E; |
---|
| 711 | [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct |
---|
| 712 | | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct |
---|
| 713 | | 3,7: #E destruct |
---|
| 714 | | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct |
---|
| 715 | ] |
---|
| 716 | | #_ #E whd in E:(?%?); |
---|
| 717 | inversion E; |
---|
| 718 | [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct |
---|
| 719 | | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct |
---|
| 720 | | 3,7: #E1 #E2 destruct |
---|
| 721 | | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct |
---|
| 722 | ] |
---|
| 723 | ] qed. |
---|
[399] | 724 | |
---|
[487] | 725 | let corec reactive_traceinf' ge s e |
---|
[399] | 726 | (EXEC:exec_from ge s e) |
---|
| 727 | (REACTIVE: ∀tr,s1,e1. |
---|
| 728 | execution_isteps tr s e s1 e1 → |
---|
[487] | 729 | (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))) |
---|
[399] | 730 | : traceinf' ≝ ?. |
---|
[487] | 731 | lapply (REACTIVE E0 s e (isteps_none …)); |
---|
| 732 | *; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H |
---|
| 733 | %{ tr ? H} |
---|
| 734 | @(reactive_traceinf' ge s' e' ?) |
---|
| 735 | [ cases (several_steps … STEPS EXEC); #_ #H' @H' |
---|
| 736 | | #tr1 #s1 #e1 #STEPS1 |
---|
| 737 | @REACTIVE |
---|
| 738 | [ 2: |
---|
| 739 | @(isteps_trans … STEPS STEPS1) |
---|
| 740 | | skip |
---|
| 741 | ] |
---|
| 742 | ] |
---|
| 743 | qed. |
---|
[399] | 744 | |
---|
| 745 | (* A slightly different version of the above, to work around a problem with the |
---|
| 746 | next result. *) |
---|
[487] | 747 | let corec reactive_traceinf'' ge s e |
---|
[399] | 748 | (EXEC:exec_from ge s e) |
---|
[487] | 749 | (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)) |
---|
[399] | 750 | (REACTIVE: ∀tr,s1,e1. |
---|
| 751 | execution_isteps tr s e s1 e1 → |
---|
[487] | 752 | (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))) |
---|
[399] | 753 | : traceinf' ≝ ?. |
---|
[487] | 754 | cases REACTIVE0; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H |
---|
| 755 | %{ tr ? H} |
---|
| 756 | @(reactive_traceinf'' ge s' e' ?) |
---|
| 757 | [ cases (several_steps … STEPS EXEC); #_ #H' @H' |
---|
| 758 | | @(REACTIVE … STEPS) |
---|
| 759 | | #tr1 #s1 #e1 #STEPS1 |
---|
| 760 | @REACTIVE |
---|
| 761 | [ 2: |
---|
| 762 | @(isteps_trans … STEPS STEPS1) |
---|
| 763 | | skip |
---|
| 764 | ] |
---|
| 765 | ] qed. |
---|
[399] | 766 | |
---|
| 767 | (* We want to prove |
---|
| 768 | |
---|
[487] | 769 | lemma show_reactive : ∀ge,s. |
---|
[399] | 770 | ∀REACTIVE:∀tr,s1,e1. |
---|
| 771 | execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 → |
---|
| 772 | Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0. |
---|
| 773 | execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)). |
---|
| 774 | |
---|
| 775 | but the current matita won't unfold reactive_traceinf' so that we can do case |
---|
| 776 | analysis on (REACTIVE …). Instead we take an "applied" version of REACTIVE that |
---|
| 777 | we can do case analysis on, then get it into the desired form afterwards. |
---|
| 778 | *) |
---|
[487] | 779 | let corec show_reactive' ge s e |
---|
[399] | 780 | (EXEC:exec_from ge s e) |
---|
[487] | 781 | (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)) |
---|
[399] | 782 | (REACTIVE: ∀tr1,s1,e1. |
---|
| 783 | execution_isteps tr1 s e s1 e1 → |
---|
[487] | 784 | (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))) |
---|
[399] | 785 | : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?. |
---|
[487] | 786 | (*>(unroll_traceinf' (reactive_traceinf'' …)) *) |
---|
| 787 | @(match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]) |
---|
| 788 | cases REACTIVE0; |
---|
| 789 | #x cases x; #tr1 #y cases y; #s1 #e1 #z cases z; #STEPS #NOTSILENT |
---|
| 790 | whd in ⊢ (?(?%)??); |
---|
| 791 | (*>(traceinf_traceinfp_app …) *) |
---|
| 792 | @(match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]) |
---|
| 793 | @(reacting … STEPS NOTSILENT) |
---|
| 794 | @show_reactive' |
---|
| 795 | qed. |
---|
[399] | 796 | |
---|
[487] | 797 | lemma show_reactive : ∀ge,s,e. |
---|
[399] | 798 | ∀EXEC:exec_from ge s e. |
---|
| 799 | ∀REACTIVE:∀tr,s1,e1. |
---|
| 800 | execution_isteps tr s e s1 e1 → |
---|
[487] | 801 | (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)). |
---|
[399] | 802 | execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e. |
---|
[487] | 803 | [ #ge #s #e #EXEC #REACTIVE |
---|
| 804 | @show_reactive' |
---|
| 805 | | @(REACTIVE … (isteps_none …)) |
---|
| 806 | ] qed. |
---|
[399] | 807 | |
---|
[487] | 808 | lemma execution_characterisation_complete: |
---|
[399] | 809 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 810 | ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P). |
---|
[399] | 811 | ∀ge,s,e. |
---|
| 812 | exec_from ge s e → |
---|
| 813 | execution_characterisation s (se_step E0 s e). |
---|
[487] | 814 | #classic #constructive_indefinite_description #ge #s #e #EXEC |
---|
| 815 | cases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 → |
---|
[399] | 816 | execution_not_over e1)); |
---|
[487] | 817 | [ #NONTERMINATING |
---|
| 818 | cases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧ |
---|
[399] | 819 | ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0)); |
---|
[487] | 820 | [ *; #tr *; #s1 *; #e1 *; #INITIAL #UNREACTIVE |
---|
| 821 | @(ec_diverges … s ? tr) |
---|
| 822 | @(diverges_diverging … INITIAL) |
---|
| 823 | @(show_divergence s1 e1) |
---|
| 824 | [ #tr2 #s2 #e2 #S @(NONTERMINATING (Eapp tr tr2) s2 e2) |
---|
| 825 | @(isteps_trans … INITIAL S) |
---|
| 826 | | #tr2 #s2 #e2 #S @(UNREACTIVE … S) |
---|
| 827 | | #tr2 #s2 #o #k #i #e2 #STEPS |
---|
| 828 | lapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?); |
---|
| 829 | [ @(isteps_trans … INITIAL STEPS) ] |
---|
| 830 | #NOTOVER inversion NOTOVER; |
---|
| 831 | [ #tr' #s' #e' #E destruct (E); |
---|
| 832 | | #o' #k' #tr' #s' #e' #i' #E destruct (E); |
---|
| 833 | %{ tr'} %{s'} %{e'} % //; |
---|
| 834 | cases (several_steps … INITIAL EXEC); #_ #EXEC1 |
---|
| 835 | cases (several_steps … STEPS EXEC1); #_ #EXEC2 |
---|
| 836 | @(interaction_is_not_silent … EXEC2) |
---|
| 837 | ] |
---|
| 838 | ] |
---|
[399] | 839 | |
---|
[487] | 840 | | *; #NOTUNREACTIVE |
---|
| 841 | cut (∀tr,s1,e1.execution_isteps tr s e s1 e1 → |
---|
[399] | 842 | ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0); |
---|
[487] | 843 | [ #tr #s1 #e1 #STEPS |
---|
| 844 | @(classical_doubleneg classic) % #NOREACTION |
---|
| 845 | @NOTUNREACTIVE |
---|
| 846 | %{ tr} %{s1} %{e1} % //; |
---|
| 847 | #tr2 #s2 #e2 #STEPS2 |
---|
| 848 | lapply (not_ex_all_not … NOREACTION); #NR1 |
---|
| 849 | lapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2 |
---|
| 850 | @(classical_doubleneg classic) |
---|
| 851 | @NR2 normalize // |
---|
| 852 | | #REACTIVE |
---|
| 853 | @ec_reacts |
---|
| 854 | [ 2: @reacts |
---|
| 855 | @(show_reactive ge s … EXEC) |
---|
| 856 | #tr #s1 #e1 #STEPS |
---|
| 857 | @constructive_indefinite_description |
---|
| 858 | @(REACTIVE … tr s1 e1 STEPS) |
---|
| 859 | | skip |
---|
| 860 | ] |
---|
| 861 | ] |
---|
| 862 | ] |
---|
[399] | 863 | |
---|
[487] | 864 | | #NOTNONTERMINATING lapply (classical_not_all_ex_not classic … NOTNONTERMINATING); |
---|
| 865 | *; #tr #NNT2 lapply (classical_not_all_ex_not classic … NNT2); |
---|
| 866 | *; #s' #NNT3 lapply (classical_not_all_ex_not classic … NNT3); |
---|
| 867 | *; #e #NNT4 elim (imply_to_and classic … NNT4); |
---|
| 868 | cases e; |
---|
| 869 | [ #tr' #r #m #STEPS #NOSTEP |
---|
| 870 | @(ec_terminates s r m ? (Eapp tr tr')) % |
---|
| 871 | [ @s' |
---|
| 872 | | @STEPS |
---|
| 873 | ] |
---|
| 874 | | #tr' #s'' #e' #STEPS *; #NOSTEP @False_rect_Type0 |
---|
| 875 | @NOSTEP // |
---|
| 876 | | #STEPS #NOSTEP |
---|
| 877 | @(ec_wrong ? s s' tr) % //; |
---|
[399] | 878 | (* The following is stupidly complicated when most of the cases are impossible. |
---|
| 879 | It ought to be simplified. *) |
---|
[487] | 880 | | #o #k #i #e' #STEPS #NOSTEP |
---|
| 881 | cases e' in STEPS NOSTEP; |
---|
| 882 | [ #tr' #r #m #STEPS #NOSTEP |
---|
| 883 | @(ec_terminates s ???) |
---|
| 884 | [ 4: @(annoying_corner_case_terminates … STEPS) ] |
---|
| 885 | | #tr1 #s1 #e1 #STEPS *; #NOSTEP |
---|
| 886 | @False_ind @NOSTEP // |
---|
| 887 | | #STEPS #NOSTEP |
---|
| 888 | lapply (exec_step_interaction ge s'); |
---|
| 889 | cases (several_steps … STEPS EXEC); #_ |
---|
| 890 | whd in ⊢ (% → ?); |
---|
| 891 | >(exec_inf_aux_unfold …) |
---|
| 892 | cases (exec_step ge s'); |
---|
| 893 | [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H; |
---|
| 894 | cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); |
---|
| 895 | cases (H i); #tr1 *; #s1 *; #K #E >K in H2 |
---|
| 896 | >(exec_inf_aux_unfold …) |
---|
[708] | 897 | whd in ⊢ (?%? → ?) @is_final_elim [ #r ] |
---|
[487] | 898 | #F #S whd in S:(?%?); cases (se_inv … S); |
---|
[708] | 899 | | #x cases x; #tr' #s' whd in ⊢ (?%? → ?) |
---|
| 900 | @is_final_elim [ #r ] #F #S whd in S:(?%?); |
---|
[487] | 901 | cases (se_inv … S); |
---|
| 902 | | #S cases (se_inv … S); |
---|
| 903 | ] |
---|
| 904 | | #o1 #k1 #i1 #e1 #STEPS #NOSTEP |
---|
| 905 | lapply (exec_step_interaction ge s'); |
---|
| 906 | cases (several_steps … STEPS EXEC); #_ |
---|
| 907 | whd in ⊢ (% → ?); |
---|
| 908 | >(exec_inf_aux_unfold …) |
---|
| 909 | cases (exec_step ge s'); |
---|
| 910 | [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H; |
---|
| 911 | cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); |
---|
| 912 | cases (H i); #tr1 *; #s1 *; #K #E >K in H2 |
---|
| 913 | >(exec_inf_aux_unfold …) |
---|
[708] | 914 | whd in ⊢ (?%? → ?) @is_final_elim [ #r ] |
---|
[487] | 915 | #F #S whd in S:(?%?); cases (se_inv … S); |
---|
[708] | 916 | | #x cases x; #tr' #s' whd in ⊢ (?%? → ?) |
---|
| 917 | @is_final_elim [ #r ] #F #S whd in S:(?%?); |
---|
[487] | 918 | cases (se_inv … S); |
---|
| 919 | | #S cases (se_inv … S); |
---|
| 920 | ] |
---|
| 921 | ] |
---|
| 922 | ] |
---|
| 923 | ] |
---|
| 924 | qed. |
---|
[399] | 925 | |
---|
[487] | 926 | inductive execution_matches_behavior: s_execution → program_behavior → Prop ≝ |
---|
[399] | 927 | | emb_terminates: ∀s,e,tr,r,m. |
---|
| 928 | execution_terminates tr s e r m → |
---|
| 929 | execution_matches_behavior e (Terminates tr r) |
---|
| 930 | | emb_diverges: ∀s,e,tr. |
---|
| 931 | execution_diverges tr s e → |
---|
| 932 | execution_matches_behavior e (Diverges tr) |
---|
| 933 | | emb_reacts: ∀s,e,tr. |
---|
| 934 | execution_reacts tr s e → |
---|
| 935 | execution_matches_behavior e (Reacts tr) |
---|
| 936 | | emb_wrong: ∀e,s,s',tr. |
---|
| 937 | execution_goes_wrong tr s e s' → |
---|
| 938 | execution_matches_behavior e (Goes_wrong tr) |
---|
| 939 | | emb_initially_wrong: |
---|
| 940 | execution_matches_behavior se_wrong (Goes_wrong E0). |
---|
| 941 | |
---|
[487] | 942 | lemma exec_state_terminates: ∀tr,tr',s,s',e,r,m. |
---|
[399] | 943 | execution_terminates tr s (se_step tr' s' e) r m → s = s'. |
---|
[487] | 944 | #tr #tr' #s #s' #e #r #m #H inversion H; |
---|
| 945 | [ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl |
---|
| 946 | | #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl |
---|
| 947 | ] qed. |
---|
[399] | 948 | |
---|
[487] | 949 | lemma exec_state_diverges: ∀tr,tr',s,s',e. |
---|
[399] | 950 | execution_diverges tr s (se_step tr' s' e) → s = s'. |
---|
[487] | 951 | #tr #tr' #s #s' #e #H inversion H; |
---|
| 952 | #tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 destruct; @refl qed. |
---|
[399] | 953 | |
---|
[487] | 954 | lemma exec_state_reacts: ∀tr,tr',s,s',e. |
---|
[399] | 955 | execution_reacts tr s (se_step tr' s' e) → s = s'. |
---|
[487] | 956 | #tr #tr' #s #s' #e #H inversion H; |
---|
| 957 | #tr1 #s1 #e1 #H' #E1 #E2 #E3 destruct; @refl qed. |
---|
[399] | 958 | |
---|
[487] | 959 | lemma exec_state_wrong: ∀tr,tr',s,s',s'',e. |
---|
[399] | 960 | execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'. |
---|
[487] | 961 | #tr #tr' #s #s' #s'' #e #H inversion H; |
---|
| 962 | #tr1 #s1 #s2 #e1 #H' #E1 #E2 #E3 #E4 destruct; @refl qed. |
---|
[399] | 963 | |
---|
[487] | 964 | lemma behavior_of_execution: ∀s,e. |
---|
[399] | 965 | execution_characterisation s e → |
---|
| 966 | ∃b:program_behavior. execution_matches_behavior e b. |
---|
[487] | 967 | #s0 #e0 #exec |
---|
| 968 | cases exec; |
---|
| 969 | [ #s #r #m #e #tr #TERM |
---|
| 970 | %{ (Terminates tr r)} |
---|
| 971 | @(emb_terminates … TERM) |
---|
| 972 | | #s #e #tr #DIV |
---|
| 973 | %{ (Diverges tr)} |
---|
| 974 | @(emb_diverges … DIV) |
---|
| 975 | | #s #e #tr #REACTS |
---|
| 976 | %{ (Reacts tr)} |
---|
| 977 | @(emb_reacts … REACTS) |
---|
| 978 | | #e #s #s' #tr #WRONG |
---|
| 979 | %{ (Goes_wrong tr)} |
---|
| 980 | @(emb_wrong … WRONG) |
---|
| 981 | ] qed. |
---|
[399] | 982 | |
---|
[487] | 983 | lemma initial_state_not_final: ∀ge,s. |
---|
[399] | 984 | initial_state ge s → |
---|
| 985 | ¬ ∃r.final_state s r. |
---|
[487] | 986 | #ge #s #H cases H; |
---|
| 987 | #b #f #ge #m #E1 #E2 #E3 #E4 % *; #r #H2 |
---|
| 988 | inversion H2; |
---|
| 989 | #r' #m' #E5 #E6 destruct (E5); |
---|
| 990 | qed. |
---|
[399] | 991 | |
---|
[487] | 992 | lemma initial_step: ∀ge,s,e. |
---|
[732] | 993 | exec_inf_aux ?? clight_exec ge (Value ??? 〈E0,s〉) = e → |
---|
[399] | 994 | ¬(∃r.final_state s r) → |
---|
[708] | 995 | ∃e'.e = e_step ??? E0 s e'. |
---|
[487] | 996 | #ge #s #e >(exec_inf_aux_unfold …) |
---|
[708] | 997 | whd in ⊢ (??%? → ?) @is_final_elim |
---|
| 998 | [ #r #FINAL #EXEC #NOTFINAL |
---|
[487] | 999 | @False_ind @(absurd ?? NOTFINAL) |
---|
[708] | 1000 | %{r} @FINAL |
---|
[487] | 1001 | | #F1 #EXEC #F2 whd in EXEC:(??%?); % [ 2: <EXEC @refl ] |
---|
| 1002 | qed. |
---|
[399] | 1003 | |
---|
[487] | 1004 | theorem exec_inf_equivalence: |
---|
[399] | 1005 | ∀classic:(∀P:Prop.P ∨ ¬P). |
---|
[487] | 1006 | ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P). |
---|
[732] | 1007 | ∀p,e. single_exec_of (exec_inf ?? clight_fullexec p) e → |
---|
[399] | 1008 | ∃b.execution_matches_behavior e b ∧ exec_program p b. |
---|
[487] | 1009 | #classic #constructive_indefinite_description #p #e |
---|
| 1010 | whd in ⊢ (?%? → ??(λ_.?(?%?)%)); |
---|
| 1011 | lapply (make_initial_state_sound p); |
---|
| 1012 | lapply (the_initial_state p); |
---|
| 1013 | cases (make_initial_state p); |
---|
| 1014 | [ #gs cases gs; #ge #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?); |
---|
| 1015 | cases INITIAL; #Ege #INITIAL'' |
---|
| 1016 | >(exec_inf_aux_unfold …) |
---|
[708] | 1017 | whd in ⊢ (?%? → ?) |
---|
| 1018 | @is_final_elim |
---|
| 1019 | [ #r #F @False_ind |
---|
[487] | 1020 | @(absurd ?? (initial_state_not_final … INITIAL'')) |
---|
[708] | 1021 | %{r} @F |
---|
[487] | 1022 | | #NOTFINAL whd in ⊢ (?%? → ?); cases e; |
---|
| 1023 | [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #EXEC0 | #o #k #i #e #EXEC0 ] |
---|
| 1024 | cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC' |
---|
| 1025 | lapply (behavior_of_execution ?? |
---|
[399] | 1026 | (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC')); |
---|
[487] | 1027 | *; #b #MATCHES %{b} % //; |
---|
| 1028 | #ge' >Ege #Ege' >(?:ge' = ge) [ 2: destruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ] |
---|
| 1029 | inversion MATCHES; |
---|
| 1030 | [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM |
---|
| 1031 | #TERM |
---|
| 1032 | lapply (exec_state_terminates … TERM); #E1 |
---|
| 1033 | >E1 in TERM #TERM |
---|
| 1034 | @(program_terminates (mk_transrel … step) ?? ge s) |
---|
| 1035 | [ 2: @INITIAL'' |
---|
| 1036 | | 3: @(terminates_sound … TERM EXEC') |
---|
| 1037 | | skip |
---|
| 1038 | | //; |
---|
| 1039 | ] |
---|
| 1040 | | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES #DIVERGES |
---|
| 1041 | lapply (exec_state_diverges … DIVERGES); |
---|
| 1042 | #E1 >E1 in DIVERGES #DIVERGES |
---|
| 1043 | inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6 |
---|
| 1044 | <E4 in INITSTEPS ⊢ % <E5 in E6 ⊢ % #E6 #INITSTEPS |
---|
| 1045 | cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] |
---|
| 1046 | #E7 <E7 in INITSTEPS #INITSTEPS |
---|
| 1047 | cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV |
---|
| 1048 | @(program_diverges (mk_transrel … step) ?? ge s … INITIAL'' INITSTAR) |
---|
| 1049 | @(silent_sound … DIVERGING EXECDIV) |
---|
| 1050 | | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS #REACTS |
---|
| 1051 | lapply (exec_state_reacts … REACTS); |
---|
| 1052 | #E1 >E1 in REACTS #REACTS |
---|
| 1053 | inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5 |
---|
| 1054 | <E4 in REACTING ⊢ % <E5 #REACTING #E6 |
---|
| 1055 | cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] |
---|
| 1056 | #E7 <E7 in REACTING #REACTING |
---|
| 1057 | @(program_reacts (mk_transrel … step) ?? ge s … INITIAL'') |
---|
| 1058 | @(reacts_sound … REACTING EXEC') |
---|
| 1059 | | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG #WRONG |
---|
| 1060 | lapply (exec_state_wrong … WRONG); |
---|
| 1061 | #E1 >E1 in WRONG #WRONG |
---|
| 1062 | inversion WRONG; #tr' #s1' #s2' #e'' #GOESWRONG #E4 #E5 #E6 #E7 |
---|
| 1063 | <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG |
---|
| 1064 | cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ] |
---|
| 1065 | #E8 <E8 in GOESWRONG #GOESWRONG |
---|
| 1066 | elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL |
---|
| 1067 | @(program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP) |
---|
| 1068 | #r % #F @(absurd ?? FINAL) %{r} @F |
---|
| 1069 | | #E destruct (E); |
---|
| 1070 | ] |
---|
| 1071 | ] |
---|
| 1072 | | whd in ⊢ ((∀_.? → %) → ?); |
---|
| 1073 | #NOINIT #_ #EXEC |
---|
| 1074 | %{ (Goes_wrong E0)} % |
---|
| 1075 | [ whd in EXEC:(?%?); |
---|
| 1076 | cases e in EXEC; |
---|
| 1077 | [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #EXEC0 | #o #k #i #e #EXEC0 ] |
---|
| 1078 | cases (se_inv … EXEC0); |
---|
| 1079 | @emb_initially_wrong |
---|
| 1080 | | #ge #Ege |
---|
| 1081 | @program_goes_initially_wrong |
---|
| 1082 | #s % #INIT cases (NOINIT s INIT); #ge' #H @H |
---|
| 1083 | ] |
---|
| 1084 | ] qed. |
---|
[399] | 1085 | |
---|