source: src/Clight/labelSimulation.ma @ 1930

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

Tidy up labelling simulation stuff a bit.

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