Changeset 1620 for src/ASM


Ignore:
Timestamp:
Dec 15, 2011, 12:23:19 AM (8 years ago)
Author:
sacerdot
Message:

One of the mutual cases of the open proof is practically finished.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1619 r1620  
    592592lemma tech_cost_of_label_shift:
    593593 ∀cost_labels,cost_map,codom_dom,l1,l2,i.
    594   i < |l1| →
     594  i < |l2| →
    595595   tech_cost_of_label cost_labels cost_map codom_dom l2 i =
    596596   tech_cost_of_label cost_labels cost_map codom_dom (l1@l2) (i+|l1|).
    597  #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H 
     597 #cost_labels #cost_Map #codom_dom #l1 #l2 #i #H
    598598 whd in match tech_cost_of_label; normalize nodelta @same_ltb_rect
    599599 [ @(ltb_rect ? i (|l2|)) @(ltb_rect ? (i+|l1|) (|l1@l2|)) #K1 #K2
     
    617617 (trace: trace_label_return (ASM_abstract_status cost_labels) initial final)
    618618 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
     619 on trace:
     620 ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
     621   block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres).
     622  let ctrace ≝ compute_cost_trace_label_return … trace in
     623  compute_max_trace_label_return_cost … trace =
     624   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
     625    ≝ ?
     626and compute_max_trace_label_label_cost_ok_with_trace
     627 (cost_labels: BitVectorTrie costlabel 16)
     628 (trace_ends_flag: trace_ends_with_ret)
     629 (cost_map: identifier_map CostTag nat)
     630 (initial: Status) (final: Status)
     631 (trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag initial final)
     632 (codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k))
    619633 (dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
    620634   block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres))
    621635 on trace:
    622   let ctrace ≝ compute_cost_trace_label_return … trace in
    623   compute_max_trace_label_return_cost … trace =
     636  let ctrace ≝ compute_cost_trace_label_label … trace in
     637  compute_max_trace_label_label_cost … trace =
    624638   (Σ_{i < |ctrace|} (tech_cost_of_label cost_labels cost_map codom_dom ctrace i))
    625639    ≝ ?.
    626 lapply (refl … initial) cases trace in ⊢ (??%? → %);
    627 [ #sb #sa #tr #_ whd in ⊢ (let ctrace ≝ % in ??%?);
    628 | #si #sl #sf #tr1 #tr2 #E whd in ⊢ (let ctrace ≝ % in ??%?);
     640cases trace
     641[ #sb #sa #tr #dom_codom
     642  @compute_max_trace_label_label_cost_ok_with_trace @dom_codom
     643| #si #sl #sf #tr1 #tr2 #dom_codom whd in ⊢ (let ctrace ≝ % in ??%?);
    629644  change with (let ctrace ≝ ? in ? = bigop (|? @ ?|) ?????)
    630645  >append_length in ⊢ (let ctrace ≝ ? in ???(?%?????));
    631646  change with (?=?) >bigop_sum_rev >commutative_plus @eq_f2
    632   [ >compute_max_trace_label_return_cost_ok_with_trace
     647  [ >(compute_max_trace_label_return_cost_ok_with_trace … cost_map … codom_dom)
    633648    -compute_max_trace_label_return_cost_ok_with_trace     
    634     [3: @cost_map
    635     |2: @codom_dom
    636     |4:lapply (code_memory_ro_label_label … tr1) >E #E2 <E2 @dom_codom]
    637     @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift
    638 
    639   |
    640   ]
     649    [2:lapply (code_memory_ro_label_label … tr1) #E2 <E2 @dom_codom]
     650    @same_bigop [//] #i #H #_ -dom_codom @tech_cost_of_label_shift //
     651  | >(compute_max_trace_label_label_cost_ok_with_trace … cost_map … codom_dom … dom_codom)
     652    @same_bigop [//] #i #H #_
    641653]
    642654(*
Note: See TracChangeset for help on using the changeset viewer.