Changeset 1510


Ignore:
Timestamp:
Nov 16, 2011, 4:38:41 PM (8 years ago)
Author:
sacerdot
Message:

All files ported to new dependent inversion.

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1244 r1510  
    6363initial_state p s → initial_state p s' → s = s'.
    6464#p #s #s' #H1 #H2
    65 inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15
    66 inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25
     65inversion H1; #b1 #f1 #ge1 #m1 #e11 #e12 #e13 #e14 #e15 #e16
     66inversion H2; #b2 #f2 #ge2 #m2 #e21 #e22 #e23 #e24 #e25 #e26
    6767>e11 in e21 #e1 >(?:ge1 = ge2) in e13 e14
    6868[ 2: destruct (e1) skip (e11); @refl ]
     
    8484#p #s cases p; #globs #fns #main #H
    8585inversion H;
    86 #b #f #ge #m #e1 #e2 #e3 #e4 #e5
     86#b #f #ge #m #e1 #e2 #e3 #e4 #e5 #e6
    8787whd in ⊢ (??%?);
    8888>e2
     
    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 <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 ⊢ (??%?);
    451     whd; inversion H2; [ #sz #sg #x | #x #sz ] #e5 #e6 #e7 %{ x} whd in ⊢ (??%?);
     451    whd; inversion H2; [ #sz #sg #x | #x #sz ] #e5 #e6 #e7 #e8 %{ x} whd in ⊢ (??%?);
    452452    @refl
    453453| #v #f #env #k #m @refl
  • src/Clight/CexecEquiv.ma

    r1352 r1510  
    118118[ #tr #r #m #E1 #E2 destruct
    119119| #tr #s #e #se #H1 #H2 #E (* destruct (E) ;*)
    120   cases (se_step_eq … E) * #E1 #E2 #E3 >E1 >E2 >E3
     120  cases (se_step_eq … E) * #E1 #E2 #E3 #E4 >E1 >E2 >E3
    121121    >(exec_e_step_inv … H2)
    122122    <(exec_e_step … H2) in H1 #H1 % //
     
    133133| #tr #s #e #se #H1 #H2 #E destruct (E)
    134134| #msg #_ #E destruct
    135 | #o #k #i #se #H1 #H2 #E destruct (E);
     135| #o #k #i #se #H1 #H2 #E #X destruct (E);
    136136    lapply (exec_step_sound ge s0);
    137137    cases (exec_step ge s0) in H2 ⊢ %;
     
    141141        inversion H1;
    142142        [ #tr #r #m #E1 #E2 destruct
    143         | #tr' #s' #e' #se' #H2 #H3 #E2 destruct (E2);
     143        | #tr' #s' #e' #se' #H2 #H3 #E2 #_ destruct (E2);
    144144            <(exec_e_step … H3) in H2 #H2 % [ 2: @H2 ]
    145145            lapply (STEP i);
     
    164164| #tr #s #e #se #H1 #H2 #E destruct (E)
    165165| #msg #_ #E destruct
    166 | #o #k #i #se #H1 #H2 #E destruct (E);
     166| #o #k #i #se #H1 #H2 #E #_ destruct (E);
    167167    lapply (exec_step_sound ge s0);
    168168    >(exec_inf_aux_unfold …) in H2;
     
    172172        #STEP
    173173        inversion H1;
    174         [ #tr #r #m #E1 #E2 lapply (STEP i); destruct;
     174        [ #tr #r #m #E1 #E2 #_ lapply (STEP i); destruct;
    175175            >(exec_inf_aux_unfold …) in E1;
    176176            cases (k' i);
     
    284284whd in EXEC;
    285285inversion EXEC;
    286 [ #tr' #r' #m' #EXEC' #E destruct (E);
     286[ #tr' #r' #m' #EXEC' #E #_ destruct (E);
    287287    lapply (exec_step_sound ge s);
    288288    >(exec_inf_aux_unfold …) in EXEC';
     
    294294    | #msg #EXEC' whd in EXEC':(??%??); destruct (EXEC');
    295295    ]
    296     inversion FINAL; #r''' #m' #E1 #E2 #H destruct (E1 E2);
     296    inversion FINAL; #r''' #m' #E1 #E2 #_ #H destruct (E1 E2);
    297297    @H
    298298| #tr' #s' #e' #se' #H #EXEC' #E destruct
     
    321321  star (mk_transrel … step) ge s tr (Returnstate (Vint I32 r) Kstop m).
    322322#ge #tr0 #s0 #r #m #e0 #H inversion H;
    323 [ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC
     323[ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
    324324    destruct (E1 E2 E3 E4 E5);
    325325    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
     
    329329    | @refl
    330330    ]
    331 | #s #s' #tr #tr' #r #e #m #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC
     331| #s #s' #tr #tr' #r #e #m #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
    332332    destruct;
    333333    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
     
    345345cut (∃s'.∃e'.∃tr'.∃tr''.(And (And (And (execution_reacting tr'' s' e') (execution_isteps tr' s e s' e')) (tr' ≠ E0)) (tr = tr'⧻tr'')));
    346346[ inversion REACTS;
    347     #tr0 #tr' #s0 #s' #e0 #e' #EREACTS #ESTEPS #REACTED #E1 #E2 #E3 destruct (E2 E3);
     347    #tr0 #tr' #s0 #s' #e0 #e' #EREACTS #ESTEPS #REACTED #E1 #E2 #E3 #_ destruct (E2 E3);
    348348    %{ s'} %{ e'} %{ tr0} %{ tr'} % [ % [ % //; | @REACTED ] | @refl ]
    349349| *; #s' *; #e' *; #tr' *; #tr''
     
    371371[ #tr #r #m #EXEC #E destruct (E)
    372372| #tr #s' #e #e' #H #EXEC #E destruct (E)
    373 | >(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 …)
    374375    cases (exec_step ge s);
    375376  [ #o #k #msg' #EXEC whd in EXEC:(??%??); destruct
     
    386387#ge #s #tr #s' #e #H whd in H; inversion H;
    387388[ #tr' #r #m #EXEC #E destruct
    388 | #tr' #s'' #e' #e'' #H #EXEC #E destruct (E);
     389| #tr' #s'' #e' #e'' #H #EXEC #E #_ destruct (E);
    389390    >(exec_inf_aux_unfold …) in EXEC;
    390391    cases (exec_step ge s);
     
    407408| #tr' #s'' #e' #e'' #H #EXEC #E destruct (E);
    408409| #msg #EXEC #E destruct
    409 | #o' #k' #i' #e' #H #EXEC #E destruct;
     410| #o' #k' #i' #e' #H #EXEC #E #_ destruct;
    410411    >(exec_inf_aux_unfold …) in EXEC;
    411412    cases (exec_step ge s);
     
    413414        inversion H;
    414415        [ #tr1 #r1 #m1 #EXECK #E destruct (E);
    415         | #tr1 #s1 #e1 #e2 #H1 #EXECK #E destruct (E);
     416        | #tr1 #s1 #e1 #e2 #H1 #EXECK #E #_ destruct (E);
    416417            >(exec_inf_aux_unfold …) in EXECK;
    417418            cases (k1 i');
     
    443444  (¬∃r. final_state s' r).
    444445#ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG;
    445 #tr #s #s' #e #msg #ESTEPS #E1 #E2 #E3 #E4 #EXEC #NOTFINAL destruct (E1 E2 E3 E4);
     446#tr #s #s' #e #msg #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC #NOTFINAL destruct (E1 E2 E3 E4);
    446447cases (several_steps … ESTEPS EXEC);
    447448#STAR #EXEC' %
     
    821822          #NOTOVER inversion NOTOVER;
    822823          [ #tr' #s' #e' #E destruct (E);
    823           | #o' #k' #tr' #s' #e' #i' #E destruct (E);
     824          | #o' #k' #tr' #s' #e' #i' #E #_ destruct (E);
    824825              %{ tr'} %{s'} %{e'} % //;
    825826              cases (several_steps … INITIAL EXEC); #_ #EXEC1
     
    934935  execution_terminates tr s (se_step tr' s' e) r m → s = s'.
    935936#tr #tr' #s #s' #e #r #m #H inversion H;
    936 [ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl
    937 | #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl
     937[ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl
     938| #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl
    938939] qed.
    939940
     
    941942  execution_diverges tr s (se_step tr' s' e) → s = s'.
    942943#tr #tr' #s #s' #e #H inversion H;
    943 #tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 destruct; @refl qed.
     944#tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed.
    944945
    945946lemma exec_state_reacts: ∀tr,tr',s,s',e.
    946947  execution_reacts tr s (se_step tr' s' e) → s = s'.
    947948#tr #tr' #s #s' #e #H inversion H;
    948 #tr1 #s1 #e1 #H' #E1 #E2 #E3 destruct; @refl qed.
     949#tr1 #s1 #e1 #H' #E1 #E2 #E3 #_ destruct; @refl qed.
    949950
    950951lemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
    951952  execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'.
    952953#tr #tr' #s #s' #s'' #e #H inversion H;
    953 #tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 destruct; @refl qed.
     954#tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed.
    954955
    955956lemma behavior_of_execution: ∀s,e.
     
    10221023            #TERM
    10231024            lapply (exec_state_terminates … TERM); #E1
    1024             >E1 in TERM #TERM
     1025            >E1 in TERM #TERM #_
    10251026            @(program_terminates (mk_transrel … step) ?? ge s)
    10261027            [ 2: @INITIAL
     
    10311032        | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES #DIVERGES
    10321033            lapply (exec_state_diverges … DIVERGES);
    1033             #E1 >E1 in DIVERGES #DIVERGES
     1034            #E1 >E1 in DIVERGES #DIVERGES #_
    10341035            inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6
    10351036            <E4 in INITSTEPS ⊢ % <E5 in E6 ⊢ % #E6 #INITSTEPS
    10361037            cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
    10371038            #E7 <E7 in INITSTEPS #INITSTEPS
    1038             cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV
     1039            cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV #_
    10391040            @(program_diverges (mk_transrel … step) ?? ge s … INITIAL)
    10401041            [ 2: <Ege @INITSTAR
     
    10431044        | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS #REACTS
    10441045            lapply (exec_state_reacts … REACTS);
    1045             #E1 >E1 in REACTS #REACTS
     1046            #E1 >E1 in REACTS #REACTS #_
    10461047            inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5
    10471048            <E4 in REACTING ⊢ % <E5 #REACTING #E6
    10481049            cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
    1049             #E7 <E7 in REACTING #REACTING
     1050            #E7 <E7 in REACTING #REACTING #_
    10501051            @(program_reacts (mk_transrel … step) ?? ge s … INITIAL)
    10511052            <Ege @(reacts_sound … REACTING EXEC')
    10521053        | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG #WRONG
    10531054            lapply (exec_state_wrong … WRONG);
    1054             #E1 >E1 in WRONG #WRONG
     1055            #E1 >E1 in WRONG #WRONG #_
    10551056            inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7
    10561057            <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG
     
    10581059            #E8 <E8 in GOESWRONG #GOESWRONG
    10591060            elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL
    1060             <Ege
     1061            <Ege #_
    10611062            @(program_goes_wrong (mk_transrel … step) ?? ? s … INITIAL STAR STOP)
    10621063            #r % #F @(absurd ?? FINAL) %{r} @F
  • src/Clight/CexecSound.ma

    r1410 r1510  
    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 <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);
     
    288288    | #a #b #c #d #e #f #g #h #i #j #k #bad destruct (bad);
    289289    ]
    290 | #e' #ty' #r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); @H'
     290| #e' #ty' #r' #loc' #ofs' #tr' #H' #pc' #e1 #e2 #e3 destruct (e1 e2 e3); #E @H'
    291291| #a #b #c #d #e #f #g #h #i #bad destruct (bad);
    292292| #a #b #c #d #e #f #g #h #i #j #k #l #k #l #bad destruct (bad);
  • src/common/Smallstep.ma

    r891 r1510  
    132132  plus tr ge s1 t s3.
    133133#tr #ge #s1 #t1 #s2 #t2 #s3 #t3 #Hstar #Hstep #e1 inversion Hstar;
    134 [ #s2' #e2 #e3 #e4 destruct; @plus_one //;
    135 | #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5
     134[ #s2' #e2 #e3 #e4 #e5s destruct; @plus_one //;
     135| #s1' #t1' #s1'' #t1'' #s2' #t2' #H1 #H2 #e2 #foo #e3 #e4 #e5 #e6
    136136    >e1 >e4 >e2 >Eapp_assoc destruct @(plus_left … H1)
    137137    [ 2: @(star_right … H2 Hstep) //;
     
    140140    ]
    141141]
    142 qed. 
     142qed.
    143143(*
    144144Lemma plus_left':
  • src/common/Values.ma

    r1369 r1510  
    10981098  ∀chunk,v1,v2.
    10991099  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
    1100 #chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 cases chunk
    1101 [ 8: #r ] whd in ⊢ (?%?); //; 
     1100#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 #e3 cases chunk
     1101[ 8: #r ] whd in ⊢ (?%?); //;
    11021102qed.
    11031103
Note: See TracChangeset for help on using the changeset viewer.