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". |
---|
19 | include "basics/jmeq.ma". |
---|
20 | |
---|
21 | discriminator option. |
---|
22 | |
---|
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 | |
---|
87 | |
---|
88 | (* |
---|
89 | lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → |
---|
90 | (i1 ≠ i2 → P false) → P (eq_instructions p i1 i2). |
---|
91 | #P #p #i1 elim i1 |
---|
92 | [* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ |
---|
93 | lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') |
---|
94 | | #rt * normalize [2: #rt' cases (dec_eq … rt rt') #H [>(\b H) | >(\bf H) ] /2/ |
---|
95 | #_ #K @K % #abs lapply (eq_to_jmeq ??? abs) #abs' destruct(abs') @(absurd ?? H) //] |
---|
96 | [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ |
---|
97 | lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') |
---|
98 | | #seq * [| #lbl] #i #IH * normalize |
---|
99 | [1,8: |2,9: #t_t |3,10: #seq1 #opt_l #i2 |4,11: #cond #ltrue #i_t #lfalse #i_f #i_c |
---|
100 | |5,12: #cond #ltrue #i_t #lfalse #i_f |6,13: #f #act_p #ret #i3 |*: #lin #io #lout #i3] |
---|
101 | #H1 #H2 try(@H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct) |
---|
102 | inversion(?==?) normalize nodelta |
---|
103 | [2,4: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct |
---|
104 | >(\b (refl …)) in ABS; #EQ destruct] |
---|
105 | #EQseq inversion(eq_instructions ???) normalize nodelta #Heq_i2 |
---|
106 | [2,4: @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct |
---|
107 | *) |
---|
108 | |
---|
109 | record env_params : Type[1] ≝ |
---|
110 | { form_params_type : Type[0] |
---|
111 | }. |
---|
112 | |
---|
113 | record signature (p : env_params) (p' : instr_params) : Type[0] ≝ |
---|
114 | { f_name : FunctionName |
---|
115 | ; f_pars : form_params_type p |
---|
116 | ; f_ret : return_type p' |
---|
117 | }. |
---|
118 | |
---|
119 | record env_item (p : env_params) (p' : instr_params) : Type[0] ≝ |
---|
120 | { f_sig :> signature p p' |
---|
121 | ; f_lab : CallCostLabel |
---|
122 | ; f_body : Instructions p' |
---|
123 | }. |
---|
124 | |
---|
125 | record state_params : Type[1] ≝ |
---|
126 | { i_pars :> instr_params |
---|
127 | ; e_pars :> env_params |
---|
128 | ; store_type : DeqSet |
---|
129 | }. |
---|
130 | |
---|
131 | record state (p : state_params) : Type[0] ≝ |
---|
132 | { code : Instructions p |
---|
133 | ; cont : list (ActionLabel × (Instructions p)) |
---|
134 | ; store : store_type p |
---|
135 | ; io_info : bool |
---|
136 | }. |
---|
137 | |
---|
138 | definition is_io : ∀p.state p → Prop ≝ λp,st.io_info … st = true. |
---|
139 | |
---|
140 | record sem_state_params (p : state_params) : Type[0] ≝ |
---|
141 | { eval_seq : seq_instr p → (store_type p) → option (store_type p) |
---|
142 | ; eval_io : io_instr p → store_type p → option (store_type p) |
---|
143 | ; eval_cond_cond : cond_instr p → store_type p → option (bool × (store_type p)) |
---|
144 | ; eval_loop_cond : loop_instr p → store_type p → option (bool × (store_type p)) |
---|
145 | ; eval_call : signature p p → act_params_type p → store_type p → option (store_type p) |
---|
146 | ; eval_after_return : return_type p → store_type p → option (store_type p) |
---|
147 | ; init_store : store_type p |
---|
148 | }. |
---|
149 | |
---|
150 | |
---|
151 | let rec lookup (p : env_params) (p' : instr_params) (l : list (env_item p p')) |
---|
152 | on l : FunctionName → option (env_item p p') ≝ |
---|
153 | match l with |
---|
154 | [ nil ⇒ λ_.None ? |
---|
155 | | cons x xs ⇒ λf.if (eq_function_name f (f_name … x)) |
---|
156 | then Some ? x |
---|
157 | else lookup … xs f |
---|
158 | ]. |
---|
159 | |
---|
160 | definition is_ret_call_act : ActionLabel → Prop ≝ |
---|
161 | λa.match a with [ret_act _ ⇒ True | call_act _ _ ⇒ True | _ ⇒ False ]. |
---|
162 | |
---|
163 | inductive execute_l (p : state_params) (p' : sem_state_params p) (env : list (env_item p p)) : |
---|
164 | ActionLabel → relation (state p) ≝ |
---|
165 | | empty : ∀st,st',hd,tl.(code ? st) = (EMPTY p)→ (cont ? st) = hd :: tl → |
---|
166 | (code ? st') = \snd hd → (cont … st') = tl → (store … st) = (store … st') → |
---|
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' |
---|
168 | | seq_sil : ∀st,st',i,cd,s,opt_l.(code ? st) = SEQ … i opt_l cd → |
---|
169 | eval_seq … p' i (store … st) = return s → (code ? st') = cd → |
---|
170 | (cont … st) = (cont … st') → (store … st') = s → |
---|
171 | io_info … st = false → io_info ? st' = false → execute_l … (cost_act opt_l) st st' |
---|
172 | | cond_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m. |
---|
173 | (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp (store … st) = return 〈true,new_m〉 → |
---|
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' |
---|
176 | | cond_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,cd,new_m. |
---|
177 | (code ? st) = COND … exp ltrue i_true lfalse i_false cd → eval_cond_cond … p' exp (store … st) = return 〈false,new_m〉 → |
---|
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' |
---|
180 | | loop_true : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m. |
---|
181 | code ? st = LOOP … exp ltrue i_true lfalse i_false → eval_loop_cond … p' exp (store … st) = return 〈true,new_m〉 → |
---|
182 | cont ? st' = 〈cost_act (None ?),LOOP … exp ltrue i_true lfalse i_false〉 :: (cont … st) → |
---|
183 | code … st' = i_true → store … st' = new_m → io_info … st = false → io_info … st' = false → |
---|
184 | execute_l … (cost_act (Some ? ltrue)) st st' |
---|
185 | | loop_false : ∀st,st',exp,ltrue,i_true,lfalse,i_false,new_m. |
---|
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 → |
---|
188 | io_info … st = false → io_info … st' = false → execute_l … (cost_act (Some ? lfalse)) st st' |
---|
189 | | io_in : ∀st,st',lin,io,lout,cd,mem.(code ? st) = IO … lin io lout cd → |
---|
190 | eval_io … p' io (store … st) = return mem → code ? st' = EMPTY 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' |
---|
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 → |
---|
195 | eval_call ? p' env_it act_p (store … st) = return mem → |
---|
196 | store ? st' = mem → code … st' = f_body … env_it → |
---|
197 | cont … st' = |
---|
198 | 〈(ret_act r_lb),cd〉 :: (cont … st) → |
---|
199 | io_info … st = false → (io_info … st') = false → |
---|
200 | execute_l … (call_act f (f_lab ?? env_it)) st st' |
---|
201 | | ret_instr : ∀st,st',r_t,mem,tl',rb,cd.code ? st = RETURN … r_t → |
---|
202 | cont … st = 〈ret_act rb,cd〉 :: tl' → cont ? st' = tl' → |
---|
203 | io_info … st = false → io_info ? st' = false → |
---|
204 | eval_after_return … p' r_t (store … st) = return mem → code … st' = cd → |
---|
205 | store … st' = mem → execute_l … (ret_act rb) st st'. |
---|
206 | |
---|
207 | let rec get_labels_of_code (p : instr_params) (i : Instructions p) on i : list CostLabel ≝ |
---|
208 | match i with |
---|
209 | [ EMPTY ⇒ [ ] |
---|
210 | | RETURN x ⇒ [ ] |
---|
211 | | SEQ x lab instr ⇒ let ih ≝ get_labels_of_code … instr in |
---|
212 | match lab with [ None ⇒ ih | Some lbl ⇒ a_non_functional_label lbl :: ih ] |
---|
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 |
---|
221 | a_non_functional_label ltrue :: a_non_functional_label lfalse :: (ih1 @ ih2) |
---|
222 | | CALL f act_p r_lb i1 ⇒ |
---|
223 | let ih1 ≝ get_labels_of_code … i1 in |
---|
224 | match r_lb with [ None ⇒ ih1 | Some lbl ⇒ a_return_post lbl :: ih1] |
---|
225 | | IO lin io lout i1 ⇒ |
---|
226 | let ih1 ≝ get_labels_of_code … i1 in |
---|
227 | a_non_functional_label lin :: a_non_functional_label lout :: ih1 |
---|
228 | ]. |
---|
229 | |
---|
230 | include "basics/lists/listb.ma". |
---|
231 | include "../src/utilities/hide.ma". |
---|
232 | |
---|
233 | let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ |
---|
234 | match l with |
---|
235 | [ nil ⇒ True |
---|
236 | | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs |
---|
237 | ]. |
---|
238 | |
---|
239 | lemma no_duplicates_append_r : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) → |
---|
240 | no_duplicates … l2. |
---|
241 | #A #l1 elim l1 // #x #xs normalize #IH #l2 * /2/ |
---|
242 | qed. |
---|
243 | |
---|
244 | lemma no_duplicates_append_l : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) → |
---|
245 | no_duplicates … l1. |
---|
246 | #A #l1 elim l1 // #x #xs normalize #IH #l2 * #H1 #H2 % [2: /2/ ] |
---|
247 | inversion(x ∈ xs @l2) in H1; normalize [ #_ * #H @⊥ @H %] #H1 #_ |
---|
248 | % inversion(x ∈ xs) normalize [2: //] #H3 #_ >(memb_append_l1 … H3) in H1; |
---|
249 | #EQ destruct(EQ) |
---|
250 | qed. |
---|
251 | |
---|
252 | record Program (p : env_params) (p' : instr_params) : Type[0] ≝ |
---|
253 | { env : list (env_item p p') |
---|
254 | ; main : Instructions p' |
---|
255 | }. |
---|
256 | |
---|
257 | |
---|
258 | definition no_duplicates_labels : ∀p,p'.Program p p' → Prop ≝ |
---|
259 | λp,p',prog. |
---|
260 | no_duplicates … |
---|
261 | (foldr … (λitem,acc.((a_call (f_lab … item)) :: get_labels_of_code … (f_body … item)) @ acc) (get_labels_of_code … (main … prog)) (env … prog)). |
---|
262 | |
---|
263 | lemma no_duplicates_domain_of_fun: |
---|
264 | ∀p,p',prog.no_duplicates_labels … prog → |
---|
265 | ∀f,env_it.lookup p p' (env … prog) f = return env_it → |
---|
266 | no_duplicates … (get_labels_of_code … (f_body … env_it)). |
---|
267 | #p #p' * #env elim env [ #main normalize #_ #f #env_it #EQ destruct(EQ)] |
---|
268 | #x #xs #IH #main whd in ⊢ (% → ?); whd in match (foldr ?????); #H #f #env_it |
---|
269 | whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta |
---|
270 | [ whd in ⊢ (? → ???% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) cases H #_ /2/ ] |
---|
271 | #H1 #EQenv_it @IH cases H /2/ |
---|
272 | qed. |
---|
273 | |
---|
274 | |
---|
275 | definition is_synt_succ : ∀p.relation (state p) ≝ λp,s1,s2.cont … s1 = cont … s2 ∧ |
---|
276 | match (code … s1) with |
---|
277 | [ CALL f act_p r_lb i1 ⇒ code … s2 = i1 |
---|
278 | | _ ⇒ False |
---|
279 | ]. |
---|
280 | |
---|
281 | definition operational_semantics : ∀p : state_params.∀p'.Program p p → abstract_status ≝ |
---|
282 | λp,p',prog.mk_abstract_status |
---|
283 | (state p) |
---|
284 | (execute_l ? p' (env … prog)) |
---|
285 | (is_synt_succ …) |
---|
286 | (λs.match (code … s) with |
---|
287 | [ COND _ _ _ _ _ _ ⇒ cl_jump |
---|
288 | | LOOP _ _ _ _ _ ⇒ cl_jump |
---|
289 | | EMPTY ⇒ if io_info … s then cl_io else cl_other |
---|
290 | | _ ⇒ cl_other |
---|
291 | ]) |
---|
292 | (λs.match (code … s) with |
---|
293 | [CALL _ _ m _ ⇒ match m with [ Some _ ⇒ true | None ⇒ false ] |
---|
294 | | _ ⇒ false |
---|
295 | ]) |
---|
296 | (λs.eq_instructions … (code … s) (main … prog) ∧ isnilb … (cont … s) ∧ store … s == init_store … p' ∧ io_info … s) |
---|
297 | (λs.match (cont … s) with |
---|
298 | [ nil ⇒ match (code … s) with |
---|
299 | [ EMPTY ⇒ true |
---|
300 | | RETURN _ ⇒ true |
---|
301 | | _ ⇒ false |
---|
302 | ] |
---|
303 | | _ ⇒ false |
---|
304 | ]) |
---|
305 | ???. |
---|
306 | @hide_prf |
---|
307 | [ #s1 #s2 #l #H #H1 inversion H1 #st #st' |
---|
308 | [ #hd #tl |
---|
309 | | #i #cd #s #opt_l |
---|
310 | |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |
---|
311 | |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m |
---|
312 | | #lin #io #lout #cd #mem |
---|
313 | | #f #act_p #r_lb #cd #mem #env_it |
---|
314 | | #r_t #mem #tl #rb #cd |
---|
315 | ] |
---|
316 | #EQcode |
---|
317 | [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQ5 #H2 #EQ' #EQ6 #EQ7 |
---|
318 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
319 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
320 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
321 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
322 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 |
---|
323 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 |
---|
324 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
325 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
326 | ] |
---|
327 | #_ destruct >EQcode in H; normalize nodelta /2 by ex_intro/ |
---|
328 | [ cases(io_info ??) normalize nodelta] #EQ destruct |
---|
329 | | #s1 #s2 #l #H #H1 inversion H1 #st #st' |
---|
330 | [ #hd #tl |
---|
331 | | #i #cd #s #opt_l |
---|
332 | |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |
---|
333 | |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m |
---|
334 | | #lin #io #lout #cd #mem |
---|
335 | | #f #act_p #r_lb #cd #mem #env_it |
---|
336 | | #r_t #mem #tl #rb #cd |
---|
337 | ] |
---|
338 | #EQcode |
---|
339 | [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7 |
---|
340 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
341 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
342 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
343 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
344 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost' #EQ7 #EQ8 #EQ9 |
---|
345 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost' #EQ6 #EQ7 #EQ8 |
---|
346 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQiost' #EQ8 #EQ9 #EQ10 |
---|
347 | | #EQ1 #EQ2 #EQ3 #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
348 | ] |
---|
349 | #_ destruct |
---|
350 | cases(code ? st') in H; normalize nodelta >EQiost' normalize nodelta |
---|
351 | #eq destruct try (#eq1 destruct) try (#eq2 destruct) try (#eq3 destruct) |
---|
352 | try (#eq4 destruct) try (#eq5 destruct) try (#eq6 destruct) %{lin} % |
---|
353 | | #s1 #s2 #l #H #H1 inversion H1 #st #st' |
---|
354 | [ #hd #tl |
---|
355 | | #i #cd #s #opt_l |
---|
356 | |3,4: #exp #ltrue #i_true #lfalse #i_false #cd #new_m |
---|
357 | |5,6: #exp #ltrue #i_true #lfalse #ifalse #new_m |
---|
358 | | #lin #io #lout #cd #mem |
---|
359 | | #f #act_p #r_lb #cd #mem #env_it |
---|
360 | | #r_t #mem #tl #rb #cd |
---|
361 | ] |
---|
362 | #EQcode |
---|
363 | [ #EQ1 #EQ2 #EQ3 #EQ4 #x #EQiost' #H2 #EQ' #EQ6 #EQ7 |
---|
364 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
365 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
366 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
367 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
368 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQiost #EQiost' #EQ7 #EQ8 #EQ9 |
---|
369 | | #EQ1 #EQ2 #EQ3 #EQiost #EQiost' #EQ6 #EQ7 #EQ8 |
---|
370 | | #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQiost #EQiost' #EQ8 #EQ9 #EQ10 |
---|
371 | | #EQ1 #EQ2 #EQiost #EQiost' #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
372 | ] |
---|
373 | #_ destruct >EQcode in H; normalize nodelta [|*: #EQ destruct] |
---|
374 | cases(io_info … st) in x; normalize nodelta [2: #_ #EQ destruct] |
---|
375 | #H3 #_ @H3 % |
---|
376 | ] |
---|
377 | qed. |
---|
378 | |
---|
379 | let rec eqb_list (D : DeqSet) (l1 : list D) on l1 : list D → bool ≝ |
---|
380 | match l1 with |
---|
381 | [ nil ⇒ λl2.match l2 with [nil ⇒ true | _ ⇒ false ] |
---|
382 | | cons x xs ⇒ λl2.match l2 with [ cons y ys ⇒ x == y ∧ eqb_list … xs ys | _ ⇒ false ] |
---|
383 | ]. |
---|
384 | |
---|
385 | definition DeqSet_List : DeqSet → DeqSet ≝ |
---|
386 | λX.mk_DeqSet (list X) (eqb_list …) ?. |
---|
387 | #x elim x [ * /2 by refl, conj/ #y #ys normalize % #EQ destruct] -x |
---|
388 | #x #xs #IH * [ normalize % #EQ destruct] #y #ys normalize % inversion(x == y) |
---|
389 | #EQ normalize nodelta |
---|
390 | [ #H >(proj1 … (IH ys) H) @eq_f2 [2: %] @(proj1 … (eqb_true …)) assumption |
---|
391 | | #EQ destruct |
---|
392 | | #EQ1 destruct @(proj2 … (IH …)) % |
---|
393 | | #EQ1 destruct <EQ @(proj2 … (eqb_true …)) % |
---|
394 | ] |
---|
395 | qed. |
---|
396 | |
---|
397 | unification hint 0 ≔ C; |
---|
398 | X ≟ DeqSet_List C |
---|
399 | (* ---------------------------------------- *) ⊢ |
---|
400 | list C ≡ carr X. |
---|
401 | |
---|
402 | |
---|
403 | unification hint 0 ≔ D,p1,p2; |
---|
404 | X ≟ DeqSet_List D |
---|
405 | (* ---------------------------------------- *) ⊢ |
---|
406 | eqb_list D p1 p2 ≡ eqb X p1 p2. |
---|
407 | |
---|
408 | definition associative_list : DeqSet → Type[0] → Type[0] ≝ |
---|
409 | λA,B.list (A × (list B)). |
---|
410 | |
---|
411 | let rec update_list (A : DeqSet) (B : Type[0]) (l : associative_list A B) |
---|
412 | on l : A → list B → associative_list A B ≝ |
---|
413 | λa,b.match l with |
---|
414 | [ nil ⇒ [〈a,b〉] |
---|
415 | | cons x xs ⇒ if (a == (\fst x)) then 〈a,b〉 :: xs |
---|
416 | else x :: (update_list … xs a b) |
---|
417 | ]. |
---|
418 | |
---|
419 | let rec get_element (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : A → list B ≝ |
---|
420 | λa.match l with [ nil ⇒ nil ? |
---|
421 | | cons x xs ⇒ if (a == \fst x) then \snd x else get_element … xs a |
---|
422 | ]. |
---|
423 | |
---|
424 | let rec domain_of_associative_list (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : list A ≝ |
---|
425 | match l with |
---|
426 | [ nil ⇒ [] |
---|
427 | | cons x xs ⇒ \fst x :: domain_of_associative_list … xs |
---|
428 | ]. |
---|
429 | |
---|
430 | lemma get_element_append_l: |
---|
431 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
432 | x ∈ domain_of_associative_list … l1 → |
---|
433 | get_element … (l1@l2) x = get_element … l1 x. |
---|
434 | #A #B #l1 elim l1 normalize [ #l2 #x * ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd)) |
---|
435 | #H [ >(\b H) | >(\bf H) ] normalize /2/ |
---|
436 | qed. |
---|
437 | |
---|
438 | lemma get_element_append_r: |
---|
439 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
440 | ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) → |
---|
441 | get_element ?? (l1@l2) x = get_element … l2 x. |
---|
442 | #A #B #l1 elim l1 normalize [ #l2 #x // ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd)) |
---|
443 | #H [ >(\b H) | >(\bf H) ] normalize /2 by/ * #K cases (K I) |
---|
444 | qed. |
---|
445 | |
---|
446 | lemma get_element_append_l1 : |
---|
447 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
448 | ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l2)) → |
---|
449 | get_element ?? (l1@l2) x = get_element … l1 x. |
---|
450 | #A #B #l1 elim l1 normalize [2: #x #xs #IH #l2 #a #H >IH // ] |
---|
451 | #l2 elim l2 // #y #ys #IH #a normalize cases(a == \fst y) normalize |
---|
452 | [ * #H @⊥ @H % ] #H @IH assumption |
---|
453 | qed. |
---|
454 | |
---|
455 | lemma get_element_append_r1 : |
---|
456 | ∀A,B. ∀l1,l2: associative_list A B. ∀x. |
---|
457 | ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) → |
---|
458 | get_element ?? (l1@l2) x = get_element … l2 x. |
---|
459 | #A #B #l1 elim l1 normalize // #x #xs #IH #l2 #a cases (?==?) |
---|
460 | normalize [* #H cases H //] #H >IH normalize // |
---|
461 | qed. |
---|
462 | |
---|
463 | definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝ |
---|
464 | λx.〈a_non_functional_label x,S x〉. |
---|
465 | |
---|
466 | definition fresh_cc_labe : ℕ → CallCostLabel × ℕ ≝ |
---|
467 | λx.〈a_call_label x,S x〉. |
---|
468 | |
---|
469 | definition fresh_rc_label : ℕ → ReturnPostCostLabel × ℕ ≝ |
---|
470 | λx.〈a_return_cost_label (S x),S x〉. |
---|
471 | |
---|
472 | record call_post_info (p : instr_params) : Type[0] ≝ |
---|
473 | { gen_labels : list CostLabel |
---|
474 | ; t_code : Instructions p |
---|
475 | ; fresh : ℕ |
---|
476 | ; lab_map : associative_list DEQCostLabel CostLabel |
---|
477 | ; lab_to_keep : list ReturnPostCostLabel |
---|
478 | }. |
---|
479 | |
---|
480 | let rec call_post_trans (p : instr_params) (i : Instructions p) (n : ℕ) on i : |
---|
481 | list CostLabel → call_post_info p ≝ |
---|
482 | λabs. |
---|
483 | match i with |
---|
484 | [ EMPTY ⇒ mk_call_post_info ? abs (EMPTY …) n (nil ?) (nil ?) |
---|
485 | | RETURN x ⇒ mk_call_post_info ? abs (RETURN … x) n (nil ?) (nil ?) |
---|
486 | | SEQ x lab instr ⇒ |
---|
487 | let ih ≝ call_post_trans … instr n abs in |
---|
488 | match lab with |
---|
489 | [ None ⇒ mk_call_post_info ? (gen_labels … ih) (SEQ … x (None ?) (t_code … ih)) |
---|
490 | (fresh … ih) (lab_map … ih) (lab_to_keep … ih) |
---|
491 | | Some lbl ⇒ |
---|
492 | mk_call_post_info ? (nil ?) (SEQ … x (Some ? lbl) (t_code … ih)) (fresh … ih) |
---|
493 | (〈a_non_functional_label lbl,(a_non_functional_label lbl :: (gen_labels … ih))〉 :: (lab_map … ih)) |
---|
494 | (lab_to_keep … ih) |
---|
495 | ] |
---|
496 | | COND x ltrue i1 lfalse i2 i3 ⇒ |
---|
497 | let ih3 ≝ call_post_trans … i3 n abs in |
---|
498 | let ih2 ≝ call_post_trans … i2 (fresh … ih3) (gen_labels … ih3) in |
---|
499 | let ih1 ≝ call_post_trans … i1 (fresh … ih2) (gen_labels … ih3) in |
---|
500 | mk_call_post_info ? (nil ?) (COND … x ltrue (t_code … ih1) lfalse (t_code … ih2) (t_code … ih3)) |
---|
501 | (fresh … ih1) |
---|
502 | (〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉:: |
---|
503 | 〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉:: |
---|
504 | ((lab_map … ih1) @ (lab_map … ih2) @ (lab_map … ih3))) |
---|
505 | ((lab_to_keep … ih1) @ (lab_to_keep … ih2) @ (lab_to_keep … ih3)) |
---|
506 | | LOOP x ltrue i1 lfalse i2 ⇒ |
---|
507 | let ih2 ≝ call_post_trans … i2 n abs in |
---|
508 | let ih1 ≝ call_post_trans … i1 (fresh … ih2) (nil ?) in |
---|
509 | mk_call_post_info ? (nil ?) (LOOP … x ltrue (t_code … ih1) lfalse (t_code … ih2)) (fresh … ih1) |
---|
510 | (〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉 :: |
---|
511 | 〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉 :: |
---|
512 | ((lab_map … ih1) @ (lab_map … ih2))) |
---|
513 | ((lab_to_keep … ih1) @ (lab_to_keep … ih2)) |
---|
514 | | CALL f act_p r_lb i1 ⇒ |
---|
515 | let ih ≝ call_post_trans … i1 n abs in |
---|
516 | match r_lb with |
---|
517 | [ None ⇒ let 〈l',f''〉 ≝ fresh_rc_label (fresh … ih) in |
---|
518 | mk_call_post_info ? ((a_return_post l')::(gen_labels … ih)) |
---|
519 | (CALL … f act_p (Some ? l') (t_code … ih)) f'' (lab_map … ih) (lab_to_keep … ih) |
---|
520 | | Some lbl ⇒ |
---|
521 | mk_call_post_info ? (nil ?) (CALL ? f act_p (Some ? lbl) (t_code … ih)) (fresh … ih) |
---|
522 | (〈a_return_post lbl,(a_return_post lbl :: (gen_labels … ih))〉 :: (lab_map … ih)) |
---|
523 | (lbl :: lab_to_keep … ih) |
---|
524 | ] |
---|
525 | | IO lin io lout i1 ⇒ |
---|
526 | let ih ≝ call_post_trans … i1 n abs in |
---|
527 | mk_call_post_info ? (nil ?) (IO ? lin io lout (t_code … ih)) (fresh … ih) |
---|
528 | (〈a_non_functional_label lout,(a_non_functional_label lout :: (gen_labels … ih))〉 :: |
---|
529 | 〈a_non_functional_label lin,[a_non_functional_label lin]〉 :: (lab_map … ih)) (lab_to_keep … ih) |
---|
530 | ]. |
---|
531 | |
---|
532 | |
---|
533 | let rec call_post_clean (p : instr_params) (i : Instructions p) on i : |
---|
534 | associative_list DEQCostLabel CostLabel → list ReturnPostCostLabel → list CostLabel → |
---|
535 | option ((list CostLabel) × (Instructions p)) ≝ |
---|
536 | λm,keep,abs. |
---|
537 | match i with |
---|
538 | [ EMPTY ⇒ Some ? 〈abs,EMPTY …〉 |
---|
539 | | RETURN x ⇒ Some ? 〈abs,RETURN … x〉 |
---|
540 | | SEQ x lab instr ⇒ |
---|
541 | ! 〈l,i1〉 ← call_post_clean … instr m keep abs; |
---|
542 | match lab with |
---|
543 | [ None ⇒ return 〈l,SEQ … x (None ?) i1〉 |
---|
544 | | Some lbl ⇒ if ((get_element … m lbl) == lbl :: l) |
---|
545 | then return 〈nil ?,SEQ … x (Some ? lbl) i1〉 |
---|
546 | else None ? |
---|
547 | ] |
---|
548 | | COND x ltrue i1 lfalse i2 i3 ⇒ |
---|
549 | ! 〈l3,instr3〉 ← call_post_clean … i3 m keep abs; |
---|
550 | ! 〈l2,instr2〉 ← call_post_clean … i2 m keep l3; |
---|
551 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep l3; |
---|
552 | if ((get_element … m ltrue) == ltrue :: l1) ∧ |
---|
553 | ((get_element … m lfalse) == lfalse :: l2) |
---|
554 | then return 〈nil ?,COND … x ltrue instr1 lfalse instr2 instr3〉 |
---|
555 | else None ? |
---|
556 | | LOOP x ltrue i1 lfalse i2 ⇒ |
---|
557 | ! 〈l2,instr2〉 ← call_post_clean … i2 m keep abs; |
---|
558 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep (nil ?); |
---|
559 | if ((get_element … m ltrue) == ltrue :: l1) ∧ |
---|
560 | ((get_element … m lfalse) == lfalse :: l2) |
---|
561 | then return 〈nil ?,LOOP … x ltrue instr1 lfalse instr2〉 |
---|
562 | else None ? |
---|
563 | | CALL f act_p r_lb i1 ⇒ |
---|
564 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs; |
---|
565 | match r_lb with |
---|
566 | [ None ⇒ None ? |
---|
567 | | Some lbl ⇒ if (lbl ∈ keep) |
---|
568 | then if ((get_element … m lbl) == lbl :: l1) |
---|
569 | then return 〈nil ?,CALL … f act_p (Some ? lbl) instr1〉 |
---|
570 | else None ? |
---|
571 | else return 〈(a_return_post lbl) :: l1,CALL … f act_p (None ?) instr1〉 |
---|
572 | ] |
---|
573 | | IO lin io lout i1 ⇒ |
---|
574 | ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs; |
---|
575 | if ((get_element … m lout) == lout :: l1) ∧ ((get_element … m lin) == [lin]) |
---|
576 | then return 〈nil ?,IO … lin io lout instr1〉 |
---|
577 | else None ? |
---|
578 | ]. |
---|
579 | |
---|
580 | let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (a : A) (l1 : list B) |
---|
581 | (l2 : list C) (f : A → B → C → A) on l1 : option A≝ |
---|
582 | match l1 with |
---|
583 | [ nil ⇒ match l2 with [ nil ⇒ return a | cons y ys ⇒ None ? ] |
---|
584 | | cons x xs ⇒ |
---|
585 | match l2 with |
---|
586 | [ nil ⇒ None ? |
---|
587 | | cons y ys ⇒ ! ih ← (foldr2 … a xs ys f); |
---|
588 | return f ih x y |
---|
589 | ] |
---|
590 | ]. |
---|
591 | |
---|
592 | definition is_silent_cost_act_b : ActionLabel → bool ≝ |
---|
593 | λact. match act with |
---|
594 | [ cost_act x ⇒ match x with [None ⇒ true | _ ⇒ false ] | _ ⇒ false]. |
---|
595 | |
---|
596 | definition eq_ActionLabel : ActionLabel → ActionLabel → bool ≝ |
---|
597 | λc1,c2. |
---|
598 | match c1 with |
---|
599 | [ call_act f l ⇒ match c2 with [ call_act f' l' ⇒ f == f' ∧ l == l' | _ ⇒ false] |
---|
600 | | ret_act x ⇒ match c2 with [ret_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false] |
---|
601 | | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false] |
---|
602 | ] |
---|
603 | | _ ⇒ false |
---|
604 | ] |
---|
605 | | cost_act x ⇒ match c2 with [cost_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true | _ ⇒ false] |
---|
606 | | Some l ⇒ match y with [ Some l' ⇒ l == l' | _ ⇒ false] |
---|
607 | ] |
---|
608 | | _ ⇒ false |
---|
609 | ] |
---|
610 | ]. |
---|
611 | |
---|
612 | definition ret_costed_abs : list ReturnPostCostLabel → option ReturnPostCostLabel → option CostLabel ≝ |
---|
613 | λkeep,x. |
---|
614 | match x with |
---|
615 | [ Some lbl ⇒ if lbl ∈ keep then return (a_return_post lbl) |
---|
616 | else None ? |
---|
617 | | None ⇒ None ? |
---|
618 | ]. |
---|
619 | |
---|
620 | |
---|
621 | definition check_continuations : ∀p : instr_params. |
---|
622 | ∀l1,l2 : list (ActionLabel × (Instructions p)). |
---|
623 | associative_list DEQCostLabel CostLabel → |
---|
624 | list ReturnPostCostLabel → option (Prop × (list CostLabel) × (list CostLabel)) ≝ |
---|
625 | λp,cont1,cont2,m,keep. |
---|
626 | foldr2 ??? 〈True,nil ?,nil ?〉 cont1 cont2 |
---|
627 | (λx,y,z. |
---|
628 | let 〈cond,abs_top',abs_tail'〉 ≝ x in |
---|
629 | match call_post_clean p (\snd z) m keep abs_top' with |
---|
630 | [ None ⇒ 〈False,nil ?,nil ?〉 |
---|
631 | | Some w ⇒ |
---|
632 | match \fst z with |
---|
633 | [ ret_act opt_x ⇒ |
---|
634 | match ret_costed_abs keep opt_x with |
---|
635 | [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ |
---|
636 | get_element … m lbl = lbl :: (\fst w),(nil ?),abs_tail'〉 |
---|
637 | | None ⇒ |
---|
638 | 〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) @ abs_tail'〉 |
---|
639 | ] |
---|
640 | | cost_act opt_x ⇒ |
---|
641 | match opt_x with |
---|
642 | [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉 |
---|
643 | | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ |
---|
644 | get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉] |
---|
645 | | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). |
---|
646 | |
---|
647 | (* |
---|
648 | definition check_continuations : ∀p : instr_params. |
---|
649 | ∀l1,l2 : list (ActionLabel × (Instructions p)). |
---|
650 | associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → |
---|
651 | list (list CostLabel) → option (Prop × (list CostLabel) × (list (list CostLabel))) ≝ |
---|
652 | λp,cont1,cont2,m,keep,abs_top,abs_tail. |
---|
653 | foldr2 ??? 〈True,abs_top,abs_tail〉 cont1 cont2 |
---|
654 | (λx,y,z. |
---|
655 | let 〈cond,abs_top',abs_tail'〉 ≝ x in |
---|
656 | match call_post_clean p (\snd z) m keep abs_top' with |
---|
657 | [ None ⇒ 〈False,nil ?,nil ?〉 |
---|
658 | | Some w ⇒ |
---|
659 | match \fst z with |
---|
660 | [ ret_act opt_x ⇒ |
---|
661 | match ret_costed_abs keep opt_x with |
---|
662 | [ Some lbl ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ |
---|
663 | get_element … m lbl = lbl :: (\fst w),(nil ?),(nil ?) :: abs_tail'〉 |
---|
664 | | None ⇒ |
---|
665 | 〈\fst y = ret_act (None ?) ∧ cond ∧ \snd w = \snd y,(nil ?),(\fst w) :: abs_tail'〉 |
---|
666 | ] |
---|
667 | | cost_act opt_x ⇒ |
---|
668 | match opt_x with |
---|
669 | [ None ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y,\fst w,abs_tail'〉 |
---|
670 | | Some xx ⇒ 〈\fst y = \fst z ∧ cond ∧ \snd w = \snd y ∧ |
---|
671 | get_element … m xx = xx :: (\fst w),(nil ?),abs_tail'〉] |
---|
672 | | _ ⇒ (* dummy *) 〈False,nil ?,nil ?〉]]). *) |
---|
673 | (* in input : |
---|
674 | abs_top is the list of labels to be propageted to the deepest level of the call stack |
---|
675 | abs_tail are the lists of labels to be propagated to the levels "below" the deepest level |
---|
676 | in output : |
---|
677 | abs_top is the list of labels to be propageted from the current level of the call stack |
---|
678 | abs_tail are the lists of labels to be propagated from the levels "below" the current level |
---|
679 | *) |
---|
680 | |
---|
681 | |
---|
682 | definition state_rel : ∀p. |
---|
683 | associative_list DEQCostLabel CostLabel → list ReturnPostCostLabel → list CostLabel →(list CostLabel) → |
---|
684 | relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2. |
---|
685 | match check_continuations ? (cont ? st1) (cont … st2) m keep with |
---|
686 | [ Some x ⇒ let 〈prf1,abs_top',abs_tail'〉 ≝ x in |
---|
687 | prf1 ∧ call_post_clean … (code … st2) m keep abs_top' = return 〈abs_top,(code … st1)〉 |
---|
688 | ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 ∧ abs_tail = abs_tail' |
---|
689 | | None ⇒ False |
---|
690 | ]. |
---|
691 | |
---|
692 | include "Simulation.ma". |
---|
693 | |
---|
694 | let rec len (s : abstract_status) (st1 : s) (st2 : s) (t : raw_trace s st1 st2) |
---|
695 | on t : ℕ ≝ |
---|
696 | match t with |
---|
697 | [ t_base s ⇒ O |
---|
698 | | t_ind s1 s2 s3 l prf lt ⇒ S (len … lt) |
---|
699 | ]. |
---|
700 | (* |
---|
701 | lemma associative_max : ∀n1,n2,n3.max (max n1 n2) n3 = max n1 (max n2 n3). |
---|
702 | #n1 #n2 #n3 normalize @leb_elim normalize |
---|
703 | [ @leb_elim normalize |
---|
704 | [ #H1 #H2 @leb_elim normalize |
---|
705 | [ @leb_elim normalize // * #H @⊥ @H assumption |
---|
706 | | @leb_elim normalize |
---|
707 | [ #H3 * #H @⊥ @H @(transitive_le … H1) assumption |
---|
708 | | * #H @⊥ @H assumption |
---|
709 | ] |
---|
710 | ] |
---|
711 | | #H1 #H2 @leb_elim normalize |
---|
712 | [ @leb_elim normalize // #_ #H cases H1 #H1 @⊥ @H1 assumption |
---|
713 | | @leb_elim normalize |
---|
714 | [ #_ * #H @⊥ @H assumption |
---|
715 | | * #H @⊥ @H @(transitive_le … H2) |
---|
716 | *) |
---|
717 | let rec compute_max_n (p : instr_params) (i : Instructions p) on i : ℕ ≝ |
---|
718 | match i with |
---|
719 | [ EMPTY ⇒ O |
---|
720 | | RETURN x ⇒ O |
---|
721 | | SEQ x lab instr ⇒ let n ≝ compute_max_n … instr in |
---|
722 | match lab with |
---|
723 | [ None ⇒ n |
---|
724 | | Some l ⇒ |
---|
725 | match l with |
---|
726 | [ a_non_functional_label n' ⇒ S (max n n') ] |
---|
727 | ] |
---|
728 | | COND x ltrue i1 lfalse i2 i3 ⇒ |
---|
729 | let n1 ≝ compute_max_n … i1 in |
---|
730 | let n2 ≝ compute_max_n … i2 in |
---|
731 | let n3 ≝ compute_max_n … i3 in |
---|
732 | let mx ≝ max (max n1 n2) n3 in |
---|
733 | match ltrue with |
---|
734 | [ a_non_functional_label lt ⇒ |
---|
735 | match lfalse with |
---|
736 | [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ] |
---|
737 | | LOOP x ltrue i1 lfalse i2 ⇒ |
---|
738 | let n1 ≝ compute_max_n … i1 in |
---|
739 | let n2 ≝ compute_max_n … i2 in |
---|
740 | let mx ≝ max n1 n2 in |
---|
741 | match ltrue with |
---|
742 | [ a_non_functional_label lt ⇒ |
---|
743 | match lfalse with |
---|
744 | [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ] |
---|
745 | | CALL f act_p r_lb i1 ⇒ |
---|
746 | let n ≝ compute_max_n … i1 in |
---|
747 | match r_lb with |
---|
748 | [ None ⇒ n |
---|
749 | | Some lbl ⇒ match lbl with [a_return_cost_label l ⇒ S(max l n) ] |
---|
750 | ] |
---|
751 | | IO lin io lout i1 ⇒ |
---|
752 | let n ≝ compute_max_n … i1 in |
---|
753 | match lin with |
---|
754 | [a_non_functional_label l1 ⇒ |
---|
755 | match lout with |
---|
756 | [a_non_functional_label l2 ⇒ S(max (max n l1) l2) ] ] |
---|
757 | ]. |
---|
758 | |
---|
759 | |
---|
760 | definition same_fresh_map_on : list CostLabel → |
---|
761 | relation (associative_list DEQCostLabel CostLabel) ≝ |
---|
762 | λdom,m1,m2.∀x.bool_to_Prop (x ∈ dom) → get_element … m1 x = get_element … m2 x. |
---|
763 | |
---|
764 | definition same_to_keep_on : list CostLabel → relation (list ReturnPostCostLabel) ≝ |
---|
765 | λdom,keep1,keep2.∀x. bool_to_Prop (a_return_post x ∈ dom) → (x ∈ keep1) = (x ∈ keep2). |
---|
766 | |
---|
767 | lemma memb_not_append : ∀D : DeqSet.∀l1,l2 : list D.∀x : D. |
---|
768 | x ∈ l1 = false → x ∈ l2 = false → x ∈ (l1 @ l2) = false. |
---|
769 | #D #l1 elim l1 |
---|
770 | [ #l2 #x #_ #H @H ] |
---|
771 | #x #xs #IH #l2 #x1 whd in match (memb ???); inversion (x1 == x) normalize nodelta |
---|
772 | [ #_ #EQ destruct] #EQx1 #EQxs #EQl2 whd in match (memb ???); >EQx1 |
---|
773 | normalize nodelta @IH // |
---|
774 | qed. |
---|
775 | |
---|
776 | lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A . |
---|
777 | no_duplicates … (l1 @ l2) → x ∈ l1 → x ∈ l2 → False. |
---|
778 | #A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???); |
---|
779 | inversion (x == x1) normalize nodelta |
---|
780 | [ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H % |
---|
781 | | #_ @IH // |
---|
782 | ] |
---|
783 | qed. |
---|
784 | |
---|
785 | |
---|
786 | lemma same_to_keep_on_append : ∀dom1,dom2,dom3 : list CostLabel. |
---|
787 | ∀l1,l2,l3,l : list ReturnPostCostLabel. |
---|
788 | no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → a_return_post x ∈ dom1) → |
---|
789 | (∀x.x ∈ l3 → a_return_post x ∈ dom3) → |
---|
790 | same_to_keep_on (dom1@dom2@dom3) (l1@l2@l3) l → |
---|
791 | same_to_keep_on dom2 l2 l. |
---|
792 | #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #sub_set1 #sub_set3 #H2 |
---|
793 | #x #Hx inversion (x ∈ l2) |
---|
794 | [ #EQkeep <H2 [> memb_append_l2 // >memb_append_l1 // ] |
---|
795 | >memb_append_l2 // >memb_append_l1 // >Hx // |
---|
796 | | #EQno_keep <H2 |
---|
797 | [2: >memb_append_l2 // >memb_append_l1 // >Hx // |
---|
798 | | @sym_eq @memb_not_append [2: @memb_not_append //] |
---|
799 | [ <associative_append in no_dup; #no_dup ] |
---|
800 | lapply(memb_no_duplicates_append … (a_return_post x) … no_dup) #H |
---|
801 | inversion(memb ???) // #H1 cases H |
---|
802 | [1,4: [>memb_append_l2 | >memb_append_l1] // >Hx // |
---|
803 | | @sub_set3 >H1 // |
---|
804 | | @sub_set1 >H1 // |
---|
805 | ] |
---|
806 | ] |
---|
807 | ] |
---|
808 | qed. |
---|
809 | |
---|
810 | lemma same_fresh_map_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l. |
---|
811 | no_duplicates … (dom1 @dom2 @ dom3) → (∀x.x ∈ domain_of_associative_list … l1 → x ∈ dom1) → |
---|
812 | (∀x.x ∈ domain_of_associative_list … l3 → x ∈ dom3) → |
---|
813 | same_fresh_map_on … (dom1 @dom2 @dom3) (l1 @l2 @ l3) l → |
---|
814 | same_fresh_map_on … dom2 l2 l. |
---|
815 | #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #subset1 #subset3 whd in ⊢ (% → ?); #H1 |
---|
816 | whd #x #Hx <H1 |
---|
817 | [2: >memb_append_l2 // >memb_append_l1 // >Hx //] |
---|
818 | >get_element_append_r [ >get_element_append_l1 // ] % #K |
---|
819 | [ lapply(subset3 … K) | lapply(subset1 … K) ] #ABS |
---|
820 | [ <associative_append in no_dup; #no_dup] @(memb_no_duplicates_append … x … no_dup) |
---|
821 | // [>memb_append_l2 | >memb_append_l1 ] // >Hx // |
---|
822 | qed. |
---|
823 | |
---|
824 | |
---|
825 | lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p. |
---|
826 | ∀x,n,l. |
---|
827 | x ∈ lab_to_keep … (call_post_trans … i n l) → a_return_post x ∈ get_labels_of_code … i. |
---|
828 | #p #i elim i // |
---|
829 | [ #seq #opt_l #instr #IH #x #n #l whd in match (call_post_trans ????); |
---|
830 | cases opt_l -opt_l normalize nodelta [|#lbl] |
---|
831 | whd in match (get_labels_of_code ??); #H [2: @orb_Prop_r] /2/ |
---|
832 | | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l |
---|
833 | whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); |
---|
834 | #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r |
---|
835 | [ >memb_append_l1 // @IH1 [3: >H // |*: ] |
---|
836 | | >memb_append_l2 // cases(memb_append … H) -H #H |
---|
837 | [>memb_append_l1 // @IH2 [3: >H // |*: ] |
---|
838 | | >memb_append_l2 // @IH3 [3: >H // |*: ] |
---|
839 | ] |
---|
840 | ] |
---|
841 | | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l |
---|
842 | whd in match (call_post_trans ????); whd in match (get_labels_of_code ??); |
---|
843 | #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r |
---|
844 | [ >memb_append_l1 | >memb_append_l2 ] // [ @IH1 | @IH2 ] [3,6: >H |*: ] // |
---|
845 | | #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????); |
---|
846 | whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); |
---|
847 | inversion(x == lbl) #Hlbl normalize nodelta |
---|
848 | [* >(\P Hlbl) @orb_Prop_l @eq_costlabel_elim // * #H @H % |
---|
849 | | #H @orb_Prop_r @IH // |
---|
850 | ] |
---|
851 | | #lin #io #lout #i1 #IH #x #n #l whd in match (call_post_trans ????); |
---|
852 | whd in match (get_labels_of_code ??); #H @orb_Prop_r @orb_Prop_r @IH // |
---|
853 | ] |
---|
854 | qed. |
---|
855 | |
---|
856 | lemma domain_of_associative_list_append : ∀A,B.∀l1,l2 : associative_list A B. |
---|
857 | domain_of_associative_list ?? (l1 @ l2) = |
---|
858 | (domain_of_associative_list ?? l1) @ (domain_of_associative_list ?? l2). |
---|
859 | #A #B #l1 elim l1 // #x #xs #IH #l2 normalize // |
---|
860 | qed. |
---|
861 | |
---|
862 | lemma lab_map_in_domain: ∀p.∀i: Instructions p. |
---|
863 | ∀x,n,l. |
---|
864 | x ∈ domain_of_associative_list … (lab_map p (call_post_trans … i n l)) → |
---|
865 | x ∈ get_labels_of_code … i. |
---|
866 | #p #i elim i // |
---|
867 | [ #seq * [|#lbl] #i1 #IH #x #n #l whd in match(call_post_trans ????); |
---|
868 | whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); |
---|
869 | inversion(x==lbl) #Hlbl normalize nodelta [#_ whd in match (memb ???); >Hlbl % ] |
---|
870 | #H >memb_cons // @IH // |
---|
871 | | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l |
---|
872 | whd in match (call_post_trans ????); whd in match (memb ???); |
---|
873 | whd in match (get_labels_of_code ??); inversion(x == ltrue) #Hlbl normalize nodelta |
---|
874 | [ #_ whd in match (memb ???); >Hlbl % ] whd in match (memb ???); |
---|
875 | inversion(x == lfalse) #Hlbl1 normalize nodelta |
---|
876 | [ #_ whd in match (memb ???); >Hlbl normalize nodelta whd in match (memb ???); |
---|
877 | >Hlbl1 % ] #H >memb_cons // >memb_cons // >domain_of_associative_list_append in H; |
---|
878 | #H cases(memb_append … H) [ #H1 >memb_append_l1 // @IH1 [3: >H1 // |*:] ] |
---|
879 | >domain_of_associative_list_append #H1 cases(memb_append … H1) |
---|
880 | #H2 >memb_append_l2 // [ >memb_append_l1 | >memb_append_l2 ] // |
---|
881 | [ @IH2 | @IH3] /2 by eq_true_to_b/ |
---|
882 | | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l whd in match (call_post_trans ????); |
---|
883 | whd in match (get_labels_of_code ??); whd in match (memb ???); inversion(x == lfalse) |
---|
884 | #Hlfalse normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlfalse // ] |
---|
885 | whd in match (memb ???); inversion(x==ltrue) normalize nodelta #Hltrue |
---|
886 | [ #_ whd in match (memb ???); >Hltrue %] >domain_of_associative_list_append #H |
---|
887 | cases(memb_append … H) #H1 >memb_cons // >memb_cons // [ >memb_append_l1 | >memb_append_l2 ] |
---|
888 | // [ @IH1 | @IH2] /2/ |
---|
889 | | #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????); |
---|
890 | whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); inversion (x == lbl) |
---|
891 | #Hlbl normalize nodelta [ #_ whd in match (memb ???); >Hlbl % ] #H >memb_cons // @IH /2/ |
---|
892 | | #lin #io #lout #i1 #IH #x #n #l whd in match (memb ???); inversion(x == lout) #Hlout |
---|
893 | normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlout % ] |
---|
894 | whd in match (memb ???); inversion(x==lin) #Hlin normalize nodelta |
---|
895 | [ #_ whd in match (memb ???); >Hlin % ] #H >memb_cons // >memb_cons // @IH /2/ |
---|
896 | ] |
---|
897 | qed. |
---|
898 | |
---|
899 | lemma eq_a_non_functional_label : |
---|
900 | ∀c1,c2.c1 == c2 → a_non_functional_label c1 == a_non_functional_label c2. |
---|
901 | #c1 #c2 #EQ cases(eqb_true DEQNonFunctionalLabel c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ |
---|
902 | #EQ destruct >(\b (refl …)) @I |
---|
903 | qed. |
---|
904 | |
---|
905 | let rec is_fresh_for_return (keep : list CostLabel) (n : ℕ) on keep : Prop ≝ |
---|
906 | match keep with |
---|
907 | [ nil ⇒ True |
---|
908 | | cons x xs ⇒ let ih ≝ is_fresh_for_return xs n in |
---|
909 | match x with |
---|
910 | [ a_return_post y ⇒ match y with [a_return_cost_label m ⇒ m ≤ n ∧ ih ] |
---|
911 | | _ ⇒ ih |
---|
912 | ] |
---|
913 | ]. |
---|
914 | |
---|
915 | lemma fresh_ok_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.∀l. |
---|
916 | n ≤ fresh … (call_post_trans p i1 n l). |
---|
917 | #p #i1 elim i1 normalize /2 by transitive_le, le_n/ |
---|
918 | [ #seq * [|#lbl] #i2 #IH #n #l normalize /2 by / |
---|
919 | | #cond #ltrue #i_true #lfalse #i_false #i2 #IH1 #IH2 #IH3 #n #l |
---|
920 | @(transitive_le … (IH3 …)) [2: @(transitive_le … (IH2 …)) [2: @(transitive_le … (IH1 …)) ]] // |
---|
921 | | #f #act_p * [|#lbl] normalize #i2 #IH /2 by le_S/ |
---|
922 | ] |
---|
923 | qed. |
---|
924 | |
---|
925 | lemma fresh_keep_n_ok : ∀n,m,l. |
---|
926 | is_fresh_for_return l n → n ≤ m → is_fresh_for_return l m. |
---|
927 | #n #m #l lapply n -n lapply m -m elim l // * |
---|
928 | [1,2,3: * #x] #xs #IH #n #m |
---|
929 | normalize [2: * #H1] #H2 #H3 [ %] /2 by transitive_le/ |
---|
930 | qed. |
---|
931 | |
---|
932 | definition cast_return_to_cost_labels ≝ map … (a_return_post …). |
---|
933 | coercion cast_return_to_cost_labels. |
---|
934 | |
---|
935 | lemma fresh_false : ∀n.∀l: list ReturnPostCostLabel.is_fresh_for_return l n → |
---|
936 | a_return_cost_label (S n) ∈ l = false. |
---|
937 | #n #l lapply n -n elim l // * #x #xs #IH #n whd in ⊢ (% → ??%?); * #H1 |
---|
938 | #H2 @eq_return_cost_lab_elim |
---|
939 | [ #EQ destruct @⊥ /2 by absurd/ |
---|
940 | | #_ >IH // |
---|
941 | ] |
---|
942 | qed. |
---|
943 | |
---|
944 | lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ. |
---|
945 | let dom ≝ get_labels_of_code … i1 in |
---|
946 | no_duplicates … dom → |
---|
947 | ∀m,keep. |
---|
948 | ∀info,l.call_post_trans p i1 n l = info → |
---|
949 | same_fresh_map_on dom (lab_map … info) m → |
---|
950 | same_to_keep_on dom (lab_to_keep … info) keep → |
---|
951 | is_fresh_for_return keep n → |
---|
952 | call_post_clean ? (t_code ? info) m keep l |
---|
953 | = return 〈gen_labels … info,i1〉. |
---|
954 | #p #i1 elim i1 |
---|
955 | [ #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); |
---|
956 | #EQ destruct(EQ) // |
---|
957 | | #x #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); |
---|
958 | #EQ destruct(EQ) // |
---|
959 | | #seq * [|#lbl] #instr #IH #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep |
---|
960 | #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%%); normalize nodelta |
---|
961 | >IH // |
---|
962 | [1,4: whd whd in H2; #x #Hx @H2 whd in match (get_labels_of_code ??); // |
---|
963 | |2,5: whd whd in H1; #x #Hx [ @H1 // ] cases no_dup #H3 #_ <H1 |
---|
964 | [2: whd in match (get_labels_of_code ??); @orb_Prop_r // ] |
---|
965 | whd in ⊢ (???%); cases(eqb_true … x lbl) inversion(x == lbl) normalize nodelta |
---|
966 | [2: //] #_ #H4 >H4 in Hx; // #H5 >H5 in H3; * #ABS @⊥ @ABS % |
---|
967 | |6: cases no_dup // |
---|
968 | ] |
---|
969 | normalize nodelta <(H1 lbl) |
---|
970 | [2: whd in match (get_labels_of_code ??); @orb_Prop_l cases(eqb_true … (a_non_functional_label lbl) lbl) |
---|
971 | #H3 #H4 >H4 % ] |
---|
972 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
973 | >(\b (refl …)) % |
---|
974 | | #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #n normalize nodelta |
---|
975 | #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); |
---|
976 | #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%?); >IH3 // |
---|
977 | [2: whd in match (get_labels_of_code ??) in H2; |
---|
978 | change with ([?;?]@?) in match (?::?) in H2; |
---|
979 | <associative_append in H2; <associative_append |
---|
980 | <(append_nil … (?@?)) <associative_append in ⊢ (??%? → ?); |
---|
981 | <(append_nil … (?@?)) in ⊢ (??%? → ?); >associative_append |
---|
982 | >associative_append in ⊢ (??%? → ?); #H2 |
---|
983 | @(same_to_keep_on_append … H2) // [ >append_nil |
---|
984 | whd in ⊢ (??%); whd in no_dup:(??%); >associative_append // ] |
---|
985 | #x #Hx cases (memb_append … Hx) -Hx #Hx @orb_Prop_r @orb_Prop_r |
---|
986 | [ >memb_append_l1 | >memb_append_l2 ] // |
---|
987 | @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |
---|
988 | |3: -H2 whd in match (get_labels_of_code ??) in H1; |
---|
989 | change with ([?;?]@?) in match (?::?) in H1; |
---|
990 | <associative_append in H1; <associative_append |
---|
991 | <(append_nil … (?@?)) >associative_append |
---|
992 | change with ([?;?]@?) in match (?::?::?) in ⊢ (??%? → ?); |
---|
993 | <associative_append in ⊢ (??%? → ?); |
---|
994 | <associative_append in ⊢ (??%? → ?); |
---|
995 | <(append_nil … (?@?)) in ⊢ (??%? → ?); |
---|
996 | >associative_append in ⊢ (??%? → ?); #H1 |
---|
997 | @(same_fresh_map_on_append … H1) // |
---|
998 | [ >append_nil >associative_append // ] |
---|
999 | #x whd in match (memb ???); inversion(x == ltrue) |
---|
1000 | [ #Hltrue normalize nodelta #_ whd in match (memb ???); >Hltrue % |
---|
1001 | | #Hltrue normalize nodelta whd in match (memb ???); inversion(x == lfalse) |
---|
1002 | [ #Hlfalse #_ @orb_Prop_r @orb_Prop_l >Hlfalse % |
---|
1003 | | #Hlfalse normalize nodelta #Hx @orb_Prop_r @orb_Prop_r |
---|
1004 | >domain_of_associative_list_append in Hx; #H |
---|
1005 | cases(memb_append … H) #H2 [ >memb_append_l1 | >memb_append_l2 ] |
---|
1006 | // @(lab_map_in_domain … (eq_true_to_b … H2)) |
---|
1007 | ] |
---|
1008 | ] |
---|
1009 | |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |] |
---|
1010 | ] |
---|
1011 | normalize nodelta >IH2 |
---|
1012 | [5: % |
---|
1013 | |2: /2 by fresh_keep_n_ok/ |
---|
1014 | |3: whd in match (get_labels_of_code ??) in H2; |
---|
1015 | change with ([?;?]@?) in match (?::?) in H2; |
---|
1016 | <associative_append in H2; #H2 |
---|
1017 | @(same_to_keep_on_append … H2) // #x #Hx [ @orb_Prop_r @orb_Prop_r ] |
---|
1018 | @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |
---|
1019 | |4: whd in match (get_labels_of_code ??) in H1; |
---|
1020 | change with ([?;?]@?) in match (?::?) in H1; |
---|
1021 | change with ([?;?]@?) in match (?::?::?) in H1 : (??%?); |
---|
1022 | <associative_append in H1; <associative_append in ⊢ (??%? → ?); #H1 |
---|
1023 | @(same_fresh_map_on_append … H1) // [2: /2 by lab_map_in_domain/ ] |
---|
1024 | #x >domain_of_associative_list_append #H cases(memb_append … H) |
---|
1025 | [ whd in ⊢ (??%? → ?%); cases(x == ltrue) // normalize nodelta |
---|
1026 | whd in ⊢ (??%? → ?%); cases(x == lfalse) // normalize nodelta |
---|
1027 | normalize #EQ destruct |
---|
1028 | | #H1 @orb_Prop_r @orb_Prop_r |
---|
1029 | @(lab_map_in_domain … (eq_true_to_b … H1)) |
---|
1030 | ] |
---|
1031 | |6: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l |
---|
1032 | |*: |
---|
1033 | ] |
---|
1034 | >m_return_bind >IH1 |
---|
1035 | [5: % |
---|
1036 | |2: /3 by fresh_keep_n_ok/ |
---|
1037 | |3: whd in match (get_labels_of_code ??) in H2; |
---|
1038 | change with ([?;?]@?) in match (?::?) in H2; |
---|
1039 | change with ([ ] @ ?) in match (lab_to_keep ??) in H2; |
---|
1040 | >associative_append in H2 : (??%?); #H2 |
---|
1041 | @(same_to_keep_on_append … H2) // #x #Hx cases(memb_append … Hx) |
---|
1042 | -Hx #Hx [ >memb_append_l1 | >memb_append_l2] // |
---|
1043 | @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |
---|
1044 | |4: whd in match (get_labels_of_code ??) in H1; |
---|
1045 | change with ([?;?]@?) in match (?::?) in H1; |
---|
1046 | change with ([?;?]@?) in match (?::?::?) in H1 : (??%?); |
---|
1047 | @(same_fresh_map_on_append … H1) // #x >domain_of_associative_list_append |
---|
1048 | #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2 ] |
---|
1049 | // @(lab_map_in_domain … (eq_true_to_b … Hx)) |
---|
1050 | |6: cases no_dup #_ * #_ @no_duplicates_append_l |
---|
1051 | |*: |
---|
1052 | ] |
---|
1053 | >m_return_bind normalize nodelta whd in H1; <H1 |
---|
1054 | [2: whd in match (get_labels_of_code ??); whd in match (memb ???); |
---|
1055 | >(\b (refl …)) % ] whd in match (get_element ????); >(\b (refl …)) |
---|
1056 | normalize nodelta >(\b (refl …)) <H1 |
---|
1057 | [2: whd in match (get_labels_of_code ??); >memb_cons // |
---|
1058 | whd in match (memb ???); >(\b (refl …)) % ] |
---|
1059 | whd in match (get_element ????); @eq_costlabel_elim normalize nodelta |
---|
1060 | [ #ABS @⊥ cases no_dup >ABS * #H #_ @H @orb_Prop_l |
---|
1061 | >(\b (refl ? (a_non_functional_label ltrue))) % ] #_ |
---|
1062 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
1063 | >(\b (refl …)) % |
---|
1064 | | #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?); |
---|
1065 | #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on #f_k |
---|
1066 | whd in ⊢ (??%?); >(IH2 … (refl …)) |
---|
1067 | [ normalize nodelta >(IH1 … (refl …)) |
---|
1068 | [ >m_return_bind <fresh_map [2: @orb_Prop_l >(\b (refl …)) % ] |
---|
1069 | whd in match (get_element ????); |
---|
1070 | inversion(a_non_functional_label ltrue == a_non_functional_label lfalse) |
---|
1071 | #Hltrue normalize nodelta |
---|
1072 | [ cases no_dup whd in match (memb ???); |
---|
1073 | cases(eqb_true … (a_non_functional_label ltrue) (a_non_functional_label lfalse)) |
---|
1074 | #H1 #_ lapply(H1 Hltrue) #EQ destruct(EQ) >(\b (refl …)) * #ABS @⊥ @ABS % ] |
---|
1075 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …)) |
---|
1076 | <fresh_map [2: @orb_Prop_r @orb_Prop_l >(\b (refl …)) % ] |
---|
1077 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
1078 | >(\b (refl …)) % |
---|
1079 | | /2 by fresh_keep_n_ok/ |
---|
1080 | | change with ([?;?]@?@?) in keep_on : (?%??); change with ((nil ?) @ ? @ ?) in keep_on : (??%?); |
---|
1081 | @(same_to_keep_on_append … keep_on) // #x /2 by lab_to_keep_in_domain/ |
---|
1082 | | change with ([?;?]@?@?) in fresh_map : (?%%?); @(same_fresh_map_on_append … fresh_map) |
---|
1083 | /2 by lab_map_in_domain/ #x whd in match (memb ???); inversion(x==lfalse) #Hlfalse |
---|
1084 | normalize nodelta |
---|
1085 | [ #_ @orb_Prop_r whd in match (memb ???); >Hlfalse % |
---|
1086 | | whd in match (memb ???); inversion(x==ltrue) #Hltrue normalize nodelta [2: *] #_ |
---|
1087 | @orb_Prop_l >Hltrue % |
---|
1088 | ] |
---|
1089 | | cases no_dup #_ * #_ /2/ |
---|
1090 | ] |
---|
1091 | | // |
---|
1092 | | change with ([?;?]@?@?) in keep_on : (?%??); <associative_append in keep_on; |
---|
1093 | <(append_nil … (?@?)) <(append_nil … (?@?)) in ⊢ (??%? → ?); |
---|
1094 | >associative_append in ⊢ (?%%? → ?); >associative_append in ⊢ (??%? → ?); |
---|
1095 | #keep_on @(same_to_keep_on_append … keep_on) // |
---|
1096 | [ >associative_append >append_nil // |
---|
1097 | | #x #Hx @orb_Prop_r @orb_Prop_r /2 by lab_to_keep_in_domain/ |
---|
1098 | ] |
---|
1099 | | change with ([?;?]@?@?) in fresh_map : (?%??); <associative_append in fresh_map; |
---|
1100 | <(append_nil … (?@?)) change with ([?;?]@?@?) in ⊢ (??%? → ?); |
---|
1101 | <associative_append in ⊢ (??%? → ?); <(append_nil … (?@?)) in ⊢ (??%? → ?); |
---|
1102 | >associative_append in ⊢ (?%%? → ?); >associative_append in ⊢ (??%? → ?); |
---|
1103 | #fresh_map @(same_fresh_map_on_append … fresh_map) // |
---|
1104 | [ >append_nil // |
---|
1105 | | #x >domain_of_associative_list_append #Hx cases(memb_append … Hx) |
---|
1106 | [2: #Hx1 @orb_Prop_r @orb_Prop_r @(lab_map_in_domain … (eq_true_to_b … Hx1)) ] |
---|
1107 | whd in match (memb ???); inversion(x == lfalse) normalize nodelta #Hlfalse |
---|
1108 | [ #_ @orb_Prop_r @orb_Prop_l >Hlfalse % |
---|
1109 | | whd in match (memb ???); inversion (x==ltrue) normalize nodelta #Hltrue |
---|
1110 | [ #_ @orb_Prop_l >Hltrue % |
---|
1111 | | whd in match (memb ???); #EQ destruct |
---|
1112 | ] |
---|
1113 | ] |
---|
1114 | ] |
---|
1115 | | cases no_dup #_ * #_ /2 by no_duplicates_append_r/ |
---|
1116 | ] |
---|
1117 | | #f #act_p * [|#r_lb] #i #IH #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?); |
---|
1118 | #EQ destruct(EQ) #fresh_map #same_keep #f_k whd in ⊢ (??%?); |
---|
1119 | >(IH … (refl …)) |
---|
1120 | [1,6: normalize nodelta |
---|
1121 | [ >fresh_false [2: /2 by fresh_keep_n_ok/] % |
---|
1122 | | <same_keep |
---|
1123 | [ whd in match (memb ???); >(\b (refl …)) normalize nodelta |
---|
1124 | <fresh_map |
---|
1125 | [ whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
1126 | >(\b (refl …)) % |
---|
1127 | | whd in match (memb ???); >(\b (refl …)) % |
---|
1128 | ] |
---|
1129 | | whd in match (memb ???); >(\b (refl …)) % |
---|
1130 | ] |
---|
1131 | ] |
---|
1132 | |2,7: // |
---|
1133 | |3,8: whd in match (get_labels_of_code ??) in same_keep; // #x #Hx <same_keep |
---|
1134 | [2: >memb_cons // >Hx // ] cases no_dup * #ABS #_ whd in ⊢ (???%); |
---|
1135 | inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) >Hx // |
---|
1136 | |4,9: whd in match (get_labels_of_code ??) in fresh_map; // #x #Hx <fresh_map |
---|
1137 | [2: >memb_cons // >Hx //] cases no_dup * #ABS #_ whd in ⊢ (???%); |
---|
1138 | inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) // |
---|
1139 | |5,10: [ @no_dup | cases no_dup // ] |
---|
1140 | ] |
---|
1141 | | #lin #io #lout #i #IH #n whd in match (get_labels_of_code ??); #no_dup |
---|
1142 | #m #keep #info #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #fresh_map #same_keep |
---|
1143 | #f_k whd in ⊢ (??%?); >(IH … (refl …)) |
---|
1144 | [ normalize nodelta <fresh_map [2: >memb_cons // >memb_hd // ] |
---|
1145 | whd in match (get_element ????); >(\b (refl …)) normalize nodelta |
---|
1146 | >(\b (refl …)) <fresh_map [2: >memb_hd //] whd in match (get_element ????); |
---|
1147 | inversion(lin==lout) |
---|
1148 | [ #ABS @⊥ cases no_dup * #ABS1 #_ @ABS1 whd in match (memb ???); >(\P ABS) |
---|
1149 | >(\b (refl …)) // |
---|
1150 | | #H inversion (a_non_functional_label lin== ? lout) |
---|
1151 | [ #ABS lapply(\P ABS) #EQ destruct >(\b (refl …)) in H; #EQ destruct |
---|
1152 | | #_ normalize nodelta whd in match (get_element ????); >(\b (refl …)) |
---|
1153 | normalize nodelta >(\b (refl …)) % |
---|
1154 | ] |
---|
1155 | ] |
---|
1156 | | // |
---|
1157 | | #x #Hx >same_keep [2: >memb_cons // >memb_cons // >Hx % ] % |
---|
1158 | | #x #Hx <fresh_map [2: >memb_cons // >memb_cons // >Hx %] |
---|
1159 | cases no_dup * #ABS1 ** #ABS2 #_ whd in ⊢ (???%); inversion(x == lout) |
---|
1160 | normalize nodelta |
---|
1161 | [2: #_ whd in ⊢ (???%); inversion(x==lin) normalize nodelta // |
---|
1162 | #H @⊥ @ABS1 >memb_cons // <(\P H) >Hx // |
---|
1163 | | #H @⊥ @ABS2 <(\P H) >Hx // |
---|
1164 | ] |
---|
1165 | | cases no_dup #_ * #_ // |
---|
1166 | ] |
---|
1167 | ] |
---|
1168 | qed. |
---|
1169 | |
---|
1170 | definition fresh_for_prog_aux : ∀p,p'.Program p p' → ℕ → ℕ ≝ |
---|
1171 | λp,p',prog,n.foldl … (λn,i.max n (compute_max_n … (f_body … i))) n (env … prog). |
---|
1172 | |
---|
1173 | include alias "arithmetics/nat.ma". |
---|
1174 | |
---|
1175 | lemma max_1 : ∀n,m,k.k ≤ m → k ≤ max m n. |
---|
1176 | #m #n #k #H normalize @leb_elim // normalize nodelta #H1 |
---|
1177 | /2 by transitive_le/ |
---|
1178 | qed. |
---|
1179 | |
---|
1180 | lemma max_2 : ∀n,m,k.k≤ n → k ≤ max m n. |
---|
1181 | #m #n #k #H normalize @leb_elim // #H1 normalize nodelta |
---|
1182 | @(transitive_le … H) @(transitive_le … (not_le_to_lt … H1)) // |
---|
1183 | qed. |
---|
1184 | |
---|
1185 | lemma fresh_aux_ok : ∀p,p'.∀prog : Program p p'.∀n,m.n ≤ m → |
---|
1186 | fresh_for_prog_aux … prog n ≤ fresh_for_prog_aux … prog m. |
---|
1187 | #p #p' * #env #main elim env // #hd #tl #IH #n #m #H whd in ⊢ (?%%); |
---|
1188 | @IH whd in ⊢ (?%?); @leb_elim normalize nodelta |
---|
1189 | [ #H1 @max_2 // | #_ @max_1 // ] |
---|
1190 | qed. |
---|
1191 | |
---|
1192 | definition fresh_for_prog : ∀p,p'.Program p p' → ℕ ≝ |
---|
1193 | λp,p',prog.fresh_for_prog_aux … prog |
---|
1194 | (compute_max_n … (main … prog)). |
---|
1195 | |
---|
1196 | definition translate_env ≝ |
---|
1197 | λp,p'.λenv : list (env_item p p').λmax_all.(foldr ?? |
---|
1198 | (λi,x.let 〈t_env,n,m,keep〉 ≝ x in |
---|
1199 | let info ≝ call_post_trans … (f_body … i) n (nil ?) in |
---|
1200 | 〈(mk_env_item ?? |
---|
1201 | (mk_signature ??(f_name ?? i) (f_pars … i) (f_ret … i)) |
---|
1202 | (f_lab … i) (t_code … info)) :: t_env, |
---|
1203 | fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 :: |
---|
1204 | ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉) |
---|
1205 | (〈nil ?,max_all,nil ?,nil ?〉) env). |
---|
1206 | |
---|
1207 | definition trans_prog : ∀p,p'.Program p p' → |
---|
1208 | ((Program p p') × (associative_list DEQCostLabel CostLabel)) × ((list ReturnPostCostLabel))≝ |
---|
1209 | λp,p',prog. |
---|
1210 | let max_all ≝ fresh_for_prog … prog in |
---|
1211 | let info_main ≝ (call_post_trans … (main … prog) max_all (nil ?)) in |
---|
1212 | let 〈t_env,n,m,keep〉 ≝ translate_env … (env … prog) (fresh … info_main) in |
---|
1213 | 〈mk_Program ?? t_env (t_code … info_main),m @ (lab_map … info_main),keep @ (lab_to_keep … info_main)〉. |
---|
1214 | |
---|
1215 | definition map_labels_on_trace : |
---|
1216 | (associative_list DEQCostLabel CostLabel) → list CostLabel → list CostLabel ≝ |
---|
1217 | λm,l.foldr … (λlab,t.(get_element … m lab) @ t) (nil ?) l. |
---|
1218 | |
---|
1219 | lemma map_labels_on_trace_append: |
---|
1220 | ∀m,l1,l2. map_labels_on_trace m (l1@l2) = |
---|
1221 | map_labels_on_trace m l1 @ map_labels_on_trace m l2. |
---|
1222 | #m #l1 elim l1 // #hd #tl #IH #l2 >associative_append <IH // |
---|
1223 | qed. |
---|
1224 | |
---|
1225 | include "../src/common/Errors.ma". |
---|
1226 | |
---|
1227 | axiom is_permutation: ∀A.list A → list A → Prop. |
---|
1228 | axiom is_permutation_eq : ∀A.∀l : list A.is_permutation … l l. |
---|
1229 | axiom is_permutation_cons : ∀A.∀l1,l2,x.is_permutation A l1 l2 → |
---|
1230 | is_permutation A (x :: l1) (x :: l2). |
---|
1231 | |
---|
1232 | (* |
---|
1233 | inductive is_permutation (A : Type[0]) : list A → list A → Prop ≝ |
---|
1234 | | p_empty : is_permutation A (nil ?) (nil ?) |
---|
1235 | | p_append : ∀x,x1,x2,y,y1,y2. |
---|
1236 | x = y → is_permutation A (x1 @ x2) (y1 @ y2) → |
---|
1237 | is_permutation A (x1 @ [x] @ x2) (y1 @ [y] @ y2). |
---|
1238 | |
---|
1239 | lemma is_permutation_eq : ∀A.∀l : list A.is_permutation … l l. |
---|
1240 | #A #l elim l // #x #xs #IH |
---|
1241 | change with ((nil ?) @ (x :: xs)) in ⊢ (??%%); |
---|
1242 | >append_cons >associative_append |
---|
1243 | @(p_append ? x (nil ?) xs x (nil ?) xs (refl …)) @IH |
---|
1244 | qed. |
---|
1245 | |
---|
1246 | lemma is_permutation_append : ∀A.∀l1,l2,l3,l4 : list A. |
---|
1247 | is_permutation A l1 l3 → is_permutation A l2 l4 → |
---|
1248 | is_permutation A (l1 @ l2) (l3 @ l4). |
---|
1249 | #A #l1 inversion (|l1|) [2: #n lapply l1 elim n |
---|
1250 | [ #l2 #l3 #l4 #H inversion H // #x #x1 #x2 #y #y1 #y2 #EQ #H1 #_ |
---|
1251 | #ABS cases(nil_to_nil … (sym_eq ??? ABS)) -ABS #_ #ABS |
---|
1252 | cases(nil_to_nil … ABS) #EQ1 destruct(EQ1) ] |
---|
1253 | #x #xs #IH #l2 #l3 #l4 #H inversion H |
---|
1254 | [#EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ) ] |
---|
1255 | #y #y1 #y2 #z #z1 #z2 #EQ destruct(EQ) #H1 #_ #EQx_xs #EQ destruct(EQ) #_ |
---|
1256 | *) |
---|
1257 | |
---|
1258 | lemma memb_append_l22 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A. |
---|
1259 | ¬ (x ∈ l1) → x∈ l1 @ l2 = (x ∈ l2). |
---|
1260 | #A #x #l1 elim l1 normalize // #y #ys #IH #l2 cases(x==y) |
---|
1261 | normalize [*] @IH |
---|
1262 | qed. |
---|
1263 | |
---|
1264 | lemma memb_append_l12 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A. |
---|
1265 | ¬ (x ∈ l2) → x∈ l1 @ l2 = (x ∈ l1). |
---|
1266 | #A #x #l1 elim l1 |
---|
1267 | [ #l2 #H whd in match (append ???); @not_b_to_eq_false @Prop_notb >H % ] |
---|
1268 | #y #ys #IH #l2 #H1 whd in match (memb ???); >IH // |
---|
1269 | qed. |
---|
1270 | |
---|
1271 | |
---|
1272 | lemma lookup_ok_append : ∀p,p',l,f,env_it. |
---|
1273 | lookup p p' l f = return env_it → ∃l1,l2. l = l1 @ [env_it] @ l2 ∧ |
---|
1274 | f_name … env_it = f. |
---|
1275 | #p #p' #l elim l [ #f #env_it normalize #EQ destruct] |
---|
1276 | #x #xs #IH #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim |
---|
1277 | [ #EQ destruct(EQ) normalize nodelta whd in ⊢ (???% → ?); #EQ destruct |
---|
1278 | %{(nil ?)} %{xs} /2/ |
---|
1279 | | #Hno_f normalize nodelta #EQ_env_it cases(IH … EQ_env_it) |
---|
1280 | #l1 * #l2 * #EQ1 #EQ2 %{(x :: l1)} %{l2} >EQ1 /2/ |
---|
1281 | ] |
---|
1282 | qed. |
---|
1283 | (* |
---|
1284 | lemma foldr_append : |
---|
1285 | ∀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. |
---|
1286 | #A #B #l1 elim l1 // |
---|
1287 | #hd #tl #Hind #l2 #f #seed normalize >Hind @refl |
---|
1288 | qed. |
---|
1289 | *) |
---|
1290 | |
---|
1291 | lemma foldr_map_append : |
---|
1292 | ∀A,B:Type[0]. ∀l1, l2 : list A. |
---|
1293 | ∀f:A → list B. ∀seed. |
---|
1294 | foldr ?? (λx,acc. (f x) @ acc) seed (l1 @ l2) = |
---|
1295 | append ? (foldr ?? (λx,acc. (f x) @ acc) (nil ?) l1) |
---|
1296 | (foldr ?? (λx,acc. (f x) @ acc) seed l2). |
---|
1297 | #A #B #l1 elim l1 normalize // /3 by eq_f, trans_eq/ |
---|
1298 | qed. |
---|
1299 | |
---|
1300 | lemma cons_append : ∀A.∀x : A.∀l.x::l = ([x]@l). |
---|
1301 | // |
---|
1302 | qed. |
---|
1303 | |
---|
1304 | lemma eq_a_call_label : |
---|
1305 | ∀c1,c2.c1 == c2 → a_call c1 == a_call c2. |
---|
1306 | #c1 #c2 #EQ cases(eqb_true ? c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ |
---|
1307 | #EQ destruct >(\b (refl …)) @I |
---|
1308 | qed. |
---|
1309 | |
---|
1310 | |
---|
1311 | lemma no_duplicates_append_commute : ∀ A : DeqSet.∀l1,l2 : list A. |
---|
1312 | no_duplicates … (l1 @ l2) → |
---|
1313 | no_duplicates … (l2 @ l1). |
---|
1314 | #A #l1 elim l1 |
---|
1315 | [ #l2 >append_nil //] |
---|
1316 | #x #xs #IH #l2 * #H1 #H2 lapply(IH … H2) lapply H1 -H1 -IH -H2 |
---|
1317 | elim l2 -l1 |
---|
1318 | [ >append_nil #H1 #H2 % // ] |
---|
1319 | #y #ys #IH * #H1 * #H2 #H3 % |
---|
1320 | [2: @IH |
---|
1321 | [ % #H4 @H1 cases(memb_append … H4) |
---|
1322 | [ #H5 >memb_append_l1 // |
---|
1323 | | #H5 >memb_append_l2 // @orb_Prop_r >H5 // |
---|
1324 | ] |
---|
1325 | | // |
---|
1326 | ] |
---|
1327 | | % #H4 cases(memb_append … H4) |
---|
1328 | [ #H5 @(absurd ?? H2) >memb_append_l1 // |
---|
1329 | | whd in match (memb ???); inversion(y==x) |
---|
1330 | [ #H5 #_ <(\P H5) in H1; #H1 @H1 >memb_append_l2 // |
---|
1331 | | #_ normalize nodelta #H5 @(absurd ?? H2) >memb_append_l2 // |
---|
1332 | ] |
---|
1333 | ] |
---|
1334 | ] |
---|
1335 | qed. |
---|
1336 | |
---|
1337 | (* aggiungere fresh_to_keep al lemma seguente??*) |
---|
1338 | |
---|
1339 | let rec subset (A : Type[0]) (l1,l2 : list A) on l1 : Prop ≝ |
---|
1340 | match l1 with |
---|
1341 | [ nil ⇒ True |
---|
1342 | | cons x xs ⇒ mem … x l2 ∧ subset … xs l2 |
---|
1343 | ]. |
---|
1344 | |
---|
1345 | interpretation "subset" 'subseteq a b = (subset ? a b). |
---|
1346 | |
---|
1347 | lemma subset_append_l2 : ∀A,l2,l1.subset A l2 (l1 @ l2). |
---|
1348 | #A #l2 elim l2 // normalize #x #xs #IH #l1 % // @mem_append_l2 whd /2/ |
---|
1349 | qed. |
---|
1350 | |
---|
1351 | lemma refl_subset : ∀A.reflexive … (subset A). |
---|
1352 | #A #l1 elim l1 // #x #xs #IH normalize % /2/ |
---|
1353 | qed. |
---|
1354 | |
---|
1355 | lemma fresh_for_subset : ∀l1,l2,n.l1 ⊆ l2 → is_fresh_for_return … l2 n → |
---|
1356 | is_fresh_for_return … l1 n. |
---|
1357 | #l1 elim l1 // * [1,2,3: * #x] #xs #IH #l2 #n * #H1 #H2 #H3 whd |
---|
1358 | try(@IH) // % [2: @IH //] elim l2 in H1 H3; normalize [*] |
---|
1359 | * [1,2,3: * #y] #ys #IH normalize |
---|
1360 | [2,3: * [2,4: #H3 [2: @IH //] * #H4 #H5 @IH // |
---|
1361 | |*: #EQ destruct * // |
---|
1362 | ]] |
---|
1363 | * |
---|
1364 | [1,3: #EQ destruct ] #H3 #H4 @IH // |
---|
1365 | qed. |
---|
1366 | |
---|
1367 | lemma fresh_append : ∀n,l1,l2.is_fresh_for_return l1 n → is_fresh_for_return l2 n → |
---|
1368 | is_fresh_for_return (l1@l2) n. |
---|
1369 | #n #l1 lapply n -n elim l1 // * [1,2,3: * #x] #xs #IH #n #l2 [2: * #H1 ] #H2 #H3 |
---|
1370 | [ % // @IH //] @IH // |
---|
1371 | qed. |
---|
1372 | |
---|
1373 | definition labels_of_prog : ∀p,p'.Program p p' → ? ≝ |
---|
1374 | λp,p',prog.foldr … (λx,l.l @ (get_labels_of_code … (f_body … x))) |
---|
1375 | (get_labels_of_code … (main … prog)) (env … prog). |
---|
1376 | |
---|
1377 | lemma cast_return_append : ∀l1,l2.cast_return_to_cost_labels … (l1 @ l2) = |
---|
1378 | (cast_return_to_cost_labels … l1) @ (cast_return_to_cost_labels … l2). |
---|
1379 | #l1 #l2 @(sym_eq … (map_append …)) qed. |
---|
1380 | |
---|
1381 | include alias "arithmetics/nat.ma". |
---|
1382 | |
---|
1383 | |
---|
1384 | lemma is_fresh_code : ∀p.∀i : Instructions p. |
---|
1385 | is_fresh_for_return (get_labels_of_code … i) (compute_max_n … i). |
---|
1386 | #p #main elim main // |
---|
1387 | [ #seq * [| * #lbl] #i #IH normalize // @(fresh_keep_n_ok … IH) |
---|
1388 | inversion(leb ? lbl) // @leb_elim #Hlbl #EQ destruct normalize nodelta |
---|
1389 | /2 by le_S/ |
---|
1390 | | #cond * #ltrue #i1 * #lfalse #i2 #i3 #IH1 #IH2 #IH3 whd in ⊢ (?%%); |
---|
1391 | @fresh_append |
---|
1392 | [ @(fresh_keep_n_ok … IH1) @le_S @max_1 @max_1 @max_1 @max_1 // |
---|
1393 | | @fresh_append |
---|
1394 | [ @(fresh_keep_n_ok … IH2) @le_S @max_1 @max_1 @max_1 @max_2 // |
---|
1395 | | @(fresh_keep_n_ok … IH3) @le_S @max_1 @max_1 @max_2 // |
---|
1396 | ] |
---|
1397 | ] |
---|
1398 | | #cond * #ltrue #i1 * #lfalse #i2 #IH1 #IH2 whd in ⊢ (?%%); @fresh_append |
---|
1399 | [ @(fresh_keep_n_ok … IH1) @le_S @max_1 @max_1 @max_1 // |
---|
1400 | | @(fresh_keep_n_ok … IH2) @le_S @max_1 @max_1 @max_2 // |
---|
1401 | ] |
---|
1402 | | #f #act_p * [| * #lbl] #i #IH whd in ⊢ (?%%); // |
---|
1403 | change with ([?]@?) in ⊢ (?%?); @fresh_append |
---|
1404 | [ whd % // @le_S @max_1 // |
---|
1405 | | @(fresh_keep_n_ok … IH) @le_S @max_2 // |
---|
1406 | ] |
---|
1407 | | * #lin #io * #lout #i #IH whd in ⊢ (?%%); @(fresh_keep_n_ok … IH) |
---|
1408 | @le_S @max_1 @max_1 // |
---|
1409 | ] |
---|
1410 | qed. |
---|
1411 | |
---|
1412 | lemma is_fresh_fresh_for_prog : ∀p,p'.∀prog : Program p p'. |
---|
1413 | is_fresh_for_return (labels_of_prog … prog) (fresh_for_prog … prog). |
---|
1414 | #p #p' * #env #main whd in match fresh_for_prog; normalize nodelta whd in ⊢ (?%?); |
---|
1415 | elim env // * #sig #cost #i #tail #IH whd in ⊢ (?%?); @fresh_append |
---|
1416 | [ @(fresh_keep_n_ok … IH) @fresh_aux_ok @max_1 // |
---|
1417 | | @(fresh_keep_n_ok … (is_fresh_code … i)) whd in match fresh_for_prog_aux; normalize nodelta |
---|
1418 | whd in ⊢ (??%); elim tail [ @max_2 // ] #hd1 #tl1 #IH1 @(transitive_le … IH1) |
---|
1419 | whd in ⊢ (??%); change with (fresh_for_prog_aux ?? (mk_Program ?? tl1 main) ?) in ⊢ (?%%); |
---|
1420 | @fresh_aux_ok @max_1 // |
---|
1421 | ] |
---|
1422 | qed. |
---|
1423 | |
---|
1424 | lemma subset_def : ∀A : DeqSet.∀l1,l2 : list A.(∀x.x ∈l1 → x ∈ l2) → l1 ⊆ l2. |
---|
1425 | #A #l1 elim l1 // #x #xs #IH #l2 #H % |
---|
1426 | [ @memb_to_mem >H // >memb_hd // |
---|
1427 | | @IH #y #H1 @H >memb_cons // >H1 // |
---|
1428 | ] |
---|
1429 | qed. |
---|
1430 | |
---|
1431 | lemma memb_cast_return : ∀keep,x.x ∈ cast_return_to_cost_labels keep → |
---|
1432 | ∃ y.x = a_return_post y ∧ bool_to_Prop (y ∈ keep). |
---|
1433 | #keep elim keep |
---|
1434 | [ #x *] #x #xs #IH #y whd in match cast_return_to_cost_labels; |
---|
1435 | whd in match (map ????); whd in match (memb ???); inversion(y==x) |
---|
1436 | [ #Hx #_ %{x} >(\P Hx) %{(refl …)} >memb_hd // |
---|
1437 | | #Hx normalize nodelta #H cases(IH … H) #z * #H1 #H2 %{z} %{H1} >memb_cons // >H2 // |
---|
1438 | ] |
---|
1439 | qed. |
---|
1440 | |
---|
1441 | lemma subset_append : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l2 ⊆ l3 → (l1 @ l2) ⊆ l3. |
---|
1442 | #A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 % /2/ |
---|
1443 | qed. |
---|
1444 | |
---|
1445 | lemma subset_def_inv : ∀A.∀l1,l2 : list A. l1 ⊆ l2 → ∀x.mem … x l1 → mem … x l2. |
---|
1446 | #A #l1 elim l1 [ #l2 * #x * ] #x #xs #IH #l2 * #H1 #H2 #y * |
---|
1447 | [ #EQ destruct // | #H3 @IH // ] |
---|
1448 | qed. |
---|
1449 | |
---|
1450 | lemma transitive_subset : ∀A.transitive … (subset A). |
---|
1451 | #A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 % |
---|
1452 | [ @(subset_def_inv … H3) // | @IH // ] |
---|
1453 | qed. |
---|
1454 | |
---|
1455 | lemma subset_append_h1 : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l1 ⊆ (l3 @ l2). |
---|
1456 | #A #l1 elim l1 // #x #x2 #IH #l2 #l3 * #H1 #H2 % [ @mem_append_l1 // | @IH // ] |
---|
1457 | qed. |
---|
1458 | |
---|
1459 | lemma subset_append_h2 : ∀A.∀l1,l2,l3 : list A.l2 ⊆ l3 → l2 ⊆ (l1 @ l3). |
---|
1460 | #A #l1 elim l1 // #x #xs #IH #l2 elim l2 // #y #ys #IH #l3 * #H1 #H2 % |
---|
1461 | [ @mem_append_l2 // | @IH // ] |
---|
1462 | qed. |
---|
1463 | |
---|
1464 | lemma lab_to_keep_in_prog : ∀p,p'.∀prog : Program p p'. |
---|
1465 | ∀t_prog,m,keep.trans_prog … prog = 〈t_prog,m,keep〉 → |
---|
1466 | (cast_return_to_cost_labels keep) ⊆ (labels_of_prog p p' prog). |
---|
1467 | #p #p' * #env #main #t_prog #m #keep whd in match trans_prog; normalize nodelta |
---|
1468 | @pair_elim * #env1 #fresh * #m1 #keep1 #EQenv1 normalize nodelta #EQ destruct |
---|
1469 | lapply EQenv1 -EQenv1 lapply keep1 -keep1 lapply m1 -m1 lapply fresh -fresh |
---|
1470 | lapply env1 -env1 generalize in match (fresh_for_prog ???); elim env |
---|
1471 | [ #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct whd in match (append ???); |
---|
1472 | @subset_def #x #H whd in match (labels_of_prog); normalize nodelta |
---|
1473 | whd in match (foldr ?????); cases(memb_cast_return … H) -H #x1 * #EQ1 #H destruct |
---|
1474 | @(lab_to_keep_in_domain … H) |
---|
1475 | | #x #xs #IH #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); @pair_elim |
---|
1476 | * #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail |
---|
1477 | change with (translate_env ????) in match (foldr ?????); #EQt_env_tail |
---|
1478 | normalize nodelta #EQ1 destruct >cast_return_append @subset_append |
---|
1479 | [ >cast_return_append @subset_append |
---|
1480 | [ whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); |
---|
1481 | @subset_def #y #H cases(memb_cast_return … H) -H #y1 * #EQ destruct #H |
---|
1482 | >memb_append_l2 // @(lab_to_keep_in_domain … H) |
---|
1483 | | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); |
---|
1484 | change with (labels_of_prog ?? (mk_Program ?? xs ?)) in match (foldr ?????); |
---|
1485 | @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail)) |
---|
1486 | >cast_return_append @subset_append_h1 // |
---|
1487 | ] |
---|
1488 | | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????); |
---|
1489 | change with (labels_of_prog ?? (mk_Program ?? xs ?)) in match (foldr ?????); |
---|
1490 | @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail)) |
---|
1491 | >cast_return_append @subset_append_h2 // |
---|
1492 | ] |
---|
1493 | ] |
---|
1494 | qed. |
---|
1495 | |
---|
1496 | lemma fresh_call_post_trans_ok : ∀p.∀i : Instructions p.∀n,l. |
---|
1497 | n ≤ fresh … (call_post_trans … i n l). |
---|
1498 | #p #i elim i // |
---|
1499 | qed. |
---|
1500 | |
---|
1501 | lemma fresh_translate_env_ok : ∀p,p'.∀env,t_env : list (env_item p p').∀n,n1,m,keep. |
---|
1502 | translate_env … env n = 〈t_env,n1,m,keep〉 → n ≤ n1. |
---|
1503 | #p #p' #env elim env |
---|
1504 | [ #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct // ] |
---|
1505 | #x #xs #IH #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?); |
---|
1506 | change with (translate_env ????) in match (foldr ?????); @pair_elim |
---|
1507 | * #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail #EQt_env_tail normalize nodelta |
---|
1508 | #EQ destruct @(transitive_le … (IH … EQt_env_tail)) @fresh_call_post_trans_ok |
---|
1509 | qed. |
---|
1510 | |
---|
1511 | |
---|
1512 | lemma trans_env_ok : ∀p : state_params.∀ prog. |
---|
1513 | no_duplicates_labels … prog → |
---|
1514 | let 〈t_prog,m,keep〉 ≝ trans_prog … prog in |
---|
1515 | ∀f,env_it.lookup p p (env … prog) f = return env_it → |
---|
1516 | let dom ≝ get_labels_of_code … (f_body … env_it) in |
---|
1517 | ∃env_it',n.is_fresh_for_return keep n ∧lookup p p (env … t_prog) f = return env_it' ∧ |
---|
1518 | let info ≝ call_post_trans … (f_body … env_it) n (nil ?) in |
---|
1519 | t_code … info = f_body … env_it' ∧ |
---|
1520 | get_element … m (a_call (f_lab … env_it')) = (a_call (f_lab … env_it')) :: gen_labels … info ∧ |
---|
1521 | f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it' ∧ |
---|
1522 | same_fresh_map_on dom m (lab_map … info) ∧ same_to_keep_on dom keep (lab_to_keep … info). |
---|
1523 | #p #prog inversion(trans_prog … prog) * #t_prog0 #m0 #keep0 #EQt_prog |
---|
1524 | lapply EQt_prog normalize nodelta |
---|
1525 | generalize in match keep0 in ⊢ (% → ? → ? → ? → ? → ??(λ_.??(λ_.?%?))); |
---|
1526 | #keep1 #EQkeep1 inversion prog in EQt_prog; #env #main #EQprog |
---|
1527 | whd in match trans_prog; normalize nodelta |
---|
1528 | @pair_elim |
---|
1529 | cut(fresh_for_prog ?? prog ≤ fresh_for_prog ?? (mk_Program … env main)) [ >EQprog //] |
---|
1530 | generalize in match (fresh_for_prog ???) in ⊢ (??% → %); |
---|
1531 | lapply t_prog0 lapply m0 lapply keep0 |
---|
1532 | elim env in ⊢ (?→ ? → ? → ? → ? → %); |
---|
1533 | [ #keep #m #t_prog #n #_ * #env' #fresh * #x #y #_ #_ #_ #f #env_it normalize in ⊢ (% → ?); #ABS destruct] |
---|
1534 | * #hd_sig #hd_lab #hd_code #tail #IH #keep #m #t_prog #fresh1 #Hfresh1 * #env' #fresh * #m' #keep' |
---|
1535 | normalize in ⊢ (% → ?); normalize nodelta @pair_elim * #env_tail #fresh_tail |
---|
1536 | * #m_tail #keep_tail change with (translate_env ????) in ⊢ (??%? → ?); #EQtail normalize nodelta #EQ1 destruct(EQ1) #EQ2 destruct(EQ2) |
---|
1537 | whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H) |
---|
1538 | change with (no_duplicates_labels p p (mk_Program p p tail main)) in match |
---|
1539 | (no_duplicates_labels p p (mk_Program p p tail main)); #no_dup_tail |
---|
1540 | lapply(no_duplicates_append_l … H) #no_dup_head normalize nodelta |
---|
1541 | #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta |
---|
1542 | [ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ) |
---|
1543 | inversion (call_post_trans … hd_code fresh_tail []) |
---|
1544 | #gen_labs #t_hd_code #t_fresh #t_lab_map #t_lab_to_keep #EQ_trans_code |
---|
1545 | %{(mk_env_item … hd_sig hd_lab t_hd_code)} %{fresh_tail} % |
---|
1546 | [ % |
---|
1547 | [ @(fresh_keep_n_ok … fresh1) |
---|
1548 | [ @(fresh_keep_n_ok … Hfresh1) |
---|
1549 | @(fresh_for_subset … (labels_of_prog … prog)) |
---|
1550 | [ @(lab_to_keep_in_prog … EQkeep1) | @is_fresh_fresh_for_prog ] |
---|
1551 | | @(transitive_le … (fresh_translate_env_ok … EQtail)) // |
---|
1552 | ] |
---|
1553 | | whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta |
---|
1554 | @eq_f cases hd_sig // ]] >EQ_trans_code % [% [ % [ % [% // whd in ⊢ (??%?); >(\b (refl …)) %] % ] % | whd |
---|
1555 | #x #Hx whd in ⊢ (??%?); >(? : (x == hd_lab) = false) |
---|
1556 | [2: inversion(x==hd_lab) // #EQx_hdlab cases Hhd_lab -Hhd_lab #Hhd_lab cases Hhd_lab |
---|
1557 | >memb_append_l1 // <(\P EQx_hdlab) >Hx // ] |
---|
1558 | normalize nodelta >get_element_append_l1 |
---|
1559 | [2: % #ABS @(memb_no_duplicates_append … x … H) // elim tail |
---|
1560 | [ whd in match (foldr ?????); @lab_map_in_domain // ] |
---|
1561 | #x #xs #IH whd in match (foldr ?????); @orb_Prop_r |
---|
1562 | >memb_append_l2 // >IH % |
---|
1563 | ] @get_element_append_l1 |
---|
1564 | % #H1 |
---|
1565 | (* subproof with no nice statement *) |
---|
1566 | lapply H1 -H1 lapply H -H lapply Hhd_lab -Hhd_lab lapply EQtail -EQtail |
---|
1567 | generalize in match fresh1; lapply env_tail -env_tail lapply fresh_tail |
---|
1568 | -fresh_tail lapply m_tail -m_tail lapply keep_tail -keep_tail elim tail |
---|
1569 | normalize nodelta |
---|
1570 | [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); |
---|
1571 | #EQ destruct(EQ) whd in match (foldr ?????); |
---|
1572 | #H1 #H2 * ] |
---|
1573 | #head #tail #IH #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); |
---|
1574 | whd in match (foldr ?????); |
---|
1575 | @pair_elim * #env_tail_res #fresh_tail_res * #lab_map_res #keep_res #EQres |
---|
1576 | normalize nodelta #EQ destruct(EQ) whd in match (foldr ?????); |
---|
1577 | #H1 #H2 whd in match (memb ???); inversion(x == ?) |
---|
1578 | [ #H3 #_ <(\P H3) in H2; change with ([?]@?) in match (?::?); #H2 |
---|
1579 | lapply(no_duplicates_append_commute … H2) -H2 ** #ABS #_ @ABS |
---|
1580 | >memb_append_l2 // >Hx % |
---|
1581 | | #H3 normalize nodelta #H4 @(IH … EQres) |
---|
1582 | [3: >domain_of_associative_list_append in H4; #H4 cases(memb_append … H4) [2: #EQ >EQ %] |
---|
1583 | #ABS @⊥ @(memb_no_duplicates_append … x … H2) // @orb_Prop_r >memb_append_l1 // |
---|
1584 | @(lab_map_in_domain … (eq_true_to_b … ABS)) |
---|
1585 | | % #ABS elim H1 -H1 #H1 @H1 cases(memb_append … ABS) |
---|
1586 | [ #H5 >memb_append_l1 // |
---|
1587 | | #H5 >memb_append_l2 // @orb_Prop_r >memb_append_l2 // |
---|
1588 | ] |
---|
1589 | | lapply(no_duplicates_append_commute … H2) * #_ >associative_append |
---|
1590 | #h @no_duplicates_append_commute @(no_duplicates_append_r … h) |
---|
1591 | ] |
---|
1592 | ] |
---|
1593 | ] |
---|
1594 | | whd #x #Hx >memb_append_l12 |
---|
1595 | [2: @notb_Prop % #ABS @(memb_no_duplicates_append … H … Hx) elim tail |
---|
1596 | [ whd in match (foldr ?????); @lab_to_keep_in_domain // ] |
---|
1597 | #x #xs #IH whd in match (foldr ?????); @orb_Prop_r |
---|
1598 | >memb_append_l2 // >IH % |
---|
1599 | ] |
---|
1600 | >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … (a_return_post x) … H) |
---|
1601 | // @⊥ |
---|
1602 | (* subproof with no nice statement *) |
---|
1603 | lapply ABS -ABS lapply H -H lapply Hhd_lab -Hhd_lab lapply EQtail -EQtail |
---|
1604 | generalize in match fresh1; lapply env_tail -env_tail lapply fresh_tail |
---|
1605 | -fresh_tail lapply m_tail -m_tail lapply keep_tail -keep_tail elim tail |
---|
1606 | normalize nodelta |
---|
1607 | [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); |
---|
1608 | #EQ destruct(EQ) whd in match (foldr ?????); |
---|
1609 | #H1 #H2 whd in ⊢ (??%? → ?); #EQ destruct ] |
---|
1610 | #head #tail #IH #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?); |
---|
1611 | whd in match (foldr ?????); |
---|
1612 | @pair_elim * #env_tail_res #fresh_tail_res * #lab_map_res #keep_res #EQres |
---|
1613 | normalize nodelta #EQ destruct(EQ) whd in match (foldr ?????); |
---|
1614 | #H1 #H2 #H3 cases(memb_append … H3) -H3 |
---|
1615 | [ #H3 change with ([?]@?) in match (?::?) in H2; |
---|
1616 | lapply(no_duplicates_append_commute … H2) -H2 * #_ #H4 @(memb_no_duplicates_append … (a_return_post x) … H4) |
---|
1617 | [ whd in match (append ???); >memb_append_l1 // >(lab_to_keep_in_domain … (eq_true_to_b … H3)) % |
---|
1618 | | // |
---|
1619 | ] |
---|
1620 | | #H3 normalize nodelta @(IH … EQres) |
---|
1621 | [3: // |
---|
1622 | | % #ABS elim H1 -H1 #H1 @H1 cases(memb_append … ABS) |
---|
1623 | [ #H5 >memb_append_l1 // |
---|
1624 | | #H5 >memb_append_l2 // @orb_Prop_r >memb_append_l2 // |
---|
1625 | ] |
---|
1626 | | lapply(no_duplicates_append_commute … H2) * #_ >associative_append |
---|
1627 | #h @no_duplicates_append_commute @(no_duplicates_append_r … h) |
---|
1628 | ] |
---|
1629 | ] |
---|
1630 | ] |
---|
1631 | | #Hf #Henv_it cases(IH … no_dup_tail … Henv_it) |
---|
1632 | [9: >EQtail in ⊢ (??%?); % |
---|
1633 | |13: % |
---|
1634 | |6: assumption |
---|
1635 | |10: % |
---|
1636 | |*: |
---|
1637 | ] |
---|
1638 | #new_env_it * #new_fresh ** #is_fresh_newfresh #EQlook_new_env_it ***** #EQt_code #EQ_get_el |
---|
1639 | #EQsign_env_it #EQ_f_lab #same_fresh_map #same_to_keep %{new_env_it} %{new_fresh} |
---|
1640 | % |
---|
1641 | [ % |
---|
1642 | [ assumption |
---|
1643 | | whd in ⊢ (??%?); @eq_function_name_elim [ #ABS >ABS in Hf; * #H @⊥ @H %] |
---|
1644 | #_ normalize nodelta assumption ]] |
---|
1645 | % [2: #x #Hx <same_to_keep // >associative_append @memb_append_l22 |
---|
1646 | inversion(memb ???) // #ABS lapply(lab_to_keep_in_domain … (eq_true_to_b … ABS)) |
---|
1647 | #ABS1 @(memb_no_duplicates_append … (a_return_post x) … H) // |
---|
1648 | cases(lookup_ok_append … Henv_it) #l1 * #l2 * #EQ1 #EQ2 destruct(EQ1 EQ2) |
---|
1649 | >foldr_map_append >memb_append_l2 // >foldr_map_append >memb_append_l1 // |
---|
1650 | whd in match (foldr ?????); @orb_Prop_r >memb_append_l1 // >Hx % ] |
---|
1651 | % [2: #x #Hx <same_fresh_map // >cons_append <associative_append |
---|
1652 | <associative_append in ⊢ (??(???(??%?)?)?); >associative_append |
---|
1653 | @(get_element_append_r1) |
---|
1654 | % >domain_of_associative_list_append #ABS cases(memb_append … ABS) |
---|
1655 | [ whd in match (memb ???); inversion(x==hd_lab) normalize nodelta |
---|
1656 | [2: #_ whd in match (memb ???); #EQ destruct ] #EQx_hdlab #_ |
---|
1657 | <(\P EQx_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it) |
---|
1658 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
1659 | * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 // |
---|
1660 | >memb_append_l1 // whd in ⊢ (??%?); cases(x==?) // |
---|
1661 | normalize nodelta >memb_append_l1 // >Hx % |
---|
1662 | | #ABS1 @(memb_no_duplicates_append … x … H) |
---|
1663 | [ @(lab_map_in_domain … (eq_true_to_b … ABS1)) |
---|
1664 | | cases(lookup_ok_append … Henv_it) |
---|
1665 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
1666 | >memb_append_l2 // >memb_append_l1 // |
---|
1667 | whd in ⊢ (??%?); cases(x==?) // |
---|
1668 | normalize nodelta >memb_append_l1 // >Hx % |
---|
1669 | ] |
---|
1670 | ] |
---|
1671 | ] |
---|
1672 | % // % // % // <EQ_get_el >cons_append <associative_append <associative_append in ⊢ (??(???(??%?)?)?); |
---|
1673 | >associative_append |
---|
1674 | @get_element_append_r1 % >domain_of_associative_list_append #ABS cases(memb_append … ABS) |
---|
1675 | [ whd in match (memb ???); inversion(a_call (f_lab … new_env_it)== a_call hd_lab) |
---|
1676 | #EQ_hdlab normalize nodelta |
---|
1677 | [2: whd in ⊢ (??%? → ?); #EQ destruct ] |
---|
1678 | #_ <(\P EQ_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it) |
---|
1679 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
1680 | * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 // |
---|
1681 | >memb_append_l1 // whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) // |
---|
1682 | | #ABS1 @(memb_no_duplicates_append … (a_call (f_lab … new_env_it)) … H) |
---|
1683 | [ @(lab_map_in_domain … (eq_true_to_b … ABS1)) |
---|
1684 | | cases(lookup_ok_append … Henv_it) |
---|
1685 | #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append |
---|
1686 | >memb_append_l2 // >memb_append_l1 // |
---|
1687 | whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) // |
---|
1688 | ] |
---|
1689 | ] |
---|
1690 | ] |
---|
1691 | qed. |
---|
1692 | |
---|
1693 | lemma len_append : ∀S : abstract_status.∀st1,st2,st3 : S. |
---|
1694 | ∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3. |
---|
1695 | len … (t1 @ t2) = len … t1 + len … t2. |
---|
1696 | #S #st1 #st2 #st3 #t1 elim t1 normalize // |
---|
1697 | qed. |
---|
1698 | |
---|
1699 | axiom permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y. |
---|
1700 | (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7) |
---|
1701 | →is_permutation A ((l6 @l2) @l7) ((l3 @l8) @l9) |
---|
1702 | →is_permutation A |
---|
1703 | (y ::((l6 @((x ::l5) @(l1 @l2))) @l7)) |
---|
1704 | (((x ::l4 @y ::l3) @l8) @l9)). |
---|
1705 | |
---|
1706 | lemma append_premeasurable : ∀S : abstract_status. |
---|
1707 | ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2: raw_trace … st2 st3. |
---|
1708 | pre_measurable_trace … t1 → pre_measurable_trace … t2 → |
---|
1709 | pre_measurable_trace … (t1 @ t2). |
---|
1710 | #S #st1 #st2 #st3 #t1 #t2 #Hpre lapply t2 -t2 elim Hpre -Hpre // |
---|
1711 | [ #s1 #s2 #s3 #l #prf #tl #Hclass #Hcost #pre_tl #IH #t2 #pr3_t2 |
---|
1712 | %2 // @IH // |
---|
1713 | | #s1 #s2 #s3 #l #Hclass #prf #tl #ret_l #pre_tl #IH #t2 #pre_t2 %3 // @IH // |
---|
1714 | | #s1 #s2 #s3 #l #prf #tl #Hclass #call #callp #pre_tl #IH #t2 #pre_t2 %4 // @IH // |
---|
1715 | | #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #tl1 #tl2 #prf2 #Hclass1 #Hclass3 #call_l1 |
---|
1716 | #nopost #pre_tl1 #pre_tl2 #succ #unlab #IH1 #IH2 #t2 #pre_t2 |
---|
1717 | normalize >append_associative in ⊢ (????(???????%)); %5 // @IH2 // |
---|
1718 | ] |
---|
1719 | qed. |
---|
1720 | |
---|
1721 | |
---|
1722 | lemma correctness_lemma : ∀p,p',prog. |
---|
1723 | no_duplicates_labels … prog → |
---|
1724 | let 〈t_prog,m,keep〉 ≝ trans_prog … prog in |
---|
1725 | ∀s1,s2,s1' : state p.∀abs_top,abs_tail. |
---|
1726 | ∀t : raw_trace (operational_semantics … p' prog) s1 s2. |
---|
1727 | pre_measurable_trace … t → |
---|
1728 | state_rel … m keep abs_top abs_tail s1 s1' → |
---|
1729 | ∃abs_top',abs_tail'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'. |
---|
1730 | state_rel … m keep abs_top' abs_tail' s2 s2' ∧ |
---|
1731 | is_permutation ? ((abs_top @ (map_labels_on_trace m (get_costlabels_of_trace … t))) @ abs_tail) |
---|
1732 | (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail') ∧ |
---|
1733 | len … t = len … t' ∧ |
---|
1734 | (∀k.∀i.option_hd … (cont … s2) = Some ? 〈ret_act (None ?),i〉 → |
---|
1735 | cont … s1 = k @ cont … s2 → |
---|
1736 | ∃k'.cont … s1' = k' @ cont … s2' ∧ |k| = |k'|) |
---|
1737 | ∧ pre_measurable_trace … t'. |
---|
1738 | #p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans |
---|
1739 | #s1 #s2 #s1' #abs_top #abs_tail #t #Hpre lapply abs_top -abs_top lapply abs_tail |
---|
1740 | -abs_tail lapply s1' -s1' elim Hpre |
---|
1741 | [ #st #Hst #s1' #abs_tail #abs_top #H %{abs_top} %{abs_tail} %{s1'} %{(t_base …)} |
---|
1742 | % |
---|
1743 | [ % |
---|
1744 | [ % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil |
---|
1745 | @is_permutation_eq |
---|
1746 | | #k #i #_ #EQcont_st %{[ ]} % // @sym_eq @eq_f @append_l1_injective_r // |
---|
1747 | ] |
---|
1748 | | %1 whd in H; cases(check_continuations ?????) in H; [*] ** #H1 #abs_top_cont |
---|
1749 | #abs_tail_cont normalize nodelta **** #_ #rel #_ #H2 #_ normalize |
---|
1750 | inversion(code ??) normalize nodelta |
---|
1751 | [|#r_t| #seq #lbl #i #_ | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ |
---|
1752 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ | #f #act_p #rlbl #i #_ |
---|
1753 | | #lin #io #lout #i #_ ] |
---|
1754 | #EQcode_s1' normalize nodelta [|*: % #EQ destruct] <H2 |
---|
1755 | >EQcode_s1' in rel; whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
1756 | normalize in Hst; <e1 in Hst; normalize nodelta // |
---|
1757 | ] |
---|
1758 | | #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12 |
---|
1759 | [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore |
---|
1760 | #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #class_st11 * #opt_l #EQ destruct(EQ) |
---|
1761 | #pre_tl #IH #s1' #abs_tail #abs_top whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?); |
---|
1762 | whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????); |
---|
1763 | inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1' |
---|
1764 | normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????); |
---|
1765 | inversion(check_continuations ?????) [ #_ *] ** #H1 #l2 #ll2 #EQHl2 |
---|
1766 | >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ ***** ] |
---|
1767 | * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta |
---|
1768 | cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta |
---|
1769 | [ #x #y #_ (*#_ #_ #_ #H*) ***** |
---|
1770 | | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1; |
---|
1771 | normalize * /2/ ] * |
---|
1772 | [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ) |
---|
1773 | #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1') |
---|
1774 | [ |
---|
1775 | | #x |
---|
1776 | | #seq #lbl #i #_ |
---|
1777 | | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ |
---|
1778 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ |
---|
1779 | | #f #act_p #ret_post #i #_ |
---|
1780 | | #l_in #io #l_out #i #_ |
---|
1781 | ] |
---|
1782 | [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)] |
---|
1783 | cases(call_post_clean ?????) normalize nodelta |
---|
1784 | [1,3,5,7,9: #EQ destruct(EQ)] |
---|
1785 | [ * #z1 #z2 cases lbl normalize nodelta [|#z3 cases(?==?) normalize nodelta] |
---|
1786 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1787 | | * #z1 #z2 cases(call_post_clean ?????) [| * #z3 #z4 ] whd in ⊢ (??%% → ?); |
---|
1788 | [2: cases(call_post_clean ?????) normalize nodelta |
---|
1789 | [| * #z5 #z6 cases(?∧?) normalize nodelta]] whd in ⊢ (??%% → ?); |
---|
1790 | #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1791 | | * #z1 #z2 cases(call_post_clean ?????) |
---|
1792 | [| * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta] |
---|
1793 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1794 | | * #z1 #z2 cases ret_post normalize nodelta |
---|
1795 | [| #z3 cases(memb ???) normalize nodelta [ cases(?==?) normalize nodelta] ] |
---|
1796 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1797 | | * #z1 #z2 cases(?∧?) normalize nodelta |
---|
1798 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1799 | ] |
---|
1800 | ] |
---|
1801 | #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ) |
---|
1802 | cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …) |
---|
1803 | [2: whd whd in match check_continuations; normalize nodelta |
---|
1804 | change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2 |
---|
1805 | normalize nodelta % // % // % // % // @EQcode_c_st12 ] |
---|
1806 | #abs_top' * #abs_tail' * #st3' * #t' **** |
---|
1807 | #Hst3st3' #EQcosts #EQlen #stack_safety #pre_t' |
---|
1808 | %{abs_top'} %{abs_tail'} %{st3'} %{(t_ind … (cost_act (None ?)) … t')} |
---|
1809 | [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉) |
---|
1810 | [3: assumption |4: assumption |*:] /3 by nmk/ ] |
---|
1811 | % |
---|
1812 | [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts] |
---|
1813 | * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%); |
---|
1814 | [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ] |
---|
1815 | destruct cases(stack_safety … EQcont_st3 … e0) #k1 * |
---|
1816 | #EQk1 #EQlength %{(〈cost_act (None ?),new_code'〉::k1)} |
---|
1817 | % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ] ] |
---|
1818 | %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio11 |
---|
1819 | normalize in class_st11; >EQcode11 in class_st11; // |
---|
1820 | | #lbl #EQconts1' normalize nodelta ******* #EQ destruct(EQ) |
---|
1821 | #HH1 #EQ destruct(EQ) #EQget_el >EQcode11 in ⊢ (% → ?); |
---|
1822 | inversion(code … s1') |
---|
1823 | [ |
---|
1824 | | #x |
---|
1825 | | #seq #lbl #i #_ |
---|
1826 | | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ |
---|
1827 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ |
---|
1828 | | #f #act_p #ret_post #i #_ |
---|
1829 | | #l_in #io #l_out #i #_ |
---|
1830 | ] |
---|
1831 | [|*: #_ whd in ⊢ (??%% → ?); |
---|
1832 | [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1833 | | cases(call_post_clean ?????) normalize nodelta |
---|
1834 | [| * #z2 #z3 cases lbl normalize nodelta |
---|
1835 | [| #z4 cases(?==?) normalize nodelta] ] |
---|
1836 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1837 | | cases(call_post_clean ?????) normalize nodelta |
---|
1838 | [| * #z2 #z3 cases(call_post_clean ?????) |
---|
1839 | [| * #z4 #z5 >m_return_bind cases(call_post_clean ?????) |
---|
1840 | [| * #z6 #z7 >m_return_bind cases(?∧?) normalize nodelta ]]] |
---|
1841 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1842 | | cases(call_post_clean ?????) normalize nodelta |
---|
1843 | [| * #z2 #z3 cases(call_post_clean ?????) |
---|
1844 | [| * #z4 #z5 >m_return_bind cases(?∧?) normalize nodelta ]] |
---|
1845 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1846 | | cases(call_post_clean ?????) normalize nodelta |
---|
1847 | [| * #z1 #z2 cases ret_post normalize nodelta |
---|
1848 | [| #z3 cases(memb ???) normalize nodelta |
---|
1849 | [ cases (?==?) normalize nodelta]]] |
---|
1850 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1851 | | cases(call_post_clean ?????) normalize nodelta |
---|
1852 | [| * #z1 #z2 cases(?∧?) normalize nodelta ] |
---|
1853 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1854 | ] |
---|
1855 | ] |
---|
1856 | #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore #EQio #EQ destruct(EQ) |
---|
1857 | cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 l3 …) |
---|
1858 | [2: whd whd in match check_continuations; normalize nodelta |
---|
1859 | change with (check_continuations ?????) in match (foldr2 ???????); |
---|
1860 | >EQHl2 in ⊢ (match % with [ _⇒ ? | _ ⇒ ?]); |
---|
1861 | normalize nodelta % // % // % // % // @EQcode_c_st12 ] |
---|
1862 | #abs_top' * #abs_tail' * #st3' * #t' **** #Hst3st3' #EQcost #EQlen #stack_safety |
---|
1863 | #pre_t' |
---|
1864 | %{abs_top'} %{abs_tail'} %{st3'} |
---|
1865 | %{(t_ind … (cost_act (Some ? lbl)) … t')} |
---|
1866 | [ @hide_prf whd @(empty ????? 〈(cost_act (Some ? lbl)),?〉) |
---|
1867 | [3: assumption |4: assumption |*:] /3 by nmk/ ] |
---|
1868 | % |
---|
1869 | [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} |
---|
1870 | >(map_labels_on_trace_append … [lbl]) (*CSC: funzionava prima*) |
---|
1871 | whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el |
---|
1872 | @is_permutation_cons assumption |
---|
1873 | | * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%); |
---|
1874 | [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ] |
---|
1875 | destruct cases(stack_safety … EQcont_st3 … e0) #k1 * |
---|
1876 | #EQk1 #EQlength %{(〈cost_act (Some ? lbl),new_code'〉::k1)} |
---|
1877 | % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ] |
---|
1878 | ]] |
---|
1879 | %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio |
---|
1880 | normalize in class_st11; >EQcode11 in class_st11; // |
---|
1881 | ] |
---|
1882 | | #seq #i #mem * [|#lbl] #EQcode_st11 #EQeval_seq #EQ destruct(EQ) #EQcont |
---|
1883 | #EQ destruct(EQ) #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hst11 |
---|
1884 | #_ #Hpre_t #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); |
---|
1885 | inversion(check_continuations ?????) normalize nodelta [1,3: #_ *] |
---|
1886 | ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** |
---|
1887 | #HH1 [ >EQcode_st11 in ⊢ (% → ?); | >EQcode_st11 in ⊢ (% → ?); ] |
---|
1888 | inversion(code ??) |
---|
1889 | [1,2,4,5,6,7,8,9,11,12,13,14: |
---|
1890 | [1,7: #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1891 | |2,8: #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1892 | |3,9: #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ |
---|
1893 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
1894 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
1895 | [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) |
---|
1896 | [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] |
---|
1897 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1898 | |4,10: #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ |
---|
1899 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
1900 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
1901 | [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] |
---|
1902 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1903 | |5,11: #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
1904 | normalize nodelta |
---|
1905 | [2,4: * #z1 #z2 cases lbl normalize nodelta |
---|
1906 | [2,4: #l1 cases(memb ???) normalize nodelta |
---|
1907 | [1,3: cases(?==?) normalize nodelta ]]] |
---|
1908 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1909 | |6,12: #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
1910 | normalize nodelta |
---|
1911 | [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] |
---|
1912 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1913 | ] |
---|
1914 | ] |
---|
1915 | #seq1 #opt_l #i' #_ #EQcode_s1' |
---|
1916 | change with (m_bind ?????) in ⊢ (??%? → ?); |
---|
1917 | inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
1918 | * #gen_labs #i'' #EQclean >m_return_bind inversion(opt_l) normalize nodelta |
---|
1919 | [2,4: #lab1 ] #EQ destruct(EQ) |
---|
1920 | [1,2: inversion(?==?) normalize nodelta #EQget_el ] |
---|
1921 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1922 | #EQstore #EQinfo #EQ destruct(EQ) |
---|
1923 | cases(IH … (mk_state ? i' (cont … s1') (store … st12) (io_info … s1')) abs_tail_cont ?) |
---|
1924 | [3,6: whd |
---|
1925 | [ <EQcont in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); >EQcheck in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); |
---|
1926 | | <EQcont in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); >EQcheck in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); |
---|
1927 | ] |
---|
1928 | normalize nodelta % // % // % // % // assumption |
---|
1929 | |2,5: |
---|
1930 | ] |
---|
1931 | #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety |
---|
1932 | #pre_t' %{abs_top1} |
---|
1933 | %{abs_tail1} %{s2'} %{(t_ind … t')} |
---|
1934 | [1,4: @hide_prf @(seq_sil … EQcode_s1') // |
---|
1935 | |2,5: |
---|
1936 | ] |
---|
1937 | % [1,3: % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} [2: assumption] |
---|
1938 | whd in ⊢ (??%%); whd in match (get_costlabels_of_trace ????); |
---|
1939 | whd in match (map_labels_on_trace ??); >(\P EQget_el) @is_permutation_cons |
---|
1940 | assumption |
---|
1941 | |*: #k #i #EQcont_st3 >EQcont #EQ |
---|
1942 | cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % // |
---|
1943 | ]] |
---|
1944 | %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct |
---|
1945 | | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12 |
---|
1946 | #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t |
---|
1947 | #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????) |
---|
1948 | [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1 |
---|
1949 | >EQcode_st11 in ⊢ (% → ?); inversion(code ??) |
---|
1950 | [1,2,3,5,6,7: |
---|
1951 | [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1952 | | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1953 | | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
1954 | normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta |
---|
1955 | [2: #l1 cases(?==?) normalize nodelta]] |
---|
1956 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1957 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ |
---|
1958 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
1959 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
1960 | [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] |
---|
1961 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1962 | | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
1963 | normalize nodelta |
---|
1964 | [2,4: * #z1 #z2 cases lbl normalize nodelta |
---|
1965 | [2,4: #l1 cases(memb ???) normalize nodelta |
---|
1966 | [1,3: cases(?==?) normalize nodelta ]]] |
---|
1967 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1968 | | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
1969 | normalize nodelta |
---|
1970 | [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] |
---|
1971 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
1972 | ] |
---|
1973 | ] |
---|
1974 | #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_ |
---|
1975 | #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta |
---|
1976 | [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????) |
---|
1977 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_ifalse1 #i_false' #EQi_false' |
---|
1978 | >m_return_bind inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
1979 | * #gen_lab_i_true' #i_true' #EQi_true' >m_return_bind inversion(?==?) normalize nodelta |
---|
1980 | [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) normalize nodelta #EQget_lfalse1 |
---|
1981 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQio11 |
---|
1982 | #EQ destruct(EQ) |
---|
1983 | cases(IH … |
---|
1984 | (mk_state ? i_true1 (〈cost_act (None ?),i'〉 :: cont … s1') (store … st12) (io_info … st12)) |
---|
1985 | abs_tail_cont gen_lab_i_true') |
---|
1986 | [2: whd whd in match (check_continuations ?????); |
---|
1987 | >EQcont_st12 in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); whd in match (foldr2 ???????); |
---|
1988 | change with (check_continuations ?????) in match (foldr2 ???????); |
---|
1989 | >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta |
---|
1990 | >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % // |
---|
1991 | ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen |
---|
1992 | #stack_safety #pre_t' %{abs_top1} %{abs_tail1} |
---|
1993 | %{s2'} %{(t_ind … t')} |
---|
1994 | [ @hide_prf @(cond_true … EQcode_s1') // |
---|
1995 | | |
---|
1996 | ] |
---|
1997 | % [ % |
---|
1998 | [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} |
---|
1999 | whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??); |
---|
2000 | >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons |
---|
2001 | assumption |
---|
2002 | | #k #i1 #EQcont_st3 #EQcont_st11 |
---|
2003 | cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …) |
---|
2004 | [2: >EQcont_st12 >EQcont_st11 % ] |
---|
2005 | * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct |
---|
2006 | %{tl1} % // whd in EQk1 : (??%%); destruct // |
---|
2007 | ]] |
---|
2008 | %2 // [2: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct |
---|
2009 | | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12 |
---|
2010 | #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t |
---|
2011 | #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????) |
---|
2012 | [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1 |
---|
2013 | >EQcode_st11 in ⊢ (% → ?); inversion(code ??) |
---|
2014 | [1,2,3,5,6,7: |
---|
2015 | [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2016 | | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2017 | | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2018 | normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta |
---|
2019 | [2: #l1 cases(?==?) normalize nodelta]] |
---|
2020 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2021 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ |
---|
2022 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2023 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2024 | [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] |
---|
2025 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2026 | | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2027 | normalize nodelta |
---|
2028 | [2,4: * #z1 #z2 cases lbl normalize nodelta |
---|
2029 | [2,4: #l1 cases(memb ???) normalize nodelta |
---|
2030 | [1,3: cases(?==?) normalize nodelta ]]] |
---|
2031 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2032 | | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2033 | normalize nodelta |
---|
2034 | [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] |
---|
2035 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2036 | ] |
---|
2037 | ] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_ |
---|
2038 | #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta |
---|
2039 | [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????) |
---|
2040 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_ifalse1 #i_false' #EQi_false' |
---|
2041 | >m_return_bind inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
2042 | * #gen_lab_i_true' #i_true' #EQi_true' >m_return_bind inversion(?==?) normalize nodelta |
---|
2043 | [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) normalize nodelta #EQget_lfalse1 |
---|
2044 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQio11 |
---|
2045 | #EQ destruct(EQ) |
---|
2046 | cases(IH … |
---|
2047 | (mk_state ? ifalse1 (〈cost_act (None ?),i'〉 :: cont … s1') (store … st12) (io_info … st12)) |
---|
2048 | abs_tail_cont gen_lab_ifalse1) |
---|
2049 | [2: whd whd in match (check_continuations ?????); |
---|
2050 | >EQcont_st12 in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); whd in match (foldr2 ???????); |
---|
2051 | change with (check_continuations ?????) in match (foldr2 ???????); |
---|
2052 | >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta |
---|
2053 | >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % // |
---|
2054 | ] #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcost #EQlen #stack_safety |
---|
2055 | #pre_t' |
---|
2056 | %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')} |
---|
2057 | [ @hide_prf @(cond_false … EQcode_s1') // |
---|
2058 | | |
---|
2059 | ] |
---|
2060 | % [ % |
---|
2061 | [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} |
---|
2062 | whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??); |
---|
2063 | >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons |
---|
2064 | assumption |
---|
2065 | | #k #i1 #EQcont_st3 #EQcont_st11 |
---|
2066 | cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …) |
---|
2067 | [2: >EQcont_st12 >EQcont_st11 % ] |
---|
2068 | * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct |
---|
2069 | %{tl1} % // whd in EQk1 : (??%%); destruct // |
---|
2070 | ] ] |
---|
2071 | %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct |
---|
2072 | | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct |
---|
2073 | #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail |
---|
2074 | whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont |
---|
2075 | #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??) |
---|
2076 | [1,2,3,4,6,7: |
---|
2077 | [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2078 | | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2079 | | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2080 | normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta |
---|
2081 | [2: #l1 cases(?==?) normalize nodelta]] |
---|
2082 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2083 | | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ |
---|
2084 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2085 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2086 | [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) |
---|
2087 | [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] |
---|
2088 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2089 | | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2090 | normalize nodelta |
---|
2091 | [2,4: * #z1 #z2 cases lbl normalize nodelta |
---|
2092 | [2,4: #l1 cases(memb ???) normalize nodelta |
---|
2093 | [1,3: cases(?==?) normalize nodelta ]]] |
---|
2094 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2095 | | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2096 | normalize nodelta |
---|
2097 | [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] |
---|
2098 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2099 | ] |
---|
2100 | ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_ |
---|
2101 | #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta |
---|
2102 | [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????) |
---|
2103 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct ] * #gen_itrue1 #i_true2 #EQi_true2 >m_return_bind |
---|
2104 | inversion (?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1 |
---|
2105 | inversion(?==?) #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) |
---|
2106 | -EQ #EQ destruct(EQ) #EQstore_11 #EQ_info11 #EQ destruct |
---|
2107 | cases(IH … |
---|
2108 | (mk_state ? i_true1 |
---|
2109 | (〈cost_act (None ?),LOOP … cond ltrue i_true1 lfalse i_false1〉 :: |
---|
2110 | cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_itrue1) |
---|
2111 | [2: whd >EQcont_st12 whd in match (check_continuations ?????); |
---|
2112 | whd in match (foldr2 ???????); |
---|
2113 | change with (check_continuations ?????) in match (foldr2 ???????); |
---|
2114 | >EQcheck normalize nodelta whd in match (call_post_clean ?????); |
---|
2115 | >EQi_false2 normalize nodelta >EQi_true2 >m_return_bind >EQget_ltrue1 |
---|
2116 | >EQget_lfalse1 normalize nodelta % // % // % // % [2: assumption] % // |
---|
2117 | % // |
---|
2118 | ] |
---|
2119 | #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety |
---|
2120 | #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')} |
---|
2121 | [ @hide_prf @(loop_true … EQcode_s1') // |] |
---|
2122 | % [ % |
---|
2123 | [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'} |
---|
2124 | whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??); |
---|
2125 | >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); |
---|
2126 | @is_permutation_cons assumption |
---|
2127 | | #k #i1 #EQcont_st3 #EQcont_st11 |
---|
2128 | cases(stack_safety … (〈cost_act (None NonFunctionalLabel), LOOP p cond ltrue (code p st12) lfalse i_false〉::k) … EQcont_st3 …) |
---|
2129 | [2: >EQcont_st12 >EQcont_st11 % ] |
---|
2130 | * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct |
---|
2131 | %{tl1} % // whd in EQk1 : (??%%); destruct // |
---|
2132 | ] ] |
---|
2133 | %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct |
---|
2134 | | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct |
---|
2135 | #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail |
---|
2136 | whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont |
---|
2137 | #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??) |
---|
2138 | [1,2,3,4,6,7: |
---|
2139 | [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2140 | | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2141 | | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2142 | normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta |
---|
2143 | [2: #l1 cases(?==?) normalize nodelta]] |
---|
2144 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2145 | | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ |
---|
2146 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2147 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2148 | [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) |
---|
2149 | [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] |
---|
2150 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2151 | | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2152 | normalize nodelta |
---|
2153 | [2,4: * #z1 #z2 cases lbl normalize nodelta |
---|
2154 | [2,4: #l1 cases(memb ???) normalize nodelta |
---|
2155 | [1,3: cases(?==?) normalize nodelta ]]] |
---|
2156 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2157 | | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2158 | normalize nodelta |
---|
2159 | [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] |
---|
2160 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2161 | ] |
---|
2162 | ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_ |
---|
2163 | #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta |
---|
2164 | [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????) |
---|
2165 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct ] * #gen_itrue1 #i_true2 #EQi_true2 >m_return_bind |
---|
2166 | inversion (?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1 |
---|
2167 | inversion(?==?) #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) |
---|
2168 | -EQ #EQ destruct(EQ) #EQstore_11 #EQ_info11 #EQ destruct |
---|
2169 | cases(IH … |
---|
2170 | (mk_state ? i_false1 |
---|
2171 | (cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_ifalse1) |
---|
2172 | [2: whd >EQcont_st12 whd in match (check_continuations ?????); |
---|
2173 | whd in match (foldr2 ???????); |
---|
2174 | change with (check_continuations ?????) in match (foldr2 ???????); |
---|
2175 | >EQcheck normalize nodelta whd in match (call_post_clean ?????); |
---|
2176 | >EQi_false2 normalize nodelta >EQi_true2 |
---|
2177 | % // % // % // % [2: %] // |
---|
2178 | ] |
---|
2179 | #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety |
---|
2180 | #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')} |
---|
2181 | [ @hide_prf @(loop_false … EQcode_s1') // |] |
---|
2182 | % [ % |
---|
2183 | [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'} |
---|
2184 | whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??); |
---|
2185 | >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); |
---|
2186 | @is_permutation_cons assumption |
---|
2187 | | #k #i #EQcont_st3 <EQcont_st12 #EQ |
---|
2188 | cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % // |
---|
2189 | ]] |
---|
2190 | %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct |
---|
2191 | | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12 |
---|
2192 | #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre |
---|
2193 | #IH #s1' #abs_top #abs_tail whd in ⊢ (% → ?); inversion(check_continuations ?????) |
---|
2194 | [#_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** |
---|
2195 | #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??) |
---|
2196 | [1,2,3,4,5,6: |
---|
2197 | [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2198 | | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2199 | | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2200 | normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta |
---|
2201 | [2: #l1 cases(?==?) normalize nodelta]] |
---|
2202 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2203 | | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ |
---|
2204 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2205 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2206 | [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) |
---|
2207 | [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] |
---|
2208 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2209 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ |
---|
2210 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2211 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2212 | [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] |
---|
2213 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2214 | | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2215 | normalize nodelta |
---|
2216 | [2,4: * #z1 #z2 cases lbl normalize nodelta |
---|
2217 | [2,4: #l1 cases(memb ???) normalize nodelta |
---|
2218 | [1,3: cases(?==?) normalize nodelta ]]] |
---|
2219 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2220 | ] |
---|
2221 | ] #lin1 #io1 #lout1 #i1 #_ #EQcode_s1' |
---|
2222 | whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta |
---|
2223 | [ #_ #EQ destruct] * #gen_lab #i2 #EQ_i2 inversion(?==?) normalize nodelta |
---|
2224 | [2: #_ #EQ destruct] #EQget_lout1 inversion(?==?) #EQget_lin1 normalize nodelta |
---|
2225 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2226 | #EQstore11 #EQinfo11 #EQ destruct |
---|
2227 | cases(IH … |
---|
2228 | (mk_state ? (EMPTY p) (〈cost_act (Some ? lout),i1〉::cont … s1') (store … st12) true) |
---|
2229 | abs_tail_cont [ ]) |
---|
2230 | [2: whd >EQcont_st12 whd in match (check_continuations ?????); |
---|
2231 | whd in match (foldr2 ???????); |
---|
2232 | change with (check_continuations ?????) in match (foldr2 ???????); |
---|
2233 | >EQcheck normalize nodelta >EQ_i2 normalize nodelta % // % // % // % |
---|
2234 | [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) % |
---|
2235 | ] |
---|
2236 | #abs_cont1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety |
---|
2237 | #pre_t' %{abs_cont1} %{abs_tail1} %{s2'} %{(t_ind … t')} |
---|
2238 | [ @hide_prf @(io_in … EQcode_s1') // |] |
---|
2239 | % [ % |
---|
2240 | [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'} |
---|
2241 | whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??); |
---|
2242 | >(\P EQget_lin1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); |
---|
2243 | @is_permutation_cons assumption |
---|
2244 | | #k #i1 #EQcont_st3 #EQcont_st11 |
---|
2245 | cases(stack_safety … (〈cost_act (Some ? lout),i〉::k) … EQcont_st3 …) |
---|
2246 | [2: >EQcont_st12 >EQcont_st11 %] |
---|
2247 | * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct |
---|
2248 | %{tl1} % // whd in EQk1 : (??%%); destruct // |
---|
2249 | ]] |
---|
2250 | %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct |
---|
2251 | | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 |
---|
2252 | #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ) |
---|
2253 | | #r_t #mem #con #rb #i #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 #EQ11 #EQ12 |
---|
2254 | destruct #t #_ * #nf #EQ destruct |
---|
2255 | ] |
---|
2256 | | #st1 #st2 #st3 #lab #st1_noio #H inversion H in ⊢ ?; |
---|
2257 | [1,2,3,4,5,6,7,8: |
---|
2258 | [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 |
---|
2259 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 |
---|
2260 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 |
---|
2261 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 |
---|
2262 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 |
---|
2263 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 |
---|
2264 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 |
---|
2265 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21 |
---|
2266 | ] |
---|
2267 | destruct #tl * #y #EQ destruct(EQ) @⊥ >EQ in x12; * #ABS @ABS % |
---|
2268 | ] |
---|
2269 | #st11 #st12 #r_t #mem #cont * [|#x] #i #EQcode_st11 #EQcont_st11 #EQ destruct(EQ) |
---|
2270 | #EQio_11 #EQio_12 #EQev_ret #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct(EQ1 EQ2 EQ3 EQ4 EQ5 EQ6) |
---|
2271 | #t * #lbl #EQ destruct(EQ) #pre_t #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); |
---|
2272 | inversion(check_continuations …) [#_ *] ** #H1 #abs_top_cont #abs_tail_cont |
---|
2273 | >EQcont_st11 in ⊢ (% → ?); inversion(cont … s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)] |
---|
2274 | * #act_lab #i #cont_s1'' #_ #EQcont_s1' whd in ⊢ (??%% → ?); |
---|
2275 | change with (check_continuations ?????) in match (foldr2 ???????); |
---|
2276 | inversion(check_continuations ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
2277 | ** #H2 #abs_top_cont' #abs_tail_cont' #EQcheck normalize nodelta |
---|
2278 | inversion(call_post_clean ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct *****] |
---|
2279 | * #gen_labs #i' #EQi' inversion act_lab normalize nodelta |
---|
2280 | [ #f #lab | * [| #lbl1 ]| * [| #nf_l]] #EQ destruct(EQ) |
---|
2281 | [1,6: whd in ⊢ (??%% → ?); #EQ destruct ***** |
---|
2282 | |4,5: normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** [2: *] #EQ destruct |
---|
2283 | ] |
---|
2284 | whd in match ret_costed_abs; normalize nodelta |
---|
2285 | [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** #EQ destruct(EQ) ] |
---|
2286 | inversion (memb ???) normalize nodelta #Hlbl1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
2287 | ****** [ * ] #EQ destruct(EQ) #HH2 #EQ destruct #EQget_el >EQcode_st11 in ⊢ (% → ?); |
---|
2288 | inversion(code … s1') |
---|
2289 | [1,3,4,5,6,7: |
---|
2290 | [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2291 | | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2292 | normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta |
---|
2293 | [2: #l1 cases(?==?) normalize nodelta]] |
---|
2294 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2295 | | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ |
---|
2296 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2297 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2298 | [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) |
---|
2299 | [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] |
---|
2300 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2301 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ |
---|
2302 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2303 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2304 | [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] |
---|
2305 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2306 | | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2307 | normalize nodelta |
---|
2308 | [2,4: * #z1 #z2 cases lbl normalize nodelta |
---|
2309 | [2,4: #l1 cases(memb ???) normalize nodelta |
---|
2310 | [1,3: cases(?==?) normalize nodelta ]]] |
---|
2311 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2312 | | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2313 | normalize nodelta |
---|
2314 | [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] |
---|
2315 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2316 | ] |
---|
2317 | ] |
---|
2318 | #r_t' #EQcode_s1' |
---|
2319 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2320 | #EQstore11 #EQio_11 #EQ destruct |
---|
2321 | cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs) |
---|
2322 | [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ] |
---|
2323 | #abs_top1 * #abs_tail1 * #s2' * #t' **** #Hst3_s2' #EQcosts #EQlen #stack_safety |
---|
2324 | #pre_t' %{abs_top1} %{abs_tail1} %{s2'} %{(t_ind … t')} |
---|
2325 | [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') // |
---|
2326 | | ] |
---|
2327 | % [ % |
---|
2328 | [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'} |
---|
2329 | whd in match (get_costlabels_of_trace ????); |
---|
2330 | whd in match (get_costlabels_of_trace ????) in ⊢ (???%); |
---|
2331 | whd in match (map_labels_on_trace ??); >EQget_el @is_permutation_cons |
---|
2332 | assumption |
---|
2333 | | * [| #hd #tl] #i1 #EQcont_st3 >EQcont_st11 #EQ whd in EQ : (???%); |
---|
2334 | [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ] |
---|
2335 | destruct cases(stack_safety … EQcont_st3 … e0) #k1 * |
---|
2336 | #EQk1 #EQlength %{(〈ret_act (Some ? lbl1),i〉::k1)} |
---|
2337 | % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ] |
---|
2338 | ]] |
---|
2339 | %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct |
---|
2340 | | #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12 |
---|
2341 | [1,2,3,4,5,6,7,9: |
---|
2342 | [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 |
---|
2343 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 |
---|
2344 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 |
---|
2345 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 |
---|
2346 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 |
---|
2347 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 |
---|
2348 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 |
---|
2349 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 |
---|
2350 | ] |
---|
2351 | destruct * #z1 * #z2 #EQ destruct(EQ) whd in ⊢ (?% → ?); >x3 in ⊢ (% → ?); * |
---|
2352 | | #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem |
---|
2353 | #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 |
---|
2354 | destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #_ #_ whd in ⊢ (?% → ?); >EQcode11 in ⊢ (% → ?); |
---|
2355 | normalize nodelta cases opt_l in EQcode11 EQcont12; normalize nodelta [ #x #y *] |
---|
2356 | #lbl #EQcode11 #EQcont12 * #pre_tl #IH #st1' #abs_top #abs_tail |
---|
2357 | whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1 |
---|
2358 | #abs_top_cont #abs_tail_cont #EQcheck |
---|
2359 | normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1') |
---|
2360 | [1,2,3,4,5,7: |
---|
2361 | [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2362 | | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2363 | | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2364 | normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta |
---|
2365 | [2: #l1 cases(?==?) normalize nodelta]] |
---|
2366 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2367 | | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ |
---|
2368 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2369 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2370 | [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) |
---|
2371 | [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] |
---|
2372 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2373 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ |
---|
2374 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2375 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2376 | [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] |
---|
2377 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2378 | | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2379 | normalize nodelta |
---|
2380 | [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] |
---|
2381 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2382 | ] |
---|
2383 | ] #f' #act_p' #opt_l' #i' #_ |
---|
2384 | #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ) |
---|
2385 | lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H |
---|
2386 | cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' |
---|
2387 | #EQenv_it' ***** #EQtrans |
---|
2388 | #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep cases daemon (*CSC: WAS WORKING |
---|
2389 | change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean; |
---|
2390 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind |
---|
2391 | inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta |
---|
2392 | [2: inversion(memb ???) normalize nodelta #Hlbl_keep |
---|
2393 | [ inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
2394 | #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta |
---|
2395 | [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_ |
---|
2396 | lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta |
---|
2397 | [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'') |
---|
2398 | #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ |
---|
2399 | #EQ destruct(EQ) |
---|
2400 | 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 ?)))) |
---|
2401 | [2: whd >EQcont12 |
---|
2402 | change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????); |
---|
2403 | >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l' |
---|
2404 | whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta |
---|
2405 | % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans |
---|
2406 | @(inverse_call_post_trans … is_fresh_fresh') |
---|
2407 | [2: % |*: [2,3: /2 by / ] |
---|
2408 | cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2 |
---|
2409 | whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append |
---|
2410 | #no_dup lapply(no_duplicates_append_r … no_dup) #H1 |
---|
2411 | lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1 |
---|
2412 | change with ([?]@?) in match (?::?); #H1 |
---|
2413 | lapply(no_duplicates_append_r … H1) >append_nil // |
---|
2414 | ] |
---|
2415 | ] |
---|
2416 | #abs_top''' * #abs_tail''' * #st3' * #t' **** #Hst3st3' #EQcosts #EQlen #stack_safety |
---|
2417 | #pre_t' %{abs_top'''} |
---|
2418 | %{abs_tail'''} %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) … t')} |
---|
2419 | [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] |
---|
2420 | % [ % |
---|
2421 | [ % [2: whd in ⊢ (??%%); >EQlen %] |
---|
2422 | %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%); |
---|
2423 | >EQlab_env_it >associative_append whd in match (append ???); >associative_append |
---|
2424 | >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%); |
---|
2425 | whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons |
---|
2426 | >append_nil whd in match (append ???) in ⊢ (???%); // |
---|
2427 | | #k #i1 #EQcont_st3 #EQcont_st11 |
---|
2428 | cases(stack_safety … (〈ret_act (Some ? lbl),i〉::k) … EQcont_st3 …) |
---|
2429 | [2: >EQcont12 >EQcont_st11 % ] |
---|
2430 | * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct |
---|
2431 | %{tl1} % // whd in EQk1 : (??%%); destruct // |
---|
2432 | ]] |
---|
2433 | %4 // [2,4: % [2: % // |]] normalize >EQcode_st1' normalize nodelta % #EQ destruct |
---|
2434 | | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2435 | ] |
---|
2436 | | whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
2437 | ] *) |
---|
2438 | ] |
---|
2439 | | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?; |
---|
2440 | [1,2,3,4,5,6,7,9: |
---|
2441 | [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 |
---|
2442 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 |
---|
2443 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 |
---|
2444 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 |
---|
2445 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 |
---|
2446 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 |
---|
2447 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 |
---|
2448 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 |
---|
2449 | ] |
---|
2450 | destruct #t1 #t2 #prf #_ #_ * #y1 * #y2 #EQ destruct(EQ) @⊥ >EQ in x12; * #H @H % |
---|
2451 | ] |
---|
2452 | #st11 #st12 #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem |
---|
2453 | #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 |
---|
2454 | destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #t1 #t2 #H inversion H in ⊢ ?; |
---|
2455 | [1,2,3,4,5,6,7,8: |
---|
2456 | [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 |
---|
2457 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 |
---|
2458 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 |
---|
2459 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20 |
---|
2460 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 |
---|
2461 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 |
---|
2462 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 |
---|
2463 | | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21 |
---|
2464 | ] |
---|
2465 | destruct #_ #_ #_ #_ #_ #_ #_ whd in ⊢ (% → ?); #EQ destruct(EQ) |
---|
2466 | @⊥ >EQ in x12; * #H @H % |
---|
2467 | ] |
---|
2468 | #st41 #st42 #r_t #mem1 #new_cont #opt_l1 #cd #EQcode41 #EQcont41 #EQ destruct(EQ) |
---|
2469 | #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #st11_noio |
---|
2470 | #st41_noio #_ whd in ⊢ (?(?%) → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta |
---|
2471 | inversion(opt_l) in ⊢(% → ?); normalize nodelta [2: #lbl #_ * ] #EQopt_l destruct(EQopt_l) |
---|
2472 | #_ #Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); * #EQcont11_42 >EQcode11 in ⊢ (% → ?); |
---|
2473 | normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?); |
---|
2474 | #EQ destruct #IH1 #IH2 #st1' #abs_top #abs_tail |
---|
2475 | whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1 |
---|
2476 | #abs_top_cont #abs_tail_cont #EQcheck |
---|
2477 | normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1') |
---|
2478 | [1,2,3,4,5,7: |
---|
2479 | [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2480 | | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2481 | | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2482 | normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta |
---|
2483 | [2: #l1 cases(?==?) normalize nodelta]] |
---|
2484 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2485 | | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ |
---|
2486 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2487 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2488 | [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) |
---|
2489 | [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] |
---|
2490 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2491 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ |
---|
2492 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2493 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2494 | [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] |
---|
2495 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2496 | | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2497 | normalize nodelta |
---|
2498 | [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] |
---|
2499 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2500 | ] |
---|
2501 | ] #f' #act_p' #opt_l' #i' #_ |
---|
2502 | #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ) |
---|
2503 | lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H |
---|
2504 | cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' #EQenv_it' ***** #EQtrans |
---|
2505 | #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep cases daemon (*CSC: was working |
---|
2506 | change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean; |
---|
2507 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind |
---|
2508 | inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta |
---|
2509 | [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] destruct(EQopt_l') |
---|
2510 | inversion(memb ???) normalize nodelta #Hlbl_keep' |
---|
2511 | [ cases(?==?) normalize nodelta ] |
---|
2512 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct |
---|
2513 | cases(IH1 |
---|
2514 | (mk_state ? |
---|
2515 | (f_body … env_it') |
---|
2516 | (〈ret_act (Some ? lbl'),i'〉 :: (cont … st1')) |
---|
2517 | (store ? st12) false) |
---|
2518 | (abs_top''@abs_tail_cont) |
---|
2519 | (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?)))) |
---|
2520 | [2: whd >EQcont12 |
---|
2521 | change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????); |
---|
2522 | >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta |
---|
2523 | whd in match ret_costed_abs; normalize nodelta >Hlbl_keep' normalize nodelta |
---|
2524 | % // % // % // % [/5 by conj/] >EQcode12 <EQtrans |
---|
2525 | @(inverse_call_post_trans … fresh') |
---|
2526 | [2: % |*: [2,3: /2 by / ] |
---|
2527 | cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2 |
---|
2528 | whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append |
---|
2529 | #no_dup lapply(no_duplicates_append_r … no_dup) #H1 |
---|
2530 | lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1 |
---|
2531 | change with ([?]@?) in match (?::?); #H1 |
---|
2532 | lapply(no_duplicates_append_r … H1) >append_nil // |
---|
2533 | ] |
---|
2534 | ] |
---|
2535 | #abs_top''' * #abs_tail''' * #st41' * #t1' **** #Hst41st41' #EQcosts #EQlen #stack_safety1 |
---|
2536 | #pre_t1' |
---|
2537 | whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ] |
---|
2538 | ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?); |
---|
2539 | whd in ⊢ (??%? → ?); inversion(cont … st41') normalize nodelta |
---|
2540 | [ #_ #EQ destruct(EQ) ] * #act_lbl #i'' #cont_st42' #_ #EQcont_st41' |
---|
2541 | change with (check_continuations ?????) in match (foldr2 ???????); |
---|
2542 | inversion(check_continuations ?????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
2543 | ** #H3 #abs_top_cont'' #abs_tail_cont'' #EQ_contst42 >m_return_bind |
---|
2544 | normalize nodelta inversion(call_post_clean ?????) normalize nodelta |
---|
2545 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct ***** ] * #abs_top'''' #i''' |
---|
2546 | #EQ_clean_i'' inversion(act_lbl) normalize nodelta |
---|
2547 | [1,3,4: |
---|
2548 | [ #x1 #x2 #EQ whd in ⊢ (??%% → ?); #EQ1 destruct ***** |
---|
2549 | | * [|#x1] #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); |
---|
2550 | #EQ destruct ****** [2: *] #EQ destruct |
---|
2551 | | #EQ whd in ⊢ (??%% → ?); #EQ1 destruct ***** |
---|
2552 | ] |
---|
2553 | ] |
---|
2554 | cut(act_lbl = ret_act (Some ? lbl') ∧ cont_st42' = cont … st1' ∧ i'' = i') |
---|
2555 | [ cases(stack_safety1 [ ] …) |
---|
2556 | [3: >EQcont41 in ⊢ (??%?); % |4: normalize // |5: % |2:] * [|#x #xs] * |
---|
2557 | whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct > EQcont_st41' in EQ1; |
---|
2558 | #EQ destruct(EQ) /3 by conj/ |
---|
2559 | ] |
---|
2560 | ** #EQ1 #EQ2 #EQ3 destruct #x #EQ destruct whd in match ret_costed_abs; normalize nodelta |
---|
2561 | >Hlbl_keep' normalize nodelta |
---|
2562 | whd in ⊢ (??%% → ?); #EQ destruct ****** #_ #HH3 #EQ destruct(EQ) |
---|
2563 | >EQcode41 in ⊢ (% → ?); inversion(code … st41') |
---|
2564 | [1,3,4,5,6,7: |
---|
2565 | [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2566 | | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2567 | normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta |
---|
2568 | [2: #l1 cases(?==?) normalize nodelta]] |
---|
2569 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2570 | | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_ |
---|
2571 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2572 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2573 | [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????) |
---|
2574 | [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]] |
---|
2575 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2576 | | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_ |
---|
2577 | whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2578 | [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????) |
---|
2579 | [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]] |
---|
2580 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2581 | | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2582 | normalize nodelta |
---|
2583 | [2,4: * #z1 #z2 cases lbl normalize nodelta |
---|
2584 | [2,4: #l1 cases(memb ???) normalize nodelta |
---|
2585 | [1,3: cases(?==?) normalize nodelta ]]] |
---|
2586 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2587 | | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????) |
---|
2588 | normalize nodelta |
---|
2589 | [2,4: * #z1 #z2 cases(?∧?) normalize nodelta] |
---|
2590 | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2591 | ] |
---|
2592 | ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?); |
---|
2593 | #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_st41' #EQinfo_st41' |
---|
2594 | #EQ destruct(EQ) >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?); |
---|
2595 | #EQ destruct(EQ) >EQi' in EQ_clean_i''; #EQ destruct(EQ) |
---|
2596 | cases(IH2 |
---|
2597 | (mk_state ? i' (cont … st1') (store … st42) (io_info … st42)) |
---|
2598 | abs_tail_cont abs_top'''') |
---|
2599 | [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ] |
---|
2600 | #abs_top_1 * #abs_tail_1 * #st5' * #t2' **** #Hst5_st5' #EQcosts' |
---|
2601 | #EQlen' #stack_safety2 #pre_t2' %{abs_top_1} %{abs_tail_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))} |
---|
2602 | [3: @hide_prf @(call … EQcode_st1' … EQenv_it') // |
---|
2603 | |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') // |
---|
2604 | |2,4: skip |
---|
2605 | ] |
---|
2606 | % [ % |
---|
2607 | [ % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 // |
---|
2608 | whd in ⊢ (??%%); @eq_f // ] |
---|
2609 | %{Hst5_st5'} whd in match (map_labels_on_trace ??); |
---|
2610 | change with (map_labels_on_trace ??) in match (foldr ?????); |
---|
2611 | >map_labels_on_trace_append >get_cost_label_append |
---|
2612 | whd in match (get_costlabels_of_trace ??? (t_ind …)); |
---|
2613 | whd in match (get_costlabels_of_trace ??? (t_ind …)); |
---|
2614 | >get_cost_label_append |
---|
2615 | whd in match (get_costlabels_of_trace ??? (t_ind …)); |
---|
2616 | >map_labels_on_trace_append >EQlab_env_it >EQgen_labels |
---|
2617 | whd in match (map_labels_on_trace ? [ ]); |
---|
2618 | whd in match (append ? (nil ?) ?); |
---|
2619 | cut (∀A.∀l: list A. [ ] @ l = l) [//] #nil_append |
---|
2620 | >nil_append >nil_append >nil_append @(permute_ok … EQcosts EQcosts') |
---|
2621 | | #k #i #EQcont_st3 #EQ |
---|
2622 | cases(stack_safety2 … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % // |
---|
2623 | ]] |
---|
2624 | %4 |
---|
2625 | [ normalize >EQcode_st1' normalize nodelta % #EQ destruct |
---|
2626 | | %{f} % // |
---|
2627 | | whd in ⊢ (?%); >EQcode_st1' normalize nodelta @I |
---|
2628 | | @append_premeasurable // %3 // |
---|
2629 | [ whd in match (as_classify ??); >EQcode_st41' normalize nodelta % #EQ destruct |
---|
2630 | | whd %{lbl'} % |
---|
2631 | ] |
---|
2632 | ] |
---|
2633 | *)] |
---|
2634 | qed. |
---|