Ignore:
Timestamp:
Feb 11, 2011, 4:45:38 PM (8 years ago)
Author:
campbell
Message:

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/CexecComplete.ma

    r499 r500  
    4848] qed.
    4949
    50 lemma eq_region_dec_true: ∀s. eq_region_dec s s = inl ???.
    51 [ #s cases s; @refl
    52 | skip
     50lemma 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
     56lemma 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
    5360] qed.
    5461
     
    105112| #m #i #sz #sz' #sg @refl
    106113| #m #f #sz #sz' @refl
    107 | #m #sp #sp' #ty #ty' #b #ofs #H1 #H2 #H3
    108     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') //
    114121| #m #sz #si #ty'' #r #H cases H; //;
    115122| #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 @refl
     123    whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
    117124] qed.
    118125
     
    133140#v #ty #r #H elim H; #v #t #H' elim H';
    134141  [ #i #is #s #ne %{ true} % //; whd; >(eq_false … ne) //;
    135   | #p #b #i #i0 #s %{ true} % //
     142  | #r #b #pc #i #i0 #s %{ true} % //
    136143  | #f #s #ne %{ true} % //; whd; >(Feq_zero_false … ne) //;
    137144  | #i #s %{ false} % //;
     
    171178    >(yields_eq ??? H3)
    172179    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
    175183    @refl
    176184| #ty' #ty @refl
     
    226234| #id #l #ty #e1 #e2 whd in ⊢ (??%?); >e1
    227235    >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 ⊢ (??%?);
    229237    >(yields_eq ??? H2)
    230238    @refl
     
    348356] qed.
    349357
    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 [ @H
    353 | #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 | @H
    360 ] qed.
    361 
    362358theorem step_complete: ∀ge,s,tr,s'.
    363359  step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉.
Note: See TracChangeset for help on using the changeset viewer.