Changeset 3491
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3490 r3491 842 842 qed. 843 843 844 844 let rec chop (A : Type[0]) (l : list A) on l : list A ≝ 845 match l with 846 [ nil ⇒ nil ? 847  cons x xs ⇒ match xs with [ nil ⇒ nil ?  cons _ _ ⇒ x :: chop … xs] 848 ]. 849 850 lemma chop_append_singleton : ∀A : Type[0].∀x : A.∀l : list A.chop ? (l@ [x]) = l. 851 #A #x #l elim l normalize // #y * normalize // 852 qed. 853 854 lemma 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/ 856 qed. 845 857 846 858 lemma static_dynamic : ∀p,p',prog. … … 859 871 ∀a1.rel_galois … good st1 a1 → 860 872 ∀labels. 861 labels = dependent_map CostLabel ? ( get_costlabels_of_trace … t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →873 labels = dependent_map CostLabel ? (chop … (get_costlabels_of_trace … t)) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) → 862 874 rel_galois … good st2 (act_abs … abs_t (big_op … labels) (act_abs … abs_t k a1)). 863 875 [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))) * 865 877 #lbl' #pc * #Hmem #EQ destruct 866 878 >(proj1 … (static_analisys_ok … EQmap … Hmem)) … … 872 884 [3: cases prf 873 885 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 876 912 #EQk_init whd in ⊢ (??%% → ?); whd in match (dependent_map ????); #EQ destruct 877 913 >act_neutral whd in match (big_op ??); >act_op >act_neutral 878 @(instr_map_ok … good … rel_fin)914 879 915 880 916 #H >act_neutral whd in prf;
Note: See TracChangeset
for help on using the changeset viewer.