source: LTS/Language.ma @ 3540

Last change on this file since 3540 was 3535, checked in by piccolo, 5 years ago

final statement of cerco with the first pass integrated in place

File size: 135.1 KB
Line 
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
15include "basics/types.ma".
16include "Traces.ma".
17include "basics/lists/list.ma".
18include "../src/utilities/option.ma".
19include "basics/jmeq.ma".
20
21discriminator option.
22
23record 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
33inductive 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
47let rec eq_instructions (p : instr_params) (i : Instructions p)
48 on i : (Instructions p) → bool ≝
49match 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(*
89lemma 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
109record env_params : Type[1] ≝
110{ form_params_type : Type[0]
111}.
112
113record 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
119record 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
125record state_params : Type[1] ≝
126{ i_pars :> instr_params
127; e_pars :> env_params
128; store_type : DeqSet
129}.
130
131record 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
138definition is_io : ∀p.state p → Prop ≝ λp,st.io_info … st = true.
139
140record 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
151let rec lookup (p : env_params) (p' : instr_params) (l : list (env_item p p'))
152 on l : FunctionName → option (env_item p p') ≝
153match 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
160definition is_ret_call_act : ActionLabel → Prop ≝
161λa.match a with [ret_act _ ⇒ True | call_act _ _ ⇒ True | _ ⇒ False ].
162
163inductive 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   
207let rec get_labels_of_code (p : instr_params) (i : Instructions p) on i : list CostLabel ≝
208match 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
230include "basics/lists/listb.ma".
231include "../src/utilities/hide.ma".
232
233let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝
234match l with
235[ nil ⇒ True
236| cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs
237].
238
239lemma no_duplicates_append_r : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) →
240no_duplicates … l2.
241#A #l1 elim l1 // #x #xs normalize #IH #l2 * /2/
242qed.
243
244lemma no_duplicates_append_l : ∀A : DeqSet.∀l1,l2 : list A.no_duplicates … (l1 @ l2) →
245no_duplicates … l1.
246#A #l1 elim l1 // #x #xs normalize #IH #l2 * #H1 #H2 % [2: /2/ ]
247inversion(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)
250qed.
251   
252record Program (p : env_params) (p' : instr_params) : Type[0] ≝
253{ env : list (env_item p p')
254; main : Instructions p'
255}.
256
257
258definition 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
263lemma 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
269whd 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/
272qed.
273
274
275definition 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
281definition 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]
377qed.
378
379let rec eqb_list (D : DeqSet) (l1 : list D) on l1 : list D → bool ≝
380match 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
385definition 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]
395qed.
396
397unification hint  0 ≔ C;
398    X ≟ DeqSet_List C
399(* ---------------------------------------- *) ⊢
400    list C ≡ carr X.
401
402
403unification hint  0 ≔ D,p1,p2;
404    X ≟ DeqSet_List D
405(* ---------------------------------------- *) ⊢
406    eqb_list D p1 p2 ≡ eqb X p1 p2.
407
408definition associative_list : DeqSet → Type[0] → Type[0] ≝
409λA,B.list (A × (list B)).
410
411let 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
419let 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
424let 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
430lemma 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/
436qed.
437
438lemma 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)
444qed.
445
446lemma 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
453qed.
454
455lemma 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 (?==?)
460normalize [* #H cases H //] #H >IH normalize //
461qed.
462
463definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝
464λx.〈a_non_functional_label x,S x〉.
465
466definition fresh_cc_labe : ℕ → CallCostLabel × ℕ ≝
467λx.〈a_call_label x,S x〉.
468
469definition fresh_rc_label : ℕ → ReturnPostCostLabel × ℕ ≝
470λx.〈a_return_cost_label (S x),S x〉.
471
472record 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
480let rec call_post_trans (p : instr_params) (i : Instructions p) (n : ℕ) on i :
481list CostLabel → call_post_info p ≝
482λabs.
483match 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
533let rec call_post_clean (p : instr_params) (i : Instructions p) on i :
534associative_list DEQCostLabel CostLabel → list ReturnPostCostLabel → list CostLabel →
535option ((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
580let 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≝
582match 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
592definition is_silent_cost_act_b : ActionLabel → bool ≝
593λact. match act with
594 [ cost_act x ⇒ match x with [None ⇒ true | _ ⇒ false ] | _ ⇒ false].
595
596definition eq_ActionLabel : ActionLabel → ActionLabel → bool ≝
597λc1,c2.
598match 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
612definition 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
621definition check_continuations : ∀p : instr_params.
622∀l1,l2 : list (ActionLabel × (Instructions p)).
623associative_list DEQCostLabel CostLabel →
624list ReturnPostCostLabel →  option (Prop × (list CostLabel) × (list CostLabel)) ≝
625λp,cont1,cont2,m,keep.
626foldr2 ??? 〈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(* in input :
648     abs_top is the list of labels to be propageted to the deepest level of the call stack
649             equivalently (?) is the list of labels I need to pay now
650
651     abs_tail are the lists of labels to be propagated to the levels "below" the deepest level
652              equivalently (?) is the list of labels I must have already payid in the
653              code already executed; generated by the continuations below me in the stack
654   in output :
655     abs_top is the list of labels to be propageted from the current level of the call stack
656             non empty only in the case of non-call stack frames (whiles, ifs, etc; but in
657             practice it is always nil!)
658     abs_tail are the lists of labels to be propagated from the levels "below" the current level
659             or equivalently (?) the list of labels I must have already paied in the code
660             already executed; generated by this level of the stack
661*)       
662       
663
664definition state_rel : ∀p.
665associative_list DEQCostLabel CostLabel → list ReturnPostCostLabel → list CostLabel →(list CostLabel) →
666relation (state p) ≝ λp,m,keep,abs_top,abs_tail,st1,st2.
667match check_continuations ? (cont ? st1) (cont … st2) m keep with
668[ Some x ⇒ let 〈prf1,abs_top',abs_tail'〉 ≝ x in
669           prf1 ∧ call_post_clean … (code … st2) m keep abs_top' = return 〈abs_top,(code … st1)〉
670           ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 ∧ abs_tail = abs_tail'
671| None ⇒ False
672].
673
674include "Simulation.ma".
675
676let rec len (s : abstract_status) (st1 : s) (st2 : s) (t : raw_trace s st1 st2)
677on t : ℕ ≝
678match t with
679[ t_base s ⇒ O
680| t_ind s1 s2 s3 l prf lt ⇒ S (len … lt)
681].
682(*
683lemma associative_max : ∀n1,n2,n3.max (max n1 n2) n3 = max n1 (max n2 n3).
684#n1 #n2 #n3 normalize @leb_elim normalize
685[ @leb_elim normalize
686  [ #H1 #H2 @leb_elim normalize
687    [ @leb_elim normalize // * #H @⊥ @H assumption 
688    | @leb_elim normalize
689      [ #H3 * #H @⊥ @H @(transitive_le … H1) assumption
690      | * #H @⊥ @H assumption
691      ]
692    ]
693  | #H1 #H2 @leb_elim normalize
694    [ @leb_elim normalize // #_ #H cases H1 #H1 @⊥ @H1 assumption
695    | @leb_elim normalize
696      [ #_ * #H @⊥ @H assumption
697      | * #H @⊥ @H @(transitive_le … H2)
698*)
699let rec compute_max_n (p : instr_params) (i : Instructions p) on i : ℕ ≝
700match i with
701[ EMPTY ⇒ O
702| RETURN x ⇒ O
703| SEQ x lab instr ⇒ let n ≝ compute_max_n … instr in
704                    match lab with
705                    [ None ⇒ n
706                    | Some l ⇒
707                        match l with
708                        [ a_non_functional_label n' ⇒ S (max n n') ]
709                    ]
710| COND x ltrue i1 lfalse i2 i3 ⇒
711  let n1 ≝ compute_max_n … i1 in
712  let n2 ≝ compute_max_n … i2 in
713  let n3 ≝ compute_max_n … i3 in
714  let mx ≝ max (max n1 n2) n3 in
715  match ltrue with
716  [ a_non_functional_label lt ⇒
717    match lfalse with
718    [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ]
719| LOOP x ltrue i1 lfalse i2 ⇒
720   let n1 ≝ compute_max_n … i1 in
721   let n2 ≝ compute_max_n … i2 in
722   let mx ≝ max n1 n2 in
723   match ltrue with
724  [ a_non_functional_label lt ⇒
725    match lfalse with
726    [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ]
727| CALL f act_p r_lb i1 ⇒
728   let n ≝ compute_max_n … i1 in
729   match r_lb with
730   [ None ⇒ n
731   | Some lbl ⇒ match lbl with [a_return_cost_label l ⇒ S(max l n) ]
732   ]
733| IO lin io lout i1 ⇒
734  let n ≝ compute_max_n … i1 in
735  match lin with
736  [a_non_functional_label l1 ⇒
737    match lout with
738    [a_non_functional_label l2 ⇒ S(max (max n l1) l2) ] ]
739].
740
741
742definition same_fresh_map_on : list CostLabel →
743relation (associative_list DEQCostLabel CostLabel) ≝
744λdom,m1,m2.∀x.bool_to_Prop (x ∈ dom) → get_element … m1 x = get_element … m2 x.
745
746definition same_to_keep_on : list CostLabel → relation (list ReturnPostCostLabel) ≝
747λdom,keep1,keep2.∀x. bool_to_Prop (a_return_post x ∈ dom) → (x ∈ keep1) = (x ∈ keep2).
748
749lemma memb_not_append : ∀D : DeqSet.∀l1,l2 : list D.∀x : D.
750x ∈ l1 = false → x ∈ l2 = false → x ∈ (l1 @ l2) = false.
751#D #l1 elim l1
752[ #l2 #x #_ #H @H ]
753#x #xs #IH #l2 #x1 whd in match (memb ???); inversion (x1 == x) normalize nodelta
754[ #_ #EQ destruct] #EQx1 #EQxs #EQl2 whd in match (memb ???); >EQx1
755normalize nodelta @IH //
756qed.
757
758lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A .
759no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False.
760#A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???);
761inversion (x == x1) normalize nodelta
762[ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H %
763| #_ @IH //
764]
765qed.
766
767
768lemma same_to_keep_on_append : ∀dom1,dom2,dom3 : list CostLabel.
769∀l1,l2,l3,l : list ReturnPostCostLabel.
770no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → a_return_post x ∈ dom1) →
771(∀x.x ∈ l3 → a_return_post x ∈ dom3) →
772same_to_keep_on (dom1@dom2@dom3) (l1@l2@l3) l →
773same_to_keep_on dom2 l2 l.
774#dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #sub_set1 #sub_set3 #H2
775#x #Hx inversion (x ∈ l2)
776 [ #EQkeep <H2 [> memb_append_l2 // >memb_append_l1 // ]
777   >memb_append_l2 // >memb_append_l1 // >Hx //
778 | #EQno_keep <H2
779   [2: >memb_append_l2 // >memb_append_l1 // >Hx //
780   | @sym_eq @memb_not_append [2: @memb_not_append //]
781   [ <associative_append in no_dup; #no_dup ]
782   lapply(memb_no_duplicates_append … (a_return_post x) … no_dup) #H
783   inversion(memb ???) // #H1 cases H
784   [1,4: [>memb_append_l2 | >memb_append_l1] // >Hx //
785   | @sub_set3 >H1 //
786   | @sub_set1 >H1 //
787   ]
788   ]
789 ]
790qed.
791
792lemma same_fresh_map_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l.
793no_duplicates … (dom1 @dom2 @ dom3) → (∀x.x ∈ domain_of_associative_list … l1 → x ∈ dom1) →
794(∀x.x ∈ domain_of_associative_list … l3 → x ∈ dom3) →
795same_fresh_map_on … (dom1 @dom2 @dom3) (l1 @l2 @ l3) l →
796same_fresh_map_on … dom2 l2 l.
797#dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #subset1 #subset3 whd in ⊢ (% → ?); #H1
798whd #x #Hx <H1
799[2: >memb_append_l2 // >memb_append_l1 // >Hx //]
800>get_element_append_r [ >get_element_append_l1 // ] % #K
801[ lapply(subset3 … K) | lapply(subset1 … K) ] #ABS
802[ <associative_append in no_dup; #no_dup] @(memb_no_duplicates_append … x … no_dup)
803// [>memb_append_l2 | >memb_append_l1 ] // >Hx //
804qed.
805
806
807lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p.
808∀x,n,l.
809x ∈ lab_to_keep … (call_post_trans … i n l) → a_return_post x ∈ get_labels_of_code …  i.
810#p #i elim i //
811[ #seq #opt_l #instr #IH #x #n #l whd in match (call_post_trans ????);
812  cases opt_l -opt_l normalize nodelta [|#lbl]
813  whd in match (get_labels_of_code ??); #H [2: @orb_Prop_r] /2/
814| #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l
815  whd in match (call_post_trans ????); whd in match (get_labels_of_code ??);
816  #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r
817  [ >memb_append_l1 // @IH1 [3: >H // |*: ]
818  | >memb_append_l2 // cases(memb_append … H) -H #H
819     [>memb_append_l1 // @IH2 [3: >H // |*: ]
820     | >memb_append_l2 // @IH3 [3: >H // |*: ]
821     ]
822  ]
823| #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l
824  whd in match (call_post_trans ????); whd in match (get_labels_of_code ??);
825  #H cases(memb_append … H) -H #H @orb_Prop_r @orb_Prop_r
826  [ >memb_append_l1 | >memb_append_l2 ] // [ @IH1 | @IH2 ] [3,6: >H |*: ] //
827| #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????);
828  whd in match (get_labels_of_code ??); /2/ whd in match (memb ???);
829  inversion(x == lbl) #Hlbl normalize nodelta
830  [*  >(\P Hlbl) @orb_Prop_l @eq_costlabel_elim // * #H @H %
831  | #H @orb_Prop_r @IH //
832  ]
833| #lin #io #lout #i1 #IH #x #n #l whd in match (call_post_trans ????);
834  whd in match (get_labels_of_code ??); #H @orb_Prop_r @orb_Prop_r @IH //
835]
836qed.
837
838lemma domain_of_associative_list_append : ∀A,B.∀l1,l2 : associative_list A B.
839domain_of_associative_list ?? (l1 @ l2) =
840 (domain_of_associative_list ?? l1) @ (domain_of_associative_list ?? l2).
841#A #B #l1 elim l1 // #x #xs #IH #l2 normalize //
842qed.
843
844lemma lab_map_in_domain: ∀p.∀i: Instructions p.
845 ∀x,n,l.
846  x ∈ domain_of_associative_list … (lab_map p (call_post_trans … i n l)) →
847   x ∈ get_labels_of_code … i.
848#p #i elim i //
849[ #seq * [|#lbl] #i1 #IH #x #n #l whd in match(call_post_trans ????);
850  whd in match (get_labels_of_code ??); /2/ whd in match (memb ???);
851  inversion(x==lbl) #Hlbl normalize nodelta [#_ whd in match (memb ???); >Hlbl % ]
852  #H >memb_cons // @IH //
853| #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #x #n #l
854  whd in match (call_post_trans ????); whd in match (memb ???);
855  whd in match (get_labels_of_code ??); inversion(x == ltrue) #Hlbl normalize nodelta
856  [ #_ whd in match (memb ???); >Hlbl % ] whd in match (memb ???);
857  inversion(x == lfalse) #Hlbl1 normalize nodelta
858  [ #_ whd in match (memb ???); >Hlbl normalize nodelta whd in match (memb ???);
859    >Hlbl1 % ] #H >memb_cons // >memb_cons // >domain_of_associative_list_append in H;
860    #H cases(memb_append … H) [ #H1 >memb_append_l1 // @IH1 [3: >H1 // |*:] ]
861    >domain_of_associative_list_append #H1 cases(memb_append … H1)
862    #H2 >memb_append_l2 // [ >memb_append_l1 | >memb_append_l2 ] //
863    [ @IH2 | @IH3] /2 by eq_true_to_b/
864| #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #x #n #l whd in match (call_post_trans ????);
865  whd in match (get_labels_of_code ??); whd in match (memb ???); inversion(x == lfalse)
866  #Hlfalse normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlfalse // ]
867  whd in match (memb ???); inversion(x==ltrue) normalize nodelta #Hltrue
868  [ #_ whd in match (memb ???); >Hltrue %] >domain_of_associative_list_append #H
869  cases(memb_append … H) #H1 >memb_cons // >memb_cons // [ >memb_append_l1 | >memb_append_l2 ]
870  // [ @IH1 | @IH2] /2/
871| #f #act_p * [|#lbl] #i1 #IH #x #n #l whd in match (call_post_trans ????);
872  whd in match (get_labels_of_code ??); /2/ whd in match (memb ???); inversion (x == lbl)
873  #Hlbl normalize nodelta [ #_ whd in match (memb ???); >Hlbl % ] #H >memb_cons // @IH /2/
874| #lin #io #lout #i1 #IH #x #n #l whd in match (memb ???); inversion(x == lout) #Hlout
875  normalize nodelta [ #_ >memb_cons // whd in match (memb ???); >Hlout % ]
876  whd in match (memb ???); inversion(x==lin) #Hlin normalize nodelta
877  [ #_ whd in match (memb ???); >Hlin % ] #H >memb_cons // >memb_cons // @IH /2/
878]
879qed.
880
881lemma eq_a_non_functional_label :
882∀c1,c2.c1 == c2 → a_non_functional_label c1 == a_non_functional_label c2.
883#c1 #c2 #EQ cases(eqb_true DEQNonFunctionalLabel c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ
884#EQ destruct >(\b (refl …)) @I
885qed.
886
887let rec is_fresh_for_return (keep : list CostLabel) (n : ℕ) on keep : Prop ≝
888match keep with
889[ nil ⇒ True
890| cons x xs ⇒ let ih ≝ is_fresh_for_return xs n in
891              match x with
892              [ a_return_post y ⇒ match y with [a_return_cost_label m ⇒ m ≤ n ∧ ih ]
893              | _ ⇒ ih
894              ]
895].
896
897lemma fresh_ok_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.∀l.
898n ≤ fresh … (call_post_trans p i1 n l).
899#p #i1 elim i1 normalize /2 by transitive_le, le_n/
900[ #seq * [|#lbl] #i2 #IH #n #l normalize /2 by /
901| #cond #ltrue #i_true #lfalse #i_false #i2 #IH1 #IH2 #IH3 #n #l
902  @(transitive_le … (IH3 …)) [2: @(transitive_le … (IH2 …)) [2: @(transitive_le … (IH1 …)) ]] //
903| #f #act_p * [|#lbl] normalize #i2 #IH /2 by le_S/
904]
905qed.
906
907lemma fresh_keep_n_ok : ∀n,m,l.
908is_fresh_for_return l n → n ≤ m → is_fresh_for_return l m.
909#n #m #l lapply n -n lapply m -m elim l // *
910[1,2,3: * #x] #xs #IH #n #m
911normalize [2: * #H1] #H2 #H3 [ %] /2 by transitive_le/
912qed.
913
914definition cast_return_to_cost_labels ≝ map … (a_return_post …).
915coercion cast_return_to_cost_labels.
916
917lemma fresh_false : ∀n.∀l: list ReturnPostCostLabel.is_fresh_for_return l n →
918a_return_cost_label (S n) ∈ l = false.
919#n #l lapply n -n elim l // * #x #xs #IH #n whd in ⊢ (% → ??%?); * #H1
920#H2 @eq_return_cost_lab_elim
921[ #EQ destruct @⊥ /2 by absurd/
922| #_ >IH //
923]
924qed.
925
926lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
927let dom ≝ get_labels_of_code … i1 in
928no_duplicates … dom →
929∀m,keep.
930∀info,l.call_post_trans p i1 n l = info →
931same_fresh_map_on dom (lab_map … info) m →
932same_to_keep_on dom (lab_to_keep … info) keep →
933is_fresh_for_return keep n →
934call_post_clean ? (t_code ? info) m keep l
935 = return 〈gen_labels … info,i1〉.
936#p #i1 elim i1
937[ #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?);
938  #EQ destruct(EQ) //
939| #x #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?);
940  #EQ destruct(EQ) //
941| #seq * [|#lbl] #instr #IH #n #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep
942  #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%%); normalize nodelta
943  >IH //
944  [1,4: whd whd in H2; #x #Hx @H2 whd in match (get_labels_of_code ??); //
945  |2,5: whd whd in H1; #x #Hx [ @H1 // ] cases no_dup #H3 #_ <H1
946       [2: whd in match (get_labels_of_code ??); @orb_Prop_r // ]
947       whd in ⊢ (???%); cases(eqb_true … x lbl) inversion(x == lbl) normalize nodelta
948       [2: //] #_ #H4 >H4 in Hx; // #H5 >H5 in H3; * #ABS @⊥ @ABS %
949  |6: cases no_dup //
950  ]
951  normalize nodelta <(H1 lbl)
952  [2: whd in match (get_labels_of_code ??); @orb_Prop_l cases(eqb_true … (a_non_functional_label lbl) lbl)
953      #H3 #H4 >H4 % ]
954  whd in match (get_element ????); >(\b (refl …)) normalize nodelta
955  >(\b (refl …)) %
956| #cond #ltrue #i1 #lfalse #i2 #i3 #IH1 #IH2 #IH3 #n normalize nodelta
957  #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?);
958  #EQ destruct(EQ) #H1 #H2 #H3 whd in ⊢ (??%?); >IH3 //
959  [2: whd  in match (get_labels_of_code ??) in H2;
960      change with ([?;?]@?) in match (?::?) in H2;
961      <associative_append in H2; <associative_append
962      <(append_nil … (?@?)) <associative_append in ⊢ (??%? → ?);
963      <(append_nil … (?@?)) in ⊢ (??%? → ?); >associative_append
964      >associative_append in ⊢ (??%? → ?); #H2
965      @(same_to_keep_on_append … H2) // [ >append_nil
966      whd in ⊢ (??%); whd in no_dup:(??%); >associative_append // ]
967      #x #Hx cases (memb_append … Hx) -Hx #Hx @orb_Prop_r @orb_Prop_r
968      [ >memb_append_l1 | >memb_append_l2 ] //
969      @(lab_to_keep_in_domain … (eq_true_to_b … Hx))
970  |3: -H2 whd in match (get_labels_of_code ??) in H1;
971      change with ([?;?]@?) in match (?::?) in H1;
972      <associative_append in H1; <associative_append     
973      <(append_nil … (?@?)) >associative_append
974      change with ([?;?]@?) in match (?::?::?) in ⊢ (??%? → ?);
975      <associative_append in ⊢ (??%? → ?);
976      <associative_append in ⊢ (??%? → ?);
977      <(append_nil … (?@?)) in ⊢ (??%? → ?);
978      >associative_append in ⊢ (??%? → ?); #H1
979      @(same_fresh_map_on_append … H1) //
980      [ >append_nil >associative_append // ]
981      #x whd in match (memb ???); inversion(x == ltrue)
982      [ #Hltrue normalize nodelta #_ whd in match (memb ???); >Hltrue %
983      | #Hltrue normalize nodelta whd in match (memb ???); inversion(x == lfalse)
984         [ #Hlfalse #_ @orb_Prop_r @orb_Prop_l >Hlfalse %
985         | #Hlfalse normalize nodelta #Hx @orb_Prop_r @orb_Prop_r
986           >domain_of_associative_list_append in Hx; #H
987           cases(memb_append … H) #H2 [ >memb_append_l1 | >memb_append_l2 ]
988           // @(lab_map_in_domain … (eq_true_to_b … H2))
989         ]
990      ]
991  |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |]
992  ]
993  normalize nodelta >IH2
994  [5: %
995  |2: /2 by fresh_keep_n_ok/
996  |3: whd  in match (get_labels_of_code ??) in H2;
997   change with ([?;?]@?) in match (?::?) in H2;
998   <associative_append in H2; #H2
999   @(same_to_keep_on_append … H2) // #x #Hx [ @orb_Prop_r @orb_Prop_r ]
1000   @(lab_to_keep_in_domain … (eq_true_to_b … Hx))
1001  |4: whd  in match (get_labels_of_code ??) in H1;
1002   change with ([?;?]@?) in match (?::?) in H1;
1003   change with ([?;?]@?) in match (?::?::?) in H1 : (??%?);
1004   <associative_append in H1; <associative_append in ⊢ (??%? → ?); #H1
1005   @(same_fresh_map_on_append … H1) // [2: /2 by lab_map_in_domain/ ]
1006   #x >domain_of_associative_list_append #H cases(memb_append … H)
1007   [ whd in ⊢ (??%? → ?%); cases(x == ltrue) // normalize nodelta
1008     whd in ⊢ (??%? → ?%); cases(x == lfalse) // normalize nodelta
1009     normalize #EQ destruct
1010   | #H1 @orb_Prop_r @orb_Prop_r
1011     @(lab_map_in_domain … (eq_true_to_b … H1))
1012   ]
1013  |6: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l
1014  |*:
1015  ]
1016  >m_return_bind >IH1
1017  [5: %
1018  |2: /3 by fresh_keep_n_ok/
1019  |3:  whd  in match (get_labels_of_code ??) in H2;
1020   change with ([?;?]@?) in match (?::?) in H2;
1021   change with ([ ] @ ?) in match (lab_to_keep ??) in H2;
1022   >associative_append in H2 : (??%?); #H2
1023   @(same_to_keep_on_append … H2) //  #x #Hx cases(memb_append … Hx)
1024   -Hx #Hx [ >memb_append_l1 | >memb_append_l2] //
1025   @(lab_to_keep_in_domain … (eq_true_to_b … Hx))
1026  |4:  whd  in match (get_labels_of_code ??) in H1;
1027   change with ([?;?]@?) in match (?::?) in H1;
1028   change with ([?;?]@?) in match (?::?::?) in H1 : (??%?);
1029    @(same_fresh_map_on_append … H1) // #x >domain_of_associative_list_append
1030    #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2 ]
1031    // @(lab_map_in_domain … (eq_true_to_b … Hx))
1032  |6: cases no_dup #_ * #_ @no_duplicates_append_l
1033  |*:
1034  ]
1035  >m_return_bind normalize nodelta whd in H1; <H1
1036  [2: whd in match (get_labels_of_code ??); whd in match (memb ???);
1037      >(\b (refl …)) % ] whd in match (get_element ????); >(\b (refl …))
1038      normalize nodelta >(\b (refl …)) <H1
1039      [2: whd in match (get_labels_of_code ??); >memb_cons //
1040      whd in match (memb ???); >(\b (refl …)) % ]
1041      whd in match (get_element ????); @eq_costlabel_elim normalize nodelta
1042      [ #ABS @⊥ cases no_dup >ABS * #H #_ @H @orb_Prop_l 
1043      >(\b (refl ? (a_non_functional_label ltrue))) % ] #_
1044      whd in match (get_element ????); >(\b (refl …)) normalize nodelta
1045      >(\b (refl …)) %
1046| #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?);
1047  #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on #f_k
1048  whd in ⊢ (??%?); >(IH2 … (refl …))
1049  [ normalize nodelta >(IH1 … (refl …))
1050    [ >m_return_bind <fresh_map [2: @orb_Prop_l >(\b (refl …)) % ]
1051      whd in match (get_element ????);
1052      inversion(a_non_functional_label ltrue == a_non_functional_label lfalse)
1053      #Hltrue normalize nodelta
1054      [ cases no_dup whd in match (memb ???);
1055        cases(eqb_true … (a_non_functional_label ltrue) (a_non_functional_label lfalse))
1056        #H1 #_ lapply(H1 Hltrue) #EQ destruct(EQ) >(\b (refl …)) * #ABS @⊥ @ABS % ]
1057      whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …))
1058      <fresh_map [2: @orb_Prop_r @orb_Prop_l >(\b (refl …)) % ]
1059      whd in match (get_element ????); >(\b (refl …)) normalize nodelta
1060      >(\b (refl …)) %
1061    | /2 by fresh_keep_n_ok/
1062    | change with ([?;?]@?@?) in keep_on : (?%??); change with ((nil ?) @ ? @ ?) in keep_on : (??%?);
1063      @(same_to_keep_on_append … keep_on) // #x /2 by lab_to_keep_in_domain/
1064    | change with ([?;?]@?@?) in fresh_map : (?%%?); @(same_fresh_map_on_append … fresh_map)
1065      /2 by lab_map_in_domain/ #x whd in match (memb ???); inversion(x==lfalse) #Hlfalse
1066      normalize nodelta
1067      [ #_ @orb_Prop_r whd in match (memb ???); >Hlfalse %
1068      | whd in match (memb ???); inversion(x==ltrue) #Hltrue normalize nodelta [2: *] #_
1069        @orb_Prop_l >Hltrue %
1070      ]
1071    | cases no_dup #_ * #_ /2/
1072    ]
1073  | //
1074  | change with ([?;?]@?@?) in keep_on : (?%??); <associative_append in keep_on;
1075    <(append_nil … (?@?)) <(append_nil … (?@?)) in ⊢ (??%? → ?);
1076    >associative_append in ⊢ (?%%? → ?); >associative_append in ⊢ (??%? → ?);
1077    #keep_on @(same_to_keep_on_append … keep_on) //
1078    [ >associative_append >append_nil //
1079    | #x #Hx @orb_Prop_r @orb_Prop_r /2 by lab_to_keep_in_domain/
1080    ]
1081  | change with ([?;?]@?@?) in fresh_map : (?%??); <associative_append in fresh_map;
1082    <(append_nil … (?@?)) change with ([?;?]@?@?) in ⊢ (??%? → ?);
1083    <associative_append in ⊢ (??%? → ?); <(append_nil … (?@?)) in ⊢ (??%? → ?);
1084    >associative_append in ⊢ (?%%? → ?); >associative_append in ⊢ (??%? → ?);
1085    #fresh_map @(same_fresh_map_on_append … fresh_map) //
1086    [ >append_nil //
1087    | #x >domain_of_associative_list_append #Hx cases(memb_append … Hx)
1088      [2: #Hx1 @orb_Prop_r @orb_Prop_r @(lab_map_in_domain … (eq_true_to_b … Hx1)) ]
1089      whd in match (memb ???); inversion(x == lfalse) normalize nodelta #Hlfalse
1090      [ #_ @orb_Prop_r @orb_Prop_l >Hlfalse %
1091      | whd in match (memb ???); inversion (x==ltrue) normalize nodelta #Hltrue
1092        [ #_ @orb_Prop_l >Hltrue %
1093        | whd in match (memb ???); #EQ destruct
1094        ]
1095      ]
1096    ]
1097  | cases no_dup #_ * #_ /2 by no_duplicates_append_r/
1098  ]
1099| #f #act_p * [|#r_lb] #i #IH #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?);
1100  #EQ destruct(EQ) #fresh_map #same_keep #f_k whd in ⊢ (??%?);
1101  >(IH … (refl …))
1102  [1,6: normalize nodelta
1103     [ >fresh_false [2: /2 by fresh_keep_n_ok/] %
1104     | <same_keep
1105       [ whd in match (memb ???); >(\b (refl …)) normalize nodelta
1106         <fresh_map
1107         [ whd in match (get_element ????); >(\b (refl …)) normalize nodelta
1108           >(\b (refl …)) %
1109         | whd in match (memb ???); >(\b (refl …)) %
1110         ]
1111       | whd in match (memb ???); >(\b (refl …)) %
1112       ]
1113    ]
1114  |2,7: //
1115  |3,8: whd in match (get_labels_of_code ??) in same_keep; // #x #Hx <same_keep
1116        [2: >memb_cons // >Hx // ] cases no_dup * #ABS #_ whd in ⊢ (???%);
1117        inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) >Hx //
1118  |4,9: whd in match (get_labels_of_code ??) in fresh_map; // #x #Hx <fresh_map
1119        [2: >memb_cons // >Hx //] cases no_dup * #ABS #_ whd in ⊢ (???%);
1120        inversion(x==?) [2: #_ //] #ABS1 @⊥ @ABS <(\P ABS1) //
1121  |5,10: [ @no_dup | cases no_dup // ]
1122  ]
1123| #lin #io #lout #i #IH #n whd in match (get_labels_of_code ??); #no_dup
1124  #m #keep #info #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #fresh_map #same_keep
1125  #f_k whd in ⊢ (??%?); >(IH … (refl …))
1126  [ normalize nodelta <fresh_map [2: >memb_cons // >memb_hd // ]
1127    whd in match (get_element ????); >(\b (refl …)) normalize nodelta
1128    >(\b (refl …)) <fresh_map [2: >memb_hd //] whd in match (get_element ????);
1129    inversion(lin==lout)
1130    [ #ABS @⊥ cases no_dup * #ABS1 #_ @ABS1 whd in match (memb ???); >(\P ABS)
1131      >(\b (refl …)) //
1132    | #H inversion (a_non_functional_label lin== ? lout)
1133      [ #ABS lapply(\P ABS) #EQ destruct >(\b (refl …)) in H; #EQ destruct
1134      | #_ normalize nodelta whd in match (get_element ????); >(\b (refl …))
1135        normalize nodelta >(\b (refl …)) %
1136      ]
1137    ]
1138  | //
1139  | #x #Hx >same_keep [2: >memb_cons // >memb_cons // >Hx % ] %
1140  | #x #Hx <fresh_map [2: >memb_cons // >memb_cons // >Hx %]
1141    cases no_dup * #ABS1 ** #ABS2 #_ whd in ⊢ (???%); inversion(x == lout)
1142    normalize nodelta
1143    [2: #_ whd in ⊢ (???%); inversion(x==lin) normalize nodelta //
1144        #H @⊥ @ABS1 >memb_cons // <(\P H) >Hx //
1145    | #H @⊥ @ABS2 <(\P H) >Hx //
1146    ]
1147  | cases no_dup #_ * #_ //
1148  ]
1149]
1150qed.
1151
1152definition fresh_for_prog_aux : ∀p,p'.Program p p' → ℕ → ℕ ≝
1153λp,p',prog,n.foldl … (λn,i.max n (compute_max_n … (f_body … i))) n (env … prog).
1154
1155include alias "arithmetics/nat.ma".
1156
1157lemma max_1 : ∀n,m,k.k ≤ m → k ≤ max m n.
1158#m #n #k #H normalize @leb_elim // normalize nodelta #H1
1159/2 by transitive_le/
1160qed.
1161
1162lemma max_2 : ∀n,m,k.k≤ n → k ≤ max m n.
1163#m #n #k #H normalize @leb_elim // #H1 normalize nodelta
1164@(transitive_le … H) @(transitive_le … (not_le_to_lt … H1)) //
1165qed.
1166
1167lemma fresh_aux_ok : ∀p,p'.∀prog : Program p p'.∀n,m.n ≤ m →
1168fresh_for_prog_aux … prog n ≤ fresh_for_prog_aux … prog m.
1169#p #p' * #env #main elim env // #hd #tl #IH #n #m #H whd in ⊢ (?%%);
1170@IH whd in ⊢ (?%?); @leb_elim normalize nodelta
1171[ #H1 @max_2 // | #_ @max_1 // ]
1172qed.
1173
1174definition fresh_for_prog : ∀p,p'.Program p p' → ℕ ≝
1175λp,p',prog.fresh_for_prog_aux … prog
1176(compute_max_n … (main … prog)).
1177
1178definition translate_env ≝
1179λp,p'.λenv : list (env_item p p').λmax_all.(foldr ??
1180           (λi,x.let 〈t_env,n,m,keep〉 ≝ x in
1181           let info ≝ call_post_trans … (f_body … i) n (nil ?) in
1182                   〈(mk_env_item ??
1183                       (mk_signature ??(f_name ?? i) (f_pars … i) (f_ret … i))
1184                       (f_lab … i) (t_code … info)) :: t_env,
1185                     fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 ::
1186                                     ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉)
1187          (〈nil ?,max_all,nil ?,nil ?〉) env).
1188
1189definition trans_prog : ∀p,p'.Program p p' →
1190((Program p p') × (associative_list DEQCostLabel CostLabel)) × ((list ReturnPostCostLabel))≝
1191λp,p',prog.
1192let max_all ≝ fresh_for_prog … prog in
1193let info_main ≝ (call_post_trans … (main … prog) max_all (nil ?)) in
1194let 〈t_env,n,m,keep〉 ≝ translate_env … (env … prog) (fresh … info_main) in
1195〈mk_Program ?? t_env (t_code … info_main),m @ (lab_map … info_main),keep @ (lab_to_keep … info_main)〉.
1196
1197definition map_labels_on_trace :
1198(associative_list DEQCostLabel CostLabel) → list CostLabel → list CostLabel ≝
1199λm,l.foldr … (λlab,t.(get_element … m lab) @ t) (nil ?) l.
1200
1201lemma map_labels_on_trace_append:
1202 ∀m,l1,l2. map_labels_on_trace m (l1@l2) =
1203  map_labels_on_trace m l1 @ map_labels_on_trace m l2.
1204 #m #l1 elim l1 // #hd #tl #IH #l2 >associative_append <IH //
1205qed.
1206
1207include "../src/common/Errors.ma".
1208include "Permutation.ma".
1209
1210(*
1211
1212axiom is_permutation: ∀A.list A → list A → Prop.
1213axiom is_permutation_eq : ∀A.∀l : list A.is_permutation … l l.
1214axiom is_permutation_cons : ∀A.∀l1,l2,x.is_permutation A l1 l2 →
1215                                       is_permutation A (x :: l1) (x :: l2).
1216*)
1217(*
1218inductive is_permutation (A : Type[0]) : list A → list A → Prop ≝
1219| p_empty : is_permutation A (nil ?) (nil ?)
1220| p_append : ∀x,x1,x2,y,y1,y2.
1221               x = y → is_permutation A (x1 @ x2) (y1 @ y2) →
1222                 is_permutation A (x1 @ [x] @ x2) (y1 @ [y] @ y2).
1223
1224lemma is_permutation_eq : ∀A.∀l : list A.is_permutation … l l.
1225#A #l elim l // #x #xs #IH
1226change with ((nil ?) @ (x :: xs)) in ⊢ (??%%);
1227>append_cons >associative_append
1228@(p_append ? x (nil ?) xs x (nil ?) xs (refl …)) @IH
1229qed.
1230
1231lemma is_permutation_append : ∀A.∀l1,l2,l3,l4 : list A.
1232is_permutation A l1 l3 → is_permutation A l2 l4 →
1233is_permutation A (l1 @ l2) (l3 @ l4).
1234#A #l1 inversion (|l1|)  [2: #n lapply l1 elim n
1235[ #l2 #l3 #l4 #H inversion H // #x #x1 #x2 #y #y1 #y2 #EQ #H1 #_
1236 #ABS cases(nil_to_nil … (sym_eq ??? ABS)) -ABS #_ #ABS
1237 cases(nil_to_nil … ABS) #EQ1 destruct(EQ1) ]
1238#x #xs #IH #l2 #l3 #l4 #H inversion H
1239[#EQ lapply(jmeq_to_eq ??? EQ) -EQ #EQ destruct(EQ) ]
1240#y #y1 #y2 #z #z1 #z2 #EQ destruct(EQ) #H1 #_ #EQx_xs #EQ destruct(EQ) #_
1241*)
1242
1243lemma memb_append_l22 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A.
1244¬ (x ∈ l1) → x∈ l1 @ l2 = (x ∈ l2).
1245#A #x #l1 elim l1 normalize // #y #ys #IH #l2 cases(x==y)
1246normalize [*] @IH
1247qed.
1248
1249lemma memb_append_l12 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A.
1250¬ (x ∈ l2) → x∈ l1 @ l2 = (x ∈ l1).
1251#A #x #l1 elim l1
1252[ #l2 #H whd in match (append ???); @not_b_to_eq_false @Prop_notb >H % ]
1253#y #ys #IH #l2 #H1 whd in match (memb ???); >IH //
1254qed.
1255
1256
1257lemma lookup_ok_append : ∀p,p',l,f,env_it.
1258lookup p p' l f = return env_it → ∃l1,l2. l = l1 @ [env_it] @ l2 ∧
1259f_name … env_it = f.
1260#p #p' #l elim l [ #f #env_it normalize #EQ destruct]
1261#x #xs #IH #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim
1262[ #EQ destruct(EQ) normalize nodelta whd in ⊢ (???% → ?); #EQ destruct
1263  %{(nil ?)} %{xs} /2/
1264| #Hno_f normalize nodelta #EQ_env_it cases(IH … EQ_env_it)
1265  #l1 * #l2 * #EQ1 #EQ2 %{(x :: l1)} %{l2} >EQ1 /2/
1266]
1267qed.
1268(*
1269lemma foldr_append :
1270  ∀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.
1271#A #B #l1 elim l1 //
1272#hd #tl #Hind #l2 #f #seed normalize >Hind @refl
1273qed.
1274*)
1275
1276lemma foldr_map_append :
1277  ∀A,B:Type[0]. ∀l1, l2 : list A.
1278   ∀f:A → list B. ∀seed.
1279    foldr ?? (λx,acc. (f x) @ acc) seed (l1 @ l2) =
1280     append ? (foldr ?? (λx,acc. (f x) @ acc) (nil ?) l1)
1281       (foldr  ?? (λx,acc. (f x) @ acc) seed l2).
1282#A #B #l1 elim l1 normalize // /3 by eq_f, trans_eq/
1283qed.
1284
1285lemma cons_append : ∀A.∀x : A.∀l.x::l = ([x]@l).
1286//
1287qed.
1288
1289lemma eq_a_call_label :
1290∀c1,c2.c1 == c2 → a_call c1 == a_call c2.
1291#c1 #c2 #EQ cases(eqb_true ? c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ
1292#EQ destruct >(\b (refl …)) @I
1293qed.
1294
1295
1296lemma no_duplicates_append_commute : ∀ A : DeqSet.∀l1,l2 : list A.
1297no_duplicates … (l1 @ l2) →
1298no_duplicates … (l2 @ l1).
1299#A #l1 elim l1
1300[ #l2 >append_nil //]
1301#x #xs #IH #l2 * #H1 #H2 lapply(IH … H2) lapply H1 -H1 -IH -H2
1302elim l2 -l1
1303[ >append_nil #H1 #H2 % // ]
1304#y #ys #IH * #H1 * #H2 #H3 %
1305[2: @IH
1306   [ % #H4 @H1 cases(memb_append … H4)
1307     [ #H5 >memb_append_l1 //
1308     | #H5 >memb_append_l2 // @orb_Prop_r >H5 //
1309     ]
1310   | //
1311   ]
1312| % #H4 cases(memb_append … H4)
1313  [ #H5 @(absurd ?? H2) >memb_append_l1 //
1314  | whd in match (memb ???); inversion(y==x)
1315    [ #H5 #_ <(\P H5) in H1; #H1 @H1 >memb_append_l2 //
1316    | #_ normalize nodelta #H5 @(absurd ?? H2) >memb_append_l2 //
1317    ]
1318  ]
1319]
1320qed.
1321
1322(* aggiungere fresh_to_keep al lemma seguente??*)
1323
1324let rec subset (A : Type[0]) (l1,l2 : list A) on l1 : Prop ≝
1325match l1 with
1326[ nil ⇒ True
1327| cons x xs ⇒ mem … x l2 ∧ subset … xs l2
1328].
1329
1330interpretation "subset" 'subseteq a b = (subset ? a b).
1331
1332lemma subset_append_l2 : ∀A,l2,l1.subset A l2 (l1 @ l2).
1333#A #l2 elim l2 // normalize #x #xs #IH #l1 % // @mem_append_l2 whd /2/
1334qed.
1335
1336lemma refl_subset : ∀A.reflexive … (subset A).
1337#A #l1 elim l1 // #x #xs #IH normalize % /2/
1338qed.
1339
1340lemma fresh_for_subset : ∀l1,l2,n.l1 ⊆ l2 → is_fresh_for_return … l2 n →
1341is_fresh_for_return … l1 n.
1342#l1 elim l1 // * [1,2,3: * #x] #xs #IH #l2 #n * #H1 #H2 #H3 whd
1343try(@IH) // % [2: @IH //] elim l2 in H1 H3; normalize [*]
1344* [1,2,3: * #y] #ys #IH normalize
1345[2,3: * [2,4: #H3 [2: @IH //] * #H4 #H5 @IH //
1346|*: #EQ destruct * //
1347]]
1348*
1349[1,3: #EQ destruct ] #H3 #H4 @IH //
1350qed.
1351
1352lemma fresh_append : ∀n,l1,l2.is_fresh_for_return l1 n → is_fresh_for_return l2 n →
1353is_fresh_for_return (l1@l2) n.
1354#n #l1 lapply n -n elim l1 // * [1,2,3: * #x] #xs #IH #n #l2 [2: * #H1 ] #H2 #H3
1355[ % // @IH //] @IH //
1356qed.
1357
1358definition labels_of_prog : ∀p,p'.Program p p' → ? ≝
1359λp,p',prog.foldr … (λx,l.l @ (get_labels_of_code … (f_body … x)))
1360 (get_labels_of_code … (main … prog)) (env … prog).
1361
1362lemma cast_return_append : ∀l1,l2.cast_return_to_cost_labels … (l1 @ l2) =
1363(cast_return_to_cost_labels … l1) @ (cast_return_to_cost_labels … l2).
1364#l1 #l2 @(sym_eq … (map_append …)) qed.
1365
1366include alias "arithmetics/nat.ma".
1367
1368
1369lemma is_fresh_code : ∀p.∀i : Instructions p.
1370is_fresh_for_return (get_labels_of_code … i) (compute_max_n … i).
1371#p #main  elim main //
1372[ #seq * [| * #lbl] #i #IH normalize // @(fresh_keep_n_ok … IH)
1373  inversion(leb ? lbl) // @leb_elim #Hlbl #EQ destruct normalize nodelta
1374  /2 by le_S/
1375| #cond * #ltrue #i1 * #lfalse #i2 #i3 #IH1 #IH2 #IH3 whd in ⊢ (?%%);
1376  @fresh_append
1377  [ @(fresh_keep_n_ok … IH1) @le_S @max_1 @max_1 @max_1 @max_1 //
1378  | @fresh_append
1379    [ @(fresh_keep_n_ok … IH2) @le_S @max_1 @max_1 @max_1 @max_2 //
1380    | @(fresh_keep_n_ok … IH3) @le_S @max_1 @max_1 @max_2 //
1381    ]
1382  ]
1383| #cond * #ltrue #i1 * #lfalse #i2 #IH1 #IH2 whd in ⊢ (?%%); @fresh_append
1384  [ @(fresh_keep_n_ok … IH1) @le_S @max_1 @max_1 @max_1 //
1385  | @(fresh_keep_n_ok … IH2) @le_S @max_1 @max_1 @max_2 //
1386  ]
1387| #f #act_p * [| * #lbl] #i #IH whd in ⊢ (?%%); //
1388  change with ([?]@?) in ⊢ (?%?); @fresh_append
1389  [ whd % // @le_S @max_1 //
1390  | @(fresh_keep_n_ok … IH) @le_S @max_2 //
1391  ]
1392| * #lin #io * #lout #i #IH whd in ⊢ (?%%); @(fresh_keep_n_ok … IH)
1393  @le_S @max_1 @max_1 //
1394]
1395qed.
1396
1397lemma is_fresh_fresh_for_prog : ∀p,p'.∀prog : Program p p'.
1398is_fresh_for_return (labels_of_prog … prog) (fresh_for_prog … prog).
1399#p #p' * #env #main whd in match fresh_for_prog; normalize nodelta whd in ⊢ (?%?);
1400elim env // * #sig #cost #i #tail #IH  whd in ⊢ (?%?); @fresh_append
1401[ @(fresh_keep_n_ok … IH) @fresh_aux_ok @max_1 //
1402| @(fresh_keep_n_ok … (is_fresh_code … i)) whd in match fresh_for_prog_aux; normalize nodelta
1403  whd in ⊢ (??%); elim tail [ @max_2 // ] #hd1 #tl1 #IH1 @(transitive_le …  IH1)
1404  whd in ⊢ (??%); change with (fresh_for_prog_aux ?? (mk_Program ?? tl1 main) ?) in ⊢ (?%%);
1405  @fresh_aux_ok @max_1 //
1406]
1407qed.
1408
1409lemma subset_def : ∀A : DeqSet.∀l1,l2 : list A.(∀x.x ∈l1 → x ∈ l2) → l1 ⊆ l2.
1410#A #l1 elim l1 // #x #xs #IH #l2 #H %
1411[ @memb_to_mem >H // >memb_hd //
1412| @IH #y #H1 @H >memb_cons // >H1 //
1413]
1414qed.
1415
1416lemma memb_cast_return : ∀keep,x.x ∈ cast_return_to_cost_labels keep →
1417∃ y.x = a_return_post y ∧ bool_to_Prop (y ∈ keep).
1418#keep elim keep
1419[ #x *] #x #xs #IH #y whd in match cast_return_to_cost_labels;
1420whd in match (map ????); whd in match (memb ???); inversion(y==x)
1421[ #Hx #_ %{x} >(\P Hx) %{(refl …)} >memb_hd //
1422| #Hx normalize nodelta #H cases(IH … H) #z * #H1 #H2 %{z} %{H1} >memb_cons // >H2 //
1423]
1424qed.
1425
1426lemma subset_append : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l2 ⊆ l3 → (l1 @ l2) ⊆ l3.
1427#A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 % /2/
1428qed.
1429
1430lemma subset_def_inv : ∀A.∀l1,l2 : list A. l1 ⊆ l2 → ∀x.mem … x l1 → mem … x l2.
1431#A #l1 elim l1 [ #l2 * #x * ] #x #xs #IH #l2 * #H1 #H2 #y *
1432[ #EQ destruct // | #H3 @IH // ]
1433qed.
1434
1435lemma transitive_subset : ∀A.transitive … (subset A).
1436#A #l1 elim l1 // #x #xs #IH #l2 #l3 * #H1 #H2 #H3 %
1437[ @(subset_def_inv … H3) // | @IH // ]
1438qed.
1439
1440lemma subset_append_h1 : ∀A.∀l1,l2,l3 : list A.l1 ⊆ l3 → l1 ⊆ (l3 @ l2).
1441#A #l1 elim l1 // #x #x2 #IH #l2 #l3 * #H1 #H2 % [ @mem_append_l1 // | @IH // ]
1442qed.
1443
1444lemma subset_append_h2 : ∀A.∀l1,l2,l3 : list A.l2 ⊆ l3 → l2 ⊆ (l1 @ l3).
1445#A #l1 elim l1 // #x #xs #IH #l2 elim l2 // #y #ys #IH #l3 * #H1 #H2 %
1446[ @mem_append_l2 // | @IH // ]
1447qed.
1448
1449lemma lab_to_keep_in_prog : ∀p,p'.∀prog : Program p p'.
1450∀t_prog,m,keep.trans_prog … prog = 〈t_prog,m,keep〉 →
1451(cast_return_to_cost_labels keep) ⊆ (labels_of_prog p p' prog).
1452#p #p' * #env #main #t_prog #m #keep whd in match trans_prog; normalize nodelta
1453@pair_elim * #env1 #fresh * #m1 #keep1 #EQenv1 normalize nodelta #EQ destruct
1454lapply EQenv1 -EQenv1 lapply keep1 -keep1 lapply m1 -m1 lapply fresh -fresh
1455lapply env1 -env1 generalize in match (fresh_for_prog ???); elim env
1456[ #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct whd in match (append ???);
1457  @subset_def #x #H whd in match (labels_of_prog); normalize nodelta
1458  whd in match (foldr ?????); cases(memb_cast_return … H) -H #x1 * #EQ1 #H destruct
1459  @(lab_to_keep_in_domain … H)
1460| #x #xs #IH #n #t_env #n1 #m #keep whd in ⊢ (??%? → ?); @pair_elim
1461  * #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail
1462  change with (translate_env ????) in match (foldr ?????); #EQt_env_tail
1463  normalize nodelta #EQ1 destruct >cast_return_append @subset_append
1464  [ >cast_return_append @subset_append
1465    [ whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????);
1466      @subset_def #y #H cases(memb_cast_return … H) -H #y1 * #EQ destruct #H
1467      >memb_append_l2 // @(lab_to_keep_in_domain … H)
1468    | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????);
1469      change with (labels_of_prog ?? (mk_Program ?? xs ?)) in match (foldr ?????);
1470      @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail))
1471      >cast_return_append @subset_append_h1 //
1472    ]
1473  | whd in match labels_of_prog; normalize nodelta whd in match (foldr ?????);
1474    change with (labels_of_prog ?? (mk_Program ?? xs ?)) in match (foldr ?????);
1475    @subset_append_h1 @(transitive_subset … (IH … EQt_env_tail))
1476     >cast_return_append @subset_append_h2 //
1477  ]
1478]
1479qed.
1480
1481lemma fresh_call_post_trans_ok : ∀p.∀i : Instructions p.∀n,l.
1482n ≤ fresh … (call_post_trans … i n l).
1483#p #i elim i //
1484qed.
1485
1486lemma fresh_translate_env_ok : ∀p,p'.∀env,t_env : list (env_item p p').∀n,n1,m,keep.
1487translate_env … env n = 〈t_env,n1,m,keep〉 → n ≤ n1.
1488#p #p' #env elim env
1489[ #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?); #EQ destruct // ]
1490#x #xs #IH #t_env #n #n1 #m #keep whd in ⊢ (??%? → ?);
1491change with (translate_env ????) in match (foldr ?????); @pair_elim
1492* #t_env_tail #fresh_tail * #t_m_tail #t_keep_tail #EQt_env_tail normalize nodelta
1493#EQ destruct @(transitive_le … (IH … EQt_env_tail)) @fresh_call_post_trans_ok
1494qed.
1495 
1496
1497lemma trans_env_ok : ∀p : state_params.∀ prog.
1498no_duplicates_labels … prog →
1499let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
1500∀f,env_it.lookup p p (env … prog) f = return env_it →
1501let dom ≝ get_labels_of_code … (f_body … env_it) in
1502∃env_it',n.is_fresh_for_return keep n ∧lookup p p (env … t_prog) f = return env_it' ∧
1503let info ≝ call_post_trans … (f_body … env_it) n (nil ?) in
1504t_code … info = f_body … env_it' ∧
1505get_element … m (a_call (f_lab … env_it')) = (a_call (f_lab … env_it')) :: gen_labels … info ∧
1506f_sig … env_it = f_sig … env_it' ∧ f_lab … env_it = f_lab … env_it' ∧
1507same_fresh_map_on dom m (lab_map … info) ∧ same_to_keep_on dom keep (lab_to_keep … info).
1508#p #prog inversion(trans_prog … prog) * #t_prog0 #m0 #keep0 #EQt_prog
1509lapply EQt_prog normalize nodelta
1510generalize in match keep0 in ⊢ (% → ? → ? → ? → ? → ??(λ_.??(λ_.?%?)));
1511#keep1 #EQkeep1 inversion prog in EQt_prog; #env #main #EQprog
1512whd in match trans_prog; normalize nodelta
1513@pair_elim
1514cut(fresh_for_prog ?? prog ≤ fresh_for_prog ?? (mk_Program … env main)) [ >EQprog //]
1515generalize in match (fresh_for_prog ???) in ⊢ (??% → %);
1516lapply t_prog0 lapply m0 lapply keep0
1517elim env in ⊢ (?→ ? → ? → ? → ? → %);
1518[ #keep #m #t_prog #n #_ * #env' #fresh * #x #y #_ #_ #_ #f #env_it normalize in ⊢ (% → ?);  #ABS destruct]
1519* #hd_sig #hd_lab #hd_code #tail #IH #keep #m #t_prog #fresh1 #Hfresh1 * #env' #fresh * #m' #keep'
1520normalize in ⊢ (% → ?); normalize nodelta @pair_elim * #env_tail #fresh_tail
1521* #m_tail #keep_tail change with (translate_env ????) in ⊢ (??%? → ?); #EQtail normalize nodelta #EQ1 destruct(EQ1) #EQ2 destruct(EQ2)
1522whd in ⊢ (% → ?); whd in match (foldr ?????); * #Hhd_lab #H lapply(no_duplicates_append_r … H)
1523change with (no_duplicates_labels p p (mk_Program p p tail main)) in match
1524(no_duplicates_labels p p (mk_Program p p tail main)); #no_dup_tail
1525lapply(no_duplicates_append_l … H) #no_dup_head normalize nodelta
1526#f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim normalize nodelta
1527[ #EQ destruct(EQ) whd in ⊢ (???% → ?); #EQ destruct(EQ)
1528  inversion (call_post_trans … hd_code fresh_tail [])
1529  #gen_labs #t_hd_code #t_fresh #t_lab_map #t_lab_to_keep #EQ_trans_code
1530  %{(mk_env_item … hd_sig hd_lab t_hd_code)} %{fresh_tail} %
1531  [ %
1532    [ @(fresh_keep_n_ok … fresh1)
1533      [ @(fresh_keep_n_ok … Hfresh1)
1534        @(fresh_for_subset … (labels_of_prog … prog))
1535        [ @(lab_to_keep_in_prog … EQkeep1) | @is_fresh_fresh_for_prog ]
1536       | @(transitive_le … (fresh_translate_env_ok … EQtail)) //
1537      ]
1538    | whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta
1539      @eq_f cases hd_sig // ]] >EQ_trans_code % [% [ % [ % [% // whd in ⊢ (??%?); >(\b (refl …)) %] % ] % | whd
1540    #x #Hx whd in ⊢ (??%?); >(? : (x == hd_lab) = false)
1541    [2: inversion(x==hd_lab) // #EQx_hdlab cases Hhd_lab -Hhd_lab #Hhd_lab cases Hhd_lab
1542        >memb_append_l1 // <(\P EQx_hdlab) >Hx // ]
1543    normalize nodelta >get_element_append_l1
1544    [2: % #ABS @(memb_no_duplicates_append … x … H) // elim tail
1545        [ whd in match (foldr ?????); @lab_map_in_domain // ]
1546        #x #xs #IH whd in match (foldr ?????); @orb_Prop_r
1547        >memb_append_l2 // >IH %
1548    ] @get_element_append_l1
1549    % #H1 
1550    (* subproof with no nice statement *)
1551    lapply H1 -H1 lapply H -H lapply Hhd_lab -Hhd_lab lapply EQtail -EQtail
1552    generalize in match fresh1; lapply env_tail -env_tail lapply fresh_tail
1553    -fresh_tail lapply m_tail -m_tail lapply keep_tail -keep_tail elim tail
1554    normalize nodelta
1555    [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?);
1556      #EQ destruct(EQ) whd in match (foldr ?????);
1557      #H1 #H2 * ]
1558    #head #tail #IH #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?);
1559    whd in match (foldr ?????);
1560    @pair_elim * #env_tail_res #fresh_tail_res * #lab_map_res #keep_res #EQres
1561    normalize nodelta #EQ destruct(EQ) whd in match (foldr ?????);
1562    #H1 #H2 whd in match (memb ???); inversion(x == ?)
1563    [ #H3 #_ <(\P H3) in H2; change with ([?]@?) in match (?::?); #H2
1564      lapply(no_duplicates_append_commute … H2) -H2 ** #ABS #_ @ABS
1565      >memb_append_l2 // >Hx %
1566    | #H3 normalize nodelta #H4 @(IH … EQres)
1567      [3: >domain_of_associative_list_append in H4; #H4 cases(memb_append … H4) [2: #EQ >EQ %]
1568          #ABS @⊥ @(memb_no_duplicates_append … x … H2) // @orb_Prop_r >memb_append_l1 //
1569          @(lab_map_in_domain … (eq_true_to_b … ABS))
1570      | % #ABS elim H1 -H1 #H1 @H1 cases(memb_append … ABS)
1571        [ #H5 >memb_append_l1 //
1572        | #H5 >memb_append_l2 // @orb_Prop_r >memb_append_l2 //
1573        ]
1574      | lapply(no_duplicates_append_commute … H2) * #_ >associative_append
1575        #h @no_duplicates_append_commute @(no_duplicates_append_r … h)
1576      ]
1577    ]
1578    ]
1579  | whd #x #Hx >memb_append_l12
1580    [2: @notb_Prop % #ABS @(memb_no_duplicates_append … H … Hx) elim tail
1581        [ whd in match (foldr ?????); @lab_to_keep_in_domain // ]
1582        #x #xs #IH whd in match (foldr ?????); @orb_Prop_r
1583        >memb_append_l2 // >IH %
1584    ]
1585    >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … (a_return_post x) … H)
1586    // @⊥
1587    (* subproof with no nice statement *)
1588    lapply ABS -ABS lapply H -H lapply Hhd_lab -Hhd_lab lapply EQtail -EQtail
1589    generalize in match fresh1; lapply env_tail -env_tail lapply fresh_tail
1590    -fresh_tail lapply m_tail -m_tail lapply keep_tail -keep_tail elim tail
1591    normalize nodelta
1592    [ #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?);
1593      #EQ destruct(EQ) whd in match (foldr ?????);
1594      #H1 #H2 whd in ⊢ (??%? → ?); #EQ destruct ]
1595    #head #tail #IH #keep_tail #m_tail #fresh_tail #env_tail #n whd in ⊢ (??%? → ?);
1596    whd in match (foldr ?????);
1597    @pair_elim * #env_tail_res #fresh_tail_res * #lab_map_res #keep_res #EQres
1598    normalize nodelta #EQ destruct(EQ) whd in match (foldr ?????);
1599    #H1 #H2 #H3 cases(memb_append … H3) -H3
1600    [ #H3 change with ([?]@?) in match (?::?) in H2;
1601      lapply(no_duplicates_append_commute … H2) -H2 * #_ #H4 @(memb_no_duplicates_append … (a_return_post x) … H4)
1602      [ whd in match (append ???); >memb_append_l1 // >(lab_to_keep_in_domain … (eq_true_to_b … H3)) %
1603      | //
1604      ]
1605    | #H3 normalize nodelta @(IH … EQres)
1606      [3: //
1607      |  % #ABS elim H1 -H1 #H1 @H1 cases(memb_append … ABS)
1608        [ #H5 >memb_append_l1 //
1609        | #H5 >memb_append_l2 // @orb_Prop_r >memb_append_l2 //
1610        ]
1611      | lapply(no_duplicates_append_commute … H2) * #_ >associative_append
1612        #h @no_duplicates_append_commute @(no_duplicates_append_r … h)
1613      ]
1614    ]
1615  ]
1616| #Hf #Henv_it cases(IH … no_dup_tail … Henv_it)
1617  [9: >EQtail in ⊢ (??%?); %
1618  |13: %
1619  |6: assumption
1620  |10: %
1621  |*:
1622  ]
1623  #new_env_it * #new_fresh ** #is_fresh_newfresh #EQlook_new_env_it ***** #EQt_code #EQ_get_el
1624  #EQsign_env_it #EQ_f_lab #same_fresh_map #same_to_keep %{new_env_it} %{new_fresh}
1625  %
1626  [ %
1627     [ assumption
1628     | whd in ⊢ (??%?); @eq_function_name_elim [ #ABS >ABS in Hf; * #H @⊥ @H %]
1629        #_ normalize nodelta assumption ]]
1630   % [2: #x #Hx <same_to_keep // >associative_append @memb_append_l22
1631        inversion(memb ???) // #ABS lapply(lab_to_keep_in_domain … (eq_true_to_b … ABS))
1632        #ABS1 @(memb_no_duplicates_append … (a_return_post x) … H) //
1633        cases(lookup_ok_append … Henv_it) #l1 * #l2 * #EQ1 #EQ2 destruct(EQ1 EQ2)
1634        >foldr_map_append >memb_append_l2 // >foldr_map_append >memb_append_l1 //
1635        whd in match (foldr ?????); @orb_Prop_r >memb_append_l1 // >Hx % ]
1636   % [2: #x #Hx <same_fresh_map // >cons_append <associative_append
1637         <associative_append in ⊢ (??(???(??%?)?)?); >associative_append
1638         @(get_element_append_r1)
1639         % >domain_of_associative_list_append #ABS cases(memb_append … ABS)
1640         [ whd in match (memb ???); inversion(x==hd_lab) normalize nodelta
1641           [2: #_ whd in match (memb ???); #EQ destruct ] #EQx_hdlab #_
1642               <(\P EQx_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it)
1643               #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append
1644               * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 //
1645               >memb_append_l1 // whd in ⊢ (??%?); cases(x==?) //
1646               normalize nodelta >memb_append_l1 // >Hx %
1647         | #ABS1 @(memb_no_duplicates_append … x … H)
1648           [ @(lab_map_in_domain … (eq_true_to_b … ABS1))
1649           | cases(lookup_ok_append … Henv_it)
1650             #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append
1651             >memb_append_l2 // >memb_append_l1 //
1652             whd in ⊢ (??%?); cases(x==?) //
1653             normalize nodelta >memb_append_l1 // >Hx %
1654           ]
1655         ]
1656     ] 
1657   % // % // % // <EQ_get_el >cons_append <associative_append  <associative_append in ⊢ (??(???(??%?)?)?);
1658   >associative_append
1659   @get_element_append_r1 % >domain_of_associative_list_append #ABS cases(memb_append … ABS)
1660         [ whd in match (memb ???); inversion(a_call (f_lab … new_env_it)== a_call hd_lab)
1661           #EQ_hdlab normalize nodelta
1662           [2: whd in ⊢ (??%? → ?); #EQ destruct ] 
1663           #_ <(\P EQ_hdlab) in Hhd_lab; cases(lookup_ok_append … Henv_it)
1664           #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append
1665           * #ABS1 @ABS1 >memb_append_l2 // >memb_append_l2 //
1666           >memb_append_l1 // whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) //
1667         | #ABS1 @(memb_no_duplicates_append … (a_call (f_lab … new_env_it)) … H)
1668           [ @(lab_map_in_domain … (eq_true_to_b … ABS1))
1669           | cases(lookup_ok_append … Henv_it)
1670             #tail1 * #tail2 * #EQ1 #EQ2 destruct >foldr_map_append >foldr_map_append
1671             >memb_append_l2 // >memb_append_l1 //
1672             whd in ⊢ (??%?); >EQ_f_lab >(\b (refl …)) //
1673           ]
1674         ]
1675]
1676qed.
1677
1678lemma len_append : ∀S : abstract_status.∀st1,st2,st3 : S.
1679∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3.
1680len … (t1 @ t2) = len … t1 + len …  t2.
1681#S #st1 #st2 #st3 #t1 elim t1 normalize //
1682qed.
1683(*
1684axiom permute_ok : ∀A.∀l1,l2,l3,l4,l5,l6,l7,l8,l9,x,y.
1685  (is_permutation A ((l5 @l1) @l6@l7) ((l4 @[]) @l6@l7)
1686 →is_permutation A ((l6 @l2) @l7) ((l3 @l8) @l9)
1687 →is_permutation A
1688   (y ::((l6 @((x ::l5) @(l1 @l2))) @l7))
1689   (((x ::l4 @y ::l3) @l8) @l9)).
1690*)   
1691lemma append_premeasurable : ∀S : abstract_status.
1692∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2: raw_trace … st2 st3.
1693pre_measurable_trace … t1 → pre_measurable_trace … t2 →
1694pre_measurable_trace … (t1 @ t2).
1695#S #st1 #st2 #st3 #t1 #t2 #Hpre lapply t2 -t2 elim Hpre -Hpre //
1696[ #s1 #s2 #s3 #l #prf #tl #Hclass #Hcost #pre_tl #IH #t2 #pr3_t2
1697  %2 // @IH //
1698| #s1 #s2 #s3 #l #Hclass #prf #tl #ret_l #pre_tl #IH #t2 #pre_t2 %3 // @IH //
1699| #s1 #s2 #s3 #l #prf #tl #Hclass #call #callp #pre_tl #IH #t2 #pre_t2 %4 // @IH //
1700| #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #tl1 #tl2 #prf2 #Hclass1 #Hclass3 #call_l1
1701  #nopost #pre_tl1 #pre_tl2 #succ #unlab #IH1 #IH2 #t2 #pre_t2
1702  normalize >append_associative in ⊢ (????(???????%)); %5 // @IH2 //
1703]
1704qed.
1705   
1706lemma correctness_lemma : ∀p,p',prog.
1707no_duplicates_labels … prog →
1708let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
1709∀s1,s2,s1' : state p.∀abs_top,abs_tail.
1710∀t : raw_trace (operational_semantics … p' prog) s1 s2.
1711pre_measurable_trace … t →
1712state_rel … m keep abs_top abs_tail s1 s1' →
1713∃abs_top'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
1714state_rel  … m keep abs_top' abs_tail s2 s2' ∧
1715is_permutation ? ((abs_top @ (map_labels_on_trace m (get_costlabels_of_trace … t))) @ abs_tail) 
1716                 (((get_costlabels_of_trace … t') @ abs_top' ) @ abs_tail) ∧
1717 len … t = len … t' ∧
1718 (∀k.∀i.option_hd … (cont … s2) = Some ? 〈ret_act (None ?),i〉 →
1719 cont … s1 = k @ cont … s2 →
1720∃k'.cont … s1' = k' @ cont … s2' ∧ |k| = |k'|)
1721∧ pre_measurable_trace … t' ∧
1722(pre_silent_trace … t → pre_silent_trace … t').
1723#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQtrans
1724#s1 #s2 #s1' #abs_top #abs_tail #t #Hpre lapply abs_top -abs_top lapply abs_tail
1725-abs_tail lapply s1' -s1' elim Hpre
1726[ #st #Hst #s1' #abs_tail #abs_top #H %{abs_top} %{s1'} %{(t_base …)}
1727  cut(? : Prop)
1728  [3: #Hpre' %
1729  [ %
1730   [ %
1731    [ % [2: %] %{H} whd in match (get_costlabels_of_trace ????); >append_nil
1732      @is_permutation_eq
1733    | #k #i #_ #EQcont_st %{[ ]} % // @sym_eq @eq_f @append_l1_injective_r //
1734    ]
1735  | @Hpre'
1736  ]
1737 | #_ %1 /2 by head_of_premeasurable_is_not_io/
1738 ]
1739 | skip
1740 ]
1741   %1 whd in H; cases(check_continuations ?????) in H; [*] ** #H1 #abs_top_cont
1742    #abs_tail_cont normalize nodelta **** #_ #rel #_ #H2 #_ normalize
1743    inversion(code ??) normalize nodelta
1744    [|#r_t| #seq #lbl #i #_ | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
1745     | #cond #ltrue #i1 #lfalse #i2 #_ #_ | #f #act_p #rlbl #i #_
1746     | #lin #io #lout #i #_ ]
1747    #EQcode_s1' normalize nodelta [|*: % #EQ destruct] <H2
1748    >EQcode_s1' in rel; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
1749    normalize in Hst; <e1 in Hst; normalize nodelta //
1750| #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12
1751  [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore
1752    #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #EQ4 destruct #tl #class_st11 * #opt_l #EQ destruct(EQ)
1753    #pre_tl #IH #s1' #abs_tail #abs_top whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 in ⊢ (% → ?);
1754    whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????);
1755    inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1'
1756    normalize nodelta change with (check_continuations ?????) in match (foldr2 ???????);
1757    inversion(check_continuations ?????) [ #_ *] ** #H1 #l2 #ll2 #EQHl2
1758    >m_return_bind normalize nodelta inversion (call_post_clean ?????) [ #_ ***** ]
1759    * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta
1760    cases l1' in EQconts1'; (*in Hio11 Hl1 EQcont11 H;*) normalize nodelta
1761    [ #x #y #_ (*#_ #_ #_ #H*) *****
1762    | #x #_ cases (ret_costed_abs ??) normalize nodelta [|#c] ******[|*] #EQ @⊥ >EQ in Hl1;
1763      normalize * /2/ ] *
1764    [ #EQconts1' normalize nodelta ****** #EQ destruct(EQ)
1765      #HH1 #EQ destruct(EQ) >EQcode11 in ⊢ (% → ?); inversion(code … s1')
1766      [
1767      | #x
1768      | #seq #lbl #i #_
1769      | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_
1770      | #cond #ltrue #i1 #lfalse #i2 #_ #_
1771      | #f #act_p #ret_post #i #_
1772      | #l_in #io #l_out #i #_
1773      ]
1774      [|*: #_ whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)]
1775           cases(call_post_clean ?????) normalize nodelta
1776           [1,3,5,7,9: #EQ destruct(EQ)]
1777        [ * #z1 #z2 cases lbl normalize nodelta [|#z3 cases(?==?) normalize nodelta]
1778          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1779        | * #z1 #z2 cases(call_post_clean ?????) [| * #z3 #z4 ] whd in ⊢ (??%% → ?);
1780          [2: cases(call_post_clean ?????) normalize nodelta
1781          [| * #z5 #z6 cases(?∧?) normalize nodelta]] whd in ⊢ (??%% → ?);
1782          #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1783        | * #z1 #z2 cases(call_post_clean ?????)
1784          [| * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta]
1785          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1786        | * #z1 #z2 cases ret_post normalize nodelta
1787          [| #z3 cases(memb ???) normalize nodelta [ cases(?==?) normalize nodelta] ]
1788          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1789        | * #z1 #z2 cases(?∧?) normalize nodelta
1790          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1791        ]
1792      ]
1793      #EQcodes1' whd in ⊢ (??%% → ?); #EQ destruct(EQ) #EQstore11 #EQio11 #EQ destruct(EQ)
1794      cases(IH (mk_state ? new_code' new_cont' (store … s1') false) ll2 abs_top …)
1795      [2: whd whd in match check_continuations; normalize nodelta
1796         change with (check_continuations ?????) in match (foldr2 ???????); >EQHl2
1797         normalize nodelta % // % // % // % // @EQcode_c_st12 ]
1798      #abs_top' * #st3' * #t' *****
1799      #Hst3st3' #EQcosts #EQlen #stack_safety #pre_t' #Hsil
1800      %{abs_top'} %{st3'} %{(t_ind … (cost_act (None ?)) …  t')}
1801      [ @hide_prf whd @(empty ????? 〈(cost_act (None ?)),?〉)
1802        [3: assumption |4: assumption |*:] /3 by nmk/ ]
1803      % [ %
1804      [ % [%   [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'} @EQcosts]
1805      * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
1806      [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
1807      destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
1808      #EQk1 #EQlength %{(〈cost_act (None ?),new_code'〉::k1)}
1809      % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ] ]
1810      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio11
1811      normalize in class_st11; >EQcode11 in class_st11; // ]
1812      #H inversion H in ⊢ ?;
1813      [ #H1 #H2 #H3 #H4 #H5 #H6 destruct ] #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
1814      destruct %2
1815      [ % whd in ⊢ (??%% → ?); >EQcodes1' normalize nodelta <EQio11 inversion(io_info … H8)
1816        normalize nodelta [2: #_ #EQ destruct] #ABS lapply class_st11 whd in match (as_classify ??);
1817        >EQcode11 normalize nodelta >ABS normalize nodelta * /2/
1818      ]
1819      @Hsil //
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) #EQstore1 #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' * #st3' * #t' ***** #Hst3st3' #EQcost #EQlen #stack_safety
1863      #pre_t' #Hsil
1864      %{abs_top'} %{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     cut(? : Prop)
1869     [3: #Hpre' %
1870      [ %
1871      [ % [% [2: whd in ⊢ (??%%); >EQlen % ] %{Hst3st3'}
1872          >(map_labels_on_trace_append … [lbl]) (*CSC: funzionava prima*)
1873          whd in match (map_labels_on_trace ? [lbl]); >append_nil >EQget_el
1874          @is_permutation_cons @EQcost
1875        | * [| #hd #tl] #i #EQcont_st3 >EQcont11 #EQ whd in EQ : (???%);
1876          [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
1877          destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
1878          #EQk1 #EQlength %{(〈cost_act (Some ? lbl),new_code'〉::k1)}
1879          % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
1880        ]]
1881      @Hpre' ]
1882      #h inversion h in ⊢ ?; [ #H21 #H22 #H23 #H24 #H25 #H26 destruct]
1883      #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 destruct
1884      |skip |
1885      %2 // [2: % //] normalize >EQcodes1' normalize nodelta <EQio
1886      normalize in class_st11; >EQcode11 in class_st11; //
1887    ]]
1888  | #seq #i #mem * [|#lbl] #EQcode_st11 #EQeval_seq #EQ destruct(EQ) #EQcont
1889    #EQ destruct(EQ) #EQio11 #EQio12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hst11
1890    #_ #Hpre_t #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?);
1891    inversion(check_continuations ?????) normalize nodelta [1,3: #_ *]
1892    ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta ****
1893    #HH1 [ >EQcode_st11 in ⊢ (% → ?); | >EQcode_st11 in ⊢ (% → ?); ]
1894    inversion(code ??)
1895    [1,2,4,5,6,7,8,9,11,12,13,14:
1896      [1,7: #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1897      |2,8: #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1898      |3,9: #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
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(call_post_clean ?????)
1902                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
1903            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1904      |4,10:  #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
1905            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
1906            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
1907                [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
1908            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1909      |5,11: #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
1910             normalize nodelta
1911             [2,4: * #z1 #z2 cases lbl normalize nodelta
1912               [2,4: #l1 cases(memb ???) normalize nodelta
1913                 [1,3: cases(?==?) normalize nodelta ]]]
1914            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1915      |6,12: #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
1916             normalize nodelta
1917             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
1918             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1919      ]
1920    ]
1921    #seq1 #opt_l #i' #_ #EQcode_s1'
1922    change with (m_bind ?????) in ⊢ (??%? → ?);
1923    inversion(call_post_clean ????) [1,3: #_ whd in ⊢ (??%% → ?); #EQ destruct]
1924    * #gen_labs #i'' #EQclean >m_return_bind inversion(opt_l) normalize nodelta
1925    [2,4: #lab1 ] #EQ destruct(EQ)
1926    [1,2: inversion(?==?) normalize nodelta #EQget_el ]
1927    whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1928    #EQstore #EQinfo #EQ destruct(EQ)
1929    cases(IH … (mk_state ? i' (cont … s1') (store … st12) (io_info … s1')) abs_tail_cont ?)
1930    [3,6: whd
1931       [ <EQcont in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); >EQcheck in ⊢ (match % with [_ ⇒ ? | _⇒ ?]);
1932       | <EQcont in ⊢ (match % with [_ ⇒ ? | _⇒ ?]); >EQcheck in ⊢ (match % with [_ ⇒ ? | _⇒ ?]);
1933       ]
1934       normalize nodelta % // % // % // % // assumption
1935    |2,5:
1936    ]
1937    #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
1938    #pre_t' #Hsil %{abs_top1} %{s2'} %{(t_ind … t')}
1939    [1,4: @hide_prf @(seq_sil … EQcode_s1') //
1940    |2,5:
1941    ]
1942    cut(? : Prop)
1943    [3,6: #Hpre'
1944       %
1945   
1946    [1,3: % [1,3: % [1,3: % [2,4: whd in ⊢ (??%%); @eq_f @EQlen ] %{Hst3_s2'} [2: @EQcosts]
1947        whd in ⊢ (??%%); whd in match (get_costlabels_of_trace ????);
1948        whd in match (map_labels_on_trace ??); >(\P EQget_el) @is_permutation_cons
1949        @EQcosts
1950      |*: #k #i #EQcont_st3 >EQcont #EQ
1951          cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
1952      ]]
1953      @Hpre'
1954      |*: #h inversion h in ⊢ ?;
1955          [1,3: #H41 #H42 #H43 #H44 #H45 #H46 destruct
1956          |*: #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct
1957              %2 [ /2 by head_of_premeasurable_is_not_io/ ] @Hsil //
1958          ]
1959          ] |1,4:]
1960    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
1961  |
1962   #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
1963    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
1964    #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????)
1965    [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1
1966    >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
1967    [1,2,3,5,6,7:
1968     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1969     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1970     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
1971       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
1972       [2: #l1 cases(?==?) normalize nodelta]]
1973       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1974     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
1975       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
1976       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
1977       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
1978       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1979     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
1980             normalize nodelta
1981             [2,4: * #z1 #z2 cases lbl normalize nodelta
1982               [2,4: #l1 cases(memb ???) normalize nodelta
1983                 [1,3: cases(?==?) normalize nodelta ]]]
1984            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1985     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
1986             normalize nodelta
1987             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
1988             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
1989      ]
1990    ]
1991    #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
1992    #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
1993    [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????)
1994    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_ifalse1 #i_false' #EQi_false'
1995    >m_return_bind inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
1996    * #gen_lab_i_true' #i_true' #EQi_true' >m_return_bind inversion(?==?) normalize nodelta
1997    [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) normalize nodelta #EQget_lfalse1
1998    whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQio11
1999    #EQ destruct(EQ)
2000    cases(IH …
2001     (mk_state ? i_true1 (〈cost_act (None ?),i'〉 :: cont … s1') (store … st12) (io_info … st12))
2002     abs_tail_cont gen_lab_i_true')
2003    [2: whd whd in match (check_continuations ?????);
2004        >EQcont_st12 in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); whd in match (foldr2 ???????);
2005        change with (check_continuations ?????) in match (foldr2 ???????);
2006        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
2007        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
2008    ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen
2009      #stack_safety #pre_t' #Hsil %{abs_top1}
2010    %{s2'} %{(t_ind … t')}
2011    [ @hide_prf @(cond_true … EQcode_s1') //
2012    |
2013    ] % [
2014    % [ %
2015    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
2016      whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
2017      >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons
2018      assumption
2019    |  #k #i1 #EQcont_st3 #EQcont_st11
2020       cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …)
2021       [2: >EQcont_st12 >EQcont_st11 % ]
2022       * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
2023       %{tl1} % // whd in EQk1 : (??%%); destruct //
2024    ]]
2025    %2 // [2: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct
2026    ]
2027    #h inversion h in ⊢ ?;
2028    [#H1 #H2 #H3 #H4 #H5 #H6 destruct
2029    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct
2030    ]
2031  | #cond #ltrue #i_true #lfalse #i_false #i #mem #EQcode_st11 #EQcond #EQcont_st12
2032    #EQ1 #EQ2 destruct(EQ1 EQ2) #EQio_st11 #EQio_st12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t
2033    #Hclass #_ #Hpre #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?); inversion(check_continuations ?????)
2034    [ #_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta **** #HH1
2035    >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
2036    [1,2,3,5,6,7:
2037     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2038     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2039     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2040       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
2041       [2: #l1 cases(?==?) normalize nodelta]]
2042       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2043     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
2044       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2045       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2046       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
2047       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2048     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2049             normalize nodelta
2050             [2,4: * #z1 #z2 cases lbl normalize nodelta
2051               [2,4: #l1 cases(memb ???) normalize nodelta
2052                 [1,3: cases(?==?) normalize nodelta ]]]
2053            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2054     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2055             normalize nodelta
2056             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
2057             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2058      ]
2059    ] #cond1 #ltrue1 #i_true1 #lfalse1 #ifalse1 #i' #_ #_ #_
2060    #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
2061    [ #_ #EQ destruct ] * #gen_lab_i' #i'' #EQi'' inversion(call_post_clean ????)
2062    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #gen_lab_ifalse1 #i_false' #EQi_false'
2063    >m_return_bind inversion(call_post_clean ????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
2064    * #gen_lab_i_true' #i_true' #EQi_true' >m_return_bind inversion(?==?) normalize nodelta
2065    [2: #_ #EQ destruct] #EQget_ltrue1 inversion(?==?) normalize nodelta #EQget_lfalse1
2066    whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore11 #EQio11
2067    #EQ destruct(EQ)
2068    cases(IH …
2069     (mk_state ? ifalse1 (〈cost_act (None ?),i'〉 :: cont … s1') (store … st12) (io_info … st12))
2070     abs_tail_cont gen_lab_ifalse1)
2071    [2: whd whd in match (check_continuations ?????);
2072        >EQcont_st12 in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); whd in match (foldr2 ???????);
2073        change with (check_continuations ?????) in match (foldr2 ???????);
2074        >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta
2075        >EQi'' normalize nodelta % // % // % // % [2: assumption ] % // % //
2076    ] #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcost #EQlen #stack_safety
2077    #pre_t' #Hsil
2078    %{abs_top1} %{s2'} %{(t_ind … t')}
2079    [ @hide_prf @(cond_false … EQcode_s1') //
2080    |
2081    ] % [
2082    % [ %
2083    [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
2084      whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
2085      >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%); @is_permutation_cons
2086      assumption
2087    | #k #i1 #EQcont_st3 #EQcont_st11
2088      cases(stack_safety … (〈cost_act (None NonFunctionalLabel),i〉::k) … EQcont_st3 …)
2089      [2: >EQcont_st12 >EQcont_st11 % ]
2090      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
2091      %{tl1} % // whd in EQk1 : (??%%); destruct //
2092    ] ]
2093    %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
2094    #h inversion h in ⊢ ?;
2095    [ #H21 #H22 #H23 #H24 #H25 #H26 destruct
2096    | #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 destruct
2097    ]
2098 | #cond #ltrue #i_true #lfalse #i_false #store #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQ2 destruct
2099   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
2100   whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont
2101   #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
2102   [1,2,3,4,6,7:
2103     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2104     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2105     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2106       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
2107       [2: #l1 cases(?==?) normalize nodelta]]
2108       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2109     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
2110            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2111            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2112                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
2113                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
2114            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2115     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2116             normalize nodelta
2117             [2,4: * #z1 #z2 cases lbl normalize nodelta
2118               [2,4: #l1 cases(memb ???) normalize nodelta
2119                 [1,3: cases(?==?) normalize nodelta ]]]
2120            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2121     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2122             normalize nodelta
2123             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
2124             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2125      ]
2126   ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
2127   #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
2128   [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????)
2129   [ #_ whd in ⊢ (??%% → ?); #EQ destruct ] * #gen_itrue1 #i_true2 #EQi_true2 >m_return_bind
2130   inversion (?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1
2131   inversion(?==?) #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ)
2132   -EQ #EQ destruct(EQ) #EQstore_11 #EQ_info11 #EQ destruct
2133   cases(IH …
2134    (mk_state ? i_true1
2135     (〈cost_act (None ?),LOOP … cond ltrue i_true1 lfalse i_false1〉 ::
2136        cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_itrue1)
2137   [2: whd >EQcont_st12 whd in match (check_continuations ?????);
2138       whd in match (foldr2 ???????);
2139       change with (check_continuations ?????) in match (foldr2 ???????);
2140       >EQcheck normalize nodelta whd in match (call_post_clean ?????);
2141       >EQi_false2 normalize nodelta >EQi_true2 >m_return_bind >EQget_ltrue1
2142       >EQget_lfalse1 normalize nodelta % // % // % // % [2: assumption] % //
2143       % //
2144   ]
2145   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
2146   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
2147   [ @hide_prf @(loop_true … EQcode_s1') // |] % [
2148   % [ %
2149   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
2150     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
2151      >(\P EQget_ltrue1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
2152     @is_permutation_cons assumption
2153   | #k #i1 #EQcont_st3 #EQcont_st11
2154      cases(stack_safety … (〈cost_act (None NonFunctionalLabel), LOOP p cond ltrue (code p st12) lfalse i_false〉::k) … EQcont_st3 …)
2155      [2: >EQcont_st12 >EQcont_st11 % ]
2156      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
2157      %{tl1} % // whd in EQk1 : (??%%); destruct //
2158   ] ]
2159   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
2160   #h inversion h in ⊢ ?;
2161   [ #H41 #H42 #H43 #H44 #H45 #H46 destruct
2162   | #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct
2163   ]
2164 | #cond #ltrue #i_true #lfalse #i_false #mem #EQcode_st11 #EQev_loop #EQcont_st12 #EQ1 #EQstore11 destruct
2165   #EQio_11 #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass11 #_ #Hpre #IH #s1' #abs_top #abs_tail
2166   whd in ⊢ (% → ?); inversion(check_continuations ?????) [ #_ * ] ** #H1 #abs_top_cont #abs_tail_cont
2167   #EQcheck normalize nodelta **** #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
2168   [1,2,3,4,6,7:
2169     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2170     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2171     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2172       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
2173       [2: #l1 cases(?==?) normalize nodelta]]
2174       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2175     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
2176            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2177            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2178                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
2179                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
2180            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2181     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2182             normalize nodelta
2183             [2,4: * #z1 #z2 cases lbl normalize nodelta
2184               [2,4: #l1 cases(memb ???) normalize nodelta
2185                 [1,3: cases(?==?) normalize nodelta ]]]
2186            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2187     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2188             normalize nodelta
2189             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
2190             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2191      ]
2192   ] #cond1 #ltrue1 #i_true1 #lfalse1 #i_false1 #_ #_
2193   #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
2194   [ #_ #EQ destruct] * #gen_ifalse1 #i_false2 #EQi_false2 inversion(call_post_clean ?????)
2195   [ #_ whd in ⊢ (??%% → ?); #EQ destruct ] * #gen_itrue1 #i_true2 #EQi_true2 >m_return_bind
2196   inversion (?==?) normalize nodelta [2: #_ #EQ destruct] #EQget_ltrue1
2197   inversion(?==?) #EQget_lfalse1 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ)
2198   -EQ #EQ destruct(EQ) #EQstore_11 #EQ_info11 #EQ destruct
2199   cases(IH …
2200    (mk_state ? i_false1
2201     (cont … s1') (store … st12) (io_info … st12)) abs_tail_cont gen_ifalse1)
2202   [2: whd >EQcont_st12 whd in match (check_continuations ?????);
2203       whd in match (foldr2 ???????);
2204       change with (check_continuations ?????) in match (foldr2 ???????);
2205       >EQcheck normalize nodelta whd in match (call_post_clean ?????);
2206       >EQi_false2 normalize nodelta >EQi_true2
2207        % // % // % // % [2: %] //
2208   ]
2209   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
2210   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
2211   [ @hide_prf @(loop_false … EQcode_s1') // |] % [
2212   % [ %
2213   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
2214     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
2215     >(\P EQget_lfalse1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
2216     @is_permutation_cons assumption
2217   | #k #i #EQcont_st3 <EQcont_st12 #EQ
2218     cases(stack_safety … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
2219   ]]
2220   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct]
2221   #h inversion h in ⊢ ?;
2222   [ #H61 #H62 #H63 #H64 #H65 #H66 destruct
2223   | #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct
2224   ]
2225 | #lin #io #lout #i #mem #EQcode_st11 #EQev_io #EQcost_st12 #EQcont_st12
2226   #EQ destruct #EQio_12 #EQ1 #EQ2 #EQ3 #EQ4 destruct #t #Hclass_11 #_ #Hpre
2227   #IH #s1' #abs_top #abs_tail whd in ⊢ (% → ?); inversion(check_continuations ?????)
2228   [#_ *] ** #H1 #abs_top_cont #abs_tail_cont #EQcheck normalize nodelta ****
2229   #HH1 >EQcode_st11 in ⊢ (% → ?); inversion(code ??)
2230   [1,2,3,4,5,6:
2231     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2232     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2233     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2234       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
2235       [2: #l1 cases(?==?) normalize nodelta]]
2236       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2237     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
2238            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2239            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2240                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
2241                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
2242            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2243     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
2244       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2245       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2246       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
2247       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2248     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2249             normalize nodelta
2250             [2,4: * #z1 #z2 cases lbl normalize nodelta
2251               [2,4: #l1 cases(memb ???) normalize nodelta
2252                 [1,3: cases(?==?) normalize nodelta ]]]
2253            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2254      ]
2255   ] #lin1 #io1 #lout1 #i1 #_ #EQcode_s1'
2256   whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta
2257   [ #_ #EQ destruct] * #gen_lab #i2 #EQ_i2 inversion(?==?) normalize nodelta
2258   [2: #_ #EQ destruct] #EQget_lout1 inversion(?==?) #EQget_lin1 normalize nodelta
2259   whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2260   #EQstore11 #EQinfo11 #EQ destruct
2261   cases(IH …
2262    (mk_state ? (EMPTY p) (〈cost_act (Some ? lout),i1〉::cont … s1') (store … st12) true)
2263    abs_tail_cont [ ])
2264   [2: whd >EQcont_st12 whd in match (check_continuations ?????);
2265       whd in match (foldr2 ???????);
2266       change with (check_continuations ?????) in match (foldr2 ???????);
2267       >EQcheck normalize nodelta >EQ_i2 normalize nodelta % // % // % // %
2268       [2: >EQcost_st12 % ] % [ % // % //] >(\P EQget_lout1) %
2269   ]
2270   #abs_cont1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
2271   #pre_t' #Hsil %{abs_cont1} %{s2'} %{(t_ind … t')}
2272   [ @hide_prf @(io_in … EQcode_s1') // |] % [
2273   % [ %
2274   [ % [2: whd in ⊢ (??%%); @eq_f //] %{Hst3_s2'}
2275     whd in match (get_costlabels_of_trace ????); whd in match(map_labels_on_trace ??);
2276     >(\P EQget_lin1) whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
2277     @is_permutation_cons assumption
2278   | #k #i1 #EQcont_st3 #EQcont_st11
2279      cases(stack_safety … (〈cost_act (Some ? lout),i〉::k) … EQcont_st3 …)
2280      [2: >EQcont_st12 >EQcont_st11 %]
2281      * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
2282      %{tl1} % // whd in EQk1 : (??%%); destruct //
2283   ]]
2284   %2 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
2285   #h inversion h in ⊢ ?;
2286   [ #H81 #H82 #H83 #H84 #H85 #H86 destruct
2287   | #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct
2288   ]
2289  | #f #act_p #r_lb #cd #mem #env_it #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10
2290    #EQ11 #EQ12 destruct #tl #_ * #x #EQ destruct(EQ)
2291  | #r_t #mem #con #rb #i #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 #EQ7 #EQ8 #EQ9 #EQ10 #EQ11 #EQ12
2292    destruct #t #_ * #nf #EQ destruct
2293  ]
2294| #st1 #st2 #st3 #lab #st1_noio #H inversion H in ⊢ ?;
2295  [1,2,3,4,5,6,7,8:
2296    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
2297    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
2298    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
2299    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
2300    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
2301    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
2302    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
2303    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21
2304    ]
2305    destruct #tl * #y #EQ destruct(EQ) @⊥ >EQ in x12; * #ABS @ABS %
2306  ]
2307  #st11 #st12 #r_t #mem #cont * [|#x] #i #EQcode_st11 #EQcont_st11 #EQ destruct(EQ)
2308  #EQio_11 #EQio_12 #EQev_ret #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct(EQ1 EQ2 EQ3 EQ4 EQ5 EQ6)
2309  #t * #lbl #EQ destruct(EQ) #pre_t #IH #s1' #abs_tail #abs_top whd in ⊢ (% → ?);
2310  inversion(check_continuations …) [#_ *] ** #H1 #abs_top_cont #abs_tail_cont
2311  >EQcont_st11 in ⊢ (% → ?); inversion(cont … s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ)]
2312  * #act_lab #i #cont_s1'' #_ #EQcont_s1' whd in ⊢ (??%% → ?);
2313  change with (check_continuations ?????) in match (foldr2 ???????);
2314  inversion(check_continuations ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
2315  ** #H2 #abs_top_cont' #abs_tail_cont' #EQcheck normalize nodelta
2316  inversion(call_post_clean ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct *****]
2317  * #gen_labs #i' #EQi' inversion act_lab normalize nodelta
2318  [ #f #lab | * [| #lbl1 ]| * [| #nf_l]] #EQ destruct(EQ)
2319  [1,6: whd in ⊢ (??%% → ?); #EQ destruct *****
2320  |4,5: normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** [2: *] #EQ destruct
2321  ]
2322  whd in match ret_costed_abs; normalize nodelta
2323  [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ****** #EQ destruct(EQ) ]
2324  inversion (memb ???) normalize nodelta #Hlbl1 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
2325  ****** [ * ] #EQ destruct(EQ) #HH2 #EQ destruct #EQget_el >EQcode_st11 in ⊢ (% → ?);
2326  inversion(code … s1')
2327  [1,3,4,5,6,7:
2328     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2329     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2330       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
2331       [2: #l1 cases(?==?) normalize nodelta]]
2332       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2333     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
2334            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2335            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2336                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
2337                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
2338            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2339     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
2340       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2341       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2342       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
2343       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2344     | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2345             normalize nodelta
2346             [2,4: * #z1 #z2 cases lbl normalize nodelta
2347               [2,4: #l1 cases(memb ???) normalize nodelta
2348                 [1,3: cases(?==?) normalize nodelta ]]]
2349            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2350     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2351             normalize nodelta
2352             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
2353             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2354      ]
2355  ]
2356   #r_t' #EQcode_s1'
2357  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2358  #EQstore11 #EQio_111 #EQ destruct
2359  cases(IH … (mk_state ? i cont_s1'' (store … st12) (io_info … st12)) abs_tail_cont gen_labs)
2360  [2: whd >EQcheck normalize nodelta % // % // % // % // @EQi' ]
2361  #abs_top1 * #s2' * #t' ***** #Hst3_s2' #EQcosts #EQlen #stack_safety
2362  #pre_t' #Hsil %{abs_top1} %{s2'} %{(t_ind … t')}
2363  [ @hide_prf @(ret_instr … EQcode_s1' … EQcont_s1') //
2364  | ] % [
2365  % [ %
2366  [ % [2: whd in ⊢ (??%%); @eq_f // ] %{Hst3_s2'}
2367    whd in match (get_costlabels_of_trace ????);
2368    whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
2369    whd in match (map_labels_on_trace ??); >EQget_el @is_permutation_cons
2370    assumption
2371  | * [| #hd #tl] #i1 #EQcont_st3 >EQcont_st11 #EQ whd in EQ : (???%);
2372    [ <EQ in EQcont_st3; whd in ⊢ (??%% → ?); #EQ1 destruct ]
2373    destruct cases(stack_safety … EQcont_st3 … e0) #k1 *
2374    #EQk1 #EQlength %{(〈ret_act (Some ? lbl1),i〉::k1)}
2375    % [ >EQk1 % | whd in ⊢ (??%%); @eq_f // ]
2376  ]]
2377  %3 // [2,4: % //] normalize >EQcode_s1' normalize nodelta % #EQ destruct ]
2378  #h inversion h in ⊢ ?;
2379  [ #H101 #H102 #H103 #H104 #H105 #H106 destruct
2380  | #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct
2381  ]
2382| #st1 #st2 #st3 #lab #H inversion H in ⊢ ?; #st11 #st12
2383  [1,2,3,4,5,6,7,9:
2384    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
2385    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
2386    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
2387    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
2388    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
2389    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
2390    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
2391    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20
2392    ]
2393    destruct * #z1 * #z2 #EQ destruct(EQ) whd in ⊢ (?% → ?); >x3 in ⊢ (% → ?); *
2394  | #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
2395    #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
2396    destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #tl #_ #_ whd in ⊢ (?% → ?); >EQcode11 in ⊢ (% → ?);
2397    normalize nodelta cases opt_l in EQcode11 EQcont12; normalize nodelta [ #x #y *]
2398    #lbl #EQcode11 #EQcont12 * #pre_tl #IH #st1' #abs_top #abs_tail
2399    whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1
2400    #abs_top_cont #abs_tail_cont #EQcheck
2401    normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
2402    [1,2,3,4,5,7:
2403     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2404     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2405     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2406       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
2407       [2: #l1 cases(?==?) normalize nodelta]]
2408       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2409     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
2410            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2411            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2412                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
2413                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
2414            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2415     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
2416       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2417       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2418       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
2419       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2420     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2421             normalize nodelta
2422             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
2423             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2424     ]
2425    ] #f' #act_p' #opt_l' #i' #_
2426    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
2427    lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
2428    cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh'
2429    #EQenv_it' ***** #EQtrans
2430    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
2431    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
2432    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
2433    inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta
2434    [2: inversion(memb ???) normalize nodelta #Hlbl_keep
2435        [  inversion (get_element ????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
2436           #lbl'' #l3' #_ #EQget_el whd in match (eqb ???); inversion (eqb ???) normalize nodelta
2437          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true ? lbl'' lbl') #H1 #_
2438          lapply(H1 H) -H -H1 #EQ destruct(EQ) inversion(eqb_list ???) normalize nodelta
2439          [2: #_ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(eqb_true (DeqSet_List ?) l3' abs_top'')
2440          #H1 #_ lapply(H1 H) -H -H1 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
2441          #EQ destruct(EQ)
2442          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 ?))))
2443          [2: whd >EQcont12
2444            change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
2445            >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta >EQopt_l'
2446            whd in match ret_costed_abs; normalize nodelta >Hlbl_keep normalize nodelta
2447            % // % // % // % [/5 by conj/] >EQgen_labels >EQcode12 <EQtrans
2448            @(inverse_call_post_trans … is_fresh_fresh')
2449            [2: % |*: [2,3: /2 by / ]
2450                cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
2451                whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append
2452                #no_dup lapply(no_duplicates_append_r … no_dup) #H1
2453                lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1
2454                change with ([?]@?) in match (?::?); #H1
2455                lapply(no_duplicates_append_r … H1) >append_nil //
2456            ]
2457          ]
2458          #abs_top''' * #st3' * #t' ***** #Hst3st3' #EQcosts #EQlen #stack_safety
2459          #pre_t' #Hsil %{abs_top'''}
2460          %{st3'} %{(t_ind … (call_act f (f_lab … env_it')) …  t')}
2461          [ @hide_prf @call /2 width=10 by jmeq_to_eq/ ] % [
2462          % [ %
2463          [ % [2: whd in ⊢ (??%%); >EQlen %]
2464            %{Hst3st3'} >map_labels_on_trace_append whd in match (get_costlabels_of_trace ????) in ⊢ (???%);
2465            >EQlab_env_it >associative_append whd in match (append ???); >associative_append
2466            >associative_append in ⊢ (???%); >(associative_append … [?]) in ⊢ (???%);
2467            whd in match (map_labels_on_trace ??); >EQgen_labels @is_permutation_cons
2468            >append_nil whd in match (append ???) in ⊢ (???%); //
2469          | #k #i1 #EQcont_st3 #EQcont_st11
2470            cases(stack_safety … (〈ret_act (Some ? lbl),i〉::k) … EQcont_st3 …)
2471            [2: >EQcont12 >EQcont_st11 % ]
2472            * [|#hd1 #tl1] * #EQk1 whd in ⊢ (??%% → ?); #EQlength destruct
2473            %{tl1} % // whd in EQk1 : (??%%); destruct //
2474          ]]
2475          %4 // [2,4: % [2: % // |]] normalize >EQcode_st1' normalize nodelta % #EQ destruct
2476          ]
2477          #h inversion h in ⊢ ?;
2478          [ #H121 #H122 #H123 #H124 #H125 #H126 destruct
2479          | #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 #H139 destruct
2480          ]
2481        | whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2482        ]
2483    | whd in ⊢ (??%% → ?); #EQ destruct(EQ)
2484    ]
2485  ]
2486| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #H inversion H in ⊢ ?;
2487  [1,2,3,4,5,6,7,9:
2488    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
2489    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
2490    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
2491    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
2492    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
2493    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
2494    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
2495    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20
2496    ]
2497    destruct #t1 #t2 #prf #_ #_ * #y1 * #y2 #EQ destruct(EQ) @⊥ >EQ in x12; * #H @H %
2498  ]
2499  #st11 #st12 #f #act_p #opt_l #i #mem #env_it #EQcode11 #EQenv_it #EQmem
2500  #EQ destruct(EQ) #EQcode12 #EQcont12 #EQio11 #EQio12 #EQ1 #EQ2 #EQ3
2501  destruct(EQ1 EQ2 EQ3) #EQ destruct(EQ) #t1 #t2 #H inversion H in ⊢ ?;
2502  [1,2,3,4,5,6,7,8:
2503    [ #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16
2504    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17
2505    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20
2506    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19 #x20   
2507    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
2508    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x17 #x18 #x19
2509    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18
2510    | #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 #x15 #x16 #x18 #x19 #x20 #x21
2511    ]
2512    destruct #_ #_ #_ #_ #_ #_ #_ whd in ⊢ (% → ?); #EQ destruct(EQ)
2513    @⊥ >EQ in x12; * #H @H %
2514  ]
2515   #st41 #st42 #r_t #mem1 #new_cont #opt_l1 #cd #EQcode41 #EQcont41 #EQ destruct(EQ)
2516   #EQio41 #EQio42 #EQmem1 #EQ1 #EQ2 #EQ3 #EQ4 #EQ5 #EQ6 destruct #st11_noio
2517   #st41_noio #_ whd in ⊢ (?(?%) → ?); >EQcode11 in ⊢ (% → ?); normalize nodelta
2518   inversion(opt_l) in ⊢(% → ?); normalize nodelta [2: #lbl #_ * ] #EQopt_l destruct(EQopt_l)
2519   #_ #Hpre_t1 #Hpre_t2 whd in ⊢ (% → ?); * #EQcont11_42 >EQcode11 in ⊢ (% → ?);
2520   normalize nodelta #EQ destruct(EQ) whd in ⊢ (% → ?);
2521   #EQ destruct #IH1 #IH2 #st1' #abs_top #abs_tail
2522    whd in ⊢ (% → ?); inversion(check_continuations ????) [ #_ *] ** #H1
2523    #abs_top_cont #abs_tail_cont #EQcheck
2524    normalize nodelta **** #HH1 >EQcode11 in ⊢ (% → ?); inversion(code … st1')
2525    [1,2,3,4,5,7:
2526     [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2527     | #r_t #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2528     | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2529       normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
2530       [2: #l1 cases(?==?) normalize nodelta]]
2531       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2532     | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
2533            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2534            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2535                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
2536                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
2537            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2538     | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
2539       whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2540       [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2541       [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
2542       whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2543     | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2544             normalize nodelta
2545             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
2546             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2547     ]
2548    ] #f' #act_p' #opt_l' #i' #_
2549    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
2550    lapply(trans_env_ok … no_dup) >EQtrans normalize nodelta #H
2551    cases(H … EQenv_it) -H #env_it' * #fresh' ** #is_fresh_fresh' #EQenv_it' ***** #EQtrans
2552    #EQgen_labels #EQsignature #EQlab_env_it #same_map #same_keep
2553    change with (m_bind ?????) in EQclean : (??%?); inversion(call_post_clean ?????) in EQclean;
2554    [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #abs_top'' #i'' #EQi' >m_return_bind
2555    inversion opt_l' in EQcode_st1'; [| #lbl'] #EQopt_l' #EQcode_st1' normalize nodelta
2556    [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] destruct(EQopt_l')
2557    inversion(memb ???) normalize nodelta #Hlbl_keep'
2558    [ cases(?==?) normalize nodelta ]
2559     whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
2560     cases(IH1
2561            (mk_state ?
2562              (f_body … env_it')
2563              (〈ret_act (Some ? lbl'),i'〉 :: (cont … st1'))
2564              (store ? st12) false)
2565            (abs_top''@abs_tail_cont)
2566            (gen_labels … (call_post_trans … (f_body … env_it) fresh' (nil ?))))
2567     [2: whd >EQcont12
2568         change with (m_bind ??? (check_continuations ?????) ?) in match (check_continuations ?????);
2569          >EQcheck >m_return_bind normalize nodelta >EQi' normalize nodelta
2570          whd in match ret_costed_abs; normalize nodelta >Hlbl_keep' normalize nodelta
2571          % // % // % // % [/5 by conj/] >EQcode12 <EQtrans
2572          @(inverse_call_post_trans … fresh')
2573          [2: % |*: [2,3: /2 by / ]
2574              cases(lookup_ok_append … EQenv_it) #env1 * #env2 * #EQ1 #EQ2
2575              whd in no_dup; destruct >EQ1 in no_dup; >foldr_map_append >foldr_map_append
2576              #no_dup lapply(no_duplicates_append_r … no_dup) #H1
2577              lapply(no_duplicates_append_l … H1) whd in match (foldr ?????); -H1
2578              change with ([?]@?) in match (?::?); #H1
2579              lapply(no_duplicates_append_r … H1) >append_nil //
2580          ]
2581     ]
2582     #abs_top''' * #st41' * #t1' ***** #Hst41st41' #EQcosts #EQlen #stack_safety1
2583     #pre_t1' #Hsil1
2584     whd in Hst41st41'; inversion(check_continuations …) in Hst41st41'; [ #_ * ]
2585     ** #H2 #abs_top_cont' #abs_tail_cont' >EQcont41 in ⊢ (% → ?);
2586     whd in ⊢ (??%? → ?); inversion(cont … st41') normalize nodelta
2587     [ #_ #EQ destruct(EQ) ] * #act_lbl #i'' #cont_st42' #_ #EQcont_st41'
2588     change with (check_continuations ?????) in match (foldr2 ???????);
2589     inversion(check_continuations ?????) [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
2590     ** #H3 #abs_top_cont'' #abs_tail_cont'' #EQ_contst42 >m_return_bind
2591     normalize nodelta inversion(call_post_clean ?????) normalize nodelta
2592     [ #_ whd in ⊢ (??%% → ?); #EQ destruct ***** ] * #abs_top'''' #i'''
2593     #EQ_clean_i'' inversion(act_lbl) normalize nodelta
2594     [1,3,4:
2595       [ #x1 #x2 #EQ whd in ⊢ (??%% → ?); #EQ1 destruct *****
2596       | * [|#x1] #EQ destruct normalize nodelta whd in ⊢ (??%% → ?);
2597         #EQ destruct ****** [2: *] #EQ destruct
2598       ]
2599     ]
2600     cut(act_lbl = ret_act (Some ? lbl') ∧ cont_st42' = cont … st1' ∧ i'' = i')
2601     [ cases(stack_safety1 [ ] …)
2602       [3: >EQcont41 in ⊢ (??%?); % |4: normalize // |5: % |2:] * [|#x #xs] *
2603       whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct > EQcont_st41' in EQ1;
2604       #EQ destruct(EQ) /3 by conj/
2605     ]
2606     ** #EQ1 #EQ2 #EQ3 destruct #x #EQ destruct whd in match ret_costed_abs; normalize nodelta
2607     >Hlbl_keep' normalize nodelta
2608     whd in ⊢ (??%% → ?); #EQ destruct ****** #_ #HH3 #EQ destruct(EQ)
2609     >EQcode41 in ⊢ (% → ?); inversion(code … st41')
2610     [1,3,4,5,6,7:
2611       [ #_ whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2612       | #seq #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2613         normalize nodelta [2: * #z1 #z2 cases lbl normalize nodelta
2614         [2: #l1 cases(?==?) normalize nodelta]]
2615         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2616       | #cond #ltrue #i1 #lfalse #i2 #i3 #_ #_ #_ #_
2617            whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2618            [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2619                [2,4: * #z3 #z4 >m_return_bind cases(call_post_clean ?????)
2620                     [2,4: * #z5 #z6 >m_return_bind cases(?∧?) normalize nodelta ]]]
2621            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2622       | #cond #ltrue #i1 #lfalse #i2 #_ #_ #_
2623         whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2624         [2,4: * #z1 #z2 normalize nodelta cases (call_post_clean ?????)
2625         [2,4: * #z3 #z4 >m_return_bind cases(?∧?) normalize nodelta ]]
2626         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2627       | #f #act_p #lbl #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2628             normalize nodelta
2629             [2,4: * #z1 #z2 cases lbl normalize nodelta
2630               [2,4: #l1 cases(memb ???) normalize nodelta
2631                 [1,3: cases(?==?) normalize nodelta ]]]
2632            whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2633       | #lin #io #lout #i #_ #_ whd in ⊢ (??%% → ?); cases(call_post_clean ?????)
2634             normalize nodelta
2635             [2,4: * #z1 #z2 cases(?∧?) normalize nodelta]
2636             whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ)
2637       ]   
2638     ] #r_t' #EQcode_st41' whd in ⊢ (??%% → ?);
2639     #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct(EQ) #EQstore_st41' #EQinfo_st41'
2640     #EQ1 >EQcont11_42 in EQcheck; >EQ_contst42 in ⊢ (% → ?);
2641     #EQ destruct(EQ) >EQi' in EQ_clean_i''; #EQ destruct(EQ)
2642     cases(IH2
2643             (mk_state ? i' (cont … st1') (store … st42) (io_info … st42))
2644             abs_tail_cont abs_top'''')
2645     [2: whd >EQ_contst42 normalize nodelta % // % // % // % // @EQi' ]
2646     #abs_top_1 * #st5' * #t2' ***** #Hst5_st5' #EQcosts'
2647     #EQlen'  #stack_safety2 #pre_t2' #Hsil2 %{abs_top_1} %{st5'} %{(t_ind … (t1' @ (t_ind … t2')))}
2648     [3: @hide_prf @(call …  EQcode_st1' …  EQenv_it') //
2649     |1: @hide_prf @(ret_instr … EQcode_st41' … EQcont_st41') //
2650     |2,4: skip
2651     ] % [
2652     % [ %
2653     [ % [2: whd in ⊢ (??%%); @eq_f >len_append >len_append @eq_f2 //
2654           whd in ⊢ (??%%); @eq_f // ]
2655       %{Hst5_st5'} whd in match (map_labels_on_trace ??);
2656       change with (map_labels_on_trace ??) in match (foldr ?????);
2657       >map_labels_on_trace_append >get_cost_label_append
2658       whd in match (get_costlabels_of_trace ??? (t_ind …));
2659       whd in match (get_costlabels_of_trace ??? (t_ind …));
2660       >get_cost_label_append
2661       whd in match (get_costlabels_of_trace ??? (t_ind …));
2662       >map_labels_on_trace_append >EQlab_env_it >EQgen_labels
2663       whd in match (map_labels_on_trace ? [ ]);
2664       whd in match (append ? (nil ?) ?);
2665       cut (∀A.∀l: list A. [ ] @ l = l) [//] #nil_append
2666       >nil_append >nil_append >nil_append @(permute_ok … EQcosts EQcosts')
2667     | #k #i #EQcont_st3 #EQ
2668       cases(stack_safety2 … EQcont_st3 … EQ) #k1 * #EQk1 #EQlength %{k1} % //
2669     ]]
2670     %4
2671     [ normalize >EQcode_st1' normalize nodelta % #EQ destruct
2672     | %{f} % //
2673     | whd in ⊢ (?%); >EQcode_st1' normalize nodelta @I
2674     | @append_premeasurable // %3 //
2675       [ whd in match (as_classify ??); >EQcode_st41' normalize nodelta % #EQ destruct
2676       | whd %{lbl'} %
2677       ]
2678     ]
2679  ] #h inversion h in ⊢ ?;
2680  [ #H141 #H142 #H143 #H144 #H145 #H146 destruct
2681  |#H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 destruct
2682  ]
2683
2684qed.
2685
2686
2687lemma silent_in_silent : ∀p,p',prog.
2688no_duplicates_labels … prog →
2689let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
2690∀s1,s2,s1' : state p.∀abs_top,abs_tail.
2691∀t : raw_trace (operational_semantics … p' prog) s1 s2.
2692silent_trace … t →
2693state_rel … m keep abs_top abs_tail s1 s1' →
2694∃abs_top'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'.
2695state_rel  … m keep abs_top' abs_tail s2 s2' ∧
2696silent_trace … t'.
2697#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
2698#s1 #s2 #s1' #abs_top #abs_tail #t *
2699[2: cases t -s1 -s2 [2: #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 cases H87 #H cases(H I)]
2700#st #_ #H %{abs_top} %{s1'} %{(t_base …)} % // %2 % * ]
2701#H #H1 lapply(correctness_lemma p p' prog no_dup) >EQt_prog normalize nodelta #H2
2702cases(H2 … (pre_silent_is_premeasurable … H) … H1)  -H2 #abs_top' * #s2' * #t' ***** #REL'
2703#_ #_ #_ #_ #H2 %{abs_top'} %{s2'} %{t'} %{REL'} % @H2 //
2704qed.
Note: See TracBrowser for help on using the repository browser.