Changeset 1516 for src/Clight/CexecEquiv.ma
 Timestamp:
 Nov 19, 2011, 12:38:20 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecEquiv.ma
r1510 r1516 55 55 P (is_final s). 56 56 #s #P #F #NF lapply (refl ? (is_final s)) 57 cases (is_final s) in ⊢ (???% → %) 58 [ #E @NF % * #r #H whd in E:(??%?) > (is_final_complete … H) in E#H destruct57 cases (is_final s) in ⊢ (???% → %); 58 [ #E @NF % * #r #H whd in E:(??%?); > (is_final_complete … H) in E; #H destruct 59 59  #r #E @F @is_final_sound @E 60 60 ] qed. … … 72 72 >(exec_inf_aux_unfold …) cases x; 73 73 [ #o #k #EXEC whd in EXEC:(??%?); destruct 74  #y cases y #tr' #s' whd in ⊢ (??%? → ?) 74  #y cases y #tr' #s' whd in ⊢ (??%? → ?); 75 75 @is_final_elim' 76 76 [ #r #FINAL  #FINAL ] … … 98 98 >(exec_inf_aux_unfold …) cases x; 99 99 [ #o #k #EXEC whd in EXEC:(??%?); destruct 100  #y cases y; #tr' #s' whd in ⊢ (??%? → ?) 100  #y cases y; #tr' #s' whd in ⊢ (??%? → ?); 101 101 @is_final_elim' [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F 102 102  #msg #EXEC whd in EXEC:(??%?); destruct … … 120 120 cases (se_step_eq … E) * #E1 #E2 #E3 #E4 >E1 >E2 >E3 121 121 >(exec_e_step_inv … H2) 122 <(exec_e_step … H2) in H1 #H1 % //122 <(exec_e_step … H2) in H1; #H1 % // 123 123  #msg #_ #E destruct 124 124  #o #k #i #se #H1 #H2 #E destruct … … 142 142 [ #tr #r #m #E1 #E2 destruct 143 143  #tr' #s' #e' #se' #H2 #H3 #E2 #_ destruct (E2); 144 <(exec_e_step … H3) in H2 #H2 % [ 2: @H2 ]144 <(exec_e_step … H3) in H2; #H2 % [ 2: @H2 ] 145 145 lapply (STEP i); 146 146 >(exec_e_step_inv … H3) … … 178 178  #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?); 179 179 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%); 180 change in match (is_final ?????) with (is_final s2)180 change in match (is_final ?????); with (is_final s2) 181 181 @IFE 182 182 [ #r' #FINAL #E whd in E:(??%??); … … 371 371 [ #tr #r #m #EXEC #E destruct (E) 372 372  #tr #s' #e #e' #H #EXEC #E destruct (E) 373  #msg #EXEC #H #_ generalize in match H H; generalize in match EXECEXEC;374 generalize in match msg msg; >(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 …) 375 375 cases (exec_step ge s); 376 376 [ #o #k #msg' #EXEC whd in EXEC:(??%??); destruct 377  #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?) @is_final_elim'377  #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?); @is_final_elim' 378 378 [ #r ] #F #EXEC whd in EXEC:(??%??); destruct 379 379  #msg1 #msg2 #EXEC #E whd in EXEC:(??%??); destruct @refl … … 391 391 cases (exec_step ge s); 392 392 [ #o #k #EXEC whd in EXEC:(??%??); destruct 393  #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?) @is_final_elim'393  #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?); @is_final_elim' 394 394 [ #r ] #F #E whd in E:(??%??); destruct @F 395 395  #msg #E whd in E:(??%??); destruct … … 420 420  #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?); 421 421 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%); 422 change in match (is_final ?????) with (is_final s2)422 change in match (is_final ?????); with (is_final s2) 423 423 @IFE [ #r ] #F #EXECK 424 424 whd in EXECK:(??%??); destruct; … … 535 535  #f #args #kk #m cases f; 536 536 [ #f' whd in ⊢ (???%); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f')) 537 #x1 #x2 whd in ⊢ (???%) @err_does_not_interact //537 #x1 #x2 whd in ⊢ (???%); @err_does_not_interact // 538 538 (* This is the only case that actually matters! *) 539 539  #fn #argtys #rty whd in ⊢ (???%); … … 637 637 [ #tr #i #m #_ #_ #_ #ENO elim (eno_stop … ENO); 638 638  #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?); 639 [ <(E0_right tr) in ⊢ (?%????) 639 [ <(E0_right tr) in ⊢ (?%????); 640 640 @isteps_one @isteps_none 641 641  #TR @(match sym_eq ??? TR with [ refl ⇒ ? ]) (* >TR in UNREACTIVE ⊢ % *) … … 643 643 @(show_divergence s') 644 644 [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1) 645 change in ⊢ (?%????) with (Eapp E0 tr1); @isteps_one645 change in ⊢ (?%????); with (Eapp E0 tr1); @isteps_one 646 646 @S 647  #tr2 #s2 #e2 #S >TR in UNREACTIVE #UNREACTIVE @(UNREACTIVE tr2 s2 e2)648 change in ⊢ (?%????) with (Eapp E0 tr2);647  #tr2 #s2 #e2 #S >TR in UNREACTIVE; #UNREACTIVE @(UNREACTIVE tr2 s2 e2) 648 change in ⊢ (?%????); with (Eapp E0 tr2); 649 649 @isteps_one @S 650 650  #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i) 651 change in ⊢ (?%????) with (Eapp E0 tr2);651 change in ⊢ (?%????); with (Eapp E0 tr2); 652 652 @(isteps_one … S) 653 653 ] … … 659 659 @False_ind @(absurd ?? NOTSILENT) 660 660 @(UNREACTIVE … s' e') 661 <(E0_right tr') in ⊢ (?%????) 661 <(E0_right tr') in ⊢ (?%????); 662 662 >EXEC 663 663 @isteps_interact //; … … 689 689 *; #E1 #E2 #H1 destruct (E1); 690 690 lapply (H i); *; #tr' *; #s'' *; #K' #TR 691 >E2 in H1 #H1 whd in H1:(?%?); >K' in H1691 >E2 in H1; #H1 whd in H1:(?%?); >K' in H1; 692 692 >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?); 693 change in match (is_final ?????) with (is_final s'')693 change in match (is_final ?????); with (is_final s'') 694 694 @is_final_elim 695 695 [ #r #F whd in ⊢ (?%? → ?); #S … … 698 698 *; #E1 #E2 #S' <E1 @TR 699 699 ] 700  #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?) 700  #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?); 701 701 @is_final_elim' [ #r ] #F #E whd in E:(?%?); 702 702 inversion E; … … 885 885 [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H; 886 886 cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2; 887 cases (H i); #tr1 *; #s1 *; #K #E >K in H2 887 cases (H i); #tr1 *; #s1 *; #K #E >K in H2; 888 888 >(exec_inf_aux_unfold …) 889 whd in ⊢ (?%? → ?) @is_final_elim [ #r ]889 whd in ⊢ (?%? → ?); @is_final_elim [ #r ] 890 890 #F #S whd in S:(?%?); cases (se_inv … S); 891  #x cases x; #tr' #s' whd in ⊢ (?%? → ?) 891  #x cases x; #tr' #s' whd in ⊢ (?%? → ?); 892 892 @is_final_elim' [ #r ] #F #S whd in S:(?%?); 893 893 cases (se_inv … S); … … 902 902 [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H; 903 903 cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2; 904 cases (H i); #tr1 *; #s1 *; #K #E >K in H2 904 cases (H i); #tr1 *; #s1 *; #K #E >K in H2; 905 905 >(exec_inf_aux_unfold …) 906 whd in ⊢ (?%? → ?) @is_final_elim [ #r ]906 whd in ⊢ (?%? → ?); @is_final_elim [ #r ] 907 907 #F #S whd in S:(?%?); cases (se_inv … S); 908  #x cases x; #tr' #s' whd in ⊢ (?%? → ?) 908  #x cases x; #tr' #s' whd in ⊢ (?%? → ?); 909 909 @is_final_elim' [ #r ] #F #S whd in S:(?%?); 910 910 cases (se_inv … S); … … 987 987 ∃e'.e = e_step ??? E0 s e'. 988 988 #ge #s #e >(exec_inf_aux_unfold …) 989 whd in ⊢ (??%? → ?) @is_final_elim'989 whd in ⊢ (??%? → ?); @is_final_elim' 990 990 [ #r #FINAL #EXEC #NOTFINAL 991 991 @False_ind @(absurd ?? NOTFINAL) … … 1003 1003 lapply (make_initial_state_sound p) 1004 1004 lapply (the_initial_state p) 1005 whd in ⊢ (? → ? → ?(match % with [_ ⇒ ?  _ ⇒ ?])? → ?) 1005 whd in ⊢ (? → ? → ?(match % with [_ ⇒ ?  _ ⇒ ?])? → ?); 1006 1006 cases (make_initial_state p) 1007 1007 [ #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?); 1008 1008 >exec_inf_aux_unfold 1009 whd in ⊢ (?%? → ?) 1009 whd in ⊢ (?%? → ?); 1010 1010 @is_final_elim' 1011 1011 [ #r #F @False_ind … … 1020 1020 #ge #Ege 1021 1021 inversion MATCHES; 1022 [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM 1022 [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM; 1023 1023 #TERM 1024 1024 lapply (exec_state_terminates … TERM); #E1 1025 >E1 in TERM #TERM #_1025 >E1 in TERM; #TERM #_ 1026 1026 @(program_terminates (mk_transrel … step) ?? ge s) 1027 1027 [ 2: @INITIAL … … 1030 1030  //; 1031 1031 ] 1032  #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES #DIVERGES1032  #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES; #DIVERGES 1033 1033 lapply (exec_state_diverges … DIVERGES); 1034 #E1 >E1 in DIVERGES #DIVERGES #_1034 #E1 >E1 in DIVERGES; #DIVERGES #_ 1035 1035 inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6 1036 <E4 in INITSTEPS ⊢ % <E5 in E6 ⊢ %#E6 #INITSTEPS1036 <E4 in INITSTEPS ⊢ %; <E5 in E6 ⊢ %; #E6 #INITSTEPS 1037 1037 cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] 1038 #E7 <E7 in INITSTEPS #INITSTEPS1038 #E7 <E7 in INITSTEPS; #INITSTEPS 1039 1039 cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV #_ 1040 1040 @(program_diverges (mk_transrel … step) ?? ge s … INITIAL) … … 1042 1042  3: <Ege @(silent_sound … DIVERGING EXECDIV) 1043 1043 ] 1044  #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS #REACTS1044  #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS; #REACTS 1045 1045 lapply (exec_state_reacts … REACTS); 1046 #E1 >E1 in REACTS #REACTS #_1046 #E1 >E1 in REACTS; #REACTS #_ 1047 1047 inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5 1048 <E4 in REACTING ⊢ % <E5 #REACTING #E61048 <E4 in REACTING ⊢ %; <E5 #REACTING #E6 1049 1049 cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ] 1050 #E7 <E7 in REACTING #REACTING #_1050 #E7 <E7 in REACTING; #REACTING #_ 1051 1051 @(program_reacts (mk_transrel … step) ?? ge s … INITIAL) 1052 1052 <Ege @(reacts_sound … REACTING EXEC') 1053  #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG #WRONG1053  #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG; #WRONG 1054 1054 lapply (exec_state_wrong … WRONG); 1055 #E1 >E1 in WRONG #WRONG #_1055 #E1 >E1 in WRONG; #WRONG #_ 1056 1056 inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7 1057 <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG1057 <E4 in GOESWRONG ⊢ %; <E5 <E7 #GOESWRONG 1058 1058 cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ] 1059 #E8 <E8 in GOESWRONG #GOESWRONG1059 #E8 <E8 in GOESWRONG; #GOESWRONG 1060 1060 elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL 1061 1061 <Ege #_
Note: See TracChangeset
for help on using the changeset viewer.