source: src/Clight/labelSimulation.ma @ 1922

Last change on this file since 1922 was 1922, checked in by campbell, 8 years ago

Main labelling simulation proof complete.

File size: 52.4 KB
Line 
1
2include "Clight/label.ma".
3include "Clight/Cexec.ma".
4
5(* for the induction principle *)
6include "Clight/CexecSound.ma".
7
8(* TODO: make something general that can live in common/Globalenvs.ma. *)
9record related_globals (ge:genv) (ge':genv) : Prop ≝ {
10  rg_find_symbol: ∀s.
11    find_symbol ?? ge s = find_symbol ?? ge' s;
12  rg_find_funct: ∀v,f.
13    find_funct ?? ge v = Some ? f →
14    find_funct ?? ge' v = Some ? (label_fundef f)
15}.
16
17lemma commute_fst_pair : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → B → C×D.
18  \fst (let 〈x,y〉 ≝ e in F x y) =  let 〈x,y〉 ≝ e in \fst (F x y).
19#A #B #C #D * //
20qed.
21
22lemma shift_fst : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → C.∀G:B → D.
23  \fst (let 〈x,y〉 ≝ e in 〈F x, G y〉) =  F (\fst e).
24#A #B #C #D * //
25qed.
26
27(* lemma to break up label_expr, label_exprs and label_statement in the labelling
28   functions *)
29lemma label_gen_elim : ∀Syn:Type[0].∀syn,u.∀T:Type[0].∀L:Syn → universe CostTag → Syn × (universe CostTag). ∀F:Syn → universe CostTag → T. ∀P:T → Type[0].
30  (∀u'. P (F (\fst (L syn u)) u')) →
31  P (let 〈syn',u'〉 ≝ L syn u in F syn' u').
32#Syn #syn #u #T #L #F #P
33cases (L syn u)
34#syn' #u' #H @H
35qed.
36
37lemma add_cost_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0].
38  (∀u',l. P (F (Expr (Ecost l e) (typeof e)) u')) →
39  P (let 〈e',u'〉 ≝ add_cost_expr e u in F e' u').
40#e #u #T #F #P #H whd in match (add_cost_expr ??);
41cases (fresh ??) #l #u' @H
42qed.
43
44
45
46lemma label_expr_type : ∀e,u.
47  typeof (\fst (label_expr e u)) = typeof e.
48* #e #ty #u >shift_fst //
49qed.
50
51inductive trace_with_extra_labels : trace → trace → Prop ≝
52| twel_0 : trace_with_extra_labels E0 E0
53| twel_both : ∀h,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels (h::t1) (h::t2)
54| twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
55
56lemma twel_refl : ∀tr. trace_with_extra_labels tr tr.
57#tr elim tr /2/
58qed.
59
60lemma twel_app : ∀tr1,tr2,tr1',tr2'.
61  trace_with_extra_labels tr1 tr1' →
62  trace_with_extra_labels tr2 tr2' →
63  trace_with_extra_labels (tr1⧺tr2) (tr1'⧺tr2').
64#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
65qed. 
66
67definition expr_lvalue_ind_combined ≝
68λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
69conj ??
70 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
71 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
72
73lemma label_expr_ok : ∀ge,ge',en,m.
74  related_globals ge ge' →
75  (∀e,v,tr.
76   exec_expr ge en m e = OK … 〈v,tr〉 →
77   ∀u. ∃tr'. exec_expr ge' en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧
78             trace_with_extra_labels tr tr') ∧
79  (∀e,ty,b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 →
80          ∀u. ∃tr'. exec_lvalue' ge' en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧
81                    trace_with_extra_labels tr tr').
82#ge #ge' #en #m #RG @expr_lvalue_ind_combined
83[ 1,2: normalize /3 by ex_intro, conj/
84| * //
85 [ #id #ty #IH #v #tr #EX #u
86   cases (bind_inversion ????? EX) -EX * * #b #o #tr1 * #EX1 #EX
87   cases (bind_inversion ????? EX) -EX #v2 * #EX2 #EX
88   normalize in EX; destruct
89   cases (IH … EX1 u) #tr1' * #EX1' #T1
90   %{(tr1')} % [ whd in ⊢ (??%?); >EX1' whd in ⊢ (??%?); >EX2 @refl | // ]
91 | #e1 #ty #IH #v #tr #EX #u
92   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
93   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
94   normalize in EXrem; destruct
95   cases (IH … EX1 u) #tr1' * #EX1' #twel1
96   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (?(??%?)?); >EX1'
97   whd in ⊢ (?(??%?)?); >EXl /2/
98 | #e1 #id #ty #IH #v #tr #EX #u
99   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
100   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
101   normalize in EXrem; destruct
102   cases (IH … EX1 u) #tr1' * #EX1' #twel1
103   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' % // whd in ⊢ (??%?); >EX1'
104   whd in ⊢ (??%?); >EXl @refl
105 ]
106| #v #ty #b #o #tr #EX #u %{tr} % [
107    whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %;
108    [ whd in ⊢ (??%? → ??%?); >(rg_find_symbol … RG) //
109    | #b // ]
110  | // ]
111| #e1 #ty #IH #b #o #tr #EX #u
112  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
113  cases (IH … EX1 u) #tr1' * #EX1' #twel1
114  %{tr1'} >shift_fst whd in ⊢ (?(??%?)?); >EX1'
115  whd in ⊢ (?(??%?)?);
116  cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct /2/
117| #ty' #e1 #ty #IH #v #tr #EX #u
118  cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
119  cases (IH … EX1 u) #tr1' * #EX1' #twel1
120  %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (?(??%?)?);
121  whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EX1'
122  whd in ⊢ (?(??%?)?);
123  cases ty' in EX1rem ⊢ %;
124  [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r)
125       #pc normalize #E destruct /2/
126  | *: normalize #A try #B try #C try #D destruct
127  ]
128| #ty #op #e1 #IH #v #tr #EX #u
129  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
130  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EXrem
131  normalize in EXrem; destruct
132  cases (IH … EX1 u) #tr1' * #EX1' #twel1
133  %{tr1'} % // >shift_fst
134  whd in ⊢ (??(????(?(???%)?))?);
135  @label_gen_elim #u2
136  whd in ⊢ (??%?); >EX1'
137  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
138| #ty #op #e1 #e2 #IH1 #IH2 #v #tr #EX
139  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
140  cases (bind_inversion ????? EX1rem) * #v2 #tr2 * #EX2 #EX2rem
141  cases (bind_inversion ????? EX2rem) #v' * #EXop #EXop'
142  #u
143  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
144  >shift_fst
145  whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
146  @label_gen_elim #u2
147  cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
148  @label_gen_elim #u3 %{(tr1'⧺tr2')}
149  whd in ⊢ (?(??%?)?); >EX1'
150  whd in ⊢ (?(??%?)?); >EX2'
151  whd in ⊢ (?(??%?)?); >label_expr_type >label_expr_type >EXop
152  normalize in EXop'; destruct % /2/
153| #ty #ty' #e1 #IH #v #tr #EX #u
154  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
155  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EX2rem
156  normalize in EX2rem; destruct
157  cases (IH … EX1 u) #tr1' * #EX1' #twel1
158  %{tr1'} % // >shift_fst >shift_fst
159  whd in ⊢ (??%?); >EX1'
160  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
161| #ty #e1 #e2 #e3 #IH1 #IH2 #IH3 #v #tr #EX #u
162  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
163  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
164  cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
165  normalize in EX2rem; destruct
166  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
167  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
168  @label_gen_elim #u2
169  @label_gen_elim #u3
170  @add_cost_expr_elim #u4 #l4
171  @label_gen_elim #u5
172  @add_cost_expr_elim #u6 #l6
173  [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx
174  [ %{(tr1'⧺trx'⧺(Echarge l4))} | %{(tr1'⧺trx'⧺(Echarge l6))} ]
175  whd in ⊢ (?(??%?)?); >EX1'
176  whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
177  whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EXx'
178  normalize % // @twel_app // <(E0_right tr2) @twel_app /2/
179| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
180  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
181  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
182  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
183  @label_gen_elim #u2
184  @label_gen_elim #u3
185  @add_cost_expr_elim #u4 #l4
186  @add_cost_expr_elim #u5 #l5
187  [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
188    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
189    -EX1rem -EXguardrem -EX2rem
190    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
191    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
192    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)}
193    whd in ⊢ (?(??%?)?); >EX1'
194    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
195    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
196    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
197    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
198    normalize in EX3rem ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
199  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
200    %{(tr1'⧺E0⧺Echarge l5)}
201    whd in ⊢ (?(??%?)?); >EX1'
202    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
203    normalize in EXguardrem; destruct % // <(E0_right tr) @twel_app /2/
204  ]
205| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
206  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
207  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
208  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
209  @label_gen_elim #u2
210  @add_cost_expr_elim #u4 #l4
211  @label_gen_elim #u3
212  @add_cost_expr_elim #u5 #l5
213  [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
214    %{(tr1'⧺Echarge l4)}
215    whd in ⊢ (?(??%?)?); >EX1'
216    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
217    normalize in EXguardrem ⊢ %; destruct % // <(E0_right tr) /3/
218  | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
219    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
220    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
221    cases (IH2 … EX2 u4) #tr2' * #EX2' #twel2
222    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)}
223    whd in ⊢ (?(??%?)?); >EX1'
224    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
225    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
226    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
227    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
228    normalize in EX3rem ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
229  ]
230| #ty #ty' #v #tr normalize /3/
231| #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %;
232  [ 7: #id #fl #IH #EX
233    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
234    cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem
235    whd in EXoffrem:(???%); destruct >shift_fst >shift_fst
236    cases (IH … EX1 u) #tr1' * #EX1' #twel1
237    %{tr1'} % //
238    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
239    whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl
240  | 8: #id #fl #IH #EX
241    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
242    whd in EX1rem:(???%); destruct >shift_fst >shift_fst
243    cases (IH … EX1 u) #tr1' * #EX1' #twel1
244    %{tr1'} % //
245    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
246    whd in ⊢ (??%?); @refl
247  | *: normalize #A #B try #C try #D try #F destruct
248  ]
249| #ty #l #e1 #IH #v #tr #EX #u
250  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
251  whd in EX1rem:(???%); destruct
252  cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(tr1'@Echarge l)}
253  >shift_fst >shift_fst whd in ⊢ (?(??%?)?); >EX1'
254  whd in ⊢ (?(??%?)?); /3/
255| #e1 #ty #NLV #b #o #tr #EX @⊥
256  cases e1 in NLV EX; normalize //
257  #A #B #C try #D try #F destruct
258] qed.
259
260lemma label_exprs_ok : ∀ge,ge'.
261   related_globals ge ge' →
262   ∀en,m,es,vs,tr.
263   exec_exprlist ge en m es = OK … 〈vs,tr〉 →
264   ∀u. ∃tr'. exec_exprlist ge' en m (\fst (label_exprs es u)) = OK … 〈vs,tr'〉 ∧
265             trace_with_extra_labels tr tr'.
266#ge #ge' #RG #en #m #es elim es
267[ #vs #tr #EX whd in EX:(??%?); destruct #u %{E0} /2/
268| #e #tl #IH #vs #tr #EX
269  cases (bind_inversion ????? EX) -EX * #v1 #tr1 * #EX1 #EX
270  cases (bind_inversion ????? EX) -EX * #tl' #tr' * #EX2 #EX
271  whd in EX:(??%%); destruct
272  #u whd in match (label_exprs ??); @label_gen_elim #u' >shift_fst
273  cases (proj1 ?? (label_expr_ok ge ge' en m RG) ??? EX1 u) #tr1' * #EX1' #T1
274  cases (IH … EX2 u') #tr'' * #EX2' #T2
275  % [2: % [ whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
276    whd in ⊢ (??%?); >EX2' in ⊢ (??%?); @refl
277  | /2/ ] | skip ]
278] qed.
279
280(* Plan:
281     - extend labelling functions to continuations and hence states
282       NO - this doesn't work because we don't know *which* cost labels to add
283       realistically we'll have to define erasure functions
284       BETTER - use predicate so that we don't need to insist on the absence of
285       cost labels in the source
286     - build a simulation relation linking states to their labelled counterparts
287     - write a predicate stating that two traces are the same except for some
288       extra costs
289     - show some labelling relationship for global environments
290     - prove that
291         exec_step ge s1 = = Value … 〈tr,s2〉 →
292         cost_related s1 s1' →
293         ∃tr'. equal_up_to_costs tr tr' ∧
294               plus ge' s1' tr' s2' ∧
295               cost_related s2 s2'
296       using some relationship between ge and ge'.
297*)
298
299inductive cont_with_labels : cont → cont → Prop ≝
300| cwl_stop : cont_with_labels Kstop Kstop
301| cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k')
302| cwl_while : ∀ue,e,us,s,cs,cpost,k,k'.
303    cont_with_labels k k' →
304    cont_with_labels (Kwhile e s k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
305| cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'.
306    cont_with_labels k k' →
307    cont_with_labels (Kdowhile e s k) (Kdowhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
308| cwl_for1 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'.
309    cont_with_labels k k' →
310    cont_with_labels (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2)))) (Kseq (Scost cpost Sskip) k'))
311| cwl_for2 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor2 e s1 s2 k) (Kfor2 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
312| cwl_for3 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor3 e s1 s2 k) (Kfor3 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
313| cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k')
314| cwl_call : ∀r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (label_function f) en k')
315| cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' →
316    cont_with_labels (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (\fst (label_lstatements ls u))) k').
317
318lemma call_cont_with_labels : ∀k,k'.
319  cont_with_labels k k' →
320  cont_with_labels (call_cont k) (call_cont k').
321#k0 #k0' #K elim K /2/
322qed.
323
324inductive state_with_labels_partial : state → state → Prop ≝
325| swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m)
326(* Extra matching states that we can reach that don't quite correspond to the
327   labelling function *)
328| swl_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
329    state_with_labels_partial (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
330| swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
331    state_with_labels_partial (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
332| swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
333    state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
334(* and the rest *)
335| swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (label_fundef fd) args k' m)
336| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
337| swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r)
338.
339
340(* We handle the switch states after the rest so that we can reuse the partial
341   result. *)
342inductive state_with_labels : state → state → Prop ≝
343| swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s'
344| swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' →
345    state_with_labels (State f (seq_of_labeled_statement ls) k e m)
346                      (State (label_function f) (seq_of_labeled_statement (\fst  (label_lstatements ls u))) k' e m)
347.
348
349inductive plus (ge:genv) : state → trace → state → Prop ≝
350| plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2
351| plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3.
352
353definition eplus ≝ λn. repeat n io_out io_in clight_fullexec.
354
355inductive hplus (ge:genv) : state → trace → trace → state → Prop ≝
356| hplus_one : ∀tr,s2,s1',tr1,tr2,s2'.
357    exec_step ge s1' = OK … 〈tr2,s2'〉 →
358    trace_with_extra_labels tr (tr1⧺tr2) →
359    state_with_labels s2 s2' →
360    hplus ge s1' tr1 tr s2
361| hplus_succ : ∀s1,tr,s2,tr1,tr2,s3.
362    exec_step ge s1 = OK … 〈tr2,s2〉 →
363    hplus ge s2 (tr1⧺tr2) tr s3 →
364    hplus ge s1 tr1 tr s3.
365
366lemma label_function_return : ∀f.
367  fn_return (label_function f) = fn_return f.
368* #rty #params #vars #body
369whd in ⊢ (??(?%)?);
370cases (label_statement ??) #body' #u'
371whd in ⊢ (??(?%)?);
372cases (add_cost_before ??) #body'' #u''
373//
374qed.
375
376lemma bindIO_inversion: ∀O,I.
377  ∀A,B: Type[0]. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
378  (f »= g = return y) →
379  ∃x. (f = return x) ∧ (g x = return y).
380#O #I #A #B #f #g #y cases f normalize
381[ #o #k #E destruct
382| #a #e %{a} /2 by conj/
383| #m #H destruct (H)
384] qed.
385
386lemma io_eq_to_res : ∀O,I. ∀T:Type[0]. ∀e:res T. ∀v.
387  err_to_io … e = Value O I T v →
388  e = OK T v.
389#O #I #T *
390[ #e #v #E normalize in E; destruct @refl
391| #m #v #E normalize in E; destruct
392]
393qed.
394
395coercion io_eq_from_res :
396  ∀O,I,T,e,v. ∀E:err_to_io O I T e = Value O I T v. e = OK T v ≝ io_eq_to_res
397  on _E:eq (IO ???) ?? to eq (res ?) ??.
398
399lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u.
400  exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) =
401  exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty.
402#ge #e #m #a #ty #u
403whd in ⊢ (??(????(???%))?); >shift_fst @refl
404qed.
405
406lemma label_expr_fun_typeof : ∀a,u.
407  fun_typeof (\fst (label_expr a u)) = fun_typeof a.
408#a #u whd in ⊢ (??%?); >label_expr_type @refl
409qed.
410
411lemma label_fundef_typeof_fundef : ∀fd.
412  type_of_fundef (label_fundef fd) = type_of_fundef fd.
413* //
414* #rty #args #vars #body
415normalize cases (label_statement ??) #body' #u
416normalize cases (fresh ??) //
417qed.
418
419lemma opt_find_funct : ∀ge,ge',m,vf,fd.
420  related_globals ge ge' →
421  opt_to_io io_out io_in … m (find_funct ?? ge vf) = Value … fd →
422  opt_to_io io_out io_in … m (find_funct ?? ge' vf) = Value … (label_fundef fd).
423#ge #ge' #m #vf #fd #RG
424lapply (rg_find_funct … RG … vf fd)
425cases (find_funct … vf)
426[ #_ #E normalize in E; destruct
427| #fd' #H #E normalize in E; destruct >(H (refl ??)) //
428] qed.
429
430(*
431lemma step_with_labels : ∀ge,s1,s1',tr,s2.
432  state_with_labels s1 s1' →
433  exec_step ge s1 = OK … 〈tr,s2〉 →
434  hplus ge s1' E0 tr s2.
435#ge #Xs1 #Xs1' #tr #s2 *
436[ #f #us #s #k #k' #e #m #KL cases s
437  [ #EX inversion KL
438    [ #E1 #E2 #_ destruct @hplus_one [3: whd in EX:(??%?) ⊢ (??%?);
439      >label_function_return >EX in ⊢ (??%?); | 1,2:skip | // | %1
440      cases f in EX ⊢ %; #rty #params #vars #body #EX whd in ⊢ (??(match ?% with [_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?|_⇒?])?); >EX
441     whd in EX:(??%?) ⊢ (??(λ_.?(?(??%?)?)?));
442
443lemma step_with_labels : ∀ge,s1,s1',tr,s2.
444  state_with_labels s1 s1' →
445  exec_step ge s1 = OK … 〈tr,s2〉 →
446  ∃n,tr',s2'. eplus n ge s1' = OK … 〈tr',s2'〉 ∧
447            trace_with_extra_labels tr tr' ∧
448            state_with_labels s2 s2'.
449#ge #Xs1 #Xs1' #tr #s2 *
450[ #f #us #s #k #k' #e #m #KL cases s
451  [ #EX %{1} %{tr} inversion KL
452    [ #E1 #E2 #_ destruct
453     whd in EX:(??%?) ⊢ (??(λ_.?(?(??%?)?)?));
454     whd in EX:(??%?) ⊢ (??(λ_.?(?(??(?????%?)?)?)?));
455     normalize in EX:(??%?) ⊢ (??(λ_.?(?(??(%??????)?)?)?));
456      % [2: % [ % [ @plus_one whd in EX:(??%?) ⊢ (??%?); >EX whd in ⊢ (??(??(??%???))?); @EX >EX @refl
457*)
458
459lemma labelled_not_skip : ∀s,u.
460  s ≠ Sskip →
461  (\fst (label_statement s u)) ≠ Sskip.
462* #u
463[ * #H cases (H (refl ??))
464| *: #a try #b try #c try #d try #e
465     (* Use the state-monad-like structure of the labelling function to break
466        it up *)
467     whd in match (label_statement ??);
468     repeat @(breakup_pair ???? (λx.\fst x ≠ Sskip))
469     % #E destruct
470] qed.
471
472lemma labelled_is_not_skip : ∀s,u.
473  s ≠ Sskip →
474  ∃pf. is_Sskip (\fst (label_statement s u)) = inr … pf.
475#s #u #NE
476cases (is_Sskip ?)
477[ #E @⊥ @(absurd ? E) @labelled_not_skip //
478| /2/
479] qed.
480
481(* TODO: this is from CexecComplete, but should live somewhere else *)
482lemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inl ?? p')) → Q f.
483#P #f #p #Q #H cases f;
484[ @H
485| #np cut False [ @(absurd ? p np) | * ]
486] qed.
487
488lemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Type[0]. (∀p'.Q (inr ?? p')) → Q f.
489#P #f #p #Q #H cases f;
490[ #np cut False [ @(absurd ? np p) | * ]
491| @H
492] qed.
493
494lemma label_select_ls : ∀sz,i,ls,u.
495  ∃u'.
496    select_switch sz i (\fst (label_lstatements ls u)) =
497    \fst (label_lstatements (select_switch sz i ls) u').
498#sz #i #ls @(labeled_statements_ind … ls)
499[ #s #u % [2: whd in match (label_lstatements ??);
500  @label_gen_elim #u1 >shift_fst @refl | skip ]
501| #sz' #i' #s #tl #IH #u
502  whd in match (label_lstatements ??);
503  whd in match (select_switch ?? (LScase ????));
504  @intsize_eq_elim_elim
505  [ #NE
506    @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
507    cases (IH u2)
508    #u4 #E %{u4} whd in ⊢ (??%?);
509    >intsize_eq_elim_false //
510  | #E <E in i' ⊢ %; #i' whd
511    @eq_bv_elim
512    [ #Ei >Ei
513      %{u}
514      whd in match (label_lstatements (if ? then ? else ?) ?);
515      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
516      whd in ⊢ (??%?);
517      >intsize_eq_elim_true
518      >eq_bv_true
519      @refl
520    | #NEi
521      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
522       whd in ⊢ (??(λ_.??%?));
523       >intsize_eq_elim_true
524       >eq_bv_false //
525    ]
526  ]
527] qed.
528
529lemma blindly_label : ∀u,s. ∀P:statement → Prop.
530match s with
531[ Sskip ⇒ P Sskip
532| Sassign e1 e2 ⇒ ∀u1,u2. P (Sassign (\fst (label_expr e1 u1)) (\fst (label_expr e2 u2)))
533| Scall eo e args ⇒ ∀u1,u2,u3. P (Scall (\fst (label_opt_expr eo u1)) (\fst (label_expr e u2)) (\fst (label_exprs args u3)))
534| Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
535| Sifthenelse e s1 s2 ⇒ ∀u1,u2,u3,c2,c3. P (Sifthenelse (\fst (label_expr e u1)) (Scost c2 (\fst (label_statement s1 u2))) (Scost c3 (\fst (label_statement s2 u3))))
536| Swhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
537| Sdowhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Sdowhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
538| Sfor s1 e s2 s3 ⇒ ∀u1,u2,u3,u4,c3,c4. P (Ssequence (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Scost c3 (\fst (label_statement s3 u4)))) (Scost c4 Sskip))
539| Sbreak ⇒ P Sbreak
540| Scontinue ⇒ P Scontinue
541| Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1)))
542| Sswitch e ls ⇒ ∀u1,u2. P (Sswitch (\fst (label_expr e u1)) (\fst (label_lstatements ls u2)))
543| Slabel l s1 ⇒ ∀u1,cs. P (Slabel l (Scost cs (\fst (label_statement s1 u1))))
544| Sgoto l ⇒ P (Sgoto l)
545| Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1)))
546] → P (\fst (label_statement s u)). 
547#u * // #A #B #C try #D try #E try #F whd in match (label_statement ??);
548@label_gen_elim #u1 //
549@label_gen_elim #u2 //
550[ 6: >shift_fst //
551| *: @label_gen_elim #u3 //
552     @label_gen_elim #u4
553     [ @label_gen_elim #u5 >shift_fst >shift_fst //
554     | 2,3: >shift_fst >shift_fst //
555     | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
556     ]
557] qed.
558
559lemma label_fn_params : ∀f.
560  fn_params (label_function f) = fn_params f.
561* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
562qed.
563
564lemma label_fn_vars : ∀f.
565  fn_vars (label_function f) = fn_vars f.
566* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
567qed.
568
569(* Apply induction hypothesis while getting Matita to infer the continuations
570   k0 and k0', and the universe u0. *)
571lemma lfl_IH : ∀s0,lbl.
572  ∀C:option (statement×cont) → option (statement×cont) → Prop.
573  ∀IH:cont → cont → universe CostTag → Prop.
574  (∀k,k',u. cont_with_labels k k' → IH k k' u) →
575  ∀k0,k0',u0. cont_with_labels k0 k0' →
576   (IH k0 k0' u0 →
577    C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0')) →
578   C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0').
579/3/
580qed.
581
582lemma label_find_label : ∀lbl,s,k,k',u.
583  cont_with_labels k k' →
584  match find_label lbl s k with
585  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
586    ∃u',cs,k1'.
587    find_label lbl (\fst (label_statement s u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
588    cont_with_labels k1 k1'
589  | None ⇒ find_label lbl (\fst (label_statement s u)) k' = None ?
590  ].
591#lbl #s @(statement_ind2 ? (λls.
592  ∀k,k',u.
593  cont_with_labels k k' →
594  match find_label_ls lbl ls k with
595  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
596    ∃u',cs,k1'.
597    find_label_ls lbl (\fst (label_lstatements ls u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
598    cont_with_labels k1 k1'
599  | None ⇒ find_label_ls lbl (\fst (label_lstatements ls u)) k' = None ?
600  ])
601 … s)
602[ #k #k' #u #F @refl
603| #e1 #e2 #k #k' #u #K @blindly_label #u1 #u2 whd @refl
604| #e0 #e #args #k #k' #u #K @blindly_label #u1 #u2 #u3 whd @refl
605| #sA #sB #IH1 #IH2 #k #k' #u #K @blindly_label #u1 #u2 whd in match (find_label ???);
606  whd in match (find_label ?? k');
607  @(lfl_IH sA … IH1) [ /2/ ]
608  cases (find_label ???)
609  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
610    @(lfl_IH … IH2) [ // ]
611    cases (find_label ???)
612    [ whd in ⊢ (% → %); #FIND2' whd in ⊢ (??%?); >FIND1' >FIND2' @refl
613    | * #s3 #k3 whd in ⊢ (% → %); * #u3 * #cs * #k1' * #FIND2' #K1'
614      % [2: %{cs} %{k1'} % // whd in ⊢ (??%?); >FIND1' in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl | skip ]
615    ]
616  | * #sA' #kA' whd in ⊢ (% → %);
617    * #u1' * #cs * #k1' * #FA' #K'
618         % [2: %{cs} %{k1'} % [ whd in ⊢ (??%?); >FA' in ⊢ (??%?); @refl | // ] |skip]
619  ]
620| #e #s1 #s2 #IH1 #IH2 #k #k' #u @blindly_label #u1 #u2 #u3 #c2 #c3 #K
621  whd in match (find_label ?? k); whd in match (find_label ?? k');
622  whd in match (find_label ?? k');
623  @(lfl_IH  … IH1) [ // ] cases (find_label ???)
624  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
625    lapply (IH2 k k' u3 K) cases (find_label ???)
626    [ whd in ⊢ (% → %); #FIND2'
627      whd in match (find_label ???); >FIND1'
628      whd in match (find_label ???); >FIND2' @refl
629    | * #s2' #k2' * #u4 * #cs * #k1' * #FIND2' #K2'
630      % [2: % [2: % [2: % [ whd in ⊢ (??%?);
631      whd in match (find_label ???); >FIND1' in ⊢ (??%?);
632      whd in match (find_label ???); >FIND2' in ⊢ (??%?); @refl
633      | // ]|skip]|skip]|skip]
634    ]
635  | * #s1' #k1 whd in ⊢ (% → %); * #u4 * #cs * #k1' * #FIND1' #K1'
636    % [2: % [2: % [2: % [
637      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
638      @refl | // ] |skip ]| skip ]| skip ]
639  ]
640| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
641  whd in match (find_label ?? k); normalize in match (find_label ?? k');
642  @(lfl_IH s0 … IH) [ /2/ ]
643  cases (find_label ???)
644  [ whd in ⊢ (% → %); #FIND1'
645    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
646  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
647    % [2: % [2: % [2: % [
648      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
649      @refl | // ]| skip ]| skip ]| skip ]
650  ]
651| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
652  whd in match (find_label ?? k); normalize in match (find_label ?? k');
653  @(lfl_IH s0 … IH) [ /2/ ]
654  cases (find_label ???)
655  [ whd in ⊢ (% → %); #FIND1'
656    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
657  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
658    % [2: % [2: % [2: % [
659      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
660      @refl | // ]| skip ]| skip ]| skip ]
661  ]
662| #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4
663  whd in match (find_label ???); normalize in match (find_label ?? k');
664  @(lfl_IH s1 … IH1) [ /2/ ]
665  cases (find_label ???)
666  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' >FIND1'
667    @(lfl_IH s3 … IH3) [ /2/ ]
668    cases (find_label ???)
669    [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND3' >FIND3'
670      @(lfl_IH s2 … IH2) [ /2/ ]
671      cases (find_label ???)
672      [ whd in ⊢ (% → %); #FIND2' >FIND2' @refl
673      | * #s2' #k2' * #u2' * #cs' * #k1' * #FIND2' #K2'
674        % [2: % [2: % [2: % [
675         whd in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl
676        | // ]| skip ]| skip ]| skip ]
677      ]
678    | * #s3' #k3' * #u3' * #cs' * #k1' * #FIND3' #K3'
679        % [2: % [2: % [2: % [
680        >FIND3' in ⊢ (??%?); whd in ⊢ (??%?); @refl
681        | // ]| skip ]| skip ]| skip ]
682    ]
683  | * #s1' #k1' * #u1' * #cs' * #k1' * #FIND1' #K1'
684        % [2: % [2: % [2: % [
685        >FIND1' in ⊢ (??%?); whd in ⊢ (??%?); @refl
686        | // ]| skip ]| skip ]| skip ]
687  ]
688| //
689| //
690| #eo #k #k' #u @blindly_label #u1 //
691| #e #ls #IH #k #k' #u #K @blindly_label #u1 #u2
692  normalize in match (find_label ???); normalize in match (find_label ???);
693  lapply (IH (Kswitch k) (Kswitch k') u2 ?) [/2/] cases (find_label_ls ???)
694  [ whd in ⊢ (% → %); //
695  | * #s1' #k1' * #u' * #cs * #k'' * #FIND' #K'
696    % [2: % [2: % [2: % [ @FIND' | // ]|skip ]|skip]|skip]
697  ]
698| #l #s0 #IH #k #k' #u #K @blindly_label #u1 #cs
699  whd in match (find_label ???); whd in match (find_label ?? k');
700  cases (ident_eq lbl l)
701  [ #E destruct whd
702    % [2: % [2: % [2: % [ @refl | // ]|skip ]|skip ]| skip ]
703  | #NE whd in ⊢ (match % with [_⇒?|_⇒?]);
704    normalize in match (find_label ?? k');
705    @(lfl_IH s0 … IH) [ // ]
706    cases (find_label ???)
707    [ //
708    | * #s0' #k0' * #u' * #cs0 * #k1' * #FIND0 #K0
709      % [2: % [2: % [2: % [ @FIND0 | // ]|skip ]|skip]|skip]
710    ]
711  ]
712| //
713| #l #s0 #IH #k #k' #u #K @blindly_label #u1 /2/
714| #s0 #IH #k #k' #u whd in match (label_lstatements ??);
715  @label_gen_elim #u1 >shift_fst >shift_fst
716  whd in match (find_label_ls ???); whd in match (find_label_ls ???);
717  @IH
718| #sz #i #s0 #tl #IH1 #IH2 #k #k' #u #K
719  whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
720  @label_gen_elim #u3 >shift_fst
721  whd in match (find_label_ls ???); normalize in match (find_label_ls ?? k');
722  @(lfl_IH s0 … IH1) [ /2/ ]
723  cases (find_label ???)
724  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND0 >FIND0
725    lapply (IH2 k k' u2 K) cases (find_label_ls ???)
726    [ whd in ⊢ (% → %); #FINDtl >FINDtl @refl
727    | * #stl #ktl //
728    ]
729  | * #s0' #k0' whd in ⊢ (% → %);
730    * #u' * #cs * #k1' * #FIND0 #K0 >FIND0
731    % [2: % [2: % [2: % [ @refl | // ] | skip ] | skip ] | skip ]
732  ]
733] qed.
734
735lemma label_find_label_fn : ∀lbl,f,k,k',s1,k1.
736  cont_with_labels k k' →
737  find_label lbl (fn_body f) (call_cont k) = Some ? 〈s1,k1〉 →
738  ∃u',cs,k1'.
739    find_label lbl (fn_body (label_function f)) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
740    cont_with_labels k1 k1'.
741#lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND
742whd in match (label_function ?);
743@label_gen_elim #u1 @label_gen_elim #u2 >shift_fst
744lapply (label_find_label lbl s (call_cont k) (call_cont k') (new_universe ?) ?)
745[ /2/ ]
746>FIND //
747qed.
748
749(* We show the main simulation in two stages.  First, we show it for all states
750   in the relation *except* those for labeled_statements, then we'll show the
751   whole thing.  This is so that we can appeal to the other cases in the proof
752   for labeled_statements. *)
753lemma step_with_labels_partial : ∀ge,ge'.
754  related_globals ge ge' →
755  ∀s1,s1',tr,s2.
756  state_with_labels_partial s1 s1' →
757  exec_step ge s1 = Value … 〈tr,s2〉 →
758   ∃tr',s2'. plus ge' s1' tr' s2' ∧
759             trace_with_extra_labels tr tr' ∧
760             state_with_labels s2 s2'.
761#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
762[ #f #us #s #k #k' #e #m #KL cases s
763  [ #EX inversion KL
764    [ #E1 #E2 #_ destruct %{tr}
765      whd in EX:(??%?);
766      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
767      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list ? m (blocks_of_env e)))}
768        % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
769        | // ] | /3/ ]
770      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
771      ]
772    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
773      %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)}
774      whd in EX:(??%%); destruct
775      % [ % [ @plus_one @refl | // ] | /3/ ]
776    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
777      whd in EX:(??%%); destruct
778      % [ 2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]
779    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
780      cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem
781      cases (bindIO_inversion ??????? EXrem) * * #EXb #EXbrem -EXrem
782      normalize in EXbrem; destruct
783      cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te
784      [ % [ 2: % [ 2: % [ % [ @plus_one
785        whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
786        whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
787        whd in ⊢ (??%?); @refl
788        | // ]
789        | @swl_partial @swl_dowhilestate // ] | skip ] | skip ]
790      | % [ 2: % [ 2: % [ % [ @plus_succ [
791        4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
792           whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
793           whd in ⊢ (??%?); @refl
794        | skip | skip
795        | 5: @plus_succ [ 4: @refl | skip | skip
796        | 5: @plus_one @refl | skip ] | skip ]
797        | <(E0_right tr) @twel_app /2/ ]
798        | /3/ ] | skip ] | skip ]
799      ]
800    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
801      whd in EX:(??%?); destruct
802      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
803    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
804      whd in EX:(??%?); destruct
805      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
806    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
807      whd in EX:(??%?); destruct
808      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
809    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
810      whd in EX:(??%?); destruct
811      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
812    | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
813      whd in EX:(??%?);
814      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
815      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
816        %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
817        @refl | // ] | /4/ ] | skip ]
818      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
819      ]
820    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
821      % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ]| skip ]| skip ]
822    ]
823  | * #a1 #ty1 #a2 #EX
824    cases (bindIO_inversion ??????? EX) -EX * * #b1 #o1 #tr1 * #EX1 #EX
825    cases (bindIO_inversion ??????? EX) -EX * #v2 #tr2 * #EX2 #EX
826    cases (bindIO_inversion ??????? EX) -EX #m3 * #EX3 #EX
827    whd in EX:(??%%); destruct
828    cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 us) #tr1' * #EX1' #T1
829    whd in match (label_statement ??);
830    @label_gen_elim #ua1 @label_gen_elim #ua2
831    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2
832    % [2: % [2: % [ % [
833      @plus_one whd in ⊢ (??%?);     
834      >exec_lvalue_labelled >EX1' in ⊢ (??%?);
835      whd in ⊢ (??%?); >EX2' in ⊢ (??%?);
836      whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?);
837      @refl
838    | @twel_app // ] | /3/ ] | skip ] | skip ]
839  | * [2: * #er #tyr ] #ef #args #EX
840    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
841    cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX
842    cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX
843    cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX
844    whd in EX:(??%%);
845    [ cases (bindIO_inversion ??????? EX) -EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ]
846    destruct
847    whd in match (label_statement ??);
848    whd in match (label_opt_expr ??);
849    [ @(label_gen_elim … (Expr er tyr)) #u' @breakup_pair | letin u' ≝ us ]
850    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u') #tr1' * #EX1' #T1
851    @label_gen_elim #u1
852    @label_gen_elim #u2
853    cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u1) #tr2' * #EX2' #T2
854    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ]
855    % [2,4: % [2,4: % [1,3: % [1,3:
856      @plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
857      whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ]
858      whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?);
859      whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ]
860      whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ]
861      @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ]
862  | #st1 #st2 #EX
863    whd in EX:(??%%); destruct
864    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
865    %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
866  | #a #st1 #st2 #EX
867    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
868    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
869    normalize in EX; destruct
870    whd in match (label_statement ??); @label_gen_elim #u1
871    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
872    @label_gen_elim #u5
873    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
874    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
875    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
876    % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9:
877      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
878      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
879      whd in ⊢ (??%?); @refl
880    | 1,2,6,7: skip
881    | 5,10: @plus_one @refl
882    | *: skip
883    ]
884    | 2,4: <(E0_right tr) @twel_app /2/
885    ]| 2,4: /3/ ] | *: skip ] | *: skip ]
886  | #a #st #EX
887    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
888    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
889    normalize in EX; destruct
890    whd in match (label_statement ??); @label_gen_elim #u1
891    @label_gen_elim #u2
892    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
893    >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7
894    >shift_fst
895    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
896    % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
897      | 5,10: @plus_succ [ 4,9:
898      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
899      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
900      whd in ⊢ (??%?); @refl
901    | 1,2,6,7: skip
902    | 5: @plus_one @refl
903    | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
904    | *: skip
905    ]
906    | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
907    ]| 2,4: /4/ ] | *: skip ] | *: skip ]
908  | #a #st #EX
909    normalize in EX; destruct
910    whd in match (label_statement ??); @label_gen_elim #u1
911    @label_gen_elim #u2
912    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
913    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
914    % [2: % [2: % [ % [ @plus_succ [ 4: @refl | 1,2: skip
915      | 5: @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ]
916      | /2/ ] | /4/ ] | skip ] | skip ]
917  | #st1 #a #st2 #st #EX
918    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
919    whd in EX:(??%?); >Eskip in EX; #EX
920    whd in match (label_statement ??); @label_gen_elim #u1
921    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
922    whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst
923    whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst
924    [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
925      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
926      normalize in EX; destruct
927      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
928      % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
929      | 5,10: @plus_succ [ 4,9:
930      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
931      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
932      whd in ⊢ (??%?); @refl
933      | 1,2,6,7: skip
934      | 5: @plus_one @refl
935      | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
936      | *: skip
937      ]
938      | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
939      ]| 2,4: /4/ ] | *: skip ] | *: skip ]
940    | whd in EX:(??%%); destruct
941      % [2: % [2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one
942        whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
943        >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ]
944      | skip ] | skip ]
945    ]
946  | #EX inversion KL
947    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
948    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
949    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
950    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
951    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
952    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
953    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
954    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
955    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
956    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
957    ]
958    whd in match (label_statement ??);
959    % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: %
960    [1,11,13: @plus_one @refl | 2,12,14: //
961    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
962    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
963    | @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/
964    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
965    ]| *: /3/ ]|*: skip]|*: skip ]
966  | #EX inversion KL
967    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
968    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
969    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
970    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
971    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
972    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
973    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
974    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
975    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
976    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
977    ]
978    whd in match (label_statement ??);
979    [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: %
980      [1,3,7,9,11: @plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ]
981      | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
982    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
983      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
984      normalize in EX; destruct
985      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
986      % [2,4: % [2,4: % [1,3: % [1,3: [ @plus_one | @plus_succ ] [ 1,5:
987        whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
988      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ]
989      whd in ⊢ (??%?); @refl
990      | 6: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
991      | // | <(E0_right tr) @twel_app /2/
992      ]
993      | /3/ | /3/ ] | *: skip ] | *: skip ]
994    ]
995  | * [2: #a ] #EX
996    whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX;
997    #Ety #EX whd in EX:(??%?);
998    [ destruct
999    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
1000      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
1001    | >Ety in EX; #EX
1002    | @⊥ cases (fn_return f) in Ety EX;
1003      [ * #H cases (H (refl ??))
1004      | *: normalize #a #b #c try #d try #e destruct
1005      ]
1006    ]
1007    whd in match (label_statement ??);
1008    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
1009    whd in EX:(??%%); destruct
1010    % [2,4: % [2,4: % [1,3: %[1,3: @plus_one
1011      whd in ⊢ (??%?);
1012      [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
1013        whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
1014      | >label_function_return >Ety in ⊢ (??%?);
1015      ] whd in ⊢ (??%?); @refl
1016      | *: // ]| *: @swl_partial @swl_returnstate /2/ ]|*:skip]|*:skip]
1017  | #a #ls #EX
1018    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
1019    cases v1 in EX1 EX;
1020    [ 2: #sz #i #EX1 #EX
1021    | *: normalize #A #B try #C destruct
1022    ]
1023    whd in EX:(??%%); destruct
1024    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
1025    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
1026    % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
1027      | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
1028      ]|skip ]| skip ]
1029  | #l #st #EX
1030    whd in EX:(??%?); destruct
1031    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
1032    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
1033    %[2: %[2: %[ %[ @plus_succ
1034      [ 4: @refl | 5: @plus_one @refl | *: skip ]
1035      | /2/ ] | /3/ ] |skip ]| skip ]
1036  | #l #EX
1037    whd in EX:(??%?);
1038    @blindly_label whd
1039    lapply (refl ? (find_label l (fn_body f) (call_cont k)))
1040    cases (find_label ???) in ⊢ (???% → ?);
1041    [ #F @⊥  >F in EX; #EX whd in EX:(??%?); destruct
1042    | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct
1043      cases (label_find_label_fn … KL F)
1044      #u' * #cs * #k1' * #F' #K'
1045      % [2: %[2: %[ %[ @plus_succ
1046        [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ]
1047        | /2/ ] | /3/ ] | skip ] | skip ]
1048    ]
1049  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
1050    % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]| skip ]
1051  ]
1052| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
1053  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
1054  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
1055  whd in EX:(??%%); destruct
1056  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
1057  [ % [2: % [2: % [ % [
1058    @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
1059                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
1060               |5: @plus_one @refl | *: skip ]
1061    | <(E0_right tr) /3/ ]| /4/ ]| skip ]| skip ]
1062  | % [2: % [2: % [ % [
1063    @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
1064                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
1065    | 5: @plus_succ [4: @refl
1066    | 5: @plus_one @refl | *: skip ] | *: skip ]
1067    | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
1068  ]
1069| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
1070  whd in EX:(??%%); destruct
1071  % [2: % [2: % [ % [
1072    @plus_succ [4: % | 5: @plus_one % | *: skip ]
1073    | /2/ ]| /4/ ]| skip ]| skip ]
1074| #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
1075  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
1076  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
1077  whd in EX:(??%%); destruct
1078  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
1079  [ % [2: % [2: % [ % [
1080    @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
1081                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
1082    | 5: whd in ⊢ (??(??%%??)??); @plus_one @refl
1083    | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ]
1084  | % [2: % [2: % [ % [
1085    @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
1086                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
1087    | 5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl
1088    | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
1089    ]
1090  ]
1091| *
1092  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
1093    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
1094    whd in EX:(??%%); destruct
1095    whd in match (label_fundef ?);
1096    whd in match (label_function ?);
1097    lapply (refl ? (label_function f)) whd in ⊢ (???% → ?);
1098    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
1099    % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
1100      whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl
1101    | 5: @plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
1102  | #id #tys #ty #args #k #k' #m #K #EX
1103    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
1104    cases (bindIO_inversion ??????? EX) -EX #ety * #EX2 #EX
1105    whd in EX2:(??%%); destruct
1106  ]
1107| #res #k #k' #m #K #EX inversion K
1108  [ #E1 #E2 #E3 destruct cases res in EX ⊢ %;
1109    [ 2: * #i #EX whd in EX:(??%?); destruct
1110    | *: normalize #A try #B try #C destruct
1111    ]
1112    % [2: % [2: % [ % [ @plus_one @refl | // ]| /2/ ]| skip ]| skip ]
1113  | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
1114    [ #EX whd in EX:(??%?); destruct
1115      % [2: % [2: % [ % [ @plus_one @refl | // ]| /3/ ]| skip ]| skip ]
1116    | * * #b #o #ty #EX
1117      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
1118      whd in EX:(??%%); destruct
1119      % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
1120    ]
1121  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
1122       destruct whd in EX:(??%?); destruct
1123  ]
1124| #r #EX whd in EX:(??%%); destruct
1125] qed.
1126
1127lemma step_with_labels : ∀ge,ge'.
1128  related_globals ge ge' →
1129  ∀s1,s1',tr,s2.
1130  state_with_labels s1 s1' →
1131  (exec_step ge s1 = Value … 〈tr,s2〉 →
1132   ∃tr',s2'. plus ge' s1' tr' s2' ∧
1133             trace_with_extra_labels tr tr' ∧
1134             state_with_labels s2 s2').
1135#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
1136[ #s1 #s1' @step_with_labels_partial //
1137| #f #u *
1138(* If we have LSdefault we need to smuggle the execution of the cost label in
1139   before the actual statement. *)
1140  [ #s #k #k' #e #m #K #EX
1141    whd in EX:(??(??(??%???))?);
1142    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
1143    >shift_fst whd in match (seq_of_labeled_statement ?);
1144    cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
1145    #tr' * #s2' * * #P #T #S
1146    % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
1147(* but for LScase it's just like the cases in step_with_labels_partial *)
1148  | #sz #i #s #ls #k #k' #e #m #K #EX
1149    whd in EX:(??(??(??%???))?);
1150    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
1151    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
1152    whd in EX:(??%?); destruct
1153    % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
1154  ]   
1155] qed.
1156
1157
1158   
1159
1160
Note: See TracBrowser for help on using the repository browser.