Ignore:
Timestamp:
Nov 19, 2011, 12:38:20 AM (8 years ago)
Author:
sacerdot
Message:

Ported to syntax of Matita 0.99.1.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1510 r1516  
    3030
    3131lemma 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 ⊢ (% → ?); *;
    3333qed.
    3434
     
    6565inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15 #e16
    6666inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25 #e26
    67 >e11 in e21 #e1 >(?:ge1 = ge2) in e13 e14
     67>e11 in e21; #e1 >(?:ge1 = ge2) in e13 e14;
    6868[ 2: destruct (e1) skip (e11); @refl ]
    6969#e13 #e14
    7070
    71 >e12 in e22 #e2 destruct (e2) skip (e12);
    72 
    73 >e13 in e23 #e3 >(?:b1 = b2) in e14
     71>e12 in e22; #e2 destruct (e2) skip (e12);
     72
     73>e13 in e23; #e3 >(?:b1 = b2) in e14;
    7474[ >e24 #e4 >(?:f2 = f1)
    7575  [ //;
     
    8888>e2
    8989whd in ⊢ (??%?);
    90 change in e1:(??%?) with (make_global (mk_program ?? globs fns main))
     90change in e1:(??%?); with (make_global (mk_program ?? globs fns main))
    9191>e1
    9292>e3
     
    100100#m #v #ty #ty' #v' #H
    101101elim H;
    102 [ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
     102[ #m #sz1 #sz2 #sg1 #sg2 #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
    103103| #m #f #sz #szi #sg @refl
    104 | #m #sz #sz' #sg #i whd in ⊢ (??%?) >intsize_eq_elim_true @refl
     104| #m #sz #sz' #sg #i whd in ⊢ (??%?); >intsize_eq_elim_true @refl
    105105| #m #f #sz #sz' @refl
    106106| #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 ⊢ (??%?); ]
    110110    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 ⊢ (??%?);
    112112    @(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 //;
    115115| #m #t #t' #r #r' #H #H' cases H; try #a try #b try #c cases H'; try #d try #e try #f
    116116    whd in ⊢ (??%?); try @refl @(dec_true ? (eq_region_dec a a) (refl ??)) #H0 @refl
     
    132132lemma 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.
    133133#v #ty #r #H elim H; #v #t #H' elim H';
    134   [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?) >intsize_eq_elim_true
     134  [ #sz #sg #i #ne %{ true} % //; whd in ⊢ (??%?); >intsize_eq_elim_true
    135135    >(eq_bv_false … ne) //
    136136  | #r #b #pc #i #i0 #s %{ true} % //
    137137  | #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 //
    139139  | #r #r' #t %{ false} % //;
    140140  | #s %{ false} % //; whd; >(Feq_zero_true …) //;
     
    144144lemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
    145145#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) //;
    147147  | #p #b #i #i0 #s //
    148148  | #f #s #ne whd; >(Feq_zero_false … ne) //;
     
    152152lemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
    153153#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 //;
    155155  | #r #r' #t //;
    156156  | #s whd; >(Feq_zero_true …) //;
     
    165165  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
    166166  (λe,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈l,off〉,tr〉)));
    167 [ #sz #sg #i whd in ⊢ (??%?) >eq_intsize_true @refl
     167[ #sz #sg #i whd in ⊢ (??%?); >eq_intsize_true @refl
    168168| #f #ty @refl
    169169| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
    170170    [ #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)
    175175    ]
    176176    >(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〉)
    178178    >H2 @refl
    179179| #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
    180     >(yields_eq ??? H2) whd in ⊢ (??%?)
     180    >(yields_eq ??? H2) whd in ⊢ (??%?);
    181181    @(dec_true ? (pointer_compat_dec l r) pc) #pc' whd
    182182    @refl
     
    326326[ #env'' #m'' %
    327327| #env1 #m1 #id #ty #l1 #m2 #loc #m3 #env2 #H1 #H2 #H3
    328   < H3 whd in H1:(??%?) ⊢ (??%?)
     328  < H3 whd in H1:(??%?) ⊢ (??%?);
    329329  < (pair_eq1 ?????? H1) < (pair_eq2 ?????? H1)
    330330  @refl
     
    337337[ //;
    338338| #env1 #m1 #id #ty #l #v #tl #loc #m2 #m3 #H1 #H2 #H3 #H4
    339     whd in ⊢ (??%?)
     339    whd in ⊢ (??%?);
    340340    >H1 whd in ⊢ (??%?);
    341341    >H2 whd in ⊢ (??%?);
     
    345345lemma eventval_match_complete': ∀ev,ty,v.
    346346  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.
    348348
    349349lemma eventval_list_match_complete: ∀vs,tys,evs.
     
    351351#vs #tys #evs #H elim H;
    352352[ //
    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 ⊢ (??%?); //
    356356] qed.
    357357
     
    360360#ge #s #tr #s' #H elim H;
    361361[ #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)
    365365    >H3 @refl
    366366| #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
     
    446446    //
    447447| #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;
    449449    #H1 #H2
    450450    >(yields_eq ??? (eventval_list_match_complete … H1)) whd in ⊢ (??%?);
     
    453453| #v #f #env #k #m @refl
    454454| #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 @refl
     455    change in ⊢ (??%? → ?); with (store_value_of_type' ty m1 〈loc,ofs〉 v)
     456    #H whd in ⊢ (??%?); >H @refl
    457457| #f #l #s #k #env #m @refl
    458458] qed.
Note: See TracChangeset for help on using the changeset viewer.