source: LTS/Language.ma @ 3416

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