[3394] | 1 | (**************************************************************************) |
---|
| 2 | (* ___ *) |
---|
| 3 | (* ||M|| *) |
---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
---|
| 5 | (* ||T|| *) |
---|
| 6 | (* ||I|| Developers: *) |
---|
| 7 | (* ||T|| The HELM team. *) |
---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 9 | (* \ / *) |
---|
| 10 | (* \ / This file is distributed under the terms of the *) |
---|
| 11 | (* v GNU General Public License Version 2 *) |
---|
| 12 | (* *) |
---|
| 13 | (**************************************************************************) |
---|
| 14 | |
---|
| 15 | include "basics/types.ma". |
---|
| 16 | include "Traces.ma". |
---|
| 17 | include "basics/lists/list.ma". |
---|
| 18 | include "../src/utilities/option.ma". |
---|
[3396] | 19 | include "basics/jmeq.ma". |
---|
[3394] | 20 | |
---|
[3397] | 21 | discriminator option. |
---|
| 22 | |
---|
[3394] | 23 | record instr_params : Type[1] ≝ |
---|
| 24 | { seq_instr : DeqSet |
---|
| 25 | ; io_instr : DeqSet |
---|
| 26 | ; cond_instr : DeqSet |
---|
| 27 | ; loop_instr : DeqSet |
---|
| 28 | ; act_params_type : DeqSet |
---|
| 29 | ; return_type : DeqSet |
---|
| 30 | }. |
---|
| 31 | |
---|
| 32 | |
---|
| 33 | inductive Instructions (p : instr_params) : Type[0] ≝ |
---|
| 34 | | EMPTY : Instructions p |
---|
| 35 | | RETURN : return_type p → Instructions p |
---|
| 36 | | SEQ : (seq_instr p) → option NonFunctionalLabel → Instructions p → Instructions p |
---|
| 37 | | COND : (cond_instr p) → NonFunctionalLabel → Instructions p → |
---|
| 38 | NonFunctionalLabel → Instructions p → Instructions p → |
---|
| 39 | Instructions p |
---|
| 40 | | LOOP : (loop_instr p) → NonFunctionalLabel → Instructions p → |
---|
| 41 | NonFunctionalLabel → Instructions p → Instructions p |
---|
| 42 | | CALL : FunctionName → (act_params_type p) → option ReturnPostCostLabel → |
---|
| 43 | Instructions p → Instructions p |
---|
| 44 | | IO : NonFunctionalLabel → (io_instr p) → NonFunctionalLabel → Instructions p → |
---|
| 45 | Instructions p. |
---|
| 46 | |
---|
| 47 | let rec eq_instructions (p : instr_params) (i : Instructions p) |
---|
| 48 | on i : (Instructions p) → bool ≝ |
---|
| 49 | match i with |
---|
| 50 | [ EMPTY ⇒ λi'.match i' with [ EMPTY ⇒ true | _ ⇒ false ] |
---|
| 51 | | RETURN x ⇒ λi'.match i' with [ RETURN y ⇒ x == y | _ ⇒ false ] |
---|
| 52 | | SEQ x lab instr ⇒ λi'.match i' with |
---|
| 53 | [ SEQ y lab' instr' ⇒ x == y ∧ eq_instructions … instr instr' ∧ |
---|
| 54 | match lab with [ None ⇒ match lab' with [ None ⇒ true | _ ⇒ false ] |
---|
| 55 | | Some l1 ⇒ match lab' with [Some l2 ⇒ eq_nf_label l1 l2 | _ ⇒ false] |
---|
| 56 | ] |
---|
| 57 | | _ ⇒ false |
---|
| 58 | ] |
---|
| 59 | | COND x ltrue i1 lfalse i2 i3 ⇒ λi'.match i' with |
---|
| 60 | [ COND y ltrue' i1' lfalse' i2' i3' ⇒ |
---|
| 61 | x == y ∧ eq_nf_label ltrue ltrue' ∧ |
---|
| 62 | eq_instructions … i1 i1' ∧ eq_nf_label lfalse lfalse' ∧ |
---|
| 63 | eq_instructions … i2 i2' ∧ eq_instructions … i3 i3' |
---|
| 64 | | _ ⇒ false |
---|
| 65 | ] |
---|
| 66 | | LOOP x ltrue i1 lfalse i2 ⇒ λi'.match i' with |
---|
| 67 | [ LOOP y ltrue' i1' lfalse' i2' ⇒ x == y ∧ |
---|
| 68 | eq_instructions … i1 i1' ∧ eq_nf_label ltrue ltrue' ∧ |
---|
| 69 | eq_instructions … i2 i2' |
---|
| 70 | | _ ⇒ false |
---|
| 71 | ] |
---|
| 72 | | CALL f act_p r_lb i1 ⇒ λi'.match i' with |
---|
| 73 | [ CALL f' act_p' r_lb' i1' ⇒ eq_function_name f f' ∧ |
---|
| 74 | act_p == act_p' ∧ eq_instructions … i1 i1' ∧ |
---|
| 75 | match r_lb with [ None ⇒ match r_lb' with [None ⇒ true | _ ⇒ false] |
---|
| 76 | | Some z ⇒ match r_lb' with [Some w ⇒ eq_return_cost_lab z w | _ ⇒ false ] |
---|
| 77 | ] |
---|
| 78 | | _ ⇒ false |
---|
| 79 | ] |
---|
| 80 | | IO lin io lout i1 ⇒ λi'.match i' with |
---|
| 81 | [ IO lin' io' lout' i1' ⇒ eq_nf_label lin lin' ∧ io == io' ∧ |
---|
| 82 | eq_nf_label lout lout' ∧ eq_instructions … i1 i1' |
---|
| 83 | | _ ⇒ false |
---|
| 84 | ] |
---|
| 85 | ]. |
---|
| 86 | |
---|
[3401] | 87 | (* |
---|
[3394] | 88 | lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → |
---|
| 89 | (i1 ≠ i2 → P false) → P (eq_instructions p i1 i2). |
---|
[3396] | 90 | #P #p #i1 elim i1 |
---|
[3401] | 91 | [* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ |
---|
| 92 | lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') |
---|
| 93 | | #rt * normalize [2: #rt' cases (dec_eq … rt rt') #H [>(\b H) | >(\bf H) ] /2/ |
---|
| 94 | #_ #K @K % #abs lapply (eq_to_jmeq ??? abs) #abs' destruct(abs') @(absurd ?? H) //] |
---|
| 95 | [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ |
---|
| 96 | lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') |
---|
| 97 | | cases daemon (*TODO*) |
---|
[3394] | 98 | qed. |
---|
[3401] | 99 | *) |
---|
[3394] | 100 | |
---|
| 101 | record env_params : Type[1] ≝ |
---|
| 102 | { form_params_type : Type[0] |
---|
| 103 | }. |
---|
| 104 | |
---|
[3397] | 105 | record signature (p : env_params) (p' : instr_params) : Type[0] ≝ |
---|
[3394] | 106 | { f_name : FunctionName |
---|
| 107 | ; f_pars : form_params_type p |
---|
[3397] | 108 | ; f_ret : return_type p' |
---|
| 109 | }. |
---|
| 110 | |
---|
| 111 | record env_item (p : env_params) (p' : instr_params) : Type[0] ≝ |
---|
| 112 | { f_sig :> signature p p' |
---|
[3394] | 113 | ; f_lab : CallCostLabel |
---|
| 114 | ; f_body : Instructions p' |
---|
| 115 | }. |
---|
| 116 | |
---|
| 117 | record state_params : Type[1] ≝ |
---|
[3399] | 118 | { i_pars :> instr_params |
---|
| 119 | ; e_pars :> env_params |
---|
[3394] | 120 | ; store_type : DeqSet |
---|
| 121 | }. |
---|
| 122 | |
---|
| 123 | record state (p : state_params) : Type[0] ≝ |
---|
| 124 | { code : Instructions p |
---|
| 125 | ; cont : list (ActionLabel × (Instructions p)) |
---|
| 126 | ; store : store_type p |
---|
| 127 | ; io_info : bool |
---|
| 128 | }. |
---|
| 129 | |
---|
| 130 | definition is_io : ∀p.state p → Prop ≝ λp,st.io_info … st = true. |
---|
| 131 | |
---|
| 132 | record sem_state_params (p : state_params) : Type[0] ≝ |
---|
| 133 | { eval_seq : seq_instr p → state p → option (store_type p) |
---|
| 134 | ; eval_io : io_instr p → state p → option (store_type p) |
---|
| 135 | ; eval_cond_cond : cond_instr p → state p → option (bool × (store_type p)) |
---|
| 136 | ; eval_loop_cond : loop_instr p → state p → option (bool × (store_type p)) |
---|
[3399] | 137 | ; eval_call : signature p p → act_params_type p → store_type p → option (store_type p) |
---|
[3394] | 138 | ; eval_after_return : return_type p → store_type p → option (store_type p) |
---|
| 139 | ; init_store : store_type p |
---|
| 140 | }. |
---|
| 141 | |
---|
| 142 | |
---|
| 143 | let rec lookup (p : env_params) (p' : instr_params) (l : list (env_item p p')) |
---|
| 144 | on l : FunctionName → option (env_item p p') ≝ |
---|
| 145 | match l with |
---|
| 146 | [ nil ⇒ λ_.None ? |
---|
| 147 | | cons x xs ⇒ λf.if (eq_function_name f (f_name … x)) |
---|
| 148 | then Some ? x |
---|
| 149 | else lookup … xs f |
---|
| 150 | ]. |
---|
| 151 | |
---|
| 152 | definition is_ret_act : ActionLabel → Prop ≝ |
---|
| 153 | λa.match a with [ret_act _ ⇒ True | _ ⇒ False ]. |
---|
| 154 | |
---|
| 155 | inductive execute_l (p : state_params) (p' : sem_state_params p) (env : list (env_item p p)) : |
---|
| 156 | ActionLabel → relation (state p) ≝ |
---|
| 157 | | empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p)→ (cont ? st) = hd :: tl → |
---|
| 158 | (code ? st') = \snd hd → (cont … st') = tl → (store … st) = (store … st') → |
---|
| 159 | (io_info … st = true → is_non_silent_cost_act (\fst hd)) → (io_info … st') = false → ¬ is_ret_act (\fst hd) → execute_l … (\fst hd) st st' |
---|
| 160 | | seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd → |
---|
| 161 | eval_seq … p' i st = return s → (code ? st') = cd → |
---|
| 162 | (cont … st) = (cont … st') → (store … st') = s → |
---|
| 163 | io_info … st = false → io_info ? st' = false → execute_l … (cost_act opt_l) st st' |
---|
| 164 | | cond_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m. |
---|
| 165 | (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp st = return 〈true,new_m〉 → |
---|
| 166 | cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_true → store … st' = new_m → |
---|
| 167 | io_info … st = false → io_info … st' = false → execute_l … (cost_act (Some ? ltrue)) st st' |
---|
| 168 | | cond_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m. |
---|
| 169 | (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp st = return 〈false,new_m〉 → |
---|
| 170 | cont ? st' = 〈cost_act (None ?),cd〉 ::(cont … st) → code … st' = i_false → store … st' = new_m → |
---|
| 171 | io_info … st = false → io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st' |
---|
| 172 | | loop_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m. |
---|
| 173 | code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp st = return 〈true,new_m〉 → |
---|
| 174 | cont ? st' = 〈cost_act (None ?),LOOP … exp ltrue i_true lfalse i_false〉 :: (cont … st) → |
---|
| 175 | code … st' = i_true → store … st' = new_m → io_info … st = false → io_info … st' = false → |
---|
| 176 | execute_l … (cost_act (Some ? ltrue)) st st' |
---|
| 177 | | loop_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m. |
---|
| 178 | code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp st = return 〈false,new_m〉 → |
---|
| 179 | cont ? st' = cont … st → code … st' = i_false → store … st = store … st' → |
---|
| 180 | io_info … st = false → io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st' |
---|
| 181 | | io_in : ∀st,st',lin,io,lout,cd,mem.(code ? st) = IO … lin io lout cd → |
---|
| 182 | eval_io … p' io st = return mem → code ? st' = EMPTY p → |
---|
| 183 | cont … st' = 〈cost_act (Some ? lout),cd〉 :: (cont … st) → store … st' = mem → |
---|
| 184 | io_info … st' = true → execute_l … (cost_act (Some ? lin)) st st' |
---|
| 185 | | call : ∀st,st',f,act_p,r_lb,cd,mem,env_it.(code ? st) = CALL … f act_p r_lb cd → |
---|
| 186 | lookup … env f = return env_it → |
---|
[3399] | 187 | eval_call ? p' env_it act_p (store … st) = return mem → |
---|
[3394] | 188 | store ? st' = mem → code … st' = f_body … env_it → |
---|
| 189 | cont … st' = |
---|
[3396] | 190 | 〈(ret_act r_lb),cd〉 :: (cont … st) → |
---|
[3394] | 191 | io_info … st = false → (io_info … st') = false → |
---|
[3396] | 192 | execute_l … (call_act f (f_lab ?? env_it)) st st' |
---|
[3394] | 193 | | ret_instr : ∀st,st',r_t,mem,tl',rb,cd.code ? st = RETURN … r_t → |
---|
| 194 | cont … st = 〈ret_act rb,cd〉 :: tl' → cont ? st' = tl' → |
---|
| 195 | io_info … st = false → io_info ? st' = false → |
---|
| 196 | eval_after_return … p' r_t (store … st) = return mem → code … st' = cd → |
---|
| 197 | store … st' = mem → execute_l … (ret_act rb) st st'. |
---|
[3400] | 198 | |
---|
| 199 | let rec get_labels_of_code (p : instr_params) (i : Instructions p) on i : list CostLabel ≝ |
---|
| 200 | match i with |
---|
| 201 | [ EMPTY ⇒ [ ] |
---|
| 202 | | RETURN x ⇒ [ ] |
---|
| 203 | | SEQ x lab instr ⇒ let ih ≝ get_labels_of_code … instr in |
---|
| 204 | match lab with [ None ⇒ ih | Some lbl ⇒ a_non_functional_label lbl :: ih ] |
---|
| 205 | | COND x ltrue i1 lfalse i2 i3 ⇒ |
---|
| 206 | let ih3 ≝ get_labels_of_code … i3 in |
---|
| 207 | let ih2 ≝ get_labels_of_code … i2 in |
---|
| 208 | let ih1 ≝ get_labels_of_code … i1 in |
---|
| 209 | ltrue :: lfalse :: (ih1 @ ih2 @ih3) |
---|
| 210 | | LOOP x ltrue i1 lfalse i2 ⇒ |
---|
| 211 | let ih2 ≝ get_labels_of_code … i2 in |
---|
| 212 | let ih1 ≝ get_labels_of_code … i1 in |
---|
| 213 | a_non_functional_label ltrue :: a_non_functional_label lfalse :: (ih1 @ ih2) |
---|
| 214 | | CALL f act_p r_lb i1 ⇒ |
---|
| 215 | let ih1 ≝ get_labels_of_code … i1 in |
---|
| 216 | match r_lb with [ None ⇒ ih1 | Some lbl ⇒ a_return_post lbl :: ih1] |
---|
| 217 | | IO lin io lout i1 ⇒ |
---|
| 218 | let ih1 ≝ get_labels_of_code … i1 in |
---|
| 219 | a_non_functional_label lin :: a_non_functional_label lout :: ih1 |
---|
| 220 | ]. |
---|
[3394] | 221 | |
---|
[3400] | 222 | include "basics/lists/listb.ma". |
---|
| 223 | include "../src/utilities/hide.ma". |
---|
| 224 | |
---|
| 225 | let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ |
---|
| 226 | match l with |
---|
| 227 | [ nil ⇒ True |
---|
| 228 | | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs |
---|
| 229 | ]. |
---|
| 230 | |
---|
| 231 | lemma no_duplicates_append_r : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) → |
---|
| 232 | no_duplicates … l2. |
---|
| 233 | #A #l1 elim l1 // #x #xs normalize #IH #l2 * /2/ |
---|
| 234 | qed. |
---|
| 235 | |
---|
| 236 | lemma no_duplicates_append_l : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) → |
---|
| 237 | no_duplicates … l1. |
---|
| 238 | #A #l1 elim l1 // #x #xs normalize #IH #l2 * #H1 #H2 % [2: /2/ ] |
---|
| 239 | inversion(x ∈ xs @l2) in H1; normalize [ #_ * #H @⊥ @H %] #H1 #_ |
---|
| 240 | % inversion(x ∈ xs) normalize [2: //] #H3 #_ >(memb_append_l1 … H3) in H1; |
---|
| 241 | #EQ destruct(EQ) |
---|
| 242 | qed. |
---|
| 243 | |
---|
[3394] | 244 | record Program (p : env_params) (p' : instr_params) : Type[0] ≝ |
---|
| 245 | { env : list (env_item p p') |
---|
| 246 | ; main : Instructions p' |
---|
| 247 | }. |
---|
| 248 | |
---|
[3400] | 249 | |
---|
| 250 | definition no_duplicates_labels : ∀p,p'.Program p p' → Prop ≝ |
---|
| 251 | λp,p',prog. |
---|
| 252 | no_duplicates … |
---|
| 253 | (foldr … (λitem,acc.((a_call (f_lab … item)) :: get_labels_of_code … (f_body … item)) @ acc) (get_labels_of_code … (main … prog)) (env … prog)). |
---|
| 254 | |
---|
| 255 | lemma no_duplicates_domain_of_fun: |
---|
| 256 | ∀p,p',prog.no_duplicates_labels … prog → |
---|
| 257 | ∀f,env_it.lookup p p' (env … prog) f = return env_it → |
---|
| 258 | no_duplicates … (get_labels_of_code … (f_body … env_it)). |
---|
| 259 | #p #p' * #env elim env [ #main normalize #_ #f #env_it #EQ destruct(EQ)] |
---|
| 260 | #x #xs #IH #main whd in ⊢ (% → ?); whd in match (foldr ?????); #H #f #env_it |
---|
| 261 | whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta |
---|
| 262 | [ whd in ⊢ (? → ???% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) cases H #_ /2/ ] |
---|
| 263 | #H1 #EQenv_it @IH cases H /2/ |
---|
| 264 | qed. |
---|
| 265 | |
---|
| 266 | |
---|
[3394] | 267 | definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.True. |
---|
| 268 | (* bisognerebbe confrontare la coda dell'istruzione corrente e la parte di stack fino alla prima label. |
---|
| 269 | match (code … s1) with |
---|
| 270 | [ CALL f act_p r_lb i1 ⇒ code … s2 = i1 |
---|
| 271 | | _ ⇒ False |
---|
| 272 | ]. |
---|
| 273 | *) |
---|
| 274 | |
---|
| 275 | definition operational_semantics : ∀p : state_params.∀p'.Program p p → abstract_status ≝ |
---|
| 276 | λp,p',prog.mk_abstract_status |
---|
| 277 | (state p) |
---|
| 278 | (execute_l ? p' (env … prog)) |
---|
| 279 | (is_synt_succ …) |
---|
| 280 | (λs.match (code … s) with |
---|
| 281 | [ COND _ _ _ _ _ _ ⇒ cl_jump |
---|
| 282 | | LOOP _ _ _ _ _ ⇒ cl_jump |
---|
| 283 | | EMPTY ⇒ if io_info … s then cl_io else cl_other |
---|
| 284 | | _ ⇒ cl_other |
---|
| 285 | ]) |
---|
| 286 | (λs.match (code … s) with |
---|
| 287 | [CALL _ _ m _ ⇒ match m with [ Some _ ⇒ true | None ⇒ false ] |
---|
| 288 | | _ ⇒ false |
---|
| 289 | ]) |
---|
| 290 | (λs.eq_instructions … (code … s) (main … prog) ∧ isnilb … (cont … s) ∧ store … s == init_store … p' ∧ io_info … s) |
---|
| 291 | (λs.match (cont … s) with |
---|
| 292 | [ nil ⇒ match (code … s) with |
---|
| 293 | [ EMPTY ⇒ true |
---|
| 294 | | RETURN _ ⇒ true |
---|
| 295 | | _ ⇒ false |
---|
| 296 | ] |
---|
| 297 | | _ ⇒ false |
---|
| 298 | ]) |
---|
| 299 | ???. |
---|
| 300 | @hide_prf |
---|
| 301 | [ #s1 #s2 #l #H #H1 inversion H1 #st #st' |
---|
| 302 | [ #hd #tl |
---|
| 303 | | #i #cd #s #opt_l |
---|
| 304 | |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |
---|
| 305 | |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m |
---|
| 306 | | #lin #io #lout #cd #mem |
---|
| 307 | | #f #act_p #r_lb #cd #mem #env_it |
---|
| 308 | | #r_t #mem #tl #rb #cd |
---|
| 309 | ] |
---|
| 310 | #EQcode |
---|
| 311 | [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQ5 #H2 #EQ' #EQ6 #EQ7 |
---|
| 312 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
| 313 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
| 314 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
| 315 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
| 316 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
| 317 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 |
---|
| 318 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
| 319 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
| 320 | ] |
---|
| 321 | #_ destruct >EQcode in H; normalize nodelta /2 by ex_intro/ |
---|
| 322 | [ cases(io_info ??) normalize nodelta] #EQ destruct |
---|
| 323 | | #s1 #s2 #l #H #H1 inversion H1 #st #st' |
---|
| 324 | [ #hd #tl |
---|
| 325 | | #i #cd #s #opt_l |
---|
| 326 | |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |
---|
| 327 | |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m |
---|
| 328 | | #lin #io #lout #cd #mem |
---|
| 329 | | #f #act_p #r_lb #cd #mem #env_it |
---|
| 330 | | #r_t #mem #tl #rb #cd |
---|
| 331 | ] |
---|
| 332 | #EQcode |
---|
| 333 | [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7 |
---|
| 334 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 335 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 336 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 337 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 338 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 339 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost' #EQ6 #EQ7 #EQ8 |
---|
| 340 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQiost' #EQ8 #EQ9 #EQ10 |
---|
| 341 | | #EQ1 #EQ2 #EQ3 #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
| 342 | ] |
---|
| 343 | #_ destruct |
---|
| 344 | cases(code ? st') in H; normalize nodelta >EQiost' normalize nodelta |
---|
| 345 | #eq destruct try (#eq1 destruct) try (#eq2 destruct) try (#eq3 destruct) |
---|
| 346 | try (#eq4 destruct) try (#eq5 destruct) try (#eq6 destruct) %{lin} % |
---|
| 347 | | #s1 #s2 #l #H #H1 inversion H1 #st #st' |
---|
| 348 | [ #hd #tl |
---|
| 349 | | #i #cd #s #opt_l |
---|
| 350 | |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |
---|
| 351 | |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m |
---|
| 352 | | #lin #io #lout #cd #mem |
---|
| 353 | | #f #act_p #r_lb #cd #mem #env_it |
---|
| 354 | | #r_t #mem #tl #rb #cd |
---|
| 355 | ] |
---|
| 356 | #EQcode |
---|
| 357 | [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7 |
---|
| 358 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 359 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 360 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 361 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 362 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 363 | | #EQ1 #EQ2 #EQ3 #EQiost #EQiost' #EQ6 #EQ7 #EQ8 |
---|
| 364 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost #EQiost' #EQ8 #EQ9 #EQ10 |
---|
| 365 | | #EQ1 #EQ2 #EQiost #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
| 366 | ] |
---|
| 367 | #_ destruct >EQcode in H; normalize nodelta [|*: #EQ destruct] |
---|
| 368 | cases(io_info … st) in x; normalize nodelta [2: #_ #EQ destruct] |
---|
| 369 | #H3 #_ @H3 % |
---|
| 370 | ] |
---|
| 371 | qed. |
---|
| 372 | |
---|
| 373 | let rec eqb_list (D : DeqSet) (l1 : list D) on l1 : list D → bool ≝ |
---|
| 374 | match l1 with |
---|
| 375 | [ nil ⇒ λl2.match l2 with [nil ⇒ true | _ ⇒ false ] |
---|
| 376 | | cons x xs ⇒ λl2.match l2 with [ cons y ys ⇒ x == y ∧ eqb_list … xs ys | _ ⇒ false ] |
---|
| 377 | ]. |
---|
| 378 | |
---|
| 379 | definition DeqSet_List : DeqSet → DeqSet ≝ |
---|
| 380 | λX.mk_DeqSet (list X) (eqb_list …) ?. |
---|
| 381 | #x elim x [ * /2 by refl, conj/ #y #ys normalize % #EQ destruct] -x |
---|
| 382 | #x #xs #IH * [ normalize % #EQ destruct] #y #ys normalize % inversion(x == y) |
---|
| 383 | #EQ normalize nodelta |
---|
| 384 | [ #H >(proj1 … (IH ys) H) @eq_f2 [2: %] @(proj1 … (eqb_true …)) assumption |
---|
| 385 | | #EQ destruct |
---|
| 386 | | #EQ1 destruct @(proj2 … (IH …)) % |
---|
| 387 | | #EQ1 destruct <EQ @(proj2 … (eqb_true …)) % |
---|
| 388 | ] |
---|
| 389 | qed. |
---|
| 390 | |
---|
| 391 | unification hint 0 ≔ C; |
---|
| 392 | X ≟ DeqSet_List C |
---|
| 393 | (* ---------------------------------------- *) ⊢ |
---|
| 394 | list C ≡ carr X. |
---|
| 395 | |
---|
| 396 | |
---|
| 397 | unification hint 0 ≔ D,p1,p2; |
---|
| 398 | X ≟ DeqSet_List D |
---|
| 399 | (* ---------------------------------------- *) ⊢ |
---|
| 400 | eqb_list D p1 p2 ≡ eqb X p1 p2. |
---|
| 401 | |
---|
| 402 | definition associative_list : DeqSet → Type[0] → Type[0] ≝ |
---|
| 403 | λA,B.list (A × (list B)). |
---|
| 404 | |
---|
| 405 | let rec update_list (A : DeqSet) (B : Type[0]) (l : associative_list A B) |
---|
| 406 | on l : A → list B → associative_list A B ≝ |
---|
| 407 | λa,b.match l with |
---|
| 408 | [ nil ⇒ [〈a,b〉] |
---|
| 409 | | cons x xs ⇒ if (a == (\fst x)) then 〈a,b〉 :: xs |
---|
| 410 | else x :: (update_list … xs a b) |
---|
| 411 | ]. |
---|
| 412 | |
---|
| 413 | let rec get_element (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : A → list B ≝ |
---|
| 414 | λa.match l with [ nil ⇒ nil ? |
---|
| 415 | | cons x xs ⇒ if (a == \fst x) then \snd x else get_element … xs a |
---|
| 416 | ]. |
---|
[3401] | 417 | |
---|
| 418 | let rec domain_of_associative_list (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : list A ≝ |
---|
| 419 | match l with |
---|
| 420 | [ nil ⇒ [] |
---|
| 421 | | cons x xs ⇒ \fst x :: domain_of_associative_list … xs |
---|
| 422 | ]. |
---|
| 423 | |
---|
| 424 | lemma get_element_append_l: |
---|
| 425 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
| 426 | x ∈ domain_of_associative_list … l1 → |
---|
| 427 | get_element … (l1@l2) x = get_element … l1 x. |
---|
| 428 | #A #B #l1 elim l1 normalize [ #l2 #x * ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd)) |
---|
| 429 | #H [ >(\b H) | >(\bf H) ] normalize /2/ |
---|
| 430 | qed. |
---|
| 431 | |
---|
| 432 | lemma get_element_append_r: |
---|
| 433 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
| 434 | ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) → |
---|
| 435 | get_element ?? (l1@l2) x = get_element … l2 x. |
---|
| 436 | #A #B #l1 elim l1 normalize [ #l2 #x // ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd)) |
---|
| 437 | #H [ >(\b H) | >(\bf H) ] normalize /2 by/ * #K cases (K I) |
---|
| 438 | qed. |
---|
| 439 | |
---|
[3403] | 440 | lemma get_element_append_l1 : |
---|
| 441 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
| 442 | ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l2)) → |
---|
| 443 | get_element ?? (l1@l2) x = get_element … l1 x. |
---|
| 444 | #A #B #l1 elim l1 normalize [2: #x #xs #IH #l2 #a #H >IH // ] |
---|
| 445 | #l2 elim l2 // #y #ys #IH #a normalize cases(a == \fst y) normalize |
---|
| 446 | [ * #H @⊥ @H % ] #H @IH assumption |
---|
| 447 | qed. |
---|
[3407] | 448 | |
---|
| 449 | lemma get_element_append_r1 : |
---|
| 450 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
| 451 | ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) → |
---|
| 452 | get_element ?? (l1@l2) x = get_element … l2 x. |
---|
| 453 | #A #B #l1 elim l1 normalize // #x #xs #IH #l2 #a cases (?==?) |
---|
| 454 | normalize [* #H cases H //] #H >IH normalize // |
---|
| 455 | qed. |
---|
| 456 | |
---|
[3394] | 457 | definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝ |
---|
| 458 | λx.〈a_non_functional_label x,S x〉. |
---|
| 459 | |
---|
| 460 | definition fresh_cc_labe : ℕ → CallCostLabel × ℕ ≝ |
---|
| 461 | λx.〈a_call_label x,S x〉. |
---|
| 462 | |
---|
| 463 | definition fresh_rc_label : ℕ → ReturnPostCostLabel × ℕ ≝ |
---|
| 464 | λx.〈a_return_cost_label x,S x〉. |
---|
| 465 | |
---|
[3396] | 466 | record call_post_info (p : instr_params) : Type[0] ≝ |
---|
| 467 | { gen_labels : list CostLabel |
---|
| 468 | ; t_code : Instructions p |
---|
| 469 | ; fresh : ℕ |
---|
| 470 | ; lab_map : associative_list DEQCostLabel CostLabel |
---|
| 471 | ; lab_to_keep : list CostLabel |
---|
| 472 | }. |
---|
| 473 | |
---|
[3394] | 474 | let rec call_post_trans (p : instr_params) (i : Instructions p) (n : ℕ) on i : |
---|
[3396] | 475 | list CostLabel → call_post_info p ≝ |
---|
| 476 | λabs. |
---|
[3394] | 477 | match i with |
---|
[3396] | 478 | [ EMPTY ⇒ mk_call_post_info ? abs (EMPTY …) n (nil ?) (nil ?) |
---|
| 479 | | RETURN x ⇒ mk_call_post_info ? abs (RETURN … x) n (nil ?) (nil ?) |
---|
[3394] | 480 | | SEQ x lab instr ⇒ |
---|
[3396] | 481 | let ih ≝ call_post_trans … instr n abs in |
---|
[3394] | 482 | match lab with |
---|
[3396] | 483 | [ None ⇒ mk_call_post_info ? (gen_labels … ih) (SEQ … x (None ?) (t_code … ih)) |
---|
| 484 | (fresh … ih) (lab_map … ih) (lab_to_keep … ih) |
---|
| 485 | | Some lbl ⇒ |
---|
| 486 | mk_call_post_info ? (nil ?) (SEQ … x (Some ? lbl) (t_code … ih)) (fresh … ih) |
---|
| 487 | (〈a_non_functional_label lbl,(a_non_functional_label lbl :: (gen_labels … ih))〉 :: (lab_map … ih)) |
---|
| 488 | (lab_to_keep … ih) |
---|
[3394] | 489 | ] |
---|
| 490 | | COND x ltrue i1 lfalse i2 i3 ⇒ |
---|
[3396] | 491 | let ih3 ≝ call_post_trans … i3 n abs in |
---|
| 492 | let ih2 ≝ call_post_trans … i2 (fresh … ih3) (gen_labels … ih3) in |
---|
| 493 | let ih1 ≝ call_post_trans … i1 (fresh … ih2) (gen_labels … ih3) in |
---|
| 494 | mk_call_post_info ? (nil ?) (COND … x ltrue (t_code … ih1) lfalse (t_code … ih2) (t_code … ih3)) |
---|
| 495 | (fresh … ih1) |
---|
| 496 | (〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉:: |
---|
| 497 | 〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉:: |
---|
| 498 | ((lab_map … ih1) @ (lab_map … ih2) @ (lab_map … ih3))) |
---|
| 499 | ((lab_to_keep … ih1) @ (lab_to_keep … ih2) @ (lab_to_keep … ih3)) |
---|
[3394] | 500 | | LOOP x ltrue i1 lfalse i2 ⇒ |
---|
[3396] | 501 | let ih2 ≝ call_post_trans … i2 n abs in |
---|
| 502 | let ih1 ≝ call_post_trans … i1 (fresh … ih2) (nil ?) in |
---|
| 503 | mk_call_post_info ? (nil ?) (LOOP … x ltrue (t_code … ih1) lfalse (t_code … ih2)) (fresh … ih1) |
---|
| 504 | (〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉 :: |
---|
| 505 | 〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉 :: |
---|
| 506 | ((lab_map … ih1) @ (lab_map … ih2))) |
---|
| 507 | ((lab_to_keep … ih1) @ (lab_to_keep … ih2)) |
---|
[3394] | 508 | | CALL f act_p r_lb i1 ⇒ |
---|
[3396] | 509 | let ih ≝ call_post_trans … i1 n abs in |
---|
[3394] | 510 | match r_lb with |
---|
[3396] | 511 | [ None ⇒ let 〈l',f''〉 ≝ fresh_rc_label (fresh … ih) in |
---|
| 512 | mk_call_post_info ? ((a_return_post l')::(gen_labels … ih)) |
---|
| 513 | (CALL … f act_p (Some ? l') (t_code … ih)) f'' (lab_map … ih) (lab_to_keep … ih) |
---|
| 514 | | Some lbl ⇒ |
---|
| 515 | mk_call_post_info ? (nil ?) (CALL ? f act_p (Some ? lbl) (t_code … ih)) (fresh … ih) |
---|
| 516 | (〈a_return_post lbl,(a_return_post lbl :: (gen_labels … ih))〉 :: (lab_map … ih)) |
---|
| 517 | (a_return_post lbl :: lab_to_keep … ih) |
---|
[3394] | 518 | ] |
---|
| 519 | | IO lin io lout i1 ⇒ |
---|
[3396] | 520 | let ih ≝ call_post_trans … i1 n abs in |
---|
| 521 | mk_call_post_info ? (nil ?) (IO ? lin io lout (t_code … ih)) (fresh … ih) |
---|
| 522 | (〈a_non_functional_label lout,(a_non_functional_label lout :: (gen_labels … ih))〉 :: |
---|
| 523 | 〈a_non_functional_label lin,[a_non_functional_label lin]〉 :: (lab_map … ih)) (lab_to_keep … ih) |
---|
[3394] | 524 | ]. |
---|
| 525 | |
---|
[3396] | 526 | |
---|
| 527 | let rec call_post_clean (p : instr_params) (i : Instructions p) on i : |
---|
| 528 | associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → |
---|
| 529 | option ((list CostLabel) × (Instructions p)) ≝ |
---|
| 530 | λm,keep,abs. |
---|
| 531 | match i with |
---|
| 532 | [ EMPTY ⇒ Some ? 〈abs,EMPTY …〉 |
---|
| 533 | | RETURN x ⇒ Some ? 〈abs,RETURN … x〉 |
---|
| 534 | | SEQ x lab instr ⇒ |
---|
| 535 | ! 〈l,i1〉 ← call_post_clean … instr m keep abs; |
---|
| 536 | match lab with |
---|
| 537 | [ None ⇒ return 〈l,SEQ … x (None ?) i1〉 |
---|
| 538 | | Some lbl ⇒ if ((get_element … m lbl) == lbl :: l) |
---|
| 539 | then return 〈nil ?,SEQ … x (Some ? lbl) i1〉 |
---|
| 540 | else None ? |
---|
| 541 | ] |
---|
| 542 | | COND x ltrue i1 lfalse i2 i3 ⇒ |
---|
| 543 | ! 〈l3,instr3〉 ← call_post_clean … i3 m keep abs; |
---|
| 544 | ! 〈l2,instr2〉 ← call_post_clean … i2 m keep l3; |
---|
| 545 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep l3; |
---|
| 546 | if ((get_element … m ltrue) == ltrue :: l1) ∧ |
---|
| 547 | ((get_element … m lfalse) == lfalse :: l2) |
---|
| 548 | then return 〈nil ?,COND … x ltrue instr1 lfalse instr2 instr3〉 |
---|
| 549 | else None ? |
---|
| 550 | | LOOP x ltrue i1 lfalse i2 ⇒ |
---|
| 551 | ! 〈l2,instr2〉 ← call_post_clean … i2 m keep abs; |
---|
| 552 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep (nil ?); |
---|
| 553 | if ((get_element … m ltrue) == ltrue :: l1) ∧ |
---|
| 554 | ((get_element … m lfalse) == lfalse :: l2) |
---|
| 555 | then return 〈nil ?,LOOP … x ltrue instr1 lfalse instr2〉 |
---|
| 556 | else None ? |
---|
| 557 | | CALL f act_p r_lb i1 ⇒ |
---|
| 558 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs; |
---|
| 559 | match r_lb with |
---|
| 560 | [ None ⇒ return 〈l1,CALL … f act_p (None ?) instr1〉 |
---|
| 561 | | Some lbl ⇒ if ((a_return_post lbl ∈ keep)) |
---|
| 562 | then if ((get_element … m lbl) == lbl :: l1) |
---|
| 563 | then return 〈nil ?,CALL … f act_p (Some ? lbl) instr1〉 |
---|
| 564 | else None ? |
---|
| 565 | else return 〈(a_return_post lbl) :: l1,CALL … f act_p (None ?) instr1〉 |
---|
| 566 | ] |
---|
| 567 | | IO lin io lout i1 ⇒ |
---|
| 568 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs; |
---|
| 569 | if ((get_element … m lout) == lout :: l1) ∧ ((get_element … m lin) == [lin]) |
---|
| 570 | then return 〈nil ?,IO … lin io lout instr1〉 |
---|
| 571 | else None ? |
---|
| 572 | ]. |
---|
| 573 | |
---|
| 574 | let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (a : A) (l1 : list B) |
---|
| 575 | (l2 : list C) (f : A → B → C → A) on l1 : option A≝ |
---|
| 576 | match l1 with |
---|
| 577 | [ nil ⇒ match l2 with [ nil ⇒ return a | cons y ys ⇒ None ? ] |
---|
| 578 | | cons x xs ⇒ |
---|
| 579 | match l2 with |
---|
| 580 | [ nil ⇒ None ? |
---|
| 581 | | cons y ys ⇒ ! ih ← (foldr2 … a xs ys f); |
---|
| 582 | return f ih x y |
---|
| 583 | ] |
---|
| 584 | ]. |
---|
| 585 | |
---|
| 586 | definition is_silent_cost_act_b : ActionLabel → bool ≝ |
---|
| 587 | λact. match act with |
---|
| 588 | [ cost_act x ⇒ match x with [None ⇒ true | _ ⇒ false ] | _ ⇒ false]. |
---|
| 589 | |
---|
| 590 | definition eq_ActionLabel : ActionLabel → ActionLabel → bool ≝ |
---|
| 591 | λc1,c2. |
---|
| 592 | match c1 with |
---|
| 593 | [ call_act f l ⇒ match c2 with [ call_act f' l' ⇒ f == f' ∧ l == l' | _ ⇒ false] |
---|
| 594 | | ret_act x ⇒ match c2 with [ret_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false] |
---|
| 595 | | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false] |
---|
| 596 | ] |
---|
| 597 | | _ ⇒ false |
---|
| 598 | ] |
---|
| 599 | | cost_act x ⇒ match c2 with [cost_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false] |
---|
| 600 | | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false] |
---|
| 601 | ] |
---|
| 602 | | _ ⇒ false |
---|
| 603 | ] |
---|
| 604 | | init_act ⇒ match c2 with [init_act ⇒ true | _ ⇒ false] |
---|
| 605 | ]. |
---|
| 606 | |
---|
| 607 | definition ret_costed_abs : list CostLabel → option ReturnPostCostLabel → option CostLabel ≝ |
---|
| 608 | λkeep,x. |
---|
| 609 | match x with |
---|
| 610 | [ Some lbl ⇒ if (a_return_post lbl) ∈ keep then return (a_return_post lbl) |
---|
| 611 | else None ? |
---|
| 612 | | None ⇒ None ? |
---|
| 613 | ]. |
---|
| 614 | |
---|
[3399] | 615 | |
---|
[3396] | 616 | definition check_continuations : ∀p : instr_params. |
---|
| 617 | ∀l1,l2 : list (ActionLabel × (Instructions p)). |
---|
[3399] | 618 | associative_list DEQCostLabel CostLabel → |
---|
| 619 | list CostLabel → option (Prop × (list CostLabel) × (list CostLabel)) ≝ |
---|
| 620 | λp,cont1,cont2,m,keep. |
---|
| 621 | foldr2 ??? 〈True,nil ?,nil ?〉 cont1 cont2 |
---|
| 622 | (λx,y,z. |
---|
| 623 | let 〈cond,abs_top',abs_tail'〉 ≝ x in |
---|
| 624 | match call_post_clean p (\snd z) m keep abs_top' with |
---|
| 625 | [ None ⇒ 〈False,nil ?,nil ?〉 |
---|
| 626 | | Some w ⇒ |
---|
| 627 | match \fst z with |
---|
| 628 | [ ret_act opt_x ⇒ |
---|
| 629 | match ret_costed_abs keep opt_x with |
---|
| 630 | [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ |
---|
| 631 | get_element … m lbl = lbl :: (\fst w),(nil ?),abs_tail'〉 |
---|
| 632 | | None ⇒ |
---|
| 633 | 〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) @ abs_tail'〉 |
---|
| 634 | ] |
---|
| 635 | | cost_act opt_x ⇒ |
---|
| 636 | match opt_x with |
---|
| 637 | [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉 |
---|
| 638 | | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ |
---|
| 639 | get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉] |
---|
| 640 | | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). |
---|
| 641 | |
---|
| 642 | (* |
---|
| 643 | definition check_continuations : ∀p : instr_params. |
---|
| 644 | ∀l1,l2 : list (ActionLabel × (Instructions p)). |
---|
[3396] | 645 | associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → |
---|
[3398] | 646 | list (list CostLabel) → option (Prop × (list CostLabel) × (list (list CostLabel))) ≝ |
---|
| 647 | λp,cont1,cont2,m,keep,abs_top,abs_tail. |
---|
| 648 | foldr2 ??? 〈True,abs_top,abs_tail〉 cont1 cont2 |
---|
[3396] | 649 | (λx,y,z. |
---|
[3398] | 650 | let 〈cond,abs_top',abs_tail'〉 ≝ x in |
---|
| 651 | match call_post_clean p (\snd z) m keep abs_top' with |
---|
| 652 | [ None ⇒ 〈False,nil ?,nil ?〉 |
---|
[3396] | 653 | | Some w ⇒ |
---|
[3397] | 654 | match \fst z with |
---|
[3396] | 655 | [ ret_act opt_x ⇒ |
---|
| 656 | match ret_costed_abs keep opt_x with |
---|
[3398] | 657 | [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ |
---|
| 658 | get_element … m lbl = lbl :: (\fst w),(nil ?),(nil ?) :: abs_tail'〉 |
---|
[3396] | 659 | | None ⇒ |
---|
[3398] | 660 | 〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) :: abs_tail'〉 |
---|
[3396] | 661 | ] |
---|
| 662 | | cost_act opt_x ⇒ |
---|
| 663 | match opt_x with |
---|
[3398] | 664 | [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉 |
---|
| 665 | | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ |
---|
| 666 | get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉] |
---|
[3399] | 667 | | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). *) |
---|
[3398] | 668 | (* in input : |
---|
| 669 | abs_top is the list of labels to be propageted to the deepest level of the call stack |
---|
| 670 | abs_tail are the lists of labels to be propagated to the levels "below" the deepest level |
---|
| 671 | in output : |
---|
| 672 | abs_top is the list of labels to be propageted from the current level of the call stack |
---|
| 673 | abs_tail are the lists of labels to be propagated from the levels "below" the current level |
---|
| 674 | *) |
---|
| 675 | |
---|
[3396] | 676 | |
---|
| 677 | definition state_rel : ∀p. |
---|
[3399] | 678 | associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel →(list CostLabel) → |
---|
[3398] | 679 | relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2. |
---|
[3399] | 680 | match check_continuations ? (cont ? st1) (cont … st2) m keep with |
---|
[3398] | 681 | [ Some x ⇒ let 〈prf1,abs_top',abs_tail'〉 ≝ x in |
---|
| 682 | prf1 ∧ call_post_clean … (code … st2) m keep abs_top' = return 〈abs_top,(code … st1)〉 |
---|
| 683 | ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 ∧ abs_tail = abs_tail' |
---|
[3396] | 684 | | None ⇒ False |
---|
| 685 | ]. |
---|
| 686 | |
---|
| 687 | include "Simulation.ma". |
---|
| 688 | |
---|
| 689 | let rec len (S : abstract_status) (st1 : S) (st2 : S) (t : raw_trace S st1 st2) |
---|
| 690 | on t : ℕ ≝ |
---|
| 691 | match t with |
---|
| 692 | [ t_base s ⇒ O |
---|
| 693 | | t_ind s1 s2 s3 l prf lt ⇒ (len … lt) + 1 |
---|
| 694 | ]. |
---|
| 695 | (* |
---|
| 696 | lemma associative_max : ∀n1,n2,n3.max (max n1 n2) n3 = max n1 (max n2 n3). |
---|
| 697 | #n1 #n2 #n3 normalize @leb_elim normalize |
---|
| 698 | [ @leb_elim normalize |
---|
| 699 | [ #H1 #H2 @leb_elim normalize |
---|
| 700 | [ @leb_elim normalize // * #H @⊥ @H assumption |
---|
| 701 | | @leb_elim normalize |
---|
| 702 | [ #H3 * #H @⊥ @H @(transitive_le … H1) assumption |
---|
| 703 | | * #H @⊥ @H assumption |
---|
| 704 | ] |
---|
| 705 | ] |
---|
| 706 | | #H1 #H2 @leb_elim normalize |
---|
| 707 | [ @leb_elim normalize // #_ #H cases H1 #H1 @⊥ @H1 assumption |
---|
| 708 | | @leb_elim normalize |
---|
| 709 | [ #_ * #H @⊥ @H assumption |
---|
| 710 | | * #H @⊥ @H @(transitive_le … H2) |
---|
| 711 | *) |
---|
| 712 | let rec compute_max_n (p : instr_params) (i : Instructions p) on i : ℕ ≝ |
---|
| 713 | match i with |
---|
| 714 | [ EMPTY ⇒ O |
---|
| 715 | | RETURN x ⇒ O |
---|
| 716 | | SEQ x lab instr ⇒ let n ≝ compute_max_n … instr in |
---|
| 717 | match lab with |
---|
| 718 | [ None ⇒ n |
---|
| 719 | | Some l ⇒ |
---|
| 720 | match l with |
---|
| 721 | [ a_non_functional_label n' ⇒ S (max n n') ] |
---|
| 722 | ] |
---|
| 723 | | COND x ltrue i1 lfalse i2 i3 ⇒ |
---|
| 724 | let n1 ≝ compute_max_n … i1 in |
---|
| 725 | let n2 ≝ compute_max_n … i2 in |
---|
| 726 | let n3 ≝ compute_max_n … i3 in |
---|
| 727 | let mx ≝ max (max n1 n2) n3 in |
---|
| 728 | match ltrue with |
---|
| 729 | [ a_non_functional_label lt ⇒ |
---|
| 730 | match lfalse with |
---|
| 731 | [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ] |
---|
| 732 | | LOOP x ltrue i1 lfalse i2 ⇒ |
---|
| 733 | let n1 ≝ compute_max_n … i1 in |
---|
| 734 | let n2 ≝ compute_max_n … i2 in |
---|
| 735 | let mx ≝ max n1 n2 in |
---|
| 736 | match ltrue with |
---|
| 737 | [ a_non_functional_label lt ⇒ |
---|
| 738 | match lfalse with |
---|
| 739 | [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ] |
---|
| 740 | | CALL f act_p r_lb i1 ⇒ |
---|
| 741 | let n ≝ compute_max_n … i1 in |
---|
| 742 | match r_lb with |
---|
| 743 | [ None ⇒ n |
---|
| 744 | | Some lbl ⇒ match lbl with [a_return_cost_label l ⇒ S(max l n) ] |
---|
| 745 | ] |
---|
| 746 | | IO lin io lout i1 ⇒ |
---|
| 747 | let n ≝ compute_max_n … i1 in |
---|
| 748 | match lin with |
---|
| 749 | [a_non_functional_label l1 ⇒ |
---|
| 750 | match lout with |
---|
| 751 | [a_non_functional_label l2 ⇒ S(max (max n l1) l2) ] ] |
---|
| 752 | ]. |
---|
| 753 | |
---|
| 754 | |
---|
[3400] | 755 | definition same_fresh_map_on : list CostLabel → |
---|
| 756 | relation (associative_list DEQCostLabel CostLabel) ≝ |
---|
| 757 | λdom,m1,m2.∀x.bool_to_Prop (x ∈ dom) → get_element … m1 x = get_element … m2 x. |
---|
| 758 | |
---|
| 759 | definition same_to_keep_on : list CostLabel → relation (list CostLabel) ≝ |
---|
| 760 | λdom,keep1,keep2.∀x. bool_to_Prop (x ∈ dom) → (x ∈ keep1) = (x ∈ keep2). |
---|
| 761 | |
---|
| 762 | lemma memb_not_append : ∀D : DeqSet.∀l1,l2 : list D.∀x : D. |
---|
| 763 | x ∈ l1 = false → x ∈ l2 = false → x ∈ (l1 @ l2) = false. |
---|
| 764 | #D #l1 elim l1 |
---|
| 765 | [ #l2 #x #_ #H @H ] |
---|
| 766 | #x #xs #IH #l2 #x1 whd in match (memb ???); inversion (x1 == x) normalize nodelta |
---|
| 767 | [ #_ #EQ destruct] #EQx1 #EQxs #EQl2 whd in match (memb ???); >EQx1 |
---|
| 768 | normalize nodelta @IH // |
---|
| 769 | qed. |
---|
| 770 | |
---|
[3403] | 771 | lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A . |
---|
| 772 | no_duplicates … (l1 @ l2) → x ∈ l1 → x ∈ l2 → False. |
---|
| 773 | #A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???); |
---|
| 774 | inversion (x == x1) normalize nodelta |
---|
| 775 | [ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H % |
---|
| 776 | | #_ @IH // |
---|
| 777 | ] |
---|
| 778 | qed. |
---|
| 779 | |
---|
| 780 | |
---|
| 781 | lemma same_to_keep_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l. |
---|
| 782 | no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → x ∈ dom1) → |
---|
| 783 | (∀x.x ∈ l3 → x ∈ dom3) → |
---|
| 784 | same_to_keep_on (dom1@dom2@dom3) (l1@l2@l3) l → |
---|
| 785 | same_to_keep_on dom2 l2 l. |
---|
| 786 | #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #sub_set1 #sub_set3 #H2 |
---|
| 787 | #x #Hx inversion (x ∈ l2) |
---|
| 788 | [ #EQkeep <H2 [> memb_append_l2 // >memb_append_l1 // ] |
---|
| 789 | >memb_append_l2 // >memb_append_l1 // >Hx // |
---|
| 790 | | #EQno_keep <H2 |
---|
| 791 | [2: >memb_append_l2 // >memb_append_l1 // >Hx // |
---|
| 792 | | @sym_eq @memb_not_append [2: @memb_not_append //] |
---|
| 793 | [ <associative_append in no_dup; #no_dup ] |
---|
| 794 | lapply(memb_no_duplicates_append … x … no_dup) #H |
---|
| 795 | inversion(memb ???) // #H1 cases H |
---|
| 796 | [1,4: [>memb_append_l2 | >memb_append_l1] // >Hx // |
---|
| 797 | | @sub_set3 >H1 // |
---|
| 798 | | @sub_set1 >H1 // |
---|
| 799 | ] |
---|
| 800 | ] |
---|
| 801 | ] |
---|
| 802 | qed. |
---|
| 803 | |
---|
| 804 | lemma same_fresh_map_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l. |
---|
| 805 | no_duplicates … (dom1 @dom2 @ dom3) → (∀x.x ∈ domain_of_associative_list … l1 → x ∈ dom1) → |
---|
| 806 | (∀x.x ∈ domain_of_associative_list … l3 → x ∈ dom3) → |
---|
| 807 | same_fresh_map_on … (dom1 @dom2 @dom3) (l1 @l2 @ l3) l → |
---|
| 808 | same_fresh_map_on … dom2 l2 l. |
---|
| 809 | #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #subset1 #subset3 whd in ⊢ (% → ?); #H1 |
---|
| 810 | whd #x #Hx <H1 |
---|
| 811 | [2: >memb_append_l2 // >memb_append_l1 // >Hx //] |
---|
| 812 | >get_element_append_r [ >get_element_append_l1 // ] % #K |
---|
| 813 | [ lapply(subset3 … K) | lapply(subset1 … K) ] #ABS |
---|
| 814 | [ <associative_append in no_dup; #no_dup] @(memb_no_duplicates_append … x … no_dup) |
---|
| 815 | // [>memb_append_l2 | >memb_append_l1 ] // >Hx // |
---|
| 816 | qed. |
---|
| 817 | |
---|
| 818 | |
---|
[3400] | 819 | lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p. |
---|
| 820 | ∀x,n,l. |
---|
| 821 | x ∈ lab_to_keep … (call_post_trans … i n l) → x ∈ get_labels_of_code … i. |
---|
| 822 | #p #i elim i // |
---|
| 823 | [ #seq #opt_l #instr #IH #x #n #l whd in match (call_post_trans ????); |
---|
| 824 | cases opt_l -opt_l normalize nodelta [|#lbl] |
---|
| 825 | whd in match (get_labels_of_code ??); #H [2: @orb_Prop_r] /2/ |
---|
| 826 | | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l |
---|
| 827 | whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); |
---|
| 828 | #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r |
---|
| 829 | [ >memb_append_l1 // @IH1 [3: >H // |*: ] |
---|
| 830 | | >memb_append_l2 // cases(memb_append … H) -H #H |
---|
| 831 | [>memb_append_l1 // @IH2 [3: >H // |*: ] |
---|
| 832 | | >memb_append_l2 // @IH3 [3: >H // |*: ] |
---|
| 833 | ] |
---|
| 834 | ] |
---|
| 835 | | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l |
---|
| 836 | whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); |
---|
| 837 | #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r |
---|
| 838 | [ >memb_append_l1 | >memb_append_l2 ] // [ @IH1 | @IH2 ] [3,6: >H |*: ] // |
---|
| 839 | | #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????); |
---|
| 840 | whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); |
---|
| 841 | inversion(x == lbl) #Hlbl normalize nodelta |
---|
| 842 | [* >(\P Hlbl) @orb_Prop_l @eq_costlabel_elim // * #H @H % |
---|
| 843 | | #H @orb_Prop_r @IH // |
---|
| 844 | ] |
---|
| 845 | | #lin #io #lout #i1 #IH #x #n #l whd in match (call_post_trans ????); |
---|
| 846 | whd in match (get_labels_of_code ??); #H @orb_Prop_r @orb_Prop_r @IH // |
---|
| 847 | ] |
---|
| 848 | qed. |
---|
[3401] | 849 | |
---|
[3402] | 850 | lemma domain_of_associative_list_append : ∀A,B.∀l1,l2 : associative_list A B. |
---|
| 851 | domain_of_associative_list ?? (l1 @ l2) = |
---|
| 852 | (domain_of_associative_list ?? l1) @ (domain_of_associative_list ?? l2). |
---|
| 853 | #A #B #l1 elim l1 // #x #xs #IH #l2 normalize // |
---|
| 854 | qed. |
---|
| 855 | |
---|
[3401] | 856 | lemma lab_map_in_domain: ∀p.∀i: Instructions p. |
---|
| 857 | ∀x,n,l. |
---|
| 858 | x ∈ domain_of_associative_list … (lab_map p (call_post_trans … i n l)) → |
---|
| 859 | x ∈ get_labels_of_code … i. |
---|
[3402] | 860 | #p #i elim i // |
---|
| 861 | [ #seq * [|#lbl] #i1 #IH #x #n #l whd in match(call_post_trans ????); |
---|
| 862 | whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); |
---|
| 863 | inversion(x==lbl) #Hlbl normalize nodelta [#_ whd in match (memb ???); >Hlbl % ] |
---|
| 864 | #H >memb_cons // @IH // |
---|
| 865 | | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l |
---|
| 866 | whd in match (call_post_trans ????); whd in match (memb ???); |
---|
| 867 | whd in match (get_labels_of_code ??); inversion(x == ltrue) #Hlbl normalize nodelta |
---|
| 868 | [ #_ whd in match (memb ???); >Hlbl % ] whd in match (memb ???); |
---|
| 869 | inversion(x == lfalse) #Hlbl1 normalize nodelta |
---|
| 870 | [ #_ whd in match (memb ???); >Hlbl normalize nodelta whd in match (memb ???); |
---|
| 871 | >Hlbl1 % ] #H >memb_cons // >memb_cons // >domain_of_associative_list_append in H; |
---|
| 872 | #H cases(memb_append … H) [ #H1 >memb_append_l1 // @IH1 [3: >H1 // |*:] ] |
---|
| 873 | >domain_of_associative_list_append #H1 cases(memb_append … H1) |
---|
| 874 | #H2 >memb_append_l2 // [ >memb_append_l1 | >memb_append_l2 ] // |
---|
| 875 | [ @IH2 | @IH3] /2 by eq_true_to_b/ |
---|
| 876 | | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l whd in match (call_post_trans ????); |
---|
| 877 | whd in match (get_labels_of_code ??); whd in match (memb ???); inversion(x == lfalse) |
---|
| 878 | #Hlfalse normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlfalse // ] |
---|
| 879 | whd in match (memb ???); inversion(x==ltrue) normalize nodelta #Hltrue |
---|
| 880 | [ #_ whd in match (memb ???); >Hltrue %] >domain_of_associative_list_append #H |
---|
| 881 | cases(memb_append … H) #H1 >memb_cons // >memb_cons // [ >memb_append_l1 | >memb_append_l2 ] |
---|
| 882 | // [ @IH1 | @IH2] /2/ |
---|
| 883 | | #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????); |
---|
| 884 | whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); inversion (x == lbl) |
---|
| 885 | #Hlbl normalize nodelta [ #_ whd in match (memb ???); >Hlbl % ] #H >memb_cons // @IH /2/ |
---|
| 886 | | #lin #io #lout #i1 #IH #x #n #l whd in match (memb ???); inversion(x == lout) #Hlout |
---|
| 887 | normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlout % ] |
---|
| 888 | whd in match (memb ???); inversion(x==lin) #Hlin normalize nodelta |
---|
| 889 | [ #_ whd in match (memb ???); >Hlin % ] #H >memb_cons // >memb_cons // @IH /2/ |
---|
| 890 | ] |
---|
[3401] | 891 | qed. |
---|
| 892 | |
---|
[3406] | 893 | lemma eq_a_non_functional_label : |
---|
| 894 | ∀c1,c2.c1 == c2 → a_non_functional_label c1 == a_non_functional_label c2. |
---|
| 895 | #c1 #c2 #EQ cases(eqb_true DEQNonFunctionalLabel c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ |
---|
| 896 | #EQ destruct >(\b (refl …)) @I |
---|
| 897 | qed. |
---|
[3400] | 898 | |
---|
| 899 | lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ. |
---|
| 900 | let dom ≝ get_labels_of_code … i1 in |
---|
| 901 | no_duplicates … dom → |
---|
[3399] | 902 | ∀m,keep. |
---|
[3396] | 903 | ∀info,l.call_post_trans p i1 n l = info → |
---|
[3400] | 904 | same_fresh_map_on dom (lab_map … info) m → |
---|
| 905 | same_to_keep_on dom (lab_to_keep … info) keep → |
---|
[3399] | 906 | call_post_clean … (t_code … info) m keep l |
---|
[3396] | 907 | = return 〈gen_labels … info,i1〉. |
---|
[3400] | 908 | #p #i1 elim i1 |
---|
| 909 | [ #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); |
---|
| 910 | #EQ destruct(EQ) // |
---|
| 911 | | #x #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); |
---|
| 912 | #EQ destruct(EQ) // |
---|
| 913 | | #seq * [|#lbl] #instr #IH #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep |
---|
| 914 | #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%%); normalize nodelta |
---|
| 915 | >IH // |
---|
| 916 | [1,4: whd whd in H2; #x #Hx @H2 whd in match (get_labels_of_code ??); // |
---|
| 917 | @orb_Prop_r // |
---|
| 918 | |2,5: whd whd in H1; #x #Hx [ @H1 // ] cases no_dup #H3 #_ <H1 |
---|
| 919 | [2: whd in match (get_labels_of_code ??); @orb_Prop_r // ] |
---|
| 920 | whd in ⊢ (???%); cases(eqb_true … x lbl) inversion(x == lbl) normalize nodelta |
---|
| 921 | [2: //] #_ #H4 >H4 in Hx; // #H5 >H5 in H3; * #ABS @⊥ @ABS % |
---|
| 922 | |6: cases no_dup // |
---|
| 923 | ] |
---|
| 924 | normalize nodelta <(H1 lbl) |
---|
| 925 | [2: whd in match (get_labels_of_code ??); @orb_Prop_l cases(eqb_true … (a_non_functional_label lbl) lbl) |
---|
| 926 | #H3 #H4 >H4 % ] |
---|
| 927 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
| 928 | >(\b (refl …)) % |
---|
| 929 | | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #n normalize nodelta |
---|
| 930 | #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); |
---|
| 931 | #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%?); >IH3 // |
---|
[3403] | 932 | [2: whd in match (get_labels_of_code ??) in H2; |
---|
| 933 | change with ([?;?]@?) in match (?::?) in H2; |
---|
| 934 | <associative_append in H2; <associative_append |
---|
| 935 | <(append_nil … (?@?)) <associative_append in ⊢ (??%? → ?); |
---|
| 936 | <(append_nil … (?@?)) in ⊢ (??%? → ?); >associative_append |
---|
| 937 | >associative_append in ⊢ (??%? → ?); #H2 |
---|
| 938 | @(same_to_keep_on_append … H2) // [ >append_nil |
---|
| 939 | whd in ⊢ (??%); whd in no_dup:(??%); >associative_append // ] |
---|
| 940 | #x #Hx cases (memb_append … Hx) -Hx #Hx @orb_Prop_r @orb_Prop_r |
---|
| 941 | [ >memb_append_l1 | >memb_append_l2 ] // |
---|
| 942 | @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |
---|
| 943 | |3: -H2 whd in match (get_labels_of_code ??) in H1; |
---|
| 944 | change with ([?;?]@?) in match (?::?) in H1; |
---|
| 945 | <associative_append in H1; <associative_append |
---|
| 946 | <(append_nil … (?@?)) >associative_append |
---|
| 947 | change with ([?;?]@?) in match (?::?::?) in ⊢ (??%? → ?); |
---|
| 948 | <associative_append in ⊢ (??%? → ?); |
---|
| 949 | <associative_append in ⊢ (??%? → ?); |
---|
| 950 | <(append_nil … (?@?)) in ⊢ (??%? → ?); |
---|
| 951 | >associative_append in ⊢ (??%? → ?); #H1 |
---|
| 952 | @(same_fresh_map_on_append … H1) // |
---|
| 953 | [ >append_nil >associative_append // ] |
---|
| 954 | #x whd in match (memb ???); inversion(x == ltrue) |
---|
| 955 | [ #Hltrue normalize nodelta #_ whd in match (memb ???); >Hltrue % |
---|
| 956 | | #Hltrue normalize nodelta whd in match (memb ???); inversion(x == lfalse) |
---|
| 957 | [ #Hlfalse #_ @orb_Prop_r @orb_Prop_l >Hlfalse % |
---|
| 958 | | #Hlfalse normalize nodelta #Hx @orb_Prop_r @orb_Prop_r |
---|
| 959 | >domain_of_associative_list_append in Hx; #H |
---|
| 960 | cases(memb_append … H) #H2 [ >memb_append_l1 | >memb_append_l2 ] |
---|
| 961 | // @(lab_map_in_domain … (eq_true_to_b … H2)) |
---|
[3400] | 962 | ] |
---|
[3403] | 963 | ] |
---|
[3400] | 964 | |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |] |
---|
| 965 | ] |
---|
| 966 | normalize nodelta >IH2 // |
---|
[3403] | 967 | [2: whd in match (get_labels_of_code ??) in H2; |
---|
| 968 | change with ([?;?]@?) in match (?::?) in H2; |
---|
| 969 | <associative_append in H2; #H2 |
---|
| 970 | @(same_to_keep_on_append … H2) // #x #Hx [ @orb_Prop_r @orb_Prop_r ] |
---|
| 971 | @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |
---|
| 972 | |3: whd in match (get_labels_of_code ??) in H1; |
---|
| 973 | change with ([?;?]@?) in match (?::?) in H1; |
---|
| 974 | change with ([?;?]@?) in match (?::?::?) in H1 : (??%?); |
---|
| 975 | <associative_append in H1; <associative_append in ⊢ (??%? → ?); #H1 |
---|
| 976 | @(same_fresh_map_on_append … H1) // [2: /2 by lab_map_in_domain/ ] |
---|
| 977 | #x >domain_of_associative_list_append #H cases(memb_append … H) |
---|
| 978 | [ whd in ⊢ (??%? → ?%); cases(x == ltrue) // normalize nodelta |
---|
| 979 | whd in ⊢ (??%? → ?%); cases(x == lfalse) // normalize nodelta |
---|
| 980 | normalize #EQ destruct |
---|
| 981 | | #H1 @orb_Prop_r @orb_Prop_r |
---|
| 982 | @(lab_map_in_domain … (eq_true_to_b … H1)) |
---|
| 983 | ] |
---|
[3401] | 984 | |4: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l |
---|
[3400] | 985 | ] |
---|
| 986 | >m_return_bind >IH1 // |
---|
[3403] | 987 | [2: whd in match (get_labels_of_code ??) in H2; |
---|
| 988 | change with ([?;?]@?) in match (?::?) in H2; |
---|
| 989 | change with ([ ] @ ?) in match (lab_to_keep ??) in H2; |
---|
| 990 | >associative_append in H2 : (??%?); #H2 |
---|
| 991 | @(same_to_keep_on_append … H2) // [ #x *] #x #Hx cases(memb_append … Hx) |
---|
| 992 | -Hx #Hx [ >memb_append_l1 | >memb_append_l2] // |
---|
| 993 | @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |
---|
| 994 | |3: whd in match (get_labels_of_code ??) in H1; |
---|
| 995 | change with ([?;?]@?) in match (?::?) in H1; |
---|
| 996 | change with ([?;?]@?) in match (?::?::?) in H1 : (??%?); |
---|
| 997 | @(same_fresh_map_on_append … H1) // #x >domain_of_associative_list_append |
---|
| 998 | #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2 ] |
---|
| 999 | // @(lab_map_in_domain … (eq_true_to_b … Hx)) |
---|
[3401] | 1000 | |4: cases no_dup #_ * #_ @no_duplicates_append_l |
---|
| 1001 | ] |
---|
[3400] | 1002 | >m_return_bind normalize nodelta whd in H1; <H1 |
---|
| 1003 | [2: whd in match (get_labels_of_code ??); whd in match (memb ???); |
---|
| 1004 | >(\b (refl …)) % ] whd in match (get_element ????); >(\b (refl …)) |
---|
| 1005 | normalize nodelta >(\b (refl …)) <H1 |
---|
| 1006 | [2: whd in match (get_labels_of_code ??); >memb_cons // |
---|
| 1007 | whd in match (memb ???); >(\b (refl …)) % ] |
---|
| 1008 | whd in match (get_element ????); @eq_costlabel_elim normalize nodelta |
---|
[3404] | 1009 | [ #ABS @⊥ cases no_dup >ABS * #H #_ @H @orb_Prop_l |
---|
| 1010 | >(\b (refl ? (a_non_functional_label ltrue))) % ] #_ |
---|
| 1011 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
| 1012 | >(\b (refl …)) % |
---|
[3406] | 1013 | | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?); |
---|
| 1014 | #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on |
---|
| 1015 | whd in ⊢ (??%?); >IH2 |
---|
| 1016 | [ normalize nodelta >IH1 |
---|
| 1017 | [ >m_return_bind <fresh_map [2: @orb_Prop_l >(\b (refl …)) % ] |
---|
| 1018 | whd in match (get_element ????); |
---|
| 1019 | inversion(a_non_functional_label ltrue == a_non_functional_label lfalse) |
---|
| 1020 | #Hltrue normalize nodelta |
---|
| 1021 | [ cases no_dup whd in match (memb ???); |
---|
| 1022 | cases(eqb_true … (a_non_functional_label ltrue) (a_non_functional_label lfalse)) |
---|
| 1023 | #H1 #_ lapply(H1 Hltrue) #EQ destruct(EQ) >(\b (refl …)) * #ABS @⊥ @ABS % ] |
---|
| 1024 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …)) |
---|
| 1025 | <fresh_map [2: @orb_Prop_r @orb_Prop_l >(\b (refl …)) % ] |
---|
| 1026 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
| 1027 | >(\b (refl …)) % |
---|
| 1028 | | change with ([?;?]@?@?) in keep_on : (?%??); change with ((nil ?) @ ? @ ?) in keep_on : (??%?); |
---|
| 1029 | @(same_to_keep_on_append … keep_on) // [ #x * | #x /2 by lab_to_keep_in_domain/ ] |
---|
| 1030 | | change with ([?;?]@?@?) in fresh_map : (?%%?); @(same_fresh_map_on_append … fresh_map) |
---|
| 1031 | /2 by lab_map_in_domain/ #x whd in match (memb ???); inversion(x==lfalse) #Hlfalse |
---|
| 1032 | normalize nodelta |
---|
| 1033 | [ #_ @orb_Prop_r whd in match (memb ???); >Hlfalse % |
---|
| 1034 | | whd in match (memb ???); inversion(x==ltrue) #Hltrue normalize nodelta [2: *] #_ |
---|
| 1035 | @orb_Prop_l >Hltrue % |
---|
| 1036 | ] |
---|
| 1037 | | % |
---|
| 1038 | | cases no_dup #_ * #_ /2/ |
---|
| 1039 | | |
---|
| 1040 | ] |
---|
| 1041 | | change with ([?;?]@?@?) in keep_on : (?%??); <associative_append in keep_on; |
---|
| 1042 | <(append_nil … (?@?)) <(append_nil … (?@?)) in ⊢ (??%? → ?); |
---|
[3408] | 1043 | >associative_append in ⊢ (?%%? → ?); >associative_append in ⊢ (??%? → ?); |
---|
| 1044 | #keep_on @(same_to_keep_on_append … keep_on) // |
---|
| 1045 | [ >associative_append >append_nil // |
---|
| 1046 | | #x #Hx @orb_Prop_r @orb_Prop_r /2 by lab_to_keep_in_domain/ |
---|
| 1047 | ] |
---|
| 1048 | | change with ([?;?]@?@?) in fresh_map : (?%??); <associative_append in fresh_map; |
---|
| 1049 | <(append_nil … (?@?)) change with ([?;?]@?@?) in ⊢ (??%? → ?); |
---|
| 1050 | <associative_append in ⊢ (??%? → ?); <(append_nil … (?@?)) in ⊢ (??%? → ?); |
---|
| 1051 | >associative_append in ⊢ (?%%? → ?); >associative_append in ⊢ (??%? → ?); |
---|
| 1052 | #fresh_map @(same_fresh_map_on_append … fresh_map) // |
---|
| 1053 | [ >append_nil // |
---|
| 1054 | | #x >domain_of_associative_list_append #Hx cases(memb_append … Hx) |
---|
| 1055 | [2: #Hx1 @orb_Prop_r @orb_Prop_r @(lab_map_in_domain … (eq_true_to_b … Hx1)) ] |
---|
| 1056 | whd in match (memb ???); inversion(x == lfalse) normalize nodelta #Hlfalse |
---|
| 1057 | [ #_ @orb_Prop_r @orb_Prop_l >Hlfalse % |
---|
| 1058 | | whd in match (memb ???); inversion (x==ltrue) normalize nodelta #Hltrue |
---|
| 1059 | [ #_ @orb_Prop_l >Hltrue % |
---|
| 1060 | | whd in match (memb ???); #EQ destruct |
---|
| 1061 | ] |
---|
| 1062 | ] |
---|
| 1063 | ] |
---|
| 1064 | | % |
---|
| 1065 | | cases no_dup #_ * #_ /2 by no_duplicates_append_r/ |
---|
| 1066 | | |
---|
| 1067 | ] |
---|
| 1068 | |*: cases daemon (*TODO*) |
---|
| 1069 | ] |
---|
[3400] | 1070 | qed. |
---|
[3396] | 1071 | |
---|
[3400] | 1072 | |
---|
[3396] | 1073 | definition trans_prog : ∀p,p'.Program p p' → |
---|
| 1074 | (Program p p') × (associative_list DEQCostLabel CostLabel) × (list CostLabel)≝ |
---|
| 1075 | λp,p',prog. |
---|
| 1076 | let max_all ≝ foldl … (λn,i.max n (compute_max_n … (f_body … i))) O (env … prog) in |
---|
| 1077 | let 〈t_env,n,m,keep〉 ≝ (foldr ?? |
---|
| 1078 | (λi,x.let 〈t_env,n,m,keep〉 ≝ x in |
---|
| 1079 | let info ≝ call_post_trans … (f_body … i) n (nil ?) in |
---|
[3397] | 1080 | 〈(mk_env_item ?? |
---|
| 1081 | (mk_signature ??(f_name ?? i) (f_pars … i) (f_ret … i)) |
---|
[3400] | 1082 | (f_lab … i) (t_code … info)) :: t_env, |
---|
[3396] | 1083 | fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 :: |
---|
| 1084 | ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉) |
---|
| 1085 | (〈nil ?,max_all,nil ?,nil ?〉) (env … prog)) in |
---|
| 1086 | 〈mk_Program ?? t_env (t_code … (call_post_trans … (main … prog) n (nil ?))),m,keep〉 . |
---|
| 1087 | |
---|
| 1088 | definition map_labels_on_trace : |
---|
| 1089 | (associative_list DEQCostLabel CostLabel) → list CostLabel → list CostLabel ≝ |
---|
| 1090 | λm,l.foldr … (λlab,t.(get_element … m lab) @ t) (nil ?) l. |
---|
| 1091 | |
---|
| 1092 | lemma map_labels_on_trace_append: |
---|
| 1093 | ∀m,l1,l2. map_labels_on_trace m (l1@l2) = |
---|
| 1094 | map_labels_on_trace m l1 @ map_labels_on_trace m l2. |
---|
| 1095 | #m #l1 elim l1 // #hd #tl #IH #l2 >associative_append <IH // |
---|
| 1096 | qed. |
---|
| 1097 | |
---|
[3397] | 1098 | include "../src/common/Errors.ma". |
---|
| 1099 | |
---|
[3399] | 1100 | axiom is_permutation: ∀A.list A → list A → Prop. |
---|
| 1101 | axiom is_permutation_eq : ∀A.∀l : list A.is_permutation … l l. |
---|
| 1102 | axiom is_permutation_cons : ∀A.∀l1,l2,x.is_permutation A l1 l2 → |
---|
| 1103 | is_permutation A (x :: l1) (x :: l2). |
---|
| 1104 | |
---|
| 1105 | (* |
---|
| 1106 | inductive is_permutation (A : Type[0]) : list A → list A → Prop ≝ |
---|
| 1107 | | p_empty : is_permutation A (nil ?) (nil ?) |
---|
| 1108 | | p_append : ∀x,x1,x2,y,y1,y2. |
---|
| 1109 | x = y → is_permutation A (x1 @ x2) (y1 @ y2) → |
---|
| 1110 | is_permutation A (x1 @ [x] @ x2) (y1 @ [y] @ y2). |
---|
| 1111 | |
---|
| 1112 | lemma is_permutation_eq : ∀A.∀l : list A.is_permutation … l l. |
---|
| 1113 | #A #l elim l // #x #xs #IH |
---|
| 1114 | change with ((nil ?) @ (x :: xs)) in ⊢ (??%%); |
---|
| 1115 | >append_cons >associative_append |
---|
| 1116 | @(p_append ? x (nil ?) xs x (nil ?) xs (refl …)) @IH |
---|
| 1117 | qed. |
---|
| 1118 | |
---|
| 1119 | lemma is_permutation_append : ∀A.∀l1,l2,l3,l4 : list A. |
---|
| 1120 | is_permutation A l1 l3 → is_permutation A l2 l4 → |
---|
| 1121 | is_permutation A (l1 @ l2) (l3 @ l4). |
---|
| 1122 | #A #l1 inversion (|l1|) [2: #n lapply l1 elim n |
---|
| 1123 | [ #l2 #l3 #l4 #H inversion H // #x #x1 #x2 #y #y1 #y2 #EQ #H1 #_ |
---|
| 1124 | #ABS cases(nil_to_nil … (sym_eq ??? ABS)) -ABS #_ #ABS |
---|
| 1125 | cases(nil_to_nil … ABS) #EQ1 destruct(EQ1) ] |
---|
| 1126 | #x #xs #IH #l2 #l3 #l4 #H inversion H |
---|
| 1127 | [#EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ) ] |
---|
| 1128 | #y #y1 #y2 #z #z1 #z2 #EQ destruct(EQ) #H1 #_ #EQx_xs #EQ destruct(EQ) #_ |
---|
| 1129 | *) |
---|
| 1130 | |
---|
[3405] | 1131 | lemma memb_append_l22 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A. |
---|
| 1132 | ¬ (x ∈ l1) → x∈ l1 @ l2 = (x ∈ l2). |
---|
| 1133 | #A #x #l1 elim l1 normalize // #y #ys #IH #l2 cases(x==y) |
---|
| 1134 | normalize [*] @IH |
---|
| 1135 | qed. |
---|
| 1136 | |
---|
| 1137 | lemma memb_append_l12 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A. |
---|
| 1138 | ¬ (x ∈ l2) → x∈ l1 @ l2 = (x ∈ l1). |
---|
| 1139 | #A #x #l1 elim l1 |
---|
| 1140 | [ #l2 #H whd in match (append ???); @not_b_to_eq_false @Prop_notb >H % ] |
---|
| 1141 | #y #ys #IH #l2 #H1 whd in match (memb ???); >IH // |
---|
| 1142 | qed. |
---|
| 1143 | |
---|
| 1144 | |
---|
| 1145 | lemma lookup_ok_append : ∀p,p',l,f,env_it. |
---|
| 1146 | lookup p p' l f = return env_it → ∃l1,l2. l = l1 @ [env_it] @ l2 ∧ |
---|
| 1147 | f_name … env_it = f. |
---|
| 1148 | #p #p' #l elim l [ #f #env_it normalize #EQ destruct] |
---|
| 1149 | #x #xs #IH #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim |
---|
| 1150 | [ #EQ destruct(EQ) normalize nodelta whd in ⊢ (???% → ?); #EQ destruct |
---|
| 1151 | %{(nil ?)} %{xs} /2/ |
---|
| 1152 | | #Hno_f normalize nodelta #EQ_env_it cases(IH … EQ_env_it) |
---|
| 1153 | #l1 * #l2 * #EQ1 #EQ2 %{(x :: l1)} %{l2} >EQ1 /2/ |
---|
| 1154 | ] |
---|
| 1155 | qed. |
---|
| 1156 | (* |
---|
| 1157 | lemma foldr_append : |
---|
| 1158 | ∀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. |
---|
| 1159 | #A #B #l1 elim l1 // |
---|
| 1160 | #hd #tl #Hind #l2 #f #seed normalize >Hind @refl |
---|
| 1161 | qed. |
---|
| 1162 | *) |
---|
| 1163 | |
---|
| 1164 | lemma foldr_map_append : |
---|
| 1165 | ∀A,B:Type[0]. ∀l1, l2 : list A. |
---|
| 1166 | ∀f:A → list B. ∀seed. |
---|
| 1167 | foldr ?? (λx,acc. (f x) @ acc) seed (l1 @ l2) = |
---|
| 1168 | append ? (foldr ?? (λx,acc. (f x) @ acc) (nil ?) l1) |
---|
| 1169 | (foldr ?? (λx,acc. (f x) @ acc) seed l2). |
---|
| 1170 | #A #B #l1 elim l1 normalize // /3 by eq_f, trans_eq/ |
---|
| 1171 | qed. |
---|
| 1172 | |
---|
[3408] | 1173 | lemma cons_append : ∀A.∀x : A.∀l.x::l = ([x]@l). |
---|
| 1174 | // |
---|
| 1175 | qed. |
---|
[3405] | 1176 | |
---|
[3408] | 1177 | lemma eq_a_call_label : |
---|
| 1178 | ∀c1,c2.c1 == c2 → a_call c1 == a_call c2. |
---|
| 1179 | #c1 #c2 #EQ cases(eqb_true ? c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ |
---|
| 1180 | #EQ destruct >(\b (refl …)) @I |
---|
| 1181 | qed. |
---|
| 1182 | |
---|
| 1183 | |
---|
[3400] | 1184 | lemma trans_env_ok : ∀p : state_params.∀ prog. |
---|
| 1185 | no_duplicates_labels … prog → |
---|
| 1186 | let 〈t_prog,m,keep〉 ≝ trans_prog … prog in |
---|
| 1187 | ∀f,env_it.lookup p p (env … prog) f = return env_it → |
---|
| 1188 | let dom ≝ get_labels_of_code … (f_body … env_it) in |
---|
| 1189 | ∃env_it',n.lookup p p (env … t_prog) f = return env_it' ∧ |
---|
| 1190 | let info ≝ call_post_trans … (f_body … env_it) n (nil ?) in |
---|
| 1191 | t_code … info = f_body … env_it' ∧ |
---|
| 1192 | get_element … m (a_call (f_lab … env_it')) = (a_call (f_lab … env_it')) :: gen_labels … info ∧ |
---|
| 1193 | f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it' ∧ |
---|
| 1194 | same_fresh_map_on dom m (lab_map … info) ∧ same_to_keep_on dom keep (lab_to_keep … info). |
---|
[3404] | 1195 | #p * #env #main @pair_elim * whd in match trans_prog; normalize nodelta |
---|
[3405] | 1196 | @pair_elim generalize in match O; elim env |
---|
[3404] | 1197 | [ #fresh1 * #env' #fresh #x #_ #t_prog #m #keep #_ #_ #f #env_it normalize in ⊢ (% → ?); #ABS destruct] |
---|
| 1198 | * #hd_sig #hd_lab #hd_code #tail #IH #fresh1 * #env' #fresh * #m' #keep' |
---|
[3400] | 1199 | normalize in ⊢ (% → ?); normalize nodelta @pair_elim * #env_tail #fresh_tail |
---|
[3404] | 1200 | * #m_tail #keep_tail #EQtail normalize nodelta #EQ1 destruct(EQ1) #t_prog |
---|
| 1201 | #m #keep #EQ2 destruct(EQ2) |
---|
[3400] | 1202 | whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H) |
---|
| 1203 | change with (no_duplicates_labels p p (mk_Program p p tail main)) in match |
---|
| 1204 | (no_duplicates_labels p p (mk_Program p p tail main)); #no_dup_tail |
---|
| 1205 | lapply(no_duplicates_append_l … H) #no_dup_head normalize nodelta |
---|
| 1206 | #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta |
---|
| 1207 | [ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ) |
---|
| 1208 | inversion (call_post_trans … hd_code fresh_tail []) |
---|
| 1209 | #gen_labs #t_hd_code #t_fresh #t_lab_map #t_lab_to_keep #EQ_trans_code |
---|
| 1210 | %{(mk_env_item … hd_sig hd_lab t_hd_code)} %{fresh_tail} % |
---|
| 1211 | [ whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta |
---|
| 1212 | @eq_f cases hd_sig // ] >EQ_trans_code % [% [ % [ % [% // whd in ⊢ (??%?); >(\b (refl …)) %] % ] % | whd |
---|
[3405] | 1213 | #x #Hx whd in ⊢ (??%?); >(? : (x == hd_lab) = false) |
---|
| 1214 | [2: inversion(x==hd_lab) // #EQx_hdlab cases Hhd_lab -Hhd_lab #Hhd_lab cases Hhd_lab |
---|
| 1215 | >memb_append_l1 // <(\P EQx_hdlab) >Hx // ] |
---|
| 1216 | normalize nodelta @get_element_append_l1 % #H1 cases daemon (* needs lemma on maps using EQtail *)] |
---|
| 1217 | | whd #x #Hx >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … x … H) |
---|
| 1218 | // cases daemon (*using EQtail in a non trivial way*) |
---|
[3400] | 1219 | ] |
---|
| 1220 | | #Hf #Henv_it cases(IH … no_dup_tail … Henv_it) |
---|
[3404] | 1221 | [5: >EQtail in ⊢ (??%?); % |
---|
| 1222 | |9: normalize nodelta % |
---|
| 1223 | |*: |
---|
| 1224 | ] |
---|
| 1225 | #new_env_it * #new_fresh * #EQlook_new_env_it ***** #EQt_code #EQ_get_el |
---|
| 1226 | #EQsign_env_it #EQ_f_lab #same_fresh_map #same_to_keep %{new_env_it} %{new_fresh} |
---|
| 1227 | % |
---|
| 1228 | [ whd in ⊢ (??%?); @eq_function_name_elim [ #ABS >ABS in Hf; * #H @⊥ @H %] |
---|
| 1229 | #_ normalize nodelta assumption ] |
---|
[3405] | 1230 | % [2: #x #Hx <same_to_keep // @memb_append_l22 |
---|
| 1231 | inversion(memb ???) // #ABS lapply(lab_to_keep_in_domain … (eq_true_to_b … ABS)) |
---|
| 1232 | #ABS1 @(memb_no_duplicates_append … x … H) // |
---|
| 1233 | cases(lookup_ok_append … Henv_it) #l1 * #l2 * #EQ1 #EQ2 destruct(EQ1 EQ2) |
---|
| 1234 | >foldr_map_append >memb_append_l2 // >foldr_map_append >memb_append_l1 // |
---|
| 1235 | whd in match (foldr ?????); @orb_Prop_r >memb_append_l1 // >Hx % ] |
---|
[3408] | 1236 | % [2: #x #Hx <same_fresh_map // >cons_append <associative_append @(get_element_append_r1) |
---|
| 1237 | % >domain_of_associative_list_append #ABS cases(memb_append … ABS) |
---|
| 1238 | [ whd in match (memb ???); inversion(x==hd_lab) normalize nodelta |
---|
| 1239 | [2: #_ whd in match (memb ???); #EQ destruct ] #EQx_hdlab #_ |
---|
| 1240 | <(\P EQx_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it) |
---|
| 1241 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
| 1242 | * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 // |
---|
| 1243 | >memb_append_l1 // whd in ⊢ (??%?); cases(x==?) // |
---|
| 1244 | normalize nodelta >memb_append_l1 // >Hx % |
---|
| 1245 | | #ABS1 @(memb_no_duplicates_append … x … H) |
---|
| 1246 | [ @(lab_map_in_domain … (eq_true_to_b … ABS1)) |
---|
| 1247 | | cases(lookup_ok_append … Henv_it) |
---|
| 1248 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
| 1249 | >memb_append_l2 // >memb_append_l1 // |
---|
| 1250 | whd in ⊢ (??%?); cases(x==?) // |
---|
| 1251 | normalize nodelta >memb_append_l1 // >Hx % |
---|
| 1252 | ] |
---|
| 1253 | ] |
---|
| 1254 | ] |
---|
| 1255 | % // % // % // <EQ_get_el >cons_append <associative_append |
---|
| 1256 | @get_element_append_r1 % >domain_of_associative_list_append #ABS cases(memb_append … ABS) |
---|
| 1257 | [ whd in match (memb ???); inversion(a_call (f_lab … new_env_it)== a_call hd_lab) |
---|
| 1258 | #EQ_hdlab normalize nodelta |
---|
| 1259 | [2: whd in ⊢ (??%? → ?); #EQ destruct ] |
---|
| 1260 | #_ <(\P EQ_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it) |
---|
| 1261 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
| 1262 | * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 // |
---|
| 1263 | >memb_append_l1 // whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) // |
---|
| 1264 | | #ABS1 @(memb_no_duplicates_append … (a_call (f_lab … new_env_it)) … H) |
---|
| 1265 | [ @(lab_map_in_domain … (eq_true_to_b … ABS1)) |
---|
| 1266 | | cases(lookup_ok_append … Henv_it) |
---|
| 1267 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
| 1268 | >memb_append_l2 // >memb_append_l1 // |
---|
| 1269 | whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) // |
---|
| 1270 | ] |
---|
| 1271 | ] |
---|
[3405] | 1272 | ] |
---|
| 1273 | qed. |
---|
[3399] | 1274 | |
---|
| 1275 | |
---|
[3400] | 1276 | |
---|
[3396] | 1277 | lemma correctness : ∀p,p',prog. |
---|
| 1278 | let 〈t_prog,m,keep〉 ≝ trans_prog … prog in |
---|
[3398] | 1279 | ∀s1,s2,s1' : state p.∀abs_top,abs_tail. |
---|
[3396] | 1280 | ∀t : raw_trace (operational_semantics … p' prog) s1 s2. |
---|
[3398] | 1281 | state_rel … m keep abs_top abs_tail s1 s1' → |
---|
| 1282 | ∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'. |
---|
| 1283 | state_rel … m keep abs_top' abs_tail' s2 s2' ∧ |
---|
[3399] | 1284 | is_permutation ? ((abs_top @ (map_labels_on_trace m (get_costlabels_of_trace … t))) @ abs_tail) |
---|
| 1285 | (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail') ∧ |
---|
[3398] | 1286 | len … t = len … t'. |
---|
[3399] | 1287 | #p #p' #prog @pair_elim * #t_prog #m #keep #EQtrans |
---|
| 1288 | #s1 #s2 #s1' #abs_top #abs_tail #t lapply abs_top -abs_top lapply abs_tail |
---|
| 1289 | -abs_tail lapply s1' -s1' elim t |
---|
| 1290 | [ #st #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)} |
---|
| 1291 | % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil |
---|
| 1292 | @is_permutation_eq |
---|
| 1293 | ] |
---|
[3396] | 1294 | #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12 |
---|
| 1295 | [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore |
---|
[3399] | 1296 | #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #IH #s1' #abs_tail #abs_top |
---|
| 1297 | whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?); |
---|
[3396] | 1298 | whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????); |
---|
| 1299 | inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1' |
---|
[3399] | 1300 | normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????); |
---|
| 1301 | inversion(check_continuations ?????) [ #_ *] ** #H1 #l2 #ll2 #EQHl2 |
---|
| 1302 | >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ ***** ] |
---|
[3396] | 1303 | * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta |
---|
[3398] | 1304 | cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta |
---|
[3399] | 1305 | [1,4: [ #x #y ] #_ (*#_ #_ #_ #H*) ***** |
---|
| 1306 | | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1; |
---|
[3397] | 1307 | normalize * /2/ ] * |
---|
[3399] | 1308 | [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ) |
---|
| 1309 | #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1') |
---|
[3397] | 1310 | [ |
---|
| 1311 | | #x |
---|
| 1312 | | #seq #lbl #i #_ |
---|
| 1313 | | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ |
---|
| 1314 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ |
---|
| 1315 | | #f #act_p #ret_post #i #_ |
---|
| 1316 | | #l_in #io #l_out #i #_ |
---|
| 1317 | ] |
---|
| 1318 | [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)] |
---|
| 1319 | cases(call_post_clean ?????) normalize nodelta |
---|
| 1320 | [1,3,5,7,9: #EQ destruct(EQ)] cases daemon (* da fare assurdi!!!*) ] |
---|
[3399] | 1321 | #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ) |
---|
| 1322 | cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …) |
---|
[3398] | 1323 | [2: whd whd in match check_continuations; normalize nodelta |
---|
[3399] | 1324 | change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2 |
---|
| 1325 | normalize nodelta % // % // % // % // @EQcode_c_st12 ] |
---|
| 1326 | #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen |
---|
| 1327 | %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) … t')} |
---|
[3397] | 1328 | [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉) |
---|
| 1329 | [3: assumption |4: assumption |*:] /3 by nmk/ ] |
---|
[3399] | 1330 | % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts |
---|
| 1331 | | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ) |
---|
| 1332 | #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?); |
---|
| 1333 | inversion(code … s1') |
---|
[3397] | 1334 | [ |
---|
| 1335 | | #x |
---|
| 1336 | | #seq #lbl #i #_ |
---|
| 1337 | | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ |
---|
| 1338 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ |
---|
| 1339 | | #f #act_p #ret_post #i #_ |
---|
| 1340 | | #l_in #io #l_out #i #_ |
---|
| 1341 | ] |
---|
| 1342 | [|*: #_ whd in ⊢ (??%% → ?); #EQ cases daemon (* da fare assurdi !!!*) ] |
---|
[3399] | 1343 | #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ) |
---|
| 1344 | cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …) |
---|
[3398] | 1345 | [2: whd whd in match check_continuations; normalize nodelta |
---|
[3399] | 1346 | change with (check_continuations ?????) in match (foldr2 ???????); |
---|
| 1347 | >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]); |
---|
| 1348 | normalize nodelta % // % // % // % // @EQcode_c_st12 ] |
---|
| 1349 | #abs_top' * #abs_tail' * #st3' * #t' ** #Hst3st3' #EQcost #EQlen |
---|
| 1350 | %{abs_top'} %{abs_tail'} %{st3'} |
---|
[3397] | 1351 | %{(t_ind … (cost_act (Some ? lbl)) … t')} |
---|
| 1352 | [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉) |
---|
| 1353 | [3: assumption |4: assumption |*:] /3 by nmk/ ] |
---|
[3399] | 1354 | % [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} >map_labels_on_trace_append |
---|
| 1355 | whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el |
---|
| 1356 | @is_permutation_cons assumption |
---|
| 1357 | ] |
---|
| 1358 | (* |
---|
[3397] | 1359 | | #seq #i #store * [| #lbl] #EQcode11 #EQstore #EQ destruct(EQ) #EQcont |
---|
| 1360 | #EQ destruct(EQ) #Hio_st11 #Hio_st12 #EQ destruct(EQ) #EQ1 #EQ2 destruct(EQ1 EQ2) |
---|
| 1361 | #EQ destruct(EQ) #tl #IH #st3 #l1 whd in ⊢ (% → ?); |
---|
| 1362 | inversion(check_continuations ?????) [1,3: #_ *] * #H1 #l2 |
---|
| 1363 | [ >EQcont in ⊢ (% → ?); | >EQcont in ⊢ (% → ?); ] #EQcheck normalize nodelta |
---|
| 1364 | *** #HH1 [ >EQcode11 in ⊢ (% → ?); | >EQcode11 in ⊢ (% → ?); ] |
---|
| 1365 | inversion(code … st3) |
---|
| 1366 | [1,2,4,5,6,7,8,9,11,12,13,14: (*assurdi da fare *) cases daemon ] |
---|
| 1367 | #seq1 #opt_l #i1 #_ #EQcode_st3 change with (m_bind ?????) in ⊢ (??%? → ?); |
---|
[3399] | 1368 | cases daemon *) |
---|
[3397] | 1369 | |8: #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem |
---|
| 1370 | #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 |
---|
[3399] | 1371 | destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #IH #st1' #abs_top #abs_tail |
---|
| 1372 | whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1 |
---|
| 1373 | #abs_top_cont #abs_tail_cont #EQcheck |
---|
| 1374 | normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1') |
---|
[3397] | 1375 | [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_ |
---|
[3399] | 1376 | #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ) |
---|
[3405] | 1377 | xxxxx |
---|
[3399] | 1378 | cut(∃env_it',n.lookup p p (env … t_prog) f = return env_it' ∧ |
---|
| 1379 | t_code … (call_post_trans … (f_body … env_it) n (nil ?)) = f_body … env_it' ∧ |
---|
| 1380 | get_element … m (a_call (f_lab … env_it')) = (a_call (f_lab … env_it')) :: gen_labels … (call_post_trans … (f_body … env_it) n (nil ?)) ∧ |
---|
| 1381 | f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it') |
---|
| 1382 | [ cases daemon (*TODO*) ] * #env_it' * #fresh' **** #EQenv_it' #EQtrans #EQgen_labels #EQsignature #EQlab_env_it |
---|
| 1383 | change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean; |
---|
| 1384 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind |
---|
| 1385 | inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta |
---|
[3397] | 1386 | [2: inversion(memb ???) normalize nodelta #Hlbl_keep |
---|
[3399] | 1387 | [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
| 1388 | #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta |
---|
| 1389 | [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_ |
---|
| 1390 | lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta |
---|
| 1391 | [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'') |
---|
| 1392 | #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ |
---|
| 1393 | #EQ destruct(EQ) |
---|
| 1394 | 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 ?)))) |
---|
| 1395 | [2: whd >EQcont12 |
---|
| 1396 | change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????); |
---|
| 1397 | >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l' |
---|
| 1398 | whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta |
---|
| 1399 | % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans |
---|
| 1400 | @(inverse_call_post_trans … fresh') [2: % |*: cases daemon (*TODO*) ] |
---|
| 1401 | ] |
---|
| 1402 | #abs_top''' * #abs_tail''' * #st3' * #t' ** #Hst3st3' #EQcosts #EQlen %{abs_top'''} |
---|
| 1403 | %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) … t')} |
---|
| 1404 | [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [2: whd in ⊢ (??%%); >EQlen %] |
---|
| 1405 | %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%); |
---|
| 1406 | >EQlab_env_it >associative_append whd in match (append ???); >associative_append |
---|
| 1407 | >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%); |
---|
| 1408 | whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons |
---|
| 1409 | >append_nil whd in match (append ???) in ⊢ (???%); // |
---|
| 1410 | | |
---|
| 1411 | xxxxxxxxxx |
---|
| 1412 | |
---|
| 1413 | |
---|
| 1414 | |
---|
| 1415 | |
---|
| 1416 | inversion(memb ???) normalize nodelta #Hlbl_keep |
---|
| 1417 | [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
| 1418 | #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta |
---|
| 1419 | [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_ |
---|
| 1420 | lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta |
---|
| 1421 | [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'') |
---|
| 1422 | #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ |
---|
| 1423 | #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta >Hlbl_keep |
---|
| 1424 | normalize nodelta >EQi' normalize nodelta % // % // % [ % // % // % //] |
---|
| 1425 | |
---|
| 1426 | |
---|
| 1427 | |
---|
| 1428 | |
---|
| 1429 | cases(IH (mk_state ? (f_body … env_it') (〈ret_act opt_l',i'〉 :: (cont … st1')) (store ? st12) false) (abs_top'' @ abs_tail_cont) (get_element … m (a_call (f_lab … env_it')))) |
---|
| 1430 | [2: whd >EQcont12 |
---|
| 1431 | change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????); |
---|
| 1432 | >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta |
---|
| 1433 | cases opt_l' in EQcode_st1' EQclean; [| #lbl'] #EQcode_st1' normalize nodelta |
---|
| 1434 | [2: inversion(memb ???) normalize nodelta #Hlbl_keep |
---|
[3397] | 1435 | [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
| 1436 | #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta |
---|
| 1437 | [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_ |
---|
| 1438 | lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta |
---|
[3399] | 1439 | [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'') |
---|
[3397] | 1440 | #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ |
---|
| 1441 | #EQ destruct(EQ) whd in match ret_costed_abs; normalize nodelta >Hlbl_keep |
---|
[3399] | 1442 | normalize nodelta >EQi' normalize nodelta % // % // % [ % // % // % //] >EQcode12 <EQtrans |
---|
[3397] | 1443 | cases daemon (*TODO*) |
---|
| 1444 | | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
[3398] | 1445 | whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta |
---|
| 1446 | % // % // % [ % // % //] >EQcode12 <EQtrans |
---|
[3397] | 1447 | * [ #_ #l3' |
---|
| 1448 | cases(bind_inversion ????? H) in ⊢ ?; |
---|
| 1449 | |
---|
| 1450 | |
---|
| 1451 | >EQcost normalize |
---|
| 1452 | |
---|
| 1453 | %{l1} |
---|
| 1454 | xxxxxxxx |
---|
| 1455 | whd in match is_silent_cost_act_b; normalize nodelta |
---|
[3396] | 1456 | cases lab1 in H Hio11; normalize nodelta |
---|
| 1457 | [1,2,4: [1,2: #x [ #y]] #H #Hio11 #EQ destruct] |
---|
| 1458 | * normalize nodelta [2: #x #H #Hio11 #EQ destruct] #H #Hio11 #_ |
---|
| 1459 | inversion(call_post_clean ?????) |
---|
| 1460 | [ #_ *** ] * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta ***** |
---|
| 1461 | #EQ destruct(EQ) #HH1 #EQ destruct(EQ) >EQcode11 |
---|
| 1462 | whd in match (call_post_clean ?????) in ⊢ (% → ?); whd in ⊢ (??%% → ?); |
---|
| 1463 | inversion(code … s1') |
---|
| 1464 | [| #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ |
---|
| 1465 | destruct(EQ) |*: cases daemon (*ASSURDI!!*)] #EQcode_s1' |
---|
| 1466 | normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio |
---|
| 1467 | cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 ?) |
---|
| 1468 | [2: whd whd in match check_continuations; normalize nodelta >EQHl2 |
---|
| 1469 | normalize nodelta % // % // >EQcode_c_st12 % // ] #l3 * #st3' * #t' ** |
---|
| 1470 | #Hst3st12' #EQcost #EQlen %{l3} %{st3'} %{(t_ind … (cost_act (None ?)) … t')} |
---|
| 1471 | [ whd @(empty ????? 〈(cost_act (None ?)),?〉) |
---|
| 1472 | [3: @hide_prf assumption |4: @hide_prf @EQconts1' |*: ] @hide_prf // |
---|
| 1473 | [ <EQio #H2 @⊥ lapply(Hio11 H2) * #F #eq destruct | % *] ] % |
---|
| 1474 | [ %{Hst3st12'} whd in match (get_costlabels_of_trace ????); |
---|
| 1475 | whd in match (get_costlabels_of_trace ????) in ⊢ (???%); // |
---|
| 1476 | | whd in match (len ????); whd in match (len ????) in ⊢ (???%); |
---|
| 1477 | >EQlen % |
---|
| 1478 | ] |
---|
| 1479 | | #non_sil_lab1 normalize nodelta inversion(call_post_clean ?????) [ #_ ****] |
---|
| 1480 | * #l3 #code' #EQcall' normalize nodelta inversion(ret_costed_abs ??) |
---|
| 1481 | [2: #x #H2 @⊥ cases lab1 in Hl1 H2; normalize |
---|
| 1482 | [ #f #c #_ |
---|
| 1483 | | #x * #ABS @⊥ @ABS % |
---|
| 1484 | | #x #_ |
---|
| 1485 | | #_ |
---|
| 1486 | ] |
---|
| 1487 | #EQ destruct(EQ) ] |
---|
| 1488 | #Hlab1 normalize nodelta ***** #EQ destruct(EQ) #HH1 #EQ destruct(EQ) |
---|
| 1489 | >EQcode11 inversion(code … s1') |
---|
| 1490 | [| #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ |
---|
| 1491 | destruct(EQ) |*: cases daemon (*ASSURDI!!*)] #EQcode_s1' |
---|
| 1492 | normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio |
---|
| 1493 | cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 ?) |
---|
| 1494 | [2: whd whd in match check_continuations; normalize nodelta >EQHl2 |
---|
| 1495 | normalize nodelta % // % // % // >EQcall' % ] #l4 * #st3' * #t' ** |
---|
| 1496 | #Hst3st3' #EQcost #EQlen %{l4} %{st3'} %{(t_ind … lab1 … t')} |
---|
| 1497 | [ whd @(empty ????? 〈lab1,?〉) |
---|
| 1498 | [3: @hide_prf assumption |4: assumption |*:] @hide_prf // #H3 @Hio11 >EQio @H3] |
---|
| 1499 | % [2: whd in match (len ????); whd in match (len ????) in ⊢ (???%); |
---|
| 1500 | >EQlen % ] |
---|
| 1501 | %{Hst3st3'} >associative_append <EQcost <associative_append |
---|
| 1502 | >map_labels_on_trace_append <associative_append @eq_f2 // |
---|
| 1503 | cases new_code' in EQcall'; |
---|
| 1504 | [| #y | #seq #opt_l #i1 | #cond #ltrue #i_true #lfalse #i_false #i1 |
---|
| 1505 | | #cond #ltrue #i_true #lfalse #ifalse | #f #act_p #ret_opt #i | #l_in #io #l_out #i ] |
---|
| 1506 | whd in match (call_post_clean ?????); |
---|
| 1507 | [1,2: #EQ destruct(EQ) // |
---|
| 1508 | |
---|
| 1509 | |
---|
| 1510 | whd in match (get_costlabels_of_trace ??? ?) in ⊢ (??%%); |
---|
| 1511 | |
---|
| 1512 | @eq_f2 whd in ⊢ (??%?); |
---|
| 1513 | |
---|
| 1514 | |
---|
| 1515 | |
---|
| 1516 | cases daemon (*TODO*) |
---|
| 1517 | qed. |
---|