Changeset 1344 for src/Clight/CexecEquiv.ma
- Timestamp:
- Oct 10, 2011, 5:47:15 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/CexecEquiv.ma
r1244 r1344 136 136 cases (exec_step ge s0) in H2 ⊢ %; 137 137 [ #o' #k' >(exec_inf_aux_unfold …) 138 #E' whd in E':(??%? ); destruct (E');138 #E' whd in E':(??%??); destruct (E'); 139 139 #STEP 140 140 inversion H1; … … 149 149 ] 150 150 | #x cases x; #tr' #s' >(exec_inf_aux_unfold …) 151 whd in ⊢ (??%? → ?); @is_final_elim'152 [ #r ] #F #E whd in E:(??%? ); destruct151 whd in ⊢ (??%?? → ?); @is_final_elim' 152 [ #r ] #F #E whd in E:(??%??); destruct 153 153 | #msg >(exec_inf_aux_unfold …) 154 #E' whd in E':(??%? ); destruct (E');154 #E' whd in E':(??%??); destruct (E'); 155 155 ] 156 156 ] qed. … … 168 168 cases (exec_step ge s0); 169 169 [ #o' #k' 170 #E' whd in E':(??%? ); destruct (E');170 #E' whd in E':(??%??); destruct (E'); 171 171 #STEP 172 172 inversion H1; … … 174 174 >(exec_inf_aux_unfold …) in E1; 175 175 cases (k' i); 176 [ #o2 #k2 #E whd in E:(??%? ); destruct (E)177 | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);176 [ #o2 #k2 #E whd in E:(??%??); destruct (E) 177 | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?); 178 178 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%) 179 179 @IFE 180 [ #r' #FINAL #E whd in E:(??%? );180 [ #r' #FINAL #E whd in E:(??%??); 181 181 destruct (E); 182 182 inversion FINAL; 183 183 #r'' #m'' #E1 #E2 destruct (E1 E2); //; 184 | #NF #E whd in E:(??%? ); destruct (E)184 | #NF #E whd in E:(??%??); destruct (E) 185 185 ] 186 | #msg #E whd in E:(??%? ); destruct (E)186 | #msg #E whd in E:(??%??); destruct (E) 187 187 ] 188 188 | #tr #s #e #e' #H #EXEC #E destruct (E) … … 190 190 | #o2 #k2 #i2 #e2 #H #EXEC #E destruct (E) 191 191 ] 192 | #x cases x; #tr #s whd in ⊢ (??%? → ?);193 @is_final_elim' [ #r ] #F #E whd in E:(??%? ); destruct (E)194 | #msg #E whd in E:(??%? ); destruct (E)192 | #x cases x; #tr #s whd in ⊢ (??%?? → ?); 193 @is_final_elim' [ #r ] #F #E whd in E:(??%??); destruct (E) 194 | #msg #E whd in E:(??%??); destruct (E) 195 195 ] 196 196 ] qed. … … 286 286 >(exec_inf_aux_unfold …) in EXEC'; 287 287 cases (exec_step ge s); 288 [ #o #k #EXEC' whd in EXEC':(??%? ); destruct (EXEC');289 | #x cases x; #tr'' #s' whd in ⊢ (??%? → ?);288 [ #o #k #EXEC' whd in EXEC':(??%??); destruct (EXEC'); 289 | #x cases x; #tr'' #s' whd in ⊢ (??%?? → ?); 290 290 @is_final_elim' [ #r'' #FINAL | #F ] 291 #EXEC' whd in EXEC':(??%? ); destruct (EXEC');292 | #msg #EXEC' whd in EXEC':(??%? ); destruct (EXEC');291 #EXEC' whd in EXEC':(??%??); destruct (EXEC'); 292 | #msg #EXEC' whd in EXEC':(??%??); destruct (EXEC'); 293 293 ] 294 294 inversion FINAL; #r''' #m' #E1 #E2 #H destruct (E1 E2); … … 371 371 | >(exec_inf_aux_unfold …) 372 372 cases (exec_step ge s); 373 [ #o #k #msg' #EXEC whd in EXEC:(??%? ); destruct374 | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim'375 [ #r ] #F #EXEC whd in EXEC:(??%? ); destruct376 | #msg1 #msg2 #EXEC #E whd in EXEC:(??%? ); destruct @refl373 [ #o #k #msg' #EXEC whd in EXEC:(??%??); destruct 374 | #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?) @is_final_elim' 375 [ #r ] #F #EXEC whd in EXEC:(??%??); destruct 376 | #msg1 #msg2 #EXEC #E whd in EXEC:(??%??); destruct @refl 377 377 ] 378 378 | #o #k #i #e #H #EXEC #E destruct … … 387 387 >(exec_inf_aux_unfold …) in EXEC; 388 388 cases (exec_step ge s); 389 [ #o #k #EXEC whd in EXEC:(??%? ); destruct390 | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim'391 [ #r ] #F #E whd in E:(??%? ); destruct @F392 | #msg #E whd in E:(??%? ); destruct389 [ #o #k #EXEC whd in EXEC:(??%??); destruct 390 | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?) @is_final_elim' 391 [ #r ] #F #E whd in E:(??%??); destruct @F 392 | #msg #E whd in E:(??%??); destruct 393 393 ] 394 394 | #msg #EXEC #E destruct … … 408 408 >(exec_inf_aux_unfold …) in EXEC; 409 409 cases (exec_step ge s); 410 [ #o1 #k1 #EXEC1 whd in EXEC1:(??%? ); destruct (EXEC1);410 [ #o1 #k1 #EXEC1 whd in EXEC1:(??%??); destruct (EXEC1); 411 411 inversion H; 412 412 [ #tr1 #r1 #m1 #EXECK #E destruct (E); … … 414 414 >(exec_inf_aux_unfold …) in EXECK; 415 415 cases (k1 i'); 416 [ #o2 #k2 #EXECK whd in EXECK:(??%? ); destruct417 | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);416 [ #o2 #k2 #EXECK whd in EXECK:(??%??); destruct 417 | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?); 418 418 lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%) 419 419 @IFE [ #r ] #F #EXECK 420 whd in EXECK:(??%? ); destruct;420 whd in EXECK:(??%??); destruct; 421 421 @(absurd ?? F) 422 422 %{ r'} //; 423 | #msg #E whd in E:(??%? ); destruct423 | #msg #E whd in E:(??%??); destruct 424 424 ] 425 | #msg #EXECK #E whd in E:(??%? ); destruct425 | #msg #EXECK #E whd in E:(??%??); destruct 426 426 | #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct 427 427 ] 428 | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?);429 @is_final_elim' [ #r ] #F #E whd in E:(??%? ); destruct;430 | #msg #E whd in E:(??%? ); destruct428 | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?); 429 @is_final_elim' [ #r ] #F #E whd in E:(??%??); destruct; 430 | #msg #E whd in E:(??%??); destruct 431 431 ] 432 432 ] qed. … … 659 659 @isteps_interact //; 660 660 ] qed. 661 662 (* XXX == > jmeq notation and coercion *)663 664 lemma jmeq_to_eq : ∀A:Type[0].∀a,b:A.jmeq A a A b → a = b.665 #A #a #b #E @gral @jm_to_eq_sigma @E666 qed.667 668 coercion jmeq_to_eq : ∀A:Type[0].∀a,b:A.∀p:jmeq A a A b.a = b ≝669 jmeq_to_eq on _p: jmeq ???? to eq ???.670 671 notation > "hvbox(a break ≃ b)"672 non associative with precedence 45673 for @{ 'jmeq ? $a ? $b }.674 675 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"676 non associative with precedence 45677 for @{ 'jmeq $t $a $u $b }.678 679 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).680 681 (* XXX < == *)682 661 683 662 lemma se_inv: ∀e1,e2.
Note: See TracChangeset
for help on using the changeset viewer.