source: LTS/Lang_meas.ma @ 3553

Last change on this file since 3553 was 3551, checked in by piccolo, 5 years ago

closed all daeomns

File size: 48.0 KB
RevLine 
[3535]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
[3549]15include "Lang_corr.ma".
[3535]16
17
18lemma top_move_source_is_empty : ∀p,p',prog.
19let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
20∀l.
21∀s1,s2,s1' : state p.∀abs_top,abs_tail.
22execute_l … p' (env … prog) l s1 s2 →
[3549]23is_costlabelled_act p l →
24(is_call_act p l → is_call_post_label p (operational_semantics p p' prog) … s1) →
[3535]25state_rel … m keep abs_top abs_tail s1 s1' → abs_top = nil ? ∧
[3549]26(is_call_act p l → is_call_post_label p (operational_semantics p p' t_prog) … s1').
[3535]27#p #p' #prog @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
28#l #s1 #s2 #s1' #abs_top #abs_tail #H elim H -s1 -s2 -l
29[ #s1 #s2 * #lab #code_cont #stack #EQcode #EQcont #EQ1 #EQ2 destruct #EQstore
30  #Hio1 #Hio2 #no_ret_lab #cost_lab whd in match state_rel; normalize nodelta
31  inversion(check_continuations ?????) [ #_ #_ *] ** #Hcont #a_top #a_tail #EQcheck #_
32  normalize nodelta **** #HHcont #EQcall_post #EQstore #EQio #EQ destruct
33  >EQcont in EQcheck; whd in ⊢ (??%? → ?); inversion(cont … s1') normalize nodelta
34  [ #_ #EQ destruct] * #lab' #code_cont' #stack' #_ #EQcont'
[3549]35    change with (check_continuations ??????) in match (foldr2 ???????);
[3535]36    inversion(check_continuations ?????) [ #_ normalize #EQ destruct]
37    ** #H2 #a_top1 #a_tail1 #EQcheck >m_return_bind normalize nodelta
38    inversion(call_post_clean ?????) normalize nodelta [ #_ whd in ⊢ (??%% → ?); #EQ destruct cases HHcont]
39    * #labels #code_cleaned #EQclean normalize nodelta
40    >EQcode in EQcall_post; inversion(code ? s1')
[3540]41        [2,3,4,5,6,7:
42          [ #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
43            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
44          #_ whd in ⊢ (??%% → ?);
45          [ | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
46          | cases(call_post_clean ?????); normalize nodelta
47            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
48               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
49                 [| #z cases(?∧?) normalize nodelta
50                 ]
51               ]
52            ]
53          | cases(call_post_clean ?????) normalize nodelta
54            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
55               [| #y cases(?∧?) normalize nodelta
56               ]
57            ]
58          | cases(call_post_clean ?????) normalize nodelta
59             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
60                [ cases (?==?) normalize nodelta ]
61             ]]
62          | cases(call_post_clean ?????) normalize nodelta
63             [| #x cases(? ∧ ?) normalize nodelta ]
64          ]
65          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
[3535]66        | #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct cases lab' normalize nodelta
67          [ #f #c whd in ⊢ (??%% → ?); #EQ destruct %{(refl …)} cases HHcont
68          | * normalize nodelta [| #Lab cases(ret_costed_abs ??) normalize nodelta [| #xxx]] whd in ⊢ (??%% → ?);
69            #EQ destruct %{(refl …)} cases HHcont * [3: *] #EQ destruct #_ #_ [ #_] * #f * #c #EQ destruct
70          | * [|#LAB] normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % // cases HHcont * #EQ destruct
71            try cases cost_lab #_ #_ cases EQ -EQ #EQ destruct #_ * #f * #c #EQ destruct
72          ]
73        ]
74| #s1 #s2 #i #instr #st * [|#lbl] #EQcode_s1 #EQst #EQ destruct #EQcont #EQ destruct #Hios1 #Hios2 *
75  whd in match state_rel; normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
76  #H1 #a_top #a_tail normalize nodelta #_ **** #HH1 >EQcode_s1 inversion(code ? s1')
[3540]77  [1,2,4,5,6,7:
78    [ | #ret | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
79            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
80          #_ whd in ⊢ (??%% → ?);
81          [ |
82          | cases(call_post_clean ?????); normalize nodelta
83            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
84               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
85                 [| #z cases(?∧?) normalize nodelta
86                 ]
87               ]
88            ]
89          | cases(call_post_clean ?????) normalize nodelta
90            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
91               [| #y cases(?∧?) normalize nodelta
92               ]
93            ]
94          | cases(call_post_clean ?????) normalize nodelta
95             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
96                [ cases (?==?) normalize nodelta ]
97             ]]
98          | cases(call_post_clean ?????) normalize nodelta
99             [| #x cases(? ∧ ?) normalize nodelta ]
100          ]
101          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
[3535]102  | #i' * [|#lb] #instr' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
103    [1,3: #EQ destruct] #x whd in ⊢ (??%% → ?); [ #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
104    cases(get_element ???) normalize nodelta [#EQ destruct] #LAB #ll normalize nodelta cases(?==?) normalize nodelta
105    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #_ % // * #f * #c #EQ4 destruct
106 ]
[3540]107| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #instrs #new_m #EQcode_s1 #EQeval #EQcont_s2 #EQ destruct #EQ destruct
108  #Hio1 #Hio2 #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta
109  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
110  [1,2,3,5,6,7:
111    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_
112       | #lin #io #lout #instr #_ ]
113          #_ whd in ⊢ (??%% → ?);
114          [ |
115          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
116          | cases(call_post_clean ?????) normalize nodelta
117            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
118               [| #y cases(?∧?) normalize nodelta
119               ]
120            ]
121          | cases(call_post_clean ?????) normalize nodelta
122             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
123                [ cases (?==?) normalize nodelta ]
124             ]]
125          | cases(call_post_clean ?????) normalize nodelta
126             [| #x cases(? ∧ ?) normalize nodelta ]
127          ]
128          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
129  ]
[3542]130  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs'  #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
131  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
132  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
133  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
134  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
135  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #EQ destruct % // * #f * #c #EQ destruct
[3549]136| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #instrs #new_m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct
137  #Hio1 #Hio2 * #_ whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta
138  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1  inversion(code ? s1')
139  [1,2,3,5,6,7:
140    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_
141       | #lin #io #lout #instr #_ ]
142          #_ whd in ⊢ (??%% → ?);
143          [ |
144          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
145          | cases(call_post_clean ?????) normalize nodelta
146            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
147               [| #y cases(?∧?) normalize nodelta
148               ]
149            ]
150          | cases(call_post_clean ?????) normalize nodelta
151             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
152                [ cases (?==?) normalize nodelta ]
153             ]]
154          | cases(call_post_clean ?????) normalize nodelta
155             [| #x cases(? ∧ ?) normalize nodelta ]
156          ]
157          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
158  ]
159  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
160  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
161  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
162  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
163  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
164  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #EQ destruct % // * #f * #c #EQ destruct
[3550]165| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
166  #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
167  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
168  [1,2,3,4,6,7:
169    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_
170       | #lin #io #lout #instr #_ ]
171          #_ whd in ⊢ (??%% → ?);
172          [ |
173          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
174          | cases(call_post_clean ?????); normalize nodelta
175            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
176               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
177                 [| #z cases(?∧?) normalize nodelta
178                 ]
179               ]
180            ]
181          | cases(call_post_clean ?????) normalize nodelta
182             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
183                [ cases (?==?) normalize nodelta ]
184             ]]
185          | cases(call_post_clean ?????) normalize nodelta
186             [| #x cases(? ∧ ?) normalize nodelta ]
187          ]
188          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
189   ]
190   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
191   cases(call_post_clean …) normalize nodelta [ #EQ destruct] * #a_top1 #i_false''
192   cases(call_post_clean …) [ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true'' >m_return_bind
193   cases(?∧?) normalize nodelta whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
194   #_ #_ #EQ destruct % // * #f * #lab #EQ destruct
195| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
196  #_ #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
197  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
198  [1,2,3,4,6,7:
199    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_
200       | #lin #io #lout #instr #_ ]
201          #_ whd in ⊢ (??%% → ?);
202          [ |
203          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
204          | cases(call_post_clean ?????); normalize nodelta
205            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
206               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
207                 [| #z cases(?∧?) normalize nodelta
208                 ]
209               ]
210            ]
211          | cases(call_post_clean ?????) normalize nodelta
212             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
213                [ cases (?==?) normalize nodelta ]
214             ]]
215          | cases(call_post_clean ?????) normalize nodelta
216             [| #x cases(? ∧ ?) normalize nodelta ]
217          ]
218          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
219   ]
220   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
221   cases(call_post_clean …) normalize nodelta [ #EQ destruct] * #a_top1 #i_false''
222   cases(call_post_clean …) [ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true'' >m_return_bind
223   cases(?∧?) normalize nodelta whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
224   #_ #_ #EQ destruct % // * #f * #lab #EQ destruct
[3535]225| #s1 #s2 #lin #io #lout #instr #men #EQcode  #EQeval #EQcodes2 #EQcont_s2 #EQ destruct #Hio * whd in match state_rel;
226  normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
227  #H1 #a_top #a_tail normalize nodelta #_ **** #HH1 >EQcode inversion(code ? s1')
[3550]228  [1,2,3,4,5,6:
229    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
230        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ ]
231          #_ whd in ⊢ (??%% → ?);
232          [ |
233          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
234          | cases(call_post_clean ?????); normalize nodelta
235            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
236               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
237                 [| #z cases(?∧?) normalize nodelta
238                 ]
239               ]
240            ]
241          | cases(call_post_clean ?????) normalize nodelta
242            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
243               [| #y cases(?∧?) normalize nodelta
244               ]
245            ]
246          | cases(call_post_clean ?????) normalize nodelta
247             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
248                [ cases (?==?) normalize nodelta ]
249             ]]
250          ]
251          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
[3535]252  | #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
253    [ #EQ destruct] #x
254    cases(get_element ???) normalize nodelta [#EQ destruct] #LAB #ll normalize nodelta cases(?∧?) normalize nodelta
255    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #_ % // * #f * #c #EQ destruct
256 ]
257| #s1 #s2 #f #act_p #lbl #instr #men #env_it #EQcode #EQenv_it  #EQeval #EQ destruct #EQcodes2 #EQ destruct #_ #_ *
258  whd in match state_rel; normalize nodelta cases(check_continuations ?????) normalize nodelta [ #_ *] **
259  #H1 #a_top #a_tail normalize nodelta #Hcall **** #HH1 >EQcode inversion(code ? s1')
[3550]260  [1,2,3,4,5,7:
261    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
262        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #lin #io #lout #instr #_  ]
263          #_ whd in ⊢ (??%% → ?);
264          [ |
265          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
266          | cases(call_post_clean ?????); normalize nodelta
267            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
268               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
269                 [| #z cases(?∧?) normalize nodelta
270                 ]
271               ]
272            ]
273          | cases(call_post_clean ?????) normalize nodelta
274            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
275               [| #y cases(?∧?) normalize nodelta
276               ]
277            ]
278         | cases(call_post_clean ?????) normalize nodelta
279             [| #x cases(? ∧ ?) normalize nodelta ]
280         ]
281         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
[3535]282  |*: #f' #act_p' #lbl' #instr' #_ #EQcode_s1' whd in ⊢ (??%% → ?); cases(call_post_clean ?????) normalize nodelta
283    [ #EQ destruct] #x cases lbl' in EQcode_s1'; normalize nodelta [ #_ #EQ destruct] #lbl'' #EQcode_s1'
284    inversion(?∈?) normalize nodelta
285    [#_ cases(get_element ???) normalize nodelta [#EQ destruct] #LAB #ll normalize nodelta
286      cases(?==?) normalize nodelta
287    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct #_#_ #EQ1 destruct % //
[3549]288    #_ whd in match (is_call_post_label ???); >EQcode_s1' %
[3535]289    ]
290    #ABS whd in ⊢ (??%% → ?);  #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct lapply(Hcall ?) [ %{f} %{(f_lab … env_it)} %]
[3549]291    whd in ⊢ (% → ?); whd in match (is_call_post_label ???); normalize nodelta >EQcode *
[3535]292 ]
293| #s1 #s2 #r_t #mem #stack * [|#lbl] #i #EQcode #EQcont #EQ destruct #_ #_ #EQeval #EQ1 #EQ2 destruct * #_
294  whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta [ #_ *]
295  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode inversion(code … s1')
[3550]296  [1,3,4,5,6,7:
297       [ | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
298        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_  ]
299          #_ whd in ⊢ (??%% → ?);
300          [
301          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
302          | cases(call_post_clean ?????); normalize nodelta
303            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
304               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
305                 [| #z cases(?∧?) normalize nodelta
306                 ]
307               ]
308            ]
309          | cases(call_post_clean ?????) normalize nodelta
310            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
311               [| #y cases(?∧?) normalize nodelta
312               ]
313            ]
314         | cases(call_post_clean ?????) normalize nodelta
315             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
316                [ cases (?==?) normalize nodelta ]
317             ]]
318         | cases(call_post_clean ?????) normalize nodelta
319             [| #x cases(? ∧ ?) normalize nodelta ]
320         ]
321         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
[3535]322  | #r_t' #EQcode_s1' whd in ⊢ (??%% → ?); #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct
323    >EQcont in EQcheck; inversion (cont ? s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
324    * #LAB #instrs #stack' #_ #EQcont_s1' whd in match check_continuations; normalize nodelta
[3549]325    whd in match (foldr2 ???????); change with (check_continuations ??????) in match (foldr2 ???????);
[3535]326    cases(check_continuations ?????) normalize nodelta [#EQ destruct] ** #H2 #a_top1 #a_tail1
327    normalize nodelta   whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta [ #EQ destruct cases HH1]
328    * #ret_top #cleaned cases LAB in EQcont_s1';
329    [ #f #c #_ normalize nodelta #EQ destruct cases HH1
330    | *
331      [ #EQcont_s1' normalize nodelta #EQ destruct cases HH1 * #EQ destruct
332      | #lbl1 #EQcont_s1' whd in match ret_costed_abs; normalize nodelta inversion(? ∈ ?) normalize nodelta
333        [ #EQkeep #EQ destruct cases HH1 ** #EQ destruct #HH2 #EQ destruct #_ #_ #_ #_ % // * #f * #c #EQ destruct
334        | #EQkeep #EQ destruct #_ #_ #_ % // * #f * #c #EQ destruct
335        ]
336      ]
337    | * [|#lbl] #EQcont_s1' normalize nodelta  #EQ destruct cases HH1 *  #EQ destruct cases EQ -EQ #EQ destruct
338    ]
339  ]
340]
341qed.
342
343lemma bool_true : ∀b : bool.b=true → b. * // #EQ destruct qed.
[3550]344
[3535]345lemma labelled_action_is_correct :
346∀p,p',prog.
347no_duplicates_labels … prog →
348let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
349∀s1,s2,s1' : state p.∀abs_top,abs_tail.
[3549]350∀l.is_costlabelled_act p l →
[3535]351∀prf :execute_l p p' (env … prog) l s1 s2.
352state_rel … m keep abs_top abs_tail s1 s1' →
[3551]353(is_call_act … l → bool_to_Prop (is_call_post_label … (operational_semantics … p' prog) … s1)) →
[3535]354∃abs_top'.∃s2'.
355execute_l p p' (env … t_prog) l s1' s2' ∧
356state_rel  … m keep abs_top' abs_tail s2 s2' ∧
[3549]357map_labels_on_trace … m … (actionlabel_to_costlabel p l) =
358actionlabel_to_costlabel p l @ abs_top'.
[3535]359#p #p' #prog  #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
360#s1 #s2 #s1' #abs_top #abs_tail #l #Hl #H lapply Hl -Hl elim H -s1 -s2 -l
361[ #s1 #s2 * #lbl #i #stack #EQcode_s1 #EQcont_s1 #EQ destruct #EQ destruct #EQstore #Hio1 #Hio2
362  #Hlbl #cost_lbl whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????)
363  normalize nodelta [ #_ *] ** #H1 #a_top #a_tail >EQcont_s1 inversion(cont … s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
[3549]364  * #lbl' #i' #stack' #_ #EQcont_s1' whd in ⊢ (??%% → ?); change with (check_continuations ??????) in match (foldr2 ???????);
[3535]365  inversion(check_continuations ?????) normalize nodelta [ #_ #EQ destruct] ** #H2 #a_top1 #a_tail1 #EQcheck
366  normalize nodelta inversion(call_post_clean ?????) normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct ***** ]
367  * #gen_labels #cleaned_i' #EQclean cases lbl' in EQcont_s1'; -lbl' normalize nodelta
368  [ #f #c #_ whd in ⊢ (??%% → ?); #EQ destruct *****
369  | * [|#lbl'] normalize nodelta #_ whd in ⊢ (??%% → ?); [2: cases(ret_costed_abs ??) normalize nodelta [|#lbl'']]
370    #EQ destruct ****** [2: *] #EQ destruct @⊥ cases Hlbl #H @H %
371  | * [|#lbl'] #EQcont_s1' normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct ****** [2: *] #EQ destruct
372    cases cost_lbl #HH2 #EQ destruct #EQget #EQ_cleaned #EQstore #EQio #EQ destruct
373    >EQcode_s1 in EQ_cleaned; inversion(code ? s1')
[3550]374    [2,3,4,5,6,7: [ #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
375            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
376          #_ whd in ⊢ (??%% → ?);
377          [ | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
378          | cases(call_post_clean ?????); normalize nodelta
379            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
380               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
381                 [| #z cases(?∧?) normalize nodelta
382                 ]
383               ]
384            ]
385          | cases(call_post_clean ?????) normalize nodelta
386            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
387               [| #y cases(?∧?) normalize nodelta
388               ]
389            ]
390          | cases(call_post_clean ?????) normalize nodelta
391             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
392                [ cases (?==?) normalize nodelta ]
393             ]]
394          | cases(call_post_clean ?????) normalize nodelta
395             [| #x cases(? ∧ ?) normalize nodelta ]
396          ]
397          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct] #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct
[3551]398    #_ %{gen_labels} %{(mk_state … i' stack' (store … s1') false)} %
[3535]399    [% [ @(empty … EQcode_s1' EQcont_s1') // #_ %{lbl'} %]
400       whd >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta % // % // % // % // >EQclean %]
401   whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >EQget >append_nil %
402 ]
403| #s1 #s2 #seq #i #store * [|#lbl] #EQcode_s1 #EQeval #EQ destruct #EQcont #EQ destruct #Hio1 #Hio2 *
404  whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta
405  [#_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
[3550]406  [1,2,4,5,6,7: [ | #ret | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
407            #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ]
408          #_ whd in ⊢ (??%% → ?);
409          [ |
410          | cases(call_post_clean ?????); normalize nodelta
411            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
412               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
413                 [| #z cases(?∧?) normalize nodelta
414                 ]
415               ]
416            ]
417          | cases(call_post_clean ?????) normalize nodelta
418            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
419               [| #y cases(?∧?) normalize nodelta
420               ]
421            ]
422          | cases(call_post_clean ?????) normalize nodelta
423             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
424                [ cases (?==?) normalize nodelta ]
425             ]]
426          | cases(call_post_clean ?????) normalize nodelta
427             [| #x cases(? ∧ ?) normalize nodelta ]
428          ]
429          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct] #seq' #opt_l' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?);
[3535]430  inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #genlab #cleaned #EQcleaned
431  cases opt_l' in EQcode_s1'; normalize nodelta [|#lbl'] #EQcode_s1' [| inversion(?==?) normalize nodelta #EQget]
[3551]432  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQst #EQioinfo #EQ destruct #_
[3535]433  %{genlab} %{(mk_state … i' (cont … s1') (store … s2) false)} % [ %
434  [ @(seq_sil … EQcode_s1') // ]
435  whd <EQcont >EQcheck normalize nodelta % // % // % // % // >EQcleaned %]
436  whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >(\P EQget) >append_nil %
[3551]437| #s1 #s2 #cond #ltrue #i_true #lfalse #i_false #instr #mem #EQcode_s1 #EQcond #EQcont_s2 #EQ1 #EQ2 destruct
438  #Hio1 #Hio2 #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) [ #_ *]
439  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
440  [1,2,3,5,6,7:
441    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_
442       | #lin #io #lout #instr #_ ]
443          #_ whd in ⊢ (??%% → ?);
444          [ |
445          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
446          | cases(call_post_clean ?????) normalize nodelta
447            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
448               [| #y cases(?∧?) normalize nodelta
449               ]
450            ]
451          | cases(call_post_clean ?????) normalize nodelta
452             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
453                [ cases (?==?) normalize nodelta ]
454             ]]
455          | cases(call_post_clean ?????) normalize nodelta
456             [| #x cases(? ∧ ?) normalize nodelta ]
457          ]
458          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
459  ]
460  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
461  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
462  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
463  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
464  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
465  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct #_
466  %{a_top3} %{(mk_state … i_true' (〈cost_act … (None ?),instrs'〉::(cont … s1')) (store … s2) false)} %
467  [2: whd in ⊢ (??%%); >(\P EQget1) >append_nil % ] %
468  [ @(cond_true … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????);
469  change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
470  >EQinstr' normalize nodelta % // % // % // % [ % // % //] >EQi_true' %
471| #s1 #s2 #cond #ltrue #i_true #lfalse #i_false #instr #mem #EQcode_s1 #EQcond #EQcont_s2 #EQ1 #EQ2 destruct
472  #Hio1 #Hio2 #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) [ #_ *]
473  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
474  [1,2,3,5,6,7:
475    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_
476       | #lin #io #lout #instr #_ ]
477          #_ whd in ⊢ (??%% → ?);
478          [ |
479          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
480          | cases(call_post_clean ?????) normalize nodelta
481            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
482               [| #y cases(?∧?) normalize nodelta
483               ]
484            ]
485          | cases(call_post_clean ?????) normalize nodelta
486             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
487                [ cases (?==?) normalize nodelta ]
488             ]]
489          | cases(call_post_clean ?????) normalize nodelta
490             [| #x cases(? ∧ ?) normalize nodelta ]
491          ]
492          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
493  ]
494  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
495  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
496  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
497  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
498  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
499  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct #_
500  %{a_top2} %{(mk_state … i_false' (〈cost_act … (None ?),instrs'〉::(cont … s1')) (store … s2) false)} %
501  [2: whd in ⊢ (??%%); >(\P EQget2) >append_nil % ] %
502  [ @(cond_false … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????);
503  change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
504  >EQinstr' normalize nodelta % // % // % // % [ % // % //] >EQi_false' %
505| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
506  #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
507  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
508  [1,2,3,4,6,7:
509    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_
510       | #lin #io #lout #instr #_ ]
511          #_ whd in ⊢ (??%% → ?);
512          [ |
513          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
514          | cases(call_post_clean ?????); normalize nodelta
515            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
516               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
517                 [| #z cases(?∧?) normalize nodelta
518                 ]
519               ]
520            ]
521          | cases(call_post_clean ?????) normalize nodelta
522             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
523                [ cases (?==?) normalize nodelta ]
524             ]]
525          | cases(call_post_clean ?????) normalize nodelta
526             [| #x cases(? ∧ ?) normalize nodelta ]
527          ]
528          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
529   ]
530   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
531   inversion(call_post_clean …) normalize nodelta [ #_ #EQ destruct] * #a_top1 #i_false''
532   #EQi_false' inversion(call_post_clean …) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true''
533   #EQi_true' >m_return_bind inversion(?==?) normalize nodelta #EQget1 [2: #EQ destruct]
534   inversion(?==?) normalize nodelta #EQget2 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
535   #EQstore #EQio #EQ destruct #_ %{a_top2}
536   %{(mk_state … i_true' (〈cost_act … (None ?),LOOP … exp ltrue i_true' lfalse i_false'〉::(cont … s1')) (store … s2) false)}
537   % [2: whd in ⊢ (??%%); >(\P EQget1) >append_nil % ] %
538    [ @(loop_true … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????);
539    change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
540    whd in match (call_post_clean ??????); >EQi_false' normalize nodelta >EQi_true'
541    >m_return_bind >(\P EQget1) >(\P EQget2) >(\b (refl …)) >(\b (refl …)) normalize nodelta
542    % // % // % // % [ % // % //] >EQi_true' %
543| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2
544  #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
545  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
546  [1,2,3,4,6,7:
547    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_
548       | #lin #io #lout #instr #_ ]
549          #_ whd in ⊢ (??%% → ?);
550          [ |
551          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
552          | cases(call_post_clean ?????); normalize nodelta
553            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
554               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
555                 [| #z cases(?∧?) normalize nodelta
556                 ]
557               ]
558            ]
559          | cases(call_post_clean ?????) normalize nodelta
560             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
561                [ cases (?==?) normalize nodelta ]
562             ]]
563          | cases(call_post_clean ?????) normalize nodelta
564             [| #x cases(? ∧ ?) normalize nodelta ]
565          ]
566          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
567   ]
568   #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
569   inversion(call_post_clean …) normalize nodelta [ #_ #EQ destruct] * #a_top1 #i_false''
570   #EQi_false' inversion(call_post_clean …) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true''
571   #EQi_true' >m_return_bind inversion(?==?) normalize nodelta #EQget1 [2: #EQ destruct]
572   inversion(?==?) normalize nodelta #EQget2 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
573   #EQstore #EQio #EQ destruct #_ %{a_top1}
574   %{(mk_state … i_false' (cont … s1') (store … s2) false)}
575   % [2: whd in ⊢ (??%%); >(\P EQget2) >append_nil % ] %
576    [ @(loop_false … EQcode_s1') // ] >EQcont_s2 >EQcheck normalize nodelta
577    % // % // % // % // >EQi_false' %
[3535]578| #s1 #s2 #lin #io #lout #i #store #EQcode_s1 #EQeval #EQcode_s2 #EQcont_s2. #EQ destruct #EQio_s2 *
579  whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta [#_ *]
580  ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code ? s1')
[3550]581  [1,2,3,4,5,6:  [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
582        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ ]
583          #_ whd in ⊢ (??%% → ?);
584          [ |
585          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
586          | cases(call_post_clean ?????); normalize nodelta
587            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
588               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
589                 [| #z cases(?∧?) normalize nodelta
590                 ]
591               ]
592            ]
593          | cases(call_post_clean ?????) normalize nodelta
594            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
595               [| #y cases(?∧?) normalize nodelta
596               ]
597            ]
598          | cases(call_post_clean ?????) normalize nodelta
599             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
600                [ cases (?==?) normalize nodelta ]
601             ]]
602          ]
603          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ]
[3535]604  #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct]
605  * #genlab #cleaned #EQcleaned inversion(?∧?) normalize nodelta #EQget whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
[3551]606  #EQ destruct #EQstore_s1_s1' #EQioinfo #EQ destruct #_ %{[]}
[3549]607  %{(mk_state … (EMPTY …) (〈cost_act p (Some ? lout),i'〉::(cont … s1')) (store … s2) true)} % [%
[3535]608  [ @(io_in … EQcode_s1') // ]
[3549]609  whd >EQcont_s2 whd in match (check_continuations ??????); change with (check_continuations ??????) in match (foldr2 ???????);
[3535]610  >EQcheck normalize nodelta >EQcleaned normalize nodelta % // % // % // % [2: >EQcode_s2 %] %
611  [2: cases(andb_Prop_true … (bool_true … EQget)) #H #_ >(\P (bool_true … H)) % ] % // % //]
612  cases(andb_Prop_true … (bool_true … EQget)) #_ #EQget'
613  whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >append_nil >append_nil inversion(? == ?) in EQget';
614  [2: #_ *] #EQget' #_ >(\P EQget') %
[3551]615| #s1 #s2 #f #act_p #r_lb #i #mem #env_it #EQcode_s1 #EQlook #EQeval #EQ destruct #EQcode_s2 #EQcont_s2
616  #Hio1 #Hio2 * whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta
617  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1')
618   [1,2,3,4,5,7:
619    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
620        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #lin #io #lout #instr #_  ]
621          #_ whd in ⊢ (??%% → ?);
622          [ |
623          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
624          | cases(call_post_clean ?????); normalize nodelta
625            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
626               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
627                 [| #z cases(?∧?) normalize nodelta
628                 ]
629               ]
630            ]
631          | cases(call_post_clean ?????) normalize nodelta
632            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
633               [| #y cases(?∧?) normalize nodelta
634               ]
635            ]
636         | cases(call_post_clean ?????) normalize nodelta
637             [| #x cases(? ∧ ?) normalize nodelta ]
638         ]
639         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
640     ]
641     #f' #act_p' #r_lb #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean …) normalize nodelta
642     [ #_ #EQ destruct] * #a_top1 #i'' #EQi' inversion(r_lb) normalize nodelta [ #_ #EQ destruct] #lbl #EQ
643     destruct inversion(? ∈ ?) normalize nodelta #EQmem [ inversion(?==?) normalize nodelta #EQget]
644     whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct
645     lapply(trans_env_ok … no_dup) >EQt_prog normalize nodelta #H cases(H … EQlook) -H #env_it' * #n
646     ** #Hfresh #EQlook' ***** #EQt_code #EQget1 #EQsig #EQlab #same_fresh #same_keep whd in match (is_call_post_label ???);
647     >EQcode_s1 normalize nodelta [ #_ | * %{f} %{(f_lab … env_it)} %]
648     %{(gen_labels … (call_post_trans … (f_body … env_it) n []))}
649     %{(mk_state … (f_body … env_it') (〈ret_act … (Some … lbl),i'〉 :: (cont … s1')) (store … s2) false)}
650     % [2,4: whd in ⊢ (??%%); >append_nil >EQlab >EQget1 % ] % [1,3: >EQlab @(call … EQcode_s1') //]
651     >EQcont_s2 whd in match (check_continuations ??????);
652     change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta
653     >EQi' normalize nodelta whd in match ret_costed_abs; normalize nodelta >EQmem normalize nodelta
654     % // % // % // % [ % [ % // % //]  >(\P EQget) % ] <EQt_code @inverse_call_post_trans //
655     [ >EQcode_s2 @no_duplicates_domain_of_fun //
656     | >EQcode_s2 #H20 #H21 >same_fresh //
657     | >EQcode_s2 #H23 #H24 >same_keep //
658     ]
659| #s1 #s2 #r_t #mem #stack * [|#lbl] #i #EQcode_s1 #EQcont_s1 #EQ destruct #Hio1 #Hio2 #EQeval #EQ1 #EQ2 destruct *
660  whd in match state_rel; normalize nodelta >EQcont_s1 inversion(cont … s1') [| * #lab #i' #stack' #_ ] #EQcont_s1'
661  whd in match (check_continuations ??????); [*] change with (check_continuations ??????) in match (foldr2 ???????);
662  inversion(check_continuations ??????) normalize nodelta [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta
663  inversion(call_post_clean …) normalize nodelta [ #_ *****] * #a_top1 #i'' #EQi' inversion lab normalize nodelta
664  [ #f #lb ****** |3: * [| #x] #EQ destruct normalize nodelta ****** [|*] #EQ destruct] * [|#lb] #EQ destruct
665  normalize nodelta [****** #EQ destruct] whd in match ret_costed_abs; normalize nodelta inversion(? ∈ ?) #EQmem
666  normalize nodelta ****** [*] #EQ destruct #HH1 #EQ destruct #EQget >EQcode_s1 inversion(code … s1')
667  [1,3,4,5,6,7:
668       [ | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_|
669        #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_  ]
670          #_ whd in ⊢ (??%% → ?);
671          [
672          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
673          | cases(call_post_clean ?????); normalize nodelta
674            [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
675               [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
676                 [| #z cases(?∧?) normalize nodelta
677                 ]
678               ]
679            ]
680          | cases(call_post_clean ?????) normalize nodelta
681            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
682               [| #y cases(?∧?) normalize nodelta
683               ]
684            ]
685         | cases(call_post_clean ?????) normalize nodelta
686             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
687                [ cases (?==?) normalize nodelta ]
688             ]]
689         | cases(call_post_clean ?????) normalize nodelta
690             [| #x cases(? ∧ ?) normalize nodelta ]
691         ]
692         whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
693   ] #r_t' #EQcode_s1' whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
694  #EQstore #EQio #EQ destruct #_
695  %{a_top1} %{(mk_state … i' stack' (store … s2) false)} % [2: whd in ⊢ (??%%); >EQget >append_nil %]
696  % [ @(ret_instr … EQcode_s1' … EQcont_s1') // ] >EQcheck normalize nodelta % // % // % // % // >EQi' %
697
[3535]698qed.
699
700include "Vm.ma".
701
702theorem correctness_theorem : ∀p,p',prog.
703no_duplicates_labels … prog →
704let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
705∀si,s1,s2,sn,si' : state p.∀abs_top,abs_tail.
[3549]706∀t : raw_trace p (operational_semantics … p' prog) si sn.
707measurable p (operational_semantics p p' prog) … s1 s2 … t →
[3535]708state_rel … m keep abs_top abs_tail si si' →
[3549]709∃abs_top',abs_tail'.∃sn'.∃t' : raw_trace p (operational_semantics … p' t_prog) si' sn'.
[3535]710state_rel  … m keep abs_top' abs_tail' sn sn' ∧
[3549]711is_permutation ? (map_labels_on_trace … m (chop … (get_costlabels_of_trace … t))) 
[3535]712                  (chop … (get_costlabels_of_trace … t')) ∧
713                  ∃s1',s2'.
[3549]714measurable p (operational_semantics … p' t_prog)  … s1' s2' … t'.
[3535]715#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
716#si #s1 #s3 #sn #si' #abs_top #abs_tail #t *  #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2
717* #prf1 * #prf2 ******* #pre_t12 #EQ destruct #Hl1 #Hl2 #Hcall_fin #sil_ti0 #sil_t3n #Hcall_init #Rsi_si'
718lapply(silent_in_silent … p' prog no_dup) >EQt_prog normalize nodelta #Hsilent
719cases(Hsilent … sil_ti0 … Rsi_si')
720#abs_top1 * #s0' * #t_i0' * #Rs0_s0' #sil_ti0'
721lapply(labelled_action_is_correct … p' prog no_dup) >EQt_prog normalize nodelta #Hmove
[3551]722cases(Hmove … prf1 … Rs0_s0') // [2: @Hcall_init]
[3535]723#abs_top2 * #s1' ** #prf1' #Rs1_s1' #EQmap_l1
724lapply(correctness_lemma … p' prog no_dup) >EQt_prog normalize nodelta #H
725cases(H … pre_t12 … Rs1_s1') -H
726#abs_top3 * #s2' * #t12' ***** #Rs2_s2' #Hperm #_ #_ #pre_t12' #_
[3551]727cases(Hmove … prf2 … Rs2_s2') -Hmove // [2: @Hcall_fin]
[3535]728#abs_top4 * #s3' ** #prf2' #Rs3_s3' #EQmap_l2
729cases(Hsilent … sil_t3n … Rs3_s3')
730#abs_top5 * #sn' * #t3n' * #Rsn_sn' #sil_t3n'
731%{abs_top5} %{abs_tail} %{sn'}
732%{(t_i0' @ (t_ind … prf1' (t12' @ (t_ind … prf2' t3n'))))} %
733[ %{Rsn_sn'} >get_cost_label_append >get_cost_label_append >(get_cost_label_silent_is_empty … sil_ti0)
734  >(get_cost_label_silent_is_empty … sil_ti0') >(get_cost_label_append … (t_ind … (t_base …)))
735  >(get_cost_label_append … (t_ind … (t_base …))) in ⊢ (???%); >get_cost_label_append
736  >get_cost_label_append whd in match (get_costlabels_of_trace … (t_ind … t3n));
737  whd in match (get_costlabels_of_trace … (t_ind … t3n'));
738  >(get_cost_label_silent_is_empty … sil_t3n) >(get_cost_label_silent_is_empty … sil_t3n')
739  >append_nil cases(actionlabel_ok … Hl2) #c2 #EQc2 >EQc2 <associative_append <associative_append
740  <associative_append >chop_append_singleton <associative_append <associative_append >chop_append_singleton
[3549]741  >append_nil whd in match (get_costlabels_of_trace ???? (t_ind ? (operational_semantics p p' t_prog) … prf1' (t_base …)));
[3535]742  >append_nil >map_labels_on_trace_append >EQmap_l1 >associative_append @is_permutation_append_left_cancellable
743  lapply(top_move_source_is_empty … p' prog) >EQt_prog normalize nodelta #H
744  >(proj1 … (H … prf2 Hl2 … Rs2_s2')) in Hperm; [2: assumption] >append_nil @permute_equal_right
745| %{s1'} %{s3'} whd %{s0'} %{s2'} %{t_i0'} %{t12'} %{t3n'} %{l1} %{l2} %{prf1'} %{prf2'}
746  % [2: lapply(top_move_source_is_empty … p' prog) >EQt_prog normalize nodelta #H
747  @(proj2 … (H … prf1 Hl1 … Rs0_s0')) assumption ] % // % // %
748  [2: lapply(top_move_source_is_empty … p' prog) >EQt_prog normalize nodelta #H
749  @(proj2 … (H … prf2 Hl2 … Rs2_s2')) assumption ] % // % // % //
750]
751qed.
Note: See TracBrowser for help on using the repository browser.