Changeset 3400
 Timestamp:
 Dec 6, 2013, 3:14:04 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3399 r3400 190 190 eval_after_return … p' r_t (store … st) = return mem → code … st' = cd → 191 191 store … st' = mem → execute_l … (ret_act rb) st st'. 192 192 193 let rec get_labels_of_code (p : instr_params) (i : Instructions p) on i : list CostLabel ≝ 194 match i with 195 [ EMPTY ⇒ [ ] 196  RETURN x ⇒ [ ] 197  SEQ x lab instr ⇒ let ih ≝ get_labels_of_code … instr in 198 match lab with [ None ⇒ ih  Some lbl ⇒ a_non_functional_label lbl :: ih ] 199  COND x ltrue i1 lfalse i2 i3 ⇒ 200 let ih3 ≝ get_labels_of_code … i3 in 201 let ih2 ≝ get_labels_of_code … i2 in 202 let ih1 ≝ get_labels_of_code … i1 in 203 ltrue :: lfalse :: (ih1 @ ih2 @ih3) 204  LOOP x ltrue i1 lfalse i2 ⇒ 205 let ih2 ≝ get_labels_of_code … i2 in 206 let ih1 ≝ get_labels_of_code … i1 in 207 a_non_functional_label ltrue :: a_non_functional_label lfalse :: (ih1 @ ih2) 208  CALL f act_p r_lb i1 ⇒ 209 let ih1 ≝ get_labels_of_code … i1 in 210 match r_lb with [ None ⇒ ih1  Some lbl ⇒ a_return_post lbl :: ih1] 211  IO lin io lout i1 ⇒ 212 let ih1 ≝ get_labels_of_code … i1 in 213 a_non_functional_label lin :: a_non_functional_label lout :: ih1 214 ]. 215 216 include "basics/lists/listb.ma". 217 include "../src/utilities/hide.ma". 218 219 let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ 220 match l with 221 [ nil ⇒ True 222  cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs 223 ]. 224 225 lemma no_duplicates_append_r : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) → 226 no_duplicates … l2. 227 #A #l1 elim l1 // #x #xs normalize #IH #l2 * /2/ 228 qed. 229 230 lemma no_duplicates_append_l : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) → 231 no_duplicates … l1. 232 #A #l1 elim l1 // #x #xs normalize #IH #l2 * #H1 #H2 % [2: /2/ ] 233 inversion(x ∈ xs @l2) in H1; normalize [ #_ * #H @⊥ @H %] #H1 #_ 234 % inversion(x ∈ xs) normalize [2: //] #H3 #_ >(memb_append_l1 … H3) in H1; 235 #EQ destruct(EQ) 236 qed. 237 193 238 record Program (p : env_params) (p' : instr_params) : Type[0] ≝ 194 239 { env : list (env_item p p') 195 240 ; main : Instructions p' 196 241 }. 242 243 244 definition no_duplicates_labels : ∀p,p'.Program p p' → Prop ≝ 245 λp,p',prog. 246 no_duplicates … 247 (foldr … (λitem,acc.((a_call (f_lab … item)) :: get_labels_of_code … (f_body … item)) @ acc) (get_labels_of_code … (main … prog)) (env … prog)). 248 249 lemma no_duplicates_domain_of_fun: 250 ∀p,p',prog.no_duplicates_labels … prog → 251 ∀f,env_it.lookup p p' (env … prog) f = return env_it → 252 no_duplicates … (get_labels_of_code … (f_body … env_it)). 253 #p #p' * #env elim env [ #main normalize #_ #f #env_it #EQ destruct(EQ)] 254 #x #xs #IH #main whd in ⊢ (% → ?); whd in match (foldr ?????); #H #f #env_it 255 whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta 256 [ whd in ⊢ (? → ???% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) cases H #_ /2/ ] 257 #H1 #EQenv_it @IH cases H /2/ 258 qed. 259 197 260 198 261 definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.True. … … 203 266 ]. 204 267 *) 205 206 include "basics/lists/listb.ma".207 include "../src/utilities/hide.ma".208 268 209 269 definition operational_semantics : ∀p : state_params.∀p'.Program p p → abstract_status ≝ … … 648 708 ]. 649 709 650 axiom some_rel : relation (associative_list DEQCostLabel CostLabel). 651 axiom some_rel1 : relation (list CostLabel). 652 653 axiom inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ. 654 n ≥ compute_max_n … i1 → 710 711 definition same_fresh_map_on : list CostLabel → 712 relation (associative_list DEQCostLabel CostLabel) ≝ 713 λdom,m1,m2.∀x.bool_to_Prop (x ∈ dom) → get_element … m1 x = get_element … m2 x. 714 715 definition same_to_keep_on : list CostLabel → relation (list CostLabel) ≝ 716 λdom,keep1,keep2.∀x. bool_to_Prop (x ∈ dom) → (x ∈ keep1) = (x ∈ keep2). 717 718 lemma memb_not_append : ∀D : DeqSet.∀l1,l2 : list D.∀x : D. 719 x ∈ l1 = false → x ∈ l2 = false → x ∈ (l1 @ l2) = false. 720 #D #l1 elim l1 721 [ #l2 #x #_ #H @H ] 722 #x #xs #IH #l2 #x1 whd in match (memb ???); inversion (x1 == x) normalize nodelta 723 [ #_ #EQ destruct] #EQx1 #EQxs #EQl2 whd in match (memb ???); >EQx1 724 normalize nodelta @IH // 725 qed. 726 727 lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p. 728 ∀x,n,l. 729 x ∈ lab_to_keep … (call_post_trans … i n l) → x ∈ get_labels_of_code … i. 730 #p #i elim i // 731 [ #seq #opt_l #instr #IH #x #n #l whd in match (call_post_trans ????); 732 cases opt_l opt_l normalize nodelta [#lbl] 733 whd in match (get_labels_of_code ??); #H [2: @orb_Prop_r] /2/ 734  #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l 735 whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); 736 #H cases(memb_append … H) H #H @orb_Prop_r @orb_Prop_r 737 [ >memb_append_l1 // @IH1 [3: >H // *: ] 738  >memb_append_l2 // cases(memb_append … H) H #H 739 [>memb_append_l1 // @IH2 [3: >H // *: ] 740  >memb_append_l2 // @IH3 [3: >H // *: ] 741 ] 742 ] 743  #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l 744 whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); 745 #H cases(memb_append … H) H #H @orb_Prop_r @orb_Prop_r 746 [ >memb_append_l1  >memb_append_l2 ] // [ @IH1  @IH2 ] [3,6: >H *: ] // 747  #f #act_p * [#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????); 748 whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); 749 inversion(x == lbl) #Hlbl normalize nodelta 750 [* >(\P Hlbl) @orb_Prop_l @eq_costlabel_elim // * #H @H % 751  #H @orb_Prop_r @IH // 752 ] 753  #lin #io #lout #i1 #IH #x #n #l whd in match (call_post_trans ????); 754 whd in match (get_labels_of_code ??); #H @orb_Prop_r @orb_Prop_r @IH // 755 ] 756 qed. 757 758 lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A . 759 no_duplicates … (l1 @ l2) → x ∈ l1 → x ∈ l2 → False. 760 #A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???); 761 inversion (x == x1) normalize nodelta 762 [ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H % 763  #_ @IH // 764 ] 765 qed. 766 767 lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ. 768 let dom ≝ get_labels_of_code … i1 in 769 no_duplicates … dom → 655 770 ∀m,keep. 656 771 ∀info,l.call_post_trans p i1 n l = info → 657 s ome_rel(lab_map … info) m →658 s ome_rel1(lab_to_keep … info) keep →772 same_fresh_map_on dom (lab_map … info) m → 773 same_to_keep_on dom (lab_to_keep … info) keep → 659 774 call_post_clean … (t_code … info) m keep l 660 775 = return 〈gen_labels … info,i1〉. 776 #p #i1 elim i1 777 [ #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); 778 #EQ destruct(EQ) // 779  #x #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); 780 #EQ destruct(EQ) // 781  #seq * [#lbl] #instr #IH #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep 782 #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%%); normalize nodelta 783 >IH // 784 [1,4: whd whd in H2; #x #Hx @H2 whd in match (get_labels_of_code ??); // 785 @orb_Prop_r // 786 2,5: whd whd in H1; #x #Hx [ @H1 // ] cases no_dup #H3 #_ <H1 787 [2: whd in match (get_labels_of_code ??); @orb_Prop_r // ] 788 whd in ⊢ (???%); cases(eqb_true … x lbl) inversion(x == lbl) normalize nodelta 789 [2: //] #_ #H4 >H4 in Hx; // #H5 >H5 in H3; * #ABS @⊥ @ABS % 790 6: cases no_dup // 791 ] 792 normalize nodelta <(H1 lbl) 793 [2: whd in match (get_labels_of_code ??); @orb_Prop_l cases(eqb_true … (a_non_functional_label lbl) lbl) 794 #H3 #H4 >H4 % ] 795 whd in match (get_element ????); >(\b (refl …)) normalize nodelta 796 >(\b (refl …)) % 797  #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #n normalize nodelta 798 #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); 799 #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%?); >IH3 // 800 [2: #x #Hx whd in H2; inversion(x ∈ lab_to_keep … (call_post_trans …)) 801 [ #EQkeep <H2 [ >memb_append_l2 // >memb_append_l2 // ] 802 whd in match (get_labels_of_code ??); @orb_Prop_r @orb_Prop_r >memb_append_l2 // 803 >memb_append_l2 // >Hx % 804  #EQno_keep <H2 805 [2: whd in match (get_labels_of_code ??); @orb_Prop_r @orb_Prop_r 806 >memb_append_l2 // >memb_append_l2 // >Hx % ] @sym_eq @memb_not_append 807 [ @memb_not_append //] inversion(x ∈ lab_to_keep ??) // #Hlab @⊥ 808 lapply(lab_to_keep_in_domain ????? (eq_true_to_b … Hlab)) #ABS 809 cases no_dup #_ * #_ #ABS1 810 [ @(memb_no_duplicates_append … x … ABS1) // >memb_append_l2 // 811  <associative_append in ABS1; #ABS1 812 @(memb_no_duplicates_append … x … ABS1) // >memb_append_l2 // >ABS % 813 ] 814 >Hx % 815 ] 816 3: whd in H1; #x #Hx <H1 (*no duplicates *) cases daemon 817 4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) ] 818 ] 819 820 normalize nodelta >IH2 // 821 [2: #x #Hx whd in H2; (*come sopra*) cases daemon 822 3: (*no duplicates ok *) cases daemon 823 4: (* come sopra *) cases daemon 824 ] 825 >m_return_bind >IH1 // 826 [2,3,4: cases daemon (*come sopra*) ] 827 >m_return_bind normalize nodelta whd in H1; <H1 828 [2: whd in match (get_labels_of_code ??); whd in match (memb ???); 829 >(\b (refl …)) % ] whd in match (get_element ????); >(\b (refl …)) 830 normalize nodelta >(\b (refl …)) <H1 831 [2: whd in match (get_labels_of_code ??); >memb_cons // 832 whd in match (memb ???); >(\b (refl …)) % ] 833 whd in match (get_element ????); @eq_costlabel_elim normalize nodelta 834 [ #ABS cases daemon (*no duplicates *) ] #_ whd in match (get_element ????); 835 >(\b (refl …)) normalize nodelta >(\b (refl …)) % 836 *: cases daemon (*TODO*) 837 ] 838 qed. 839 661 840 662 841 definition trans_prog : ∀p,p'.Program p p' → … … 669 848 〈(mk_env_item ?? 670 849 (mk_signature ??(f_name ?? i) (f_pars … i) (f_ret … i)) 671 (f_lab … i) ( f_body … i)) :: t_env,850 (f_lab … i) (t_code … info)) :: t_env, 672 851 fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 :: 673 852 ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉) … … 717 896 #y #y1 #y2 #z #z1 #z2 #EQ destruct(EQ) #H1 #_ #EQx_xs #EQ destruct(EQ) #_ 718 897 *) 898 899 lemma trans_env_ok : ∀p : state_params.∀ prog. 900 no_duplicates_labels … prog → 901 let 〈t_prog,m,keep〉 ≝ trans_prog … prog in 902 ∀f,env_it.lookup p p (env … prog) f = return env_it → 903 let dom ≝ get_labels_of_code … (f_body … env_it) in 904 ∃env_it',n.lookup p p (env … t_prog) f = return env_it' ∧ 905 let info ≝ call_post_trans … (f_body … env_it) n (nil ?) in 906 t_code … info = f_body … env_it' ∧ 907 get_element … m (a_call (f_lab … env_it')) = (a_call (f_lab … env_it')) :: gen_labels … info ∧ 908 f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it' ∧ 909 same_fresh_map_on dom m (lab_map … info) ∧ same_to_keep_on dom keep (lab_to_keep … info). 910 #p * #env #main @pair_elim * #t_prog #m #keep whd in match trans_prog; 911 normalize nodelta @pair_elim generalize in match O; xxxx (*probably needs invariant *) elim env 912 [ * #env' #fresh #x #_ #_ #_ #f #env_it normalize in ⊢ (% → ?); #ABS destruct] 913 * #hd_sig #hd_lab #hd_code #tail #IH * #env' #fresh * #m' #keep' 914 normalize in ⊢ (% → ?); normalize nodelta @pair_elim * #env_tail #fresh_tail 915 * #m_tail #keep_tail #EQtail normalize nodelta #EQ1 #EQ2 destruct(EQ1 EQ2) 916 whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H) 917 change with (no_duplicates_labels p p (mk_Program p p tail main)) in match 918 (no_duplicates_labels p p (mk_Program p p tail main)); #no_dup_tail 919 lapply(no_duplicates_append_l … H) #no_dup_head normalize nodelta 920 #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta 921 [ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ) 922 inversion (call_post_trans … hd_code fresh_tail []) 923 #gen_labs #t_hd_code #t_fresh #t_lab_map #t_lab_to_keep #EQ_trans_code 924 %{(mk_env_item … hd_sig hd_lab t_hd_code)} %{fresh_tail} % 925 [ whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta 926 @eq_f cases hd_sig // ] >EQ_trans_code % [% [ % [ % [% // whd in ⊢ (??%?); >(\b (refl …)) %] % ] %  whd 927 #x #Hx whd in ⊢ (??%?); >(? : (x == hd_lab) = false) [2: cases daemon (*per Hhd_lab*)] 928 normalize nodelta cases daemon (* needs lemma on maps *)] 929  whd cases daemon (*using lab_to_keep_in_domain and H *) 930 ] 931  #Hf #Henv_it cases(IH … no_dup_tail … Henv_it) 932 [4: >EQtail in ⊢ (??%?); 933 934 935 [ >EQ_trans_code %  >EQ_trans_code 936 [ >EQ_trans_code %  >EQ_trans_code whd in ⊢ (??%?); 937 cases(eqb_true … (a_call hd_lab) hd_lab) #_ #H1 >(H1 (refl …)) // ]] 938 939 #EQt_prog 719 940 720 941
Note: See TracChangeset
for help on using the changeset viewer.