[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". |
---|
[3549] | 20 | include "utils.ma". |
---|
[3394] | 21 | |
---|
[3397] | 22 | discriminator option. |
---|
| 23 | |
---|
[3394] | 24 | record instr_params : Type[1] ≝ |
---|
| 25 | { seq_instr : DeqSet |
---|
| 26 | ; io_instr : DeqSet |
---|
| 27 | ; cond_instr : DeqSet |
---|
| 28 | ; loop_instr : DeqSet |
---|
| 29 | ; act_params_type : DeqSet |
---|
| 30 | ; return_type : DeqSet |
---|
| 31 | }. |
---|
| 32 | |
---|
| 33 | |
---|
[3549] | 34 | inductive Instructions (p : instr_params) |
---|
| 35 | (l_p :label_params) : Type[0] ≝ |
---|
| 36 | | EMPTY : Instructions p l_p |
---|
| 37 | | RETURN : return_type p → Instructions p l_p |
---|
| 38 | | SEQ : (seq_instr p) → option (NonFunctionalLabel l_p) → Instructions p l_p → Instructions p l_p |
---|
| 39 | | COND : (cond_instr p) → (NonFunctionalLabel l_p) → Instructions p l_p → |
---|
| 40 | (NonFunctionalLabel l_p) → Instructions p l_p → Instructions p l_p → |
---|
| 41 | Instructions p l_p |
---|
| 42 | | LOOP : (loop_instr p) → NonFunctionalLabel l_p → Instructions p l_p → |
---|
| 43 | NonFunctionalLabel l_p → Instructions p l_p → Instructions p l_p |
---|
| 44 | | CALL : FunctionName → (act_params_type p) → option (ReturnPostCostLabel l_p) → |
---|
| 45 | Instructions p l_p → Instructions p l_p |
---|
| 46 | | IO : NonFunctionalLabel l_p → (io_instr p) → NonFunctionalLabel l_p → Instructions p l_p → |
---|
| 47 | Instructions p l_p. |
---|
[3394] | 48 | |
---|
[3549] | 49 | let rec eq_instructions (p : instr_params) (l_p : label_params) (i : Instructions p l_p) |
---|
| 50 | on i : (Instructions p l_p) → bool ≝ |
---|
[3394] | 51 | match i with |
---|
| 52 | [ EMPTY ⇒ λi'.match i' with [ EMPTY ⇒ true | _ ⇒ false ] |
---|
| 53 | | RETURN x ⇒ λi'.match i' with [ RETURN y ⇒ x == y | _ ⇒ false ] |
---|
| 54 | | SEQ x lab instr ⇒ λi'.match i' with |
---|
| 55 | [ SEQ y lab' instr' ⇒ x == y ∧ eq_instructions … instr instr' ∧ |
---|
| 56 | match lab with [ None ⇒ match lab' with [ None ⇒ true | _ ⇒ false ] |
---|
[3549] | 57 | | Some l1 ⇒ match lab' with [Some l2 ⇒ eq_nf_label … l1 l2 | _ ⇒ false] |
---|
[3394] | 58 | ] |
---|
| 59 | | _ ⇒ false |
---|
| 60 | ] |
---|
| 61 | | COND x ltrue i1 lfalse i2 i3 ⇒ λi'.match i' with |
---|
| 62 | [ COND y ltrue' i1' lfalse' i2' i3' ⇒ |
---|
[3549] | 63 | x == y ∧ eq_nf_label … ltrue ltrue' ∧ |
---|
| 64 | eq_instructions … i1 i1' ∧ eq_nf_label … lfalse lfalse' ∧ |
---|
[3394] | 65 | eq_instructions … i2 i2' ∧ eq_instructions … i3 i3' |
---|
| 66 | | _ ⇒ false |
---|
| 67 | ] |
---|
| 68 | | LOOP x ltrue i1 lfalse i2 ⇒ λi'.match i' with |
---|
| 69 | [ LOOP y ltrue' i1' lfalse' i2' ⇒ x == y ∧ |
---|
[3549] | 70 | eq_instructions … i1 i1' ∧ eq_nf_label … ltrue ltrue' ∧ |
---|
[3394] | 71 | eq_instructions … i2 i2' |
---|
| 72 | | _ ⇒ false |
---|
| 73 | ] |
---|
| 74 | | CALL f act_p r_lb i1 ⇒ λi'.match i' with |
---|
| 75 | [ CALL f' act_p' r_lb' i1' ⇒ eq_function_name f f' ∧ |
---|
| 76 | act_p == act_p' ∧ eq_instructions … i1 i1' ∧ |
---|
| 77 | match r_lb with [ None ⇒ match r_lb' with [None ⇒ true | _ ⇒ false] |
---|
[3549] | 78 | | Some z ⇒ match r_lb' with [Some w ⇒ eq_return_cost_lab … z w | _ ⇒ false ] |
---|
[3394] | 79 | ] |
---|
| 80 | | _ ⇒ false |
---|
| 81 | ] |
---|
| 82 | | IO lin io lout i1 ⇒ λi'.match i' with |
---|
[3549] | 83 | [ IO lin' io' lout' i1' ⇒ eq_nf_label … lin lin' ∧ io == io' ∧ |
---|
| 84 | eq_nf_label … lout lout' ∧ eq_instructions … i1 i1' |
---|
[3394] | 85 | | _ ⇒ false |
---|
| 86 | ] |
---|
| 87 | ]. |
---|
| 88 | |
---|
[3449] | 89 | |
---|
[3401] | 90 | (* |
---|
[3394] | 91 | lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → |
---|
| 92 | (i1 ≠ i2 → P false) → P (eq_instructions p i1 i2). |
---|
[3396] | 93 | #P #p #i1 elim i1 |
---|
[3401] | 94 | [* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ |
---|
| 95 | lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') |
---|
| 96 | | #rt * normalize [2: #rt' cases (dec_eq … rt rt') #H [>(\b H) | >(\bf H) ] /2/ |
---|
| 97 | #_ #K @K % #abs lapply (eq_to_jmeq ??? abs) #abs' destruct(abs') @(absurd ?? H) //] |
---|
| 98 | [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ |
---|
| 99 | lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') |
---|
[3449] | 100 | | #seq * [| #lbl] #i #IH * normalize |
---|
| 101 | [1,8: |2,9: #t_t |3,10: #seq1 #opt_l #i2 |4,11: #cond #ltrue #i_t #lfalse #i_f #i_c |
---|
| 102 | |5,12: #cond #ltrue #i_t #lfalse #i_f |6,13: #f #act_p #ret #i3 |*: #lin #io #lout #i3] |
---|
| 103 | #H1 #H2 try(@H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct) |
---|
| 104 | inversion(?==?) normalize nodelta |
---|
| 105 | [2,4: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct |
---|
| 106 | >(\b (refl …)) in ABS; #EQ destruct] |
---|
| 107 | #EQseq inversion(eq_instructions ???) normalize nodelta #Heq_i2 |
---|
| 108 | [2,4: @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct |
---|
[3401] | 109 | *) |
---|
[3394] | 110 | |
---|
| 111 | record env_params : Type[1] ≝ |
---|
| 112 | { form_params_type : Type[0] |
---|
| 113 | }. |
---|
| 114 | |
---|
[3397] | 115 | record signature (p : env_params) (p' : instr_params) : Type[0] ≝ |
---|
[3394] | 116 | { f_name : FunctionName |
---|
| 117 | ; f_pars : form_params_type p |
---|
[3397] | 118 | ; f_ret : return_type p' |
---|
| 119 | }. |
---|
| 120 | |
---|
[3549] | 121 | record env_item (p : env_params) (p' : instr_params) (l_p : label_params) : Type[0] ≝ |
---|
[3397] | 122 | { f_sig :> signature p p' |
---|
[3549] | 123 | ; f_lab : CallCostLabel l_p |
---|
| 124 | ; f_body : Instructions p' l_p |
---|
[3394] | 125 | }. |
---|
| 126 | |
---|
| 127 | record state_params : Type[1] ≝ |
---|
[3399] | 128 | { i_pars :> instr_params |
---|
| 129 | ; e_pars :> env_params |
---|
[3549] | 130 | ; l_pars :> label_params |
---|
[3394] | 131 | ; store_type : DeqSet |
---|
| 132 | }. |
---|
| 133 | |
---|
| 134 | record state (p : state_params) : Type[0] ≝ |
---|
[3549] | 135 | { code : Instructions p p |
---|
| 136 | ; cont : list (ActionLabel p × (Instructions p p)) |
---|
[3394] | 137 | ; store : store_type p |
---|
| 138 | ; io_info : bool |
---|
| 139 | }. |
---|
| 140 | |
---|
| 141 | definition is_io : ∀p.state p → Prop ≝ λp,st.io_info … st = true. |
---|
| 142 | |
---|
| 143 | record sem_state_params (p : state_params) : Type[0] ≝ |
---|
[3446] | 144 | { eval_seq : seq_instr p → (store_type p) → option (store_type p) |
---|
| 145 | ; eval_io : io_instr p → store_type p → option (store_type p) |
---|
| 146 | ; eval_cond_cond : cond_instr p → store_type p → option (bool × (store_type p)) |
---|
| 147 | ; eval_loop_cond : loop_instr p → store_type p → option (bool × (store_type p)) |
---|
[3399] | 148 | ; eval_call : signature p p → act_params_type p → store_type p → option (store_type p) |
---|
[3394] | 149 | ; eval_after_return : return_type p → store_type p → option (store_type p) |
---|
| 150 | ; init_store : store_type p |
---|
| 151 | }. |
---|
| 152 | |
---|
| 153 | |
---|
[3549] | 154 | let rec lookup (p : env_params) (p' : instr_params) (l_p : label_params) (l : list (env_item p p' l_p)) |
---|
| 155 | on l : FunctionName → option (env_item p p' l_p) ≝ |
---|
[3394] | 156 | match l with |
---|
| 157 | [ nil ⇒ λ_.None ? |
---|
| 158 | | cons x xs ⇒ λf.if (eq_function_name f (f_name … x)) |
---|
| 159 | then Some ? x |
---|
| 160 | else lookup … xs f |
---|
| 161 | ]. |
---|
| 162 | |
---|
[3549] | 163 | inductive execute_l (p : state_params) (p' : sem_state_params p) (env : list (env_item p p p)) : |
---|
| 164 | ActionLabel p → relation (state p) ≝ |
---|
| 165 | | empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p p)→ (cont ? st) = hd :: tl → |
---|
[3394] | 166 | (code ? st') = \snd hd → (cont … st') = tl → (store … st) = (store … st') → |
---|
[3549] | 167 | (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' |
---|
[3394] | 168 | | seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd → |
---|
[3446] | 169 | eval_seq … p' i (store … st) = return s → (code ? st') = cd → |
---|
[3394] | 170 | (cont … st) = (cont … st') → (store … st') = s → |
---|
[3549] | 171 | io_info … st = false → io_info ? st' = false → execute_l … (cost_act … opt_l) st st' |
---|
[3394] | 172 | | cond_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m. |
---|
[3446] | 173 | (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp (store … st) = return 〈true,new_m〉 → |
---|
[3549] | 174 | cont ? st' = 〈cost_act … (None ?),cd〉 ::(cont … st) → code … st' = i_true → store … st' = new_m → |
---|
| 175 | io_info … st = false → io_info … st' = false → execute_l … (cost_act … (Some ? ltrue)) st st' |
---|
[3394] | 176 | | cond_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m. |
---|
[3446] | 177 | (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp (store … st) = return 〈false,new_m〉 → |
---|
[3549] | 178 | cont ? st' = 〈cost_act … (None ?),cd〉 ::(cont … st) → code … st' = i_false → store … st' = new_m → |
---|
| 179 | io_info … st = false → io_info … st' = false → execute_l … (cost_act … (Some ? lfalse)) st st' |
---|
[3394] | 180 | | loop_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m. |
---|
[3446] | 181 | code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp (store … st) = return 〈true,new_m〉 → |
---|
[3549] | 182 | cont ? st' = 〈cost_act … (None ?),LOOP … exp ltrue i_true lfalse i_false〉 :: (cont … st) → |
---|
[3394] | 183 | code … st' = i_true → store … st' = new_m → io_info … st = false → io_info … st' = false → |
---|
[3549] | 184 | execute_l … (cost_act … (Some ? ltrue)) st st' |
---|
[3394] | 185 | | loop_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m. |
---|
[3446] | 186 | code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp (store … st) = return 〈false,new_m〉 → |
---|
| 187 | cont ? st' = cont … st → code … st' = i_false → store … st' = new_m → |
---|
[3549] | 188 | io_info … st = false → io_info … st' = false → execute_l … (cost_act … (Some ? lfalse)) st st' |
---|
[3394] | 189 | | io_in : ∀st,st',lin,io,lout,cd,mem.(code ? st) = IO … lin io lout cd → |
---|
[3549] | 190 | eval_io … p' io (store … st) = return mem → code ? st' = EMPTY p p → |
---|
| 191 | cont … st' = 〈cost_act … (Some ? lout),cd〉 :: (cont … st) → store … st' = mem → |
---|
| 192 | io_info … st' = true → execute_l … (cost_act … (Some ? lin)) st st' |
---|
[3394] | 193 | | call : ∀st,st',f,act_p,r_lb,cd,mem,env_it.(code ? st) = CALL … f act_p r_lb cd → |
---|
| 194 | lookup … env f = return env_it → |
---|
[3399] | 195 | eval_call ? p' env_it act_p (store … st) = return mem → |
---|
[3394] | 196 | store ? st' = mem → code … st' = f_body … env_it → |
---|
| 197 | cont … st' = |
---|
[3549] | 198 | 〈(ret_act … r_lb),cd〉 :: (cont … st) → |
---|
[3394] | 199 | io_info … st = false → (io_info … st') = false → |
---|
[3549] | 200 | execute_l … (call_act … f (f_lab … env_it)) st st' |
---|
[3394] | 201 | | ret_instr : ∀st,st',r_t,mem,tl',rb,cd.code ? st = RETURN … r_t → |
---|
[3549] | 202 | cont … st = 〈ret_act … rb,cd〉 :: tl' → cont ? st' = tl' → |
---|
[3394] | 203 | io_info … st = false → io_info ? st' = false → |
---|
| 204 | eval_after_return … p' r_t (store … st) = return mem → code … st' = cd → |
---|
[3549] | 205 | store … st' = mem → execute_l … (ret_act … rb) st st'. |
---|
[3400] | 206 | |
---|
[3549] | 207 | let rec get_labels_of_code (p : instr_params) (l_p : label_params) (i : Instructions p l_p) on i : list (CostLabel l_p) ≝ |
---|
[3400] | 208 | match i with |
---|
| 209 | [ EMPTY ⇒ [ ] |
---|
| 210 | | RETURN x ⇒ [ ] |
---|
| 211 | | SEQ x lab instr ⇒ let ih ≝ get_labels_of_code … instr in |
---|
[3549] | 212 | match lab with [ None ⇒ ih | Some lbl ⇒ a_non_functional_label … lbl :: ih ] |
---|
[3400] | 213 | | COND x ltrue i1 lfalse i2 i3 ⇒ |
---|
| 214 | let ih3 ≝ get_labels_of_code … i3 in |
---|
| 215 | let ih2 ≝ get_labels_of_code … i2 in |
---|
| 216 | let ih1 ≝ get_labels_of_code … i1 in |
---|
| 217 | ltrue :: lfalse :: (ih1 @ ih2 @ih3) |
---|
| 218 | | LOOP x ltrue i1 lfalse i2 ⇒ |
---|
| 219 | let ih2 ≝ get_labels_of_code … i2 in |
---|
| 220 | let ih1 ≝ get_labels_of_code … i1 in |
---|
[3549] | 221 | a_non_functional_label … ltrue :: a_non_functional_label … lfalse :: (ih1 @ ih2) |
---|
[3400] | 222 | | CALL f act_p r_lb i1 ⇒ |
---|
| 223 | let ih1 ≝ get_labels_of_code … i1 in |
---|
[3549] | 224 | match r_lb with [ None ⇒ ih1 | Some lbl ⇒ a_return_post … lbl :: ih1] |
---|
[3400] | 225 | | IO lin io lout i1 ⇒ |
---|
| 226 | let ih1 ≝ get_labels_of_code … i1 in |
---|
[3549] | 227 | a_non_functional_label … lin :: a_non_functional_label … lout :: ih1 |
---|
[3400] | 228 | ]. |
---|
| 229 | |
---|
[3549] | 230 | record Program (p : env_params) (p' : instr_params) (l_p : label_params) : Type[0] ≝ |
---|
| 231 | { env : list (env_item p p' l_p) |
---|
| 232 | ; main : Instructions p' l_p |
---|
[3394] | 233 | }. |
---|
| 234 | |
---|
[3400] | 235 | |
---|
[3549] | 236 | |
---|
| 237 | definition no_duplicates_labels : ∀p,p',l_p.Program p p' l_p → Prop ≝ |
---|
| 238 | λp,p',l_p,prog. |
---|
[3400] | 239 | no_duplicates … |
---|
[3549] | 240 | (foldr … |
---|
| 241 | (λitem,acc.((a_call … (f_lab … item)) :: get_labels_of_code … (f_body … item)) @ acc) |
---|
| 242 | (get_labels_of_code … (main … prog)) (env … prog)). |
---|
[3400] | 243 | |
---|
| 244 | lemma no_duplicates_domain_of_fun: |
---|
[3549] | 245 | ∀p,p',l_p,prog.no_duplicates_labels … prog → |
---|
| 246 | ∀f,env_it.lookup p p' l_p (env … prog) f = return env_it → |
---|
[3400] | 247 | no_duplicates … (get_labels_of_code … (f_body … env_it)). |
---|
[3549] | 248 | #p #p' #l_p * #env elim env [ #main normalize #_ #f #env_it #EQ destruct(EQ)] |
---|
[3400] | 249 | #x #xs #IH #main whd in ⊢ (% → ?); whd in match (foldr ?????); #H #f #env_it |
---|
| 250 | whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta |
---|
| 251 | [ whd in ⊢ (? → ???% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) cases H #_ /2/ ] |
---|
| 252 | #H1 #EQenv_it @IH cases H /2/ |
---|
| 253 | qed. |
---|
| 254 | |
---|
| 255 | |
---|
[3447] | 256 | definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.cont … s1 = cont … s2 ∧ |
---|
[3394] | 257 | match (code … s1) with |
---|
| 258 | [ CALL f act_p r_lb i1 ⇒ code … s2 = i1 |
---|
| 259 | | _ ⇒ False |
---|
| 260 | ]. |
---|
| 261 | |
---|
[3549] | 262 | definition operational_semantics : ∀p : state_params.∀p'.Program p p p → abstract_status p ≝ |
---|
| 263 | λp,p',prog.mk_abstract_status … |
---|
[3394] | 264 | (state p) |
---|
| 265 | (execute_l ? p' (env … prog)) |
---|
| 266 | (is_synt_succ …) |
---|
| 267 | (λs.match (code … s) with |
---|
| 268 | [ COND _ _ _ _ _ _ ⇒ cl_jump |
---|
| 269 | | LOOP _ _ _ _ _ ⇒ cl_jump |
---|
| 270 | | EMPTY ⇒ if io_info … s then cl_io else cl_other |
---|
| 271 | | _ ⇒ cl_other |
---|
| 272 | ]) |
---|
| 273 | (λs.match (code … s) with |
---|
| 274 | [CALL _ _ m _ ⇒ match m with [ Some _ ⇒ true | None ⇒ false ] |
---|
| 275 | | _ ⇒ false |
---|
| 276 | ]) |
---|
| 277 | (λs.eq_instructions … (code … s) (main … prog) ∧ isnilb … (cont … s) ∧ store … s == init_store … p' ∧ io_info … s) |
---|
| 278 | (λs.match (cont … s) with |
---|
| 279 | [ nil ⇒ match (code … s) with |
---|
| 280 | [ EMPTY ⇒ true |
---|
| 281 | | RETURN _ ⇒ true |
---|
| 282 | | _ ⇒ false |
---|
| 283 | ] |
---|
| 284 | | _ ⇒ false |
---|
| 285 | ]) |
---|
| 286 | ???. |
---|
| 287 | @hide_prf |
---|
| 288 | [ #s1 #s2 #l #H #H1 inversion H1 #st #st' |
---|
| 289 | [ #hd #tl |
---|
| 290 | | #i #cd #s #opt_l |
---|
| 291 | |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |
---|
| 292 | |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m |
---|
| 293 | | #lin #io #lout #cd #mem |
---|
| 294 | | #f #act_p #r_lb #cd #mem #env_it |
---|
| 295 | | #r_t #mem #tl #rb #cd |
---|
| 296 | ] |
---|
| 297 | #EQcode |
---|
| 298 | [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQ5 #H2 #EQ' #EQ6 #EQ7 |
---|
| 299 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
| 300 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
| 301 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
| 302 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
| 303 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
| 304 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 |
---|
| 305 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
| 306 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
| 307 | ] |
---|
| 308 | #_ destruct >EQcode in H; normalize nodelta /2 by ex_intro/ |
---|
| 309 | [ cases(io_info ??) normalize nodelta] #EQ destruct |
---|
| 310 | | #s1 #s2 #l #H #H1 inversion H1 #st #st' |
---|
| 311 | [ #hd #tl |
---|
| 312 | | #i #cd #s #opt_l |
---|
| 313 | |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |
---|
| 314 | |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m |
---|
| 315 | | #lin #io #lout #cd #mem |
---|
| 316 | | #f #act_p #r_lb #cd #mem #env_it |
---|
| 317 | | #r_t #mem #tl #rb #cd |
---|
| 318 | ] |
---|
| 319 | #EQcode |
---|
| 320 | [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7 |
---|
| 321 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 322 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 323 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 324 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 325 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 326 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost' #EQ6 #EQ7 #EQ8 |
---|
| 327 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQiost' #EQ8 #EQ9 #EQ10 |
---|
| 328 | | #EQ1 #EQ2 #EQ3 #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
| 329 | ] |
---|
| 330 | #_ destruct |
---|
| 331 | cases(code ? st') in H; normalize nodelta >EQiost' normalize nodelta |
---|
| 332 | #eq destruct try (#eq1 destruct) try (#eq2 destruct) try (#eq3 destruct) |
---|
| 333 | try (#eq4 destruct) try (#eq5 destruct) try (#eq6 destruct) %{lin} % |
---|
| 334 | | #s1 #s2 #l #H #H1 inversion H1 #st #st' |
---|
| 335 | [ #hd #tl |
---|
| 336 | | #i #cd #s #opt_l |
---|
| 337 | |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |
---|
| 338 | |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m |
---|
| 339 | | #lin #io #lout #cd #mem |
---|
| 340 | | #f #act_p #r_lb #cd #mem #env_it |
---|
| 341 | | #r_t #mem #tl #rb #cd |
---|
| 342 | ] |
---|
| 343 | #EQcode |
---|
| 344 | [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7 |
---|
| 345 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 346 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 347 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 348 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 349 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
| 350 | | #EQ1 #EQ2 #EQ3 #EQiost #EQiost' #EQ6 #EQ7 #EQ8 |
---|
| 351 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost #EQiost' #EQ8 #EQ9 #EQ10 |
---|
| 352 | | #EQ1 #EQ2 #EQiost #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
| 353 | ] |
---|
| 354 | #_ destruct >EQcode in H; normalize nodelta [|*: #EQ destruct] |
---|
| 355 | cases(io_info … st) in x; normalize nodelta [2: #_ #EQ destruct] |
---|
| 356 | #H3 #_ @H3 % |
---|
| 357 | ] |
---|
| 358 | qed. |
---|
| 359 | |
---|
[3549] | 360 | record call_post_info (p : instr_params) (l_p : label_params) : Type[0] ≝ |
---|
| 361 | { gen_labels : list (CostLabel l_p) |
---|
| 362 | ; t_code : Instructions p l_p |
---|
| 363 | ; fresh : l_p |
---|
| 364 | ; lab_map : associative_list (DEQCostLabel l_p) (CostLabel l_p) |
---|
| 365 | ; lab_to_keep : list (ReturnPostCostLabel l_p) |
---|
[3396] | 366 | }. |
---|
| 367 | |
---|
[3549] | 368 | let rec call_post_trans (p : instr_params) (l_p : label_params) (i : Instructions p l_p) (n : l_p) on i : |
---|
| 369 | list (CostLabel l_p) → call_post_info p l_p ≝ |
---|
[3396] | 370 | λabs. |
---|
[3394] | 371 | match i with |
---|
[3549] | 372 | [ EMPTY ⇒ mk_call_post_info … abs (EMPTY …) n (nil ?) (nil ?) |
---|
| 373 | | RETURN x ⇒ mk_call_post_info … abs (RETURN … x) n (nil ?) (nil ?) |
---|
[3394] | 374 | | SEQ x lab instr ⇒ |
---|
[3396] | 375 | let ih ≝ call_post_trans … instr n abs in |
---|
[3394] | 376 | match lab with |
---|
[3549] | 377 | [ None ⇒ mk_call_post_info … (gen_labels ?? ih) (SEQ … x (None ?) (t_code … ih)) |
---|
[3396] | 378 | (fresh … ih) (lab_map … ih) (lab_to_keep … ih) |
---|
| 379 | | Some lbl ⇒ |
---|
[3549] | 380 | mk_call_post_info … (nil ?) (SEQ … x (Some ? lbl) (t_code … ih)) (fresh … ih) |
---|
| 381 | (〈a_non_functional_label … lbl,((a_non_functional_label … lbl) :: (gen_labels … ih))〉 :: (lab_map … ih)) |
---|
[3396] | 382 | (lab_to_keep … ih) |
---|
[3394] | 383 | ] |
---|
| 384 | | COND x ltrue i1 lfalse i2 i3 ⇒ |
---|
[3396] | 385 | let ih3 ≝ call_post_trans … i3 n abs in |
---|
| 386 | let ih2 ≝ call_post_trans … i2 (fresh … ih3) (gen_labels … ih3) in |
---|
| 387 | let ih1 ≝ call_post_trans … i1 (fresh … ih2) (gen_labels … ih3) in |
---|
[3549] | 388 | mk_call_post_info p l_p (nil ?) (COND … x ltrue (t_code … ih1) lfalse (t_code … ih2) (t_code … ih3)) |
---|
[3396] | 389 | (fresh … ih1) |
---|
[3549] | 390 | (〈a_non_functional_label … ltrue,(a_non_functional_label … ltrue :: (gen_labels … ih1))〉:: |
---|
| 391 | 〈a_non_functional_label … lfalse,(a_non_functional_label … lfalse :: (gen_labels … ih2))〉:: |
---|
[3396] | 392 | ((lab_map … ih1) @ (lab_map … ih2) @ (lab_map … ih3))) |
---|
| 393 | ((lab_to_keep … ih1) @ (lab_to_keep … ih2) @ (lab_to_keep … ih3)) |
---|
[3394] | 394 | | LOOP x ltrue i1 lfalse i2 ⇒ |
---|
[3396] | 395 | let ih2 ≝ call_post_trans … i2 n abs in |
---|
| 396 | let ih1 ≝ call_post_trans … i1 (fresh … ih2) (nil ?) in |
---|
[3549] | 397 | mk_call_post_info p l_p (nil ?) (LOOP … x ltrue (t_code … ih1) lfalse (t_code … ih2)) (fresh … ih1) |
---|
| 398 | (〈a_non_functional_label … lfalse,(a_non_functional_label … lfalse :: (gen_labels … ih2))〉 :: |
---|
| 399 | 〈a_non_functional_label … ltrue,(a_non_functional_label … ltrue :: (gen_labels … ih1))〉 :: |
---|
[3396] | 400 | ((lab_map … ih1) @ (lab_map … ih2))) |
---|
| 401 | ((lab_to_keep … ih1) @ (lab_to_keep … ih2)) |
---|
[3394] | 402 | | CALL f act_p r_lb i1 ⇒ |
---|
[3396] | 403 | let ih ≝ call_post_trans … i1 n abs in |
---|
[3394] | 404 | match r_lb with |
---|
[3549] | 405 | [ None ⇒ let 〈l',f''〉 ≝ fresh_rc_label l_p (fresh … ih) in |
---|
| 406 | mk_call_post_info p l_p ((a_return_post … l')::(gen_labels … ih)) |
---|
[3396] | 407 | (CALL … f act_p (Some ? l') (t_code … ih)) f'' (lab_map … ih) (lab_to_keep … ih) |
---|
| 408 | | Some lbl ⇒ |
---|
[3549] | 409 | mk_call_post_info p l_p (nil ?) (CALL … f act_p (Some ? lbl) (t_code … ih)) (fresh … ih) |
---|
| 410 | (〈a_return_post … lbl,(a_return_post … lbl :: (gen_labels … ih))〉 :: (lab_map … ih)) |
---|
[3414] | 411 | (lbl :: lab_to_keep … ih) |
---|
[3394] | 412 | ] |
---|
| 413 | | IO lin io lout i1 ⇒ |
---|
[3396] | 414 | let ih ≝ call_post_trans … i1 n abs in |
---|
[3549] | 415 | mk_call_post_info p l_p (nil ?) (IO … lin io lout (t_code … ih)) (fresh … ih) |
---|
| 416 | (〈a_non_functional_label … lout,(a_non_functional_label … lout :: (gen_labels … ih))〉 :: |
---|
| 417 | 〈a_non_functional_label … lin,[a_non_functional_label … lin]〉 :: (lab_map … ih)) (lab_to_keep … ih) |
---|
[3394] | 418 | ]. |
---|
| 419 | |
---|
[3396] | 420 | |
---|
[3549] | 421 | let rec call_post_clean (p : instr_params) (l_p : label_params) (i : Instructions p l_p) on i : |
---|
| 422 | associative_list (DEQCostLabel l_p) (CostLabel l_p) → list (ReturnPostCostLabel l_p) → list (CostLabel l_p) → |
---|
| 423 | option ((list (CostLabel l_p)) × (Instructions p l_p)) ≝ |
---|
[3396] | 424 | λm,keep,abs. |
---|
| 425 | match i with |
---|
| 426 | [ EMPTY ⇒ Some ? 〈abs,EMPTY …〉 |
---|
| 427 | | RETURN x ⇒ Some ? 〈abs,RETURN … x〉 |
---|
| 428 | | SEQ x lab instr ⇒ |
---|
| 429 | ! 〈l,i1〉 ← call_post_clean … instr m keep abs; |
---|
| 430 | match lab with |
---|
| 431 | [ None ⇒ return 〈l,SEQ … x (None ?) i1〉 |
---|
| 432 | | Some lbl ⇒ if ((get_element … m lbl) == lbl :: l) |
---|
| 433 | then return 〈nil ?,SEQ … x (Some ? lbl) i1〉 |
---|
| 434 | else None ? |
---|
| 435 | ] |
---|
| 436 | | COND x ltrue i1 lfalse i2 i3 ⇒ |
---|
| 437 | ! 〈l3,instr3〉 ← call_post_clean … i3 m keep abs; |
---|
| 438 | ! 〈l2,instr2〉 ← call_post_clean … i2 m keep l3; |
---|
| 439 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep l3; |
---|
| 440 | if ((get_element … m ltrue) == ltrue :: l1) ∧ |
---|
| 441 | ((get_element … m lfalse) == lfalse :: l2) |
---|
| 442 | then return 〈nil ?,COND … x ltrue instr1 lfalse instr2 instr3〉 |
---|
| 443 | else None ? |
---|
| 444 | | LOOP x ltrue i1 lfalse i2 ⇒ |
---|
| 445 | ! 〈l2,instr2〉 ← call_post_clean … i2 m keep abs; |
---|
| 446 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep (nil ?); |
---|
| 447 | if ((get_element … m ltrue) == ltrue :: l1) ∧ |
---|
| 448 | ((get_element … m lfalse) == lfalse :: l2) |
---|
| 449 | then return 〈nil ?,LOOP … x ltrue instr1 lfalse instr2〉 |
---|
| 450 | else None ? |
---|
| 451 | | CALL f act_p r_lb i1 ⇒ |
---|
| 452 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs; |
---|
| 453 | match r_lb with |
---|
[3410] | 454 | [ None ⇒ None ? |
---|
[3414] | 455 | | Some lbl ⇒ if (lbl ∈ keep) |
---|
[3396] | 456 | then if ((get_element … m lbl) == lbl :: l1) |
---|
| 457 | then return 〈nil ?,CALL … f act_p (Some ? lbl) instr1〉 |
---|
| 458 | else None ? |
---|
[3549] | 459 | else return 〈(a_return_post l_p lbl) :: l1,CALL … f act_p (None ?) instr1〉 |
---|
[3396] | 460 | ] |
---|
| 461 | | IO lin io lout i1 ⇒ |
---|
| 462 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs; |
---|
| 463 | if ((get_element … m lout) == lout :: l1) ∧ ((get_element … m lin) == [lin]) |
---|
| 464 | then return 〈nil ?,IO … lin io lout instr1〉 |
---|
| 465 | else None ? |
---|
| 466 | ]. |
---|
| 467 | |
---|
| 468 | |
---|
[3549] | 469 | definition ret_costed_abs : ∀p.list (ReturnPostCostLabel p) → option (ReturnPostCostLabel p) → |
---|
| 470 | option (CostLabel p) ≝ |
---|
| 471 | λp,keep,x. |
---|
[3396] | 472 | match x with |
---|
[3549] | 473 | [ Some lbl ⇒ if lbl ∈ keep then return (a_return_post … lbl) |
---|
[3396] | 474 | else None ? |
---|
| 475 | | None ⇒ None ? |
---|
| 476 | ]. |
---|
| 477 | |
---|
[3399] | 478 | |
---|
[3549] | 479 | definition check_continuations : ∀p : instr_params.∀l_p : label_params. |
---|
| 480 | ∀l1,l2 : list ((ActionLabel l_p) × (Instructions p l_p)). |
---|
| 481 | associative_list (DEQCostLabel l_p) (CostLabel l_p) → |
---|
| 482 | list (ReturnPostCostLabel l_p) → option (Prop × (list (CostLabel l_p)) × (list (CostLabel l_p))) ≝ |
---|
| 483 | λp,l_p,cont1,cont2,m,keep. |
---|
[3399] | 484 | foldr2 ??? 〈True,nil ?,nil ?〉 cont1 cont2 |
---|
| 485 | (λx,y,z. |
---|
| 486 | let 〈cond,abs_top',abs_tail'〉 ≝ x in |
---|
[3549] | 487 | match call_post_clean p l_p (\snd z) m keep abs_top' with |
---|
[3399] | 488 | [ None ⇒ 〈False,nil ?,nil ?〉 |
---|
| 489 | | Some w ⇒ |
---|
| 490 | match \fst z with |
---|
| 491 | [ ret_act opt_x ⇒ |
---|
[3549] | 492 | match ret_costed_abs … keep opt_x with |
---|
[3399] | 493 | [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ |
---|
| 494 | get_element … m lbl = lbl :: (\fst w),(nil ?),abs_tail'〉 |
---|
| 495 | | None ⇒ |
---|
[3549] | 496 | 〈\fst y = ret_act … (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) @ abs_tail'〉 |
---|
[3399] | 497 | ] |
---|
| 498 | | cost_act opt_x ⇒ |
---|
| 499 | match opt_x with |
---|
| 500 | [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉 |
---|
| 501 | | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ |
---|
| 502 | get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉] |
---|
| 503 | | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). |
---|
| 504 | |
---|
[3398] | 505 | (* in input : |
---|
| 506 | abs_top is the list of labels to be propageted to the deepest level of the call stack |
---|
[3525] | 507 | equivalently (?) is the list of labels I need to pay now |
---|
| 508 | |
---|
[3398] | 509 | abs_tail are the lists of labels to be propagated to the levels "below" the deepest level |
---|
[3525] | 510 | equivalently (?) is the list of labels I must have already payid in the |
---|
| 511 | code already executed; generated by the continuations below me in the stack |
---|
[3398] | 512 | in output : |
---|
| 513 | abs_top is the list of labels to be propageted from the current level of the call stack |
---|
[3525] | 514 | non empty only in the case of non-call stack frames (whiles, ifs, etc; but in |
---|
| 515 | practice it is always nil!) |
---|
| 516 | abs_tail are the lists of labels to be propagated from the levels "below" the current level |
---|
| 517 | or equivalently (?) the list of labels I must have already paied in the code |
---|
| 518 | already executed; generated by this level of the stack |
---|
| 519 | *) |
---|
[3398] | 520 | |
---|
[3396] | 521 | |
---|
[3549] | 522 | definition state_rel : ∀p : state_params. |
---|
| 523 | associative_list (DEQCostLabel p) (CostLabel p) → list (ReturnPostCostLabel p) → |
---|
| 524 | list (CostLabel p) → list (CostLabel p) → |
---|
[3398] | 525 | relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2. |
---|
[3549] | 526 | match check_continuations … (cont ? st1) (cont … st2) m keep with |
---|
[3398] | 527 | [ Some x ⇒ let 〈prf1,abs_top',abs_tail'〉 ≝ x in |
---|
| 528 | prf1 ∧ call_post_clean … (code … st2) m keep abs_top' = return 〈abs_top,(code … st1)〉 |
---|
| 529 | ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 ∧ abs_tail = abs_tail' |
---|
[3396] | 530 | | None ⇒ False |
---|
| 531 | ]. |
---|
| 532 | |
---|
[3549] | 533 | let rec compute_max_n (p : instr_params) (l_p : label_params) (i : Instructions p l_p) on i : l_p ≝ |
---|
[3396] | 534 | match i with |
---|
[3549] | 535 | [ EMPTY ⇒ e … l_p |
---|
| 536 | | RETURN x ⇒ e … l_p |
---|
[3396] | 537 | | SEQ x lab instr ⇒ let n ≝ compute_max_n … instr in |
---|
| 538 | match lab with |
---|
| 539 | [ None ⇒ n |
---|
| 540 | | Some l ⇒ |
---|
| 541 | match l with |
---|
[3549] | 542 | [ a_non_functional_label n' ⇒ op … l_p n n' ] |
---|
[3396] | 543 | ] |
---|
| 544 | | COND x ltrue i1 lfalse i2 i3 ⇒ |
---|
| 545 | let n1 ≝ compute_max_n … i1 in |
---|
| 546 | let n2 ≝ compute_max_n … i2 in |
---|
| 547 | let n3 ≝ compute_max_n … i3 in |
---|
[3549] | 548 | let mx ≝ op … l_p (op … l_p n1 n2) n3 in |
---|
[3396] | 549 | match ltrue with |
---|
| 550 | [ a_non_functional_label lt ⇒ |
---|
| 551 | match lfalse with |
---|
[3549] | 552 | [a_non_functional_label lf ⇒ op … l_p (op … l_p mx lt) lf ] ] |
---|
[3396] | 553 | | LOOP x ltrue i1 lfalse i2 ⇒ |
---|
| 554 | let n1 ≝ compute_max_n … i1 in |
---|
| 555 | let n2 ≝ compute_max_n … i2 in |
---|
[3549] | 556 | let mx ≝ op … l_p n1 n2 in |
---|
[3396] | 557 | match ltrue with |
---|
| 558 | [ a_non_functional_label lt ⇒ |
---|
| 559 | match lfalse with |
---|
[3549] | 560 | [a_non_functional_label lf ⇒ op … l_p (op … l_p mx lt) lf ] ] |
---|
[3396] | 561 | | CALL f act_p r_lb i1 ⇒ |
---|
| 562 | let n ≝ compute_max_n … i1 in |
---|
| 563 | match r_lb with |
---|
| 564 | [ None ⇒ n |
---|
[3549] | 565 | | Some lbl ⇒ match lbl with [a_return_cost_label l ⇒ op … l_p l n ] |
---|
[3396] | 566 | ] |
---|
| 567 | | IO lin io lout i1 ⇒ |
---|
| 568 | let n ≝ compute_max_n … i1 in |
---|
| 569 | match lin with |
---|
| 570 | [a_non_functional_label l1 ⇒ |
---|
| 571 | match lout with |
---|
[3549] | 572 | [a_non_functional_label l2 ⇒ op … l_p (op … l_p n l1) l2 ] ] |
---|
[3396] | 573 | ]. |
---|
| 574 | |
---|
| 575 | |
---|
[3549] | 576 | definition same_fresh_map_on : ∀p.list (CostLabel p) → |
---|
| 577 | relation (associative_list (DEQCostLabel p) (CostLabel p)) ≝ |
---|
| 578 | λp,dom,m1,m2.∀x.bool_to_Prop (x ∈ dom) → get_element … m1 x = get_element … m2 x. |
---|
[3400] | 579 | |
---|
[3549] | 580 | definition same_to_keep_on : ∀p. list (CostLabel p) → relation (list (ReturnPostCostLabel p)) ≝ |
---|
| 581 | λp,dom,keep1,keep2.∀x. bool_to_Prop (a_return_post … x ∈ dom) → (x ∈ keep1) = (x ∈ keep2). |
---|
[3400] | 582 | |
---|
| 583 | |
---|
[3549] | 584 | lemma same_to_keep_on_append : ∀p.∀dom1,dom2,dom3 : list (CostLabel p). |
---|
| 585 | ∀l1,l2,l3,l : list (ReturnPostCostLabel p). |
---|
| 586 | no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → a_return_post … x ∈ dom1) → |
---|
| 587 | (∀x.x ∈ l3 → a_return_post … x ∈ dom3) → |
---|
| 588 | same_to_keep_on … (dom1@dom2@dom3) (l1@l2@l3) l → |
---|
| 589 | same_to_keep_on … dom2 l2 l. |
---|
| 590 | #p #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #sub_set1 #sub_set3 #H2 |
---|
[3403] | 591 | #x #Hx inversion (x ∈ l2) |
---|
| 592 | [ #EQkeep <H2 [> memb_append_l2 // >memb_append_l1 // ] |
---|
| 593 | >memb_append_l2 // >memb_append_l1 // >Hx // |
---|
| 594 | | #EQno_keep <H2 |
---|
| 595 | [2: >memb_append_l2 // >memb_append_l1 // >Hx // |
---|
| 596 | | @sym_eq @memb_not_append [2: @memb_not_append //] |
---|
| 597 | [ <associative_append in no_dup; #no_dup ] |
---|
[3549] | 598 | lapply(memb_no_duplicates_append … (a_return_post … x) … no_dup) #H |
---|
[3403] | 599 | inversion(memb ???) // #H1 cases H |
---|
| 600 | [1,4: [>memb_append_l2 | >memb_append_l1] // >Hx // |
---|
| 601 | | @sub_set3 >H1 // |
---|
| 602 | | @sub_set1 >H1 // |
---|
| 603 | ] |
---|
| 604 | ] |
---|
| 605 | ] |
---|
| 606 | qed. |
---|
| 607 | |
---|
[3549] | 608 | lemma same_fresh_map_on_append : ∀p.∀dom1,dom2,dom3,l1,l2,l3,l. |
---|
[3403] | 609 | no_duplicates … (dom1 @dom2 @ dom3) → (∀x.x ∈ domain_of_associative_list … l1 → x ∈ dom1) → |
---|
| 610 | (∀x.x ∈ domain_of_associative_list … l3 → x ∈ dom3) → |
---|
[3549] | 611 | same_fresh_map_on p … (dom1 @dom2 @dom3) (l1 @l2 @ l3) l → |
---|
| 612 | same_fresh_map_on p … dom2 l2 l. |
---|
| 613 | #p #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #subset1 #subset3 whd in ⊢ (% → ?); #H1 |
---|
[3403] | 614 | whd #x #Hx <H1 |
---|
| 615 | [2: >memb_append_l2 // >memb_append_l1 // >Hx //] |
---|
| 616 | >get_element_append_r [ >get_element_append_l1 // ] % #K |
---|
| 617 | [ lapply(subset3 … K) | lapply(subset1 … K) ] #ABS |
---|
| 618 | [ <associative_append in no_dup; #no_dup] @(memb_no_duplicates_append … x … no_dup) |
---|
| 619 | // [>memb_append_l2 | >memb_append_l1 ] // >Hx // |
---|
| 620 | qed. |
---|
| 621 | |
---|
| 622 | |
---|
[3549] | 623 | lemma lab_to_keep_in_domain : ∀p,l_p.∀i : Instructions p l_p. |
---|
[3400] | 624 | ∀x,n,l. |
---|
[3549] | 625 | x ∈ lab_to_keep … (call_post_trans … i n l) → a_return_post … x ∈ get_labels_of_code … i. |
---|
| 626 | #p #l_p #i elim i // |
---|
[3400] | 627 | [ #seq #opt_l #instr #IH #x #n #l whd in match (call_post_trans ????); |
---|
| 628 | cases opt_l -opt_l normalize nodelta [|#lbl] |
---|
| 629 | whd in match (get_labels_of_code ??); #H [2: @orb_Prop_r] /2/ |
---|
| 630 | | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l |
---|
| 631 | whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); |
---|
| 632 | #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r |
---|
| 633 | [ >memb_append_l1 // @IH1 [3: >H // |*: ] |
---|
| 634 | | >memb_append_l2 // cases(memb_append … H) -H #H |
---|
| 635 | [>memb_append_l1 // @IH2 [3: >H // |*: ] |
---|
| 636 | | >memb_append_l2 // @IH3 [3: >H // |*: ] |
---|
| 637 | ] |
---|
| 638 | ] |
---|
| 639 | | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l |
---|
| 640 | whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); |
---|
| 641 | #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r |
---|
| 642 | [ >memb_append_l1 | >memb_append_l2 ] // [ @IH1 | @IH2 ] [3,6: >H |*: ] // |
---|
| 643 | | #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????); |
---|
| 644 | whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); |
---|
| 645 | inversion(x == lbl) #Hlbl normalize nodelta |
---|
| 646 | [* >(\P Hlbl) @orb_Prop_l @eq_costlabel_elim // * #H @H % |
---|
| 647 | | #H @orb_Prop_r @IH // |
---|
| 648 | ] |
---|
| 649 | | #lin #io #lout #i1 #IH #x #n #l whd in match (call_post_trans ????); |
---|
| 650 | whd in match (get_labels_of_code ??); #H @orb_Prop_r @orb_Prop_r @IH // |
---|
| 651 | ] |
---|
| 652 | qed. |
---|
[3401] | 653 | |
---|
[3549] | 654 | lemma lab_map_in_domain: ∀p,l_p.∀i: Instructions p l_p. |
---|
[3401] | 655 | ∀x,n,l. |
---|
[3549] | 656 | x ∈ domain_of_associative_list … (lab_map … (call_post_trans … i n l)) → |
---|
[3401] | 657 | x ∈ get_labels_of_code … i. |
---|
[3549] | 658 | #p #l_p #i elim i // |
---|
[3402] | 659 | [ #seq * [|#lbl] #i1 #IH #x #n #l whd in match(call_post_trans ????); |
---|
| 660 | whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); |
---|
| 661 | inversion(x==lbl) #Hlbl normalize nodelta [#_ whd in match (memb ???); >Hlbl % ] |
---|
| 662 | #H >memb_cons // @IH // |
---|
| 663 | | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l |
---|
| 664 | whd in match (call_post_trans ????); whd in match (memb ???); |
---|
| 665 | whd in match (get_labels_of_code ??); inversion(x == ltrue) #Hlbl normalize nodelta |
---|
| 666 | [ #_ whd in match (memb ???); >Hlbl % ] whd in match (memb ???); |
---|
| 667 | inversion(x == lfalse) #Hlbl1 normalize nodelta |
---|
| 668 | [ #_ whd in match (memb ???); >Hlbl normalize nodelta whd in match (memb ???); |
---|
| 669 | >Hlbl1 % ] #H >memb_cons // >memb_cons // >domain_of_associative_list_append in H; |
---|
| 670 | #H cases(memb_append … H) [ #H1 >memb_append_l1 // @IH1 [3: >H1 // |*:] ] |
---|
| 671 | >domain_of_associative_list_append #H1 cases(memb_append … H1) |
---|
| 672 | #H2 >memb_append_l2 // [ >memb_append_l1 | >memb_append_l2 ] // |
---|
| 673 | [ @IH2 | @IH3] /2 by eq_true_to_b/ |
---|
| 674 | | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l whd in match (call_post_trans ????); |
---|
| 675 | whd in match (get_labels_of_code ??); whd in match (memb ???); inversion(x == lfalse) |
---|
| 676 | #Hlfalse normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlfalse // ] |
---|
| 677 | whd in match (memb ???); inversion(x==ltrue) normalize nodelta #Hltrue |
---|
| 678 | [ #_ whd in match (memb ???); >Hltrue %] >domain_of_associative_list_append #H |
---|
| 679 | cases(memb_append … H) #H1 >memb_cons // >memb_cons // [ >memb_append_l1 | >memb_append_l2 ] |
---|
| 680 | // [ @IH1 | @IH2] /2/ |
---|
| 681 | | #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????); |
---|
| 682 | whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); inversion (x == lbl) |
---|
| 683 | #Hlbl normalize nodelta [ #_ whd in match (memb ???); >Hlbl % ] #H >memb_cons // @IH /2/ |
---|
| 684 | | #lin #io #lout #i1 #IH #x #n #l whd in match (memb ???); inversion(x == lout) #Hlout |
---|
| 685 | normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlout % ] |
---|
| 686 | whd in match (memb ???); inversion(x==lin) #Hlin normalize nodelta |
---|
| 687 | [ #_ whd in match (memb ???); >Hlin % ] #H >memb_cons // >memb_cons // @IH /2/ |
---|
| 688 | ] |
---|
[3401] | 689 | qed. |
---|
| 690 | |
---|
[3549] | 691 | let rec is_fresh_for_return (p : label_params) (keep : list (CostLabel p)) (n : p) on keep : Prop ≝ |
---|
[3414] | 692 | match keep with |
---|
| 693 | [ nil ⇒ True |
---|
[3549] | 694 | | cons x xs ⇒ let ih ≝ is_fresh_for_return … xs n in |
---|
[3414] | 695 | match x with |
---|
[3549] | 696 | [ a_return_post y ⇒ match y with [a_return_cost_label m ⇒ m ⊑^{p} n ∧ ih ] |
---|
[3416] | 697 | | _ ⇒ ih |
---|
| 698 | ] |
---|
[3414] | 699 | ]. |
---|
| 700 | |
---|
[3549] | 701 | lemma fresh_ok_call_post_trans : ∀p : instr_params.∀l_p.∀i1 : Instructions p l_p.∀n : l_p.∀l. |
---|
| 702 | n ⊑^{l_p} fresh … (call_post_trans … i1 n l). |
---|
| 703 | #p #l_p #i1 elim i1 normalize /2 by trans_po_rel, refl_po_rel/ |
---|
[3414] | 704 | [ #seq * [|#lbl] #i2 #IH #n #l normalize /2 by / |
---|
| 705 | | #cond #ltrue #i_true #lfalse #i_false #i2 #IH1 #IH2 #IH3 #n #l |
---|
[3549] | 706 | @(trans_po_rel … (IH3 …)) [2: @(trans_po_rel … (IH2 …)) [2: @(trans_po_rel … (IH1 …)) ]] // |
---|
| 707 | | #f #act_p * [|#lbl] normalize #i2 #IH /2 by / #n #l @(trans_po_rel … (IH … l …)) @lab_po_rel_succ |
---|
[3414] | 708 | ] |
---|
| 709 | qed. |
---|
| 710 | |
---|
[3549] | 711 | lemma fresh_keep_n_ok : ∀p : label_params.∀n,m.∀l. |
---|
| 712 | is_fresh_for_return p l n → n ⊑^{p} m → is_fresh_for_return p l m. |
---|
| 713 | #p #n #m #l lapply n -n lapply m -m elim l // * |
---|
[3478] | 714 | [1,2,3: * #x] #xs #IH #n #m |
---|
[3549] | 715 | normalize [2: * #H1] #H2 #H3 [ %] /2 by trans_po_rel/ @(IH … H2) assumption |
---|
[3414] | 716 | qed. |
---|
| 717 | |
---|
[3549] | 718 | definition cast_return_to_cost_labels ≝ λp.map … (a_return_post p …). |
---|
[3416] | 719 | coercion cast_return_to_cost_labels. |
---|
| 720 | |
---|
[3549] | 721 | lemma succ_label_leq_absurd : ∀p : label_params.∀x : p.succ_label … p … x ⊑^{p} x → False. |
---|
| 722 | #p #x #ABS @(absurd ?? (no_maps_in_id … p x)) @(antisym_po_rel … (po_label … p)) // |
---|
| 723 | qed. |
---|
| 724 | |
---|
| 725 | lemma fresh_false : ∀p.∀n.∀l: list (ReturnPostCostLabel p).is_fresh_for_return … l n → |
---|
| 726 | a_return_cost_label p (succ_label … n) ∈ l = false. |
---|
| 727 | #p #n #l lapply n -n elim l // * #x #xs #IH #n whd in ⊢ (% → ??%?); * #H1 |
---|
[3416] | 728 | #H2 @eq_return_cost_lab_elim |
---|
[3549] | 729 | [ #EQ destruct @⊥ @succ_label_leq_absurd // |
---|
[3414] | 730 | | #_ >IH // |
---|
| 731 | ] |
---|
| 732 | qed. |
---|
| 733 | |
---|
[3549] | 734 | lemma inverse_call_post_trans : ∀p : instr_params.∀l_p : label_params.∀i1 : Instructions p l_p.∀n : l_p. |
---|
[3400] | 735 | let dom ≝ get_labels_of_code … i1 in |
---|
| 736 | no_duplicates … dom → |
---|
[3399] | 737 | ∀m,keep. |
---|
[3549] | 738 | ∀info,l.call_post_trans … i1 n l = info → |
---|
| 739 | same_fresh_map_on … dom (lab_map … info) m → |
---|
| 740 | same_to_keep_on … dom (lab_to_keep … info) keep → |
---|
| 741 | is_fresh_for_return … keep n → |
---|
| 742 | call_post_clean … (t_code … info) m keep l |
---|
[3396] | 743 | = return 〈gen_labels … info,i1〉. |
---|
[3549] | 744 | #p #l_p #i1 elim i1 |
---|
[3400] | 745 | [ #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); |
---|
| 746 | #EQ destruct(EQ) // |
---|
| 747 | | #x #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); |
---|
| 748 | #EQ destruct(EQ) // |
---|
| 749 | | #seq * [|#lbl] #instr #IH #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep |
---|
[3414] | 750 | #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%%); normalize nodelta |
---|
[3400] | 751 | >IH // |
---|
| 752 | [1,4: whd whd in H2; #x #Hx @H2 whd in match (get_labels_of_code ??); // |
---|
| 753 | |2,5: whd whd in H1; #x #Hx [ @H1 // ] cases no_dup #H3 #_ <H1 |
---|
| 754 | [2: whd in match (get_labels_of_code ??); @orb_Prop_r // ] |
---|
| 755 | whd in ⊢ (???%); cases(eqb_true … x lbl) inversion(x == lbl) normalize nodelta |
---|
| 756 | [2: //] #_ #H4 >H4 in Hx; // #H5 >H5 in H3; * #ABS @⊥ @ABS % |
---|
| 757 | |6: cases no_dup // |
---|
| 758 | ] |
---|
| 759 | normalize nodelta <(H1 lbl) |
---|
[3549] | 760 | [2: whd in match (get_labels_of_code ??); @orb_Prop_l cases(eqb_true … (a_non_functional_label … lbl) lbl) |
---|
[3400] | 761 | #H3 #H4 >H4 % ] |
---|
| 762 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
| 763 | >(\b (refl …)) % |
---|
| 764 | | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #n normalize nodelta |
---|
| 765 | #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); |
---|
[3414] | 766 | #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%?); >IH3 // |
---|
[3403] | 767 | [2: whd in match (get_labels_of_code ??) in H2; |
---|
| 768 | change with ([?;?]@?) in match (?::?) in H2; |
---|
| 769 | <associative_append in H2; <associative_append |
---|
[3549] | 770 | <(append_nil … (?@?)) <associative_append in ⊢ (???%? → ?); |
---|
| 771 | <(append_nil … (?@?)) in ⊢ (???%? → ?); >associative_append |
---|
| 772 | >associative_append in ⊢ (???%? → ?); #H2 |
---|
[3403] | 773 | @(same_to_keep_on_append … H2) // [ >append_nil |
---|
| 774 | whd in ⊢ (??%); whd in no_dup:(??%); >associative_append // ] |
---|
| 775 | #x #Hx cases (memb_append … Hx) -Hx #Hx @orb_Prop_r @orb_Prop_r |
---|
| 776 | [ >memb_append_l1 | >memb_append_l2 ] // |
---|
| 777 | @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |
---|
| 778 | |3: -H2 whd in match (get_labels_of_code ??) in H1; |
---|
| 779 | change with ([?;?]@?) in match (?::?) in H1; |
---|
| 780 | <associative_append in H1; <associative_append |
---|
| 781 | <(append_nil … (?@?)) >associative_append |
---|
[3549] | 782 | change with ([?;?]@?) in match (?::?::?) in ⊢ (???%? → ?); |
---|
| 783 | <associative_append in ⊢ (???%? → ?); |
---|
| 784 | <associative_append in ⊢ (???%? → ?); |
---|
| 785 | <(append_nil … (?@?)) in ⊢ (???%? → ?); |
---|
| 786 | >associative_append in ⊢ (???%? → ?); #H1 |
---|
[3403] | 787 | @(same_fresh_map_on_append … H1) // |
---|
| 788 | [ >append_nil >associative_append // ] |
---|
| 789 | #x whd in match (memb ???); inversion(x == ltrue) |
---|
| 790 | [ #Hltrue normalize nodelta #_ whd in match (memb ???); >Hltrue % |
---|
| 791 | | #Hltrue normalize nodelta whd in match (memb ???); inversion(x == lfalse) |
---|
| 792 | [ #Hlfalse #_ @orb_Prop_r @orb_Prop_l >Hlfalse % |
---|
| 793 | | #Hlfalse normalize nodelta #Hx @orb_Prop_r @orb_Prop_r |
---|
| 794 | >domain_of_associative_list_append in Hx; #H |
---|
| 795 | cases(memb_append … H) #H2 [ >memb_append_l1 | >memb_append_l2 ] |
---|
| 796 | // @(lab_map_in_domain … (eq_true_to_b … H2)) |
---|
[3400] | 797 | ] |
---|
[3403] | 798 | ] |
---|
[3400] | 799 | |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |] |
---|
| 800 | ] |
---|
[3414] | 801 | normalize nodelta >IH2 |
---|
| 802 | [5: % |
---|
| 803 | |2: /2 by fresh_keep_n_ok/ |
---|
| 804 | |3: whd in match (get_labels_of_code ??) in H2; |
---|
[3403] | 805 | change with ([?;?]@?) in match (?::?) in H2; |
---|
| 806 | <associative_append in H2; #H2 |
---|
| 807 | @(same_to_keep_on_append … H2) // #x #Hx [ @orb_Prop_r @orb_Prop_r ] |
---|
| 808 | @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |
---|
[3414] | 809 | |4: whd in match (get_labels_of_code ??) in H1; |
---|
[3403] | 810 | change with ([?;?]@?) in match (?::?) in H1; |
---|
[3549] | 811 | change with ([?;?]@?) in match (?::?::?) in H1 : (???%?); |
---|
| 812 | <associative_append in H1; <associative_append in ⊢ (???%? → ?); #H1 |
---|
[3403] | 813 | @(same_fresh_map_on_append … H1) // [2: /2 by lab_map_in_domain/ ] |
---|
| 814 | #x >domain_of_associative_list_append #H cases(memb_append … H) |
---|
| 815 | [ whd in ⊢ (??%? → ?%); cases(x == ltrue) // normalize nodelta |
---|
| 816 | whd in ⊢ (??%? → ?%); cases(x == lfalse) // normalize nodelta |
---|
| 817 | normalize #EQ destruct |
---|
| 818 | | #H1 @orb_Prop_r @orb_Prop_r |
---|
| 819 | @(lab_map_in_domain … (eq_true_to_b … H1)) |
---|
| 820 | ] |
---|
[3414] | 821 | |6: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l |
---|
| 822 | |*: |
---|
[3400] | 823 | ] |
---|
[3414] | 824 | >m_return_bind >IH1 |
---|
| 825 | [5: % |
---|
| 826 | |2: /3 by fresh_keep_n_ok/ |
---|
| 827 | |3: whd in match (get_labels_of_code ??) in H2; |
---|
[3403] | 828 | change with ([?;?]@?) in match (?::?) in H2; |
---|
[3549] | 829 | change with ([ ] @ ?) in match (lab_to_keep ???) in H2; |
---|
| 830 | >associative_append in H2 : (???%?); #H2 |
---|
[3414] | 831 | @(same_to_keep_on_append … H2) // #x #Hx cases(memb_append … Hx) |
---|
[3403] | 832 | -Hx #Hx [ >memb_append_l1 | >memb_append_l2] // |
---|
| 833 | @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |
---|
[3414] | 834 | |4: whd in match (get_labels_of_code ??) in H1; |
---|
[3403] | 835 | change with ([?;?]@?) in match (?::?) in H1; |
---|
[3549] | 836 | change with ([?;?]@?) in match (?::?::?) in H1 : (???%?); |
---|
[3403] | 837 | @(same_fresh_map_on_append … H1) // #x >domain_of_associative_list_append |
---|
| 838 | #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2 ] |
---|
| 839 | // @(lab_map_in_domain … (eq_true_to_b … Hx)) |
---|
[3414] | 840 | |6: cases no_dup #_ * #_ @no_duplicates_append_l |
---|
| 841 | |*: |
---|
[3401] | 842 | ] |
---|
[3400] | 843 | >m_return_bind normalize nodelta whd in H1; <H1 |
---|
| 844 | [2: whd in match (get_labels_of_code ??); whd in match (memb ???); |
---|
| 845 | >(\b (refl …)) % ] whd in match (get_element ????); >(\b (refl …)) |
---|
| 846 | normalize nodelta >(\b (refl …)) <H1 |
---|
| 847 | [2: whd in match (get_labels_of_code ??); >memb_cons // |
---|
| 848 | whd in match (memb ???); >(\b (refl …)) % ] |
---|
| 849 | whd in match (get_element ????); @eq_costlabel_elim normalize nodelta |
---|
[3404] | 850 | [ #ABS @⊥ cases no_dup >ABS * #H #_ @H @orb_Prop_l |
---|
[3549] | 851 | >(\b (refl ? (a_non_functional_label … ltrue))) % ] #_ |
---|
[3404] | 852 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
[3414] | 853 | >(\b (refl …)) % |
---|
[3406] | 854 | | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?); |
---|
[3414] | 855 | #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on #f_k |
---|
| 856 | whd in ⊢ (??%?); >(IH2 … (refl …)) |
---|
| 857 | [ normalize nodelta >(IH1 … (refl …)) |
---|
[3406] | 858 | [ >m_return_bind <fresh_map [2: @orb_Prop_l >(\b (refl …)) % ] |
---|
| 859 | whd in match (get_element ????); |
---|
[3549] | 860 | inversion(a_non_functional_label … ltrue == a_non_functional_label … lfalse) |
---|
[3406] | 861 | #Hltrue normalize nodelta |
---|
| 862 | [ cases no_dup whd in match (memb ???); |
---|
[3549] | 863 | cases(eqb_true … (a_non_functional_label … ltrue) (a_non_functional_label … lfalse)) |
---|
[3406] | 864 | #H1 #_ lapply(H1 Hltrue) #EQ destruct(EQ) >(\b (refl …)) * #ABS @⊥ @ABS % ] |
---|
| 865 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …)) |
---|
| 866 | <fresh_map [2: @orb_Prop_r @orb_Prop_l >(\b (refl …)) % ] |
---|
| 867 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
| 868 | >(\b (refl …)) % |
---|
[3414] | 869 | | /2 by fresh_keep_n_ok/ |
---|
[3549] | 870 | | change with ([?;?]@?@?) in keep_on : (??%??); change with ((nil ?) @ ? @ ?) in keep_on : (???%?); |
---|
[3414] | 871 | @(same_to_keep_on_append … keep_on) // #x /2 by lab_to_keep_in_domain/ |
---|
[3549] | 872 | | change with ([?;?]@?@?) in fresh_map : (??%%?); @(same_fresh_map_on_append … fresh_map) |
---|
[3406] | 873 | /2 by lab_map_in_domain/ #x whd in match (memb ???); inversion(x==lfalse) #Hlfalse |
---|
| 874 | normalize nodelta |
---|
| 875 | [ #_ @orb_Prop_r whd in match (memb ???); >Hlfalse % |
---|
| 876 | | whd in match (memb ???); inversion(x==ltrue) #Hltrue normalize nodelta [2: *] #_ |
---|
| 877 | @orb_Prop_l >Hltrue % |
---|
| 878 | ] |
---|
| 879 | | cases no_dup #_ * #_ /2/ |
---|
| 880 | ] |
---|
[3414] | 881 | | // |
---|
[3549] | 882 | | change with ([?;?]@?@?) in keep_on : (??%??); <associative_append in keep_on; |
---|
| 883 | <(append_nil … (?@?)) <(append_nil … (?@?)) in ⊢ (???%? → ?); |
---|
| 884 | >associative_append in ⊢ (??%%? → ?); >associative_append in ⊢ (???%? → ?); |
---|
[3408] | 885 | #keep_on @(same_to_keep_on_append … keep_on) // |
---|
| 886 | [ >associative_append >append_nil // |
---|
| 887 | | #x #Hx @orb_Prop_r @orb_Prop_r /2 by lab_to_keep_in_domain/ |
---|
| 888 | ] |
---|
[3549] | 889 | | change with ([?;?]@?@?) in fresh_map : (??%??); <associative_append in fresh_map; |
---|
| 890 | <(append_nil … (?@?)) change with ([?;?]@?@?) in ⊢ (???%? → ?); |
---|
| 891 | <associative_append in ⊢ (???%? → ?); <(append_nil … (?@?)) in ⊢ (???%? → ?); |
---|
| 892 | >associative_append in ⊢ (??%%? → ?); >associative_append in ⊢ (???%? → ?); |
---|
[3408] | 893 | #fresh_map @(same_fresh_map_on_append … fresh_map) // |
---|
| 894 | [ >append_nil // |
---|
| 895 | | #x >domain_of_associative_list_append #Hx cases(memb_append … Hx) |
---|
| 896 | [2: #Hx1 @orb_Prop_r @orb_Prop_r @(lab_map_in_domain … (eq_true_to_b … Hx1)) ] |
---|
| 897 | whd in match (memb ???); inversion(x == lfalse) normalize nodelta #Hlfalse |
---|
| 898 | [ #_ @orb_Prop_r @orb_Prop_l >Hlfalse % |
---|
| 899 | | whd in match (memb ???); inversion (x==ltrue) normalize nodelta #Hltrue |
---|
| 900 | [ #_ @orb_Prop_l >Hltrue % |
---|
| 901 | | whd in match (memb ???); #EQ destruct |
---|
| 902 | ] |
---|
| 903 | ] |
---|
| 904 | ] |
---|
| 905 | | cases no_dup #_ * #_ /2 by no_duplicates_append_r/ |
---|
| 906 | ] |
---|
[3410] | 907 | | #f #act_p * [|#r_lb] #i #IH #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?); |
---|
[3414] | 908 | #EQ destruct(EQ) #fresh_map #same_keep #f_k whd in ⊢ (??%?); |
---|
| 909 | >(IH … (refl …)) |
---|
| 910 | [1,6: normalize nodelta |
---|
[3416] | 911 | [ >fresh_false [2: /2 by fresh_keep_n_ok/] % |
---|
[3414] | 912 | | <same_keep |
---|
| 913 | [ whd in match (memb ???); >(\b (refl …)) normalize nodelta |
---|
| 914 | <fresh_map |
---|
| 915 | [ whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
| 916 | >(\b (refl …)) % |
---|
| 917 | | whd in match (memb ???); >(\b (refl …)) % |
---|
| 918 | ] |
---|
| 919 | | whd in match (memb ???); >(\b (refl …)) % |
---|
| 920 | ] |
---|
| 921 | ] |
---|
| 922 | |2,7: // |
---|
[3549] | 923 | |3,8: whd in match (get_labels_of_code ???) in same_keep; // #x #Hx <same_keep |
---|
[3414] | 924 | [2: >memb_cons // >Hx // ] cases no_dup * #ABS #_ whd in ⊢ (???%); |
---|
| 925 | inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) >Hx // |
---|
[3549] | 926 | |4,9: whd in match (get_labels_of_code ???) in fresh_map; // #x #Hx <fresh_map |
---|
[3414] | 927 | [2: >memb_cons // >Hx //] cases no_dup * #ABS #_ whd in ⊢ (???%); |
---|
| 928 | inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) // |
---|
| 929 | |5,10: [ @no_dup | cases no_dup // ] |
---|
| 930 | ] |
---|
[3549] | 931 | | #lin #io #lout #i #IH #n whd in match (get_labels_of_code ???); #no_dup |
---|
[3414] | 932 | #m #keep #info #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #fresh_map #same_keep |
---|
| 933 | #f_k whd in ⊢ (??%?); >(IH … (refl …)) |
---|
| 934 | [ normalize nodelta <fresh_map [2: >memb_cons // >memb_hd // ] |
---|
| 935 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
| 936 | >(\b (refl …)) <fresh_map [2: >memb_hd //] whd in match (get_element ????); |
---|
| 937 | inversion(lin==lout) |
---|
| 938 | [ #ABS @⊥ cases no_dup * #ABS1 #_ @ABS1 whd in match (memb ???); >(\P ABS) |
---|
| 939 | >(\b (refl …)) // |
---|
[3549] | 940 | | #H inversion (a_non_functional_label … lin== ? lout) |
---|
[3414] | 941 | [ #ABS lapply(\P ABS) #EQ destruct >(\b (refl …)) in H; #EQ destruct |
---|
| 942 | | #_ normalize nodelta whd in match (get_element ????); >(\b (refl …)) |
---|
| 943 | normalize nodelta >(\b (refl …)) % |
---|
| 944 | ] |
---|
| 945 | ] |
---|
| 946 | | // |
---|
| 947 | | #x #Hx >same_keep [2: >memb_cons // >memb_cons // >Hx % ] % |
---|
| 948 | | #x #Hx <fresh_map [2: >memb_cons // >memb_cons // >Hx %] |
---|
| 949 | cases no_dup * #ABS1 ** #ABS2 #_ whd in ⊢ (???%); inversion(x == lout) |
---|
| 950 | normalize nodelta |
---|
| 951 | [2: #_ whd in ⊢ (???%); inversion(x==lin) normalize nodelta // |
---|
| 952 | #H @⊥ @ABS1 >memb_cons // <(\P H) >Hx // |
---|
| 953 | | #H @⊥ @ABS2 <(\P H) >Hx // |
---|
| 954 | ] |
---|
| 955 | | cases no_dup #_ * #_ // |
---|
| 956 | ] |
---|
[3408] | 957 | ] |
---|
[3416] | 958 | qed. |
---|
[3396] | 959 | |
---|
[3549] | 960 | definition fresh_for_prog_aux : ∀p,p',l_p.Program p p' l_p → l_p → l_p ≝ |
---|
| 961 | λp,p',l_p,prog,n.foldl … (λn,i.op … l_p … n (compute_max_n … (f_body … i))) n (env … prog). |
---|
[3445] | 962 | |
---|
| 963 | |
---|
[3549] | 964 | lemma fresh_aux_ok : ∀p,p',l_p.∀prog : Program p p' l_p.∀n,m.n ⊑^{l_p} m → |
---|
| 965 | fresh_for_prog_aux … prog n ⊑^{l_p} fresh_for_prog_aux … prog m. |
---|
| 966 | #p #p' #l_p * #env #main elim env // #hd #tl #IH #n #m #H whd in ⊢ (???%%); |
---|
| 967 | @IH whd in ⊢ (???%?); @(monotonic_magg … l_p … H) |
---|
[3445] | 968 | qed. |
---|
| 969 | |
---|
[3549] | 970 | definition fresh_for_prog : ∀p,p',l_p.Program p p' l_p → l_p ≝ |
---|
| 971 | λp,p',l_p,prog.fresh_for_prog_aux … prog |
---|
[3445] | 972 | (compute_max_n … (main … prog)). |
---|
[3400] | 973 | |
---|
[3416] | 974 | definition translate_env ≝ |
---|
[3549] | 975 | λp,p',l_p.λenv : list (env_item p p' l_p).λmax_all.(foldr ?? |
---|
[3396] | 976 | (λi,x.let 〈t_env,n,m,keep〉 ≝ x in |
---|
| 977 | let info ≝ call_post_trans … (f_body … i) n (nil ?) in |
---|
[3549] | 978 | 〈(mk_env_item ??? |
---|
[3397] | 979 | (mk_signature ??(f_name ?? i) (f_pars … i) (f_ret … i)) |
---|
[3400] | 980 | (f_lab … i) (t_code … info)) :: t_env, |
---|
[3549] | 981 | fresh … info, 〈a_call … (f_lab … i),(a_call … (f_lab … i)) :: (gen_labels ?? info)〉 :: |
---|
[3396] | 982 | ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉) |
---|
[3416] | 983 | (〈nil ?,max_all,nil ?,nil ?〉) env). |
---|
[3396] | 984 | |
---|
[3549] | 985 | definition trans_prog : ∀p,p',l_p.Program p p' l_p → |
---|
| 986 | ((Program p p' l_p) × (associative_list (DEQCostLabel l_p) (CostLabel l_p)) × ((list (ReturnPostCostLabel l_p))))≝ |
---|
| 987 | λp,p',l_p,prog. |
---|
[3416] | 988 | let max_all ≝ fresh_for_prog … prog in |
---|
| 989 | let info_main ≝ (call_post_trans … (main … prog) max_all (nil ?)) in |
---|
| 990 | let 〈t_env,n,m,keep〉 ≝ translate_env … (env … prog) (fresh … info_main) in |
---|
[3549] | 991 | 〈mk_Program ??? t_env (t_code … info_main),m @ (lab_map … info_main),keep @ (lab_to_keep … info_main)〉. |
---|
[3416] | 992 | |
---|
[3549] | 993 | definition map_labels_on_trace : ∀p : label_params. |
---|
| 994 | (associative_list (DEQCostLabel p) (CostLabel p)) → list (CostLabel p) → list (CostLabel p) ≝ |
---|
| 995 | λp,m,l.foldr … (λlab,t.(get_element … m lab) @ t) (nil ?) l. |
---|
[3396] | 996 | |
---|
| 997 | lemma map_labels_on_trace_append: |
---|
[3549] | 998 | ∀p,m,l1,l2. map_labels_on_trace p m (l1@l2) = |
---|
| 999 | map_labels_on_trace p m l1 @ map_labels_on_trace p m l2. |
---|
| 1000 | #p #m #l1 elim l1 // #hd #tl #IH #l2 >associative_append <IH // |
---|
[3396] | 1001 | qed. |
---|
| 1002 | |
---|
[3397] | 1003 | include "../src/common/Errors.ma". |
---|
[3527] | 1004 | include "Permutation.ma". |
---|
[3397] | 1005 | |
---|
[3527] | 1006 | (* |
---|
| 1007 | |
---|
[3399] | 1008 | axiom is_permutation: ∀A.list A → list A → Prop. |
---|
| 1009 | axiom is_permutation_eq : ∀A.∀l : list A.is_permutation … l l. |
---|
| 1010 | axiom is_permutation_cons : ∀A.∀l1,l2,x.is_permutation A l1 l2 → |
---|
| 1011 | is_permutation A (x :: l1) (x :: l2). |
---|
[3527] | 1012 | *) |
---|
[3399] | 1013 | (* |
---|
| 1014 | inductive is_permutation (A : Type[0]) : list A → list A → Prop ≝ |
---|
| 1015 | | p_empty : is_permutation A (nil ?) (nil ?) |
---|
| 1016 | | p_append : ∀x,x1,x2,y,y1,y2. |
---|
| 1017 | x = y → is_permutation A (x1 @ x2) (y1 @ y2) → |
---|
| 1018 | is_permutation A (x1 @ [x] @ x2) (y1 @ [y] @ y2). |
---|
| 1019 | |
---|
| 1020 | lemma is_permutation_eq : ∀A.∀l : list A.is_permutation … l l. |
---|
| 1021 | #A #l elim l // #x #xs #IH |
---|
| 1022 | change with ((nil ?) @ (x :: xs)) in ⊢ (??%%); |
---|
| 1023 | >append_cons >associative_append |
---|
| 1024 | @(p_append ? x (nil ?) xs x (nil ?) xs (refl …)) @IH |
---|
| 1025 | qed. |
---|
| 1026 | |
---|
| 1027 | lemma is_permutation_append : ∀A.∀l1,l2,l3,l4 : list A. |
---|
| 1028 | is_permutation A l1 l3 → is_permutation A l2 l4 → |
---|
| 1029 | is_permutation A (l1 @ l2) (l3 @ l4). |
---|
| 1030 | #A #l1 inversion (|l1|) [2: #n lapply l1 elim n |
---|
| 1031 | [ #l2 #l3 #l4 #H inversion H // #x #x1 #x2 #y #y1 #y2 #EQ #H1 #_ |
---|
| 1032 | #ABS cases(nil_to_nil … (sym_eq ??? ABS)) -ABS #_ #ABS |
---|
| 1033 | cases(nil_to_nil … ABS) #EQ1 destruct(EQ1) ] |
---|
| 1034 | #x #xs #IH #l2 #l3 #l4 #H inversion H |
---|
| 1035 | [#EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ) ] |
---|
| 1036 | #y #y1 #y2 #z #z1 #z2 #EQ destruct(EQ) #H1 #_ #EQx_xs #EQ destruct(EQ) #_ |
---|
| 1037 | *) |
---|
| 1038 | |
---|
[3405] | 1039 | |
---|
| 1040 | |
---|
[3549] | 1041 | lemma lookup_ok_append : ∀p,p',l_p,l,f,env_it. |
---|
| 1042 | lookup p p' l_p l f = return env_it → ∃l1,l2. l = l1 @ [env_it] @ l2 ∧ |
---|
[3405] | 1043 | f_name … env_it = f. |
---|
[3549] | 1044 | #p #p' #l_p #l elim l [ #f #env_it normalize #EQ destruct] |
---|
[3405] | 1045 | #x #xs #IH #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim |
---|
| 1046 | [ #EQ destruct(EQ) normalize nodelta whd in ⊢ (???% → ?); #EQ destruct |
---|
| 1047 | %{(nil ?)} %{xs} /2/ |
---|
| 1048 | | #Hno_f normalize nodelta #EQ_env_it cases(IH … EQ_env_it) |
---|
| 1049 | #l1 * #l2 * #EQ1 #EQ2 %{(x :: l1)} %{l2} >EQ1 /2/ |
---|
| 1050 | ] |
---|
| 1051 | qed. |
---|
| 1052 | (* |
---|
| 1053 | lemma foldr_append : |
---|
| 1054 | ∀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. |
---|
| 1055 | #A #B #l1 elim l1 // |
---|
| 1056 | #hd #tl #Hind #l2 #f #seed normalize >Hind @refl |
---|
| 1057 | qed. |
---|
| 1058 | *) |
---|
| 1059 | |
---|
| 1060 | |
---|
| 1061 | |
---|
[3414] | 1062 | (* aggiungere fresh_to_keep al lemma seguente??*) |
---|
[3409] | 1063 | |
---|
[3549] | 1064 | lemma fresh_for_subset : ∀p : label_params.∀l1,l2,n.l1 ⊆ l2 → is_fresh_for_return p … l2 n → |
---|
| 1065 | is_fresh_for_return p … l1 n. |
---|
| 1066 | #p #l1 elim l1 // * [1,2,3: * #x] #xs #IH #l2 #n * #H1 #H2 #H3 whd |
---|
[3416] | 1067 | try(@IH) // % [2: @IH //] elim l2 in H1 H3; normalize [*] |
---|
[3478] | 1068 | * [1,2,3: * #y] #ys #IH normalize |
---|
[3416] | 1069 | [2,3: * [2,4: #H3 [2: @IH //] * #H4 #H5 @IH // |
---|
| 1070 | |*: #EQ destruct * // |
---|
| 1071 | ]] |
---|
| 1072 | * |
---|
[3478] | 1073 | [1,3: #EQ destruct ] #H3 #H4 @IH // |
---|
[3416] | 1074 | qed. |
---|
| 1075 | |
---|
[3549] | 1076 | lemma fresh_append : ∀p.∀n,l1,l2.is_fresh_for_return p l1 n → is_fresh_for_return p l2 n → |
---|
| 1077 | is_fresh_for_return p (l1@l2) n. |
---|
| 1078 | #p #n #l1 lapply n -n elim l1 // * [1,2,3: * #x] #xs #IH #n #l2 [2: * #H1 ] #H2 #H3 |
---|
[3416] | 1079 | [ % // @IH //] @IH // |
---|
| 1080 | qed. |
---|
| 1081 | |
---|
[3549] | 1082 | definition labels_of_prog : ∀p,p',l_p.Program p p' l_p → ? ≝ |
---|
| 1083 | λp,p',l_p,prog.foldr … (λx,l.l @ (get_labels_of_code … (f_body … x))) |
---|
[3445] | 1084 | (get_labels_of_code … (main … prog)) (env … prog). |
---|
[3416] | 1085 | |
---|
[3549] | 1086 | lemma cast_return_append : ∀p.∀l1,l2.cast_return_to_cost_labels p … (l1 @ l2) = |
---|
| 1087 | (cast_return_to_cost_labels p … l1) @ (cast_return_to_cost_labels p … l2). |
---|
| 1088 | #p #l1 #l2 @(sym_eq … (map_append …)) qed. |
---|
[3416] | 1089 | |
---|
[3445] | 1090 | include alias "arithmetics/nat.ma". |
---|
| 1091 | |
---|
| 1092 | |
---|
[3549] | 1093 | lemma is_fresh_code : ∀p,l_p.∀i : Instructions p l_p. |
---|
| 1094 | is_fresh_for_return l_p (get_labels_of_code … i) (compute_max_n … i). |
---|
| 1095 | #p #l_p #main elim main // |
---|
| 1096 | [ #seq * [| * #lbl] #i #IH normalize // @(fresh_keep_n_ok … IH) // |
---|
| 1097 | | #cond * #ltrue #i1 * #lfalse #i2 #i3 #IH1 #IH2 #IH3 whd in ⊢ (??%%); |
---|
[3445] | 1098 | @fresh_append |
---|
[3549] | 1099 | [ @(fresh_keep_n_ok … IH1) @max_1 @max_1 @max_1 @max_1 // |
---|
[3445] | 1100 | | @fresh_append |
---|
[3549] | 1101 | [ @(fresh_keep_n_ok … IH2) @max_1 @max_1 @max_1 @max_2 // |
---|
| 1102 | | @(fresh_keep_n_ok … IH3) @max_1 @max_1 @max_2 // |
---|
[3445] | 1103 | ] |
---|
| 1104 | ] |
---|
[3549] | 1105 | | #cond * #ltrue #i1 * #lfalse #i2 #IH1 #IH2 whd in ⊢ (??%%); @fresh_append |
---|
| 1106 | [ @(fresh_keep_n_ok … IH1) @max_1 @max_1 @max_1 // |
---|
| 1107 | | @(fresh_keep_n_ok … IH2) @max_1 @max_1 @max_2 // |
---|
[3445] | 1108 | ] |
---|
[3549] | 1109 | | #f #act_p * [| * #lbl] #i #IH whd in ⊢ (??%%); // |
---|
| 1110 | change with ([?]@?) in ⊢ (??%?); @fresh_append |
---|
| 1111 | [ whd % // |
---|
| 1112 | | @(fresh_keep_n_ok … IH) @max_2 // |
---|
[3445] | 1113 | ] |
---|
[3549] | 1114 | | * #lin #io * #lout #i #IH whd in ⊢ (??%%); @(fresh_keep_n_ok … IH) |
---|
| 1115 | @max_1 @max_1 // |
---|
[3445] | 1116 | ] |
---|
| 1117 | qed. |
---|
| 1118 | |
---|
[3549] | 1119 | lemma is_fresh_fresh_for_prog : ∀p,p',l_p.∀prog : Program p p' l_p. |
---|
| 1120 | is_fresh_for_return … (labels_of_prog … prog) (fresh_for_prog … prog). |
---|
| 1121 | #p #p' #l_p * #env #main whd in match fresh_for_prog; normalize nodelta whd in ⊢ (??%?); |
---|
| 1122 | elim env // * #sig #cost #i #tail #IH whd in ⊢ (??%?); @fresh_append |
---|
[3445] | 1123 | [ @(fresh_keep_n_ok … IH) @fresh_aux_ok @max_1 // |
---|
| 1124 | | @(fresh_keep_n_ok … (is_fresh_code … i)) whd in match fresh_for_prog_aux; normalize nodelta |
---|
[3549] | 1125 | whd in ⊢ (????%); elim tail [ @max_2 // ] #hd1 #tl1 #IH1 @(trans_po_rel … IH1) |
---|
| 1126 | whd in ⊢ (????%); change with (fresh_for_prog_aux ??? (mk_Program ??? tl1 main) ?) in ⊢ (???%%); |
---|
[3445] | 1127 | @fresh_aux_ok @max_1 // |
---|
| 1128 | ] |
---|
| 1129 | qed. |
---|
| 1130 | |
---|
[3549] | 1131 | lemma memb_cast_return : ∀p.∀keep,x.x ∈ cast_return_to_cost_labels p keep → |
---|
| 1132 | ∃ y.x = a_return_post … y ∧ bool_to_Prop (y ∈ keep). |
---|
| 1133 | #p #keep elim keep |
---|
[3445] | 1134 | [ #x *] #x #xs #IH #y whd in match cast_return_to_cost_labels; |
---|
| 1135 | whd in match (map ????); whd in match (memb ???); inversion(y==x) |
---|
| 1136 | [ #Hx #_ %{x} >(\P Hx) %{(refl …)} >memb_hd // |
---|
| 1137 | | #Hx normalize nodelta #H cases(IH … H) #z * #H1 #H2 %{z} %{H1} >memb_cons // >H2 // |
---|
| 1138 | ] |
---|
| 1139 | qed. |
---|
| 1140 | |
---|
[3549] | 1141 | lemma lab_to_keep_in_prog : ∀p,p',l_p.∀prog : Program p p' l_p. |
---|
[3445] | 1142 | ∀t_prog,m,keep.trans_prog … prog = 〈t_prog,m,keep〉 → |
---|
[3549] | 1143 | (cast_return_to_cost_labels l_p keep) ⊆ (labels_of_prog p p' l_p prog). |
---|
| 1144 | #p #p' #l_p * #env #main #t_prog #m #keep whd in match trans_prog; normalize nodelta |
---|
[3445] | 1145 | @pair_elim * #env1 #fresh * #m1 #keep1 #EQenv1 normalize nodelta #EQ destruct |
---|
| 1146 | lapply EQenv1 -EQenv1 lapply keep1 -keep1 lapply m1 -m1 lapply fresh -fresh |
---|
[3549] | 1147 | lapply env1 -env1 generalize in match (fresh_for_prog ????); elim env |
---|
[3445] | 1148 | [ #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct whd in match (append ???); |
---|
| 1149 | @subset_def #x #H whd in match (labels_of_prog); normalize nodelta |
---|
| 1150 | whd in match (foldr ?????); cases(memb_cast_return … H) -H #x1 * #EQ1 #H destruct |
---|
| 1151 | @(lab_to_keep_in_domain … H) |
---|
| 1152 | | #x #xs #IH #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); @pair_elim |
---|
| 1153 | * #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail |
---|
[3549] | 1154 | change with (translate_env ?????) in match (foldr ?????); #EQt_env_tail |
---|
[3445] | 1155 | normalize nodelta #EQ1 destruct >cast_return_append @subset_append |
---|
| 1156 | [ >cast_return_append @subset_append |
---|
| 1157 | [ whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); |
---|
| 1158 | @subset_def #y #H cases(memb_cast_return … H) -H #y1 * #EQ destruct #H |
---|
| 1159 | >memb_append_l2 // @(lab_to_keep_in_domain … H) |
---|
| 1160 | | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); |
---|
[3549] | 1161 | change with (labels_of_prog ??? (mk_Program ??? xs ?)) in match (foldr ?????); |
---|
[3445] | 1162 | @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail)) |
---|
| 1163 | >cast_return_append @subset_append_h1 // |
---|
| 1164 | ] |
---|
| 1165 | | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); |
---|
[3549] | 1166 | change with (labels_of_prog ??? (mk_Program ??? xs ?)) in match (foldr ?????); |
---|
[3445] | 1167 | @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail)) |
---|
| 1168 | >cast_return_append @subset_append_h2 // |
---|
| 1169 | ] |
---|
| 1170 | ] |
---|
| 1171 | qed. |
---|
| 1172 | |
---|
[3549] | 1173 | lemma fresh_call_post_trans_ok : ∀p,l_p.∀i : Instructions p l_p.∀n,l. |
---|
| 1174 | n ⊑^{l_p} fresh … (call_post_trans … i n l). |
---|
| 1175 | #p #l_p #i elim i // |
---|
[3445] | 1176 | qed. |
---|
| 1177 | |
---|
[3549] | 1178 | lemma fresh_translate_env_ok : ∀p,p',l_p.∀env,t_env : list (env_item p p' l_p).∀n,n1,m,keep. |
---|
| 1179 | translate_env … env n = 〈t_env,n1,m,keep〉 → n ⊑^{l_p} n1. |
---|
| 1180 | #p #p' #l_p #env elim env |
---|
[3445] | 1181 | [ #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct // ] |
---|
| 1182 | #x #xs #IH #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?); |
---|
[3549] | 1183 | change with (translate_env ?????) in match (foldr ?????); @pair_elim |
---|
[3445] | 1184 | * #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail #EQt_env_tail normalize nodelta |
---|
[3549] | 1185 | #EQ destruct @(trans_po_rel … (IH … EQt_env_tail)) @fresh_call_post_trans_ok |
---|
[3445] | 1186 | qed. |
---|
| 1187 | |
---|
| 1188 | |
---|
[3400] | 1189 | lemma trans_env_ok : ∀p : state_params.∀ prog. |
---|
| 1190 | no_duplicates_labels … prog → |
---|
| 1191 | let 〈t_prog,m,keep〉 ≝ trans_prog … prog in |
---|
[3549] | 1192 | ∀f,env_it.lookup p p p (env … prog) f = return env_it → |
---|
[3416] | 1193 | let dom ≝ get_labels_of_code … (f_body … env_it) in |
---|
[3549] | 1194 | ∃env_it',n.is_fresh_for_return p keep n ∧lookup p p p (env … t_prog) f = return env_it' ∧ |
---|
[3400] | 1195 | let info ≝ call_post_trans … (f_body … env_it) n (nil ?) in |
---|
| 1196 | t_code … info = f_body … env_it' ∧ |
---|
[3549] | 1197 | get_element … m (a_call … (f_lab … env_it')) = (a_call … (f_lab … env_it')) :: gen_labels … info ∧ |
---|
[3400] | 1198 | f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it' ∧ |
---|
[3549] | 1199 | same_fresh_map_on … dom m (lab_map … info) ∧ same_to_keep_on … dom keep (lab_to_keep … info). |
---|
[3416] | 1200 | #p #prog inversion(trans_prog … prog) * #t_prog0 #m0 #keep0 #EQt_prog |
---|
| 1201 | lapply EQt_prog normalize nodelta |
---|
| 1202 | generalize in match keep0 in ⊢ (% → ? → ? → ? → ? → ??(λ_.??(λ_.?%?))); |
---|
| 1203 | #keep1 #EQkeep1 inversion prog in EQt_prog; #env #main #EQprog |
---|
| 1204 | whd in match trans_prog; normalize nodelta |
---|
| 1205 | @pair_elim |
---|
[3549] | 1206 | cut(fresh_for_prog ??? prog ⊑^{p} fresh_for_prog ??? (mk_Program … env main)) [ >EQprog //] |
---|
| 1207 | generalize in match (fresh_for_prog ????) in ⊢ (????% → %); |
---|
[3416] | 1208 | lapply t_prog0 lapply m0 lapply keep0 |
---|
| 1209 | elim env in ⊢ (?→ ? → ? → ? → ? → %); |
---|
| 1210 | [ #keep #m #t_prog #n #_ * #env' #fresh * #x #y #_ #_ #_ #f #env_it normalize in ⊢ (% → ?); #ABS destruct] |
---|
| 1211 | * #hd_sig #hd_lab #hd_code #tail #IH #keep #m #t_prog #fresh1 #Hfresh1 * #env' #fresh * #m' #keep' |
---|
[3400] | 1212 | normalize in ⊢ (% → ?); normalize nodelta @pair_elim * #env_tail #fresh_tail |
---|
[3549] | 1213 | * #m_tail #keep_tail change with (translate_env ?????) in ⊢ (??%? → ?); #EQtail normalize nodelta #EQ1 destruct(EQ1) #EQ2 destruct(EQ2) |
---|
[3400] | 1214 | whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H) |
---|
[3549] | 1215 | change with (no_duplicates_labels p p p (mk_Program p p p tail main)) in match |
---|
| 1216 | (no_duplicates_labels p p p (mk_Program p p p tail main)); #no_dup_tail |
---|
[3400] | 1217 | lapply(no_duplicates_append_l … H) #no_dup_head normalize nodelta |
---|
| 1218 | #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta |
---|
| 1219 | [ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ) |
---|
| 1220 | inversion (call_post_trans … hd_code fresh_tail []) |
---|
| 1221 | #gen_labs #t_hd_code #t_fresh #t_lab_map #t_lab_to_keep #EQ_trans_code |
---|
[3416] | 1222 | %{(mk_env_item … hd_sig hd_lab t_hd_code)} %{fresh_tail} % |
---|
| 1223 | [ % |
---|
| 1224 | [ @(fresh_keep_n_ok … fresh1) |
---|
| 1225 | [ @(fresh_keep_n_ok … Hfresh1) |
---|
| 1226 | @(fresh_for_subset … (labels_of_prog … prog)) |
---|
[3445] | 1227 | [ @(lab_to_keep_in_prog … EQkeep1) | @is_fresh_fresh_for_prog ] |
---|
[3549] | 1228 | | @(trans_po_rel … (fresh_translate_env_ok … EQtail)) // |
---|
[3416] | 1229 | ] |
---|
| 1230 | | whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta |
---|
| 1231 | @eq_f cases hd_sig // ]] >EQ_trans_code % [% [ % [ % [% // whd in ⊢ (??%?); >(\b (refl …)) %] % ] % | whd |
---|
[3405] | 1232 | #x #Hx whd in ⊢ (??%?); >(? : (x == hd_lab) = false) |
---|
| 1233 | [2: inversion(x==hd_lab) // #EQx_hdlab cases Hhd_lab -Hhd_lab #Hhd_lab cases Hhd_lab |
---|
| 1234 | >memb_append_l1 // <(\P EQx_hdlab) >Hx // ] |
---|
[3416] | 1235 | normalize nodelta >get_element_append_l1 |
---|
[3448] | 1236 | [2: % #ABS @(memb_no_duplicates_append … x … H) // elim tail |
---|
| 1237 | [ whd in match (foldr ?????); @lab_map_in_domain // ] |
---|
| 1238 | #x #xs #IH whd in match (foldr ?????); @orb_Prop_r |
---|
| 1239 | >memb_append_l2 // >IH % |
---|
| 1240 | ] @get_element_append_l1 |
---|
[3416] | 1241 | % #H1 |
---|
[3409] | 1242 | (* subproof with no nice statement *) |
---|
| 1243 | lapply H1 -H1 lapply H -H lapply Hhd_lab -Hhd_lab lapply EQtail -EQtail |
---|
[3416] | 1244 | generalize in match fresh1; lapply env_tail -env_tail lapply fresh_tail |
---|
| 1245 | -fresh_tail lapply m_tail -m_tail lapply keep_tail -keep_tail elim tail |
---|
[3409] | 1246 | normalize nodelta |
---|
| 1247 | [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); |
---|
| 1248 | #EQ destruct(EQ) whd in match (foldr ?????); |
---|
| 1249 | #H1 #H2 * ] |
---|
| 1250 | #head #tail #IH #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); |
---|
| 1251 | whd in match (foldr ?????); |
---|
| 1252 | @pair_elim * #env_tail_res #fresh_tail_res * #lab_map_res #keep_res #EQres |
---|
| 1253 | normalize nodelta #EQ destruct(EQ) whd in match (foldr ?????); |
---|
| 1254 | #H1 #H2 whd in match (memb ???); inversion(x == ?) |
---|
| 1255 | [ #H3 #_ <(\P H3) in H2; change with ([?]@?) in match (?::?); #H2 |
---|
| 1256 | lapply(no_duplicates_append_commute … H2) -H2 ** #ABS #_ @ABS |
---|
| 1257 | >memb_append_l2 // >Hx % |
---|
| 1258 | | #H3 normalize nodelta #H4 @(IH … EQres) |
---|
| 1259 | [3: >domain_of_associative_list_append in H4; #H4 cases(memb_append … H4) [2: #EQ >EQ %] |
---|
| 1260 | #ABS @⊥ @(memb_no_duplicates_append … x … H2) // @orb_Prop_r >memb_append_l1 // |
---|
| 1261 | @(lab_map_in_domain … (eq_true_to_b … ABS)) |
---|
| 1262 | | % #ABS elim H1 -H1 #H1 @H1 cases(memb_append … ABS) |
---|
| 1263 | [ #H5 >memb_append_l1 // |
---|
| 1264 | | #H5 >memb_append_l2 // @orb_Prop_r >memb_append_l2 // |
---|
| 1265 | ] |
---|
| 1266 | | lapply(no_duplicates_append_commute … H2) * #_ >associative_append |
---|
| 1267 | #h @no_duplicates_append_commute @(no_duplicates_append_r … h) |
---|
| 1268 | ] |
---|
| 1269 | ] |
---|
| 1270 | ] |
---|
[3448] | 1271 | | whd #x #Hx >memb_append_l12 |
---|
| 1272 | [2: @notb_Prop % #ABS @(memb_no_duplicates_append … H … Hx) elim tail |
---|
| 1273 | [ whd in match (foldr ?????); @lab_to_keep_in_domain // ] |
---|
| 1274 | #x #xs #IH whd in match (foldr ?????); @orb_Prop_r |
---|
| 1275 | >memb_append_l2 // >IH % |
---|
| 1276 | ] |
---|
[3549] | 1277 | >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … (a_return_post … x) … H) |
---|
[3409] | 1278 | // @⊥ |
---|
| 1279 | (* subproof with no nice statement *) |
---|
| 1280 | lapply ABS -ABS lapply H -H lapply Hhd_lab -Hhd_lab lapply EQtail -EQtail |
---|
[3416] | 1281 | generalize in match fresh1; lapply env_tail -env_tail lapply fresh_tail |
---|
| 1282 | -fresh_tail lapply m_tail -m_tail lapply keep_tail -keep_tail elim tail |
---|
[3409] | 1283 | normalize nodelta |
---|
| 1284 | [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); |
---|
| 1285 | #EQ destruct(EQ) whd in match (foldr ?????); |
---|
| 1286 | #H1 #H2 whd in ⊢ (??%? → ?); #EQ destruct ] |
---|
| 1287 | #head #tail #IH #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); |
---|
| 1288 | whd in match (foldr ?????); |
---|
| 1289 | @pair_elim * #env_tail_res #fresh_tail_res * #lab_map_res #keep_res #EQres |
---|
| 1290 | normalize nodelta #EQ destruct(EQ) whd in match (foldr ?????); |
---|
| 1291 | #H1 #H2 #H3 cases(memb_append … H3) -H3 |
---|
| 1292 | [ #H3 change with ([?]@?) in match (?::?) in H2; |
---|
[3549] | 1293 | lapply(no_duplicates_append_commute … H2) -H2 * #_ #H4 @(memb_no_duplicates_append … (a_return_post … x) … H4) |
---|
[3409] | 1294 | [ whd in match (append ???); >memb_append_l1 // >(lab_to_keep_in_domain … (eq_true_to_b … H3)) % |
---|
| 1295 | | // |
---|
| 1296 | ] |
---|
| 1297 | | #H3 normalize nodelta @(IH … EQres) |
---|
| 1298 | [3: // |
---|
| 1299 | | % #ABS elim H1 -H1 #H1 @H1 cases(memb_append … ABS) |
---|
| 1300 | [ #H5 >memb_append_l1 // |
---|
| 1301 | | #H5 >memb_append_l2 // @orb_Prop_r >memb_append_l2 // |
---|
| 1302 | ] |
---|
| 1303 | | lapply(no_duplicates_append_commute … H2) * #_ >associative_append |
---|
| 1304 | #h @no_duplicates_append_commute @(no_duplicates_append_r … h) |
---|
| 1305 | ] |
---|
| 1306 | ] |
---|
[3400] | 1307 | ] |
---|
| 1308 | | #Hf #Henv_it cases(IH … no_dup_tail … Henv_it) |
---|
[3416] | 1309 | [9: >EQtail in ⊢ (??%?); % |
---|
| 1310 | |13: % |
---|
| 1311 | |6: assumption |
---|
| 1312 | |10: % |
---|
[3404] | 1313 | |*: |
---|
| 1314 | ] |
---|
[3416] | 1315 | #new_env_it * #new_fresh ** #is_fresh_newfresh #EQlook_new_env_it ***** #EQt_code #EQ_get_el |
---|
[3404] | 1316 | #EQsign_env_it #EQ_f_lab #same_fresh_map #same_to_keep %{new_env_it} %{new_fresh} |
---|
| 1317 | % |
---|
[3416] | 1318 | [ % |
---|
| 1319 | [ assumption |
---|
| 1320 | | whd in ⊢ (??%?); @eq_function_name_elim [ #ABS >ABS in Hf; * #H @⊥ @H %] |
---|
| 1321 | #_ normalize nodelta assumption ]] |
---|
| 1322 | % [2: #x #Hx <same_to_keep // >associative_append @memb_append_l22 |
---|
[3405] | 1323 | inversion(memb ???) // #ABS lapply(lab_to_keep_in_domain … (eq_true_to_b … ABS)) |
---|
[3549] | 1324 | #ABS1 @(memb_no_duplicates_append … (a_return_post … x) … H) // |
---|
[3405] | 1325 | cases(lookup_ok_append … Henv_it) #l1 * #l2 * #EQ1 #EQ2 destruct(EQ1 EQ2) |
---|
| 1326 | >foldr_map_append >memb_append_l2 // >foldr_map_append >memb_append_l1 // |
---|
| 1327 | whd in match (foldr ?????); @orb_Prop_r >memb_append_l1 // >Hx % ] |
---|
[3416] | 1328 | % [2: #x #Hx <same_fresh_map // >cons_append <associative_append |
---|
| 1329 | <associative_append in ⊢ (??(???(??%?)?)?); >associative_append |
---|
| 1330 | @(get_element_append_r1) |
---|
[3408] | 1331 | % >domain_of_associative_list_append #ABS cases(memb_append … ABS) |
---|
| 1332 | [ whd in match (memb ???); inversion(x==hd_lab) normalize nodelta |
---|
| 1333 | [2: #_ whd in match (memb ???); #EQ destruct ] #EQx_hdlab #_ |
---|
| 1334 | <(\P EQx_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it) |
---|
| 1335 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
| 1336 | * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 // |
---|
| 1337 | >memb_append_l1 // whd in ⊢ (??%?); cases(x==?) // |
---|
| 1338 | normalize nodelta >memb_append_l1 // >Hx % |
---|
| 1339 | | #ABS1 @(memb_no_duplicates_append … x … H) |
---|
| 1340 | [ @(lab_map_in_domain … (eq_true_to_b … ABS1)) |
---|
| 1341 | | cases(lookup_ok_append … Henv_it) |
---|
| 1342 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
| 1343 | >memb_append_l2 // >memb_append_l1 // |
---|
| 1344 | whd in ⊢ (??%?); cases(x==?) // |
---|
| 1345 | normalize nodelta >memb_append_l1 // >Hx % |
---|
| 1346 | ] |
---|
| 1347 | ] |
---|
| 1348 | ] |
---|
[3416] | 1349 | % // % // % // <EQ_get_el >cons_append <associative_append <associative_append in ⊢ (??(???(??%?)?)?); |
---|
| 1350 | >associative_append |
---|
[3408] | 1351 | @get_element_append_r1 % >domain_of_associative_list_append #ABS cases(memb_append … ABS) |
---|
[3549] | 1352 | [ whd in match (memb ???); inversion(a_call … (f_lab … new_env_it)== a_call … hd_lab) |
---|
[3408] | 1353 | #EQ_hdlab normalize nodelta |
---|
| 1354 | [2: whd in ⊢ (??%? → ?); #EQ destruct ] |
---|
| 1355 | #_ <(\P EQ_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it) |
---|
| 1356 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
| 1357 | * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 // |
---|
| 1358 | >memb_append_l1 // whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) // |
---|
[3549] | 1359 | | #ABS1 @(memb_no_duplicates_append … (a_call … (f_lab … new_env_it)) … H) |
---|
[3408] | 1360 | [ @(lab_map_in_domain … (eq_true_to_b … ABS1)) |
---|
| 1361 | | cases(lookup_ok_append … Henv_it) |
---|
| 1362 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
| 1363 | >memb_append_l2 // >memb_append_l1 // |
---|
| 1364 | whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) // |
---|
| 1365 | ] |
---|
| 1366 | ] |
---|
[3405] | 1367 | ] |
---|
[3409] | 1368 | qed. |
---|
[3399] | 1369 | |
---|
[3527] | 1370 | (* |
---|
[3445] | 1371 | axiom permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y. |
---|
| 1372 | (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7) |
---|
| 1373 | →is_permutation A ((l6 @l2) @l7) ((l3 @l8) @l9) |
---|
| 1374 | →is_permutation A |
---|
| 1375 | (y ::((l6 @((x ::l5) @(l1 @l2))) @l7)) |
---|
| 1376 | (((x ::l4 @y ::l3) @l8) @l9)). |
---|
[3527] | 1377 | *) |
---|
[3531] | 1378 | |
---|