Changeset 961 for src/Clight/CexecComplete.ma
- Timestamp:
- Jun 15, 2011, 4:15:52 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/CexecComplete.ma
r891 r961 100 100 #m #v #ty #ty' #v' #H 101 101 elim H; 102 [ #m # i #sz1 #sz2 #sg1 #sg2@refl102 [ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl 103 103 | #m #f #sz #szi #sg @refl 104 | #m # i #sz #sz' #sg@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' … … 111 111 #pc' whd in ⊢ (??%?) 112 112 @(dec_true ? (pointer_compat_dec b sp2) pc') // 113 | #m #sz #si #ty'' #r #H cases H; //; 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 //; 114 115 | #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f 115 116 whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl … … 131 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. 132 133 #v #ty #r #H elim H; #v #t #H' elim H'; 133 [ #i #is #s #ne %{ true} % //; whd; >(eq_false … ne) //; 134 [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?) >intsize_eq_elim_true 135 >(eq_bv_false … ne) // 134 136 | #r #b #pc #i #i0 #s %{ true} % // 135 137 | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //; 136 | # i #s %{ false} % //;138 | #sz #sg %{ false} % // whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true // 137 139 | #r #r' #t %{ false} % //; 138 140 | #s %{ false} % //; whd; >(Feq_zero_true …) //; … … 142 144 lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true. 143 145 #v #ty #H elim H; 144 [ #i #is #s #ne whd ; >(eq_false … ne) //;146 [ #i #is #s #ne whd in ⊢ (??%?) >intsize_eq_elim_true >(eq_bv_false … ne) //; 145 147 | #p #b #i #i0 #s // 146 148 | #f #s #ne whd; >(Feq_zero_false … ne) //; … … 150 152 lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false. 151 153 #v #ty #H elim H; 152 [ # i #s//;154 [ #sz #sg whd in ⊢ (??%?) >intsize_eq_elim_true >eq_bv_true //; 153 155 | #r #r' #t //; 154 156 | #s whd; >(Feq_zero_true …) //; … … 163 165 (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉)) 164 166 (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉))); 165 [ # i #ty@refl167 [ #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl 166 168 | #f #ty @refl 167 169 | #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1) … … 179 181 @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd 180 182 @refl 181 | #ty' # ty@refl183 | #ty' #sz #sg @refl 182 184 | #op #e #ty #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?); 183 185 >(yields_eq ??? H3) … … 342 344 lemma eventval_match_complete': ∀ev,ty,v. 343 345 eventval_match ev ty v → yields ? (check_eventval' v ty) ev. 344 #ev #ty #v #H elim H; // ;qed.346 #ev #ty #v #H elim H; // #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl qed. 345 347 346 348 lemma eventval_list_match_complete: ∀vs,tys,evs. … … 431 433 | #r #f' #env' #k' #H1 #H2 whd in ⊢ (??%?); >H2 @refl 432 434 ] 433 | #f #e #s #k #env #m # i #tr #H1 whd in ⊢ (??%?);435 | #f #e #s #k #env #m #sz #i #tr #H1 whd in ⊢ (??%?); 434 436 >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?); 435 437 @refl … … 446 448 #H1 #H2 447 449 >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?); 448 whd; inversion H2; #x #sz [ #sg] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);450 whd; inversion H2; [ #sz #sg #x | #x #sz ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?); 449 451 @refl 450 452 | #v #f #env #k #m @refl
Note: See TracChangeset
for help on using the changeset viewer.