Changeset 2313 for src/RTLabs/CostCheck.ma
 Timestamp:
 Aug 31, 2012, 2:39:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/CostCheck.ma
r2308 r2313 385 385 ] qed. 386 386 387 (* TODO: share with Traces.ma. *) 388 inductive bad_label_list (g:graph statement) (head:label) : label → Prop ≝ 389  gl_end : bad_label_list g head head 390  gl_step : ∀l1,l2,H. 391 l2 ∈ successors (lookup_present … g l1 H) → 392 ¬ is_cost_label (lookup_present … g l1 H) → 393 bad_label_list g head l2 → 394 bad_label_list g head l1. 395 (* 396 inductive checked_label_costs (g:graph statement) : list label → label → Prop ≝ 397  clc_start : ∀l. checked_label_costs g [ ] l 398  clc_two : ∀l,H,l'. ¬ is_cost_label (lookup_present … g l H) → checked_label_costs g [l'] l 399  clc_many : ∀h,t,l,H. ¬ is_cost_label (lookup_present … g h H) → checked_label_costs g t l → checked_label_costs g (h::t) l. 400 *) 387 include "RTLabs/CostMisc.ma". 388 401 389 lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM. 402 390 (checking_tail ≠ [ ] → ¬ is_cost_label (lookup_present … g checking PR)) → 403 391 check_label_bounded g CL checking PR checking_tail to_check term_check TERM = None ? → 404 392 ∃head,PR'. bool_to_Prop (¬ is_cost_label (lookup_present … g head PR')) ∧ 405 (bad_label_list g head head ∨ 406 (bool_to_Prop (head ∈ checking::checking_tail) ∧ bad_label_list g head checking)). 393 ((∃l. Exists ? (λl'.l'=l) (successors (lookup_present … g head PR')) ∧ 394 bad_label_list g head l) ∨ 395 (bool_to_Prop (head ∈ checking_tail) ∧ bad_label_list g head checking)). 407 396 #g #CL #term_check elim term_check 408 397 [ #A #B #C #D #TERM @⊥ inversion TERM #E try #F try #G try #H destruct … … 417 406 cases (try_remove ????) 418 407 [ #H whd in ⊢ (??%? → ?); @if_elim 419 (* base case  we've found the head of the list *) 420 [ #IN #_ %{h} % [ @PR' @eq_true_to_b @memb_hd ] % [ @NCS ] %2 % 421 [ cases (orb_Prop_true … IN) /2/ 422  @(gl_step … (gl_end …)) 408 (* base case  we've found the head of the list *) 409 [ #IN #_ cases (orb_Prop_true … IN) 410 [ (* selfloop *) #E >(proj1 ?? (eqb_true …) E) in SUCC PR' NCS; #SUCC #PR' #NCS %{checking} %{PR} 411 %{NCS} %1 %{checking} % [ >SUCC % %  // ] 412  #IN' %{h} % [ @PR' @eq_true_to_b @memb_hd ] %{NCS} %2 %{IN'} 413 @(gl_step … (gl_end …)) 423 414 [ @PR 424 415  >SUCC @eq_true_to_b @memb_hd … … 437 428 [ #BLL %{head} %{PRhead} % /2/ 438 429  * whd in ⊢ (?% → ?); @if_elim 439 [ #E #_ >(proj1 ?? (eqb_true …) E) in PRhead ⊢ %; #PRh #BLL %{h} %{PRh} %{NCS} %1 @BLL 430 [ #E #_ >(proj1 ?? (eqb_true …) E) in PRhead NCShead ⊢ %; #PRh #NCSh #BLL %{checking} %{PRh} %{NCSh} 431 %1 %{h} >SUCC % [ % %  @BLL ] 440 432  #NE #INtl #BLL %{head} %{PRhead} %{NCShead} %2 % // 441 433 @(gl_step … BLL) … … 443 435  >SUCC @eq_true_to_b @memb_hd 444 436  cases checking_tail in PRECS INtl; 445 [ #_ #INc <(memb_single … INc) in PR ⊢ %; //437 [ #_ * 446 438  #h #t #H #_ @H % #E destruct 447 439 ] … … 550 542 ] qed. 551 543 544 lemma check_graph_bounded_bad : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM. 545 check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = false → 546 ∃l. present ?? g l ∧ ∀n. ¬ bound_on_instrs_to_cost g l n. 547 #g #CL #term_check elim term_check 548 [ #a #b #c #d #e #f #TERM @⊥ inversion TERM #A try #B try #C try #D destruct 549  #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM 550 whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); 551 cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)? → ?); 552 [ #CHECK_LABEL whd in ⊢ (??%? → ?); #_ 553 cases (check_label_bounded_bad … CHECK_LABEL) 554 [ #head * #PR_head * #NCS_head * 555 [ * #next * #NEXT #BLL 556 %{head} %{PR_head} #n % #BOUND 557 cases (bound_step1 … BOUND … NEXT) #m #BOUND' 558 @(absurd ? BOUND' (loop_soundness_contradiction … NEXT NCS_head BLL m)) 559  * * 560 ] 561  * #H cases (H (refl ??)) 562 ] 563  #to_check' #CHECK_LABEL whd in ⊢ (??%? → ?); 564 generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?); 565 cases (choose LabelTag unit to_check') 566 [ #H1 #H2 #H3 whd in ⊢ (??%? → ?); #E destruct 567  * * #next * #to_check'' #H2 #H3 #H4 whd in ⊢ (??%? → ?); 568 @IH 569 ] 570 ] 571 ] qed. 572 573 552 574 (* TODO: move *) 553 575 definition id_set_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝ … … 598 620 ] qed. 599 621 600 axiomcheck_sound_cost_fn_ok : ∀fn.622 lemma check_sound_cost_fn_ok : ∀fn. 601 623 well_cost_labelled_fn fn → 602 624 bool_to_Prop (check_sound_cost_fn fn) ↔ soundly_labelled_fn fn. 603 (*604 625 #fn #WCL % 605 626 [ whd in ⊢ (?% → %); … … 624 645 ] 625 646 ] 626  TODO 627 *) 647  whd in ⊢ (% → %); #SOUND 648 lapply (refl ? (check_sound_cost_fn fn)) 649 cases (check_sound_cost_fn fn) in ⊢ (???% → %); 650 [ // 651  whd in ⊢ (??%? → %); 652 generalize in ⊢ (??(?%??)? → ?); generalize in ⊢ (? → ??(??%?)? → ?); generalize in ⊢ (? → ? → ??(???%)? → ?); 653 cases (try_remove ????) 654 [ #H1 #H2 #H3 @⊥ cases (f_entry fn) in H3; #l #PR #E 655 lapply (proj1 … (id_set_of_map_present …) PR) whd in ⊢ (% → ?); 656 >(E (refl ??)) * /3/ 657  * * #to_check #H1 #H2 #H3 658 whd in ⊢ (??%? → ?); #CHECK 659 lapply (check_graph_bounded_bad … CHECK) CHECK H1 H2 H3 660 * #l * #PR #NOT cases (SOUND l PR) #n #B 661 @(absurd ? B) @NOT 662 ] 663 ] 664 ] qed. 665 628 666 629 667 definition check_cost_program : RTLabs_program → bool ≝
Note: See TracChangeset
for help on using the changeset viewer.