Changeset 1564
- Timestamp:
- Nov 25, 2011, 3:31:40 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r1561 r1564 520 520 [ O ⇒ λ_. 0 521 521 | S m ⇒ λH. bigplus0 n f m ? ] (refl … n). 522 // 522 <H % (* Automation works, but finds an ugly proof that goes in the contexts 523 of later theorems *) 524 qed. 525 526 lemma bigplus_0: ∀n. n=0 → ∀f. bigplus n f = 0. 527 #n #E >E // 528 qed. 529 530 lemma bigplus0_extensional: 531 ∀b,f1,f2,n,K. (∀n,H. f1 n H = f2 n H) → bigplus0 b f1 n K = bigplus0 b f2 n K. 532 #b #f1 #f2 #n elim n // 533 #m #IH #K #ext normalize @eq_f2 [ @ext | @IH @ext ] 534 qed. 535 536 lemma bigplus_extensional: 537 ∀b,f1,f2. (∀n,H. f1 n H = f2 n H) → bigplus b f1 = bigplus b f2. 538 #b cases b // #n #f1 #f2 @bigplus0_extensional 539 qed. 540 541 (*CSC: !!!!!!!!!!!!!!!!!!!!!!! *) 542 axiom pi_f: ∀b. ∀f: ∀n. n < b → nat. ∀n. ∀p1,p2: n < b. f n p1 = f n p2. 543 544 axiom bigplus0_sum: 545 ∀b1,b2. ∀f:(∀n. n < b1+b2 → nat). ∀n,K. 546 bigplus0 (b1+b2) f n K = 547 if ltb n b1 then 548 bigplus0 b1 (λn,H. f n ?) n ? 549 else 550 bigplus b1 (λn,H. f n ?) + bigplus0 b2 (λn,H. f (b1+n) ?) (n-b1) ?. 551 cases daemon 552 qed. 553 554 lemma bigplus_sum: 555 ∀b1,b2. ∀f:(∀n. n < b1+b2 → nat). 556 bigplus (b1+b2) f = 557 bigplus b1 (λn,H. f n ?) + bigplus b2 (λn,H. f (b1+n) ?). 558 [2: normalize in H ⊢ %; >plus_n_Sm @le_plus // (*CSC: Automation is lost here*) 559 |3: normalize in H ⊢ %; @(transitive_le ? b1) // (*CSC: here too*) 560 | #b1 #b2 lapply (refl … (b1+b2)) cases (b1+b2) in ⊢ (??%? → ?); 561 [ #E #f cut (b1=0) [//] #E1 >bigplus_0 [2://] >bigplus_0 [2://] 562 cut (b2=0) // #E2 >bigplus_0 // 563 | #n #E #f whd in ⊢ (??%?); >bigplus0_sum 564 565 #f cases b1 566 cases (b1+b2) 567 ] 523 568 qed. 524 569 … … 530 575 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k). 531 576 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → 532 block_cost (code_memory … initial) cost_labels pc 2^16 = 533 lookup_present … k_pres). 577 block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres). 534 578 let ctrace ≝ compute_cost_trace_label_return … trace in 535 579 compute_max_trace_label_return_cost … trace = … … 537 581 [2: cases (nth_safe … i ctrace H) normalize #id * #id_pc #K 538 582 lapply (codom_dom … K) #k_pres // 539 | #cost_labels #costmap #initial #final #trace #codom_dom #dom_codom normalize nodelta 540 whd in match 583 | #cost_labels #costmap #initial #final #trace #codom_dom #dom_codom 584 cases trace 585 [ #sb #sa #tr whd in ⊢ (let ctrace ≝ % in ??%?); 586 | #si #sl #sf #tr1 #tr2 whd in ⊢ (let ctrace ≝ % in ??%?); 587 ] 541 588 542 589 lemma
Note: See TracChangeset
for help on using the changeset viewer.