Changeset 2176 for src/Clight/CexecComplete.ma
 Timestamp:
 Jul 12, 2012, 1:28:28 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecComplete.ma
r2120 r2176 39 39 ] qed. 40 40 41 (* 41 42 lemma is_pointer_compat_true: ∀b,sp. 42 43 pointer_compat b sp → … … 46 47 [ // 47 48  #H' @False_ind @(absurd … H H') 48 ] qed. 49 ] qed.*) 49 50 50 51 theorem is_det: ∀p,s,s'. … … 92 93  #m #sz #sz' #sg #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl 93 94  #m #f #sz #sz' @refl 95  #m #ty0 #ty0' #ptr #H1 #H2 cases H1 cases H2 // 96  #m #sz #sg #ty' #H' cases H' [ #ty''  #ty'' #n  #tys #ty'' ] whd in ⊢ (??%?); 97 >intsize_eq_elim_true whd in ⊢ (??%?); cases sz // 98  #m #ty0 #ty0' #H1 #H2 cases H1 cases H2 // 99 (* 94 100  #m #ty #ty' * #r #b #pc #ofs #r' #H1 #H2 #pc' 95 101 elim H1 in pc ⊢ %; [ #r1 #ty1 #pc  #r1 #ty1 #n1 #pc  #tys1 #ty1 #pc letin r1 ≝ Code ] … … 103 109  #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f 104 110 whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl 111 *) 105 112 ] qed. 106 113 … … 122 129 [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?); >intsize_eq_elim_true 123 130 >(eq_bv_false … ne) // 124  * #r #b #pc #i #i0 #s%{ true} % //131  * #b #i #i0 %{ true} % // 125 132  #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //; 126 133  #sz #sg %{ false} % // whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true // 127  #r #r'#t %{ false} % //;134  #t %{ false} % //; 128 135  #s %{ false} % //; whd; >(Feq_zero_true …) //; 129 136 ] … … 133 140 #v #ty #H elim H; 134 141 [ #i #is #s #ne whd in ⊢ (??%?); >intsize_eq_elim_true >(eq_bv_false … ne) //; 135  * #p #b #i #i0#s //142  #s // 136 143  #f #s #ne whd; >(Feq_zero_false … ne) //; 137 144 ] … … 141 148 #v #ty #H elim H; 142 149 [ #sz #sg whd in ⊢ (??%?); >intsize_eq_elim_true >eq_bv_true //; 143  # r #r' #t //;150  #t //; 144 151  #s whd; >(Feq_zero_true …) //; 145 152 ] … … 165 172 whd in ⊢ (??%?); change with (load_value_of_type' ty m 〈l,off〉) in H2:(??%?); 166 173 >H2 @refl 167  #e #ty # r #l #pc#off #tr #H1 #H2 whd in ⊢ (??%?);174  #e #ty #l #off #tr #H1 #H2 whd in ⊢ (??%?); 168 175 >(yields_eq ??? H2) whd in ⊢ (??%?); 169 @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd 176 (* @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd*) 170 177 @refl 171 178  #ty' #sz #sg @refl … … 221 228  #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1 222 229 >e2 @refl 223  #e #ty # r #l #pc#ofs #tr #H1 #H2 whd in ⊢ (??%?);230  #e #ty #l #ofs #tr #H1 #H2 whd in ⊢ (??%?); 224 231 >(yields_eq ??? H2) 225 232 @refl … … 262 269 (it:∀i,s. P (Tint i s)) 263 270 (fl:∀f. P (Tfloat f)) 264 (pt:∀ s,t. P t → P (Tpointer st))265 (ar:∀ s,t,n. P t → P (Tarray st n))271 (pt:∀t. P t → P (Tpointer t)) 272 (ar:∀t,n. P t → P (Tarray t n)) 266 273 (fn:∀tl,t. Q tl → P t → P (Tfunction tl t)) 267 274 (st:∀i,fl. P (Tstruct i fl)) 268 275 (un:∀i,fl. P (Tunion i fl)) 269 (cp:∀ r,i. P (Tcomp_ptrr i))276 (cp:∀i. P (Tcomp_ptr i)) 270 277 (nl:Q Tnil) 271 278 (cs:∀t,tl. P t → Q tl → Q (Tcons t tl)) … … 275 282  Tint i s ⇒ it i s 276 283  Tfloat s ⇒ fl s 277  Tpointer s t' ⇒ pt st' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')278  Tarray s t' n ⇒ ar st' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')284  Tpointer t' ⇒ pt t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t') 285  Tarray t' n ⇒ ar t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t') 279 286  Tfunction tl t' ⇒ fn tl t' (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t') 280 287  Tstruct i fs ⇒ st i fs 281 288  Tunion i fs ⇒ un i fs 282  Tcomp_ptr r i ⇒ cp ri289  Tcomp_ptr i ⇒ cp i 283 290 ] 284 291 and typelist_ind2l … … 287 294 (it:∀i,s. P (Tint i s)) 288 295 (fl:∀f. P (Tfloat f)) 289 (pt:∀ s,t. P t → P (Tpointer st))290 (ar:∀ s,t,n. P t → P (Tarray st n))296 (pt:∀t. P t → P (Tpointer t)) 297 (ar:∀t,n. P t → P (Tarray t n)) 291 298 (fn:∀tl,t. Q tl → P t → P (Tfunction tl t)) 292 299 (st:∀i,fl. P (Tstruct i fl)) 293 300 (un:∀i,fl. P (Tunion i fl)) 294 (cp:∀ r,i. P (Tcomp_ptrr i))301 (cp:∀i. P (Tcomp_ptr i)) 295 302 (nl:Q Tnil) 296 303 (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
Note: See TracChangeset
for help on using the changeset viewer.