(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) include "basics/types.ma". include "Traces.ma". include "basics/lists/list.ma". include "../src/utilities/option.ma". include "basics/jmeq.ma". discriminator option. record instr_params : Type[1] ≝ { seq_instr : DeqSet ; io_instr : DeqSet ; cond_instr : DeqSet ; loop_instr : DeqSet ; act_params_type : DeqSet ; return_type : DeqSet }. inductive Instructions (p : instr_params) : Type[0] ≝ | EMPTY : Instructions p | RETURN : return_type p → Instructions p | SEQ : (seq_instr p) → option NonFunctionalLabel → Instructions p → Instructions p | COND : (cond_instr p) → NonFunctionalLabel → Instructions p → NonFunctionalLabel → Instructions p → Instructions p → Instructions p | LOOP : (loop_instr p) → NonFunctionalLabel → Instructions p → NonFunctionalLabel → Instructions p → Instructions p | CALL : FunctionName → (act_params_type p) → option ReturnPostCostLabel → Instructions p → Instructions p | IO : NonFunctionalLabel → (io_instr p) → NonFunctionalLabel → Instructions p → Instructions p. let rec eq_instructions (p : instr_params) (i : Instructions p) on i : (Instructions p) → bool ≝ match i with [ EMPTY ⇒ λi'.match i' with [ EMPTY ⇒ true | _ ⇒ false ] | RETURN x ⇒ λi'.match i' with [ RETURN y ⇒ x == y | _ ⇒ false ] | SEQ x lab instr ⇒ λi'.match i' with [ SEQ y lab' instr' ⇒ x == y ∧ eq_instructions … instr instr' ∧ match lab with [ None ⇒ match lab' with [ None ⇒ true | _ ⇒ false ] | Some l1 ⇒ match lab' with [Some l2 ⇒ eq_nf_label l1 l2 | _ ⇒ false] ] | _ ⇒ false ] | COND x ltrue i1 lfalse i2 i3 ⇒ λi'.match i' with [ COND y ltrue' i1' lfalse' i2' i3' ⇒ x == y ∧ eq_nf_label ltrue ltrue' ∧ eq_instructions … i1 i1' ∧ eq_nf_label lfalse lfalse' ∧ eq_instructions … i2 i2' ∧ eq_instructions … i3 i3' | _ ⇒ false ] | LOOP x ltrue i1 lfalse i2 ⇒ λi'.match i' with [ LOOP y ltrue' i1' lfalse' i2' ⇒ x == y ∧ eq_instructions … i1 i1' ∧ eq_nf_label ltrue ltrue' ∧ eq_instructions … i2 i2' | _ ⇒ false ] | CALL f act_p r_lb i1 ⇒ λi'.match i' with [ CALL f' act_p' r_lb' i1' ⇒ eq_function_name f f' ∧ act_p == act_p' ∧ eq_instructions … i1 i1' ∧ match r_lb with [ None ⇒ match r_lb' with [None ⇒ true | _ ⇒ false] | Some z ⇒ match r_lb' with [Some w ⇒ eq_return_cost_lab z w | _ ⇒ false ] ] | _ ⇒ false ] | IO lin io lout i1 ⇒ λi'.match i' with [ IO lin' io' lout' i1' ⇒ eq_nf_label lin lin' ∧ io == io' ∧ eq_nf_label lout lout' ∧ eq_instructions … i1 i1' | _ ⇒ false ] ]. (* lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → (i1 ≠ i2 → P false) → P (eq_instructions p i1 i2). #P #p #i1 elim i1 [* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') | #rt * normalize [2: #rt' cases (dec_eq … rt rt') #H [>(\b H) | >(\bf H) ] /2/ #_ #K @K % #abs lapply (eq_to_jmeq ??? abs) #abs' destruct(abs') @(absurd ?? H) //] [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') | #seq * [| #lbl] #i #IH * normalize [1,8: |2,9: #t_t |3,10: #seq1 #opt_l #i2 |4,11: #cond #ltrue #i_t #lfalse #i_f #i_c |5,12: #cond #ltrue #i_t #lfalse #i_f |6,13: #f #act_p #ret #i3 |*: #lin #io #lout #i3] #H1 #H2 try(@H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct) inversion(?==?) normalize nodelta [2,4: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >(\b (refl …)) in ABS; #EQ destruct] #EQseq inversion(eq_instructions ???) normalize nodelta #Heq_i2 [2,4: @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct *) record env_params : Type[1] ≝ { form_params_type : Type[0] }. record signature (p : env_params) (p' : instr_params) : Type[0] ≝ { f_name : FunctionName ; f_pars : form_params_type p ; f_ret : return_type p' }. record env_item (p : env_params) (p' : instr_params) : Type[0] ≝ { f_sig :> signature p p' ; f_lab : CallCostLabel ; f_body : Instructions p' }. record state_params : Type[1] ≝ { i_pars :> instr_params ; e_pars :> env_params ; store_type : DeqSet }. record state (p : state_params) : Type[0] ≝ { code : Instructions p ; cont : list (ActionLabel × (Instructions p)) ; store : store_type p ; io_info : bool }. definition is_io : ∀p.state p → Prop ≝ λp,st.io_info … st = true. record sem_state_params (p : state_params) : Type[0] ≝ { eval_seq : seq_instr p → (store_type p) → option (store_type p) ; eval_io : io_instr p → store_type p → option (store_type p) ; eval_cond_cond : cond_instr p → store_type p → option (bool × (store_type p)) ; eval_loop_cond : loop_instr p → store_type p → option (bool × (store_type p)) ; eval_call : signature p p → act_params_type p → store_type p → option (store_type p) ; eval_after_return : return_type p → store_type p → option (store_type p) ; init_store : store_type p }. let rec lookup (p : env_params) (p' : instr_params) (l : list (env_item p p')) on l : FunctionName → option (env_item p p') ≝ match l with [ nil ⇒ λ_.None ? | cons x xs ⇒ λf.if (eq_function_name f (f_name … x)) then Some ? x else lookup … xs f ]. definition is_ret_call_act : ActionLabel → Prop ≝ λa.match a with [ret_act _ ⇒ True | call_act _ _ ⇒ True | _ ⇒ False ]. inductive execute_l (p : state_params) (p' : sem_state_params p) (env : list (env_item p p)) : ActionLabel → relation (state p) ≝ | empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p)→ (cont ? st) = hd :: tl → (code ? st') = \snd hd → (cont … st') = tl → (store … st) = (store … st') → (io_info … st = true → is_non_silent_cost_act (\fst hd)) → (io_info … st') = false → ¬ is_ret_call_act (\fst hd) → execute_l … (\fst hd) st st' | seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd → eval_seq … p' i (store … st) = return s → (code ? st') = cd → (cont … st) = (cont … st') → (store … st') = s → io_info … st = false → io_info ? st' = false → execute_l … (cost_act opt_l) st st' | cond_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m. (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp (store … st) = return 〈true,new_m〉 → cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_true → store … st' = new_m → io_info … st = false → io_info … st' = false → execute_l … (cost_act (Some ? ltrue)) st st' | cond_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m. (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp (store … st) = return 〈false,new_m〉 → cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_false → store … st' = new_m → io_info … st = false → io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st' | loop_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m. code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp (store … st) = return 〈true,new_m〉 → cont ? st' = 〈cost_act (None ?),LOOP … exp ltrue i_true lfalse i_false〉 :: (cont … st) → code … st' = i_true → store … st' = new_m → io_info … st = false → io_info … st' = false → execute_l … (cost_act (Some ? ltrue)) st st' | loop_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m. code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp (store … st) = return 〈false,new_m〉 → cont ? st' = cont … st → code … st' = i_false → store … st' = new_m → io_info … st = false → io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st' | io_in : ∀st,st',lin,io,lout,cd,mem.(code ? st) = IO … lin io lout cd → eval_io … p' io (store … st) = return mem → code ? st' = EMPTY p → cont … st' = 〈cost_act (Some ? lout),cd〉 :: (cont … st) → store … st' = mem → io_info … st' = true → execute_l … (cost_act (Some ? lin)) st st' | call : ∀st,st',f,act_p,r_lb,cd,mem,env_it.(code ? st) = CALL … f act_p r_lb cd → lookup … env f = return env_it → eval_call ? p' env_it act_p (store … st) = return mem → store ? st' = mem → code … st' = f_body … env_it → cont … st' = 〈(ret_act r_lb),cd〉 :: (cont … st) → io_info … st = false → (io_info … st') = false → execute_l … (call_act f (f_lab ?? env_it)) st st' | ret_instr : ∀st,st',r_t,mem,tl',rb,cd.code ? st = RETURN … r_t → cont … st = 〈ret_act rb,cd〉 :: tl' → cont ? st' = tl' → io_info … st = false → io_info ? st' = false → eval_after_return … p' r_t (store … st) = return mem → code … st' = cd → store … st' = mem → execute_l … (ret_act rb) st st'. let rec get_labels_of_code (p : instr_params) (i : Instructions p) on i : list CostLabel ≝ match i with [ EMPTY ⇒ [ ] | RETURN x ⇒ [ ] | SEQ x lab instr ⇒ let ih ≝ get_labels_of_code … instr in match lab with [ None ⇒ ih | Some lbl ⇒ a_non_functional_label lbl :: ih ] | COND x ltrue i1 lfalse i2 i3 ⇒ let ih3 ≝ get_labels_of_code … i3 in let ih2 ≝ get_labels_of_code … i2 in let ih1 ≝ get_labels_of_code … i1 in ltrue :: lfalse :: (ih1 @ ih2 @ih3) | LOOP x ltrue i1 lfalse i2 ⇒ let ih2 ≝ get_labels_of_code … i2 in let ih1 ≝ get_labels_of_code … i1 in a_non_functional_label ltrue :: a_non_functional_label lfalse :: (ih1 @ ih2) | CALL f act_p r_lb i1 ⇒ let ih1 ≝ get_labels_of_code … i1 in match r_lb with [ None ⇒ ih1 | Some lbl ⇒ a_return_post lbl :: ih1] | IO lin io lout i1 ⇒ let ih1 ≝ get_labels_of_code … i1 in a_non_functional_label lin :: a_non_functional_label lout :: ih1 ]. include "basics/lists/listb.ma". include "../src/utilities/hide.ma". let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ match l with [ nil ⇒ True | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs ]. lemma no_duplicates_append_r : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) → no_duplicates … l2. #A #l1 elim l1 // #x #xs normalize #IH #l2 * /2/ qed. lemma no_duplicates_append_l : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) → no_duplicates … l1. #A #l1 elim l1 // #x #xs normalize #IH #l2 * #H1 #H2 % [2: /2/ ] inversion(x ∈ xs @l2) in H1; normalize [ #_ * #H @⊥ @H %] #H1 #_ % inversion(x ∈ xs) normalize [2: //] #H3 #_ >(memb_append_l1 … H3) in H1; #EQ destruct(EQ) qed. record Program (p : env_params) (p' : instr_params) : Type[0] ≝ { env : list (env_item p p') ; main : Instructions p' }. definition no_duplicates_labels : ∀p,p'.Program p p' → Prop ≝ λp,p',prog. no_duplicates … (foldr … (λitem,acc.((a_call (f_lab … item)) :: get_labels_of_code … (f_body … item)) @ acc) (get_labels_of_code … (main … prog)) (env … prog)). lemma no_duplicates_domain_of_fun: ∀p,p',prog.no_duplicates_labels … prog → ∀f,env_it.lookup p p' (env … prog) f = return env_it → no_duplicates … (get_labels_of_code … (f_body … env_it)). #p #p' * #env elim env [ #main normalize #_ #f #env_it #EQ destruct(EQ)] #x #xs #IH #main whd in ⊢ (% → ?); whd in match (foldr ?????); #H #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta [ whd in ⊢ (? → ???% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) cases H #_ /2/ ] #H1 #EQenv_it @IH cases H /2/ qed. definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.cont … s1 = cont … s2 ∧ match (code … s1) with [ CALL f act_p r_lb i1 ⇒ code … s2 = i1 | _ ⇒ False ]. definition operational_semantics : ∀p : state_params.∀p'.Program p p → abstract_status ≝ λp,p',prog.mk_abstract_status (state p) (execute_l ? p' (env … prog)) (is_synt_succ …) (λs.match (code … s) with [ COND _ _ _ _ _ _ ⇒ cl_jump | LOOP _ _ _ _ _ ⇒ cl_jump | EMPTY ⇒ if io_info … s then cl_io else cl_other | _ ⇒ cl_other ]) (λs.match (code … s) with [CALL _ _ m _ ⇒ match m with [ Some _ ⇒ true | None ⇒ false ] | _ ⇒ false ]) (λs.eq_instructions … (code … s) (main … prog) ∧ isnilb … (cont … s) ∧ store … s == init_store … p' ∧ io_info … s) (λs.match (cont … s) with [ nil ⇒ match (code … s) with [ EMPTY ⇒ true | RETURN _ ⇒ true | _ ⇒ false ] | _ ⇒ false ]) ???. @hide_prf [ #s1 #s2 #l #H #H1 inversion H1 #st #st' [ #hd #tl | #i #cd #s #opt_l |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m | #lin #io #lout #cd #mem | #f #act_p #r_lb #cd #mem #env_it | #r_t #mem #tl #rb #cd ] #EQcode [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQ5 #H2 #EQ' #EQ6 #EQ7 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 ] #_ destruct >EQcode in H; normalize nodelta /2 by ex_intro/ [ cases(io_info ??) normalize nodelta] #EQ destruct | #s1 #s2 #l #H #H1 inversion H1 #st #st' [ #hd #tl | #i #cd #s #opt_l |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m | #lin #io #lout #cd #mem | #f #act_p #r_lb #cd #mem #env_it | #r_t #mem #tl #rb #cd ] #EQcode [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost' #EQ6 #EQ7 #EQ8 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQiost' #EQ8 #EQ9 #EQ10 | #EQ1 #EQ2 #EQ3 #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 ] #_ destruct cases(code ? st') in H; normalize nodelta >EQiost' normalize nodelta #eq destruct try (#eq1 destruct) try (#eq2 destruct) try (#eq3 destruct) try (#eq4 destruct) try (#eq5 destruct) try (#eq6 destruct) %{lin} % | #s1 #s2 #l #H #H1 inversion H1 #st #st' [ #hd #tl | #i #cd #s #opt_l |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m | #lin #io #lout #cd #mem | #f #act_p #r_lb #cd #mem #env_it | #r_t #mem #tl #rb #cd ] #EQcode [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 | #EQ1 #EQ2 #EQ3 #EQiost #EQiost' #EQ6 #EQ7 #EQ8 | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost #EQiost' #EQ8 #EQ9 #EQ10 | #EQ1 #EQ2 #EQiost #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 ] #_ destruct >EQcode in H; normalize nodelta [|*: #EQ destruct] cases(io_info … st) in x; normalize nodelta [2: #_ #EQ destruct] #H3 #_ @H3 % ] qed. let rec eqb_list (D : DeqSet) (l1 : list D) on l1 : list D → bool ≝ match l1 with [ nil ⇒ λl2.match l2 with [nil ⇒ true | _ ⇒ false ] | cons x xs ⇒ λl2.match l2 with [ cons y ys ⇒ x == y ∧ eqb_list … xs ys | _ ⇒ false ] ]. definition DeqSet_List : DeqSet → DeqSet ≝ λX.mk_DeqSet (list X) (eqb_list …) ?. #x elim x [ * /2 by refl, conj/ #y #ys normalize % #EQ destruct] -x #x #xs #IH * [ normalize % #EQ destruct] #y #ys normalize % inversion(x == y) #EQ normalize nodelta [ #H >(proj1 … (IH ys) H) @eq_f2 [2: %] @(proj1 … (eqb_true …)) assumption | #EQ destruct | #EQ1 destruct @(proj2 … (IH …)) % | #EQ1 destruct (\b H) | >(\bf H) ] normalize /2/ qed. lemma get_element_append_r: ∀A,B. ∀l1,l2: associative_list A B. ∀x. ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) → get_element ?? (l1@l2) x = get_element … l2 x. #A #B #l1 elim l1 normalize [ #l2 #x // ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd)) #H [ >(\b H) | >(\bf H) ] normalize /2 by/ * #K cases (K I) qed. lemma get_element_append_l1 : ∀A,B. ∀l1,l2: associative_list A B. ∀x. ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l2)) → get_element ?? (l1@l2) x = get_element … l1 x. #A #B #l1 elim l1 normalize [2: #x #xs #IH #l2 #a #H >IH // ] #l2 elim l2 // #y #ys #IH #a normalize cases(a == \fst y) normalize [ * #H @⊥ @H % ] #H @IH assumption qed. lemma get_element_append_r1 : ∀A,B. ∀l1,l2: associative_list A B. ∀x. ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) → get_element ?? (l1@l2) x = get_element … l2 x. #A #B #l1 elim l1 normalize // #x #xs #IH #l2 #a cases (?==?) normalize [* #H cases H //] #H >IH normalize // qed. definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝ λx.〈a_non_functional_label x,S x〉. definition fresh_cc_labe : ℕ → CallCostLabel × ℕ ≝ λx.〈a_call_label x,S x〉. definition fresh_rc_label : ℕ → ReturnPostCostLabel × ℕ ≝ λx.〈a_return_cost_label (S x),S x〉. record call_post_info (p : instr_params) : Type[0] ≝ { gen_labels : list CostLabel ; t_code : Instructions p ; fresh : ℕ ; lab_map : associative_list DEQCostLabel CostLabel ; lab_to_keep : list ReturnPostCostLabel }. let rec call_post_trans (p : instr_params) (i : Instructions p) (n : ℕ) on i : list CostLabel → call_post_info p ≝ λabs. match i with [ EMPTY ⇒ mk_call_post_info ? abs (EMPTY …) n (nil ?) (nil ?) | RETURN x ⇒ mk_call_post_info ? abs (RETURN … x) n (nil ?) (nil ?) | SEQ x lab instr ⇒ let ih ≝ call_post_trans … instr n abs in match lab with [ None ⇒ mk_call_post_info ? (gen_labels … ih) (SEQ … x (None ?) (t_code … ih)) (fresh … ih) (lab_map … ih) (lab_to_keep … ih) | Some lbl ⇒ mk_call_post_info ? (nil ?) (SEQ … x (Some ? lbl) (t_code … ih)) (fresh … ih) (〈a_non_functional_label lbl,(a_non_functional_label lbl :: (gen_labels … ih))〉 :: (lab_map … ih)) (lab_to_keep … ih) ] | COND x ltrue i1 lfalse i2 i3 ⇒ let ih3 ≝ call_post_trans … i3 n abs in let ih2 ≝ call_post_trans … i2 (fresh … ih3) (gen_labels … ih3) in let ih1 ≝ call_post_trans … i1 (fresh … ih2) (gen_labels … ih3) in mk_call_post_info ? (nil ?) (COND … x ltrue (t_code … ih1) lfalse (t_code … ih2) (t_code … ih3)) (fresh … ih1) (〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉:: 〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉:: ((lab_map … ih1) @ (lab_map … ih2) @ (lab_map … ih3))) ((lab_to_keep … ih1) @ (lab_to_keep … ih2) @ (lab_to_keep … ih3)) | LOOP x ltrue i1 lfalse i2 ⇒ let ih2 ≝ call_post_trans … i2 n abs in let ih1 ≝ call_post_trans … i1 (fresh … ih2) (nil ?) in mk_call_post_info ? (nil ?) (LOOP … x ltrue (t_code … ih1) lfalse (t_code … ih2)) (fresh … ih1) (〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉 :: 〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉 :: ((lab_map … ih1) @ (lab_map … ih2))) ((lab_to_keep … ih1) @ (lab_to_keep … ih2)) | CALL f act_p r_lb i1 ⇒ let ih ≝ call_post_trans … i1 n abs in match r_lb with [ None ⇒ let 〈l',f''〉 ≝ fresh_rc_label (fresh … ih) in mk_call_post_info ? ((a_return_post l')::(gen_labels … ih)) (CALL … f act_p (Some ? l') (t_code … ih)) f'' (lab_map … ih) (lab_to_keep … ih) | Some lbl ⇒ mk_call_post_info ? (nil ?) (CALL ? f act_p (Some ? lbl) (t_code … ih)) (fresh … ih) (〈a_return_post lbl,(a_return_post lbl :: (gen_labels … ih))〉 :: (lab_map … ih)) (lbl :: lab_to_keep … ih) ] | IO lin io lout i1 ⇒ let ih ≝ call_post_trans … i1 n abs in mk_call_post_info ? (nil ?) (IO ? lin io lout (t_code … ih)) (fresh … ih) (〈a_non_functional_label lout,(a_non_functional_label lout :: (gen_labels … ih))〉 :: 〈a_non_functional_label lin,[a_non_functional_label lin]〉 :: (lab_map … ih)) (lab_to_keep … ih) ]. let rec call_post_clean (p : instr_params) (i : Instructions p) on i : associative_list DEQCostLabel CostLabel → list ReturnPostCostLabel → list CostLabel → option ((list CostLabel) × (Instructions p)) ≝ λm,keep,abs. match i with [ EMPTY ⇒ Some ? 〈abs,EMPTY …〉 | RETURN x ⇒ Some ? 〈abs,RETURN … x〉 | SEQ x lab instr ⇒ ! 〈l,i1〉 ← call_post_clean … instr m keep abs; match lab with [ None ⇒ return 〈l,SEQ … x (None ?) i1〉 | Some lbl ⇒ if ((get_element … m lbl) == lbl :: l) then return 〈nil ?,SEQ … x (Some ? lbl) i1〉 else None ? ] | COND x ltrue i1 lfalse i2 i3 ⇒ ! 〈l3,instr3〉 ← call_post_clean … i3 m keep abs; ! 〈l2,instr2〉 ← call_post_clean … i2 m keep l3; ! 〈l1,instr1〉 ← call_post_clean … i1 m keep l3; if ((get_element … m ltrue) == ltrue :: l1) ∧ ((get_element … m lfalse) == lfalse :: l2) then return 〈nil ?,COND … x ltrue instr1 lfalse instr2 instr3〉 else None ? | LOOP x ltrue i1 lfalse i2 ⇒ ! 〈l2,instr2〉 ← call_post_clean … i2 m keep abs; ! 〈l1,instr1〉 ← call_post_clean … i1 m keep (nil ?); if ((get_element … m ltrue) == ltrue :: l1) ∧ ((get_element … m lfalse) == lfalse :: l2) then return 〈nil ?,LOOP … x ltrue instr1 lfalse instr2〉 else None ? | CALL f act_p r_lb i1 ⇒ ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs; match r_lb with [ None ⇒ None ? | Some lbl ⇒ if (lbl ∈ keep) then if ((get_element … m lbl) == lbl :: l1) then return 〈nil ?,CALL … f act_p (Some ? lbl) instr1〉 else None ? else return 〈(a_return_post lbl) :: l1,CALL … f act_p (None ?) instr1〉 ] | IO lin io lout i1 ⇒ ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs; if ((get_element … m lout) == lout :: l1) ∧ ((get_element … m lin) == [lin]) then return 〈nil ?,IO … lin io lout instr1〉 else None ? ]. let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (a : A) (l1 : list B) (l2 : list C) (f : A → B → C → A) on l1 : option A≝ match l1 with [ nil ⇒ match l2 with [ nil ⇒ return a | cons y ys ⇒ None ? ] | cons x xs ⇒ match l2 with [ nil ⇒ None ? | cons y ys ⇒ ! ih ← (foldr2 … a xs ys f); return f ih x y ] ]. definition is_silent_cost_act_b : ActionLabel → bool ≝ λact. match act with [ cost_act x ⇒ match x with [None ⇒ true | _ ⇒ false ] | _ ⇒ false]. definition eq_ActionLabel : ActionLabel → ActionLabel → bool ≝ λc1,c2. match c1 with [ call_act f l ⇒ match c2 with [ call_act f' l' ⇒ f == f' ∧ l == l' | _ ⇒ false] | ret_act x ⇒ match c2 with [ret_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false] | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false] ] | _ ⇒ false ] | cost_act x ⇒ match c2 with [cost_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false] | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false] ] | _ ⇒ false ] | init_act ⇒ match c2 with [init_act ⇒ true | _ ⇒ false] ]. definition ret_costed_abs : list ReturnPostCostLabel → option ReturnPostCostLabel → option CostLabel ≝ λkeep,x. match x with [ Some lbl ⇒ if lbl ∈ keep then return (a_return_post lbl) else None ? | None ⇒ None ? ]. definition check_continuations : ∀p : instr_params. ∀l1,l2 : list (ActionLabel × (Instructions p)). associative_list DEQCostLabel CostLabel → list ReturnPostCostLabel → option (Prop × (list CostLabel) × (list CostLabel)) ≝ λp,cont1,cont2,m,keep. foldr2 ??? 〈True,nil ?,nil ?〉 cont1 cont2 (λx,y,z. let 〈cond,abs_top',abs_tail'〉 ≝ x in match call_post_clean p (\snd z) m keep abs_top' with [ None ⇒ 〈False,nil ?,nil ?〉 | Some w ⇒ match \fst z with [ ret_act opt_x ⇒ match ret_costed_abs keep opt_x with [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ get_element … m lbl = lbl :: (\fst w),(nil ?),abs_tail'〉 | None ⇒ 〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) @ abs_tail'〉 ] | cost_act opt_x ⇒ match opt_x with [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉 | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉] | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). (* definition check_continuations : ∀p : instr_params. ∀l1,l2 : list (ActionLabel × (Instructions p)). associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → list (list CostLabel) → option (Prop × (list CostLabel) × (list (list CostLabel))) ≝ λp,cont1,cont2,m,keep,abs_top,abs_tail. foldr2 ??? 〈True,abs_top,abs_tail〉 cont1 cont2 (λx,y,z. let 〈cond,abs_top',abs_tail'〉 ≝ x in match call_post_clean p (\snd z) m keep abs_top' with [ None ⇒ 〈False,nil ?,nil ?〉 | Some w ⇒ match \fst z with [ ret_act opt_x ⇒ match ret_costed_abs keep opt_x with [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ get_element … m lbl = lbl :: (\fst w),(nil ?),(nil ?) :: abs_tail'〉 | None ⇒ 〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) :: abs_tail'〉 ] | cost_act opt_x ⇒ match opt_x with [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉 | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉] | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). *) (* in input : abs_top is the list of labels to be propageted to the deepest level of the call stack abs_tail are the lists of labels to be propagated to the levels "below" the deepest level in output : abs_top is the list of labels to be propageted from the current level of the call stack abs_tail are the lists of labels to be propagated from the levels "below" the current level *) definition state_rel : ∀p. associative_list DEQCostLabel CostLabel → list ReturnPostCostLabel → list CostLabel →(list CostLabel) → relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2. match check_continuations ? (cont ? st1) (cont … st2) m keep with [ Some x ⇒ let 〈prf1,abs_top',abs_tail'〉 ≝ x in prf1 ∧ call_post_clean … (code … st2) m keep abs_top' = return 〈abs_top,(code … st1)〉 ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 ∧ abs_tail = abs_tail' | None ⇒ False ]. include "Simulation.ma". let rec len (s : abstract_status) (st1 : s) (st2 : s) (t : raw_trace s st1 st2) on t : ℕ ≝ match t with [ t_base s ⇒ O | t_ind s1 s2 s3 l prf lt ⇒ S (len … lt) ]. (* lemma associative_max : ∀n1,n2,n3.max (max n1 n2) n3 = max n1 (max n2 n3). #n1 #n2 #n3 normalize @leb_elim normalize [ @leb_elim normalize [ #H1 #H2 @leb_elim normalize [ @leb_elim normalize // * #H @⊥ @H assumption | @leb_elim normalize [ #H3 * #H @⊥ @H @(transitive_le … H1) assumption | * #H @⊥ @H assumption ] ] | #H1 #H2 @leb_elim normalize [ @leb_elim normalize // #_ #H cases H1 #H1 @⊥ @H1 assumption | @leb_elim normalize [ #_ * #H @⊥ @H assumption | * #H @⊥ @H @(transitive_le … H2) *) let rec compute_max_n (p : instr_params) (i : Instructions p) on i : ℕ ≝ match i with [ EMPTY ⇒ O | RETURN x ⇒ O | SEQ x lab instr ⇒ let n ≝ compute_max_n … instr in match lab with [ None ⇒ n | Some l ⇒ match l with [ a_non_functional_label n' ⇒ S (max n n') ] ] | COND x ltrue i1 lfalse i2 i3 ⇒ let n1 ≝ compute_max_n … i1 in let n2 ≝ compute_max_n … i2 in let n3 ≝ compute_max_n … i3 in let mx ≝ max (max n1 n2) n3 in match ltrue with [ a_non_functional_label lt ⇒ match lfalse with [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ] | LOOP x ltrue i1 lfalse i2 ⇒ let n1 ≝ compute_max_n … i1 in let n2 ≝ compute_max_n … i2 in let mx ≝ max n1 n2 in match ltrue with [ a_non_functional_label lt ⇒ match lfalse with [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ] | CALL f act_p r_lb i1 ⇒ let n ≝ compute_max_n … i1 in match r_lb with [ None ⇒ n | Some lbl ⇒ match lbl with [a_return_cost_label l ⇒ S(max l n) ] ] | IO lin io lout i1 ⇒ let n ≝ compute_max_n … i1 in match lin with [a_non_functional_label l1 ⇒ match lout with [a_non_functional_label l2 ⇒ S(max (max n l1) l2) ] ] ]. definition same_fresh_map_on : list CostLabel → relation (associative_list DEQCostLabel CostLabel) ≝ λdom,m1,m2.∀x.bool_to_Prop (x ∈ dom) → get_element … m1 x = get_element … m2 x. definition same_to_keep_on : list CostLabel → relation (list ReturnPostCostLabel) ≝ λdom,keep1,keep2.∀x. bool_to_Prop (a_return_post x ∈ dom) → (x ∈ keep1) = (x ∈ keep2). lemma memb_not_append : ∀D : DeqSet.∀l1,l2 : list D.∀x : D. x ∈ l1 = false → x ∈ l2 = false → x ∈ (l1 @ l2) = false. #D #l1 elim l1 [ #l2 #x #_ #H @H ] #x #xs #IH #l2 #x1 whd in match (memb ???); inversion (x1 == x) normalize nodelta [ #_ #EQ destruct] #EQx1 #EQxs #EQl2 whd in match (memb ???); >EQx1 normalize nodelta @IH // qed. lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A . no_duplicates … (l1 @ l2) → x ∈ l1 → x ∈ l2 → False. #A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???); inversion (x == x1) normalize nodelta [ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H % | #_ @IH // ] qed. lemma same_to_keep_on_append : ∀dom1,dom2,dom3 : list CostLabel. ∀l1,l2,l3,l : list ReturnPostCostLabel. no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → a_return_post x ∈ dom1) → (∀x.x ∈ l3 → a_return_post x ∈ dom3) → same_to_keep_on (dom1@dom2@dom3) (l1@l2@l3) l → same_to_keep_on dom2 l2 l. #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #sub_set1 #sub_set3 #H2 #x #Hx inversion (x ∈ l2) [ #EQkeep

memb_append_l2 // >memb_append_l1 // ] >memb_append_l2 // >memb_append_l1 // >Hx // | #EQno_keep

memb_append_l2 // >memb_append_l1 // >Hx // | @sym_eq @memb_not_append [2: @memb_not_append //] [ memb_append_l2 | >memb_append_l1] // >Hx // | @sub_set3 >H1 // | @sub_set1 >H1 // ] ] ] qed. lemma same_fresh_map_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l. no_duplicates … (dom1 @dom2 @ dom3) → (∀x.x ∈ domain_of_associative_list … l1 → x ∈ dom1) → (∀x.x ∈ domain_of_associative_list … l3 → x ∈ dom3) → same_fresh_map_on … (dom1 @dom2 @dom3) (l1 @l2 @ l3) l → same_fresh_map_on … dom2 l2 l. #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #subset1 #subset3 whd in ⊢ (% → ?); #H1 whd #x #Hx

memb_append_l2 // >memb_append_l1 // >Hx //] >get_element_append_r [ >get_element_append_l1 // ] % #K [ lapply(subset3 … K) | lapply(subset1 … K) ] #ABS [ memb_append_l2 | >memb_append_l1 ] // >Hx // qed. lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p. ∀x,n,l. x ∈ lab_to_keep … (call_post_trans … i n l) → a_return_post x ∈ get_labels_of_code … i. #p #i elim i // [ #seq #opt_l #instr #IH #x #n #l whd in match (call_post_trans ????); cases opt_l -opt_l normalize nodelta [|#lbl] whd in match (get_labels_of_code ??); #H [2: @orb_Prop_r] /2/ | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r [ >memb_append_l1 // @IH1 [3: >H // |*: ] | >memb_append_l2 // cases(memb_append … H) -H #H [>memb_append_l1 // @IH2 [3: >H // |*: ] | >memb_append_l2 // @IH3 [3: >H // |*: ] ] ] | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r [ >memb_append_l1 | >memb_append_l2 ] // [ @IH1 | @IH2 ] [3,6: >H |*: ] // | #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); inversion(x == lbl) #Hlbl normalize nodelta [* >(\P Hlbl) @orb_Prop_l @eq_costlabel_elim // * #H @H % | #H @orb_Prop_r @IH // ] | #lin #io #lout #i1 #IH #x #n #l whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); #H @orb_Prop_r @orb_Prop_r @IH // ] qed. lemma domain_of_associative_list_append : ∀A,B.∀l1,l2 : associative_list A B. domain_of_associative_list ?? (l1 @ l2) = (domain_of_associative_list ?? l1) @ (domain_of_associative_list ?? l2). #A #B #l1 elim l1 // #x #xs #IH #l2 normalize // qed. lemma lab_map_in_domain: ∀p.∀i: Instructions p. ∀x,n,l. x ∈ domain_of_associative_list … (lab_map p (call_post_trans … i n l)) → x ∈ get_labels_of_code … i. #p #i elim i // [ #seq * [|#lbl] #i1 #IH #x #n #l whd in match(call_post_trans ????); whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); inversion(x==lbl) #Hlbl normalize nodelta [#_ whd in match (memb ???); >Hlbl % ] #H >memb_cons // @IH // | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l whd in match (call_post_trans ????); whd in match (memb ???); whd in match (get_labels_of_code ??); inversion(x == ltrue) #Hlbl normalize nodelta [ #_ whd in match (memb ???); >Hlbl % ] whd in match (memb ???); inversion(x == lfalse) #Hlbl1 normalize nodelta [ #_ whd in match (memb ???); >Hlbl normalize nodelta whd in match (memb ???); >Hlbl1 % ] #H >memb_cons // >memb_cons // >domain_of_associative_list_append in H; #H cases(memb_append … H) [ #H1 >memb_append_l1 // @IH1 [3: >H1 // |*:] ] >domain_of_associative_list_append #H1 cases(memb_append … H1) #H2 >memb_append_l2 // [ >memb_append_l1 | >memb_append_l2 ] // [ @IH2 | @IH3] /2 by eq_true_to_b/ | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); whd in match (memb ???); inversion(x == lfalse) #Hlfalse normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlfalse // ] whd in match (memb ???); inversion(x==ltrue) normalize nodelta #Hltrue [ #_ whd in match (memb ???); >Hltrue %] >domain_of_associative_list_append #H cases(memb_append … H) #H1 >memb_cons // >memb_cons // [ >memb_append_l1 | >memb_append_l2 ] // [ @IH1 | @IH2] /2/ | #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); inversion (x == lbl) #Hlbl normalize nodelta [ #_ whd in match (memb ???); >Hlbl % ] #H >memb_cons // @IH /2/ | #lin #io #lout #i1 #IH #x #n #l whd in match (memb ???); inversion(x == lout) #Hlout normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlout % ] whd in match (memb ???); inversion(x==lin) #Hlin normalize nodelta [ #_ whd in match (memb ???); >Hlin % ] #H >memb_cons // >memb_cons // @IH /2/ ] qed. lemma eq_a_non_functional_label : ∀c1,c2.c1 == c2 → a_non_functional_label c1 == a_non_functional_label c2. #c1 #c2 #EQ cases(eqb_true DEQNonFunctionalLabel c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ #EQ destruct >(\b (refl …)) @I qed. let rec is_fresh_for_return (keep : list CostLabel) (n : ℕ) on keep : Prop ≝ match keep with [ nil ⇒ True | cons x xs ⇒ let ih ≝ is_fresh_for_return xs n in match x with [ a_return_post y ⇒ match y with [a_return_cost_label m ⇒ m ≤ n ∧ ih ] | _ ⇒ ih ] ]. lemma fresh_ok_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.∀l. n ≤ fresh … (call_post_trans p i1 n l). #p #i1 elim i1 normalize /2 by transitive_le, le_n/ [ #seq * [|#lbl] #i2 #IH #n #l normalize /2 by / | #cond #ltrue #i_true #lfalse #i_false #i2 #IH1 #IH2 #IH3 #n #l @(transitive_le … (IH3 …)) [2: @(transitive_le … (IH2 …)) [2: @(transitive_le … (IH1 …)) ]] // | #f #act_p * [|#lbl] normalize #i2 #IH /2 by le_S/ ] qed. lemma fresh_keep_n_ok : ∀n,m,l. is_fresh_for_return l n → n ≤ m → is_fresh_for_return l m. #n #m #l lapply n -n lapply m -m elim l // ** #x #xs #IH #n #m normalize [2: * #H1] #H2 #H3 [ %] /2 by transitive_le/ qed. definition cast_return_to_cost_labels ≝ map … (a_return_post …). coercion cast_return_to_cost_labels. lemma fresh_false : ∀n.∀l: list ReturnPostCostLabel.is_fresh_for_return l n → a_return_cost_label (S n) ∈ l = false. #n #l lapply n -n elim l // * #x #xs #IH #n whd in ⊢ (% → ??%?); * #H1 #H2 @eq_return_cost_lab_elim [ #EQ destruct @⊥ /2 by absurd/ | #_ >IH // ] qed. lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ. let dom ≝ get_labels_of_code … i1 in no_duplicates … dom → ∀m,keep. ∀info,l.call_post_trans p i1 n l = info → same_fresh_map_on dom (lab_map … info) m → same_to_keep_on dom (lab_to_keep … info) keep → is_fresh_for_return keep n → call_post_clean ? (t_code ? info) m keep l = return 〈gen_labels … info,i1〉. #p #i1 elim i1 [ #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) // | #x #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) // | #seq * [|#lbl] #instr #IH #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%%); normalize nodelta >IH // [1,4: whd whd in H2; #x #Hx @H2 whd in match (get_labels_of_code ??); // |2,5: whd whd in H1; #x #Hx [ @H1 // ] cases no_dup #H3 #_

H4 in Hx; // #H5 >H5 in H3; * #ABS @⊥ @ABS % |6: cases no_dup // ] normalize nodelta <(H1 lbl) [2: whd in match (get_labels_of_code ??); @orb_Prop_l cases(eqb_true … (a_non_functional_label lbl) lbl) #H3 #H4 >H4 % ] whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …)) % | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #n normalize nodelta #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%?); >IH3 // [2: whd in match (get_labels_of_code ??) in H2; change with ([?;?]@?) in match (?::?) in H2; associative_append >associative_append in ⊢ (??%? → ?); #H2 @(same_to_keep_on_append … H2) // [ >append_nil whd in ⊢ (??%); whd in no_dup:(??%); >associative_append // ] #x #Hx cases (memb_append … Hx) -Hx #Hx @orb_Prop_r @orb_Prop_r [ >memb_append_l1 | >memb_append_l2 ] // @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |3: -H2 whd in match (get_labels_of_code ??) in H1; change with ([?;?]@?) in match (?::?) in H1; associative_append change with ([?;?]@?) in match (?::?::?) in ⊢ (??%? → ?); associative_append in ⊢ (??%? → ?); #H1 @(same_fresh_map_on_append … H1) // [ >append_nil >associative_append // ] #x whd in match (memb ???); inversion(x == ltrue) [ #Hltrue normalize nodelta #_ whd in match (memb ???); >Hltrue % | #Hltrue normalize nodelta whd in match (memb ???); inversion(x == lfalse) [ #Hlfalse #_ @orb_Prop_r @orb_Prop_l >Hlfalse % | #Hlfalse normalize nodelta #Hx @orb_Prop_r @orb_Prop_r >domain_of_associative_list_append in Hx; #H cases(memb_append … H) #H2 [ >memb_append_l1 | >memb_append_l2 ] // @(lab_map_in_domain … (eq_true_to_b … H2)) ] ] |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |] ] normalize nodelta >IH2 [5: % |2: /2 by fresh_keep_n_ok/ |3: whd in match (get_labels_of_code ??) in H2; change with ([?;?]@?) in match (?::?) in H2; domain_of_associative_list_append #H cases(memb_append … H) [ whd in ⊢ (??%? → ?%); cases(x == ltrue) // normalize nodelta whd in ⊢ (??%? → ?%); cases(x == lfalse) // normalize nodelta normalize #EQ destruct | #H1 @orb_Prop_r @orb_Prop_r @(lab_map_in_domain … (eq_true_to_b … H1)) ] |6: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l |*: ] >m_return_bind >IH1 [5: % |2: /3 by fresh_keep_n_ok/ |3: whd in match (get_labels_of_code ??) in H2; change with ([?;?]@?) in match (?::?) in H2; change with ([ ] @ ?) in match (lab_to_keep ??) in H2; >associative_append in H2 : (??%?); #H2 @(same_to_keep_on_append … H2) // #x #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2] // @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |4: whd in match (get_labels_of_code ??) in H1; change with ([?;?]@?) in match (?::?) in H1; change with ([?;?]@?) in match (?::?::?) in H1 : (??%?); @(same_fresh_map_on_append … H1) // #x >domain_of_associative_list_append #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2 ] // @(lab_map_in_domain … (eq_true_to_b … Hx)) |6: cases no_dup #_ * #_ @no_duplicates_append_l |*: ] >m_return_bind normalize nodelta whd in H1;

(\b (refl …)) % ] whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …))

memb_cons // whd in match (memb ???); >(\b (refl …)) % ] whd in match (get_element ????); @eq_costlabel_elim normalize nodelta [ #ABS @⊥ cases no_dup >ABS * #H #_ @H @orb_Prop_l >(\b (refl ? (a_non_functional_label ltrue))) % ] #_ whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …)) % | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on #f_k whd in ⊢ (??%?); >(IH2 … (refl …)) [ normalize nodelta >(IH1 … (refl …)) [ >m_return_bind (\b (refl …)) % ] whd in match (get_element ????); inversion(a_non_functional_label ltrue == a_non_functional_label lfalse) #Hltrue normalize nodelta [ cases no_dup whd in match (memb ???); cases(eqb_true … (a_non_functional_label ltrue) (a_non_functional_label lfalse)) #H1 #_ lapply(H1 Hltrue) #EQ destruct(EQ) >(\b (refl …)) * #ABS @⊥ @ABS % ] whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …)) (\b (refl …)) % ] whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …)) % | /2 by fresh_keep_n_ok/ | change with ([?;?]@?@?) in keep_on : (?%??); change with ((nil ?) @ ? @ ?) in keep_on : (??%?); @(same_to_keep_on_append … keep_on) // #x /2 by lab_to_keep_in_domain/ | change with ([?;?]@?@?) in fresh_map : (?%%?); @(same_fresh_map_on_append … fresh_map) /2 by lab_map_in_domain/ #x whd in match (memb ???); inversion(x==lfalse) #Hlfalse normalize nodelta [ #_ @orb_Prop_r whd in match (memb ???); >Hlfalse % | whd in match (memb ???); inversion(x==ltrue) #Hltrue normalize nodelta [2: *] #_ @orb_Prop_l >Hltrue % ] | cases no_dup #_ * #_ /2/ ] | // | change with ([?;?]@?@?) in keep_on : (?%??); associative_append in ⊢ (?%%? → ?); >associative_append in ⊢ (??%? → ?); #keep_on @(same_to_keep_on_append … keep_on) // [ >associative_append >append_nil // | #x #Hx @orb_Prop_r @orb_Prop_r /2 by lab_to_keep_in_domain/ ] | change with ([?;?]@?@?) in fresh_map : (?%??); associative_append in ⊢ (?%%? → ?); >associative_append in ⊢ (??%? → ?); #fresh_map @(same_fresh_map_on_append … fresh_map) // [ >append_nil // | #x >domain_of_associative_list_append #Hx cases(memb_append … Hx) [2: #Hx1 @orb_Prop_r @orb_Prop_r @(lab_map_in_domain … (eq_true_to_b … Hx1)) ] whd in match (memb ???); inversion(x == lfalse) normalize nodelta #Hlfalse [ #_ @orb_Prop_r @orb_Prop_l >Hlfalse % | whd in match (memb ???); inversion (x==ltrue) normalize nodelta #Hltrue [ #_ @orb_Prop_l >Hltrue % | whd in match (memb ???); #EQ destruct ] ] ] | cases no_dup #_ * #_ /2 by no_duplicates_append_r/ ] | #f #act_p * [|#r_lb] #i #IH #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #fresh_map #same_keep #f_k whd in ⊢ (??%?); >(IH … (refl …)) [1,6: normalize nodelta [ >fresh_false [2: /2 by fresh_keep_n_ok/] % | (\b (refl …)) normalize nodelta (\b (refl …)) normalize nodelta >(\b (refl …)) % | whd in match (memb ???); >(\b (refl …)) % ] | whd in match (memb ???); >(\b (refl …)) % ] ] |2,7: // |3,8: whd in match (get_labels_of_code ??) in same_keep; // #x #Hx memb_cons // >Hx // ] cases no_dup * #ABS #_ whd in ⊢ (???%); inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) >Hx // |4,9: whd in match (get_labels_of_code ??) in fresh_map; // #x #Hx memb_cons // >Hx //] cases no_dup * #ABS #_ whd in ⊢ (???%); inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) // |5,10: [ @no_dup | cases no_dup // ] ] | #lin #io #lout #i #IH #n whd in match (get_labels_of_code ??); #no_dup #m #keep #info #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #fresh_map #same_keep #f_k whd in ⊢ (??%?); >(IH … (refl …)) [ normalize nodelta memb_cons // >memb_hd // ] whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …)) memb_hd //] whd in match (get_element ????); inversion(lin==lout) [ #ABS @⊥ cases no_dup * #ABS1 #_ @ABS1 whd in match (memb ???); >(\P ABS) >(\b (refl …)) // | #H inversion (a_non_functional_label lin== ? lout) [ #ABS lapply(\P ABS) #EQ destruct >(\b (refl …)) in H; #EQ destruct | #_ normalize nodelta whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …)) % ] ] | // | #x #Hx >same_keep [2: >memb_cons // >memb_cons // >Hx % ] % | #x #Hx memb_cons // >memb_cons // >Hx %] cases no_dup * #ABS1 ** #ABS2 #_ whd in ⊢ (???%); inversion(x == lout) normalize nodelta [2: #_ whd in ⊢ (???%); inversion(x==lin) normalize nodelta // #H @⊥ @ABS1 >memb_cons // <(\P H) >Hx // | #H @⊥ @ABS2 <(\P H) >Hx // ] | cases no_dup #_ * #_ // ] ] qed. definition fresh_for_prog_aux : ∀p,p'.Program p p' → ℕ → ℕ ≝ λp,p',prog,n.foldl … (λn,i.max n (compute_max_n … (f_body … i))) n (env … prog). include alias "arithmetics/nat.ma". lemma max_1 : ∀n,m,k.k ≤ m → k ≤ max m n. #m #n #k #H normalize @leb_elim // normalize nodelta #H1 /2 by transitive_le/ qed. lemma max_2 : ∀n,m,k.k≤ n → k ≤ max m n. #m #n #k #H normalize @leb_elim // #H1 normalize nodelta @(transitive_le … H) @(transitive_le … (not_le_to_lt … H1)) // qed. lemma fresh_aux_ok : ∀p,p'.∀prog : Program p p'.∀n,m.n ≤ m → fresh_for_prog_aux … prog n ≤ fresh_for_prog_aux … prog m. #p #p' * #env #main elim env // #hd #tl #IH #n #m #H whd in ⊢ (?%%); @IH whd in ⊢ (?%?); @leb_elim normalize nodelta [ #H1 @max_2 // | #_ @max_1 // ] qed. definition fresh_for_prog : ∀p,p'.Program p p' → ℕ ≝ λp,p',prog.fresh_for_prog_aux … prog (compute_max_n … (main … prog)). definition translate_env ≝ λp,p'.λenv : list (env_item p p').λmax_all.(foldr ?? (λi,x.let 〈t_env,n,m,keep〉 ≝ x in let info ≝ call_post_trans … (f_body … i) n (nil ?) in 〈(mk_env_item ?? (mk_signature ??(f_name ?? i) (f_pars … i) (f_ret … i)) (f_lab … i) (t_code … info)) :: t_env, fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 :: ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉) (〈nil ?,max_all,nil ?,nil ?〉) env). definition trans_prog : ∀p,p'.Program p p' → ((Program p p') × (associative_list DEQCostLabel CostLabel)) × ((list ReturnPostCostLabel))≝ λp,p',prog. let max_all ≝ fresh_for_prog … prog in let info_main ≝ (call_post_trans … (main … prog) max_all (nil ?)) in let 〈t_env,n,m,keep〉 ≝ translate_env … (env … prog) (fresh … info_main) in 〈mk_Program ?? t_env (t_code … info_main),m @ (lab_map … info_main),keep @ (lab_to_keep … info_main)〉. definition map_labels_on_trace : (associative_list DEQCostLabel CostLabel) → list CostLabel → list CostLabel ≝ λm,l.foldr … (λlab,t.(get_element … m lab) @ t) (nil ?) l. lemma map_labels_on_trace_append: ∀m,l1,l2. map_labels_on_trace m (l1@l2) = map_labels_on_trace m l1 @ map_labels_on_trace m l2. #m #l1 elim l1 // #hd #tl #IH #l2 >associative_append append_cons >associative_append @(p_append ? x (nil ?) xs x (nil ?) xs (refl …)) @IH qed. lemma is_permutation_append : ∀A.∀l1,l2,l3,l4 : list A. is_permutation A l1 l3 → is_permutation A l2 l4 → is_permutation A (l1 @ l2) (l3 @ l4). #A #l1 inversion (|l1|) [2: #n lapply l1 elim n [ #l2 #l3 #l4 #H inversion H // #x #x1 #x2 #y #y1 #y2 #EQ #H1 #_ #ABS cases(nil_to_nil … (sym_eq ??? ABS)) -ABS #_ #ABS cases(nil_to_nil … ABS) #EQ1 destruct(EQ1) ] #x #xs #IH #l2 #l3 #l4 #H inversion H [#EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ) ] #y #y1 #y2 #z #z1 #z2 #EQ destruct(EQ) #H1 #_ #EQx_xs #EQ destruct(EQ) #_ *) lemma memb_append_l22 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A. ¬ (x ∈ l1) → x∈ l1 @ l2 = (x ∈ l2). #A #x #l1 elim l1 normalize // #y #ys #IH #l2 cases(x==y) normalize [*] @IH qed. lemma memb_append_l12 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A. ¬ (x ∈ l2) → x∈ l1 @ l2 = (x ∈ l1). #A #x #l1 elim l1 [ #l2 #H whd in match (append ???); @not_b_to_eq_false @Prop_notb >H % ] #y #ys #IH #l2 #H1 whd in match (memb ???); >IH // qed. lemma lookup_ok_append : ∀p,p',l,f,env_it. lookup p p' l f = return env_it → ∃l1,l2. l = l1 @ [env_it] @ l2 ∧ f_name … env_it = f. #p #p' #l elim l [ #f #env_it normalize #EQ destruct] #x #xs #IH #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim [ #EQ destruct(EQ) normalize nodelta whd in ⊢ (???% → ?); #EQ destruct %{(nil ?)} %{xs} /2/ | #Hno_f normalize nodelta #EQ_env_it cases(IH … EQ_env_it) #l1 * #l2 * #EQ1 #EQ2 %{(x :: l1)} %{l2} >EQ1 /2/ ] qed. (* lemma foldr_append : ∀A,B:Type[0]. ∀l1, l2 : list A. ∀f:A → B → B. ∀seed. foldr ?? f seed (l1 @ l2) = foldr ?? f (foldr ?? f seed l2) l1. #A #B #l1 elim l1 // #hd #tl #Hind #l2 #f #seed normalize >Hind @refl qed. *) lemma foldr_map_append : ∀A,B:Type[0]. ∀l1, l2 : list A. ∀f:A → list B. ∀seed. foldr ?? (λx,acc. (f x) @ acc) seed (l1 @ l2) = append ? (foldr ?? (λx,acc. (f x) @ acc) (nil ?) l1) (foldr ?? (λx,acc. (f x) @ acc) seed l2). #A #B #l1 elim l1 normalize // /3 by eq_f, trans_eq/ qed. lemma cons_append : ∀A.∀x : A.∀l.x::l = ([x]@l). // qed. lemma eq_a_call_label : ∀c1,c2.c1 == c2 → a_call c1 == a_call c2. #c1 #c2 #EQ cases(eqb_true ? c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ #EQ destruct >(\b (refl …)) @I qed. lemma no_duplicates_append_commute : ∀ A : DeqSet.∀l1,l2 : list A. no_duplicates … (l1 @ l2) → no_duplicates … (l2 @ l1). #A #l1 elim l1 [ #l2 >append_nil //] #x #xs #IH #l2 * #H1 #H2 lapply(IH … H2) lapply H1 -H1 -IH -H2 elim l2 -l1 [ >append_nil #H1 #H2 % // ] #y #ys #IH * #H1 * #H2 #H3 % [2: @IH [ % #H4 @H1 cases(memb_append … H4) [ #H5 >memb_append_l1 // | #H5 >memb_append_l2 // @orb_Prop_r >H5 // ] | // ] | % #H4 cases(memb_append … H4) [ #H5 @(absurd ?? H2) >memb_append_l1 // | whd in match (memb ???); inversion(y==x) [ #H5 #_ <(\P H5) in H1; #H1 @H1 >memb_append_l2 // | #_ normalize nodelta #H5 @(absurd ?? H2) >memb_append_l2 // ] ] ] qed. (* aggiungere fresh_to_keep al lemma seguente??*) let rec subset (A : Type[0]) (l1,l2 : list A) on l1 : Prop ≝ match l1 with [ nil ⇒ True | cons x xs ⇒ mem … x l2 ∧ subset … xs l2 ]. interpretation "subset" 'subseteq a b = (subset ? a b). lemma subset_append_l2 : ∀A,l2,l1.subset A l2 (l1 @ l2). #A #l2 elim l2 // normalize #x #xs #IH #l1 % // @mem_append_l2 whd /2/ qed. lemma refl_subset : ∀A.reflexive … (subset A). #A #l1 elim l1 // #x #xs #IH normalize % /2/ qed. lemma fresh_for_subset : ∀l1,l2,n.l1 ⊆ l2 → is_fresh_for_return … l2 n → is_fresh_for_return … l1 n. #l1 elim l1 // ** #x #xs #IH #l2 #n * #H1 #H2 #H3 whd try(@IH) // % [2: @IH //] elim l2 in H1 H3; normalize [*] ** #y #ys #IH normalize [2,3: * [2,4: #H3 [2: @IH //] * #H4 #H5 @IH // |*: #EQ destruct * // ]] * [ #EQ destruct ] #H3 #H4 @IH // qed. lemma fresh_append : ∀n,l1,l2.is_fresh_for_return l1 n → is_fresh_for_return l2 n → is_fresh_for_return (l1@l2) n. #n #l1 lapply n -n elim l1 // ** #x #xs #IH #n #l2 [2: * #H1 ] #H2 #H3 [ % // @IH //] @IH // qed. definition labels_of_prog : ∀p,p'.Program p p' → ? ≝ λp,p',prog.foldr … (λx,l.l @ (get_labels_of_code … (f_body … x))) (get_labels_of_code … (main … prog)) (env … prog). lemma cast_return_append : ∀l1,l2.cast_return_to_cost_labels … (l1 @ l2) = (cast_return_to_cost_labels … l1) @ (cast_return_to_cost_labels … l2). #l1 #l2 @(sym_eq … (map_append …)) qed. include alias "arithmetics/nat.ma". lemma is_fresh_code : ∀p.∀i : Instructions p. is_fresh_for_return (get_labels_of_code … i) (compute_max_n … i). #p #main elim main // [ #seq * [| * #lbl] #i #IH normalize // @(fresh_keep_n_ok … IH) inversion(leb ? lbl) // @leb_elim #Hlbl #EQ destruct normalize nodelta /2 by le_S/ | #cond * #ltrue #i1 * #lfalse #i2 #i3 #IH1 #IH2 #IH3 whd in ⊢ (?%%); @fresh_append [ @(fresh_keep_n_ok … IH1) @le_S @max_1 @max_1 @max_1 @max_1 // | @fresh_append [ @(fresh_keep_n_ok … IH2) @le_S @max_1 @max_1 @max_1 @max_2 // | @(fresh_keep_n_ok … IH3) @le_S @max_1 @max_1 @max_2 // ] ] | #cond * #ltrue #i1 * #lfalse #i2 #IH1 #IH2 whd in ⊢ (?%%); @fresh_append [ @(fresh_keep_n_ok … IH1) @le_S @max_1 @max_1 @max_1 // | @(fresh_keep_n_ok … IH2) @le_S @max_1 @max_1 @max_2 // ] | #f #act_p * [| * #lbl] #i #IH whd in ⊢ (?%%); // change with ([?]@?) in ⊢ (?%?); @fresh_append [ whd % // @le_S @max_1 // | @(fresh_keep_n_ok … IH) @le_S @max_2 // ] | * #lin #io * #lout #i #IH whd in ⊢ (?%%); @(fresh_keep_n_ok … IH) @le_S @max_1 @max_1 // ] qed. lemma is_fresh_fresh_for_prog : ∀p,p'.∀prog : Program p p'. is_fresh_for_return (labels_of_prog … prog) (fresh_for_prog … prog). #p #p' * #env #main whd in match fresh_for_prog; normalize nodelta whd in ⊢ (?%?); elim env // * #sig #cost #i #tail #IH whd in ⊢ (?%?); @fresh_append [ @(fresh_keep_n_ok … IH) @fresh_aux_ok @max_1 // | @(fresh_keep_n_ok … (is_fresh_code … i)) whd in match fresh_for_prog_aux; normalize nodelta whd in ⊢ (??%); elim tail [ @max_2 // ] #hd1 #tl1 #IH1 @(transitive_le … IH1) whd in ⊢ (??%); change with (fresh_for_prog_aux ?? (mk_Program ?? tl1 main) ?) in ⊢ (?%%); @fresh_aux_ok @max_1 // ] qed. lemma subset_def : ∀A : DeqSet.∀l1,l2 : list A.(∀x.x ∈l1 → x ∈ l2) → l1 ⊆ l2. #A #l1 elim l1 // #x #xs #IH #l2 #H % [ @memb_to_mem >H // >memb_hd // | @IH #y #H1 @H >memb_cons // >H1 // ] qed. lemma memb_cast_return : ∀keep,x.x ∈ cast_return_to_cost_labels keep → ∃ y.x = a_return_post y ∧ bool_to_Prop (y ∈ keep). #keep elim keep [ #x *] #x #xs #IH #y whd in match cast_return_to_cost_labels; whd in match (map ????); whd in match (memb ???); inversion(y==x) [ #Hx #_ %{x} >(\P Hx) %{(refl …)} >memb_hd // | #Hx normalize nodelta #H cases(IH … H) #z * #H1 #H2 %{z} %{H1} >memb_cons // >H2 // ] qed. lemma subset_append : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l2 ⊆ l3 → (l1 @ l2) ⊆ l3. #A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 % /2/ qed. lemma subset_def_inv : ∀A.∀l1,l2 : list A. l1 ⊆ l2 → ∀x.mem … x l1 → mem … x l2. #A #l1 elim l1 [ #l2 * #x * ] #x #xs #IH #l2 * #H1 #H2 #y * [ #EQ destruct // | #H3 @IH // ] qed. lemma transitive_subset : ∀A.transitive … (subset A). #A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 % [ @(subset_def_inv … H3) // | @IH // ] qed. lemma subset_append_h1 : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l1 ⊆ (l3 @ l2). #A #l1 elim l1 // #x #x2 #IH #l2 #l3 * #H1 #H2 % [ @mem_append_l1 // | @IH // ] qed. lemma subset_append_h2 : ∀A.∀l1,l2,l3 : list A.l2 ⊆ l3 → l2 ⊆ (l1 @ l3). #A #l1 elim l1 // #x #xs #IH #l2 elim l2 // #y #ys #IH #l3 * #H1 #H2 % [ @mem_append_l2 // | @IH // ] qed. lemma lab_to_keep_in_prog : ∀p,p'.∀prog : Program p p'. ∀t_prog,m,keep.trans_prog … prog = 〈t_prog,m,keep〉 → (cast_return_to_cost_labels keep) ⊆ (labels_of_prog p p' prog). #p #p' * #env #main #t_prog #m #keep whd in match trans_prog; normalize nodelta @pair_elim * #env1 #fresh * #m1 #keep1 #EQenv1 normalize nodelta #EQ destruct lapply EQenv1 -EQenv1 lapply keep1 -keep1 lapply m1 -m1 lapply fresh -fresh lapply env1 -env1 generalize in match (fresh_for_prog ???); elim env [ #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct whd in match (append ???); @subset_def #x #H whd in match (labels_of_prog); normalize nodelta whd in match (foldr ?????); cases(memb_cast_return … H) -H #x1 * #EQ1 #H destruct @(lab_to_keep_in_domain … H) | #x #xs #IH #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); @pair_elim * #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail change with (translate_env ????) in match (foldr ?????); #EQt_env_tail normalize nodelta #EQ1 destruct >cast_return_append @subset_append [ >cast_return_append @subset_append [ whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); @subset_def #y #H cases(memb_cast_return … H) -H #y1 * #EQ destruct #H >memb_append_l2 // @(lab_to_keep_in_domain … H) | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); change with (labels_of_prog ?? (mk_Program ?? xs ?)) in match (foldr ?????); @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail)) >cast_return_append @subset_append_h1 // ] | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); change with (labels_of_prog ?? (mk_Program ?? xs ?)) in match (foldr ?????); @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail)) >cast_return_append @subset_append_h2 // ] ] qed. lemma fresh_call_post_trans_ok : ∀p.∀i : Instructions p.∀n,l. n ≤ fresh … (call_post_trans … i n l). #p #i elim i // qed. lemma fresh_translate_env_ok : ∀p,p'.∀env,t_env : list (env_item p p').∀n,n1,m,keep. translate_env … env n = 〈t_env,n1,m,keep〉 → n ≤ n1. #p #p' #env elim env [ #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct // ] #x #xs #IH #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?); change with (translate_env ????) in match (foldr ?????); @pair_elim * #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail #EQt_env_tail normalize nodelta #EQ destruct @(transitive_le … (IH … EQt_env_tail)) @fresh_call_post_trans_ok qed. lemma trans_env_ok : ∀p : state_params.∀ prog. no_duplicates_labels … prog → let 〈t_prog,m,keep〉 ≝ trans_prog … prog in ∀f,env_it.lookup p p (env … prog) f = return env_it → let dom ≝ get_labels_of_code … (f_body … env_it) in ∃env_it',n.is_fresh_for_return keep n ∧lookup p p (env … t_prog) f = return env_it' ∧ let info ≝ call_post_trans … (f_body … env_it) n (nil ?) in t_code … info = f_body … env_it' ∧ get_element … m (a_call (f_lab … env_it')) = (a_call (f_lab … env_it')) :: gen_labels … info ∧ f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it' ∧ same_fresh_map_on dom m (lab_map … info) ∧ same_to_keep_on dom keep (lab_to_keep … info). #p #prog inversion(trans_prog … prog) * #t_prog0 #m0 #keep0 #EQt_prog lapply EQt_prog normalize nodelta generalize in match keep0 in ⊢ (% → ? → ? → ? → ? → ??(λ_.??(λ_.?%?))); #keep1 #EQkeep1 inversion prog in EQt_prog; #env #main #EQprog whd in match trans_prog; normalize nodelta @pair_elim cut(fresh_for_prog ?? prog ≤ fresh_for_prog ?? (mk_Program … env main)) [ >EQprog //] generalize in match (fresh_for_prog ???) in ⊢ (??% → %); lapply t_prog0 lapply m0 lapply keep0 elim env in ⊢ (?→ ? → ? → ? → ? → %); [ #keep #m #t_prog #n #_ * #env' #fresh * #x #y #_ #_ #_ #f #env_it normalize in ⊢ (% → ?); #ABS destruct] * #hd_sig #hd_lab #hd_code #tail #IH #keep #m #t_prog #fresh1 #Hfresh1 * #env' #fresh * #m' #keep' normalize in ⊢ (% → ?); normalize nodelta @pair_elim * #env_tail #fresh_tail * #m_tail #keep_tail change with (translate_env ????) in ⊢ (??%? → ?); #EQtail normalize nodelta #EQ1 destruct(EQ1) #EQ2 destruct(EQ2) whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H) change with (no_duplicates_labels p p (mk_Program p p tail main)) in match (no_duplicates_labels p p (mk_Program p p tail main)); #no_dup_tail lapply(no_duplicates_append_l … H) #no_dup_head normalize nodelta #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta [ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ) inversion (call_post_trans … hd_code fresh_tail []) #gen_labs #t_hd_code #t_fresh #t_lab_map #t_lab_to_keep #EQ_trans_code %{(mk_env_item … hd_sig hd_lab t_hd_code)} %{fresh_tail} % [ % [ @(fresh_keep_n_ok … fresh1) [ @(fresh_keep_n_ok … Hfresh1) @(fresh_for_subset … (labels_of_prog … prog)) [ @(lab_to_keep_in_prog … EQkeep1) | @is_fresh_fresh_for_prog ] | @(transitive_le … (fresh_translate_env_ok … EQtail)) // ] | whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta @eq_f cases hd_sig // ]] >EQ_trans_code % [% [ % [ % [% // whd in ⊢ (??%?); >(\b (refl …)) %] % ] % | whd #x #Hx whd in ⊢ (??%?); >(? : (x == hd_lab) = false) [2: inversion(x==hd_lab) // #EQx_hdlab cases Hhd_lab -Hhd_lab #Hhd_lab cases Hhd_lab >memb_append_l1 // <(\P EQx_hdlab) >Hx // ] normalize nodelta >get_element_append_l1 [2: % #ABS @(memb_no_duplicates_append … x … H) // elim tail [ whd in match (foldr ?????); @lab_map_in_domain // ] #x #xs #IH whd in match (foldr ?????); @orb_Prop_r >memb_append_l2 // >IH % ] @get_element_append_l1 % #H1 (* subproof with no nice statement *) lapply H1 -H1 lapply H -H lapply Hhd_lab -Hhd_lab lapply EQtail -EQtail generalize in match fresh1; lapply env_tail -env_tail lapply fresh_tail -fresh_tail lapply m_tail -m_tail lapply keep_tail -keep_tail elim tail normalize nodelta [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); #EQ destruct(EQ) whd in match (foldr ?????); #H1 #H2 * ] #head #tail #IH #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); whd in match (foldr ?????); @pair_elim * #env_tail_res #fresh_tail_res * #lab_map_res #keep_res #EQres normalize nodelta #EQ destruct(EQ) whd in match (foldr ?????); #H1 #H2 whd in match (memb ???); inversion(x == ?) [ #H3 #_ <(\P H3) in H2; change with ([?]@?) in match (?::?); #H2 lapply(no_duplicates_append_commute … H2) -H2 ** #ABS #_ @ABS >memb_append_l2 // >Hx % | #H3 normalize nodelta #H4 @(IH … EQres) [3: >domain_of_associative_list_append in H4; #H4 cases(memb_append … H4) [2: #EQ >EQ %] #ABS @⊥ @(memb_no_duplicates_append … x … H2) // @orb_Prop_r >memb_append_l1 // @(lab_map_in_domain … (eq_true_to_b … ABS)) | % #ABS elim H1 -H1 #H1 @H1 cases(memb_append … ABS) [ #H5 >memb_append_l1 // | #H5 >memb_append_l2 // @orb_Prop_r >memb_append_l2 // ] | lapply(no_duplicates_append_commute … H2) * #_ >associative_append #h @no_duplicates_append_commute @(no_duplicates_append_r … h) ] ] ] | whd #x #Hx >memb_append_l12 [2: @notb_Prop % #ABS @(memb_no_duplicates_append … H … Hx) elim tail [ whd in match (foldr ?????); @lab_to_keep_in_domain // ] #x #xs #IH whd in match (foldr ?????); @orb_Prop_r >memb_append_l2 // >IH % ] >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … (a_return_post x) … H) // @⊥ (* subproof with no nice statement *) lapply ABS -ABS lapply H -H lapply Hhd_lab -Hhd_lab lapply EQtail -EQtail generalize in match fresh1; lapply env_tail -env_tail lapply fresh_tail -fresh_tail lapply m_tail -m_tail lapply keep_tail -keep_tail elim tail normalize nodelta [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); #EQ destruct(EQ) whd in match (foldr ?????); #H1 #H2 whd in ⊢ (??%? → ?); #EQ destruct ] #head #tail #IH #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); whd in match (foldr ?????); @pair_elim * #env_tail_res #fresh_tail_res * #lab_map_res #keep_res #EQres normalize nodelta #EQ destruct(EQ) whd in match (foldr ?????); #H1 #H2 #H3 cases(memb_append … H3) -H3 [ #H3 change with ([?]@?) in match (?::?) in H2; lapply(no_duplicates_append_commute … H2) -H2 * #_ #H4 @(memb_no_duplicates_append … (a_return_post x) … H4) [ whd in match (append ???); >memb_append_l1 // >(lab_to_keep_in_domain … (eq_true_to_b … H3)) % | // ] | #H3 normalize nodelta @(IH … EQres) [3: // | % #ABS elim H1 -H1 #H1 @H1 cases(memb_append … ABS) [ #H5 >memb_append_l1 // | #H5 >memb_append_l2 // @orb_Prop_r >memb_append_l2 // ] | lapply(no_duplicates_append_commute … H2) * #_ >associative_append #h @no_duplicates_append_commute @(no_duplicates_append_r … h) ] ] ] | #Hf #Henv_it cases(IH … no_dup_tail … Henv_it) [9: >EQtail in ⊢ (??%?); % |13: % |6: assumption |10: % |*: ] #new_env_it * #new_fresh ** #is_fresh_newfresh #EQlook_new_env_it ***** #EQt_code #EQ_get_el #EQsign_env_it #EQ_f_lab #same_fresh_map #same_to_keep %{new_env_it} %{new_fresh} % [ % [ assumption | whd in ⊢ (??%?); @eq_function_name_elim [ #ABS >ABS in Hf; * #H @⊥ @H %] #_ normalize nodelta assumption ]] % [2: #x #Hx associative_append @memb_append_l22 inversion(memb ???) // #ABS lapply(lab_to_keep_in_domain … (eq_true_to_b … ABS)) #ABS1 @(memb_no_duplicates_append … (a_return_post x) … H) // cases(lookup_ok_append … Henv_it) #l1 * #l2 * #EQ1 #EQ2 destruct(EQ1 EQ2) >foldr_map_append >memb_append_l2 // >foldr_map_append >memb_append_l1 // whd in match (foldr ?????); @orb_Prop_r >memb_append_l1 // >Hx % ] % [2: #x #Hx cons_append associative_append @(get_element_append_r1) % >domain_of_associative_list_append #ABS cases(memb_append … ABS) [ whd in match (memb ???); inversion(x==hd_lab) normalize nodelta [2: #_ whd in match (memb ???); #EQ destruct ] #EQx_hdlab #_ <(\P EQx_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it) #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 // >memb_append_l1 // whd in ⊢ (??%?); cases(x==?) // normalize nodelta >memb_append_l1 // >Hx % | #ABS1 @(memb_no_duplicates_append … x … H) [ @(lab_map_in_domain … (eq_true_to_b … ABS1)) | cases(lookup_ok_append … Henv_it) #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append >memb_append_l2 // >memb_append_l1 // whd in ⊢ (??%?); cases(x==?) // normalize nodelta >memb_append_l1 // >Hx % ] ] ] % // % // % // cons_append associative_append @get_element_append_r1 % >domain_of_associative_list_append #ABS cases(memb_append … ABS) [ whd in match (memb ???); inversion(a_call (f_lab … new_env_it)== a_call hd_lab) #EQ_hdlab normalize nodelta [2: whd in ⊢ (??%? → ?); #EQ destruct ] #_ <(\P EQ_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it) #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 // >memb_append_l1 // whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) // | #ABS1 @(memb_no_duplicates_append … (a_call (f_lab … new_env_it)) … H) [ @(lab_map_in_domain … (eq_true_to_b … ABS1)) | cases(lookup_ok_append … Henv_it) #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append >memb_append_l2 // >memb_append_l1 // whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) // ] ] ] qed. lemma len_append : ∀S : abstract_status.∀st1,st2,st3 : S. ∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3. len … (t1 @ t2) = len … t1 + len … t2. #S #st1 #st2 #st3 #t1 elim t1 normalize // qed. axiom permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y. (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7) →is_permutation A ((l6 @l2) @l7) ((l3 @l8) @l9) →is_permutation A (y ::((l6 @((x ::l5) @(l1 @l2))) @l7)) (((x ::l4 @y ::l3) @l8) @l9)). lemma append_premeasurable : ∀S : abstract_status. ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2: raw_trace … st2 st3. pre_measurable_trace … t1 → pre_measurable_trace … t2 → pre_measurable_trace … (t1 @ t2). #S #st1 #st2 #st3 #t1 #t2 #Hpre lapply t2 -t2 elim Hpre -Hpre // [ #s1 #s2 #s3 #l #prf #tl #Hclass #Hcost #pre_tl #IH #t2 #pr3_t2 %2 // @IH // | #s1 #s2 #s3 #l #Hclass #prf #tl #ret_l #pre_tl #IH #t2 #pre_t2 %3 // @IH // | #s1 #s2 #s3 #l #prf #tl #Hclass #call #callp #pre_tl #IH #t2 #pre_t2 %4 // @IH // | #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #tl1 #tl2 #prf2 #Hclass1 #Hclass3 #call_l1 #nopost #pre_tl1 #pre_tl2 #succ #unlab #IH1 #IH2 #t2 #pre_t2 normalize >append_associative in ⊢ (????(???????%)); %5 // @IH2 // ] qed. lemma correctness_lemma : ∀p,p',prog. no_duplicates_labels … prog → let 〈t_prog,m,keep〉 ≝ trans_prog … prog in ∀s1,s2,s1' : state p.∀abs_top,abs_tail. ∀t : raw_trace (operational_semantics … p' prog) s1 s2. pre_measurable_trace … t → state_rel … m keep abs_top abs_tail s1 s1' → ∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'. state_rel … m keep abs_top' abs_tail' s2 s2' ∧ is_permutation ? ((abs_top @ (map_labels_on_trace m (get_costlabels_of_trace … t))) @ abs_tail) (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail') ∧ len … t = len … t' ∧ (∀k.∀i.option_hd … (cont … s2) = Some ? 〈ret_act (None ?),i〉 → cont … s1 = k @ cont … s2 → ∃k'.cont … s1' = k' @ cont … s2' ∧ |k| = |k'|) ∧ pre_measurable_trace … t'. #p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans #s1 #s2 #s1' #abs_top #abs_tail #t #Hpre lapply abs_top -abs_top lapply abs_tail -abs_tail lapply s1' -s1' elim Hpre [ #st #Hst #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)} % [ % [ % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil @is_permutation_eq | #k #i #_ #EQcont_st %{[ ]} % // @sym_eq @eq_f @append_l1_injective_r // ] | %1 whd in H; cases(check_continuations ?????) in H; [*] ** #H1 #abs_top_cont #abs_tail_cont normalize nodelta **** #_ #rel #_ #H2 #_ normalize inversion(code ??) normalize nodelta [|#r_t| #seq #lbl #i #_ | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ | #cond #ltrue #i1 #lfalse #i2 #_ #_ | #f #act_p #rlbl #i #_ | #lin #io #lout #i #_ ] #EQcode_s1' normalize nodelta [|*: % #EQ destruct]

EQcode_s1' in rel; whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize in Hst; EQcont11 in ⊢ (% → ?); whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????); inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1' normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????); inversion(check_continuations ?????) [ #_ *] ** #H1 #l2 #ll2 #EQHl2 >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ ***** ] * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) ***** | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1; normalize * /2/ ] * [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ) #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1') [ | #x | #seq #lbl #i #_ | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ | #cond #ltrue #i1 #lfalse #i2 #_ #_ | #f #act_p #ret_post #i #_ | #l_in #io #l_out #i #_ ] [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)] cases(call_post_clean ?????) normalize nodelta [1,3,5,7,9: #EQ destruct(EQ)] [ * #z1 #z2 cases lbl normalize nodelta [|#z3 cases(?==?) normalize nodelta] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | * #z1 #z2 cases(call_post_clean ?????) [| * #z3 #z4 ] whd in ⊢ (??%% → ?); [2: cases(call_post_clean ?????) normalize nodelta [| * #z5 #z6 cases(?∧?) normalize nodelta]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | * #z1 #z2 cases(call_post_clean ?????) [| * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | * #z1 #z2 cases ret_post normalize nodelta [| #z3 cases(memb ???) normalize nodelta [ cases(?==?) normalize nodelta] ] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | * #z1 #z2 cases(?∧?) normalize nodelta whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ) cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …) [2: whd whd in match check_continuations; normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2 normalize nodelta % // % // % // % // @EQcode_c_st12 ] #abs_top' * #abs_tail' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety #pre_t' %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) … t')} [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉) [3: assumption |4: assumption |*:] /3 by nmk/ ] % [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts] * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%); [ EQk1 % | whd in ⊢ (??%%); @eq_f // ] ] %2 // [2: % //] normalize >EQcodes1' normalize nodelta EQcode11 in class_st11; // | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ) #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?); inversion(code … s1') [ | #x | #seq #lbl #i #_ | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ | #cond #ltrue #i1 #lfalse #i2 #_ #_ | #f #act_p #ret_post #i #_ | #l_in #io #l_out #i #_ ] [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | cases(call_post_clean ?????) normalize nodelta [| * #z2 #z3 cases lbl normalize nodelta [| #z4 cases(?==?) normalize nodelta] ] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | cases(call_post_clean ?????) normalize nodelta [| * #z2 #z3 cases(call_post_clean ?????) [| * #z4 #z5 >m_return_bind cases(call_post_clean ?????) [| * #z6 #z7 >m_return_bind cases(?∧?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | cases(call_post_clean ?????) normalize nodelta [| * #z2 #z3 cases(call_post_clean ?????) [| * #z4 #z5 >m_return_bind cases(?∧?) normalize nodelta ]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | cases(call_post_clean ?????) normalize nodelta [| * #z1 #z2 cases ret_post normalize nodelta [| #z3 cases(memb ???) normalize nodelta [ cases (?==?) normalize nodelta]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | cases(call_post_clean ?????) normalize nodelta [| * #z1 #z2 cases(?∧?) normalize nodelta ] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ) cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …) [2: whd whd in match check_continuations; normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]); normalize nodelta % // % // % // % // @EQcode_c_st12 ] #abs_top' * #abs_tail' * #st3' * #t' **** #Hst3st3' #EQcost #EQlen #stack_safety #pre_t' %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (Some ? lbl)) … t')} [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉) [3: assumption |4: assumption |*:] /3 by nmk/ ] % [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el @is_permutation_cons assumption | * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%); [ EQk1 % | whd in ⊢ (??%%); @eq_f // ] ]] %2 // [2: % //] normalize >EQcodes1' normalize nodelta EQcode11 in class_st11; // ] | #seq #i #mem * [|#lbl] #EQcode_st11 #EQeval_seq #EQ destruct(EQ) #EQcont #EQ destruct(EQ) #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hst11 #_ #Hpre_t #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????) normalize nodelta [1,3: #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1 [ >EQcode_st11 in ⊢ (% → ?); | >EQcode_st11 in ⊢ (% → ?); ] inversion(code ??) [1,2,4,5,6,7,8,9,11,12,13,14: [1,7: #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |2,8: #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |3,9: #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |4,10: #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |5,11: #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases lbl normalize nodelta [2,4: #l1 cases(memb ???) normalize nodelta [1,3: cases(?==?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |6,12: #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #seq1 #opt_l #i' #_ #EQcode_s1' change with (m_bind ?????) in ⊢ (??%? → ?); inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_labs #i'' #EQclean >m_return_bind inversion(opt_l) normalize nodelta [2,4: #lab1 ] #EQ destruct(EQ) [1,2: inversion(?==?) normalize nodelta #EQget_el ] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore #EQinfo #EQ destruct(EQ) cases(IH … (mk_state ? i' (cont … s1') (store … st12) (io_info … s1')) abs_tail_cont ?) [3,6: whd [ EQcheck in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); | EQcheck in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); ] normalize nodelta % // % // % // % // assumption |2,5: ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety #pre_t' %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')} [1,4: @hide_prf @(seq_sil … EQcode_s1') // |2,5: ] % [1,3: % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} [2: assumption] whd in ⊢ (??%%); whd in match (get_costlabels_of_trace ????); whd in match (map_labels_on_trace ??); >(\P EQget_el) @is_permutation_cons assumption |*: #k #i #EQcont_st3 >EQcont #EQ cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % // ]] %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12 #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??) [1,2,3,5,6,7: [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta [2: #l1 cases(?==?) normalize nodelta]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases lbl normalize nodelta [2,4: #l1 cases(memb ???) normalize nodelta [1,3: cases(?==?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_ifalse1 #i_false' #EQi_false' >m_return_bind inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_i_true' #i_true' #EQi_true' >m_return_bind inversion(?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) normalize nodelta #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ) cases(IH … (mk_state ? i_true1 (〈cost_act (None ?),i'〉 :: cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_lab_i_true') [2: whd whd in match (check_continuations ?????); >EQcont_st12 in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); whd in match (foldr2 ???????); change with (check_continuations ?????) in match (foldr2 ???????); >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % // ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety #pre_t' %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')} [ @hide_prf @(cond_true … EQcode_s1') // | ] % [ % [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??); >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons assumption | #k #i1 #EQcont_st3 #EQcont_st11 cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …) [2: >EQcont_st12 >EQcont_st11 % ] * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct %{tl1} % // whd in EQk1 : (??%%); destruct // ]] %2 // [2: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12 #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??) [1,2,3,5,6,7: [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta [2: #l1 cases(?==?) normalize nodelta]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases lbl normalize nodelta [2,4: #l1 cases(memb ???) normalize nodelta [1,3: cases(?==?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_ifalse1 #i_false' #EQi_false' >m_return_bind inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_i_true' #i_true' #EQi_true' >m_return_bind inversion(?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) normalize nodelta #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ) cases(IH … (mk_state ? ifalse1 (〈cost_act (None ?),i'〉 :: cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_lab_ifalse1) [2: whd whd in match (check_continuations ?????); >EQcont_st12 in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); whd in match (foldr2 ???????); change with (check_continuations ?????) in match (foldr2 ???????); >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % // ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety #pre_t' %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')} [ @hide_prf @(cond_false … EQcode_s1') // | ] % [ % [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??); >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons assumption | #k #i1 #EQcont_st3 #EQcont_st11 cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …) [2: >EQcont_st12 >EQcont_st11 % ] * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct %{tl1} % // whd in EQk1 : (??%%); destruct // ] ] %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??) [1,2,3,4,6,7: [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta [2: #l1 cases(?==?) normalize nodelta]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases lbl normalize nodelta [2,4: #l1 cases(memb ???) normalize nodelta [1,3: cases(?==?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct ] * #gen_itrue1 #i_true2 #EQi_true2 >m_return_bind inversion (?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_11 #EQ_info11 #EQ destruct cases(IH … (mk_state ? i_true1 (〈cost_act (None ?),LOOP … cond ltrue i_true1 lfalse i_false1〉 :: cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_itrue1) [2: whd >EQcont_st12 whd in match (check_continuations ?????); whd in match (foldr2 ???????); change with (check_continuations ?????) in match (foldr2 ???????); >EQcheck normalize nodelta whd in match (call_post_clean ?????); >EQi_false2 normalize nodelta >EQi_true2 >m_return_bind >EQget_ltrue1 >EQget_lfalse1 normalize nodelta % // % // % // % [2: assumption] % // % // ] #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')} [ @hide_prf @(loop_true … EQcode_s1') // |] % [ % [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'} whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??); >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons assumption | #k #i1 #EQcont_st3 #EQcont_st11 cases(stack_safety … (〈cost_act (None NonFunctionalLabel), LOOP p cond ltrue (code p st12) lfalse i_false〉::k) … EQcont_st3 …) [2: >EQcont_st12 >EQcont_st11 % ] * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct %{tl1} % // whd in EQk1 : (??%%); destruct // ] ] %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??) [1,2,3,4,6,7: [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta [2: #l1 cases(?==?) normalize nodelta]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases lbl normalize nodelta [2,4: #l1 cases(memb ???) normalize nodelta [1,3: cases(?==?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct ] * #gen_itrue1 #i_true2 #EQi_true2 >m_return_bind inversion (?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_11 #EQ_info11 #EQ destruct cases(IH … (mk_state ? i_false1 (cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_ifalse1) [2: whd >EQcont_st12 whd in match (check_continuations ?????); whd in match (foldr2 ???????); change with (check_continuations ?????) in match (foldr2 ???????); >EQcheck normalize nodelta whd in match (call_post_clean ?????); >EQi_false2 normalize nodelta >EQi_true2 % // % // % // % [2: %] // ] #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')} [ @hide_prf @(loop_false … EQcode_s1') // |] % [ % [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'} whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??); >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons assumption | #k #i #EQcont_st3 EQcode_s1' normalize nodelta % #EQ destruct | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12 #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre #IH #s1' #abs_top #abs_tail whd in ⊢ (% → ?); inversion(check_continuations ?????) [#_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??) [1,2,3,4,5,6: [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta [2: #l1 cases(?==?) normalize nodelta]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases lbl normalize nodelta [2,4: #l1 cases(memb ???) normalize nodelta [1,3: cases(?==?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #lin1 #io1 #lout1 #i1 #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #gen_lab #i2 #EQ_i2 inversion(?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_lout1 inversion(?==?) #EQget_lin1 normalize nodelta whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQinfo11 #EQ destruct cases(IH … (mk_state ? (EMPTY p) (〈cost_act (Some ? lout),i1〉::cont … s1') (store … st12) true) abs_tail_cont [ ]) [2: whd >EQcont_st12 whd in match (check_continuations ?????); whd in match (foldr2 ???????); change with (check_continuations ?????) in match (foldr2 ???????); >EQcheck normalize nodelta >EQ_i2 normalize nodelta % // % // % // % [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) % ] #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')} [ @hide_prf @(io_in … EQcode_s1') // |] % [ % [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'} whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??); >(\P EQget_lin1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons assumption | #k #i1 #EQcont_st3 #EQcont_st11 cases(stack_safety … (〈cost_act (Some ? lout),i〉::k) … EQcont_st3 …) [2: >EQcont_st12 >EQcont_st11 %] * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct %{tl1} % // whd in EQk1 : (??%%); destruct // ]] %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ) | #r_t #mem #con #rb #i #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 #EQ11 #EQ12 destruct #t #_ * #nf #EQ destruct ] | #st1 #st2 #st3 #lab #st1_noio #H inversion H in ⊢ ?; [1,2,3,4,5,6,7,8: [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21 ] destruct #tl * #y #EQ destruct(EQ) @⊥ >EQ in x12; * #ABS @ABS % ] #st11 #st12 #r_t #mem #cont * [|#x] #i #EQcode_st11 #EQcont_st11 #EQ destruct(EQ) #EQio_11 #EQio_12 #EQev_ret #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct(EQ1 EQ2 EQ3 EQ4 EQ5 EQ6) #t * #lbl #EQ destruct(EQ) #pre_t #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations …) [#_ *] ** #H1 #abs_top_cont #abs_tail_cont >EQcont_st11 in ⊢ (% → ?); inversion(cont … s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)] * #act_lab #i #cont_s1'' #_ #EQcont_s1' whd in ⊢ (??%% → ?); change with (check_continuations ?????) in match (foldr2 ???????); inversion(check_continuations ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] ** #H2 #abs_top_cont' #abs_tail_cont' #EQcheck normalize nodelta inversion(call_post_clean ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct *****] * #gen_labs #i' #EQi' inversion act_lab normalize nodelta [ #f #lab | * [| #lbl1 ]| * [| #nf_l] |] #EQ destruct(EQ) [1,6: whd in ⊢ (??%% → ?); #EQ destruct ***** |4,5: normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** [2: *] #EQ destruct ] whd in match ret_costed_abs; normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** #EQ destruct(EQ) ] inversion (memb ???) normalize nodelta #Hlbl1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** [ * ] #EQ destruct(EQ) #HH2 #EQ destruct #EQget_el >EQcode_st11 in ⊢ (% → ?); inversion(code … s1') [1,3,4,5,6,7: [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta [2: #l1 cases(?==?) normalize nodelta]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases lbl normalize nodelta [2,4: #l1 cases(memb ???) normalize nodelta [1,3: cases(?==?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #r_t' #EQcode_s1' whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQio_11 #EQ destruct cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs) [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety #pre_t' %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')} [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') // | ] % [ % [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} whd in match (get_costlabels_of_trace ????); whd in match (get_costlabels_of_trace ????) in ⊢ (???%); whd in match (map_labels_on_trace ??); >EQget_el @is_permutation_cons assumption | * [| #hd #tl] #i1 #EQcont_st3 >EQcont_st11 #EQ whd in EQ : (???%); [ EQk1 % | whd in ⊢ (??%%); @eq_f // ] ]] %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct | #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12 [1,2,3,4,5,6,7,9: [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 ] destruct * #z1 * #z2 #EQ destruct(EQ) whd in ⊢ (?% → ?); >x3 in ⊢ (% → ?); * | #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #_ #_ whd in ⊢ (?% → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta cases opt_l in EQcode11 EQcont12; normalize nodelta [ #x #y *] #lbl #EQcode11 #EQcont12 * #pre_tl #IH #st1' #abs_top #abs_tail whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1') [1,2,3,4,5,7: [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta [2: #l1 cases(?==?) normalize nodelta]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #f' #act_p' #opt_l' #i' #_ #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ) lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' #EQenv_it' ***** #EQtrans #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean; [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta [2: inversion(memb ???) normalize nodelta #Hlbl_keep [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'') #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) 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 ?)))) [2: whd >EQcont12 change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????); >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l' whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 EQ1 in no_dup; >foldr_map_append >foldr_map_append #no_dup lapply(no_duplicates_append_r … no_dup) #H1 lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1 change with ([?]@?) in match (?::?); #H1 lapply(no_duplicates_append_r … H1) >append_nil // ] ] #abs_top''' * #abs_tail''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety #pre_t' %{abs_top'''} %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) … t')} [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [ % [ % [2: whd in ⊢ (??%%); >EQlen %] %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%); >EQlab_env_it >associative_append whd in match (append ???); >associative_append >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%); whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons >append_nil whd in match (append ???) in ⊢ (???%); // | #k #i1 #EQcont_st3 #EQcont_st11 cases(stack_safety … (〈ret_act (Some ? lbl),i〉::k) … EQcont_st3 …) [2: >EQcont12 >EQcont_st11 % ] * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct %{tl1} % // whd in EQk1 : (??%%); destruct // ]] %4 // [2,4: % [2: % // |]] normalize >EQcode_st1' normalize nodelta % #EQ destruct | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] | whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] ] | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?; [1,2,3,4,5,6,7,9: [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 ] destruct #t1 #t2 #prf #_ #_ * #y1 * #y2 #EQ destruct(EQ) @⊥ >EQ in x12; * #H @H % ] #st11 #st12 #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #t1 #t2 #H inversion H in ⊢ ?; [1,2,3,4,5,6,7,8: [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21 ] destruct #_ #_ #_ #_ #_ #_ #_ whd in ⊢ (% → ?); #EQ destruct(EQ) @⊥ >EQ in x12; * #H @H % ] #st41 #st42 #r_t #mem1 #new_cont #opt_l1 #cd #EQcode41 #EQcont41 #EQ destruct(EQ) #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #st11_noio #st41_noio #_ whd in ⊢ (?(?%) → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta inversion(opt_l) in ⊢(% → ?); normalize nodelta [2: #lbl #_ * ] #EQopt_l destruct(EQopt_l) #_ #Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); * #EQcont11_42 >EQcode11 in ⊢ (% → ?); normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); #EQ destruct #IH1 #IH2 #st1' #abs_top #abs_tail whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1') [1,2,3,4,5,7: [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta [2: #l1 cases(?==?) normalize nodelta]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #f' #act_p' #opt_l' #i' #_ #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ) lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' #EQenv_it' ***** #EQtrans #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean; [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] destruct(EQopt_l') inversion(memb ???) normalize nodelta #Hlbl_keep' [ cases(?==?) normalize nodelta ] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct cases(IH1 (mk_state ? (f_body … env_it') (〈ret_act (Some ? lbl'),i'〉 :: (cont … st1')) (store ? st12) false) (abs_top''@abs_tail_cont) (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?)))) [2: whd >EQcont12 change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????); >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta whd in match ret_costed_abs; normalize nodelta >Hlbl_keep' normalize nodelta % // % // % // % [/5 by conj/] >EQcode12 EQ1 in no_dup; >foldr_map_append >foldr_map_append #no_dup lapply(no_duplicates_append_r … no_dup) #H1 lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1 change with ([?]@?) in match (?::?); #H1 lapply(no_duplicates_append_r … H1) >append_nil // ] ] #abs_top''' * #abs_tail''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety1 #pre_t1' whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ] ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?); whd in ⊢ (??%? → ?); inversion(cont … st41') normalize nodelta [ #_ #EQ destruct(EQ) ] * #act_lbl #i'' #cont_st42' #_ #EQcont_st41' change with (check_continuations ?????) in match (foldr2 ???????); inversion(check_continuations ?????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] ** #H3 #abs_top_cont'' #abs_tail_cont'' #EQ_contst42 >m_return_bind normalize nodelta inversion(call_post_clean ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct ***** ] * #abs_top'''' #i''' #EQ_clean_i'' inversion(act_lbl) normalize nodelta [1,3,4: [ #x1 #x2 #EQ whd in ⊢ (??%% → ?); #EQ1 destruct ***** | * [|#x1] #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct ****** [2: *] #EQ destruct | #EQ whd in ⊢ (??%% → ?); #EQ1 destruct ***** ] ] cut(act_lbl = ret_act (Some ? lbl') ∧ cont_st42' = cont … st1' ∧ i'' = i') [ cases(stack_safety1 [ ] …) [3: >EQcont41 in ⊢ (??%?); % |4: normalize // |5: % |2:] * [|#x #xs] * whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct > EQcont_st41' in EQ1; #EQ destruct(EQ) /3 by conj/ ] ** #EQ1 #EQ2 #EQ3 destruct #x #EQ destruct whd in match ret_costed_abs; normalize nodelta >Hlbl_keep' normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct ****** #_ #HH3 #EQ destruct(EQ) >EQcode41 in ⊢ (% → ?); inversion(code … st41') [1,3,4,5,6,7: [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta [2: #l1 cases(?==?) normalize nodelta]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases lbl normalize nodelta [2,4: #l1 cases(memb ???) normalize nodelta [1,3: cases(?==?) normalize nodelta ]]] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) ] ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_st41' #EQinfo_st41' #EQ destruct(EQ) >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?); #EQ destruct(EQ) >EQi' in EQ_clean_i''; #EQ destruct(EQ) cases(IH2 (mk_state ? i' (cont … st1') (store … st42) (io_info … st42)) abs_tail_cont abs_top'''') [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ] #abs_top_1 * #abs_tail_1 * #st5' * #t2' **** #Hst5_st5' #EQcosts' #EQlen' #stack_safety2 #pre_t2' %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))} [3: @hide_prf @(call … EQcode_st1' … EQenv_it') // |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') // |2,4: skip ] % [ % [ % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 // whd in ⊢ (??%%); @eq_f // ] %{Hst5_st5'} whd in match (map_labels_on_trace ??); change with (map_labels_on_trace ??) in match (foldr ?????); >map_labels_on_trace_append >get_cost_label_append whd in match (get_costlabels_of_trace ??? (t_ind …)); whd in match (get_costlabels_of_trace ??? (t_ind …)); >get_cost_label_append whd in match (get_costlabels_of_trace ??? (t_ind …)); >map_labels_on_trace_append >EQlab_env_it >EQgen_labels whd in match (map_labels_on_trace ? [ ]); whd in match (append ? (nil ?) ?); cut (∀A.∀l: list A. [ ] @ l = l) [//] #nil_append >nil_append >nil_append >nil_append @(permute_ok … EQcosts EQcosts') | #k #i #EQcont_st3 #EQ cases(stack_safety2 … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % // ]] %4 [ normalize >EQcode_st1' normalize nodelta % #EQ destruct | %{f} % // | whd in ⊢ (?%); >EQcode_st1' normalize nodelta @I | @append_premeasurable // %3 // [ whd in match (as_classify ??); >EQcode_st41' normalize nodelta % #EQ destruct | whd %{lbl'} % ] ] ] qed.