Changeset 1464 for src/Cminor/toRTLabs.ma
 Timestamp:
 Oct 25, 2011, 7:12:50 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r1410 r1464 284 284 ] qed. 285 285 286 lemma present_inc : ∀le,f,l.287 ∀f':Σf':partial_fn le. fn_graph_included le f f'.286 lemma present_included : ∀le,f,f',l. 287 fn_graph_included le f f' → 288 288 present ?? (pf_graph le f) l → 289 289 present ?? (pf_graph le f') l. 290 #le #f #l * #f' * #H1 #H2 @H1 @H2 qed. 290 #le #f #f' #l * #H1 #H2 @H1 @H2 qed. 291 292 (* Some definitions for the add_stmt function later, which we introduce now so 293 that we can build the whole fn_graph_included machinery at once. *) 294 295 (* We need to show that the graph only grows, and that Cminor labels will end 296 up in the graph. *) 297 definition Cminor_labels_added ≝ λle,s,f'. 298 ∀l. Exists ? (λl'.l=l') (labels_of s) → 299 ∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'. 300 301 record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝ 302 { stmt_graph_inc : fn_graph_included ? f f' 303 ; stmt_labels_added : Cminor_labels_added le s f' 304 }. 305 306 (* Build some machinery to solve fn_graph_included goals. *) 307 308 (* A datatype saying how we intend to prove a step. *) 309 inductive fn_inc_because (le:label_env) : partial_fn le → Type[0] ≝ 310  fn_inc_eq : ∀f. fn_inc_because le f 311  fn_inc_sig : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 → 312 ∀f3:(Σf3:partial_fn le.fn_graph_included le f2 f3). fn_inc_because le f3 313  fn_inc_addinv : ∀f1,f2:partial_fn le. fn_graph_included le f1 f2 → 314 ∀s.∀f3:(Σf3:partial_fn le.add_stmt_inv le s f2 f3). fn_inc_because le f3 315 . 316 317 (* Extract the starting function for a step. *) 318 let rec fn_inc_because_left le f0 (b:fn_inc_because le f0) on b : partial_fn le ≝ 319 match b with [ fn_inc_eq f ⇒ f  fn_inc_sig f _ _ _ ⇒ f  fn_inc_addinv f _ _ _ _ ⇒ f ]. 320 321 (* Some unification hints to pick the right step to apply. The dummy variable 322 is there to provide goal that the lemma can't apply to, which causes an error 323 and forces the "repeat" tactical to stop. The first hint recognises that we 324 have reached the desired starting point. *) 325 326 unification hint 0 ≔ le:label_env, f:partial_fn le, dummy:True; 327 f' ≟ f, 328 b ≟ fn_inc_eq le f 329 ⊢ 330 fn_graph_included le f f' ≡ fn_graph_included le (fn_inc_because_left le f' b) f' 331 . 332 333 unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, f3:(Σf3:partial_fn le. fn_graph_included le f2 f3); 334 b ≟ fn_inc_sig le f1 f2 H12 f3 335 ⊢ 336 fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3 337 . 338 339 unification hint 1 ≔ le:label_env, f1:partial_fn le, f2:partial_fn le, H12 : fn_graph_included le f1 f2, s:stmt, f3:(Σf3:partial_fn le. add_stmt_inv le s f2 f3); 340 b ≟ fn_inc_addinv le f1 f2 H12 s f3 341 ⊢ 342 fn_graph_included le f1 f3 ≡ fn_graph_included le (fn_inc_because_left le f3 b) f3 343 . 344 345 (* A lemma to perform a step of the proof. We can repeat this to do the whole 346 proof. *) 347 lemma fn_includes_step : ∀le,f. ∀b:fn_inc_because le f. fn_graph_included le (fn_inc_because_left le f b) f. 348 #le #f * 349 [ #f @fn_graph_included_refl 350  #f1 #f2 #H12 * #f2 #H23 @(fn_graph_inc_trans … H12 H23) 351  #f1 #f2 #H12 #s * #f2 * #H23 #X @(fn_graph_inc_trans … H12 H23) 352 ] qed. 353 291 354 292 355 axiom BadCminorProgram : String. … … 332 395 let f ≝ add_fresh_to_graph ? (St_cost l) f ? in 333 396 «f, ?» 334 ] Env. 397 ] Env. 335 398 (* For new labels, we need to step back through the definitions of f until we 336 399 hit the point that it was added. *) 337 try @fn_graph_included_refl400 try (repeat @fn_includes_step @I) 338 401 try (#l #H @H) 339 [ 7: #l #H whd % [ @H  340 @present_inc 341 @present_inc 342 @present_inc 343 @(use_sig ? (present ???)) ] 344  8: #l #H 345 @present_inc 346 @(use_sig ? (present ???)) 347 (* For the monotonicity properties, we just keep going back until we're at the 348 start. The repeat tactical helps here. *) 349  *: repeat @fn_graph_included_sig @fn_graph_included_refl 402 [ #l #H whd % [ @H  @(present_included … (use_sig … lfalse)) repeat @fn_includes_step @I ] 403  #l #H @(present_included … (use_sig ?? resume_at)) repeat @fn_includes_step @I 350 404 ] qed. 351 405 … … 364 418 ] 365 419 ] Env pf. 366 [ // 367  2,3: normalize in pf; destruct 368  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl 420 try (repeat @fn_includes_step @I) 421 [ 1,2: normalize in pf; destruct 369 422  @Env 370 423  @(proj2 … Env) 371  normalize in pf; destruct @e0 ] qed. 424  normalize in pf; destruct @e0 425 ] qed. 372 426 373 427 axiom UnknownLabel : String. … … 417 471 qed. 418 472 419 (* We need to show that the graph only grows, and that Cminor labels will end420 up in the graph. *)421 definition Cminor_labels_added ≝ λle,s,f'.422 ∀l. Exists ? (λl'.l=l') (labels_of s) →423 ∃l'. lookup ?? le l = Some ? l' ∧ present ?? (pf_graph le f') l'.424 425 record add_stmt_inv (le:label_env) (s:stmt) (f:partial_fn le) (f':partial_fn le) : Prop ≝426 { stmt_graph_inc : fn_graph_included ? f f'427 ; stmt_labels_added : Cminor_labels_added le s f'428 }.429 430 473 lemma empty_Cminor_labels_added : ∀le,s,f'. 431 474 labels_of s = [ ] → Cminor_labels_added le s f'. … … 439 482 qed. 440 483 441 lemma fn_graph_included_inv : ∀label_env,s,f,f0. 442 ∀f':Σf':partial_fn label_env. add_stmt_inv label_env s f0 f'. 443 fn_graph_included label_env f f0 → 444 fn_graph_included label_env f f'. 445 #label_env #s #f #f0 * #f' * #H1 #H2 #H3 446 @(fn_graph_inc_trans … H3 H1) 447 qed. 448 449 lemma present_inc' : ∀le,s,f,l. 450 ∀f':(Σf':partial_fn le. add_stmt_inv le s f f'). 451 present ?? (pf_graph le f) l → 452 present ?? (pf_graph le f') l. 453 #le #s #f #l * #f' * * #H1 #H2 #H3 454 @H1 @H3 484 lemma Cminor_labels_inc : ∀le,s,f,f'. 485 fn_graph_included le f f' → 486 Cminor_labels_added le s f → 487 Cminor_labels_added le s f'. 488 #le #s #f #f' #INC #ADDED 489 #l #E cases (ADDED l E) #l' * #L #P 490 %{l'} % [ @L  @(present_included … P) @INC ] 455 491 qed. 456 492 … … 461 497 #le #s #s' #f * #f' * #H1 #H2 #H3 462 498 #l #E cases (H3 l E) #l' * #L #P 463 %{l'} % [ @L  @ present_inc' @P]499 %{l'} % [ @L  @(present_included … P) @H1 ] 464 500 qed. 465 501 … … 470 506 #le #s #f * #f' #H1 #H2 471 507 #l #E cases (H2 l E) #l' * #L #P 472 %{l'} % [ @L  @ present_inc @P]508 %{l'} % [ @L  @(present_included … P) @H1 ] 473 509 qed. 474 510 … … 580 616 try @(π2 (π1 Env)) 581 617 try @mk_add_stmt_inv 618 try (repeat @fn_includes_step @I) 582 619 try (@empty_Cminor_labels_added @refl) 583 620 try (@(All_mp … (use_sig ?? exits))) 584 try @fn_graph_included_refl585 try (repeat @fn_graph_included_inv repeat @fn_graph_included_sig @fn_graph_included_refl)586 621 try (#l #H @I) 587 622 try (#l #H @H) 588 623 [ f @(choose_regs_length … (sym_eq … Eregs)) 589  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl590 624  whd in Env @(π1 (π1 (π1 Env))) 591 625  f @(choose_regs_length … (sym_eq … Eregs)) 592  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl593 626  #l #H cases (Exists_append … H) 594 627 [ #H1 @(stmt_labels_added ???? (use_sig ?? f1) ? H1) 595  #H2 @(Cminor_labels_inv … H2) @(stmt_labels_added ???? (use_sig ?? f2)) 596 ] 597  #l #H @present_inc' @H 598  #l #H @present_inc' @use_sig 599  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl 628  @(Cminor_labels_inc ?? f2 f1 ???) [ repeat @fn_includes_step @I  @(stmt_labels_added ???? (use_sig ?? f2)) ] 629 ] 630  #l #H @(present_included … H) repeat @fn_includes_step @I 631  #l #H @(present_included … (use_sig ?? l_next)) repeat @fn_includes_step @I 600 632  #l #H cases (Exists_append … H) 601 [ #H1 @(Cminor_labels_sig … H1) @Cminor_labels_sig @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f1)) 602  #H2 @(Cminor_labels_sig … H2) @Cminor_labels_sig @Cminor_labels_sig @Cminor_labels_inv @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ?? f2)) 603 ] 604  #l #H % [ @H  @present_inc @present_inc' @present_inc @(use_sig ?? (pf_entry ? f2)) ] 605  #l #H @present_inc @present_inc' @H 606  #l #H @present_inc @H 633 [ @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f1))) repeat @fn_includes_step @I 634  @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f2))) repeat @fn_includes_step @I 635 ] 636  #l #H % [ @H  @(present_included … (use_sig ?? l2)) repeat @fn_includes_step @I ] 637  9,10: #l #H @(present_included … H) repeat @fn_includes_step @I 607 638  @(use_sig ?? (pf_entry ??)) 608  @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_sig @fn_graph_included_refl609 639  @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl  @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ] 610 640  % [ @use_sig  @(use_sig ?? exits) ] 611 641  @(equal_Cminor_labels_added ?? s) [ @refl  @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ] 612 642  #l #H @use_sig 613  #l #H @present_inc @use_sig 614  #l #H % [ @present_inc @present_inc @present_inc @present_inc @use_sig  @H ] 615  @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_sig @fn_graph_included_refl 643  #l #H @(present_included … (use_sig ?? l_default)) repeat @fn_includes_step @I 644  #l #H % [ @(present_included … (use_sig ?? l_case)) repeat @fn_includes_step @I  @H ] 616 645  @use_sig 617  @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl618 646  #l1 * [ #E >E %{l'} % [ @lookup_label_rev'  whd >lookup_add_hit % #E' destruct (E') ] 619 647 @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) 620 648 ] 621 649  #l1 #H whd %2 @lookup_label_lpresent 622  @fn_graph_included_sig @fn_graph_included_inv @fn_graph_included_refl623 650  @(equal_Cminor_labels_added ?? s') [ @refl  @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ] 624 651 ] qed. 625 626 (*627 definition mk_fn : ∀le. partial_fn le → internal_function ≝628 λle, f.629 mk_internal_function630 (pf_labgen ? f)631 (pf_reggen ? f)632 (pf_result ? f)633 (pf_params ? f)634 (pf_locals ? f)635 (pf_stacksize ? f)636 (pf_graph ? f)637 ?638 (pf_entry ? f)639 (pf_exit ? f).640 #l #s #E @(labels_P_mp … (pf_closed ? f l s E))641 #l' * [ //  #H642 *)643 652 644 653 definition c2ra_function (*: internal_function → internal_function*) ≝
Note: See TracChangeset
for help on using the changeset viewer.