Changeset 3399


Ignore:
Timestamp:
Nov 28, 2013, 9:05:46 PM (6 years ago)
Author:
piccolo
Message:

call case not absorbing

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3398 r3399  
    110110
    111111record state_params : Type[1] ≝
    112 { i_pars : instr_params
    113 ; e_pars : env_params
     112{ i_pars :> instr_params
     113; e_pars :> env_params
    114114; store_type : DeqSet
    115115}.
    116 
    117 coercion i_pars.
    118 coercion e_pars.
    119116
    120117record state (p : state_params) : Type[0] ≝
     
    132129; eval_cond_cond : cond_instr p → state p → option (bool × (store_type p))
    133130; eval_loop_cond : loop_instr p → state p → option (bool × (store_type p))
    134 ; eval_call : signature p p → act_params_type p → state p → option (store_type p)
     131; eval_call : signature p p → act_params_type p → store_type p → option (store_type p)
    135132; eval_after_return : return_type p → store_type p → option (store_type p)
    136133; init_store : store_type p
     
    182179| call : ∀st,st',f,act_p,r_lb,cd,mem,env_it.(code ? st) = CALL … f act_p r_lb cd →
    183180    lookup … env f = return env_it →
    184     eval_call ? p' env_it act_p st = return mem →
     181    eval_call ? p' env_it act_p (store … st) = return mem →
    185182    store ? st' = mem → code … st' = f_body … env_it →
    186183     cont … st' =
     
    512509              ].
    513510
     511
     512definition check_continuations : ∀p : instr_params.
     513∀l1,l2 : list (ActionLabel × (Instructions p)).
     514associative_list DEQCostLabel CostLabel →
     515list CostLabel →  option (Prop × (list CostLabel) × (list CostLabel)) ≝
     516λp,cont1,cont2,m,keep.
     517foldr2 ??? 〈True,nil ?,nil ?〉 cont1 cont2
     518 (λx,y,z.
     519   let 〈cond,abs_top',abs_tail'〉 ≝ x in
     520   match call_post_clean p (\snd z) m keep abs_top' with
     521   [ None ⇒ 〈False,nil ?,nil ?〉
     522   | Some w ⇒
     523      match \fst z with
     524       [ ret_act opt_x ⇒
     525           match ret_costed_abs keep opt_x with
     526           [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧
     527                               get_element … m lbl = lbl :: (\fst w),(nil ?),abs_tail'〉
     528           | None ⇒
     529              〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) @ abs_tail'〉
     530           ]
     531       | cost_act opt_x ⇒
     532           match opt_x with
     533           [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉
     534           | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧
     535                               get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉]
     536       | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]).
     537
     538(*
    514539definition check_continuations : ∀p : instr_params.
    515540∀l1,l2 : list (ActionLabel × (Instructions p)).
     
    536561           | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧
    537562                               get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉]
    538        | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]).
     563       | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). *)
    539564(* in input :
    540565     abs_top is the list of labels to be propageted to the deepest level of the call stack
     
    547572
    548573definition state_rel : ∀p.
    549 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → list (list CostLabel) →
     574associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →(list CostLabel) →
    550575relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2.
    551 match check_continuations ? (cont ? st1) (cont … st2) m keep (nil ?) (nil ?) with
     576match check_continuations ? (cont ? st1) (cont … st2) m keep with
    552577[ Some x ⇒ let 〈prf1,abs_top',abs_tail'〉 ≝ x in
    553578           prf1 ∧ call_post_clean … (code … st2) m keep abs_top' = return 〈abs_top,(code … st1)〉
     
    623648].
    624649
    625 
    626 lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
     650axiom some_rel : relation (associative_list DEQCostLabel CostLabel).
     651axiom some_rel1 : relation (list CostLabel).
     652
     653axiom inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
    627654n ≥ compute_max_n … i1 →
     655∀m,keep.
    628656∀info,l.call_post_trans p i1 n l = info →
    629 call_post_clean … (t_code … info) (lab_map … info) (lab_to_keep … info) l
     657some_rel (lab_map … info) m →
     658some_rel1 (lab_to_keep … info) keep →
     659call_post_clean … (t_code … info) m keep l
    630660 = return 〈gen_labels … info,i1〉.
    631 cases daemon (*TODO*)
    632 qed.
    633661
    634662definition trans_prog : ∀p,p'.Program p p' →
     
    659687include "../src/common/Errors.ma".
    660688
     689axiom is_permutation: ∀A.list A → list A → Prop.
     690axiom is_permutation_eq : ∀A.∀l : list A.is_permutation … l l.
     691axiom is_permutation_cons : ∀A.∀l1,l2,x.is_permutation A l1 l2 →
     692                                       is_permutation A (x :: l1) (x :: l2).
     693
     694(*
     695inductive is_permutation (A : Type[0]) : list A → list A → Prop ≝
     696| p_empty : is_permutation A (nil ?) (nil ?)
     697| p_append : ∀x,x1,x2,y,y1,y2.
     698               x = y → is_permutation A (x1 @ x2) (y1 @ y2) →
     699                 is_permutation A (x1 @ [x] @ x2) (y1 @ [y] @ y2).
     700
     701lemma is_permutation_eq : ∀A.∀l : list A.is_permutation … l l.
     702#A #l elim l // #x #xs #IH
     703change with ((nil ?) @ (x :: xs)) in ⊢ (??%%);
     704>append_cons >associative_append
     705@(p_append ? x (nil ?) xs x (nil ?) xs (refl …)) @IH
     706qed.
     707
     708lemma is_permutation_append : ∀A.∀l1,l2,l3,l4 : list A.
     709is_permutation A l1 l3 → is_permutation A l2 l4 →
     710is_permutation A (l1 @ l2) (l3 @ l4).
     711#A #l1 inversion (|l1|)  [2: #n lapply l1 elim n
     712[ #l2 #l3 #l4 #H inversion H // #x #x1 #x2 #y #y1 #y2 #EQ #H1 #_
     713 #ABS cases(nil_to_nil … (sym_eq ??? ABS)) -ABS #_ #ABS
     714 cases(nil_to_nil … ABS) #EQ1 destruct(EQ1) ]
     715#x #xs #IH #l2 #l3 #l4 #H inversion H
     716[#EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ) ]
     717#y #y1 #y2 #z #z1 #z2 #EQ destruct(EQ) #H1 #_ #EQx_xs #EQ destruct(EQ) #_
     718*)
     719
     720
     721
    661722lemma correctness : ∀p,p',prog.
    662723let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
     
    666727∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
    667728state_rel  … m keep abs_top' abs_tail' s2 s2' ∧
    668 (foldr … (append …) (nil ?) (rev … abs_tail')) @ abs_top' @
    669   (map_labels_on_trace m (get_costlabels_of_trace … t)) =
    670   (get_costlabels_of_trace … t') @ abs_top @ (foldr … (append …) (nil ?) abs_tail) ∧
     729is_permutation ? ((abs_top @ (map_labels_on_trace m (get_costlabels_of_trace … t))) @ abs_tail) 
     730                 (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail') ∧
    671731 len … t = len … t'.
    672 xxxxxx
    673 #p #p' #prog @pair_elim * #trans_prog #m #keep #EQtrans
    674 #s1 #s2 #s1' #l #t lapply l -l lapply s1' -s1' elim t
    675 [ #st #s1' #l #H %{l} %{s1'} %{(t_base …)} % [2: %] %{H} normalize // ]
     732#p #p' #prog @pair_elim * #t_prog #m #keep #EQtrans
     733#s1 #s2 #s1' #abs_top #abs_tail #t lapply abs_top -abs_top lapply abs_tail
     734-abs_tail lapply s1' -s1' elim t
     735[ #st #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)}
     736  % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
     737  @is_permutation_eq
     738]
    676739#st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
    677740[ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
    678   #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #_ destruct #tl #IH #s1' #l1
    679   whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11
     741  #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #IH #s1' #abs_tail #abs_top
     742  whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?);
    680743  whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????);
    681744  inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1'
    682   normalize nodelta change with (check_continuations ??????) in match (foldr2 ???????);
    683   inversion(check_continuations ??????) [ #_ *] * #H1 #l2 #EQHl2
    684   >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ **** ]
     745  normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????);
     746  inversion(check_continuations ?????) [ #_ *] ** #H1 #l2 #ll2 #EQHl2
     747  >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ ***** ]
    685748  * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
    686749  cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta
    687   [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) ****
    688   | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] *****[|*] #EQ @⊥ >EQ in Hl1;
     750  [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) *****
     751  | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1;
    689752    normalize * /2/ ] *
    690   [ #EQconts1' normalize nodelta ***** #EQ destruct(EQ)
    691     #HH1 #EQ destruct(EQ) >EQcode11 inversion(code … s1')
     753  [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ)
     754    #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1')
    692755    [
    693756    | #x
     
    701764         cases(call_post_clean ?????) normalize nodelta
    702765         [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ]
    703     #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11
    704     cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 …)
     766    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ)
     767    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …)
    705768    [2: whd whd in match check_continuations; normalize nodelta
    706     change with (check_continuations ??????) in match (foldr2 ???????); >EQHl2
    707         normalize nodelta % // % // % // @EQcode_c_st12 ]
    708     #l3 * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{l3} %{st3'}
    709     %{(t_ind … (cost_act (None ?)) …  t')}
     769       change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2
     770        normalize nodelta % // % // % // % // @EQcode_c_st12 ]
     771    #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen
     772    %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
    710773    [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
    711774      [3: assumption |4: assumption |*:] /3 by nmk/ ]
    712     % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
    713     whd in match (get_costlabels_of_trace ????);
    714     whd in match (get_costlabels_of_trace ????); >EQcosts %
    715   | #lbl #EQconts1' normalize nodelta ****** #EQ destruct(EQ)
    716     #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 inversion(code … s1')
     775    % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts
     776  | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ)
     777    #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?);
     778    inversion(code … s1')
    717779    [
    718780    | #x
     
    724786    ]
    725787    [|*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ]
    726     #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio
    727     cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l3 …)
     788    #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ)
     789    cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …)
    728790    [2: whd whd in match check_continuations; normalize nodelta
    729        change with (check_continuations ??????) in match (foldr2 ???????);  >EQHl2
    730         normalize nodelta % // % // % // @EQcode_c_st12 ]
    731     #l3' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen %{l3'} %{st3'}
     791       change with (check_continuations ?????) in match (foldr2 ???????);
     792       >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]);
     793        normalize nodelta % // % // % // % // @EQcode_c_st12 ]
     794    #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen
     795    %{abs_top'} %{abs_tail'} %{st3'}
    732796    %{(t_ind … (cost_act (Some ? lbl)) … t')}
    733797    [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉)
    734798      [3: assumption |4: assumption |*:] /3 by nmk/ ]
    735     % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
    736     whd in match (get_costlabels_of_trace ????);
    737     whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
    738     whd in match map_labels_on_trace; normalize nodelta
    739     whd in match (foldr ?????);
    740     change with (map_labels_on_trace ??) in match (foldr ?????); >EQget_el
    741     whd in match (append ???); whd in match (append ???) in ⊢ (???%); @eq_f
    742     whd in match (append ???) in ⊢ (??(???%)(??%?)); @EQcost
    743   ]   
     799    % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append
     800    whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
     801    @is_permutation_cons assumption
     802  ]
     803(*     
    744804| #seq #i #store * [| #lbl] #EQcode11 #EQstore #EQ destruct(EQ) #EQcont
    745805  #EQ destruct(EQ) #Hio_st11 #Hio_st12 #EQ destruct(EQ) #EQ1 #EQ2 destruct(EQ1 EQ2)
     
    751811  [1,2,4,5,6,7,8,9,11,12,13,14: (*assurdi da fare *) cases daemon ]
    752812  #seq1 #opt_l #i1 #_ #EQcode_st3 change with (m_bind ?????) in ⊢ (??%? → ?);
    753   cases daemon
     813  cases daemon *)
    754814|8: #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
    755815    #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
    756     destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #l1 whd in ⊢ (% → ?);
    757     inversion(check_continuations ??????) [1,3: #_ *] * #H1 #l2 #EQcheck
    758     normalize nodelta *** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
     816    destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #abs_top #abs_tail
     817    whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1
     818    #abs_top_cont #abs_tail_cont #EQcheck
     819    normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
    759820    [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_
    760     #EQcode_st1' #EQclean #EQstore #EQio
    761     cut(∃env_it',n.lookup p p (env … trans_prog) f = return env_it' ∧
    762           t_code … (call_post_trans … (f_body … env_it) n (nil ?)) = f_body … env_it')
    763     [1,3: cases daemon (*TODO*) ] * #env_it' * #fresh' * #EQenv_it' #EQtrans
    764     cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) l2 …)
    765     [2: whd >EQcont12 change with (m_bind ??? (check_continuations ??????) ?) in match (check_continuations ??????);
    766         >EQcheck >m_return_bind change with (m_bind ?????) in EQclean : (??%?);
    767     inversion(call_post_clean ?????) in EQclean; [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
    768     * #l3 #i'' #EQi'' >m_return_bind cases opt_l' in EQcode_st1'; [| #lbl'] #EQcode_st1'
    769     normalize nodelta
     821    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
     822    cut(∃env_it',n.lookup p p (env … t_prog) f = return env_it' ∧
     823          t_code … (call_post_trans … (f_body … env_it) n (nil ?)) = f_body … env_it' ∧
     824          get_element … m (a_call (f_lab … env_it')) = (a_call (f_lab … env_it')) :: gen_labels … (call_post_trans … (f_body … env_it) n (nil ?)) ∧
     825          f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it')
     826    [ cases daemon (*TODO*) ] * #env_it' * #fresh' **** #EQenv_it' #EQtrans #EQgen_labels #EQsignature #EQlab_env_it
     827    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
     828    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
     829    inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta
     830    [2: inversion(memb ???) normalize nodelta #Hlbl_keep
     831        [  inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
     832           #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
     833          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
     834          lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
     835          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
     836          #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
     837          #EQ destruct(EQ)
     838          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 ?))))
     839          [2: whd >EQcont12
     840            change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
     841            >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l'
     842            whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
     843            % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans
     844            @(inverse_call_post_trans … fresh') [2: % |*: cases daemon (*TODO*) ]
     845          ]
     846          #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{abs_top'''}
     847          %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
     848          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %]
     849          %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
     850          >EQlab_env_it >associative_append whd in match (append ???); >associative_append
     851          >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
     852          whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons
     853          >append_nil whd in match (append ???) in ⊢ (???%); //
     854        | 
     855          xxxxxxxxxx
     856           
     857           
     858           
     859                   
     860            inversion(memb ???) normalize nodelta #Hlbl_keep
     861            [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
     862          #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
     863          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
     864          lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
     865          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
     866          #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
     867          #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta >Hlbl_keep
     868          normalize nodelta >EQi' normalize nodelta % // % // % [ % // % // % //]
     869   
     870   
     871   
     872   
     873    cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_top'' @ abs_tail_cont) (get_element … m (a_call (f_lab … env_it'))))
     874    [2: whd >EQcont12
     875     change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
     876     >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta
     877     cases opt_l' in EQcode_st1' EQclean; [| #lbl'] #EQcode_st1' normalize nodelta
    770878    [2: inversion(memb ???) normalize nodelta #Hlbl_keep
    771879        [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
     
    773881          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
    774882          lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
    775           [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' l3)
     883          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
    776884          #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
    777885          #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta >Hlbl_keep
    778           normalize nodelta % // % // % [ % // % // % //] >EQcode12 <EQtrans
     886          normalize nodelta >EQi' normalize nodelta % // % // % [ % // % // % //] >EQcode12 <EQtrans
    779887          cases daemon (*TODO*)
    780888        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
Note: See TracChangeset for help on using the changeset viewer.