Changeset 891 for src


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

Revise proofs affected by recent matita change.

Location:
src
Files:
12 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/BitVectorZ.ma

    r700 r891  
    8484    | #q #H change with ((succ one)+ (p0 p') ≤ (p0 q))
    8585      >p0_times2 >(p0_times2 q)
     86      change with (succ one * succ p' ≤ succ one * q)
    8687      @monotonic_le_times_r @IH
    8788      @le_S_S_to_le @H

  • src/Clight/Cexec.ma

    r880 r891  
    344344] qed.
    345345
    346 definition is_Sskip : ∀s:statement. (s = Sskip) + (s ≠ Sskip) ≝
    347 λs.match s return λs'.(s' = Sskip) + (s' ≠ Sskip) with
     346definition is_Sskip : ∀s:statement. (s = Sskip) ⊎ (s ≠ Sskip) ≝
     347λs.match s return λs'.(s' = Sskip) ⊎ (s' ≠ Sskip) with
    348348[ Sskip ⇒ inl ?? (refl ??)
    349349| _ ⇒ inr ?? (nmk ? (λH.?))

  • src/Clight/CexecComplete.ma

    r879 r891  
    167167| #e #ty #l #off #v #tr #H1 #H2 @(lvalue_expr … H1)
    168168    [ #id | #e' | #e' #id ] #H3
    169     whd in ⊢ (??%?);
     169    whd in ⊢ (??%?)
     170    [ change in H3:(??%?) with (exec_lvalue' ge env m (Evar id) ty)
     171    | change in H3:(??%?) with (exec_lvalue' ge env m (Ederef e') ty)
     172    | change in H3:(??%?) with (exec_lvalue' ge env m (Efield e' id) ty)
     173    ]
    170174    >(yields_eq ??? H3)
    171     whd in ⊢ (??%?); >H2 @refl
     175    whd in ⊢ (??%?) change in H2:(??%?) with (load_value_of_type' ty m 〈l,off〉)
     176    >H2 @refl
    172177| #e #ty #r #l #pc #off #tr #H1 #H2 whd in ⊢ (??%?);
    173178    >(yields_eq ??? H2) whd in ⊢ (??%?)
    … …  
    352357#ge #s #tr #s' #H elim H;
    353358[ #f #e #e1 #k #e2 #m #loc #ofs #v #m' #tr1 #tr2 #H1 #H2 #H3 whd in ⊢ (??%?);
    354     >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?);
    355     >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
     359    >(yields_eq ??? (lvalue_complete … H1)) whd in ⊢ (??%?)
     360    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?)
     361    change in H3:(??%?) with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v)
    356362    >H3 @refl
    357363| #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
    … …  
    443449    @refl
    444450| #v #f #env #k #m @refl
    445 | #v #f #env #k #m1 #m2 #loc #ofs #ty #H whd in ⊢ (??%?);
    446     >H @refl
     451| #v #f #env #k #m1 #m2 #loc #ofs #ty
     452    change in ⊢ (??%? → ?) with (store_value_of_type' ty m1 〈loc,ofs〉 v)
     453    #H whd in ⊢ (??%?) >H @refl
    447454| #f #l #s #k #env #m @refl
    448455] qed.

  • src/Clight/CexecEquiv.ma

    r798 r891  
    5252 (∀r. final_state s r → P (Some ? r)) →
    5353 ((¬∃r.final_state s r) → P (None ?)) →
    54 P (is_final ?? clight_exec s).
    55 #s #P #F #NF lapply (refl ? (is_final ?? clight_exec s))
    56 cases (is_final ?? clight_exec s) in ⊢ (???% → %)
    57 [ #E @NF % * #r #H > (is_final_complete … H) in E #H destruct
     54P (is_final s).
     55#s #P #F #NF lapply (refl ? (is_final s))
     56cases (is_final s) in ⊢ (???% → %)
     57[ #E @NF % * #r #H whd in E:(??%?) > (is_final_complete … H) in E #H destruct
    5858| #r #E @F @is_final_sound @E
    5959] qed.
     60
     61lemma is_final_elim': ∀s.∀P:option int → Type[0].
     62 (∀r. final_state s r → P (Some ? r)) →
     63 ((¬∃r.final_state s r) → P (None ?)) →
     64P (is_final io_out io_in clight_fullexec s).
     65@is_final_elim qed.
    6066
    6167lemma exec_e_step: ∀ge,x,tr,s,e.
    … …  
    6672[ #o #k #EXEC whd in EXEC:(??%?); destruct
    6773| #y cases y #tr' #s' whd in ⊢ (??%? → ?)
    68   @is_final_elim 
     74  @is_final_elim'
    6975  [ #r #FINAL | #FINAL ]
    7076  #EXEC whd in EXEC:(??%?); destruct @refl
    … …  
    7985[ #o #k #EXEC whd in EXEC:(??%?); destruct
    8086| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
    81   @is_final_elim
     87  @is_final_elim'
    8288  [ #r ] #FINAL #EXEC whd in EXEC:(??%?);
    8389  destruct @refl
    … …  
    9298[ #o #k #EXEC whd in EXEC:(??%?); destruct
    9399| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
    94   @is_final_elim [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
     100  @is_final_elim' [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
    95101| #msg #EXEC whd in EXEC:(??%?); destruct
    96102] qed.
    … …  
    143149        ]
    144150    | #x cases x; #tr' #s' >(exec_inf_aux_unfold …)
    145         whd in ⊢ (??%? → ?); @is_final_elim
     151        whd in ⊢ (??%? → ?); @is_final_elim'
    146152        [ #r ] #F #E whd in E:(??%?); destruct
    147153    | #msg >(exec_inf_aux_unfold …)
    … …  
    170176            [ #o2 #k2 #E whd in E:(??%?); destruct (E)
    171177            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
    172                 @is_final_elim
     178                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     179                @IFE
    173180                [ #r' #FINAL #E whd in E:(??%?);
    174181                    destruct (E);
    … …  
    184191       ]
    185192   | #x cases x; #tr #s whd in ⊢ (??%? → ?);
    186        @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct (E)
     193       @is_final_elim' [ #r ] #F #E whd in E:(??%?); destruct (E)
    187194   | #msg #E whd in E:(??%?); destruct (E)
    188195   ]
    … …  
    281288    [ #o #k #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    282289    | #x cases x; #tr'' #s' whd in ⊢ (??%? → ?);
    283         @is_final_elim [ #r'' #FINAL | #F ]
     290        @is_final_elim' [ #r'' #FINAL | #F ]
    284291        #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    285292    | #msg #EXEC' whd in EXEC':(??%?); destruct (EXEC');
    … …  
    299306>(exec_inf_aux_unfold …) cases x;
    300307[ #o #k #EXEC whd in EXEC:(??%?); destruct;
    301 | #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim
     308| #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim'
    302309  [ #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
    303310      destruct (EXEC); @refl
    … …  
    365372    cases (exec_step ge s);
    366373  [ #o #k #msg' #EXEC whd in EXEC:(??%?); destruct
    367   | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim
     374  | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim'
    368375      [ #r ] #F #EXEC whd in EXEC:(??%?); destruct
    369376  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%?); destruct @refl
    … …  
    381388    cases (exec_step ge s);
    382389    [ #o #k #EXEC whd in EXEC:(??%?); destruct
    383     | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim
     390    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim'
    384391        [ #r ] #F #E whd in E:(??%?); destruct @F
    385392    | #msg #E whd in E:(??%?); destruct
    … …  
    409416            [ #o2 #k2 #EXECK whd in EXECK:(??%?); destruct
    410417            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
    411                 @is_final_elim [ #r ] #F #EXECK
     418                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%)
     419                @IFE [ #r ] #F #EXECK
    412420                whd in EXECK:(??%?); destruct;
    413421                @(absurd ?? F)
    … …  
    419427        ]
    420428    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?);
    421         @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct;
     429        @is_final_elim' [ #r ] #F #E whd in E:(??%?); destruct;
    422430    | #msg #E whd in E:(??%?); destruct
    423431    ]
    … …  
    707715    ]
    708716| #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?)
    709     @is_final_elim [ #r ] #F #E whd in E:(?%?);
     717    @is_final_elim' [ #r ] #F #E whd in E:(?%?);
    710718    inversion E;
    711719    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
    … …  
    898906                #F #S whd in S:(?%?); cases (se_inv … S);
    899907            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
    900                 @is_final_elim [ #r ] #F #S whd in S:(?%?);
     908                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
    901909                cases (se_inv … S);
    902910            | #msg #S cases (se_inv … S);
    … …  
    915923                #F #S whd in S:(?%?); cases (se_inv … S);
    916924            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?)
    917                 @is_final_elim [ #r ] #F #S whd in S:(?%?);
     925                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
    918926                cases (se_inv … S);
    919927            | #msg #S cases (se_inv … S);
    … …  
    9951003  ∃e'.e = e_step ??? E0 s e'.
    9961004#ge #s #e >(exec_inf_aux_unfold …)
    997 whd in ⊢ (??%? → ?) @is_final_elim
     1005whd in ⊢ (??%? → ?) @is_final_elim'
    9981006[ #r #FINAL #EXEC #NOTFINAL
    9991007    @False_ind @(absurd ?? NOTFINAL)
    … …  
    10091017#classic #constructive_indefinite_description #p #e
    10101018whd in ⊢ (?%? → ??(λ_.?(?%?)%));
    1011 lapply (make_initial_state_sound p);
    1012 lapply (the_initial_state p);
    1013 cases (make_initial_state p);
     1019lapply (make_initial_state_sound p)
     1020lapply (the_initial_state p)
     1021whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?)
     1022cases (make_initial_state p)
    10141023[ #gs cases gs; #ge #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
    10151024    cases INITIAL; #Ege #INITIAL''
    1016     >(exec_inf_aux_unfold …)
     1025    >exec_inf_aux_unfold
    10171026    whd in ⊢ (?%? → ?)
    1018     @is_final_elim
     1027    @is_final_elim'
    10191028    [ #r #F @False_ind
    10201029        @(absurd ?? (initial_state_not_final … INITIAL''))
    … …  
    10251034    lapply (behavior_of_execution ??
    10261035              (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
    1027         *; #b #MATCHES %{b} % //;
     1036        *; #b #MATCHES %{b} % [ @MATCHES ]
    10281037        #ge' >Ege #Ege' >(?:ge' = ge) [ 2: destruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ]
    10291038        inversion MATCHES;

  • 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)))

  • src/Clight/TypeComparison.ma

    r882 r891  
    1616
    1717let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
    18 match t1 return λt'. (t' = t2) + (t' ≠ t2) with
    19 [ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    20 | Tint sz sg ⇒ match t2 return λt'. (Tint ?? = t') + (Tint ?? ≠ t')  with [ Tint sz' sg' ⇒
     18match t1 return λt'. Sum (t' = t2) (t' ≠ t2) with
     19[ Tvoid ⇒ match t2 return λt'. Sum (Tvoid = t') (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     20| Tint sz sg ⇒ match t2 return λt'. Sum (Tint ?? = t') (Tint ?? ≠ t')  with [ Tint sz' sg' ⇒
    2121    match sz_eq_dec sz sz' with [ inl e1 ⇒
    2222    match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???
    … …  
    2424    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    2525    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    26 | Tfloat f ⇒ match t2 return λt'. (Tfloat ? = t') + (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
     26| Tfloat f ⇒ match t2 return λt'. Sum (Tfloat ? = t') (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
    2727    match fs_eq_dec f f' with [ inl e1 ⇒ inl ???
    2828    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    2929    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    30 | Tpointer s t ⇒ match t2 return λt'. (Tpointer ?? = t') + (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
     30| Tpointer s t ⇒ match t2 return λt'. Sum (Tpointer ?? = t') (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
    3131    match eq_region_dec s s' with [ inl e1 ⇒
    3232      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
    3333      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
    3434    | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    35 | Tarray s t n ⇒ match t2 return λt'. (Tarray ??? = t') + (Tarray ??? ≠ t')  with [ Tarray s' t' n' ⇒
     35| Tarray s t n ⇒ match t2 return λt'. Sum (Tarray ??? = t') (Tarray ??? ≠ t')  with [ Tarray s' t' n' ⇒
    3636    match eq_region_dec s s' with [ inl e1 ⇒
    3737      match type_eq_dec t t' with [ inl e2 ⇒
    … …  
    4141        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    4242        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    43 | Tfunction tl t ⇒ match t2 return λt'. (Tfunction ?? = t') + (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
     43| Tfunction tl t ⇒ match t2 return λt'. Sum (Tfunction ?? = t') (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
    4444    match typelist_eq_dec tl tl' with [ inl e1 ⇒
    4545    match type_eq_dec t t' with [ inl e2 ⇒ inl ???
    … …  
    4848  | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    4949| Tstruct i fl ⇒
    50     match t2 return λt'. (Tstruct ?? = t') + (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
     50    match t2 return λt'. Sum (Tstruct ?? = t') (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
    5151    match ident_eq i i' with [ inl e1 ⇒
    5252    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
    … …  
    5555    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    5656| Tunion i fl ⇒
    57     match t2 return λt'. (Tunion ?? = t') + (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
     57    match t2 return λt'. Sum (Tunion ?? = t') (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
    5858    match ident_eq i i' with [ inl e1 ⇒
    5959    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
    … …  
    6161    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    6262    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
    63 | Tcomp_ptr r i ⇒ match t2 return λt'. (Tcomp_ptr ? ? = t') + (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
     63| Tcomp_ptr r i ⇒ match t2 return λt'. Sum (Tcomp_ptr ? ? = t') (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
    6464    match eq_region_dec r r' with [ inl e1 ⇒
    6565      match ident_eq i i' with [ inl e2 ⇒ inl ???
    … …  
    6868    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    6969]
    70 and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
    71 match tl1 return λtl'. (tl' = tl2) + (tl' ≠ tl2) with
    72 [ Tnil ⇒ match tl2 return λtl'. (Tnil = tl') + (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    73 | Tcons t1 ts1 ⇒ match tl2 return λtl'. (Tcons ?? = tl') + (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
     70and typelist_eq_dec (tl1,tl2:typelist) : Sum (tl1 = tl2) (tl1 ≠ tl2) ≝
     71match tl1 return λtl'. Sum (tl' = tl2) (tl' ≠ tl2) with
     72[ Tnil ⇒ match tl2 return λtl'. Sum (Tnil = tl') (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     73| Tcons t1 ts1 ⇒ match tl2 return λtl'. Sum (Tcons ?? = tl') (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
    7474    match type_eq_dec t1 t2 with [ inl e1 ⇒
    7575    match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ???
    … …  
    7777    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
    7878]
    79 and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
    80 match fl1 return λfl'. (fl' = fl2) + (fl' ≠ fl2) with
    81 [ Fnil ⇒ match fl2 return λfl'. (Fnil = fl') + (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
    82 | Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. (Fcons ??? = fl') + (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
     79and fieldlist_eq_dec (fl1,fl2:fieldlist) : Sum (fl1 = fl2) (fl1 ≠ fl2) ≝
     80match fl1 return λfl'. Sum (fl' = fl2) (fl' ≠ fl2) with
     81[ Fnil ⇒ match fl2 return λfl'. Sum (Fnil = fl') (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
     82| Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. Sum (Fcons ??? = fl') (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
    8383    match ident_eq i1 i2 with [ inl e1 ⇒
    8484      match type_eq_dec t1 t2 with [ inl e2 ⇒

  • src/common/Mem.ma

    r790 r891  
    6666  ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block -> A.
    6767  update_block … x v f x = v.
    68 #A * * #ix #v #f whd in ⊢ (??%?);
    69 >(eqZb_z_z …) //;
     68#A * * #ix #v #f whd in ⊢ (??%?)
     69>eq_block_b_b //
    7070qed.
    7171

  • src/common/Smallstep.ma

    r700 r891  
    133133#tr #ge #s1 #t1 #s2 #t2 #s3 #t3 #Hstar #Hstep #e1 inversion Hstar;
    134134[ #s2' #e2 #e3 #e4 destruct; @plus_one //;
    135 | #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 destruct;
    136     >(Eapp_assoc …) @(plus_left … H1)
     135| #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5
     136    >e1 >e4 >e2 >Eapp_assoc destruct @(plus_left … H1)
    137137    [ 2: @(star_right … H2 Hstep) //;
    138138    | skip;

  • src/common/Values.ma

    r797 r891  
    6464| @H2 % #E destruct elim H3 /2/
    6565] qed.
     66
     67lemma eq_block_b_b : ∀b. eq_block b b = true.
     68* * #z whd in ⊢ (??%?) >eqZb_z_z @refl
     69qed.
    6670
    6771(* Characterise the memory regions which the pointer representations can
    … …  
    12251229lemma sign_ext_lessdef:
    12261230  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
    1227 #n #v1 #v2 #H inversion H;//;#v #e1 #e2 <e1 in H >e2 //;
     1231#n #v1 #v2 #H inversion H // #v #e1 #e2 whd in ⊢ (?%?) //
    12281232qed.
    12291233(*

  • src/utilities/binary/Z.ma

    r697 r891  
    333333|#n cases y;
    334334   [@nmk #H elim (not_eq_OZ_pos n);#H2 /2/;
    335    |#m @eqb_elim
     335   |#m normalize @eqb_elim
    336336      [//
    337337      | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) //
    … …  
    341341   [@nmk #H elim (not_eq_OZ_neg n);#H /2/;
    342342   |#m @nmk #H destruct
    343    |#m @eqb_elim
     343   |#m normalize @eqb_elim
    344344      [//
    345345      | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) //
    … …  
    458458
    459459theorem sym_Zplus : ∀x,y:Z. x+y = y+x.
    460 #x #y cases x;
    461 [>(Zplus_z_OZ ?) (*XXX*) //
     460#x #y cases x
     461[>Zplus_z_OZ //
    462462|#p cases y
    463463   [//
    464    |normalize;//
    465    |#q normalize;>(pos_compare_n_m_m_n ??) (*XXX*)
     464   |//
     465   |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n
    466466      cases (pos_compare q p);//]
    467467|#p cases y
    468468   [//;
    469    |#q normalize;>(pos_compare_n_m_m_n ??) (*XXX*)
     469   |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n
    470470      cases (pos_compare q p);//
    471471   |normalize;//]
    … …  
    503503  ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
    504504#n #m
    505 normalize;
     505whd in ⊢ (??%%)
    506506<(pos_compare_S_S …)
    507 >(partialminus_S_S …)
    508 >(partialminus_S_S …) //;
     507>(minus_S_S …)
     508>(minus_S_S …) //;
    509509qed.
    510510
    … …  
    521521#n #m @(pos_cases … n) @(pos_cases … m)
    522522[ //;
    523 | #m' >(Zpred_pos_succ …)
    524     >(?:pos (succ m') = Zsucc (pos m')) //;
    525 | #m' normalize; >(pos_compare_S_one …) normalize;
    526     >(partial_minus_S_one …) normalize; >(pos_nonzero …)
    527     <(pred_succ_n …) //;
    528 | #m' #n' normalize; <(pos_compare_S_S …)
    529     >(partialminus_S_S …)
    530     >(partialminus_S_S …)
    531     >(pos_nonzero …)
    532     >(pos_nonzero …)
    533     <(pred_succ_n …)
    534     <(pred_succ_n …)
     523| #m' >Zpred_pos_succ
     524    change in ⊢ (??(??%)?) with (Zsucc (pos m'))
     525    <Zpred_Zplus_neg_O >Zpred_Zsucc @refl
     526| #m' whd in ⊢ (??%%) >pos_compare_S_one normalize;
     527    >partial_minus_S_one normalize; >pos_nonzero
     528    <pred_succ_n //
     529| #m' #n' whd in ⊢ (??%%) <pos_compare_S_S
     530    >minus_S_S
     531    >minus_S_S normalize
     532    >pos_nonzero
     533    >pos_nonzero
     534    <pred_succ_n
     535    <pred_succ_n
    535536    normalize; //;
    536537] qed.
    … …  
    600601
    601602lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m.
    602 #n #m normalize; <(pos_compare_S_S …)
    603 >(partialminus_S_S …)
    604 >(partialminus_S_S …)
     603#n #m whd in ⊢ (??%%) <pos_compare_S_S
     604>minus_S_S >minus_S_S
    605605 //; qed.
    606606
    … …  
    676676#x #y cases x
    677677[cases y;//
    678 |*:#n cases y;//;#m normalize;@pos_compare_elim normalize;//]
     678|*:#n cases y;//;#m whd in ⊢ (??(?%)%) @pos_compare_elim normalize;//]
    679679qed.
    680680
    … …  
    686686#x cases x
    687687[//
    688 |*:#n normalize;>(pos_compare_n_n ?) //]
     688|*:#n whd in ⊢ (??%?) >pos_compare_n_n //]
    689689qed.
    690690

  • src/utilities/binary/positive.ma

    r697 r891  
    10951095  [ LT ⇒ n < m
    10961096  | EQ ⇒ n = m
    1097   | GT ⇒ m < n ]) ?????) (* FIXME: don't want to put all these ?, especially when … does not work! *)
     1097  | GT ⇒ m < n ]))
    10981098[1,2:@pos_cases
    10991099  [ 1,3: /2/;
    11001100  | 2,4: #m' cases m'; //;
    11011101  ]
    1102 |#n1 #m1 normalize;<(pos_compare_S_S …) cases (pos_compare n1 m1);
    1103    [1,3:normalize;#IH @le_succ_succ //;
    1104    |normalize;#IH >IH //]
     1102|#n1 #m1 <pos_compare_S_S cases (pos_compare n1 m1)
     1103   [1,3: #IH @le_succ_succ //
     1104   | #IH >IH //
     1105   ]
     1106]
    11051107qed.
    11061108

  • src/utilities/extralib.ma

    r882 r891  
    119119
    120120lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
    121 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y);
    122 /3/; cases x; /3/; qed.
     121#x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
     122/3/ whd in ⊢ (% → ??%) /3/ qed.
    123123
    124124lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
    125 #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y);
    126 cases x; /3/; qed.
     125#x #y whd in ⊢ (??%) lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
     126whd in ⊢ (% → ??%) /3/ qed.
    127127
    128128theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
    … …  
    327327  ∀A:Type[0]. ∀l1,l2:list A.
    328328    l1 @ l2 = [] → l1 = [] ∧ l2 = [].
    329 #A #l1 #l2 cases l1;
    330 [ cases l2;
     329#A #l1 #l2 cases l1
     330[ cases l2
    331331  [ /2/
    332   | #h #t #H destruct;
    333   ]
    334 | cases l2;
    335   [ normalize; #h #t #H destruct;
    336   | normalize; #h1 #t1 #h2 #h3 #H destruct;
     332  | normalize #h #t #H destruct
     333  ]
     334| cases l2
     335  [ normalize #h #t #H destruct
     336  | normalize #h1 #t1 #h2 #h3 #H destruct
    337337  ]
    338338] qed.
Note: See TracChangeset for help on using the changeset viewer.