Changeset 1570 for src/ASM/CostsProof.ma
 Timestamp:
 Nov 25, 2011, 8:48:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1567 r1570 585 585 start_status final_status the_trace. 586 586 587 (* 587 588 (* To be moved elsewhere*) 588 589 lemma le_S_n_m_to_le_n_m: ∀n,m. S n ≤ m → n ≤ m. 589 590 #n #m #H change with (pred (S n) ≤ m) @(transitive_le ? (S n)) // 590 591 qed. 591 592 (* Here I would like to use arithmetics/bigops.ma, but it requires the 593 function f to be total on nat, which is not the case here *) 594 let rec bigplus0 (b:nat) (f: ∀n:nat. n < b → nat) (n:nat) on n ≝ 595 match n return λn.n < b → nat with 596 [ O ⇒ λ_. 0 597  S k ⇒ λH. f k ? + bigplus0 b f k ? 598 ]. 599 @(le_S_n_m_to_le_n_m … H) 600 qed. 601 602 definition bigplus ≝ 603 λn,f. 604 match n return λx. x = n → nat with 605 [ O ⇒ λ_. 0 606  S m ⇒ λH. bigplus0 n f m ? ] (refl … n). 607 <H % (* Automation works, but finds an ugly proof that goes in the contexts 608 of later theorems *) 609 qed. 610 611 lemma bigplus_0: ∀n. n=0 → ∀f. bigplus n f = 0. 612 #n #E >E // 613 qed. 614 615 lemma bigplus0_extensional: 616 ∀b,f1,f2,n,K. (∀n,H. f1 n H = f2 n H) → bigplus0 b f1 n K = bigplus0 b f2 n K. 617 #b #f1 #f2 #n elim n // 618 #m #IH #K #ext normalize @eq_f2 [ @ext  @IH @ext ] 619 qed. 620 621 lemma bigplus_extensional: 622 ∀b,f1,f2. (∀n,H. f1 n H = f2 n H) → bigplus b f1 = bigplus b f2. 623 #b cases b // #n #f1 #f2 @bigplus0_extensional 624 qed. 625 626 (*CSC: !!!!!!!!!!!!!!!!!!!!!!! *) 627 axiom pi_f: ∀b. ∀f: ∀n. n < b → nat. ∀n. ∀p1,p2: n < b. f n p1 = f n p2. 628 629 axiom bigplus0_sum: 630 ∀b1,b2. ∀f:(∀n. n < b1+b2 → nat). ∀n,K. 631 bigplus0 (b1+b2) f n K = 632 if ltb n b1 then 633 bigplus0 b1 (λn,H. f n ?) n ? 634 else 635 bigplus b1 (λn,H. f n ?) + bigplus0 b2 (λn,H. f (b1+n) ?) (nb1) ?. 636 cases daemon 637 qed. 638 639 lemma bigplus_sum: 640 ∀b1,b2. ∀f:(∀n. n < b1+b2 → nat). 641 bigplus (b1+b2) f = 642 bigplus b1 (λn,H. f n ?) + bigplus b2 (λn,H. f (b1+n) ?). 643 [2: normalize in H ⊢ %; >plus_n_Sm @le_plus // (*CSC: Automation is lost here*) 644 3: normalize in H ⊢ %; @(transitive_le ? b1) // (*CSC: here too*) 645  #b1 #b2 lapply (refl … (b1+b2)) cases (b1+b2) in ⊢ (??%? → ?); 646 [ #E #f cut (b1=0) [//] #E1 >bigplus_0 [2://] >bigplus_0 [2://] 647 cut (b2=0) // #E2 >bigplus_0 // 648  #n #E #f whd in ⊢ (??%?); >bigplus0_sum 649 650 #f cases b1 651 cases (b1+b2) 652 ] 653 qed. 654 655 lemma compute_max_trace_label_return_cost_ok_with_trace: 592 *) 593 594 include "arithmetics/bigops.ma". 595 596 (* This shoudl go in bigops! *) 597 theorem bigop_sum_rev: ∀k1,k2,p,B,nil.∀op:Aop B nil.∀f:nat→B. 598 \big[op,nil]_{i<k1+k2p i} (f i) = 599 op \big[op,nil]_{i<k2p (i+k1)} (f (i+k1)) \big[op,nil]_{i<k1p i} (f i). 600 #k1 #k2 #p #B #nil #op #f >bigop_sum >commutative_plus @same_bigop #i @leb_elim normalize 601 [2,4: // 602  #H1 #H2 <plus_minus_m_m // 603  #H1 #H2 #H3 <plus_minus_m_m //] 604 qed. 605 606 (* This is taken by sigma_pi.ma that does not compile now *) 607 definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n)) 608 (λa,b,c.sym_eq ??? (associative_plus a b c)). 609 610 definition natACop ≝ mk_ACop nat 0 natAop commutative_plus. 611 612 definition natDop ≝ mk_Dop nat 0 natACop times (λn.(sym_eq ??? (times_n_O n))) 613 distributive_times_plus. 614 615 unification hint 0 ≔ ; 616 S ≟ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n)) 617 (λa,b,c.sym_eq ??? (associative_plus a b c)) 618 (*  *) ⊢ 619 plus ≡ op ? ? S. 620 621 unification hint 0 ≔ ; 622 S ≟ mk_ACop nat 0 (mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n)) 623 (λa,b,c.sym_eq ??? (associative_plus a b c))) commutative_plus 624 (*  *) ⊢ 625 plus ≡ op ? ? S. 626 627 unification hint 0 ≔ ; 628 S ≟ natDop 629 (*  *) ⊢ 630 plus ≡ sum ? ? S. 631 632 unification hint 0 ≔ ; 633 S ≟ natDop 634 (*  *) ⊢ 635 times ≡ prod ? ? S. 636 637 notation "Σ_{ ident i < n } f" 638 with precedence 20 639 for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}. 640 641 axiom code_memory_ro_label_label: 642 ∀cost_labels. ∀ends_flag. 643 ∀initial,final. trace_label_label (ASM_abstract_status cost_labels) ends_flag initial final → 644 code_memory … initial = code_memory … final. 645 646 (* 647 axiom code_memory_ro_label_return: 648 ∀cost_labels. 649 ∀initial,final. trace_label_return (ASM_abstract_status cost_labels) initial final → 650 code_memory … initial = code_memory … final. 651 *) 652 653 definition tech_cost_of_label0: 656 654 ∀cost_labels: BitVectorTrie costlabel 16. 657 655 ∀cost_map: identifier_map CostTag nat. 658 ∀initial,final.659 ∀trace: trace_label_return (ASM_abstract_status cost_labels) initial final.660 656 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k). 661 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → 662 block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres). 657 ∀ctrace:list (Σk:costlabel.∃pc. lookup_opt costlabel 16 pc cost_labels = Some ? k). 658 ∀i,p. present … cost_map (nth_safe ? i ctrace p). 659 #cost_labels #cost_map #codom_dom #ctrace #i #p 660 cases (nth_safe … i ctrace ?) normalize #id * #id_pc #K 661 lapply (codom_dom … K) #k_pres >(lookup_lookup_present … k_pres) 662 % #abs destruct (abs) 663 qed. 664 665 lemma ltb_rect: 666 ∀P:Type[0].∀n,m. (n < m → P) → (¬ n < m → P) → P. 667 #P #n #m lapply (refl … (ltb n m)) cases (ltb n m) in ⊢ (???% → %); #E #H1 #H2 668 [ @H1 @leb_true_to_le @E  @H2 @leb_false_to_not_le @E ] 669 qed. 670 671 lemma same_ltb_rect: 672 ∀P,n,m,H1,H2,n',m',H1',H2'. 673 ltb n m = ltb n' m' → (∀x,y. H1 x = H1' y) → (∀x,y. H2 x = H2' y) → 674 ltb_rect P n m H1 H2 = 675 ltb_rect P n' m' H1' H2'. 676 #P #n #m #H1 #H2 #n' #m' #H1' #H2' #E #K1 #K2 whd in ⊢ (??%?); 677 cut (∀xxx,yyy,xxx',yyy'. 678 match ltb n m 679 return λx:bool. 680 eq bool (ltb n m) x 681 → (lt n m → P) → (Not (lt n m) → P) → P 682 with 683 [ true ⇒ 684 λE0:eq bool (ltb n m) true. 685 λH10:lt n m → P. 686 λH20:Not (lt n m) → P. H10 (xxx E0) 687  false ⇒ 688 λE0:eq bool (ltb n m) false. 689 λH10:lt n m → P. 690 λH20:Not (lt n m) → P. H20 (yyy E0)] 691 (refl … (ltb n m)) H1 H2 = 692 match ltb n' m' 693 return λx:bool. 694 eq bool (ltb n' m') x 695 → (lt n' m' → P) → (Not (lt n' m') → P) → P 696 with 697 [ true ⇒ 698 λE0:eq bool (ltb n' m') true. 699 λH10:lt n' m' → P. 700 λH20:Not (lt n' m') → P. H10 (xxx' E0) 701  false ⇒ 702 λE0:eq bool (ltb n' m') false. 703 λH10:lt n' m' → P. 704 λH20:Not (lt n' m') → P. H20 (yyy' E0)] 705 (refl … (ltb n' m')) H1' H2' 706 ) [2: #X @X] 707 >E cases (ltb n' m') #xxx #yyy #xxx' #yyy' normalize 708 [ @K1  @K2 ] 709 qed. 710 711 712 definition tech_cost_of_label: 713 ∀cost_labels: BitVectorTrie costlabel 16. 714 ∀cost_map: identifier_map CostTag nat. 715 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k). 716 list (Σk:costlabel.∃pc. lookup_opt costlabel 16 pc cost_labels = Some ? k) → 717 nat → nat 718 ≝ λcost_labels,cost_map,codom_dom,ctrace,i. 719 ltb_rect ? i (ctrace) 720 (λH. lookup_present ?? cost_map (nth_safe ? i ctrace H) ?) 721 (λ_.0). 722 @tech_cost_of_label0 @codom_dom 723 qed. 724 725 lemma shift_nth_safe: 726 ∀T,i,l2,l1,K1,K2. 727 nth_safe T i l1 K1 = nth_safe T (i+l2) (l2@l1) K2. 728 #T #i #l2 elim l2 normalize 729 [ #l1 #K1 <plus_n_O #K2 % 730  #hd #tl #IH #l1 #K1 <plus_n_Sm #K2 change with (? < ?) in K1; change with (? < ?) in K2; 731 whd in ⊢ (???%); @IH ] 732 qed. 733 734 lemma tech_cost_of_label_shift: 735 ∀cost_labels,cost_map,codom_dom,l1,l2,i. 736 i < l1 → 737 tech_cost_of_label cost_labels cost_map codom_dom l2 i = 738 tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) (i+l1). 739 #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H 740 cut (ltb i (l2) = ltb (i+l1) (l1@l2)) 741 [ change with (leb ?? = leb ??); @leb_elim 742 [ #H1 change with (i < ?) in H1; >le_to_leb_true [//] change with (? < ?) 743 >append_length >commutative_plus @monotonic_lt_plus_r // 744  #H1 change with (¬ i < ?) in H1; >not_le_to_leb_false [//] 745 >append_length >commutative_plus % #H2 746 change with (? < ?) in H2; @(absurd ?? H1) @(lt_plus_to_lt_r … H2) ] 747  #E whd in match tech_cost_of_label; normalize nodelta 748 @same_ltb_rect [@E] 749 [ #K1 #K2 lapply (shift_nth_safe ? i l1 l2 K1 K2) #H check eq_f 750 lapply (eq_f ?? (lookup_present CostTag nat cost_Map) ?? H) 751 752 753 754 cut (decide_bool (ltb i (l2)) = decide_bool (ltb (i+(l1)) (l1@l2))) 755 whd in match tech_cost_of_label; normalize nodelta 756 757 758 let rec compute_max_trace_label_return_cost_ok_with_trace 759 (cost_labels: BitVectorTrie costlabel 16) 760 (cost_map: identifier_map CostTag nat) 761 (initial: Status) (final: Status) 762 (trace: trace_label_return (ASM_abstract_status cost_labels) initial final) 763 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k)) 764 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → 765 block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres)) 766 on trace: 663 767 let ctrace ≝ compute_cost_trace_label_return … trace in 664 768 compute_max_trace_label_return_cost … trace = 665 bigplus (ctrace) (λi,H.lookup_present … cost_map (nth_safe ? i ctrace H) ?). 666 [2: cases (nth_safe … i ctrace H) normalize #id * #id_pc #K 667 lapply (codom_dom … K) #k_pres // 668  #cost_labels #costmap #initial #final #trace #codom_dom #dom_codom 669 cases trace 670 [ #sb #sa #tr whd in ⊢ (let ctrace ≝ % in ??%?); 671  #si #sl #sf #tr1 #tr2 whd in ⊢ (let ctrace ≝ % in ??%?); 672 ] 769 Σ_{i < ctrace} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i) 770 ≝ ?. 771 lapply (refl … initial) cases trace in ⊢ (??%? → %); 772 [ #sb #sa #tr #_ whd in ⊢ (let ctrace ≝ % in ??%?); 773  #si #sl #sf #tr1 #tr2 #E whd in ⊢ (let ctrace ≝ % in ??%?); 774 change with (let ctrace ≝ ? in ? = bigop (? @ ?) ?????) 775 >append_length in ⊢ (let ctrace ≝ ? in ???(?%?????)); 776 change with (?=?) >bigop_sum_rev >commutative_plus @eq_f2 777 [ >compute_max_trace_label_return_cost_ok_with_trace 778 compute_max_trace_label_return_cost_ok_with_trace 779 [3: @cost_map 780 2: @codom_dom 781 4:lapply (code_memory_ro_label_label … tr1) >E #E2 <E2 @dom_codom] 782 @same_bigop [//] #i #H #_ dom_codom 783 generalize in match (compute_cost_trace_label_return cost_labels sl sf tr2); #l1 784 generalize in match (compute_cost_trace_label_label cost_labels doesnt_end_with_ret si sl tr1); 785 786 i < l1 → 787 tech_cost_of_label cost_labels cost_map codom_dom l1 i = 788 tech_cost_of_label cost_labels cost_map codom_dom (l2@l1) (i+l1) 789 790 791 whd in ⊢ (??%%); 792  793 ] 794 ] 673 795 674 796 lemma
Note: See TracChangeset
for help on using the changeset viewer.