Changeset 1516 for src/Clight


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

Ported to syntax of Matita 0.99.1.

Location:
src/Clight
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1244 r1516  
    3636lemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b.
    3737#v #ty #r #H elim H; #v #t #H' elim H';
    38   [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?) >(eq_bv_false … ne) //
     38  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
    3939  | #r #b #pc #i #i0 #s %{ true} % //
    4040  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
  • 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.
  • src/Clight/CexecEquiv.ma

    r1510 r1516  
    5555P (is_final s).
    5656#s #P #F #NF lapply (refl ? (is_final s))
    57 cases (is_final s) in ⊢ (???% → %)
    58 [ #E @NF % * #r #H whd in E:(??%?) > (is_final_complete … H) in E #H destruct
     57cases (is_final s) in ⊢ (???% → %);
     58[ #E @NF % * #r #H whd in E:(??%?); > (is_final_complete … H) in E; #H destruct
    5959| #r #E @F @is_final_sound @E
    6060] qed.
     
    7272>(exec_inf_aux_unfold …) cases x;
    7373[ #o #k #EXEC whd in EXEC:(??%?); destruct
    74 | #y cases y #tr' #s' whd in ⊢ (??%? → ?)
     74| #y cases y #tr' #s' whd in ⊢ (??%? → ?);
    7575  @is_final_elim'
    7676  [ #r #FINAL | #FINAL ]
     
    9898>(exec_inf_aux_unfold …) cases x;
    9999[ #o #k #EXEC whd in EXEC:(??%?); destruct
    100 | #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
     100| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
    101101  @is_final_elim' [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
    102102| #msg #EXEC whd in EXEC:(??%?); destruct
     
    120120  cases (se_step_eq … E) * #E1 #E2 #E3 #E4 >E1 >E2 >E3
    121121    >(exec_e_step_inv … H2)
    122     <(exec_e_step … H2) in H1 #H1 % //
     122    <(exec_e_step … H2) in H1; #H1 % //
    123123| #msg #_ #E destruct
    124124| #o #k #i #se #H1 #H2 #E destruct
     
    142142        [ #tr #r #m #E1 #E2 destruct
    143143        | #tr' #s' #e' #se' #H2 #H3 #E2 #_ destruct (E2);
    144             <(exec_e_step … H3) in H2 #H2 % [ 2: @H2 ]
     144            <(exec_e_step … H3) in H2; #H2 % [ 2: @H2 ]
    145145            lapply (STEP i);
    146146            >(exec_e_step_inv … H3)
     
    178178            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    179179                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
    180                 change in match (is_final ?????) with (is_final s2)
     180                change in match (is_final ?????); with (is_final s2)
    181181                @IFE
    182182                [ #r' #FINAL #E whd in E:(??%??);
     
    371371[ #tr #r #m #EXEC #E destruct (E)
    372372| #tr #s' #e #e' #H #EXEC #E destruct (E)
    373 | #msg #EXEC #H #_ generalize in match H -H; generalize in match EXEC -EXEC;
    374   generalize in match msg -msg; >(exec_inf_aux_unfold …)
     373| #msg #EXEC #H #_ generalize in match H; -H; generalize in match EXEC; -EXEC;
     374  generalize in match msg; -msg; >(exec_inf_aux_unfold …)
    375375    cases (exec_step ge s);
    376376  [ #o #k #msg' #EXEC whd in EXEC:(??%??); destruct
    377   | #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?) @is_final_elim'
     377  | #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?); @is_final_elim'
    378378      [ #r ] #F #EXEC whd in EXEC:(??%??); destruct
    379379  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%??); destruct @refl
     
    391391    cases (exec_step ge s);
    392392    [ #o #k #EXEC whd in EXEC:(??%??); destruct
    393     | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?) @is_final_elim'
     393    | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?); @is_final_elim'
    394394        [ #r ] #F #E whd in E:(??%??); destruct @F
    395395    | #msg #E whd in E:(??%??); destruct
     
    420420            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
    421421                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
    422                 change in match (is_final ?????) with (is_final s2)
     422                change in match (is_final ?????); with (is_final s2)
    423423                @IFE [ #r ] #F #EXECK
    424424                whd in EXECK:(??%??); destruct;
     
    535535| #f #args #kk #m cases f;
    536536  [ #f' whd in ⊢ (???%); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
    537     #x1 #x2 whd in ⊢ (???%) @err_does_not_interact //
     537    #x1 #x2 whd in ⊢ (???%); @err_does_not_interact //
    538538  (* This is the only case that actually matters! *)
    539539  | #fn #argtys #rty whd in ⊢ (???%);
     
    637637[ #tr #i #m #_ #_ #_ #ENO elim (eno_stop … ENO);
    638638| #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?);
    639   [ <(E0_right tr) in ⊢ (?%????)
     639  [ <(E0_right tr) in ⊢ (?%????);
    640640      @isteps_one @isteps_none
    641641  | #TR @(match sym_eq ??? TR with [ refl ⇒ ? ]) (* >TR in UNREACTIVE ⊢ % *)
     
    643643      @(show_divergence s')
    644644      [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1)
    645         change in ⊢ (?%????) with (Eapp E0 tr1); @isteps_one
     645        change in ⊢ (?%????); with (Eapp E0 tr1); @isteps_one
    646646        @S
    647       | #tr2 #s2 #e2 #S >TR in UNREACTIVE #UNREACTIVE @(UNREACTIVE tr2 s2 e2)
    648           change in ⊢ (?%????) with (Eapp E0 tr2);
     647      | #tr2 #s2 #e2 #S >TR in UNREACTIVE; #UNREACTIVE @(UNREACTIVE tr2 s2 e2)
     648          change in ⊢ (?%????); with (Eapp E0 tr2);
    649649          @isteps_one @S
    650650      | #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i)
    651           change in ⊢ (?%????) with (Eapp E0 tr2);
     651          change in ⊢ (?%????); with (Eapp E0 tr2);
    652652          @(isteps_one … S)
    653653      ]
     
    659659    @False_ind @(absurd ?? NOTSILENT)
    660660    @(UNREACTIVE … s' e')
    661     <(E0_right tr') in ⊢ (?%????)
     661    <(E0_right tr') in ⊢ (?%????);
    662662    >EXEC
    663663    @isteps_interact //;
     
    689689    *; #E1 #E2 #H1 destruct (E1);
    690690    lapply (H i); *; #tr' *; #s'' *; #K' #TR
    691     >E2 in H1 #H1 whd in H1:(?%?); >K' in H1
     691    >E2 in H1; #H1 whd in H1:(?%?); >K' in H1;
    692692    >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?);
    693     change in match (is_final ?????) with (is_final s'')
     693    change in match (is_final ?????); with (is_final s'')
    694694    @is_final_elim
    695695    [ #r #F whd in ⊢ (?%? → ?); #S
     
    698698        *; #E1 #E2 #S' <E1 @TR
    699699    ]
    700 | #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?)
     700| #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?);
    701701    @is_final_elim' [ #r ] #F #E whd in E:(?%?);
    702702    inversion E;
     
    885885            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
    886886                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
    887                 cases (H i); #tr1 *; #s1 *; #K #E >K in H2
     887                cases (H i); #tr1 *; #s1 *; #K #E >K in H2;
    888888                >(exec_inf_aux_unfold …)
    889                 whd in ⊢ (?%? → ?) @is_final_elim [ #r ]
     889                whd in ⊢ (?%? → ?); @is_final_elim [ #r ]
    890890                #F #S whd in S:(?%?); cases (se_inv … S);
    891             | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
     891            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
    892892                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
    893893                cases (se_inv … S);
     
    902902            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
    903903                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
    904                 cases (H i); #tr1 *; #s1 *; #K #E >K in H2
     904                cases (H i); #tr1 *; #s1 *; #K #E >K in H2;
    905905                >(exec_inf_aux_unfold …)
    906                 whd in ⊢ (?%? → ?) @is_final_elim [ #r ]
     906                whd in ⊢ (?%? → ?); @is_final_elim [ #r ]
    907907                #F #S whd in S:(?%?); cases (se_inv … S);
    908             | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
     908            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
    909909                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
    910910                cases (se_inv … S);
     
    987987  ∃e'.e = e_step ??? E0 s e'.
    988988#ge #s #e >(exec_inf_aux_unfold …)
    989 whd in ⊢ (??%? → ?) @is_final_elim'
     989whd in ⊢ (??%? → ?); @is_final_elim'
    990990[ #r #FINAL #EXEC #NOTFINAL
    991991    @False_ind @(absurd ?? NOTFINAL)
     
    10031003lapply (make_initial_state_sound p)
    10041004lapply (the_initial_state p)
    1005 whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?)
     1005whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?);
    10061006cases (make_initial_state p)
    10071007[ #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
    10081008    >exec_inf_aux_unfold
    1009     whd in ⊢ (?%? → ?)
     1009    whd in ⊢ (?%? → ?);
    10101010    @is_final_elim'
    10111011    [ #r #F @False_ind
     
    10201020        #ge #Ege
    10211021        inversion MATCHES;
    1022         [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM
     1022        [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM;
    10231023            #TERM
    10241024            lapply (exec_state_terminates … TERM); #E1
    1025             >E1 in TERM #TERM #_
     1025            >E1 in TERM; #TERM #_
    10261026            @(program_terminates (mk_transrel … step) ?? ge s)
    10271027            [ 2: @INITIAL
     
    10301030            | //;
    10311031            ]
    1032         | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES #DIVERGES
     1032        | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES; #DIVERGES
    10331033            lapply (exec_state_diverges … DIVERGES);
    1034             #E1 >E1 in DIVERGES #DIVERGES #_
     1034            #E1 >E1 in DIVERGES; #DIVERGES #_
    10351035            inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6
    1036             <E4 in INITSTEPS ⊢ % <E5 in E6 ⊢ % #E6 #INITSTEPS
     1036            <E4 in INITSTEPS ⊢ %; <E5 in E6 ⊢ %; #E6 #INITSTEPS
    10371037            cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
    1038             #E7 <E7 in INITSTEPS #INITSTEPS
     1038            #E7 <E7 in INITSTEPS; #INITSTEPS
    10391039            cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV #_
    10401040            @(program_diverges (mk_transrel … step) ?? ge s … INITIAL)
     
    10421042            | 3: <Ege @(silent_sound … DIVERGING EXECDIV)
    10431043            ]
    1044         | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS #REACTS
     1044        | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS; #REACTS
    10451045            lapply (exec_state_reacts … REACTS);
    1046             #E1 >E1 in REACTS #REACTS #_
     1046            #E1 >E1 in REACTS; #REACTS #_
    10471047            inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5
    1048             <E4 in REACTING ⊢ % <E5 #REACTING #E6
     1048            <E4 in REACTING ⊢ %; <E5 #REACTING #E6
    10491049            cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
    1050             #E7 <E7 in REACTING #REACTING #_
     1050            #E7 <E7 in REACTING; #REACTING #_
    10511051            @(program_reacts (mk_transrel … step) ?? ge s … INITIAL)
    10521052            <Ege @(reacts_sound … REACTING EXEC')
    1053         | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG #WRONG
     1053        | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG; #WRONG
    10541054            lapply (exec_state_wrong … WRONG);
    1055             #E1 >E1 in WRONG #WRONG #_
     1055            #E1 >E1 in WRONG; #WRONG #_
    10561056            inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7
    1057             <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG
     1057            <E4 in GOESWRONG ⊢ %; <E5 <E7 #GOESWRONG
    10581058            cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ]
    1059             #E8 <E8 in GOESWRONG #GOESWRONG
     1059            #E8 <E8 in GOESWRONG; #GOESWRONG
    10601060            elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL
    10611061            <Ege #_
  • src/Clight/CexecSound.ma

    r1510 r1516  
    66cases v; [ | #sz #i | #f | #r1 | #r' #b #pc #of ]
    77cases ty; [ 2,11,20,29,38: #sz' #sg | 3,12,21,30,39: #sz' | 4,13,22,31,40: #rg #ty | 5,14,23,32,41: #r #ty #n | 6,15,24,33,42: #args #rty | 7,8,16,17,25,26,34,35,43,44: #id #fs | 9,18,27,36,45: #r #id ]
    8 whd in ⊢ (??%? → ?)
     8whd in ⊢ (??%? → ?);
    99[ 2: @intsize_eq_elim_elim
    1010  [ #NE #H destruct
     
    1515  ]
    1616| 8: #H cases (eq_dec f Fzero)
    17   [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
    18   | #ne >Feq_zero_false in H // #E destruct @bool_of_val_true @is_true_float @ne
     17  [ #e >e in H ⊢ %; >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
     18  | #ne >Feq_zero_false in H; // #E destruct @bool_of_val_true @is_true_float @ne
    1919  ]
    2020| 14: #H destruct @bool_of_val_false @is_false_pointer
     
    3535lemma try_cast_null_sound: ∀m,sz,i,ty,ty',v'. try_cast_null m sz i ty ty' = OK ? v' → cast m (Vint sz i) ty ty' v'.
    3636#m #sz #i #ty #ty' #v'
    37 whd in ⊢ (??%? → ?)
     37whd in ⊢ (??%? → ?);
    3838@eq_bv_elim
    3939[ #e >e
     
    5555  | 7,8,9: #a #b #H whd in H:(??%?); destruct;
    5656  | #sz1 #si1 cases ty';
    57     [ whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     57    [ whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    5858      [ #NE #H destruct
    5959      | *; whd #H whd in H:(??%?); destruct;
    6060      ]
    61     | 3: #a whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     61    | 3: #a whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    6262      [ #E #H whd in H:(??%?); destruct
    6363      | *; whd #H whd in H:(??%?); destruct; @cast_if
    6464      ]
    65     | 2,7,8,9: #a #b whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     65    | 2,7,8,9: #a #b whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    6666      [ 1,3,5,7: #NE #H destruct
    6767      | *: *; whd #H whd in H:(??%?); destruct; //
     
    7070                 | #sp #ty'' #n letin t ≝ (Tarray sp ty'' n)
    7171                 | #args #rty letin t ≝ (Tfunction args rty) ]
    72         whd in ⊢ (??%? → ?) @intsize_eq_elim_elim
     72        whd in ⊢ (??%? → ?); @intsize_eq_elim_elim
    7373        [ 1,3,5: #NE #H destruct
    7474        | *: *; whd
     
    100100    cases ty' in H2; normalize; try #a try #b try #c try #d destruct;
    101101    @cast_pp_z //;
    102 | #r #b #pc #of whd in ⊢ (??%? → ?) #e
     102| #r #b #pc #of whd in ⊢ (??%? → ?); #e
    103103    elim (bind_inversion ????? e) #s * #es #e'
    104104    elim (bind_inversion ????? e') #u * #eu #e'' -e';
     
    113113        | #Hty'
    114114            cut (s = r). elim (eq_region_dec r s) in eu; //; normalize; #_ #e destruct.
    115             #e >e in Hty #Hty
    116             cases (pointer_compat_dec b s') in e'''
     115            #e >e in Hty; #Hty
     116            cases (pointer_compat_dec b s') in e''';
    117117            #Hcompat #e''' whd in e''':(??%?); destruct (e'''); /2/
    118118        ]
     
    190190(P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
    191191#ge #en #m #e @(expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e)
    192 [ #sz #ty #c whd in ⊢ (???%) cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%)
     192[ #sz #ty #c whd in ⊢ (???%); cases ty try #sz' try #sg try #x try @I whd in ⊢ (???%);
    193193  @eq_intsize_elim #E try @I <E whd %
    194194| #ty #c whd //
     
    197197    @bind2_OK #x cases x; #y cases y; #sp #loc #ofs #tr #H
    198198    @opt_bind_OK #vl #evl whd in evl:(??%?); @(eval_Elvalue … evl)
    199     >H in He' #He' @He'
     199    >H in He'; #He' @He'
    200200| #v #ty
    201201    whd in ⊢ (???%);
    202202    lapply (refl ? (lookup SymbolTag block en v))
    203     cases (lookup SymbolTag block en v) in ⊢ (???% → %)
     203    cases (lookup SymbolTag block en v) in ⊢ (???% → %);
    204204    [ #eget @opt_bind_OK #sploc cases sploc; #sp #loc #efind
    205205        whd; @(eval_Evar_global … eget efind)
    206206    | #loc #eget @(eval_Evar_local … eget)
    207207    ]
    208 | #ty #e #He whd in ⊢ (???%)
     208| #ty #e #He whd in ⊢ (???%);
    209209    @bind2_OK #v cases v // #r #l #pc #ofs #tr #Hv whd
    210     >Hv in He #He
     210    >Hv in He; #He
    211211    @eval_Ederef [ 3: @He | *: skip ]
    212212| #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H
    213213  cases ty // * #pty
    214   cases loc in H ⊢ % * #loc' #H
     214  cases loc in H ⊢ %; * #loc' #H
    215215  whd try @I
    216   @eval_Eaddrof whd in H:(??%?) >H in He'' #He'' @He''
     216  @eval_Eaddrof whd in H:(??%?); >H in He''; #He'' @He''
    217217| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
    218218    @opt_bind_OK #v #ev
    219219    @(eval_Eunop … ev)
    220     >Hv1 in He1 #He1 @He1
     220    >Hv1 in He1; #He1 @He1
    221221| #ty #op #e1 #e2 #He1 #He2
    222     @bind2_OK #v1 #tr1 #ev1 >ev1 in He1 #He1
    223     @bind2_OK #v2 #tr2 #ev2 >ev2 in He2 #He2
     222    @bind2_OK #v1 #tr1 #ev1 >ev1 in He1; #He1
     223    @bind2_OK #v2 #tr2 #ev2 >ev2 in He2; #He2
    224224    @opt_bind_OK #v #ev whd in He1 He2; whd;
    225225    @(eval_Ebinop … He1 He2 ev)
    226226| #ty #ty' #e' #He'
    227     @bind2_OK #v #tr #Hv >Hv in He' #He'
     227    @bind2_OK #v #tr #Hv >Hv in He'; #He'
    228228    @bind_OK #v' #ev'
    229229    @(eval_Ecast … He' ?)
     
    231231    @(exec_cast_sound … ev')
    232232| #ty #e1 #e2 #e3 #He1 #He2 #He3
    233     @bind2_OK #vb #tr1 #Hvb >Hvb in He1 #He1
     233    @bind2_OK #vb #tr1 #Hvb >Hvb in He1; #He1
    234234    @bind_OK #b
    235235    cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
    236     @bind2_OK #v #tr #Hv whd in Hv:(??%?)
    237     [ >Hv in He2 #He2 whd in He2 Hv:(??%?) ⊢%;
     236    @bind2_OK #v #tr #Hv whd in Hv:(??%?);
     237    [ >Hv in He2; #He2 whd in He2 Hv:(??%?) ⊢%;
    238238        @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb)
    239     | >Hv in He3 #He3 whd in He3 Hv:(??%?) ⊢%;
     239    | >Hv in He3; #He3 whd in He3 Hv:(??%?) ⊢%;
    240240        @(eval_Econdition_false … He1 ? He3) @(bool_of ??? Hb)
    241241    ]
    242242| #ty #e1 #e2 #He1 #He2
    243     @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
     243    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
    244244    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
    245     [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
     245    [ @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
    246246        @bind_OK #b2 #eb2
    247247        @(eval_Eandbool_2 … He1 … He2)
     
    250250    ]
    251251| #ty #e1 #e2 #He1 #He2
    252     @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1 #He1
     252    @bind2_OK #v1 #tr1 #Hv1 >Hv1 in He1; #He1
    253253    @bind_OK #b1 cases b1; #eb1 lapply (exec_bool_of_val_sound … eb1); #Hb1
    254254    [ @(eval_Eorbool_1 … He1) @(bool_of … Hb1)
    255     | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2 #He2
     255    | @bind2_OK #v2 #tr2 #Hv2 >Hv2 in He2; #He2
    256256        @bind_OK #b2 #eb2
    257257        @(eval_Eorbool_2 … He1 … He2)
     
    261261| #ty #e' #ty' #i cases ty'; //;
    262262    [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
    263         @bind_OK #delta #Hdelta whd in H:(??%?) >H in He' #He'
     263        @bind_OK #delta #Hdelta whd in H:(??%?); >H in He'; #He'
    264264        @(eval_Efield_struct …  He' (refl ??) Hdelta)
    265     | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?)
    266         >H in He' #He'
     265    | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?);
     266        >H in He'; #He'
    267267        @(eval_Efield_union … He' (refl ??))
    268268    ]
    269 | #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He' #He'
     269| #ty #l #e' #He' @bind2_OK #v #tr1 #H >H in He'; #He'
    270270    @(eval_Ecost … He')
    271271(* exec_lvalue fails on non-lvalues. *)
     
    280280#ge #en #m #e #r #loc #pc #off #tr #ty #H inversion H;
    281281[ 1,2,5: #a #b #c #H @False_ind destruct (H);
    282 | #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1 #H1 @False_ind
     282| #a #b #c #d #e #f #H1 #g #H2 #E1 #E2 #E3 <H2 in H1; #H1 @False_ind
    283283    @(eval_lvalue_inv_ind … H1)
    284284    [ #a #b #c #d #bad destruct (bad);
     
    304304exec_lvalue ge en m e = OK ? 〈〈mk_block r loc,off〉,tr〉 →
    305305exec_expr ge en m (Expr (Eaddrof e) (Tpointer r Tvoid)) = OK ? 〈Vptr r (mk_block r loc) (same_compat ??) off, tr〉.
    306 #ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?)
    307 >H whd in ⊢ (??%?) cases r @refl
     306#ge #en #m #e #r #loc #off #tr #H whd in ⊢ (??%?);
     307>H whd in ⊢ (??%?); cases r @refl
    308308qed.
    309309
     
    312312#ge #en #m #e lapply (refl ? (exec_lvalue ge en m e));
    313313cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    314 [ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ % #locr #loci #H
     314[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ %; #locr #loci #H
    315315    @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ]
    316316    lapply (addrof_exec_lvalue … H) #H'
     
    350350| * #id #ty #t #IH #en #m #en' #m'
    351351  lapply (refl ? (alloc m O (sizeof ty) Any)) #ALLOC #EXEC
    352   whd in EXEC:(??%?) ALLOC:(???%)
     352  whd in EXEC:(??%?) ALLOC:(???%);
    353353 @(alloc_variables_cons … ALLOC)
    354354 @IH @EXEC
     
    365365      @opt_bind_OK #m' #STORE
    366366      lapply (refl ? (exec_bind_parameters en m' ps' vs))
    367       cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %) [2: #msg #_ %]
     367      cases (exec_bind_parameters en m' ps' vs) in ⊢ (???% → %); [2: #msg #_ %]
    368368      #m'' #BIND
    369369      @(bind_parameters_cons … GET STORE)
    370       lapply (IH vs en m') whd in ⊢ (% → ?) >BIND //
     370      lapply (IH vs en m') whd in ⊢ (% → ?); >BIND //
    371371    ]
    372372] qed.
     
    378378| #v #vs #IH *
    379379  [ //
    380   | #ty #tys whd in ⊢ (???%)
     380  | #ty #tys whd in ⊢ (???%);
    381381    cases ty [ #sz #sg | #sz | #r ] cases v //
    382     [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?)
     382    [ #sz' #v @bind_OK #ev whd in ⊢ (??%? → ?);
    383383      @eq_intsize_elim #E #CHECKev whd in CHECKev:(??%?); destruct
    384384    | #v ] @bind_OK #evs #CHECKevs
     
    498498  ]
    499499| #f0 #vargs #k #m whd in ⊢ (?????%); cases f0;
    500   [ #fn whd in ⊢ (?????%)
     500  [ #fn whd in ⊢ (?????%);
    501501    lapply (refl ? (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)))
    502     cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %)
    503     #en' #m' #ALLOC whd in ⊢ (?????%)
     502    cases (exec_alloc_variables empty_env m (fn_params fn@fn_vars fn)) in ⊢ (???% → %);
     503    #en' #m' #ALLOC whd in ⊢ (?????%);
    504504    @res_bindIO_OK #m2 #BIND
    505505    whd; @(step_internal_function … (exec_alloc_variables_sound … ALLOC))
  • src/Clight/casts.ma

    r1489 r1516  
    5454<add_with_carries_unfold
    5555cases (add_with_carries n x y c)
    56 #rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?) >bool_eta //
     56#rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?); >bool_eta //
    5757qed.
    5858
     
    6060  tail … (addition_n (S n) (hx:::x) (hy:::y)) = addition_n … x y.
    6161#n #hx #hy #x #y
    62 whd in ⊢ (??(???%)%)
     62whd in ⊢ (??(???%)%);
    6363<(add_with_carries_extend n hx hy x y false)
    6464cases (add_with_carries (S n) (hx:::x) (hy:::y) false)
     
    9595#m elim m
    9696[ #n #x #y #c >truncate_eq >truncate_eq cases (add_with_carries n x y c) #rs #cs
    97   whd in ⊢ (??%?) >truncate_eq >truncate_eq  @refl
     97  whd in ⊢ (??%?); >truncate_eq >truncate_eq  @refl
    9898| #m' #IH #n #x #y #c
    9999  >(hdtl … x) >(hdtl … y)
    100100  >truncate_head >truncate_head <IH
    101101  <(add_with_carries_extend ? (head' ?? x) (head' ?? y) (tail ?? x) (tail ?? y))
    102   cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%)
     102  cases (add_with_carries ????) #rs #cs whd in ⊢ (??%%);
    103103  <truncate_tail <truncate_tail @refl
    104104] qed.
     
    106106lemma truncate_plus : ∀m,n,x,y.
    107107  truncate m n (addition_n … x y) = addition_n … (truncate … x) (truncate … y).
    108 #m #n #x #y whd in ⊢ (??(???%)%) <truncate_add_with_carries
     108#m #n #x #y whd in ⊢ (??(???%)%); <truncate_add_with_carries
    109109cases (add_with_carries ????) //
    110110qed.
     
    114114#m0 elim m0
    115115[ #n #x >truncate_eq //
    116 | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
     116| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH
    117117] qed.
    118118
    119119theorem zero_plus_reduce : ∀m,n,x,y.
    120120  truncate m n (addition_n (m+n) (pad … x) (pad … y)) = addition_n n x y.
    121 #m #n #x #y <(truncate_pad m n x) in ⊢ (???%) <(truncate_pad m n y) in ⊢ (???%)
     121#m #n #x #y <(truncate_pad m n x) in ⊢ (???%); <(truncate_pad m n y) in ⊢ (???%);
    122122@truncate_plus
    123123qed.
     
    130130#m0 elim m0
    131131[ #n #x >truncate_eq //
    132 | #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?) @IH
     132| #m #IH #n #x >truncate_tail normalize in ⊢ (??(???%)?); @IH
    133133] qed.
    134134
    135135theorem sign_plus_reduce : ∀m,n,x,y.
    136136  truncate m n (addition_n (m+n) (sign … x) (sign … y)) = addition_n n x y.
    137 #m #n #x #y <(truncate_sign m n x) in ⊢ (???%) <(truncate_sign m n y) in ⊢ (???%)
     137#m #n #x #y <(truncate_sign m n x) in ⊢ (???%); <(truncate_sign m n y) in ⊢ (???%);
    138138@truncate_plus
    139139qed.
     
    171171  <add_with_carries_unfold
    172172  cases (add_with_carries n x y c)
    173   #lb #cs whd in ⊢ (??%%) >bool_eta
     173  #lb #cs whd in ⊢ (??%%); >bool_eta
    174174  //
    175175| *: skip
     
    181181#m #n #x @(vector_inv_n … x) #h #t elim n
    182182[ @refl
    183 | #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?) >IH @refl
     183| #n' #IH >sign_vcons whd in IH:(??%?) ⊢ (??%?); >IH @refl
    184184] qed.
    185185
     
    201201lemma zero_negate_reduce : ∀m,n,x.
    202202  truncate m (S n) (two_complement_negation (m+S n) (pad … x)) = two_complement_negation ? x.
    203 #m #n #x whd in ⊢ (??(???%)%)
     203#m #n #x whd in ⊢ (??(???%)%);
    204204lapply (truncate_add_with_carries m (S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
    205205cases (add_with_carries (m + S n) (negation_bv (m+S n) (pad m (S n) x)) (zero ?) true)
    206 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     206#rs #cs whd in ⊢ (??%? → ??(???%)?);
    207207>truncate_negation_bv
    208208>truncate_pad >truncate_zero cases (add_with_carries ????)
     
    212212lemma sign_negate_reduce : ∀m,n,x.
    213213  truncate m (S n) (two_complement_negation (m+S n) (sign … x)) = two_complement_negation ? x.
    214 #m #n #x whd in ⊢ (??(???%)%)
     214#m #n #x whd in ⊢ (??(???%)%);
    215215>sign_bitflip <(zero_sign (S n) m)
    216216lapply (truncate_add_with_carries m (S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
    217217cases (add_with_carries (m + S n) (sign (S n) m (negation_bv (S n) x)) (sign (S n) m (zero (S n))) true)
    218 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     218#rs #cs whd in ⊢ (??%? → ??(???%)?);
    219219>truncate_sign >truncate_sign cases (add_with_carries ????)
    220220#rs' #cs' #E destruct //
     
    224224  truncate m (S n) (subtraction … (pad … x) (pad … y)) = subtraction … x y.
    225225#m #n #x #y
    226 whd in ⊢ (??(???%)%)
     226whd in ⊢ (??(???%)%);
    227227lapply (truncate_add_with_carries m (S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
    228228cases (add_with_carries (m+S n) (pad … x) (two_complement_negation (m+S n) (pad … y)) false)
    229 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     229#rs #cs whd in ⊢ (??%? → ??(???%)?);
    230230>zero_negate_reduce >truncate_pad
    231231cases (add_with_carries ????)
     
    236236  truncate m (S n) (subtraction … (sign … x) (sign … y)) = subtraction … x y.
    237237#m #n #x #y
    238 whd in ⊢ (??(???%)%)
     238whd in ⊢ (??(???%)%);
    239239lapply (truncate_add_with_carries m (S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
    240240cases (add_with_carries (m+S n) (sign (S n) m x) (two_complement_negation (m+S n) (sign (S n) m y)) false)
    241 #rs #cs whd in ⊢ (??%? → ??(???%)?)
     241#rs #cs whd in ⊢ (??%? → ??(???%)?);
    242242>sign_negate_reduce >truncate_sign
    243243cases (add_with_carries ????)
  • src/Clight/toCminor.ma

    r1515 r1516  
    122122  local_id (add ?? vars id (Global r)) id' → local_id vars id'.
    123123#var #id #r #id'
    124 whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?)
     124whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?);
    125125cases (identifier_eq ? id id')
    126 [ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
     126[ #E >E >lookup_add_hit whd in ⊢ (% → ?); *
    127127| #NE >lookup_add_miss /2/
    128128] qed.
     
    131131  id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
    132132#vars #id #t #id' #NE
    133 whd in ⊢ (% → %)
    134 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
     133whd in ⊢ (% → %);
     134whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]);
    135135>lookup_add_miss
    136136[ #H @H | /2/ ]
     
    142142      Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
    143143#globals #f
    144 whd in ⊢ (∀_.∀_.??%? → ?)
     144whd in ⊢ (∀_.∀_.??%? → ?);
    145145elim (fn_params f @ fn_vars f)
    146 [ #vars #n whd in ⊢ (??%? → ?) #E destruct #i #H @False_ind
    147   elim globals in H
     146[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H @False_ind
     147  elim globals in H;
    148148  [ normalize //
    149   | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H)
     149  | * #id #rg #t #IH whd in ⊢ (?%? → ?); #H @IH @(local_id_add_global ???? H)
    150150  ]
    151 | * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i
     151| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i
    152152  cases (identifier_eq ? id i)
    153153  [ #E' <E' #H % @refl
    154154  | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
    155     whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
    156     cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
     155    whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     156    cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
    157157    #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
    158158    @(IH m0 n0)
    159     [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ
     159    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ
    160160    | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE
    161161    ]
     
    348348  expr_vars ? e P.
    349349#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
    350 whd in ⊢ (??%? → ?)
     350whd in ⊢ (??%? → ?);
    351351[ cases (classify_add ty1 ty2)
    352   [ 3,4: #z ] whd in ⊢ (??%? → ?)
    353   [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     352  [ 3,4: #z ] whd in ⊢ (??%? → ?);
     353  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    354354    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    355355    whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
    356   | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     356  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    357357    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    358358    whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
     
    360360  ]
    361361| cases (classify_sub ty1 ty2)
    362   [ 3,4: #z] whd in ⊢ (??%? → ?)
    363   [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
     362  [ 3,4: #z] whd in ⊢ (??%? → ?);
     363  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?);
    364364    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
    365365    whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
     
    737737  〈tmp,u'〉 = alloc_tmp q u → tmps_preserved vars u u'.
    738738#tmp #g #g' #vars #q
    739 whd in ⊢ (???% → ?) #E
     739whd in ⊢ (???% → ?); #E
    740740#id #H
    741741cases (identifier_eq ? id tmp)
    742742destruct #E
    743 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]
     743whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ];
    744744[ >E >lookup_add_hit @I
    745745| cases E #NE >lookup_add_miss [ @H | /2/
     
    765765lemma local_id_add_local_oblivious : ∀vars,id,id'.
    766766  local_id vars id → local_id (add ?? vars id' Local) id.
    767 #vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
     767#vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    768768cases (identifier_eq ? id id')
    769769[ #E >E >lookup_add_hit @I
     
    791791  〈tmp,u〉 = alloc_tmp q u0 → local_id (add_tmps vars u) tmp.
    792792#tmp #u #q #u0 #vars
    793 whd in ⊢ (???% → ?) #E
     793whd in ⊢ (???% → ?); #E
    794794destruct
    795 whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit
     795whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit
    796796@I
    797797qed.
     
    987987lemma lookup_label_add : ∀lbls,l,l'.
    988988  lookup_label (add … lbls l l') l = OK ? l'.
    989 #lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl
     989#lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl
    990990qed.
    991991
     
    994994  lookup_label (add … lbls l l') l0 = lookup_label lbls l0.
    995995#lbls #l #l' #l0 #NE
    996 whd in ⊢ (??%%)
     996whd in ⊢ (??%%);
    997997>lookup_add_miss
    998998[ @refl | @NE ]
     
    10121012].
    10131013[ #l #l' #H %2 @H
    1014 | cases lbls1 #lbls' #I whd in ⊢ (??%?)
     1014| cases lbls1 #lbls' #I whd in ⊢ (??%?);
    10151015  #l1 #l1' #E1 @(eq_identifier_elim … l l1)
    10161016  [ #E %1 %1 @E
    10171017  | #NE cases (I l1 l1' E1)
    10181018    [ #H %1 %2 @H
    1019     | #LOOK' %2 >lookup_label_miss in LOOK' /2/ #H @H
     1019    | #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H
    10201020    ]
    10211021  ]
     
    10271027  OK ? «lbls, ?».
    10281028#l #l' #E cases (H l l' E) //
    1029 whd in ⊢ (??%? → ?) #H destruct
     1029whd in ⊢ (??%? → ?); #H destruct
    10301030qed.
    10311031
     
    10341034  local_id vars i ∨ Exists ? (λx.\fst x = i) (tmp_env tmpgen).
    10351035#vars #tmpgen #i
    1036 whd in ⊢ (?%? → ?)
     1036whd in ⊢ (?%? → ?);
    10371037elim (tmp_env tmpgen)
    10381038[ #H %1 @H
     
    10861086  #l * #l' #LOOKUP
    10871087  lapply (Ilbls l' l LOOKUP) #DEFINED
    1088   cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP #Ex destruct (Ex)
     1088  cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex)
    10891089  #H @H
    10901090] qed.
Note: See TracChangeset for help on using the changeset viewer.