source: src/Clight/labelSimulation.ma @ 1920

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

Most of the labelling simulation. Still need to sort out switch statements
and function calls.

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