Changeset 702 for src/Clight/CexecEquiv.ma
 Timestamp:
 Mar 21, 2011, 6:27:22 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecEquiv.ma
r700 r702 49 49 ] qed. 50 50 51 lemma exec_e_step: ∀p,ge,x,tr,s,e. 52 exec_inf_aux (clight_exec p) ge x = e_step ??? tr s e → 53 exec_inf_aux (clight_exec p) ge (exec_step ge s) = e. 54 #p #ge #x #tr #s #e 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 ?)) → 54 P (is_final clight_exec s). 55 #s #P #F #NF whd in ⊢ (?%) cases (is_final_state s) 56 [ * #r #FINAL @F @FINAL 57  #NOTFINAL @NF @NOTFINAL 58 ] qed. 59 60 lemma exec_e_step: ∀ge,x,tr,s,e. 61 exec_inf_aux clight_exec ge x = e_step ??? tr s e → 62 exec_inf_aux clight_exec ge (exec_step ge s) = e. 63 #ge #x #tr #s #e 55 64 >(exec_inf_aux_unfold …) cases x; 56 65 [ #o #k #EXEC whd in EXEC:(??%?); destruct 57  #y cases y; #tr' #s' whd in ⊢ (??%? → ?); >(?:? (clight_exec p) s' = is_final s'); whd in match (? (clight_exec) s') in ⊢ %; whd in ⊢ (??%? → ?); 58 cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct; 59 @refl 66  #y cases y; #tr' #s' whd in ⊢ (??%? → ?) 67 @is_final_elim 68 [ #r #FINAL  #FINAL ] 69 (* Some trickery to prevent destruct normalizing clight_exec *) 70 #EXEC whd in EXEC:(??%?); [ @False_ind destruct  71 cut (s = s') [ generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #E destruct @refl ] 72 #Es <Es in EXEC #EXEC 73 generalize in EXEC:(??(??????%)?) ⊢ (??%?) 74 #e0 #E destruct @refl 75 ] 60 76  #EXEC whd in EXEC:(??%?); destruct 61 77 ] qed. 62 78 63 79 lemma exec_e_step_inv: ∀ge,x,tr,s,e. 64 exec_inf_aux ge x = e_steptr s e →80 exec_inf_aux clight_exec ge x = e_step ??? tr s e → 65 81 x = Value ??? 〈tr,s〉. 66 82 #ge #x #tr #s #e … … 68 84 [ #o #k #EXEC whd in EXEC:(??%?); destruct 69 85  #y cases y; #tr' #s' whd in ⊢ (??%? → ?); 70 cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct; 86 @is_final_elim 87 [ #r ] #FINAL #EXEC whd in EXEC:(??%?) 88 (* Again, prevent destruct blowing up *) 89 [ 2: generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #EXEC ] 90 destruct; 71 91 @refl 72 92  #EXEC whd in EXEC:(??%?); destruct … … 74 94 75 95 lemma exec_e_step_inv2: ∀ge,x,tr,s,e. 76 exec_inf_aux ge x = e_steptr s e →96 exec_inf_aux clight_exec ge x = e_step ??? tr s e → 77 97 ¬∃r.final_state s r. 78 98 #ge #x #tr #s #e 79 99 >(exec_inf_aux_unfold …) cases x; 80 100 [ #o #k #EXEC whd in EXEC:(??%?); destruct 81  #y cases y; #tr' #s' whd in ⊢ (??%? → ?) ;82 cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;83 @FINAL101  #y cases y; #tr' #s' whd in ⊢ (??%? → ?) 102 @is_final_elim [ #r #F #EXEC whd in EXEC:(??%?); destruct 103  #F whd in ⊢ (??%? → ?) generalize in ⊢ (??(??????%)? → ?) #e0 #EXEC destruct @F ] 84 104  #EXEC whd in EXEC:(??%?); destruct 85 105 ] qed. 86 106 87 107 definition exec_from : genv → state → s_execution → Prop ≝ 88 λge,s,se. single_exec_of (exec_inf_aux ge (exec_step ge s)) se. 108 λge,s,se. single_exec_of (exec_inf_aux clight_exec ge (exec_step ge s)) se. 109 110 lemma se_step_eq : ∀tr,s,e,tr',s',e'. 111 se_step tr s e = se_step tr' s' e' → 112 tr = tr' ∧ s = s' ∧ e = e'. 113 #tr #s #e #tr' #s' #e' #E 114 (* destruct This takes a hideous amount of time, not sure why. *) 115 @(match E return λl.λ_. match l with [ se_step tr0 s0 e0 ⇒ tr = tr0 ∧ s = s0 ∧ e = e0  _ ⇒ False ] with [ refl ⇒ ? ]) 116 whd % try % @refl qed. 89 117 90 118 lemma exec_from_step : ∀ge,s,tr,s',e. … … 93 121 #ge #s0 #tr0 #s0' #e0 #H inversion H; 94 122 [ #tr #r #m #E1 #E2 destruct 95  #tr #s #e #se #H1 #H2 #E destruct (E); 123  #tr #s #e #se #H1 #H2 #E (*destruct (E);*) 124 lapply (se_step_eq … E) * * #E1 #E2 #E3 >E1 >E2 >E3 96 125 >(exec_e_step_inv … H2) 97 126 <(exec_e_step … H2) in H1 #H1 % // … … 100 129 ] qed. 101 130 102 lemmaexec_from_interact : ∀ge,s,o,k,i,tr,s',e.131 axiom exec_from_interact : ∀ge,s,o,k,i,tr,s',e. 103 132 exec_from ge s (se_interact o k i (se_step tr s' e)) → 104 133 step ge s tr s' ∧ 105 134 (*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e. 135 (* 106 136 #ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H; 107 137 [ #tr #r #m #E1 #E2 destruct 108 138  #tr #s #e #se #H1 #H2 #E destruct (E) 109 139  #_ #E destruct 110  #o #k #i #se #H1 #H2 #E destruct (E);140  #o #k #i #se #H1 #H2 #E (*destruct (E);*) 111 141 lapply (exec_step_sound ge s0); 112 142 cases (exec_step ge s0) in H2 ⊢ %; … … 130 160 #E' whd in E':(??%?); destruct (E'); 131 161 ] 132 ] qed. 133 134 lemmaexec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.162 ] qed.*) 163 164 axiom exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m. 135 165 exec_from ge s (se_interact o k i (se_stop tr r m)) → 136 166 step ge s tr (Returnstate (Vint r) Kstop m). 167 (* 137 168 #ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H; 138 169 [ #tr #r #m #E1 #E2 destruct … … 169 200  #E whd in E:(??%?); destruct (E) 170 201 ] 171 ] qed. 202 ] qed.*) 172 203 173 204 (* NB: the E0 in the execs are irrelevant. *) … … 251 282 ] qed. 252 283 253 lemmafinal_step: ∀ge,tr,r,m,s.284 axiom final_step: ∀ge,tr,r,m,s. 254 285 exec_from ge s (se_stop tr r m) → 255 286 step ge s tr (Returnstate (Vint r) Kstop m). 287 (* 256 288 #ge #tr #r #m #s #EXEC 257 289 whd in EXEC; … … 272 304  #EXEC' #E destruct 273 305  #o #k #i #e #H #EXEC #E destruct 274 ] qed. 306 ] qed.*) 275 307 276 308 277 309 lemma e_stop_inv: ∀ge,x,tr,r,m. 278 exec_inf_aux ge x = e_stoptr r m →310 exec_inf_aux clight_exec ge x = e_stop ??? tr r m → 279 311 x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉. 280 312 #ge #x #tr #r #m 281 313 >(exec_inf_aux_unfold …) cases x; 282 314 [ #o #k #EXEC whd in EXEC:(??%?); destruct; 283  #z cases z; #tr' #s' whd in ⊢ (??%? → ?); cases (is_final_state s');284 [ # F cases F; #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);315  #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim 316 [ #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?); 285 317 destruct (EXEC); @refl 286 318  #F #EXEC whd in EXEC:(??%?); destruct (EXEC); … … 347 379 cases (exec_step ge s); 348 380 [ #o #k #EXEC whd in EXEC:(??%?); destruct 349  #x cases x; #tr #s' whd in ⊢ (??%? → ?) ; cases (is_final_state s');350 #F #EXEC whd in EXEC:(??%?); destruct381  #x cases x; #tr #s' whd in ⊢ (??%? → ?) @is_final_elim 382 [ #r ] #F #EXEC whd in EXEC:(??%?); destruct 351 383  // 352 384 ] … … 363 395 cases (exec_step ge s); 364 396 [ #o #k #EXEC whd in EXEC:(??%?); destruct 365  #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) ; cases (is_final_state s1);366 #F #E whd in E:(??%?); destruct; @F397  #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim 398 [ #r ] #F #E whd in E:(??%?); [ destruct  generalize in E:(??(??????%)?) ⊢ ? #e0 #E destruct; @F ] 367 399  #E whd in E:(??%?); destruct 368 400 ]
Note: See TracChangeset
for help on using the changeset viewer.