Changeset 2507


Ignore:
Timestamp:
Nov 29, 2012, 7:14:46 PM (7 years ago)
Author:
piccolo
Message:

finished pop case in commutation eval_Seq_no_pc

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2501 r2507  
    11221122  err_to_io O I X m = return v → m = return v.
    11231123#O #I #X * #x #v normalize #EQ destruct % qed.
     1124
     1125lemma err_eq_to_io : ∀O,I,X,m,v.
     1126   m = return v → err_to_io O I X m = return v.
     1127#O #I #X #m #v #H >H //
     1128qed.
     1129
     1130lemma set_istack_sigma_commute :
     1131∀p,p',graph_prog,sigma,gss,st,is,sigma_is,prf1,prf2.
     1132sigma_is_opt p p' graph_prog sigma is = return sigma_is →
     1133set_istack ? sigma_is (sigma_state p p' graph_prog sigma gss st prf1) =
     1134sigma_state ???? gss (set_istack ? is st) prf2.
     1135#p #p' #graph_prog #sigma #gss #st #is #sigmais #prf1 #prf2 #H
     1136whd in match set_istack; normalize nodelta
     1137whd in match sigma_state; normalize nodelta
     1138whd in match sigma_is; normalize nodelta
     1139@opt_safe_elim #x #H1
     1140cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %]
     1141#EQ >EQ //
     1142qed.
    11241143
    11251144lemma eval_seq_no_pc_sigma_commute :
     
    12111230      #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)]
    12121231      normalize nodelta >m_return_bind
    1213      
    1214      
    1215      
    1216       #INUTILE #H <H
    1217      
    1218      
    1219      
    1220     inversion(istack ??) normalize nodelta [
    1221     whd in match (istack ??);
    1222     whd in match sigma_state in ⊢ (??%?); normalize nodelta
    1223   acca_store p(joint_closed_internal_function
    1224    (make_sem_lin_params p p'))
    1225   (make_sem_lin_params p p') a v st1
    1226   =return sigma_state p p' graph_prog sigma gss st' prf')
    1227 
    1228    
    1229    
    1230     cut(well_formed_state … gss st1) [ cases daemon (* to be added to gss *) ]
    1231     #wf_st1
    1232     lapply(acca_store_wf ????????? H wf_st1)
    1233     * #_ #sigma_val_spec
    1234     lapply vals_spec -vals_spec
    1235     whd in match pop; normalize nodelta
    1236     #H1 elim (bind_inversion ????? H1) -H1 * #g_bev #g_is * #ispop_spec
    1237     whd in ⊢ ((??%%) → ?); #EQ (*to be destructed*)
    1238     lapply ispop_spec -ispop_spec
    1239     whd in match is_pop; normalize nodelta
    1240     cases (istack ? st) normalize nodelta
    1241     [ #ABS whd in ABS : (???%); destruct(ABS)
    1242     | #one whd in ⊢ ((??%%) → ?); #EQ1 destruct(EQ1)
    1243       cases (istack ? (sigma_state … st prf)) normalize nodelta
    1244    
    1245     lapply (acca_store_ ???????????????????????? H)
    1246 
    1247    
    1248      -val_spec * #bv #is * #bv_is_spec
    1249     #EQ whd in EQ : (??%%); destruct(EQ)
    1250     whd in match is_pop in bv_is_spec; normalize nodelta in bv_is_spec;
    1251     inversion (istack ? st) in bv_is_spec;
    1252     [ #_ normalize nodelta whd in ⊢ ((???%) → ?); #ABS destruct(ABS)
    1253     | #bv1 #bv1_spec normalize nodelta whd in ⊢ ((??%%) → ?); #EQ destruct(EQ)
    1254     lapply(acca_store_wf ????????? H prf) check acca_store_ok check(acca_store_ok ?????????????? H)
    1255  
    1256   @(pair_reg_move_ok ? ? ? ? gss mv_sig st st' ? ?) whd in match pair_reg_move in ⊢ (%→?); normalize nodelta     
    1257     #H
    1258 qed.       
     1232      @err_eq_to_io <acca_store_commute
     1233      whd in match helper_def_store; normalize nodelta
     1234      whd in match acca_store; normalize nodelta
     1235      whd in match sigma_beval; normalize nodelta
     1236     @opt_safe_elim #xx #xx_spec
     1237     [  >xx_spec in sigma_bv_spec; #EQ destruct(EQ) //
     1238     | cut(xx =sigma_bv) [>xx_spec in sigma_bv_spec; #EQ destruct(EQ) %]
     1239       #EQ >EQ @m_bind_ext_eq #reg
     1240       change with (return set_regs (make_sem_lin_params p p') ?
     1241                                   (set_istack (make_sem_lin_params p p') ? ?) = ?);
     1242       change with (? = return set_regs ? ?
     1243                   (sigma_state p p' graph_prog sigma gss
     1244                   (set_istack ? (one_is Bv_not_used) st) ?))
     1245       >(set_istack_sigma_commute ?????? (one_is Bv_not_used) (one_is sigma_bv_not_used) ???)
     1246       [2: whd in match sigma_is_opt; normalize nodelta >sigma_bv_not_used_spec
     1247           >m_return_bind whd in ⊢ (??%%); % | % |]
     1248     ]
     1249  | (* PUSH *)
     1250     #a #H lapply(err_eq_from_io ????? H) -H #H elim (bind_inversion ????? H) -H
     1251     #val *
     1252     change with (((acca_arg_retrieve p
     1253                (joint_closed_internal_function (make_sem_graph_params p p'))
     1254                 (make_sem_graph_params p p') st a) = ?) → ?)
     1255     #graph_ret_spec
     1256     change with (((push (make_sem_graph_params p p') ? ?) = ?) → ?)
     1257     #graph_push_spec
     1258     elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf graph_ret_spec)
     1259     #val_wf #acca_arg_retrieve_commute
     1260     whd in match push in graph_push_spec; normalize nodelta  in graph_push_spec;
     1261     elim(bind_inversion ????? graph_push_spec) -graph_push_spec
     1262     #int_stack * #int_stack_spec #EQ whd in EQ : (??%%); destruct(EQ)
     1263     %
     1264     [ @hide_prf % [% [% [ @(proj1 … (proj1 … (proj1 … prf))) ]]]
     1265       [2: @(proj2 … (proj1 … prf))] [2: @(proj2 … prf)]
     1266       lapply int_stack_spec -int_stack_spec
     1267       cases int_stack
     1268       [  whd in match is_push; normalize nodelta 
     1269          cases(istack ? ?) normalize nodelta
     1270          [2: #x ] [3: #x #y] #EQ whd in EQ : (??%%); destruct(EQ)
     1271       |2,3: [#x | #y #x ] whd in match is_push; normalize nodelta
     1272        inversion(istack ? ?) normalize nodelta
     1273        [ #_ #EQ whd in EQ : (??%%); destruct(EQ)
     1274           whd in match sigma_is_opt; normalize nodelta
     1275           inversion(sigma_beval_opt ?????)
     1276           [  #EQ @⊥ elim val_wf #H @H //
     1277           |  #z #_ >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS)
     1278           ]
     1279        | #x #_ #ABS whd in ABS : (??%%); destruct(ABS)
     1280        | #x #y #_ #ABS whd in ABS : (???%); destruct(ABS)
     1281        | #_ #ABS whd in ABS : (??%%); destruct(ABS)
     1282        | #z #H #EQ whd in EQ : (??%%); destruct(EQ)
     1283          whd in match sigma_is_opt; normalize nodelta
     1284          inversion(sigma_beval_opt ???? y)
     1285          [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf)))
     1286          xxxxxxxxxxxxxxxxxx
     1287       
     1288 qed.       
    12591289       
    12601290inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
Note: See TracChangeset for help on using the changeset viewer.