Changeset 1510 for src/Clight/CexecEquiv.ma
 Timestamp:
 Nov 16, 2011, 4:38:41 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecEquiv.ma
r1352 r1510 118 118 [ #tr #r #m #E1 #E2 destruct 119 119  #tr #s #e #se #H1 #H2 #E (* destruct (E) ;*) 120 cases (se_step_eq … E) * #E1 #E2 #E3 >E1 >E2 >E3120 cases (se_step_eq … E) * #E1 #E2 #E3 #E4 >E1 >E2 >E3 121 121 >(exec_e_step_inv … H2) 122 122 <(exec_e_step … H2) in H1 #H1 % // … … 133 133  #tr #s #e #se #H1 #H2 #E destruct (E) 134 134  #msg #_ #E destruct 135  #o #k #i #se #H1 #H2 #E destruct (E);135  #o #k #i #se #H1 #H2 #E #X destruct (E); 136 136 lapply (exec_step_sound ge s0); 137 137 cases (exec_step ge s0) in H2 ⊢ %; … … 141 141 inversion H1; 142 142 [ #tr #r #m #E1 #E2 destruct 143  #tr' #s' #e' #se' #H2 #H3 #E2 destruct (E2);143  #tr' #s' #e' #se' #H2 #H3 #E2 #_ destruct (E2); 144 144 <(exec_e_step … H3) in H2 #H2 % [ 2: @H2 ] 145 145 lapply (STEP i); … … 164 164  #tr #s #e #se #H1 #H2 #E destruct (E) 165 165  #msg #_ #E destruct 166  #o #k #i #se #H1 #H2 #E destruct (E);166  #o #k #i #se #H1 #H2 #E #_ destruct (E); 167 167 lapply (exec_step_sound ge s0); 168 168 >(exec_inf_aux_unfold …) in H2; … … 172 172 #STEP 173 173 inversion H1; 174 [ #tr #r #m #E1 #E2 lapply (STEP i); destruct;174 [ #tr #r #m #E1 #E2 #_ lapply (STEP i); destruct; 175 175 >(exec_inf_aux_unfold …) in E1; 176 176 cases (k' i); … … 284 284 whd in EXEC; 285 285 inversion EXEC; 286 [ #tr' #r' #m' #EXEC' #E destruct (E);286 [ #tr' #r' #m' #EXEC' #E #_ destruct (E); 287 287 lapply (exec_step_sound ge s); 288 288 >(exec_inf_aux_unfold …) in EXEC'; … … 294 294  #msg #EXEC' whd in EXEC':(??%??); destruct (EXEC'); 295 295 ] 296 inversion FINAL; #r''' #m' #E1 #E2 # H destruct (E1 E2);296 inversion FINAL; #r''' #m' #E1 #E2 #_ #H destruct (E1 E2); 297 297 @H 298 298  #tr' #s' #e' #se' #H #EXEC' #E destruct … … 321 321 star (mk_transrel … step) ge s tr (Returnstate (Vint I32 r) Kstop m). 322 322 #ge #tr0 #s0 #r #m #e0 #H inversion H; 323 [ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 # EXEC323 [ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC 324 324 destruct (E1 E2 E3 E4 E5); 325 325 cases (several_steps … ESTEPS EXEC); #STARs' #EXECs' … … 329 329  @refl 330 330 ] 331  #s #s' #tr #tr' #r #e #m #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 # EXEC331  #s #s' #tr #tr' #r #e #m #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC 332 332 destruct; 333 333 cases (several_steps … ESTEPS EXEC); #STARs' #EXECs' … … 345 345 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''))); 346 346 [ inversion REACTS; 347 #tr0 #tr' #s0 #s' #e0 #e' #EREACTS #ESTEPS #REACTED #E1 #E2 #E3 destruct (E2 E3);347 #tr0 #tr' #s0 #s' #e0 #e' #EREACTS #ESTEPS #REACTED #E1 #E2 #E3 #_ destruct (E2 E3); 348 348 %{ s'} %{ e'} %{ tr0} %{ tr'} % [ % [ % //;  @REACTED ]  @refl ] 349 349  *; #s' *; #e' *; #tr' *; #tr'' … … 371 371 [ #tr #r #m #EXEC #E destruct (E) 372 372  #tr #s' #e #e' #H #EXEC #E destruct (E) 373  >(exec_inf_aux_unfold …) 373  #msg #EXEC #H #_ generalize in match H H; generalize in match EXEC EXEC; 374 generalize in match msg msg; >(exec_inf_aux_unfold …) 374 375 cases (exec_step ge s); 375 376 [ #o #k #msg' #EXEC whd in EXEC:(??%??); destruct … … 386 387 #ge #s #tr #s' #e #H whd in H; inversion H; 387 388 [ #tr' #r #m #EXEC #E destruct 388  #tr' #s'' #e' #e'' #H #EXEC #E destruct (E);389  #tr' #s'' #e' #e'' #H #EXEC #E #_ destruct (E); 389 390 >(exec_inf_aux_unfold …) in EXEC; 390 391 cases (exec_step ge s); … … 407 408  #tr' #s'' #e' #e'' #H #EXEC #E destruct (E); 408 409  #msg #EXEC #E destruct 409  #o' #k' #i' #e' #H #EXEC #E destruct;410  #o' #k' #i' #e' #H #EXEC #E #_ destruct; 410 411 >(exec_inf_aux_unfold …) in EXEC; 411 412 cases (exec_step ge s); … … 413 414 inversion H; 414 415 [ #tr1 #r1 #m1 #EXECK #E destruct (E); 415  #tr1 #s1 #e1 #e2 #H1 #EXECK #E destruct (E);416  #tr1 #s1 #e1 #e2 #H1 #EXECK #E #_ destruct (E); 416 417 >(exec_inf_aux_unfold …) in EXECK; 417 418 cases (k1 i'); … … 443 444 (¬∃r. final_state s' r). 444 445 #ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG; 445 #tr #s #s' #e #msg #ESTEPS #E1 #E2 #E3 #E4 # EXEC #NOTFINAL destruct (E1 E2 E3 E4);446 #tr #s #s' #e #msg #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC #NOTFINAL destruct (E1 E2 E3 E4); 446 447 cases (several_steps … ESTEPS EXEC); 447 448 #STAR #EXEC' % … … 821 822 #NOTOVER inversion NOTOVER; 822 823 [ #tr' #s' #e' #E destruct (E); 823  #o' #k' #tr' #s' #e' #i' #E destruct (E);824  #o' #k' #tr' #s' #e' #i' #E #_ destruct (E); 824 825 %{ tr'} %{s'} %{e'} % //; 825 826 cases (several_steps … INITIAL EXEC); #_ #EXEC1 … … 934 935 execution_terminates tr s (se_step tr' s' e) r m → s = s'. 935 936 #tr #tr' #s #s' #e #r #m #H inversion H; 936 [ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl937  #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl937 [ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl 938  #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl 938 939 ] qed. 939 940 … … 941 942 execution_diverges tr s (se_step tr' s' e) → s = s'. 942 943 #tr #tr' #s #s' #e #H inversion H; 943 #tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 destruct; @refl qed.944 #tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed. 944 945 945 946 lemma exec_state_reacts: ∀tr,tr',s,s',e. 946 947 execution_reacts tr s (se_step tr' s' e) → s = s'. 947 948 #tr #tr' #s #s' #e #H inversion H; 948 #tr1 #s1 #e1 #H' #E1 #E2 #E3 destruct; @refl qed.949 #tr1 #s1 #e1 #H' #E1 #E2 #E3 #_ destruct; @refl qed. 949 950 950 951 lemma exec_state_wrong: ∀tr,tr',s,s',s'',e. 951 952 execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'. 952 953 #tr #tr' #s #s' #s'' #e #H inversion H; 953 #tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 destruct; @refl qed.954 #tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed. 954 955 955 956 lemma behavior_of_execution: ∀s,e. … … 1022 1023 #TERM 1023 1024 lapply (exec_state_terminates … TERM); #E1 1024 >E1 in TERM #TERM 1025 >E1 in TERM #TERM #_ 1025 1026 @(program_terminates (mk_transrel … step) ?? ge s) 1026 1027 [ 2: @INITIAL … … 1031 1032  #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES #DIVERGES 1032 1033 lapply (exec_state_diverges … DIVERGES); 1033 #E1 >E1 in DIVERGES #DIVERGES 1034 #E1 >E1 in DIVERGES #DIVERGES #_ 1034 1035 inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6 1035 1036 <E4 in INITSTEPS ⊢ % <E5 in E6 ⊢ % #E6 #INITSTEPS 1036 1037 cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] 1037 1038 #E7 <E7 in INITSTEPS #INITSTEPS 1038 cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV 1039 cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV #_ 1039 1040 @(program_diverges (mk_transrel … step) ?? ge s … INITIAL) 1040 1041 [ 2: <Ege @INITSTAR … … 1043 1044  #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS #REACTS 1044 1045 lapply (exec_state_reacts … REACTS); 1045 #E1 >E1 in REACTS #REACTS 1046 #E1 >E1 in REACTS #REACTS #_ 1046 1047 inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5 1047 1048 <E4 in REACTING ⊢ % <E5 #REACTING #E6 1048 1049 cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] 1049 #E7 <E7 in REACTING #REACTING 1050 #E7 <E7 in REACTING #REACTING #_ 1050 1051 @(program_reacts (mk_transrel … step) ?? ge s … INITIAL) 1051 1052 <Ege @(reacts_sound … REACTING EXEC') 1052 1053  #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG #WRONG 1053 1054 lapply (exec_state_wrong … WRONG); 1054 #E1 >E1 in WRONG #WRONG 1055 #E1 >E1 in WRONG #WRONG #_ 1055 1056 inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7 1056 1057 <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG … … 1058 1059 #E8 <E8 in GOESWRONG #GOESWRONG 1059 1060 elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL 1060 <Ege 1061 <Ege #_ 1061 1062 @(program_goes_wrong (mk_transrel … step) ?? ? s … INITIAL STAR STOP) 1062 1063 #r % #F @(absurd ?? FINAL) %{r} @F
Note: See TracChangeset
for help on using the changeset viewer.