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/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 #_
Note: See TracChangeset for help on using the changeset viewer.