 Timestamp:
 Nov 29, 2012, 7:14:46 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2501 r2507 1122 1122 err_to_io O I X m = return v → m = return v. 1123 1123 #O #I #X * #x #v normalize #EQ destruct % qed. 1124 1125 lemma 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 // 1128 qed. 1129 1130 lemma set_istack_sigma_commute : 1131 ∀p,p',graph_prog,sigma,gss,st,is,sigma_is,prf1,prf2. 1132 sigma_is_opt p p' graph_prog sigma is = return sigma_is → 1133 set_istack ? sigma_is (sigma_state p p' graph_prog sigma gss st prf1) = 1134 sigma_state ???? gss (set_istack ? is st) prf2. 1135 #p #p' #graph_prog #sigma #gss #st #is #sigmais #prf1 #prf2 #H 1136 whd in match set_istack; normalize nodelta 1137 whd in match sigma_state; normalize nodelta 1138 whd in match sigma_is; normalize nodelta 1139 @opt_safe_elim #x #H1 1140 cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %] 1141 #EQ >EQ // 1142 qed. 1124 1143 1125 1144 lemma eval_seq_no_pc_sigma_commute : … … 1211 1230 #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)] 1212 1231 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. 1259 1289 1260 1290 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
Note: See TracChangeset
for help on using the changeset viewer.