Changeset 3396 for LTS/Language.ma
 Timestamp:
 Nov 15, 2013, 2:51:50 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Language.ma
r3394 r3396 17 17 include "basics/lists/list.ma". 18 18 include "../src/utilities/option.ma". 19 include "basics/jmeq.ma". 19 20 20 21 record instr_params : Type[1] ≝ … … 84 85 lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → 85 86 (i1 ≠ i2 → P false) → P (eq_instructions p i1 i2). 87 #P #p #i1 elim i1 88 [ * normalize [/2/ ] #x [*: #y #z [2,3: #w1 #w2 [#w3] 4,5: #w1]] #_ #H2 @H2 % #EQ 89 (* destruct(EQ) gives no choice for ID(instructions_discr) *) cases daemon ] 86 90 cases daemon (*TODO*) 87 91 qed. … … 175 179 store ? st' = mem → code … st' = f_body … env_it → 176 180 cont … st' = 177 〈(ret_act (match r_lb with [Some lb ⇒ Some ? (inl ?? lb) 178  None ⇒ None ?])),cd〉 :: (cont … st) → 181 〈(ret_act r_lb),cd〉 :: (cont … st) → 179 182 io_info … st = false → (io_info … st') = false → 180 execute_l … (call_act f ( inl ?? (f_lab ?? env_it))) st st'183 execute_l … (call_act f (f_lab ?? env_it)) st st' 181 184  ret_instr : ∀st,st',r_t,mem,tl',rb,cd.code ? st = RETURN … r_t → 182 185 cont … st = 〈ret_act rb,cd〉 :: tl' → cont ? st' = tl' → … … 354 357 λx.〈a_return_cost_label x,S x〉. 355 358 359 record call_post_info (p : instr_params) : Type[0] ≝ 360 { gen_labels : list CostLabel 361 ; t_code : Instructions p 362 ; fresh : ℕ 363 ; lab_map : associative_list DEQCostLabel CostLabel 364 ; lab_to_keep : list CostLabel 365 }. 366 356 367 let rec call_post_trans (p : instr_params) (i : Instructions p) (n : ℕ) on i : 357 ((list CostLabel) × (Instructions p)) × (ℕ × (associative_list DEQCostLabel CostLabel)) ≝ 368 list CostLabel → call_post_info p ≝ 369 λabs. 358 370 match i with 359 [ EMPTY ⇒ 〈nil ?,EMPTY p,n,nil ?〉360  RETURN x ⇒ 〈nil ?,RETURN … x,n,nil ?〉371 [ EMPTY ⇒ mk_call_post_info ? abs (EMPTY …) n (nil ?) (nil ?) 372  RETURN x ⇒ mk_call_post_info ? abs (RETURN … x) n (nil ?) (nil ?) 361 373  SEQ x lab instr ⇒ 362 let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … instr nin374 let ih ≝ call_post_trans … instr n abs in 363 375 match lab with 364 [ None ⇒ 〈l1,SEQ … x (None ?) instr1,n1,m1〉 365  Some lbl ⇒ 〈nil CostLabel,SEQ … x (Some ? lbl) instr1, n1, update_list ?? m1 lbl (lbl :: l1) 〉 376 [ None ⇒ mk_call_post_info ? (gen_labels … ih) (SEQ … x (None ?) (t_code … ih)) 377 (fresh … ih) (lab_map … ih) (lab_to_keep … ih) 378  Some lbl ⇒ 379 mk_call_post_info ? (nil ?) (SEQ … x (Some ? lbl) (t_code … ih)) (fresh … ih) 380 (〈a_non_functional_label lbl,(a_non_functional_label lbl :: (gen_labels … ih))〉 :: (lab_map … ih)) 381 (lab_to_keep … ih) 366 382 ] 367 383  COND x ltrue i1 lfalse i2 i3 ⇒ 368 let 〈l3,instr3,n3,m3〉 ≝ call_post_trans … i3 n in 369 let 〈l2,instr2,n2,m2〉 ≝ call_post_trans … i2 n3 in 370 let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 n2 in 371 〈nil ?,COND … x ltrue instr1 lfalse instr2 instr3,n1, 372 update_list DEQCostLabel CostLabel 373 (update_list DEQCostLabel CostLabel (m1 @ m2 @ m3) ltrue (ltrue :: (l1 @ l3))) 374 lfalse (lfalse :: (l2 @ l3))〉 384 let ih3 ≝ call_post_trans … i3 n abs in 385 let ih2 ≝ call_post_trans … i2 (fresh … ih3) (gen_labels … ih3) in 386 let ih1 ≝ call_post_trans … i1 (fresh … ih2) (gen_labels … ih3) in 387 mk_call_post_info ? (nil ?) (COND … x ltrue (t_code … ih1) lfalse (t_code … ih2) (t_code … ih3)) 388 (fresh … ih1) 389 (〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉:: 390 〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉:: 391 ((lab_map … ih1) @ (lab_map … ih2) @ (lab_map … ih3))) 392 ((lab_to_keep … ih1) @ (lab_to_keep … ih2) @ (lab_to_keep … ih3)) 375 393  LOOP x ltrue i1 lfalse i2 ⇒ 376 let 〈l2,instr2,n2,m2〉 ≝ call_post_trans … i2 n in 377 let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 n2 in 378 〈nil ?,LOOP … x ltrue instr1 lfalse instr2,n1, 379 update_list DEQCostLabel CostLabel 380 (update_list DEQCostLabel CostLabel (m1 @ m2) ltrue (ltrue :: l1)) 381 lfalse (lfalse :: l2)〉 394 let ih2 ≝ call_post_trans … i2 n abs in 395 let ih1 ≝ call_post_trans … i1 (fresh … ih2) (nil ?) in 396 mk_call_post_info ? (nil ?) (LOOP … x ltrue (t_code … ih1) lfalse (t_code … ih2)) (fresh … ih1) 397 (〈a_non_functional_label lfalse,(a_non_functional_label lfalse :: (gen_labels … ih2))〉 :: 398 〈a_non_functional_label ltrue,(a_non_functional_label ltrue :: (gen_labels … ih1))〉 :: 399 ((lab_map … ih1) @ (lab_map … ih2))) 400 ((lab_to_keep … ih1) @ (lab_to_keep … ih2)) 382 401  CALL f act_p r_lb i1 ⇒ 383 let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 nin402 let ih ≝ call_post_trans … i1 n abs in 384 403 match r_lb with 385 [ None ⇒ let 〈l',f''〉 ≝ fresh_rc_label n1 in 386 〈(a_return_post l')::l1,CALL … f act_p (Some ? l') instr1,f'',m1〉 387  Some lbl ⇒ 〈nil ?,CALL ? f act_p (Some ? lbl) instr1,n1,update_list ?? m1 lbl (lbl :: l1)〉 404 [ None ⇒ let 〈l',f''〉 ≝ fresh_rc_label (fresh … ih) in 405 mk_call_post_info ? ((a_return_post l')::(gen_labels … ih)) 406 (CALL … f act_p (Some ? l') (t_code … ih)) f'' (lab_map … ih) (lab_to_keep … ih) 407  Some lbl ⇒ 408 mk_call_post_info ? (nil ?) (CALL ? f act_p (Some ? lbl) (t_code … ih)) (fresh … ih) 409 (〈a_return_post lbl,(a_return_post lbl :: (gen_labels … ih))〉 :: (lab_map … ih)) 410 (a_return_post lbl :: lab_to_keep … ih) 388 411 ] 389 412  IO lin io lout i1 ⇒ 390 let 〈l1,instr1,n1,m1〉 ≝ call_post_trans … i1 n in 391 〈nil ?,IO ? lin io lout instr1,n1,update_list ?? (update_list ?? m1 lout (lout :: l1)) lin [lin]〉 392 ]. 393 413 let ih ≝ call_post_trans … i1 n abs in 414 mk_call_post_info ? (nil ?) (IO ? lin io lout (t_code … ih)) (fresh … ih) 415 (〈a_non_functional_label lout,(a_non_functional_label lout :: (gen_labels … ih))〉 :: 416 〈a_non_functional_label lin,[a_non_functional_label lin]〉 :: (lab_map … ih)) (lab_to_keep … ih) 417 ]. 418 419 420 let rec call_post_clean (p : instr_params) (i : Instructions p) on i : 421 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → 422 option ((list CostLabel) × (Instructions p)) ≝ 423 λm,keep,abs. 424 match i with 425 [ EMPTY ⇒ Some ? 〈abs,EMPTY …〉 426  RETURN x ⇒ Some ? 〈abs,RETURN … x〉 427  SEQ x lab instr ⇒ 428 ! 〈l,i1〉 ← call_post_clean … instr m keep abs; 429 match lab with 430 [ None ⇒ return 〈l,SEQ … x (None ?) i1〉 431  Some lbl ⇒ if ((get_element … m lbl) == lbl :: l) 432 then return 〈nil ?,SEQ … x (Some ? lbl) i1〉 433 else None ? 434 ] 435  COND x ltrue i1 lfalse i2 i3 ⇒ 436 ! 〈l3,instr3〉 ← call_post_clean … i3 m keep abs; 437 ! 〈l2,instr2〉 ← call_post_clean … i2 m keep l3; 438 ! 〈l1,instr1〉 ← call_post_clean … i1 m keep l3; 439 if ((get_element … m ltrue) == ltrue :: l1) ∧ 440 ((get_element … m lfalse) == lfalse :: l2) 441 then return 〈nil ?,COND … x ltrue instr1 lfalse instr2 instr3〉 442 else None ? 443  LOOP x ltrue i1 lfalse i2 ⇒ 444 ! 〈l2,instr2〉 ← call_post_clean … i2 m keep abs; 445 ! 〈l1,instr1〉 ← call_post_clean … i1 m keep (nil ?); 446 if ((get_element … m ltrue) == ltrue :: l1) ∧ 447 ((get_element … m lfalse) == lfalse :: l2) 448 then return 〈nil ?,LOOP … x ltrue instr1 lfalse instr2〉 449 else None ? 450  CALL f act_p r_lb i1 ⇒ 451 ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs; 452 match r_lb with 453 [ None ⇒ return 〈l1,CALL … f act_p (None ?) instr1〉 454  Some lbl ⇒ if ((a_return_post lbl ∈ keep)) 455 then if ((get_element … m lbl) == lbl :: l1) 456 then return 〈nil ?,CALL … f act_p (Some ? lbl) instr1〉 457 else None ? 458 else return 〈(a_return_post lbl) :: l1,CALL … f act_p (None ?) instr1〉 459 ] 460  IO lin io lout i1 ⇒ 461 ! 〈l1,instr1〉 ← call_post_clean … i1 m keep abs; 462 if ((get_element … m lout) == lout :: l1) ∧ ((get_element … m lin) == [lin]) 463 then return 〈nil ?,IO … lin io lout instr1〉 464 else None ? 465 ]. 466 467 let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (a : A) (l1 : list B) 468 (l2 : list C) (f : A → B → C → A) on l1 : option A≝ 469 match l1 with 470 [ nil ⇒ match l2 with [ nil ⇒ return a  cons y ys ⇒ None ? ] 471  cons x xs ⇒ 472 match l2 with 473 [ nil ⇒ None ? 474  cons y ys ⇒ ! ih ← (foldr2 … a xs ys f); 475 return f ih x y 476 ] 477 ]. 478 479 definition is_silent_cost_act_b : ActionLabel → bool ≝ 480 λact. match act with 481 [ cost_act x ⇒ match x with [None ⇒ true  _ ⇒ false ]  _ ⇒ false]. 482 483 definition eq_ActionLabel : ActionLabel → ActionLabel → bool ≝ 484 λc1,c2. 485 match c1 with 486 [ call_act f l ⇒ match c2 with [ call_act f' l' ⇒ f == f' ∧ l == l'  _ ⇒ false] 487  ret_act x ⇒ match c2 with [ret_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true  _ ⇒ false] 488  Some l ⇒ match y with [ Some l' ⇒ l == l'  _ ⇒ false] 489 ] 490  _ ⇒ false 491 ] 492  cost_act x ⇒ match c2 with [cost_act y ⇒ match x with [ None ⇒ match y with [ None ⇒ true  _ ⇒ false] 493  Some l ⇒ match y with [ Some l' ⇒ l == l'  _ ⇒ false] 494 ] 495  _ ⇒ false 496 ] 497  init_act ⇒ match c2 with [init_act ⇒ true  _ ⇒ false] 498 ]. 499 500 definition ret_costed_abs : list CostLabel → option ReturnPostCostLabel → option CostLabel ≝ 501 λkeep,x. 502 match x with 503 [ Some lbl ⇒ if (a_return_post lbl) ∈ keep then return (a_return_post lbl) 504 else None ? 505  None ⇒ None ? 506 ]. 507 508 definition check_continuations : ∀p : instr_params. 509 ∀l1,l2 : list (ActionLabel × (Instructions p)). 510 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → 511 option (Prop × (list CostLabel)) ≝ 512 λp,cont1,cont2,m,abs,keep. 513 foldr2 ??? 〈True,abs〉 cont1 cont2 514 (λx,y,z. 515 match call_post_clean p (\snd z) m keep (\snd x) with 516 [ None ⇒ 〈False,nil ?〉 517  Some w ⇒ 518 match \fst y with 519 [ ret_act opt_x ⇒ 520 match ret_costed_abs keep opt_x with 521 [ Some lbl ⇒ 〈\fst y = \fst z ∧\fst x ∧ \snd w = \snd y ∧ 522 get_element … m lbl = lbl :: (\fst w),(nil ?)〉 523  None ⇒ 524 〈\fst z = ret_act (None ?) ∧ \fst x ∧ \snd w = \snd y,\fst w〉 525 ] 526  cost_act opt_x ⇒ 527 match opt_x with 528 [ None ⇒ 〈\fst y = \fst z ∧ \fst x ∧ \snd w = \snd y,\fst w〉 529  Some xx ⇒ 〈\fst y = \fst z ∧\fst x ∧ \snd w = \snd y ∧ 530 get_element … m xx = xx :: (\fst w),(nil ?)〉] 531  _ ⇒ (* dummy *) 〈False,nil ?〉]]). 532 533 definition state_rel : ∀p. 534 associative_list DEQCostLabel CostLabel → list CostLabel → list CostLabel → 535 relation (state p) ≝ λp,m,l,keep,st1,st2. 536 match check_continuations ? (cont ? st1) (cont … st2) m (nil ?) keep with 537 [ Some x ⇒ let 〈prf1,l'〉 ≝ x in 538 prf1 ∧ call_post_clean … (code … st2) m keep l' = return 〈l,(code … st1)〉 539 ∧ store … st1 = store … st2 ∧ io_info … st1 = io_info … st2 540  None ⇒ False 541 ]. 542 543 include "Simulation.ma". 544 545 let rec len (S : abstract_status) (st1 : S) (st2 : S) (t : raw_trace S st1 st2) 546 on t : ℕ ≝ 547 match t with 548 [ t_base s ⇒ O 549  t_ind s1 s2 s3 l prf lt ⇒ (len … lt) + 1 550 ]. 551 (* 552 lemma associative_max : ∀n1,n2,n3.max (max n1 n2) n3 = max n1 (max n2 n3). 553 #n1 #n2 #n3 normalize @leb_elim normalize 554 [ @leb_elim normalize 555 [ #H1 #H2 @leb_elim normalize 556 [ @leb_elim normalize // * #H @⊥ @H assumption 557  @leb_elim normalize 558 [ #H3 * #H @⊥ @H @(transitive_le … H1) assumption 559  * #H @⊥ @H assumption 560 ] 561 ] 562  #H1 #H2 @leb_elim normalize 563 [ @leb_elim normalize // #_ #H cases H1 #H1 @⊥ @H1 assumption 564  @leb_elim normalize 565 [ #_ * #H @⊥ @H assumption 566  * #H @⊥ @H @(transitive_le … H2) 567 *) 568 let rec compute_max_n (p : instr_params) (i : Instructions p) on i : ℕ ≝ 569 match i with 570 [ EMPTY ⇒ O 571  RETURN x ⇒ O 572  SEQ x lab instr ⇒ let n ≝ compute_max_n … instr in 573 match lab with 574 [ None ⇒ n 575  Some l ⇒ 576 match l with 577 [ a_non_functional_label n' ⇒ S (max n n') ] 578 ] 579  COND x ltrue i1 lfalse i2 i3 ⇒ 580 let n1 ≝ compute_max_n … i1 in 581 let n2 ≝ compute_max_n … i2 in 582 let n3 ≝ compute_max_n … i3 in 583 let mx ≝ max (max n1 n2) n3 in 584 match ltrue with 585 [ a_non_functional_label lt ⇒ 586 match lfalse with 587 [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ] 588  LOOP x ltrue i1 lfalse i2 ⇒ 589 let n1 ≝ compute_max_n … i1 in 590 let n2 ≝ compute_max_n … i2 in 591 let mx ≝ max n1 n2 in 592 match ltrue with 593 [ a_non_functional_label lt ⇒ 594 match lfalse with 595 [a_non_functional_label lf ⇒ S (max (max mx lt) lf) ] ] 596  CALL f act_p r_lb i1 ⇒ 597 let n ≝ compute_max_n … i1 in 598 match r_lb with 599 [ None ⇒ n 600  Some lbl ⇒ match lbl with [a_return_cost_label l ⇒ S(max l n) ] 601 ] 602  IO lin io lout i1 ⇒ 603 let n ≝ compute_max_n … i1 in 604 match lin with 605 [a_non_functional_label l1 ⇒ 606 match lout with 607 [a_non_functional_label l2 ⇒ S(max (max n l1) l2) ] ] 608 ]. 609 610 611 lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ. 612 n ≥ compute_max_n … i1 → 613 ∀info,l.call_post_trans p i1 n l = info → 614 call_post_clean … (t_code … info) (lab_map … info) (lab_to_keep … info) l 615 = return 〈gen_labels … info,i1〉. 616 cases daemon (*TODO*) 617 qed. 618 619 definition trans_prog : ∀p,p'.Program p p' → 620 (Program p p') × (associative_list DEQCostLabel CostLabel) × (list CostLabel)≝ 621 λp,p',prog. 622 let max_all ≝ foldl … (λn,i.max n (compute_max_n … (f_body … i))) O (env … prog) in 623 let 〈t_env,n,m,keep〉 ≝ (foldr ?? 624 (λi,x.let 〈t_env,n,m,keep〉 ≝ x in 625 let info ≝ call_post_trans … (f_body … i) n (nil ?) in 626 〈(mk_env_item … (f_name … i) (f_pars … i) (f_lab … i) 627 (t_code … info) (f_ret … i)) :: t_env, 628 fresh … info, 〈a_call (f_lab … i),(a_call (f_lab … i)) :: (gen_labels ? info)〉 :: 629 ((lab_map … info) @ m),(lab_to_keep … info) @ keep〉) 630 (〈nil ?,max_all,nil ?,nil ?〉) (env … prog)) in 631 〈mk_Program ?? t_env (t_code … (call_post_trans … (main … prog) n (nil ?))),m,keep〉 . 632 633 discriminator option. 634 635 definition map_labels_on_trace : 636 (associative_list DEQCostLabel CostLabel) → list CostLabel → list CostLabel ≝ 637 λm,l.foldr … (λlab,t.(get_element … m lab) @ t) (nil ?) l. 638 639 lemma map_labels_on_trace_append: 640 ∀m,l1,l2. map_labels_on_trace m (l1@l2) = 641 map_labels_on_trace m l1 @ map_labels_on_trace m l2. 642 #m #l1 elim l1 // #hd #tl #IH #l2 >associative_append <IH // 643 qed. 644 645 lemma correctness : ∀p,p',prog. 646 let 〈t_prog,m,keep〉 ≝ trans_prog … prog in 647 ∀s1,s2,s1' : state p.∀l. 648 ∀t : raw_trace (operational_semantics … p' prog) s1 s2. 649 state_rel … m l keep s1 s1' → 650 ∃l'.∃s2'.∃t' : raw_trace (operational_semantics … p' t_prog) s1' s2'. 651 state_rel … m l' keep s2 s2' ∧ 652 l @ (map_labels_on_trace m (get_costlabels_of_trace … t)) = 653 (get_costlabels_of_trace … t') @ l' 654 ∧ len … t = len … t'. 655 #p #p' #prog @pair_elim * #trans_prog #m #keep #EQtrans 656 #s1 #s2 #s1' #l #t lapply l l lapply s1' s1' elim t 657 [ #st #s1' #l #H %{l} %{s1'} %{(t_base …)} % [2: %] %{H} normalize // ] 658 #st1 #st2 #st3 #lab whd in ⊢ (% → ?); #H inversion H in ⊢ ?; #st11 #st12 659 [ * #lab1 #new_code #new_cont #EQcode11 #EQcont11 #EQcode12 #EQcont12 #EQstore 660 #Hio11 #EQio12 #Hl1 #EQ1 #EQ2 #EQ3 #_ destruct #tl #IH #s1' #l1 661 whd in match state_rel in ⊢ (% → ?); normalize nodelta >EQcont11 662 whd in match check_continuations; normalize nodelta whd in match (foldr2 ???????); 663 inversion (cont ? s1') [ #_ *] * #l1' #new_code' #new_cont' #_ #EQconts1' 664 normalize nodelta inversion (foldr2 ???????) [ #_ *] * #H1 #l2 #EQHl2 665 >m_return_bind normalize nodelta 666 667 inversion (call_post_clean ?????) [ #_ **** ] 668 * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta 669 cases lab1 in Hio11 Hl1 EQcont11 H; normalize nodelta 670 671 [ whd in match is_silent_cost_act_b; normalize nodelta 672 cases lab1 in H Hio11; normalize nodelta 673 [1,2,4: [1,2: #x [ #y]] #H #Hio11 #EQ destruct] 674 * normalize nodelta [2: #x #H #Hio11 #EQ destruct] #H #Hio11 #_ 675 inversion(call_post_clean ?????) 676 [ #_ *** ] * #l3 #code_c_st12 #EQcode_c_st12 normalize nodelta ***** 677 #EQ destruct(EQ) #HH1 #EQ destruct(EQ) >EQcode11 678 whd in match (call_post_clean ?????) in ⊢ (% → ?); whd in ⊢ (??%% → ?); 679 inversion(code … s1') 680 [ #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ 681 destruct(EQ) *: cases daemon (*ASSURDI!!*)] #EQcode_s1' 682 normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio 683 cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 ?) 684 [2: whd whd in match check_continuations; normalize nodelta >EQHl2 685 normalize nodelta % // % // >EQcode_c_st12 % // ] #l3 * #st3' * #t' ** 686 #Hst3st12' #EQcost #EQlen %{l3} %{st3'} %{(t_ind … (cost_act (None ?)) … t')} 687 [ whd @(empty ????? 〈(cost_act (None ?)),?〉) 688 [3: @hide_prf assumption 4: @hide_prf @EQconts1' *: ] @hide_prf // 689 [ <EQio #H2 @⊥ lapply(Hio11 H2) * #F #eq destruct  % *] ] % 690 [ %{Hst3st12'} whd in match (get_costlabels_of_trace ????); 691 whd in match (get_costlabels_of_trace ????) in ⊢ (???%); // 692  whd in match (len ????); whd in match (len ????) in ⊢ (???%); 693 >EQlen % 694 ] 695  #non_sil_lab1 normalize nodelta inversion(call_post_clean ?????) [ #_ ****] 696 * #l3 #code' #EQcall' normalize nodelta inversion(ret_costed_abs ??) 697 [2: #x #H2 @⊥ cases lab1 in Hl1 H2; normalize 698 [ #f #c #_ 699  #x * #ABS @⊥ @ABS % 700  #x #_ 701  #_ 702 ] 703 #EQ destruct(EQ) ] 704 #Hlab1 normalize nodelta ***** #EQ destruct(EQ) #HH1 #EQ destruct(EQ) 705 >EQcode11 inversion(code … s1') 706 [ #x #EQ1 normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ 707 destruct(EQ) *: cases daemon (*ASSURDI!!*)] #EQcode_s1' 708 normalize in ⊢ (% → ?); #EQ destruct(EQ) #EQstore #EQio 709 cases(IH (mk_state ? new_code' new_cont' (store … s1') false) l1 ?) 710 [2: whd whd in match check_continuations; normalize nodelta >EQHl2 711 normalize nodelta % // % // % // >EQcall' % ] #l4 * #st3' * #t' ** 712 #Hst3st3' #EQcost #EQlen %{l4} %{st3'} %{(t_ind … lab1 … t')} 713 [ whd @(empty ????? 〈lab1,?〉) 714 [3: @hide_prf assumption 4: assumption *:] @hide_prf // #H3 @Hio11 >EQio @H3] 715 % [2: whd in match (len ????); whd in match (len ????) in ⊢ (???%); 716 >EQlen % ] 717 %{Hst3st3'} >associative_append <EQcost <associative_append 718 >map_labels_on_trace_append <associative_append @eq_f2 // 719 cases new_code' in EQcall'; 720 [ #y  #seq #opt_l #i1  #cond #ltrue #i_true #lfalse #i_false #i1 721  #cond #ltrue #i_true #lfalse #ifalse  #f #act_p #ret_opt #i  #l_in #io #l_out #i ] 722 whd in match (call_post_clean ?????); 723 [1,2: #EQ destruct(EQ) // 724 725 726 whd in match (get_costlabels_of_trace ??? ?) in ⊢ (??%%); 727 728 @eq_f2 whd in ⊢ (??%?); 729 730 731 732 cases daemon (*TODO*) 733 qed.
Note: See TracChangeset
for help on using the changeset viewer.