Changeset 500 for Deliverables/D3.1/Csemantics/CexecComplete.ma
 Timestamp:
 Feb 11, 2011, 4:45:38 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/CexecComplete.ma
r499 r500 48 48 ] qed. 49 49 50 lemma eq_region_dec_true: ∀s. eq_region_dec s s = inl ???. 51 [ #s cases s; @refl 52  skip 50 lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f. 51 #P #f #p #Q #H cases f; 52 [ @H 53  #np cut False [ @(absurd ? p np)  * ] 54 ] qed. 55 56 lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f. 57 #P #f #p #Q #H cases f; 58 [ #np cut False [ @(absurd ? np p)  * ] 59  @H 53 60 ] qed. 54 61 … … 105 112  #m #i #sz #sz' #sg @refl 106 113  #m #f #sz #sz' @refl 107  #m # sp #sp' #ty #ty' #b #ofs #H1 #H2 #H3108 elim H1 ; [ #sp1 #ty1  #sp1 #ty1 #n1  #tys1 #ty1 letin sp1 ≝ Code ]109 whd in ⊢ (??%?) ;110 [ 1,2: >(eq_region_dec_true …) whd in ⊢ (??%?);]111 elim H2 in H3⊢ %; [ 1,4,7: #sp2 #ty2  2,5,8: #sp2 #ty2 #n2  3,6,9: #tys2 #ty2 letin sp2 ≝ Code ]112 # H3 whd in ⊢ (??%?);113 >(is_pointer_compat_true …) //;114  #m #r #r' #ty #ty' #b #pc #ofs #H1 #H2 #pc' 115 elim H1 in pc ⊢ % [ #r1 #ty1 #pc  #r1 #ty1 #n1 #pc  #tys1 #ty1 #pc letin r1 ≝ Code ] 116 whd in ⊢ (??%?) 117 [ 1,2: @(dec_true ? (eq_region_dec r1 r1) (refl ??) …) #H0 whd in ⊢ (??%?) ] 118 elim H2 in pc' ⊢ %; [ 1,4,7: #sp2 #ty2  2,5,8: #sp2 #ty2 #n2  3,6,9: #tys2 #ty2 letin sp2 ≝ Code ] 119 #pc' whd in ⊢ (??%?) 120 @(dec_true ? (pointer_compat_dec b sp2) pc') // 114 121  #m #sz #si #ty'' #r #H cases H; //; 115 122  #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f 116 whd in ⊢ (??%?); try @refl >eq_region_dec_true@refl123 whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl 117 124 ] qed. 118 125 … … 133 140 #v #ty #r #H elim H; #v #t #H' elim H'; 134 141 [ #i #is #s #ne %{ true} % //; whd; >(eq_false … ne) //; 135  # p #b#i #i0 #s %{ true} % //142  #r #b #pc #i #i0 #s %{ true} % // 136 143  #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //; 137 144  #i #s %{ false} % //; … … 171 178 >(yields_eq ??? H3) 172 179 whd in ⊢ (??%?); >H2 @refl 173  #e #ty #sp #l #off #tr #H1 #H2 whd in ⊢ (??%?); 174 >(yields_eq ??? H2) 180  #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?); 181 >(yields_eq ??? H2) whd in ⊢ (??%?) 182 @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd 175 183 @refl 176 184  #ty' #ty @refl … … 226 234  #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1 227 235 >e2 @refl 228  #e #ty #r #l # ofs #tr #H1 #H2 whd in ⊢ (??%?);236  #e #ty #r #l #pc #ofs #tr #H1 #H2 whd in ⊢ (??%?); 229 237 >(yields_eq ??? H2) 230 238 @refl … … 348 356 ] qed. 349 357 350 lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inl ?? p')) → Q f.351 #P #f #p #Q #H cases f;352 [ @H353  #np @False_ind @(absurd ? p np)354 ] qed.355 356 lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inr ?? p')) → Q f.357 #P #f #p #Q #H cases f;358 [ #np @False_ind @(absurd ? np p)359  @H360 ] qed.361 362 358 theorem step_complete: ∀ge,s,tr,s'. 363 359 step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉.
Note: See TracChangeset
for help on using the changeset viewer.