Changeset 3414 for LTS/Language.ma


Ignore:
Timestamp:
Dec 27, 2013, 9:09:10 PM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3411 r3414  
    469469; fresh : ℕ
    470470; lab_map : associative_list DEQCostLabel CostLabel
    471 ; lab_to_keep : list CostLabel
     471; lab_to_keep : list ReturnPostCostLabel
    472472}.
    473473
     
    515515      mk_call_post_info ? (nil ?) (CALL ? f act_p (Some ? lbl) (t_code … ih)) (fresh … ih)
    516516       (〈a_return_post lbl,(a_return_post lbl :: (gen_labels … ih))〉 :: (lab_map … ih))
    517        (a_return_post lbl :: lab_to_keep … ih)
     517       (lbl :: lab_to_keep … ih)
    518518   ]
    519519| IO lin io lout i1 ⇒
     
    526526
    527527let rec call_post_clean (p : instr_params) (i : Instructions p) on i :
    528 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →
     528associative_list DEQCostLabel CostLabel → list ReturnPostCostLabel → list CostLabel →
    529529option ((list CostLabel) × (Instructions p)) ≝
    530530λm,keep,abs.
     
    559559  match r_lb with
    560560  [ None ⇒ None ?
    561   | Some lbl ⇒ if ((a_return_post lbl ∈ keep))
     561  | Some lbl ⇒ if (lbl ∈ keep)
    562562               then if ((get_element … m lbl) == lbl :: l1)
    563563                    then return 〈nil ?,CALL … f act_p (Some ? lbl) instr1〉
     
    605605].
    606606
    607 definition ret_costed_abs : list CostLabel → option ReturnPostCostLabel → option CostLabel ≝
     607definition ret_costed_abs : list ReturnPostCostLabel → option ReturnPostCostLabel → option CostLabel ≝
    608608λkeep,x.
    609609 match x with
    610               [ Some lbl ⇒ if (a_return_post lbl) ∈ keep then return (a_return_post lbl)
     610              [ Some lbl ⇒ if lbl ∈ keep then return (a_return_post lbl)
    611611                           else None ?
    612612              | None ⇒ None ?
     
    617617∀l1,l2 : list (ActionLabel × (Instructions p)).
    618618associative_list DEQCostLabel CostLabel →
    619 list CostLabel →  option (Prop × (list CostLabel) × (list CostLabel)) ≝
     619list ReturnPostCostLabel →  option (Prop × (list CostLabel) × (list CostLabel)) ≝
    620620λp,cont1,cont2,m,keep.
    621621foldr2 ??? 〈True,nil ?,nil ?〉 cont1 cont2
     
    676676
    677677definition state_rel : ∀p.
    678 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →(list CostLabel) →
     678associative_list DEQCostLabel CostLabel → list ReturnPostCostLabel → list CostLabel →(list CostLabel) →
    679679relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2.
    680680match check_continuations ? (cont ? st1) (cont … st2) m keep with
     
    757757λdom,m1,m2.∀x.bool_to_Prop (x ∈ dom) → get_element … m1 x = get_element … m2 x.
    758758
    759 definition same_to_keep_on : list CostLabel → relation (list CostLabel) ≝
    760 λdom,keep1,keep2.∀x. bool_to_Prop (x ∈ dom) → (x ∈ keep1) = (x ∈ keep2).
     759definition same_to_keep_on : list CostLabel → relation (list ReturnPostCostLabel) ≝
     760λdom,keep1,keep2.∀x. bool_to_Prop (a_return_post x ∈ dom) → (x ∈ keep1) = (x ∈ keep2).
    761761
    762762lemma memb_not_append : ∀D : DeqSet.∀l1,l2 : list D.∀x : D.
     
    779779
    780780
    781 lemma same_to_keep_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l.
    782 no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → x ∈ dom1) →
    783 (∀x.x ∈ l3 → x ∈ dom3) →
     781lemma same_to_keep_on_append : ∀dom1,dom2,dom3 : list CostLabel.
     782∀l1,l2,l3,l : list ReturnPostCostLabel.
     783no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → a_return_post x ∈ dom1) →
     784(∀x.x ∈ l3 → a_return_post x ∈ dom3) →
    784785same_to_keep_on (dom1@dom2@dom3) (l1@l2@l3) l →
    785786same_to_keep_on dom2 l2 l.
     
    792793   | @sym_eq @memb_not_append [2: @memb_not_append //]
    793794   [ <associative_append in no_dup; #no_dup ]
    794    lapply(memb_no_duplicates_append … x … no_dup) #H
     795   lapply(memb_no_duplicates_append … (a_return_post x) … no_dup) #H
    795796   inversion(memb ???) // #H1 cases H
    796797   [1,4: [>memb_append_l2 | >memb_append_l1] // >Hx //
     
    819820lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p.
    820821∀x,n,l.
    821 x ∈ lab_to_keep … (call_post_trans … i n l) → x ∈ get_labels_of_code …  i.
     822x ∈ lab_to_keep … (call_post_trans … i n l) → a_return_post x ∈ get_labels_of_code …  i.
    822823#p #i elim i //
    823824[ #seq #opt_l #instr #IH #x #n #l whd in match (call_post_trans ????);
     
    896897#EQ destruct >(\b (refl …)) @I
    897898qed.
    898  
     899
     900let rec is_fresh_keep (keep : list ReturnPostCostLabel) (n : ℕ) on keep : Prop ≝
     901match keep with
     902[ nil ⇒ True
     903| cons x xs ⇒ let ih ≝ is_fresh_keep xs n in
     904              match x with
     905              [ a_return_cost_label m ⇒ m < n ∧ ih ]
     906].
     907
     908lemma fresh_ok_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.∀l.
     909n ≤ fresh … (call_post_trans p i1 n l).
     910#p #i1 elim i1 normalize /2 by transitive_le, le_n/
     911[ #seq * [|#lbl] #i2 #IH #n #l normalize /2 by /
     912| #cond #ltrue #i_true #lfalse #i_false #i2 #IH1 #IH2 #IH3 #n #l
     913  @(transitive_le … (IH3 …)) [2: @(transitive_le … (IH2 …)) [2: @(transitive_le … (IH1 …)) ]] //
     914| #f #act_p * [|#lbl] normalize #i2 #IH /2 by le_S/
     915]
     916qed.
     917
     918lemma fresh_keep_n_ok : ∀n,m,l.
     919is_fresh_keep l n → n ≤ m → is_fresh_keep l m.
     920#n #m #l lapply n -n lapply m -m elim l // * #x #xs #IH #n #m
     921normalize * #H1 #H2 #H3 % /2 by transitive_le/
     922qed.
     923
     924lemma fresh_false : ∀n,l.is_fresh_keep l n → a_return_cost_label n ∈ l = false.
     925#n #l lapply n -n elim l // * #x #xs #IH #n whd in ⊢ (% → ??%?); * #H1 #H2
     926whd in match (eqb ???); @eqb_elim
     927[ #EQ destruct @⊥ /2 by absurd/
     928| #_ >IH //
     929]
     930qed.
     931
     932
    899933lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
    900934let dom ≝ get_labels_of_code … i1 in
     
    904938same_fresh_map_on dom (lab_map … info) m →
    905939same_to_keep_on dom (lab_to_keep … info) keep →
    906 call_post_clean … (t_code … info) m keep l
     940is_fresh_keep keep n →
     941call_post_clean ? (t_code ? info) m keep l
    907942 = return 〈gen_labels … info,i1〉.
    908943#p #i1 elim i1
     
    912947  #EQ destruct(EQ) //
    913948| #seq * [|#lbl] #instr #IH #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep
    914   #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%%); normalize nodelta
     949  #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%%); normalize nodelta
    915950  >IH //
    916951  [1,4: whd whd in H2; #x #Hx @H2 whd in match (get_labels_of_code ??); //
    917         @orb_Prop_r //
    918952  |2,5: whd whd in H1; #x #Hx [ @H1 // ] cases no_dup #H3 #_ <H1
    919953       [2: whd in match (get_labels_of_code ??); @orb_Prop_r // ]
     
    929963| #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #n normalize nodelta
    930964  #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?);
    931   #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%?); >IH3 //
     965  #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%?); >IH3 //
    932966  [2: whd  in match (get_labels_of_code ??) in H2;
    933967      change with ([?;?]@?) in match (?::?) in H2;
     
    964998  |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |]
    965999  ]
    966   normalize nodelta >IH2 //
    967   [2: whd  in match (get_labels_of_code ??) in H2;
     1000  normalize nodelta >IH2
     1001  [5: %
     1002  |2: /2 by fresh_keep_n_ok/
     1003  |3: whd  in match (get_labels_of_code ??) in H2;
    9681004   change with ([?;?]@?) in match (?::?) in H2;
    9691005   <associative_append in H2; #H2
    9701006   @(same_to_keep_on_append … H2) // #x #Hx [ @orb_Prop_r @orb_Prop_r ]
    9711007   @(lab_to_keep_in_domain … (eq_true_to_b … Hx))
    972   |3: whd  in match (get_labels_of_code ??) in H1;
     1008  |4: whd  in match (get_labels_of_code ??) in H1;
    9731009   change with ([?;?]@?) in match (?::?) in H1;
    9741010   change with ([?;?]@?) in match (?::?::?) in H1 : (??%?);
     
    9821018     @(lab_map_in_domain … (eq_true_to_b … H1))
    9831019   ]
    984   |4: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l
     1020  |6: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l
     1021  |*:
    9851022  ]
    986   >m_return_bind >IH1 //
    987   [2:  whd  in match (get_labels_of_code ??) in H2;
     1023  >m_return_bind >IH1
     1024  [5: %
     1025  |2: /3 by fresh_keep_n_ok/
     1026  |3:  whd  in match (get_labels_of_code ??) in H2;
    9881027   change with ([?;?]@?) in match (?::?) in H2;
    9891028   change with ([ ] @ ?) in match (lab_to_keep ??) in H2;
    9901029   >associative_append in H2 : (??%?); #H2
    991    @(same_to_keep_on_append … H2) // [ #x *] #x #Hx cases(memb_append … Hx)
     1030   @(same_to_keep_on_append … H2) // #x #Hx cases(memb_append … Hx)
    9921031   -Hx #Hx [ >memb_append_l1 | >memb_append_l2] //
    9931032   @(lab_to_keep_in_domain … (eq_true_to_b … Hx))
    994   |3:  whd  in match (get_labels_of_code ??) in H1;
     1033  |4:  whd  in match (get_labels_of_code ??) in H1;
    9951034   change with ([?;?]@?) in match (?::?) in H1;
    9961035   change with ([?;?]@?) in match (?::?::?) in H1 : (??%?);
     
    9981037    #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2 ]
    9991038    // @(lab_map_in_domain … (eq_true_to_b … Hx))
    1000   |4: cases no_dup #_ * #_ @no_duplicates_append_l
     1039  |6: cases no_dup #_ * #_ @no_duplicates_append_l
     1040  |*:
    10011041  ]
    10021042  >m_return_bind normalize nodelta whd in H1; <H1
     
    10101050      >(\b (refl ? (a_non_functional_label ltrue))) % ] #_
    10111051      whd in match (get_element ????); >(\b (refl …)) normalize nodelta
    1012       >(\b (refl …)) % 
     1052      >(\b (refl …)) %
    10131053| #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?);
    1014   #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on
    1015   whd in ⊢ (??%?); >IH2
    1016   [ normalize nodelta >IH1
     1054  #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on #f_k
     1055  whd in ⊢ (??%?); >(IH2 … (refl …))
     1056  [ normalize nodelta >(IH1 … (refl …))
    10171057    [ >m_return_bind <fresh_map [2: @orb_Prop_l >(\b (refl …)) % ]
    10181058      whd in match (get_element ????);
     
    10261066      whd in match (get_element ????); >(\b (refl …)) normalize nodelta
    10271067      >(\b (refl …)) %
     1068    | /2 by fresh_keep_n_ok/
    10281069    | change with ([?;?]@?@?) in keep_on : (?%??); change with ((nil ?) @ ? @ ?) in keep_on : (??%?);
    1029       @(same_to_keep_on_append … keep_on) // [ #x * | #x /2 by lab_to_keep_in_domain/ ]
     1070      @(same_to_keep_on_append … keep_on) // #x /2 by lab_to_keep_in_domain/
    10301071    | change with ([?;?]@?@?) in fresh_map : (?%%?); @(same_fresh_map_on_append … fresh_map)
    10311072      /2 by lab_map_in_domain/ #x whd in match (memb ???); inversion(x==lfalse) #Hlfalse
     
    10351076        @orb_Prop_l >Hltrue %
    10361077      ]
    1037     | %
    10381078    | cases no_dup #_ * #_ /2/
    1039     |
    10401079    ]
     1080  | //
    10411081  | change with ([?;?]@?@?) in keep_on : (?%??); <associative_append in keep_on;
    10421082    <(append_nil … (?@?)) <(append_nil … (?@?)) in ⊢ (??%? → ?);
     
    10621102      ]
    10631103    ]
    1064   | %
    10651104  | cases no_dup #_ * #_ /2 by no_duplicates_append_r/
    1066   |
    10671105  ]
    10681106| #f #act_p * [|#r_lb] #i #IH #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?);
    1069   #EQ destruct(EQ) cases daemon
    1070 |*: cases daemon (*TODO*)
     1107  #EQ destruct(EQ) #fresh_map #same_keep #f_k whd in ⊢ (??%?);
     1108  >(IH … (refl …))
     1109  [1,6: normalize nodelta
     1110     [ >fresh_false [2: /2 by fresh_keep_n_ok/ ] %
     1111     | <same_keep
     1112       [ whd in match (memb ???); >(\b (refl …)) normalize nodelta
     1113         <fresh_map
     1114         [ whd in match (get_element ????); >(\b (refl …)) normalize nodelta
     1115           >(\b (refl …)) %
     1116         | whd in match (memb ???); >(\b (refl …)) %
     1117         ]
     1118       | whd in match (memb ???); >(\b (refl …)) %
     1119       ]
     1120    ]
     1121  |2,7: //
     1122  |3,8: whd in match (get_labels_of_code ??) in same_keep; // #x #Hx <same_keep
     1123        [2: >memb_cons // >Hx // ] cases no_dup * #ABS #_ whd in ⊢ (???%);
     1124        inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) >Hx //
     1125  |4,9: whd in match (get_labels_of_code ??) in fresh_map; // #x #Hx <fresh_map
     1126        [2: >memb_cons // >Hx //] cases no_dup * #ABS #_ whd in ⊢ (???%);
     1127        inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) //
     1128  |5,10: [ @no_dup | cases no_dup // ]
     1129  ]
     1130| #lin #io #lout #i #IH #n whd in match (get_labels_of_code ??); #no_dup
     1131  #m #keep #info #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #fresh_map #same_keep
     1132  #f_k whd in ⊢ (??%?); >(IH … (refl …))
     1133  [ normalize nodelta <fresh_map [2: >memb_cons // >memb_hd // ]
     1134    whd in match (get_element ????); >(\b (refl …)) normalize nodelta
     1135    >(\b (refl …)) <fresh_map [2: >memb_hd //] whd in match (get_element ????);
     1136    inversion(lin==lout)
     1137    [ #ABS @⊥ cases no_dup * #ABS1 #_ @ABS1 whd in match (memb ???); >(\P ABS)
     1138      >(\b (refl …)) //
     1139    | #H inversion (a_non_functional_label lin== ? lout)
     1140      [ #ABS lapply(\P ABS) #EQ destruct >(\b (refl …)) in H; #EQ destruct
     1141      | #_ normalize nodelta whd in match (get_element ????); >(\b (refl …))
     1142        normalize nodelta >(\b (refl …)) %
     1143      ]
     1144    ]
     1145  | //
     1146  | #x #Hx >same_keep [2: >memb_cons // >memb_cons // >Hx % ] %
     1147  | #x #Hx <fresh_map [2: >memb_cons // >memb_cons // >Hx %]
     1148    cases no_dup * #ABS1 ** #ABS2 #_ whd in ⊢ (???%); inversion(x == lout)
     1149    normalize nodelta
     1150    [2: #_ whd in ⊢ (???%); inversion(x==lin) normalize nodelta //
     1151        #H @⊥ @ABS1 >memb_cons // <(\P H) >Hx //
     1152    | #H @⊥ @ABS2 <(\P H) >Hx //
     1153    ]
     1154  | cases no_dup #_ * #_ //
     1155  ]
    10711156]
    1072 qed.
     1157qed.
     1158
    10731159
    10741160
    10751161definition trans_prog : ∀p,p'.Program p p' →
    1076 (Program p p') × (associative_list DEQCostLabel CostLabel) × (list CostLabel)≝
     1162(Program p p') × (associative_list DEQCostLabel CostLabel) × (list ReturnPostCostLabel)≝
    10771163λp,p',prog.
    10781164let max_all ≝ foldl … (λn,i.max n (compute_max_n … (f_body … i))) O (env … prog) in
     
    12091295]
    12101296qed.
     1297
     1298(* aggiungere fresh_to_keep al lemma seguente??*)
     1299
     1300xxxxxxx
    12111301
    12121302
     
    12731363    ]
    12741364    ]
    1275   | whd #x #Hx >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … x … H)
     1365  | whd #x #Hx >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … (a_return_post x) … H)
    12761366    // @⊥
    12771367    (* subproof with no nice statement *)
     
    12891379    #H1 #H2 #H3 cases(memb_append … H3) -H3
    12901380    [ #H3 change with ([?]@?) in match (?::?) in H2;
    1291       lapply(no_duplicates_append_commute … H2) -H2 * #_ #H4 @(memb_no_duplicates_append … x … H4)
     1381      lapply(no_duplicates_append_commute … H2) -H2 * #_ #H4 @(memb_no_duplicates_append … (a_return_post x) … H4)
    12921382      [ whd in match (append ???); >memb_append_l1 // >(lab_to_keep_in_domain … (eq_true_to_b … H3)) %
    12931383      | //
     
    13161406   % [2: #x #Hx <same_to_keep // @memb_append_l22
    13171407        inversion(memb ???) // #ABS lapply(lab_to_keep_in_domain … (eq_true_to_b … ABS))
    1318         #ABS1 @(memb_no_duplicates_append … x … H) //
     1408        #ABS1 @(memb_no_duplicates_append … (a_return_post x) … H) //
    13191409        cases(lookup_ok_append … Henv_it) #l1 * #l2 * #EQ1 #EQ2 destruct(EQ1 EQ2)
    13201410        >foldr_map_append >memb_append_l2 // >foldr_map_append >memb_append_l1 //
     
    15221612    ]
    15231613  ]
    1524 |       
    1525 
    1526 8:
    1527     #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
    1528     #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
    1529     #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
    1530     destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #abs_top #abs_tail
     1614| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?;
     1615  [1,2,3,4,5,6,7,9: cases daemon (*assurdi*) ]
     1616  #st11 #st12 #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
     1617  #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
     1618  destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #t1 #t2 #H inversion H in ⊢ ?;
     1619  [1,2,3,4,5,6,7,8: cases daemon (*assurdi*) ]
     1620   #st41 #st42 #r_t #mem1 #new_cont #opt_l1 #cd #EQcode41 #EQcont41 #EQ destruct(EQ)
     1621   #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #_ #_
     1622   #_ whd in ⊢ (?(?%) → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta
     1623   inversion(opt_l) in ⊢(% → ?); normalize nodelta [2: #lbl #_ * ] #EQopt_l *
     1624   #Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); #EQcont11_42 whd in ⊢ (% → ?); #EQ destruct
     1625   #IH1 #IH2 #st1' #abs_top #abs_tail
    15311626    whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1
    15321627    #abs_top_cont #abs_tail_cont #EQcheck
     
    15401635    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
    15411636    inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta
    1542     [2: inversion(memb ???) normalize nodelta #Hlbl_keep
    1543         [  inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
    1544            #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
    1545           [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
    1546           lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
    1547           [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
    1548           #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
    1549           #EQ destruct(EQ)
    1550           cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_tail_cont) (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?))))
    1551           [2: whd >EQcont12
    1552             change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
    1553             >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l'
    1554             whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
    1555             % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans
    1556             @(inverse_call_post_trans … fresh')
    1557             [2: % |*: [2,3: /2 by / ]
    1558                 cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
    1559                 whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append
    1560                 #no_dup lapply(no_duplicates_append_r … no_dup) #H1
    1561                 lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1
    1562                 change with ([?]@?) in match (?::?); #H1
    1563                 lapply(no_duplicates_append_r … H1) >append_nil //
    1564             ]
    1565           ]
    1566           #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{abs_top'''}
    1567           %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
    1568           [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %]
    1569           %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    1570           >EQlab_env_it >associative_append whd in match (append ???); >associative_append
    1571           >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
    1572           whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons
    1573           >append_nil whd in match (append ???) in ⊢ (???%); //
    1574         | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
     1637    [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] cases(memb ???) normalize nodelta
     1638    [ cases(?==?) normalize nodelta ]
     1639     whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     1640     xxxxxxx
     1641     
     1642     
     1643     
    15751644          cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_top''@abs_tail_cont) (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?))))
    15761645          [2: whd >EQcont12
Note: See TracChangeset for help on using the changeset viewer.