Changeset 1920 for src/Clight/labelSimulation.ma
 Timestamp:
 May 8, 2012, 11:16:18 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r1893 r1920 5 5 (* for the induction principle *) 6 6 include "Clight/CexecSound.ma". 7 8 (* TODO: make something general that can live in common/Globalenvs.ma. *) 9 record 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 }. 7 16 8 17 lemma commute_fst_pair : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → B → C×D. … … 16 25 qed. 17 26 18 lemma label_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0]. 19 (∀u'. P (F (\fst (label_expr e u)) u')) → 20 P (let 〈e',u'〉 ≝ label_expr e u in F e' u'). 21 #e #u #T #F #P 22 cases (label_expr e u) 23 #e' #u' #H @H 27 (* lemma to break up label_expr, label_exprs and label_statement in the labelling 28 functions *) 29 lemma 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 33 cases (L syn u) 34 #syn' #u' #H @H 24 35 qed. 25 36 … … 54 65 qed. 55 66 56 lemma label_expr_ok : ∀ge,en,m,e,v,tr. 57 exec_expr ge en m e = OK … 〈v,tr〉 → 58 ∀u. ∃tr'. exec_expr ge en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧ 59 trace_with_extra_labels tr tr'. 60 #ge #en #m #e 61 @(expr_lvalue_ind ? 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') … e) 67 definition expr_lvalue_ind_combined ≝ 68 λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx. 69 conj ?? 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 73 lemma 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 65 83 [ 1,2: normalize /3 by ex_intro, conj/ 66 84  * // 67 [ normalize /3 by ex_intro, conj/ 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  // ] 68 91  #e1 #ty #IH #v #tr #EX #u 69 92 cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r … … 81 104 whd in ⊢ (??%?); >EXl @refl 82 105 ] 83  #v #ty #b #o #tr #EX #u %{tr} % /2/ 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  // ] 84 111  #e1 #ty #IH #b #o #tr #EX #u 85 112 cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem … … 106 133 %{tr1'} % // >shift_fst 107 134 whd in ⊢ (??(????(?(???%)?))?); 108 @label_ expr_elim #u2135 @label_gen_elim #u2 109 136 whd in ⊢ (??%?); >EX1' 110 137 whd in ⊢ (??%?); >label_expr_type >EX2 @refl … … 117 144 >shift_fst 118 145 whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); 119 @label_ expr_elim #u2146 @label_gen_elim #u2 120 147 cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2 121 @label_ expr_elim #u3 %{(tr1'⧺tr2')}148 @label_gen_elim #u3 %{(tr1'⧺tr2')} 122 149 whd in ⊢ (?(??%?)?); >EX1' 123 150 whd in ⊢ (?(??%?)?); >EX2' … … 139 166 cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 140 167 >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); 141 @label_ expr_elim #u2142 @label_ expr_elim #u3168 @label_gen_elim #u2 169 @label_gen_elim #u3 143 170 @add_cost_expr_elim #u4 #l4 144 @label_ expr_elim #u5171 @label_gen_elim #u5 145 172 @add_cost_expr_elim #u6 #l6 146 173 [ cases (IH2 … EX2 u2)  cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx … … 154 181 cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem 155 182 >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); 156 @label_ expr_elim #u2157 @label_ expr_elim #u3183 @label_gen_elim #u2 184 @label_gen_elim #u3 158 185 @add_cost_expr_elim #u4 #l4 159 186 @add_cost_expr_elim #u5 #l5 … … 180 207 cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem 181 208 >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?)); 182 @label_ expr_elim #u2209 @label_gen_elim #u2 183 210 @add_cost_expr_elim #u4 #l4 184 @label_ expr_elim #u3211 @label_gen_elim #u3 185 212 @add_cost_expr_elim #u5 #l5 186 213 [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1 … … 231 258 ] qed. 232 259 260 lemma 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 233 280 (* Plan: 234 281  extend labelling functions to continuations and hence states 235 282 NO  this doesn't work because we don't know *which* cost labels to add 236 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 237 286  build a simulation relation linking states to their labelled counterparts 238 287  write a predicate stating that two traces are the same except for some … … 246 295 cost_related s2 s2' 247 296 using some relationship between ge and ge'. 248 249 WAIT  do I really want functions to erase the labels? Or a predicate? 250 251 let rec erase_label_expr (e:expr) : expr ≝ 252 match e with 253 [ Expr ed ty ⇒ Expr (erase_label_expr_descr ed) ty 297 *) 298 299 inductive 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 318 lemma 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/ 322 qed. 323 324 inductive 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 343 inductive 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 347 definition eplus ≝ λn. repeat n io_out io_in clight_fullexec. 348 349 inductive 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 360 lemma label_function_return : ∀f. 361 fn_return (label_function f) = fn_return f. 362 * #rty #params #vars #body 363 whd in ⊢ (??(?%)?); 364 cases (label_statement ??) #body' #u' 365 whd in ⊢ (??(?%)?); 366 cases (add_cost_before ??) #body'' #u'' 367 // 368 qed. 369 370 lemma 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 380 lemma 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 254 386 ] 255 and erase_label_expr_descr (e:expr_descr) : expr_descr ≝ 256 match e with 257 [ Ederef e' ⇒ Ederef (erase_label_expr_descr e') 258  Eaddrof e' ⇒ Eaddrof (erase_label_expr_descr e') 259  Eunop op e' 387 qed. 388 389 coercion 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 393 lemma 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 397 whd in ⊢ (??(????(???%))?); >shift_fst @refl 398 qed. 399 400 lemma 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 403 qed. 404 405 lemma label_fundef_typeof_fundef : ∀fd. 406 type_of_fundef (label_fundef fd) = type_of_fundef fd. 407 * // 408 * #rty #args #vars #body 409 normalize cases (label_statement ??) #body' #u 410 normalize cases (fresh ??) // 411 qed. 412 413 lemma 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 418 lapply (rg_find_funct … RG … vf fd) 419 cases (find_funct … vf) 420 [ #_ #E normalize in E; destruct 421  #fd' #H #E normalize in E; destruct >(H (refl ??)) // 422 ] qed. 423 424 (* 425 lemma 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 437 lemma 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 260 451 *) 452 453 lemma 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 statemonadlike 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 466 lemma labelled_is_not_skip : ∀s,u. 467 s ≠ Sskip → 468 ∃pf. is_Sskip (\fst (label_statement s u)) = inr … pf. 469 #s #u #NE 470 cases (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 *) 476 lemma 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 482 lemma 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 488 lemma 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 523 lemma blindly_label : ∀u,s. ∀P:statement → Prop. 524 match 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. *) 555 lemma 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/ 564 qed. 565 566 lemma 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 719 lemma 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 726 whd in match (label_function ?); 727 @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst 728 lapply (label_find_label lbl s (call_cont k) (call_cont k') (new_universe ?) ?) 729 [ /2/ ] 730 >FIND // 731 qed. 732 733 lemma 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 TracChangeset
for help on using the changeset viewer.