Changeset 2308
 Timestamp:
 Aug 30, 2012, 7:20:43 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/CostCheck.ma
r2307 r2308 94 94 match t with 95 95 [ nil ⇒ λSC. (* single successor *) 96 let PR' ≝ ? in 97 let st' ≝ lookup_present … g h PR' in 98 if is_cost_label st' then stop_now else 96 99 match try_remove … to_check h return λx. (∀a,m'. x = ? → ?) → ? with 97 100 [ Some to_check' ⇒ λH'. 98 let PR' ≝ ? in 99 let st' ≝ lookup_present … g h PR' in 100 if is_cost_label st' then stop_now else 101 if h ∈ checking_tail then None ? else 102 check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ? 101 check_label_bounded g CL h PR' (checking::checking_tail) (\snd to_check') term_check' ? 103 102  None ⇒ λ_. 104 103 if h == checking ∨ h ∈ checking_tail then None ? else … … 121 120 successors (lookup_present … g l PR) = [ ] → 122 121 check_label_bounded_spec g l tl toch toch 123  clbs_checked : ∀l,PR,l',tl,toch. 122  clbs_checked : ∀l,PR,l',tl,toch. (* this case overlaps with clbs_cost *) 124 123 successors (lookup_present … g l PR) = [l'] → 125 124 ¬ l' ∈ toch → … … 129 128  clbs_cost : ∀l,PR,l',PR',tl,toch. 130 129 successors (lookup_present … g l PR) = [l'] → 131 l' ∈ toch →132 130 is_cost_label (lookup_present … g l' PR') → 133 131 check_label_bounded_spec g l tl toch toch … … 159 157 160 158 lemma check_label_bounded_s : ∀term_check,g,CL,checking,PR,checking_tail,to_check,TERM,to_check'. 159 (∀l. l∈to_check → ¬ l∈checking::checking_tail) → 161 160 check_label_bounded g CL checking PR checking_tail to_check term_check TERM = Some ? to_check' → 162 161 check_label_bounded_spec g checking checking_tail to_check to_check'. 163 162 #n elim n 164 163 [ #a #b #c #d #d #e #g @⊥ /3 by n_plus_1_n_to_False, div_plus_times/ (* ! *) 165  #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check' 164  #term_check #IH #g #CL #checking #PR #checking_tail #to_check #TERM #to_check' #REMOVING 166 165 whd in ⊢ (??%? → ?); 167 166 generalize in ⊢ (??(?%)? → ?); … … 169 168 cases (successors (lookup_present … PR)) in ⊢ (???% → %); 170 169 [ #SUCC whd in ⊢ (? → ??%? → ?); #_ #E destruct %1 // 171  #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' generalize in ⊢ (??(?%)? → ?); 172 lapply (refl ? (try_remove … to_check h)) 173 cases (try_remove ????) in ⊢ (???% → %); 174 [ #RM whd in ⊢ (? → ??%? → ?); #H @if_elim 175 [ #H' #E destruct 176  #H' cases (not_orb ?? H') #H1 #H2 #E destruct @(clbs_checked … SUCC) 177 [ whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) // 178  % #E >E in H1; >(proj2 … (eqb_true …) (refl ??)) * 179  assumption 170  #h * [ #SUCC whd in ⊢ (? → ??%? → ?); #PR' @if_elim 171 [ #CS #E destruct @(clbs_cost … SUCC) // 172  #NCS generalize in ⊢ (??(?%)? → ?); 173 lapply (refl ? (try_remove … to_check h)) 174 cases (try_remove ????) in ⊢ (???% → %); 175 [ #RM whd in ⊢ (? → ??%? → ?); #H @if_elim 176 [ #H' #E destruct 177  #H' cases (not_orb ?? H') #H1 #H2 #E destruct @(clbs_checked … SUCC) 178 [ whd in ⊢ (?(?%)); >(proj1 … (try_remove_empty …) RM) // 179  % #E >E in H1; >(proj2 … (eqb_true …) (refl ??)) * 180  assumption 181 ] 180 182 ] 181 ] 182  * * #to_check'' #RM #H whd in ⊢ (??%? → ?); 183 @if_elim 184 [ #CS #E destruct @(clbs_cost … SUCC … CS) 185 cases (try_remove_some ?????? RM) * #L #_ #_ whd in ⊢ (?%); >L // 186  #CS 187 @if_elim 188 [ #IN whd in ⊢ (??%? → ?); #E destruct 189  #OUT whd in ⊢ (??%? → ?); #H 190 @(clbs_step … SUCC OUT CS RM) @(IH … H) 183  * * #to_check'' #RM #H whd in ⊢ (??%? → ?); 184 whd in ⊢ (??%? → ?); #H 185 cases (try_remove_some ?????? RM) * #L1 #L2 #L3 186 @(clbs_step … SUCC ? NCS RM) 187 [ @notb_Prop @(not_to_not … (Prop_notb … (REMOVING h ?))) /2/ 188 whd in ⊢ (?%); >L1 // 189  @(IH … H) 190 #l #IN'' @notb_Prop % whd in ⊢ (?% → ?); @if_elim 191 [ #E #_ whd in IN'':(?%); >(proj1 ?? (eqb_true …) E) in IN''; 192 >L2 * 193  #NE lapply (REMOVING l ?) 194 [ whd in ⊢ (?%); cases (L3 l) [ #E destruct cases (Prop_notb … NE) #X @⊥ @X @eq_true_to_b @(proj2 ?? (eqb_true …)) % 195  #L >L @IN'' 196 ] 197  cases (l∈checking::checking_tail) * * 198 ] 199 ] 191 200 ] 192 201 ] … … 210 219 * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR 211 220 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 212 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);221 whd in ⊢ (??%?); @if_elim [ // ] #NCS generalize in ⊢ (??(?%)?); 213 222 cut (lookup … toch l' = None ?) [ whd in NIN_toch:(?(?%)); cases (lookup ????) in NIN_toch ⊢ %; [ //  * * ] ] 214 223 #L >(proj2 … (try_remove_empty …) L) #H2 215 224 whd in ⊢ (??%?); >(proj2 … (eqb_false …) NEQ) >(Prop_notb … NIN_tl) 216 225 % 217  #l #PR #l' #PR' #tl #toch #SUCC # IN #CS226  #l #PR #l' #PR' #tl #toch #SUCC #CS 218 227 * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR 219 228 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 220 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); 221 cut (lookup … toch l' = Some ? it) [ whd in IN:(?%); cases (lookup ????) in IN ⊢ %; [ *  * // ] ] 222 #L cases (try_remove_this ????? L) #to_check' #RM >RM #H2 223 whd in ⊢ (??%?); >CS whd in ⊢ (??%?); % 229 whd in ⊢ (??%?); >CS whd in ⊢ (??%?); % 224 230  #l #PR #l' #PR' #tl #toch #toch' #toch'' #SUCC #NIN #NCS #RM #H #IH 225 231 * [ #TERM @⊥ inversion TERM #E [2: #F #G #H] destruct ] #term_check' #TERM #PR 226 232 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >SUCC #H1 233 whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS)) 227 234 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?); >RM #H2 228 whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NCS))229 235 whd in ⊢ (??%?); >(not_b_to_eq_false ? (Prop_notb ? NIN)) 230 236 whd in ⊢ (??%?); >(IH term_check' ??) % … … 332 338  #IN %1 assumption 333 339 ] 334  #l #PR #l' #PR' #tl #toch #SUCC # IN #CS #INV #l'' *340  #l #PR #l' #PR' #tl #toch #SUCC #CS #INV #l'' * 335 341 [ #E destruct %2 %{1} % [ //  #l'' >SUCC * [2: *] #E destruct @boitc_here // ] 336 342  /2/ … … 379 385 ] qed. 380 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 *) 401 lemma check_label_bounded_bad : ∀g,CL,term_check,checking,PR,checking_tail,to_check,TERM. 402 (checking_tail ≠ [ ] → ¬ is_cost_label (lookup_present … g checking PR)) → 403 check_label_bounded g CL checking PR checking_tail to_check term_check TERM = None ? → 404 ∃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)). 407 #g #CL #term_check elim term_check 408 [ #A #B #C #D #TERM @⊥ inversion TERM #E try #F try #G try #H destruct 409  #term_check' #IH 410 #checking #PR #checking_tail #to_check #TERM #PRECS 411 whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); lapply (refl ? (successors (lookup_present … PR))) 412 cases (successors ?) in ⊢ (???% → %); 413 [ #H #H' whd in ⊢ (??%? → ?); #E destruct ] 414 #h * [2: #y #zs #H #H' whd in ⊢ (??%? → ?); #E destruct ] 415 #SUCC #PR' whd in ⊢ (??%? → ?); @if_elim 416 [ #CS #E destruct ] #NCS generalize in ⊢ (??(?%)? → ?); 417 cases (try_remove ????) 418 [ #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 …)) 423 [ @PR 424  >SUCC @eq_true_to_b @memb_hd 425  cases (orb_Prop_true … IN) 426 [ #E <(proj1 ?? (eqb_true …) E) in PR ⊢ %; // 427  cases checking_tail in PRECS ⊢ %; 428 [ #_ *  #h' #t #H #_ @H % #E destruct ] 429 ] 430 ] 431 ] 432  #_ #E destruct 433 ] 434  * * #to_check' #H1 whd in ⊢ (??%? → ?); 435 #CHECK' cases (IH … CHECK') 436 [ #head * #PRhead * #NCShead * 437 [ #BLL %{head} %{PRhead} % /2/ 438  * whd in ⊢ (?% → ?); @if_elim 439 [ #E #_ >(proj1 ?? (eqb_true …) E) in PRhead ⊢ %; #PRh #BLL %{h} %{PRh} %{NCS} %1 @BLL 440  #NE #INtl #BLL %{head} %{PRhead} %{NCShead} %2 % // 441 @(gl_step … BLL) 442 [ @PR 443  >SUCC @eq_true_to_b @memb_hd 444  cases checking_tail in PRECS INtl; 445 [ #_ #INc <(memb_single … INc) in PR ⊢ %; // 446  #h #t #H #_ @H % #E destruct 447 ] 448 ] 449 ] 450 ] 451  #_ // 452 ] 453 ] 454 ] qed. 455 456 457 458 381 459 let rec check_graph_bounded 382 460 (g : graph statement) … … 386 464 (start : label) 387 465 (PR : present ?? g start) 466 (REMOVED : notb (member ?? to_check start)) 388 467 (SMALLER : gt (id_map_size … g) (id_map_size … to_check)) 389 468 (term_check : nat) … … 399 478 [ None ⇒ λ_.λ_.λ_. true 400 479  Some l_to_check'' ⇒ λL,SUB',C. 401 check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ?? term_check' ?480 check_graph_bounded g CL (\snd l_to_check'') ? (\fst (\fst l_to_check'')) ??? term_check' ? 402 481 ] (choose_some … to_check') (choose_some_subset … to_check') (choose_some_card … to_check') 403 482 ] (refl ??) 404 483 ]. 405 [ 2,3,4,5: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB' 406 lapply (check_label_bounded_subset … (check_label_bounded_s … H')) #SUB'' 484 [ 2,3,4,5,6: cases l_to_check'' in C L SUB' ⊢ %; * #l * #to_check'' #C #L #SUB' 485 lapply (check_label_bounded_subset … (check_label_bounded_s … H')) 486 [ 1,3,5,7,9: #l' #IN @notb_Prop % #IS >(memb_single … IS) in IN; #IN' 487 @(absurd … IN' (Prop_notb … REMOVED)) ] 488 #SUB'' 407 489 ] 408 490 [ #id #IN @SUB @SUB'' @(SUB' ??? (refl ??)) @IN 409 491  @member_present @SUB @SUB'' cases (L ??? (refl ??)) * #L #_ #_ whd in ⊢ (?%); >L // 492  cases (L … (refl ??)) * #L1 #L2 #L3 whd in ⊢ (?(?%)); >L2 // 410 493  whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/ 411 494  whd <(C ??? (refl ??)) lapply (subset_card … SUB'') #Z @(transitive_le … Z) /2/ … … 414 497 ] qed. 415 498 416 lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR, SMALLER,TERM.499 lemma check_graph_bounded_ok : ∀g.∀CL:graph_closed g. ∀term_check,to_check,SUB,start,PR,REMOVED,SMALLER,TERM. 417 500 (∀l,PR. well_cost_labelled_statement g (lookup_present … g l PR) (CL l ? (lookup_lookup_present … PR))) → 418 check_graph_bounded g CL to_check SUB start PR SMALLER term_check TERM = true →501 check_graph_bounded g CL to_check SUB start PR REMOVED SMALLER term_check TERM = true → 419 502 (∀l. l∈g → ¬l∈to_check → l≠start → ∃n. bound_on_instrs_to_cost g l n) → 420 503 ∀l. l∈g → ∃n. bound_on_instrs_to_cost g l n. 421 504 #g #CL #term_check elim term_check 422 [ #to_check #SUB #start #PR # SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct423  #term_check' #IH #to_check #SUB #start #PR # SMALLER #TERM #WCL505 [ #to_check #SUB #start #PR #REMOVED #SMALLER #TERM @⊥ inversion TERM #A try #B try #C try #D destruct 506  #term_check' #IH #to_check #SUB #start #PR #REMOVED #SMALLER #TERM #WCL 424 507 whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); 425 508 cases (check_label_bounded ????????) in ⊢ (???% → ??(match % with [_⇒?_⇒?]?)? → ?); … … 435 518  // 436 519  @WCL 520  #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN' 521 >(memb_single … IN') in IN; // 437 522  #l' #IN_g #NIN_to_check #NEQ #_ @H // 438 523  cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E … … 454 539  // 455 540  @WCL 541  #l' #IN @notb_Prop @(not_to_not … (Prop_notb … REMOVED)) #IN' 542 >(memb_single … IN') in IN; // 456 543  #l' #IN_g #NIN_to_check #NEQ #_ @H // 457 544  cases (orb_Prop_true … CHECKED) /2/ #E %1 @(proj1 … (eqb_true …)) @E … … 491 578 [ None ⇒ λEMP. ⊥ 492 579  Some to_check ⇒ λ_.λCARD,L. 493 check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ?? (f_graph fn) ?580 check_graph_bounded (f_graph fn) (f_closed fn) (\snd to_check) ? (f_entry fn) ??? (f_graph fn) ? 494 581 ] (proj1 ?? (try_remove_empty LabelTag unit (id_set_of_map … (f_graph fn)) (f_entry fn))) 495 582 (try_remove_some_card ????) … … 506 593 ] 507 594  cases (f_entry fn) // 508  4,5: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) // 595  cases to_check in L ⊢ %; * #to_check0 #L cases (L … (refl ??)) * #L1 #L2 #L3 596 whd in ⊢ (?(?%)); >L2 // 597  5,6: <id_set_of_map_card in CARD; cases to_check * #m' #CARD >(CARD ?? (refl ??)) // 509 598 ] qed. 510 599
Note: See TracChangeset
for help on using the changeset viewer.