Ignore:
Timestamp:
Jun 7, 2011, 4:53:53 PM (9 years ago)
Author:
campbell
Message:

Revise proofs affected by recent matita change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecSound.ma

    r882 r891  
    33(*include "Plogic/connectives.ma".*)
    44
     5(* Is rather careful about using destruct because it currently uses excessive
     6   normalization. *)
    57lemma exec_bool_of_val_sound: ∀v,ty,r.
    68 exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    79#v #ty #r
    810cases v; [ | #i | #f | #r1 | #r' #b #pc #of ]
    9 cases ty; [ 2,11,20,29,38: #sz #sg | 3,12,21,30,39: #sz | 4,13,22,31,40: #r #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 ]
    10 #H whd in H:(??%?); destruct;
    11 [ lapply (eq_spec i zero); elim (eq i zero);
    12   [ #e >e @bool_of_val_false //;
    13   | #ne (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vint i) (Tint sz sg)) normalize #H @H /2/;
    14   ]
    15 | elim (eq_dec f Fzero);
    16   [ #e >e >(Feq_zero_true …) @bool_of_val_false //;
    17   | #ne >(Feq_zero_false …) //; (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vfloat f) (Tfloat sz)) normalize #H @H /2/;
    18   ]
    19 | @bool_of_val_false //
    20 | (* XXX hack due to destruct's normalize *) lapply (bool_of_val_true (Vptr r' b pc of) (Tpointer r ty)) normalize #H @H //
     11cases 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 ]
     12#H whd in H:(??%?);
     13[ 2: lapply (eq_spec i zero) cases (eq i zero) in H ⊢ %
     14  [ #E1 #E2 destruct @bool_of_val_false @is_false_int
     15  | #E1 #E2 >(?:r=¬false) [ @bool_of_val_true @is_true_int_int @E2 | destruct @refl ]
     16  ]
     17| 8: cases (eq_dec f Fzero)
     18  [ #e >e in H ⊢ % >Feq_zero_true #E destruct @bool_of_val_false @is_false_float
     19  | #ne >Feq_zero_false in H // #E >(?:r=¬false) [ @bool_of_val_true @is_true_float @ne | destruct @refl ]
     20  ]
     21| 14: >(?:r=false) [ @bool_of_val_false @is_false_pointer | destruct @refl ]
     22| 15: >(?:r=true) [ @bool_of_val_true @is_true_pointer_pointer | destruct @refl ]
     23| *: destruct
    2124] qed.
    2225
     
    197200    >Hv in He #He
    198201    @eval_Ederef [ 3: @He | *: skip ]
    199 | #ty #e'' #ty'' #He'' @bind2_OK #x cases x #loc #ofs #tr #H
    200   cases ty // *#pty
     202| #ty #e'' #ty'' #He'' @bind2_OK * #loc #ofs #tr #H
     203  cases ty // * #pty
    201204  cases loc in H ⊢ % * #loc' #H
    202205  whd try @I
    203   @eval_Eaddrof >H in He'' #He'' @He''
     206  @eval_Eaddrof whd in H:(??%?) >H in He'' #He'' @He''
    204207| #ty #op #e1 #He1 @bind2_OK #v1 #tr #Hv1
    205208    @opt_bind_OK #v #ev
     
    221224    @bind_OK #b
    222225    cases b; #eb lapply (exec_bool_of_val_sound … eb); #Hb
    223     @bind2_OK #v #tr #Hv
     226    @bind2_OK #v #tr #Hv whd in Hv:(??%?)
    224227    [ >Hv in He2 #He2 whd in He2 Hv:(??%?) ⊢%;
    225228        @(eval_Econdition_true … He1 ? He2) @(bool_of ??? Hb)
     
    248251| #ty #e' #ty' #i cases ty'; //;
    249252    [ #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
    250         @bind_OK #delta #Hdelta >H in He' #He'
     253        @bind_OK #delta #Hdelta whd in H:(??%?) >H in He' #He'
    251254        @(eval_Efield_struct …  He' (refl ??) Hdelta)
    252     | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H
     255    | #id #fs #He' @bind2_OK #x cases x; #sp #l #ofs #H whd in H:(??%?)
    253256        >H in He' #He'
    254257        @(eval_Efield_union … He' (refl ??))
     
    300303cases (exec_lvalue ge en m e) in ⊢ (???% → %);
    301304[ #x cases x #y cases y #loc #off #tr #H whd cases loc in H ⊢ % #locr #loci #H
    302     @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ /2/ ]
     305    @(addrof_eval_lvalue … locr … (Tpointer locr Tvoid)) [ @same_compat ]
    303306    lapply (addrof_exec_lvalue … H) #H'
    304307    lapply (exec_expr_sound ge en m (Expr (Eaddrof e) (Tpointer locr Tvoid)))
Note: See TracChangeset for help on using the changeset viewer.