Changeset 3400


Ignore:
Timestamp:
Dec 6, 2013, 3:14:04 PM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3399 r3400  
    190190   eval_after_return … p' r_t (store … st) = return mem → code … st' = cd →
    191191   store … st' = mem → execute_l … (ret_act rb) st st'.
    192 
     192   
     193let rec get_labels_of_code (p : instr_params) (i : Instructions p) on i : list CostLabel ≝
     194match 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
     216include "basics/lists/listb.ma".
     217include "../src/utilities/hide.ma".
     218
     219let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝
     220match l with
     221[ nil ⇒ True
     222| cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
     223].
     224
     225lemma no_duplicates_append_r : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) →
     226no_duplicates … l2.
     227#A #l1 elim l1 // #x #xs normalize #IH #l2 * /2/
     228qed.
     229
     230lemma no_duplicates_append_l : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) →
     231no_duplicates … l1.
     232#A #l1 elim l1 // #x #xs normalize #IH #l2 * #H1 #H2 % [2: /2/ ]
     233inversion(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)
     236qed.
     237   
    193238record Program (p : env_params) (p' : instr_params) : Type[0] ≝
    194239{ env : list (env_item p p')
    195240; main : Instructions p'
    196241}.
     242
     243
     244definition 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
     249lemma 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
     255whd 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/
     258qed.
     259
    197260
    198261definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.True.
     
    203266 ].
    204267*)
    205 
    206 include "basics/lists/listb.ma".
    207 include "../src/utilities/hide.ma".
    208268
    209269definition operational_semantics : ∀p : state_params.∀p'.Program p p → abstract_status ≝
     
    648708].
    649709
    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
     711definition same_fresh_map_on : list CostLabel →
     712relation (associative_list DEQCostLabel CostLabel) ≝
     713λdom,m1,m2.∀x.bool_to_Prop (x ∈ dom) → get_element … m1 x = get_element … m2 x.
     714
     715definition same_to_keep_on : list CostLabel → relation (list CostLabel) ≝
     716λdom,keep1,keep2.∀x. bool_to_Prop (x ∈ dom) → (x ∈ keep1) = (x ∈ keep2).
     717
     718lemma memb_not_append : ∀D : DeqSet.∀l1,l2 : list D.∀x : D.
     719x ∈ 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
     724normalize nodelta @IH //
     725qed.
     726
     727lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p.
     728∀x,n,l.
     729x ∈ 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]
     756qed.
     757 
     758lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A .
     759no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False.
     760#A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???);
     761inversion (x == x1) normalize nodelta
     762[ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H %
     763| #_ @IH //
     764]
     765qed.
     766 
     767lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
     768let dom ≝ get_labels_of_code … i1 in
     769no_duplicates … dom →
    655770∀m,keep.
    656771∀info,l.call_post_trans p i1 n l = info →
    657 some_rel (lab_map … info) m →
    658 some_rel1 (lab_to_keep … info) keep →
     772same_fresh_map_on dom (lab_map … info) m →
     773same_to_keep_on dom (lab_to_keep … info) keep →
    659774call_post_clean … (t_code … info) m keep l
    660775 = 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]
     838qed.
     839
    661840
    662841definition trans_prog : ∀p,p'.Program p p' →
     
    669848                   〈(mk_env_item ??
    670849                       (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,
    672851                     fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 ::
    673852                                     ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉)
     
    717896#y #y1 #y2 #z #z1 #z2 #EQ destruct(EQ) #H1 #_ #EQx_xs #EQ destruct(EQ) #_
    718897*)
     898
     899lemma trans_env_ok : ∀p : state_params.∀ prog.
     900no_duplicates_labels … prog →
     901let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
     902∀f,env_it.lookup p p (env … prog) f = return env_it →
     903let dom ≝ get_labels_of_code … (f_body … env_it) in
     904∃env_it',n.lookup p p (env … t_prog) f = return env_it' ∧
     905let info ≝ call_post_trans … (f_body … env_it) n (nil ?) in
     906t_code … info = f_body … env_it' ∧
     907get_element … m (a_call (f_lab … env_it')) = (a_call (f_lab … env_it')) :: gen_labels … info ∧
     908f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it' ∧
     909same_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;
     911normalize 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'
     914normalize in ⊢ (% → ?); normalize nodelta @pair_elim * #env_tail #fresh_tail
     915* #m_tail #keep_tail #EQtail normalize nodelta #EQ1 #EQ2 destruct(EQ1 EQ2)
     916whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H)
     917change 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
     919lapply(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
    719940
    720941
Note: See TracChangeset for help on using the changeset viewer.