Changeset 2845 for src/ERTLptr
 Timestamp:
 Mar 11, 2013, 6:50:48 PM (8 years ago)
 Location:
 src/ERTLptr
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLptrToLTLProof.ma
r2796 r2845 4 4 include "joint/Traces.ma". 5 5 include "common/StatusSimulation.ma". 6 7 definition stacksizes_from_model : stack_cost_model → (ident → option ℕ) ≝ 8 λm,id.find ?? 9 (λid_stack.let 〈id', stack〉 ≝ id_stack in 10 if id' == id then Some ? stack else None ?) m. 11 12 axiom ERTLptrToLTL_ok : 6 include "common/AssocList.ma". 7 8 9 10 (* Inefficient, replace with Trie lookup *) 11 definition lookup_stack_cost ≝ 12 λp.λid : ident. 13 assoc_list_lookup ? ℕ id (eq_identifier …) p. 14 15 (*TO BE MOVED*) 16 definition ERTLptr_status ≝ 17 λprog : ertlptr_program.λstack_sizes. 18 joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes). 19 20 definition LTL_status ≝ 21 λprog : ltl_program.λstack_sizes. 22 joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes). 23 24 axiom sigma_stored_pc : ertlptr_program → (block → label → list label) → 25 program_counter → program_counter. 26 27 axiom sigma_fb_state: ertlptr_program → (block → label → list label) → 28 (block → label → list register) → list register → 29 state ERTLptr_semantics → state ERTLptr_semantics. 30 31 axiom sigma_sb_state: ertlptr_program → (block → label → list label) → 32 (block → label → list register) → list register → 33 state LTL_semantics → state ERTLptr_semantics. 34 35 definition dummy_state : state ERTLptr_semantics ≝ 36 mk_state ERTL_semantics 37 (None ?) empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty. 38 39 definition dummy_state_pc : state_pc ERTLptr_semantics ≝ 40 mk_state_pc ? dummy_state (null_pc one) (null_pc one). 41 42 43 definition sigma_fb_state_pc : ertlptr_program → (block → label → list label) → 44 (block → label → list register) → 45 state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝ 46 λprog,f_lbls,f_regs,st. 47 let ge ≝ globalenv_noinit … prog in 48 let globals ≝ prog_var_names … prog in 49 match fetch_internal_function … ge (pc_block (pc … st)) with 50 [ OK y ⇒ ? 51  Error e ⇒ dummy_state_pc 52 ]. 53 cases daemon qed. 54 55 definition sigma_sb_state_pc : ertlptr_program → (block → label → list label) → 56 (block → label → list register) → state_pc LTL_semantics → state_pc ERTLptr_semantics ≝ 57 λprog,f_lbls,f_regs,st. 58 let ge ≝ globalenv_noinit … prog in 59 let globals ≝ prog_var_names … prog in 60 match fetch_internal_function … ge (pc_block (pc … st)) with 61 [ OK y ⇒ ? 62  Error e ⇒ dummy_state_pc 63 ]. 64 cases daemon qed. 65 66 67 definition ERTLptr_to_LTL_StatusSimulation : 68 ∀fix_comp : fixpoint_computer. 69 ∀colour : coloured_graph_computer. 70 ∀ prog : ertlptr_program. 71 ∀ f_lbls. ∀ f_regs. ∀f_bl_r. 72 ∀p_out,m,n. 73 ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉 → 74 let stacksizes ≝ lookup_stack_cost … m in 75 b_graph_transform_program_props ERTLptr_semantics LTL_semantics 76 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs → 77 status_rel (ERTLptr_status prog stacksizes) (LTL_status p_out stacksizes) ≝ 78 λfix_comp,colour,prog,f_lbls,f_regs,f_bl_r,p_out,m,n,EQ. 79 λgood. 80 mk_status_rel ?? 81 (* sem_rel ≝ *) (λs1:ERTLptr_status prog ?. 82 λs2: LTL_status ? ?. 83 sigma_fb_state_pc prog f_lbls f_regs s1 = sigma_sb_state_pc prog f_lbls f_regs s2) 84 (* call_rel ≝ *) 85 (λs1:Σs.as_classifier … s cl_call. 86 λs2:Σs.as_classifier … s cl_call. 87 pc … s1 =sigma_stored_pc prog f_lbls (pc … s2)) 88 (* sim_final ≝ *) ?. 89 cases daemon 90 qed. 91 92 axiom as_label_ok : 93 ∀fix_comp,colour. 94 ∀prog. 95 ∀p_out,m,n. 96 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉. 97 ∀f_lbls,f_regs. 98 ∀f_bl_r. 99 ∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 100 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 101 ∀st1,st2,fn,id,stmt. 102 let stack_sizes ≝ lookup_stack_cost m in 103 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in 104 R st1 st2 → 105 fetch_statement ERTLptr_semantics (prog_var_names … prog) 106 (globalenv_noinit … prog) (pc … st1) = return 〈id,fn,stmt〉 → 107 as_label (LTL_status p_out stack_sizes) st2 = 108 as_label (ERTLptr_status prog stack_sizes) st1. 109 110 111 112 (* 113 (* Copy the proof too from previous pass *) 114 axiom fetch_stmt_ok_sigma_state_ok : 115 ∀prog : ertlptr_program. 116 ∀ f_lbls,f_regs,id,fn,stmt,st. 117 fetch_statement ERTLptr_semantics (prog_var_names … prog) 118 (globalenv_noinit … prog) (pc ? (sigma_sb_state_pc prog f_lbls f_regs st)) = 119 return 〈id,fn,stmt〉 → 120 let added ≝ (added_registers ERTLptr (prog_var_names … prog) fn 121 (f_regs (pc_block (pc … st)))) in 122 st_no_pc … (sigma_sb_state_pc prog f_lbls f_regs st) = 123 sigma_sb_state prog f_lbls f_regs added (st_no_pc … st). 124 *) 125 126 lemma set_no_pc_eta: 127 ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1. 128 #P * // 129 qed. 130 131 lemma pc_of_label_eq : 132 ∀p,p'.let pars ≝ mk_sem_graph_params p p' in 133 ∀globals,ge,bl,i_fn,lbl. 134 fetch_internal_function ? ge bl = return i_fn → 135 pc_of_label pars globals ge bl lbl = 136 OK ? (pc_of_point ERTL_semantics bl lbl). 137 #p #p' #globals #ge #bl #i_fn #lbl #EQf 138 whd in match pc_of_label; 139 normalize nodelta >EQf >m_return_bind % 140 qed. 141 142 lemma eq_OK_OK_to_eq: ∀T,x,y. OK T x = OK T y → x=y. 143 #T #x #y #EQ destruct % 144 qed. 145 146 147 axiom pc_block_eq_sigma_commute : ∀fix_comp,colour. 148 ∀prog. 149 ∀p_out,m,n. 150 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉. 151 ∀ f_lbls,f_regs. 152 ∀f_bl_r. 153 ∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 154 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 155 ∀st1,st2. 156 let stack_sizes ≝ lookup_stack_cost m in 157 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in 158 R st1 st2 → 159 pc_block (pc … st1) = pc_block (pc … st2). 160 161 axiom change_pc_sigma_commute : ∀fix_comp,colour. 162 ∀prog. 163 ∀p_out,m,n. 164 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉. 165 ∀ f_lbls,f_regs. 166 ∀f_bl_r. 167 ∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 168 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 169 ∀st1,st2. 170 let stack_sizes ≝ lookup_stack_cost m in 171 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in 172 R st1 st2 → 173 ∀pc1,pc2.pc1 = pc2 → 174 R (set_pc … pc1 st1) (set_pc … pc2 st2). 175 176 axiom globals_commute : ∀fix_comp,colour. 177 ∀prog. 178 ∀p_out,m,n. 179 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉. 180 prog_var_names … prog = prog_var_names … p_out. 181 182 include "joint/semantics_blocks.ma". 183 include "ASM/Util.ma". 184 185 lemma eval_cond_ok : 186 ∀fix_comp,colour. 187 ∀prog. 188 ∀p_out,m,n. 189 ∀EQp_out: ertlptr_to_ltl fix_comp colour prog = 〈p_out, m, n〉. 190 ∀ f_lbls,f_regs. 191 ∀f_bl_r. 192 ∀ good :b_graph_transform_program_props ERTLptr_semantics LTL_semantics 193 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») prog f_bl_r f_lbls f_regs. 194 ∀st1,st2,st1',f,fn,a,ltrue,lfalse. 195 let stack_sizes ≝ lookup_stack_cost m in 196 let R ≝ sem_rel … (ERTLptr_to_LTL_StatusSimulation fix_comp colour … EQp_out … good) in 197 R st1 st2 → 198 fetch_statement ERTLptr_semantics … 199 (globalenv_noinit ? prog) (pc … st1) = 200 return 〈f, fn, sequential … (COND ERTLptr … a ltrue) lfalse〉 → 201 eval_state ERTLptr_semantics 202 (prog_var_names … ℕ prog) 203 (ev_genv … (mk_prog_params ERTLptr_semantics prog stack_sizes)) 204 st1 = return st1' → 205 as_costed (ERTLptr_status prog stack_sizes) st1' → 206 ∃ st2'. R st1' st2' ∧ 207 ∃taf : trace_any_any_free (LTL_status p_out stack_sizes) 208 st2 st2'. 209 bool_to_Prop (taaf_non_empty … taf). 210 #fix_comp #colour #prog #transf_prog #stack_size #maxstack #EQtransf_prog 211 #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a #ltrue #lfalse 212 #Rst1st2 213 #EQfetch whd in match eval_state; normalize nodelta >EQfetch >m_return_bind 214 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 215 whd in match eval_statement_advance; normalize nodelta 216 change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); 217 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H 218 #bv >set_no_pc_eta 219 #EQbv #H @('bind_inversion H) H * #EQbool normalize nodelta 220 lapply(fetch_statement_inv … EQfetch) * #EQfn #_ 221 [ whd in match goto; normalize nodelta >(pc_of_label_eq ??????? EQfn) >m_return_bind 222  whd in match next; normalize nodelta 223 ] 224 whd in ⊢ (??%% → ?); #EQ <(eq_OK_OK_to_eq ??? EQ) EQ st1' 225 #n_cost 226 cases(b_graph_transform_program_fetch_statement … good … EQfetch) 227 #init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta 228 [2,4: #r #tl *] #EQ >EQ init_data >if_merge_right in ⊢ (% → ?); [2,4: %] * #labs ** 229 [2,4: #hd #tl ** #_ #_ *** #pre #inst #post * whd in ⊢ (%→?); *] ** #EQlabs #EQf_regs 230 whd in match translate_step; normalize nodelta * #bl * 231 whd in ⊢ (% → ?); inversion (〈?,?〉) * #blp #blm #bls #EQ #EQbl >EQbl bl 232 letin p≝ (mk_prog_params LTL_semantics (\fst (\fst (ertlptr_to_ltl fix_comp colour prog))) (lookup_stack_cost stack_size)) 233 whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l 234 cases(? : ∃st2'.repeat_eval_seq_no_pc p f (map_eval ?? blp mid1) (st_no_pc … st2) = return (st_no_pc … st2') ∧ 235 pc … st2' = (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1) ∧ 236 last_pop … st2' = last_pop … st2) 237 [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ] 238 #st2_pre_cond ** #res_st2_pre_cond #EQpc_st2_pre_cond #EQlast_pop_st2_pre_cond 239 >(pc_block_eq_sigma_commute … EQtransf_prog … good … Rst1st2) in EQt_fn1; #EQt_fn1 240 241 xxxxxxxxxxxxxxxxxxxxxxxxxxxx 242 243 lapply(taaf_to_taa ??? 244 (produce_trace_any_any_free p st2 f t_fn1 ??? st2_pre_cond EQt_fn1 seq_pre_l res_st2_pre_cond) ?) 245 246 @(map_eval ??? mid1) lapply blp whd in match p; normalize nodelta 247 whd in match (globals ?); whd in match prog_var_names; normalize nodelta 248 change with (prog_var_names ??) in match (globals ??); 249 250 lapply(produce_trace_any_any_free p st2 ????? 251 252 253 %{(set_pc … (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) ?) st2)} 254 [ @ltrue 3: @lfalse] 255 % [1,3: @(change_pc_sigma_commute … EQtransf_prog … good … Rst1st2) 256 <(pc_block_eq_sigma_commute … EQtransf_prog … good … Rst1st2) %] 257 258 259 260 bl whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 261 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * 262 #nxt1 * #EQcond #EQ destruct(EQ) whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) 263 whd in EQmid1 : (??%%); destruct(EQmid1) 264 %{(taaf_step_jump … (taa_base …) …) I} 265 [2,5: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 266 <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind 267 >EQcond % 268 3,6: whd whd in match eval_state; normalize nodelta whd in match eval_statement_no_pc; 269 normalize nodelta whd in match fetch_statement; normalize nodelta 270 <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQt_fn1 >m_return_bind 271 >EQcond >m_return_bind normalize nodelta >m_return_bind 272 whd in match eval_statement_advance; normalize nodelta 273 change with (ps_reg_retrieve ??) in match (acca_retrieve ?????); 274 cases(ps_reg_retrieve_ok … EQbv) #bv1 * #EQbv1 #EQsem >EQbv1 275 >m_return_bind >EQsem in EQbool; #EQbool cases(bool_of_beval_ok … EQbool) 276 #bool1 * #EQbool1 #EQ destruct(EQ) >EQbool1 >m_return_bind normalize nodelta 277 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) [2: %] whd in match goto; 278 normalize nodelta >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQt_fn1; #EQt_fn1 279 >(pc_of_label_eq … EQt_fn1) >m_return_bind % 280 *: lapply n_cost whd in match as_costed; normalize nodelta 281 [ cut((mk_state_pc ERTL_semantics 282 (sigma_state prog f_lbls f_regs 283 (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn 284 (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2) 285 (pc_of_point ERTL_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) 286 (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) = 287 sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2 288 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) 289 (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize nodelta 290 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] 291 #EQ >EQ >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2 292 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) ltrue) 293 (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below *) 294  cut((mk_state_pc ERTL_semantics 295 (sigma_state prog f_lbls f_regs 296 (added_registers ERTL (prog_var_names (joint_function ERTL) ℕ prog) fn 297 (f_regs (pc_block (pc ERTLptr_semantics st2)))) st2) 298 (succ_pc ERTL_semantics (pc ERTLptr_semantics st2) 299 (point_of_succ ERTLptr_semantics 300 (point_of_pc ERTLptr_semantics 301 (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) 302 (sigma_stored_pc prog f_lbls (last_pop ERTLptr_semantics st2))) = 303 sigma_state_pc prog f_lbls f_regs (mk_state_pc ERTLptr_semantics st2 304 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) 305 (point_of_succ ERTLptr_semantics 306 (point_of_pc ERTLptr_semantics 307 (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) 308 (last_pop ERTLptr_semantics st2))) [ whd in match sigma_state_pc; normalize nodelta 309 >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in EQfn; #EQfn >EQfn %] #EQ >EQ 310 >(as_label_ok … good … (mk_state_pc ERTLptr_semantics st2 311 (pc_of_point ERTLptr_semantics (pc_block (pc ERTLptr_semantics st2)) 312 (point_of_succ ERTLptr_semantics 313 (point_of_pc ERTLptr_semantics 314 (pc ERTL_semantics (sigma_state_pc prog f_lbls f_regs st2))) nxt1)) 315 (last_pop ERTLptr_semantics st2))) [#H @H] cases daemon (*needs lemma see below ! *) 316 ] 317 qed.*) 318 319 320 theorem ERTLptrToLTL_ok : 13 321 ∀fix_comp : fixpoint_computer. 14 322 ∀colour : coloured_graph_computer. … … 16 324 let 〈p_out, m, n〉 ≝ ertlptr_to_ltl fix_comp colour p_in in 17 325 (* what should we do with n? *) 18 let stacksizes ≝ stacksizes_from_modelm in326 let stacksizes ≝ lookup_stack_cost m in 19 327 ∃[1] R. 20 328 status_simulation … … 22 330 (joint_status LTL_semantics p_out stacksizes) 23 331 R. 332 #fix_comp #colour #p_in 333 @pair_elim * #p_out #m #n #EQp_out whd 334 cases(make_b_graph_transform_program_props ERTLptr_semantics LTL_semantics 335 (λglobals,fn.«translate_data fix_comp colour globals fn,(refl …)») p_in) 336 #fregs * #f_lbls * #f_bl_r #good 337 %{(ERTLptr_to_LTL_StatusSimulation … EQp_out … good)} 338 whd in match status_simulation; normalize nodelta 339 whd in match ERTLptr_status; whd in match LTL_status; normalize nodelta 340 whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2 341 change with 342 (eval_state ERTLptr_semantics (prog_var_names ???) ?? = ? → ?) 343 #EQeval @('bind_inversion EQeval) 344 ** #id #fn #stmt #H lapply (err_eq_from_io ????? H) H #EQfetch 345 #_ whd in match ERTLptr_to_LTL_StatusSimulation; normalize nodelta #EQst2 346 cases stmt in EQfetch; stmt 347 [ * [ #cost  #called_id #args #dest #reg #lbl  #seq] #nxt  #fin_step  *] 348 #EQfetch 349 change with (joint_classify ??) in 350 ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]); 351 [ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta 352 (* XXX 353 cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne 354 %{st2'} %{taf} >tafne normalize nodelta % [ % [@I  assumption]] 355 whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *) 356 *) cases daemon 357  (*CALL*) whd in match joint_classify; normalize nodelta >EQfetch 358 normalize nodelta #is_call_st1 359 (* XXX 360 cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1' 361 * #st2_pre_call * #is_call_st2_pre_call * * #Hcall 362 #call_rel * #taa * #st2' * #sem_rel #eval_rel 363 %{(«st2_pre_call,is_call_st2_pre_call»)} % [ % assumption] 364 %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption] 365 whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*) 366 *) cases daemon 367  (*COND*) whd in match joint_classify; normalize nodelta >EQfetch 368 normalize nodelta #n_costed 369 cases(eval_cond_ok … EQp_out … good … EQst2 … EQfetch EQeval … n_costed) 370 #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@Iassumption]] 371 whd >EQst2' >(as_label_ok fix_comp colour … EQp_out … good … EQst2') [%] cases daemon (*TODO*) 372  (*seq*) XXX whd in match joint_classify; normalize nodelta >EQfetch 373 normalize nodelta 374 cases (eval_seq_no_call_ok … good … EQfetch EQeval) 375 #st3 * #EQ destruct * #taf #taf_spec %{st3} %{taf} 376 % [% //] whd >(as_label_ok … good … st3) [%] 377 cases daemon (*needs lemma about preservation of fetch_statement *) 378  cases fin_step in EQfetch; 379 [ (*GOTO*) #lbl #EQfetch whd in match joint_classify; normalize nodelta 380 >EQfetch normalize nodelta 381 cases (eval_goto_ok … good … EQfetch EQeval) 382 #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta 383 % [% //] whd >(as_label_ok … good … st3) [%] 384 cases daemon (*needs lemma about preservation of fetch_statement *) 385  (*RETURN*) #EQfetch 386 whd in match joint_classify; normalize nodelta 387 >EQfetch normalize nodelta 388 cases (eval_return_ok … good … EQfetch EQeval) #is_ret 389 * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf 390 % [2: % [2: % [2: %{(taa_base …)} %{taf}] *: ] *:] 391 % [2: whd >(as_label_ok … good … st3) [%] cases daemon (*needs lemma *)] 392 % [2: assumption] % [2: %] % [2: assumption] % assumption 393  (*TAILCALL*) * 394 ] 395 ] 396 
src/ERTLptr/Interference.ma
r2739 r2845 13 13 { colouring: vertex → decision 14 14 ; spilled_no: nat 15 ; prop_colouring: ∀l. ∀v1, v2: vertex. 15 ; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 → 16 16 lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2 17 17 ; prop_spilled_no: (*CSC: the existguarded premise is just to make the proof more general *)
Note: See TracChangeset
for help on using the changeset viewer.