Changeset 3491


Ignore:
Timestamp:
Sep 24, 2014, 6:15:46 PM (5 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3490 r3491  
    842842qed.
    843843
    844 
     844let rec chop (A : Type[0]) (l : list A) on l : list A ≝
     845match l with
     846[ nil ⇒ nil ?
     847| cons x xs ⇒ match xs with [ nil ⇒ nil ? | cons _ _ ⇒ x :: chop … xs]
     848].
     849
     850lemma chop_append_singleton : ∀A : Type[0].∀x : A.∀l : list A.chop ? (l@ [x]) = l.
     851#A #x #l elim l normalize // #y * normalize //
     852qed.
     853
     854lemma chop_mem : ∀A : Type[0].∀x : A.∀l : list A. mem … x (chop ? l) → mem … x l.
     855#A #x #l elim l [*] #y * [ normalize /2/] #z #zs #IH * [/2/] /3/
     856qed.
    845857
    846858lemma static_dynamic : ∀p,p',prog.
     
    859871∀a1.rel_galois … good st1 a1 →
    860872∀labels.
    861 labels = dependent_map CostLabel ? (get_costlabels_of_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
     873labels = dependent_map CostLabel ? (chop … (get_costlabels_of_trace …  t)) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
    862874rel_galois … good st2 (act_abs … abs_t (big_op … labels) (act_abs … abs_t k a1)).
    863875[2: @hide_prf
    864     cases(mem_map ????? (labels_of_trace_are_in_code … prf)) *
     876    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
    865877    #lbl' #pc * #Hmem #EQ destruct   
    866878    >(proj1 … (static_analisys_ok … EQmap … Hmem))
     
    872884  [3: cases prf
    873885  |2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in match (get_costlabels_of_trace ????);
    874       whd in match (get_costlabels_of_trace ????); cases st2 in prf; -st2 [3: #st2] *
    875       #EQpc_st2 #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); @opt_safe_elim #k_init
     886      whd in match (get_costlabels_of_trace ????);
     887      lapply(instr_map_ok … good … prf … rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] *
     888      #EQpc #EQ destruct #H whd in ⊢ (??%% → ?); whd in match (dependent_map ????);
     889      #EQ destruct >act_neutral >act_neutral normalize in H;
     890      <(act_neutral ?? (act_abs ? abs_t) a1) @H
     891  | @eqb_elim normalize nodelta
     892    [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels
     893   
     894      >(rewrite_in_dependent_map …) [2: @eq_f [2: @get_cost_label_append |]|
     895      >rewrite_in_dependent_map [2:
     896      @chop_append_singleton
     897      whd in ⊢ (??%% → ?); whd in match (dependent_map ????);
     898     
     899       >(act_neutral … a1) in H;
     900     
     901     
     902       #H #H1
     903      cases st2 in prf; -st2 [3: #st2] #prf
     904      lapply(instr_map_ok … good … prf … rel_fin)
     905     
     906       lapply prf *
     907      #EQpc_st2 #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
     908      >act_neutral >act_neutral @(instr_map_ok … good … rel_fin)
     909     
     910     
     911       @opt_safe_elim #k_init
    876912      #EQk_init whd in ⊢ (??%% → ?); whd in match (dependent_map ????); #EQ destruct
    877913      >act_neutral whd in match (big_op ??); >act_op >act_neutral
    878       @(instr_map_ok … good … rel_fin)
     914     
    879915     
    880916       #H >act_neutral whd in prf;
Note: See TracChangeset for help on using the changeset viewer.