Changeset 1516 for src/Clight/CexecComplete.ma
- Timestamp:
- Nov 19, 2011, 12:38:20 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/CexecComplete.ma
r1510 r1516 30 30 31 31 lemma yields_eq: ∀A,a,v'. yields A a v' → a = OK ? v'. 32 #A #a #v' cases a; // #m whd in ⊢ (% → ?) *;32 #A #a #v' cases a; // #m whd in ⊢ (% → ?); *; 33 33 qed. 34 34 … … 65 65 inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15 #e16 66 66 inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25 #e26 67 >e11 in e21 #e1 >(?:ge1 = ge2) in e13 e1467 >e11 in e21; #e1 >(?:ge1 = ge2) in e13 e14; 68 68 [ 2: destruct (e1) skip (e11); @refl ] 69 69 #e13 #e14 70 70 71 >e12 in e22 #e2 destruct (e2) skip (e12);72 73 >e13 in e23 #e3 >(?:b1 = b2) in e1471 >e12 in e22; #e2 destruct (e2) skip (e12); 72 73 >e13 in e23; #e3 >(?:b1 = b2) in e14; 74 74 [ >e24 #e4 >(?:f2 = f1) 75 75 [ //; … … 88 88 >e2 89 89 whd in ⊢ (??%?); 90 change in e1:(??%?) with (make_global (mk_program ?? globs fns main))90 change in e1:(??%?); with (make_global (mk_program ?? globs fns main)) 91 91 >e1 92 92 >e3 … … 100 100 #m #v #ty #ty' #v' #H 101 101 elim H; 102 [ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl102 [ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl 103 103 | #m #f #sz #szi #sg @refl 104 | #m #sz #sz' #sg #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl104 | #m #sz #sz' #sg #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl 105 105 | #m #f #sz #sz' @refl 106 106 | #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc' 107 elim H1 in pc ⊢ % [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ]108 whd in ⊢ (??%?) 109 [ 1,2: @(dec_true ? (eq_region_dec r1 r1) (refl ??) …) #H0 whd in ⊢ (??%?) ]107 elim H1 in pc ⊢ %; [ #r1 #ty1 #pc | #r1 #ty1 #n1 #pc | #tys1 #ty1 #pc letin r1 ≝ Code ] 108 whd in ⊢ (??%?); 109 [ 1,2: @(dec_true ? (eq_region_dec r1 r1) (refl ??) …) #H0 whd in ⊢ (??%?); ] 110 110 elim H2 in pc' ⊢ %; [ 1,4,7: #sp2 #ty2 | 2,5,8: #sp2 #ty2 #n2 | 3,6,9: #tys2 #ty2 letin sp2 ≝ Code ] 111 #pc' whd in ⊢ (??%?) 111 #pc' whd in ⊢ (??%?); 112 112 @(dec_true ? (pointer_compat_dec b sp2) pc') // 113 | #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?) 114 >intsize_eq_elim_true whd in ⊢ (??%?) cases sz //;113 | #m #sz #si #ty'' #r #H cases H; [ #s #t | #s #t #n | #tys #ty0 ] whd in ⊢ (??%?); 114 >intsize_eq_elim_true whd in ⊢ (??%?); cases sz //; 115 115 | #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f 116 116 whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl … … 132 132 lemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ? (exec_bool_of_val v ty) b. 133 133 #v #ty #r #H elim H; #v #t #H' elim H'; 134 [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?) >intsize_eq_elim_true134 [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?); >intsize_eq_elim_true 135 135 >(eq_bv_false … ne) // 136 136 | #r #b #pc #i #i0 #s %{ true} % // 137 137 | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //; 138 | #sz #sg %{ false} % // whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //138 | #sz #sg %{ false} % // whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true // 139 139 | #r #r' #t %{ false} % //; 140 140 | #s %{ false} % //; whd; >(Feq_zero_true …) //; … … 144 144 lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true. 145 145 #v #ty #H elim H; 146 [ #i #is #s #ne whd in ⊢ (??%?) >intsize_eq_elim_true >(eq_bv_false … ne) //;146 [ #i #is #s #ne whd in ⊢ (??%?); >intsize_eq_elim_true >(eq_bv_false … ne) //; 147 147 | #p #b #i #i0 #s // 148 148 | #f #s #ne whd; >(Feq_zero_false … ne) //; … … 152 152 lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false. 153 153 #v #ty #H elim H; 154 [ #sz #sg whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //;154 [ #sz #sg whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //; 155 155 | #r #r' #t //; 156 156 | #s whd; >(Feq_zero_true …) //; … … 165 165 (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉)) 166 166 (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉))); 167 [ #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl167 [ #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl 168 168 | #f #ty @refl 169 169 | #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1) 170 170 [ #id | #e' | #e' #id ] #H3 171 whd in ⊢ (??%?) 172 [ change in H3:(??%?) with (exec_lvalue' ge env m (Evar id) ty)173 | change in H3:(??%?) with (exec_lvalue' ge env m (Ederef e') ty)174 | change in H3:(??%?) with (exec_lvalue' ge env m (Efield e' id) ty)171 whd in ⊢ (??%?); 172 [ change in H3:(??%?); with (exec_lvalue' ge env m (Evar id) ty) 173 | change in H3:(??%?); with (exec_lvalue' ge env m (Ederef e') ty) 174 | change in H3:(??%?); with (exec_lvalue' ge env m (Efield e' id) ty) 175 175 ] 176 176 >(yields_eq ??? H3) 177 whd in ⊢ (??%?) change in H2:(??%?)with (load_value_of_type' ty m 〈l,off〉)177 whd in ⊢ (??%?); change in H2:(??%?); with (load_value_of_type' ty m 〈l,off〉) 178 178 >H2 @refl 179 179 | #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?); 180 >(yields_eq ??? H2) whd in ⊢ (??%?) 180 >(yields_eq ??? H2) whd in ⊢ (??%?); 181 181 @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd 182 182 @refl … … 326 326 [ #env'' #m'' % 327 327 | #env1 #m1 #id #ty #l1 #m2 #loc #m3 #env2 #H1 #H2 #H3 328 < H3 whd in H1:(??%?) ⊢ (??%?) 328 < H3 whd in H1:(??%?) ⊢ (??%?); 329 329 < (pair_eq1 ?????? H1) < (pair_eq2 ?????? H1) 330 330 @refl … … 337 337 [ //; 338 338 | #env1 #m1 #id #ty #l #v #tl #loc #m2 #m3 #H1 #H2 #H3 #H4 339 whd in ⊢ (??%?) 339 whd in ⊢ (??%?); 340 340 >H1 whd in ⊢ (??%?); 341 341 >H2 whd in ⊢ (??%?); … … 345 345 lemma eventval_match_complete': ∀ev,ty,v. 346 346 eventval_match ev ty v → yields ? (check_eventval' v ty) ev. 347 #ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl qed.347 #ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl qed. 348 348 349 349 lemma eventval_list_match_complete: ∀vs,tys,evs. … … 351 351 #vs #tys #evs #H elim H; 352 352 [ // 353 | #e #etl #ty #tytl #v #vtl #H1 #H2 #H3 whd in ⊢ (??%?) 354 >(yields_eq ??? (eventval_match_complete' … H1)) whd in ⊢ (??%?) 355 >(yields_eq ??? H3) whd in ⊢ (??%?) //353 | #e #etl #ty #tytl #v #vtl #H1 #H2 #H3 whd in ⊢ (??%?); 354 >(yields_eq ??? (eventval_match_complete' … H1)) whd in ⊢ (??%?); 355 >(yields_eq ??? H3) whd in ⊢ (??%?); // 356 356 ] qed. 357 357 … … 360 360 #ge #s #tr #s' #H elim H; 361 361 [ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?); 362 >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?) 363 >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?) 364 change in H3:(??%?) with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v)362 >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?); 363 >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?); 364 change in H3:(??%?); with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v) 365 365 >H3 @refl 366 366 | #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?); … … 446 446 // 447 447 | #id #tys #rty #args #k #m #rv #tr #H whd in ⊢ (??%?); 448 inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 #e5 <e1 in H1 H2 448 inversion H; #f' #args' #rv' #eargs #erv #H1 #H2 #e1 #e2 #e3 #e4 #e5 <e1 in H1 H2; 449 449 #H1 #H2 450 450 >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?); … … 453 453 | #v #f #env #k #m @refl 454 454 | #v #f #env #k #m1 #m2 #loc #ofs #ty 455 change in ⊢ (??%? → ?) with (store_value_of_type' ty m1 〈loc,ofs〉 v)456 #H whd in ⊢ (??%?) >H @refl455 change in ⊢ (??%? → ?); with (store_value_of_type' ty m1 〈loc,ofs〉 v) 456 #H whd in ⊢ (??%?); >H @refl 457 457 | #f #l #s #k #env #m @refl 458 458 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.