Changeset 1638
 Timestamp:
 Jan 10, 2012, 4:31:27 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1637 r1638 229 229 . 230 230 231 (* The way we will use [will_return] won't satisfy Matita's guardedness check, 232 so we will measure the length of these termination proofs and use an upper 233 bound to show termination of the finite structured trace construction 234 functions. *) 235 231 236 let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝ 232 237 match T with … … 236 241  wr_base _ _ _ _ _ _ ⇒ S O 237 242 ]. 243 238 244 include alias "arithmetics/nat.ma". 239 245 246 (* Specialised to the particular situation it is used in. *) 240 247 lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False. 241 248 #ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH] … … 246 253 normalize #E destruct 247 254 qed. 248 (* 249 lemma wrl_nonzero : ∀ge,d,s,tr,T. ∀P:nat → Prop. (∀x. P (S x)) → P (will_return_length ge d s tr T). 250 #ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH] #P #H @H 251 qed. 252 *) 253 discriminator nat. 254 255 lemma will_return_call : ∀ge,depth,s,trace. 256 will_return ge depth s trace → 257 will_return ge (pred depth) s trace. 258 #ge #depth #s #trace #H elim H 259 [ #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %1 // 260  #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %2 // 261 cases d in H1 H2 ⊢ %; // 262  #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 263 cases d in H1 H2 ⊢ %; [ #H1 #H2 %4 //  /2/ ] 264  #s1 #tr #s2 #EX #trc #CL %4 // 265 ] qed. 266 267 lemma will_return_call' : ∀ge,d,s,tr,s',EX,trace. 255 256 (* Inversion lemmas on [will_return] that also note the effect on the length 257 of the proof. *) 258 lemma will_return_call : ∀ge,d,s,tr,s',EX,trace. 268 259 RTLabs_classify s = cl_call → 269 260 ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). … … 451 442 452 443 (* A bit of mucking around with the depth to avoid proving termination after 453 termination. *) 444 termination. Note that we keep a proof that our upper bound on the length 445 of the termination proof is respected. *) 454 446 record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) (limit:nat) : Type[0] ≝ { 455 447 new_state : state; … … 463 455 }. 464 456 457 (* The same with a flag indicating whether the function returned, as opposed to 458 encountering a label. *) 465 459 record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ { 466 460 ends : trace_ends_with_ret; 467 461 trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) (T ends) limit 468 462 }. 463 464 (* We often return the result from a recursive call with an addition to the 465 structured trace, so we define a couple of functions to help. The bound on 466 the size of the termination proof might need to be relaxed, too. *) 469 467 470 468 definition replace_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 → … … 488 486 (replace_trace … lGE … r trace). 489 487 488 (* Small syntax hack to avoid ambiguous input problems. *) 490 489 definition myge : nat → nat → Prop ≝ ge. 491 490 … … 498 497 (TIME: nat) 499 498 (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES)))) 500 on TIME : trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝ 499 on TIME : trace_result ge depth 500 (trace_label_return (RTLabs_status ge) s) 501 (will_return_length … TERMINATES) ≝ 502 501 503 match TIME return λTIME. TIME ≥ ? → ? with 502 504 [ O ⇒ λTERMINATES_IN_TIME. ⊥ 503 505  S TIME ⇒ λTERMINATES_IN_TIME. 504 let r ≝ make_label_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES TIME ? in 506 507 let r ≝ make_label_label ge depth s 508 trace 509 ENV_COSTLABELLED 510 STATE_COSTLABELLED 511 STATEMENT_COSTLABEL 512 TERMINATES 513 TIME ? in 505 514 match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with 506 515 [ ends_with_ret ⇒ λr. … … 508 517  doesnt_end_with_ret ⇒ λr. 509 518 let r' ≝ make_label_return ge depth (new_state … r) 510 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? (pi1 … (terminates … r)) TIME ? in 519 (remainder … r) 520 ENV_COSTLABELLED 521 (cost_labelled … r) ? 522 (pi1 … (terminates … r)) TIME ? in 511 523 replace_trace … r' 512 (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') (new_trace … r) (new_trace … r')) 524 (tlr_step (RTLabs_status ge) s (new_state … r) 525 (new_state … r') (new_trace … r) (new_trace … r')) 513 526 ] (trace_res … r) 527 514 528 ] TERMINATES_IN_TIME 529 515 530 516 531 and make_label_label ge depth s … … 522 537 (TIME: nat) 523 538 (TERMINATES_IN_TIME: myge TIME (plus 1 (times 3 (will_return_length … TERMINATES)))) 524 on TIME : sub_trace_result ge depth (λends. trace_label_label (RTLabs_status ge) ends s) (will_return_length … TERMINATES) ≝ 539 on TIME : sub_trace_result ge depth 540 (λends. trace_label_label (RTLabs_status ge) ends s) 541 (will_return_length … TERMINATES) ≝ 542 525 543 match TIME return λTIME. TIME ≥ ? → ? with 526 544 [ O ⇒ λTERMINATES_IN_TIME. ⊥ 527 545  S TIME ⇒ λTERMINATES_IN_TIME. 546 528 547 let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in 529 548 replace_sub_trace … r 530 549 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) 550 531 551 ] TERMINATES_IN_TIME 552 532 553 533 554 and make_any_label ge depth s … … 538 559 (TIME: nat) 539 560 (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES))) 540 on TIME : sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TERMINATES) ≝ 561 on TIME : sub_trace_result ge depth 562 (λends. trace_any_label (RTLabs_status ge) ends s) 563 (will_return_length … TERMINATES) ≝ 541 564 542 565 match TIME return λTIME. TIME ≥ ? → ? with 543 566 [ O ⇒ λTERMINATES_IN_TIME. ⊥ 544 567  S TIME ⇒ λTERMINATES_IN_TIME. 568 545 569 match trace return λs,trace. well_cost_labelled_state s → ∀TM:will_return ??? trace. myge ? (times 3 (will_return_length ??? trace TM)) → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with 546 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ? 570 [ ft_stop st FINAL ⇒ 571 λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ? 572 547 573  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. 548 574 match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 549 575 [ cl_other ⇒ λCL. 550 576 match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 577 (* We're about to run into a label. *) 551 578 [ true ⇒ λCS. 552 579 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ? 553 580 doesnt_end_with_ret 554 (mk_trace_result ge ??? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?) 581 (mk_trace_result ge ??? next trace' ? 582 (tal_base_not_return (RTLabs_status ge) start next ???) ?) 583 (* An ordinary step, keep going. *) 555 584  false ⇒ λCS. 556 let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? ?TIME ? in585 let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in 557 586 replace_sub_trace … r 558 (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??) 587 (tal_step_default (RTLabs_status ge) (ends … r) 588 start next (new_state … r) ? (new_trace … r) ??) 559 589 ] (refl ??) 590 560 591  cl_jump ⇒ λCL. 561 592 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ? 562 593 doesnt_end_with_ret 563 (mk_trace_result ge ??? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?) 594 (mk_trace_result ge ??? next trace' ? 595 (tal_base_not_return (RTLabs_status ge) start next ???) ?) 596 564 597  cl_call ⇒ λCL. 565 let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ??? TIME ? in 566 let r' ≝ make_any_label ge depth (new_state … r) (remainder … r) ENV_COSTLABELLED ? (pi1 … (terminates … r)) TIME ? in 598 let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in 599 let r' ≝ make_any_label ge depth 600 (new_state … r) (remainder … r) ENV_COSTLABELLED ? 601 (pi1 … (terminates … r)) TIME ? in 567 602 replace_sub_trace … r' 568 (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r')) 603 (tal_step_call (RTLabs_status ge) (ends … r') 604 start next (new_state … r) (new_state … r') ? CL ? 605 (new_trace … r) (new_trace … r')) 606 569 607  cl_return ⇒ λCL. 570 608 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ? … … 577 615 ?) 578 616 ] (refl ? (RTLabs_classify start)) 617 579 618  ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ 619 580 620 ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME 581 621 ] TERMINATES_IN_TIME. … … 597 637  @le_S_S_to_le @TERMINATES_IN_TIME 598 638  @(wrl_nonzero … TERMINATES_IN_TIME) 599  639  (* Bad  we've reached the end of the trace; need to fix semantics so that 640 this can't happen *) 600 641  @(will_return_return … CL TERMINATES) 601 642  %{tr} @EV … … 606 647  @(well_cost_labelled_jump … EV) // 607 648  @(well_cost_labelled_state_step … EV) // 608  27: @(will_return_call' … CL TERMINATES)609 649  cases r #H1 #H2 #H3 #H4 * #H5 610 cases (will_return_call '… CL TERMINATES)650 cases (will_return_call … CL TERMINATES) 611 651 #TM #X #Y @le_S_to_le @(transitive_lt … Y X) 612  (* oh dear *)652  (* TODO oh dear *) 613 653  %{tr} @EV 614 654  @(cost_labelled … r) 615 655  cases r #H72 #H73 #H74 #H75 * #H76 #H78 616 656 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) 617 cases (will_return_call '… TERMINATES) in H78;657 cases (will_return_call … TERMINATES) in H78; 618 658 #X #Y #Z 619 659 @(transitive_le … (monotonic_lt_times_r 3 … Y)) … … 623 663  @(well_cost_labelled_state_step … EV) // 624 664  @(well_cost_labelled_call … EV) // 625  cases (will_return_call' … TERMINATES) 665  skip 666  cases (will_return_call … TERMINATES) 626 667 #TM #GT @le_S_S_to_le 627 668 >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times … … 633 674  @CS 634 675  @(well_cost_labelled_state_step … EV) // 635  39: @(will_return_notfn … TERMINATES) %1 @CL636 676  cases (will_return_notfn … TERMINATES) #TM @le_S_to_le 637 677  % whd in ⊢ (% → ?); >CS #E destruct … … 639 679  %{tr} @EV 640 680  @(well_cost_labelled_state_step … EV) // 681  %1 @CL 641 682  cases (will_return_notfn … TERMINATES) #TM #GT 642 683 @le_S_S_to_le … … 651 692 ] cases daemon qed. 652 693 694 (* We can initialise TIME with a suitably large value based on the length of the 695 termination proof. *) 653 696 let rec make_label_return' ge depth s 654 697 (trace: flat_trace io_out io_in ge s)
Note: See TracChangeset
for help on using the changeset viewer.