Changeset 1570 for src/ASM


Ignore:
Timestamp:
Nov 25, 2011, 8:48:49 PM (8 years ago)
Author:
sacerdot
Message:

Dependent type crazyness.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1567 r1570  
    585585   start_status final_status the_trace.
    586586
     587(*
    587588(* To be moved elsewhere*)
    588589lemma le_S_n_m_to_le_n_m: ∀n,m. S n ≤ m → n ≤ m.
    589590 #n #m #H change with (pred (S n) ≤ m) @(transitive_le ? (S n)) //
    590591qed.
    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) ?) (n-b1) ?.
    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
     594include "arithmetics/bigops.ma".
     595
     596(* This shoudl go in bigops! *)
     597theorem bigop_sum_rev: ∀k1,k2,p,B,nil.∀op:Aop B nil.∀f:nat→B.
     598 \big[op,nil]_{i<k1+k2|p i} (f i) =
     599 op \big[op,nil]_{i<k2|p (i+k1)} (f (i+k1)) \big[op,nil]_{i<k1|p 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 //]
     604qed.
     605
     606(* This is taken by sigma_pi.ma that does not compile now *)
     607definition 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
     610definition natACop ≝ mk_ACop nat 0 natAop commutative_plus.
     611
     612definition natDop ≝ mk_Dop nat 0 natACop times (λn.(sym_eq ??? (times_n_O n)))
     613   distributive_times_plus.
     614
     615unification 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
     621unification 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   
     627unification hint  0 ≔ ;
     628   S ≟ natDop
     629(* ---------------------------------------- *) ⊢
     630   plus ≡ sum ? ? S.
     631
     632unification hint  0 ≔ ;
     633   S ≟ natDop
     634(* ---------------------------------------- *) ⊢
     635   times ≡ prod ? ? S.
     636
     637notation "Σ_{ ident i < n } f"
     638  with precedence 20
     639for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
     640
     641axiom 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(*
     647axiom 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
     653definition tech_cost_of_label0:
    656654 ∀cost_labels: BitVectorTrie costlabel 16.
    657655 ∀cost_map: identifier_map CostTag nat.
    658  ∀initial,final.
    659  ∀trace: trace_label_return (ASM_abstract_status cost_labels) initial final.
    660656 ∀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)
     663qed.
     664
     665lemma 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 ]
     669qed.
     670
     671lemma 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 ]
     709qed.
     710
     711
     712definition 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
     723qed.
     724
     725lemma 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 ]
     732qed.
     733
     734lemma 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
     758let 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:
    663767  let ctrace ≝ compute_cost_trace_label_return … trace in
    664768  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    ≝ ?.
     771lapply (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
     786i < |l1| →
     787tech_cost_of_label cost_labels cost_map codom_dom l1 i =
     788tech_cost_of_label cost_labels cost_map codom_dom (l2@l1) (i+|l1|)
     789
     790
     791     whd in ⊢ (??%%);
     792  |
     793  ]
     794]
    673795
    674796lemma
Note: See TracChangeset for help on using the changeset viewer.