source: src/Clight/labelSimulation.ma @ 2107

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

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