source: LTS/Language.ma @ 3579

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