Changeset 1564


Ignore:
Timestamp:
Nov 25, 2011, 3:31:40 PM (8 years ago)
Author:
sacerdot
Message:

Commit where we use a dependently typed version of bigops.
I am now going to try to revert it to the standard version, so this
commit is to keep trace of the old version.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1561 r1564  
    520520 [ O ⇒ λ_. 0
    521521 | 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 *)
     524qed.
     525
     526lemma bigplus_0: ∀n. n=0 → ∀f. bigplus n f = 0.
     527 #n #E >E //
     528qed.
     529
     530lemma 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 ]
     534qed.
     535
     536lemma 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
     539qed.
     540
     541(*CSC: !!!!!!!!!!!!!!!!!!!!!!! *)
     542axiom pi_f: ∀b. ∀f: ∀n. n < b → nat. ∀n. ∀p1,p2: n < b. f n p1 = f n p2.
     543
     544axiom 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
     552qed.
     553
     554lemma 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 ]
    523568qed.
    524569
     
    530575 ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
    531576 ∀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).
    534578  let ctrace ≝ compute_cost_trace_label_return … trace in
    535579  compute_max_trace_label_return_cost … trace =
     
    537581 [2: cases (nth_safe … i ctrace H) normalize #id * #id_pc #K
    538582   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   ]
    541588
    542589lemma
Note: See TracChangeset for help on using the changeset viewer.