Changeset 2708 for src/joint/linearise.ma
 Timestamp:
 Feb 22, 2013, 7:11:30 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/linearise.ma
r2702 r2708 256 256 cases s in H3; [3: *] 257 257 [ * ] normalize nodelta 258 [2,4: [#f #args #dest #s'] #nxt * #EQnth_opt #H %{EQnth_opt} 259 inversion (lookup … visited nxt) in H; [2: #n'] #EQlookup 258 [1,2,4: [ #c  #f #args #dest #s'] #nxt * #EQnth_opt #H %{EQnth_opt} 259 inversion (lookup … visited nxt) in H; [2,4,6: #n'] normalize nodelta 260 #EQlookup 260 261 normalize nodelta * 261 [ #EQn' %1 >EQn' %262  #H %2{H}263  #H' lapply (All_nth … H … H')262 [1,3,5: #EQn' %1 >EQn' % 263 2,4,6: #H %2{H} 264 *: #H' lapply (All_nth … H … H') 264 265 whd in ⊢ (?%→?); >EQlookup * 265 266 ] 266  3:#a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}267  #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1} 267 268 inversion (lookup … visited lfalse) in H2; 268 269 [ #ABS * #H' lapply (All_nth … H … H') … … 270 271  #n' #_ normalize nodelta #EQ >EQ % 271 272 ] 272  #s #H (*CSC XXXXXXXXXXXXXXXXXXXX @H *)273  #s #H @H 273 274 ] 274 275 ] … … 326 327 12: (* add_req_gen utility *) 327 328 #P whd in match add_req_gen; 328 cases statement [ * [#f #args #dest #a #ltrue  #s ] #nxt  #s  * ] 329 [2,4: normalize nodelta #l #H1 #H2 lapply (H2 … (refl …)) H2 330 cases (l ∈ add …) in H1; normalize nodelta #H1 #H2 try @H2 try @H1 try % 331 // 332 3,5: normalize nodelta [#_] #H #_ @H % 333  normalize nodelta in dest nxt ⊢ %; inversion (args ∈ add …) #EQ 334 normalize nodelta [ @nxt  @dest ] >EQ try % ] 335 14: skip 336 ] cases daemon (*CSC: XXXXXXXXX 329 cases statement [ * [ #cost  #f #args #dest #a #ltrue  #s ] #nxt  #s  * ] 330 normalize nodelta 331 [3,5: #H #_ @(H I) ] 332 inversion (nxt ∈ visited') #EQ normalize nodelta 333 #H1 #H2 [1,3,5: @(H2 … (refl …)) >EQ % *: @H1 % * ] 337 334 3: elim H #pre ** #H1 #H2 #_ 338 335 #i >mem_set_union … … 341 338 #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption 342 339  >mem_set_union 343 #H elim (orb_Prop_true … H) H (*CSC XXXXXXXXXX340 #H elim (orb_Prop_true … H) H 344 341 [ #i_expl %1 @Exists_append_l 345 342 lapply i_expl whd in match translated_statement; 346 cases statement [ * [ #f #args #dest  #a #ltrue  #s ] #nxt  #s  *] normalize nodelta #H 343 cases statement [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  *] 344 normalize nodelta #H 347 345 lapply (mem_list_as_set … H) H #H 348 [1, 3,4: @Exists_append_r assumption ]346 [1,2,4,5: @Exists_append_r assumption ] 349 347 cases (nxt ∈ visited') in H; normalize nodelta * [2,4: * [2: * ]] 350 348 #EQ destruct(EQ) [ %1 % *: %2 %1 % ] … … 366 364 #i_vis %2 >mem_set_add @orb_Prop_r assumption 367 365 ] 368 ] *) cases daemon366 ] 369 367 ] 370 368 4,5,6: change with reverse in match rev; … … 423 421 lapply (in_map_domain … visited vis_hd) 424 422 >H3 normalize nodelta // 425  %{statement} (*CSC XXXXXXX423  %{statement} 426 424 % 427 425 [ @lookup_eq_safe … … 429 427 change with statement in match (lookup_safe ?????); 430 428 cases statement; 431 [ * [ # f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] normalize nodelta432 [1,2,3 : inversion (nxt ∈ visited') normalize nodelta #nxt_vis ]433 [1,2, 5,6: %  %2  %1 % ]434 [1,3,5,7,9,1 0,12:429 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] normalize nodelta 430 [1,2,3,4: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ] 431 [1,2,3,4,7,8: %  %2  %1 % ] 432 [1,3,5,7,9,11,13,14,16: 435 433 >nth_opt_append_r >rev_length <gen_length_prf try % 436 <minus_n_n try % whd in match graph_to_lin_statement; normalize nodelta437 >nxt_vis % 434 <minus_n_n try % try( whd in match graph_to_lin_statement; normalize nodelta 435 >nxt_vis %) 438 436 *: 439 437 lapply (in_map_domain … visited' nxt) >nxt_vis normalize nodelta 440 [1,3: * #n' ] #EQlookup >EQlookup normalize nodelta 441 [1,2: %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4: %2 %1 ] 442 <minus_Sn_n % 443 *: %% 444 ] 445 ]*) cases daemon 438 [1,3,5: * #n' ] #EQlookup >EQlookup normalize nodelta 439 try (%% @False) 440 %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4,6: %2 %1 ] 441 <minus_Sn_n % 442 ] 446 443 ] 447 444 ] 448 445  #NEQ #n_i >(lookup_add_miss … visited … NEQ) 449 cases daemon (*CSC XXXX450 446 #Hlookup elim (generated_prf1 … Hlookup) 451 447 #G1 * #s * #G2 #G3 … … 463 459 %{G2} 464 460 cases s in G3; 465 [ * [ #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] 466 [1,3: * #EQnth_opt #next_spec %  * [*] #EQnth_opt [#next_spec %1 %  %2]  #EQnth_opt ] 467 [1,3,5,7: @nth_opt_append_hit_l assumption 468 2,4,6: @(eq_identifier_elim … nxt vis_hd) 469 [1,3: #EQ destruct(EQ) >lookup_add_hit whd [ %1 ] 461 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] 462 [1,2,4: normalize nodelta #H cases H in ⊢ ?; H 463 #EQnth_opt #next_spec % 3: normalize nodelta * [*] #EQnth_opt [#next_spec %1 %  %2]  #EQnth_opt ] 464 [1,3,5,7,9: @nth_opt_append_hit_l assumption 465 2,4,6,8: @(eq_identifier_elim … nxt vis_hd) 466 [1,3,5,7: #EQ destruct(EQ) >lookup_add_hit whd 467 [1,2,3: %1] 470 468 lapply (in_map_domain … visited vis_hd) 471 469 >H3 #EQ >EQ in next_spec; * #_ #OK >OK % 472 *: #NEQ' >(lookup_add_miss … visited … NEQ') 473 lapply (in_map_domain … visited nxt) 474 inversion (nxt ∈ visited) #nxt_vis [1,3: * #n'' ] #EQlookup' 475 >EQlookup' in next_spec; whd in ⊢ (%→%); 476 [ * [ #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption 477  #H @H 478 *: * >H2 470 *: #NEQ' >(lookup_add_miss … visited … NEQ') in 471 ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 472 generalize in match next_spec in ⊢ ?; 473 inversion (lookup … visited nxt) normalize nodelta 474 [2,4,6,8: #n'' ] #EQlookup' 475 [1,2,3: * [1,3,5: #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption 476 4: #H @H 477 *: * #nxt_visiting @⊥ 478 >H2 in nxt_visiting; 479 479 cases pre in H1; 480 [1,3 : #_480 [1,3,5,7: #_ 481 481 *: #frst #pre_tl * #ABS #_ 482 482 ] whd in ⊢ (??%?→?); #EQ destruct(EQ) 483 [1,2 : cases NEQ' #ABS cases (ABS ?) %484 *: >nxt_vis in ABS;*483 [1,2,3,4: cases NEQ' #ABS cases (ABS ?) % 484 *: lapply ABS; whd in ⊢ (?%→?); >EQlookup' * 485 485 ] 486 486 ] 487 487 ] 488 10: @nth_opt_append_hit_l assumption 488 489 ] 489 ] *)490 ] 490 491 ] 491 492  #i whd in match visited'; … … 498 499  change with (bool_to_Prop (¬eq_identifier ??? ∧ ?)) 499 500 >eq_identifier_false [2: % #ABS <ABS in Heq; * #ABS' @ABS' % ] 500 @add_req_gen_prf [ #_  #s #next #_ #_] %501 @add_req_gen_prf [ #_  #s #next #_ ] % 501 502 ] 502 503 ] 503 504  @add_req_gen_prf 504 [ #K  # s #next #K #next_vis %1 %1 %{(GOTO … next)} % ]505 [ #K  #next #K #next_vis %1 %1 %{(GOTO … next)} % ] 505 506 whd in match generated'; whd in match translated_statement; 506 507 normalize nodelta 507 508 change with statement in match (lookup_safe ?????); 508 509 cases statement in K; 509 [ * [ # s  #a #ltrue] #nxt  #s #_ %1 %1 %{s} %  * ] normalize nodelta510 [ 2: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis510 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s #_ %1 %1 %{s} %  * ] normalize nodelta 511 [3: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis 511 512 [ >nxt_vis normalize nodelta %1 %2 %{a} %{ltrue} %{nxt} % ] 512  #nxt_vis ]513 *: #nxt_vis ] 513 514 %2 % * >nxt_vis * 514 515  whd in match generated'; 515 @add_req_gen_prf [ #_  # s #next #_ #_ ] normalize >gen_length_prf %516 @add_req_gen_prf [ #_  #next #_ #_ ] normalize >gen_length_prf % 516 517  517 ] *)518 ] 518 519 qed. 519 520 … … 643 644 [ sequential s' nxt ⇒ 644 645 match s' with 645 [ step_seq _ ⇒ 646 (stmt_at … c n = Some ? (sequential … s' it)) ∧ 646 [ COND a ltrue ⇒ 647 (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨ 648 (stmt_at … c n = Some ? (FCOND … I a ltrue nxt)) 649  _ ⇒ 650 (stmt_at … c n = Some ? (sequential … s' it)) ∧ 647 651 ((sigma nxt = Some ? (S n)) ∨ 648 652 (stmt_at … c (S n) = Some ? (GOTO … nxt))) 649  COND a ltrue ⇒650 (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨651 (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))652  CALL _ _ _ ⇒653 (stmt_at … c n = Some ? (sequential … s' it)) ∧654 ((sigma nxt = Some ? (S n)) ∨655 (stmt_at … c (S n) = Some ? (GOTO … nxt)))656  COST_LABEL _ ⇒657 (stmt_at … c n = Some ? (sequential … s' it)) ∧658 ((sigma nxt = Some ? (S n)) ∨659 (stmt_at … c (S n) = Some ? (GOTO … nxt)))660 653 ] 661 654  final s' ⇒ … … 708 701  >commutative_plus change with (? ≤ g) % 709 702 ] 710 cases daemon qed. (*711 703 ** 712 704 #visited #required #generated normalize nodelta **** … … 725 717 * #n_lbl #EQsigma 726 718 elim (sigma_prop … EQsigma) #_ * #stmt * #_ 727 cases stmt [ * [ # s  #a #ltrue] #nxt  #s  * ] normalize nodelta728 [ * #EQnth_opt #_  * [ * ] #EQnth_opt [ #_ ] #EQnth_opt ]719 cases stmt [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] normalize nodelta 720 [1,2,4: * #EQnth_opt #_ 3: * [ * ] #EQnth_opt [ #_ ] 5: #EQnth_opt ] 729 721 >(nth_opt_index_of_label ???? n_lbl ? H) 730 [1,4,7,10: normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption 731 3: @(sequential … s it) 6: @(sequential … (COND … a ltrue) it) 732 9: @(FCOND … I a ltrue nxt) 12: @(final … s) 733 2,5,8,11: >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind 734 >H2 % 722 try (normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption) 723 [1,3,5,7,9,11: 724 >nth_opt_filter_labels in ⊢ (??%?); 725 (* without the try it does not work *) 726 try >EQnth_opt in ⊢ (??%?); 727 >m_return_bind in ⊢ (??%?); 728 >m_return_bind in ⊢ (??%?); 729 >H2 in ⊢ (??%?); % 730 *: 735 731 ] 736 732  #eq_lookup elim (sigma_prop ?? eq_lookup) … … 739 735 [ @All_append 740 736 [ cases stmt in stmt_spec; 741 [ * [ #s  #a #ltrue ] #nxt  #s #_ %  * ] 742 normalize nodelta * [ #stmt_at_EQ * #nxt_spec  * #stmt_at_EQ #nxt_spec  #stmt_at_EQ ] 737 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s #_ %  * ] 738 normalize nodelta 739 [1,2,4: * #stmt_at_EQ * #nxt_spec 3: * [ * ] #stmt_at_EQ [ #nxt_spec ]] 743 740 %{I} 744 [1,3: >nxt_spec % #ABS destruct(ABS) 745 *: lapply (in_map_domain … visited nxt) 746 >req_vis 747 [1,3: * #x #EQ >EQ % #ABS destruct(ABS) 748 2: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …)) 749 whd in ⊢ (??%?); >nxt_spec % 750 4: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …))) 751 whd in ⊢ (??%?); >stmt_at_EQ % 752 ] 741 try (>nxt_spec % #ABS destruct(ABS) @False) 742 lapply (in_map_domain … visited nxt) 743 >req_vis 744 [1,3,5,7: * #x #EQ >EQ % #ABS destruct(ABS) 745 2,4,6: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …)) 746 whd in ⊢ (??%?); >nxt_spec % 747 8: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …))) 748 whd in ⊢ (??%?); >stmt_at_EQ % 753 749 ] 754 750  cases stmt in stmt_spec; 755 [ * [ # s  #a #ltrue] #nxt  #s  * ] normalize nodelta756 [ * #EQ #_  * [ * #EQ #_  #EQ ] #EQ ]751 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] normalize nodelta 752 [1,2,4: * #EQ #_ 3: * [ * ] #EQ [ #_ ] 5: #EQ ] 757 753 whd in match stmt_explicit_labels; normalize nodelta 758 [ @(All_mp … (labels_in_req n (sequential … s it) ?)) 754 [ @(All_mp … (labels_in_req n (sequential … (COST_LABEL … cost) it) ?)) 755  @(All_mp … (labels_in_req n (sequential … (CALL … f args dest) it) ?)) 756  @(All_mp … (labels_in_req n (sequential … s it) ?)) 759 757  @(All_mp … (labels_in_req n (sequential … (COND … a ltrue) it) ?)) 758 6: @(All_mp … (labels_in_req n (final … s) ?)) 760 759  cases (labels_in_req n (FCOND … I a ltrue nxt) ?) 761 760 [ #l_req #_ %{I} lapply (in_map_domain … visited ltrue) 762 761 >(req_vis … l_req) * #n #EQ' >EQ' % #ABS destruct(ABS) ] 763  @(All_mp … (labels_in_req n (final … s) ?))764 762 ] 765 [1,3,6: #l #l_req >(lookup_eq_safe … (req_vis … l_req)) % #ABS destruct(ABS) 763 [1,3,5,7,9: #l #l_req >(lookup_eq_safe … (req_vis … l_req)) 764 % #ABS destruct(ABS) 766 765 *: whd in ⊢ (??%?); >EQ % 767 766 ] 768 767 ] 769 768  cases stmt in stmt_spec; 770 [ * [ # s  #a #ltrue] #nxt  #s  * ] normalize nodelta771 [ * #EQ #H  * [ * #EQ #H  #EQ ] #EQ ]769 [ * [ #cost  #f #args #dest  #a #ltrue  #s ] #nxt  #s  * ] normalize nodelta 770 [1,2,4: * #EQ #H 3: * [ * ] #EQ [ #H ] 5: #EQ ] 772 771 >stmt_at_filter_labels 773 772 whd in match (stmt_at (mk_lin_params p) ?? n); >EQ normalize nodelta 774 [ % [%] cases H H [#H %1{H}  #EQ' %2 >stmt_at_filter_labels whd in ⊢ (??%?); >EQ' % ] 773 [1,2,3: % [1,3,5: %] cases H H 774 #H try (%1{H}) %2 >stmt_at_filter_labels whd in ⊢ (??%?); >H % 775 775  %1 %{H} % 776 776  %2 % … … 796 796 cut (generated = S i) 797 797 [ @(le_to_le_to_eq … (not_lt_to_le … INEQ) ) 798 elim (option_bind_inverse ????? EQ) #x * #EQ1 #EQ2 798 whd in EQ : (??%?); inversion (nth_opt ???) in EQ; 799 [2: #x ] #EQ1 whd in ⊢ (??%%→?); #EQ2 destruct 799 800 <length_reverse 800 801 @(nth_opt_hit_length … EQ1) … … 843 844 〈«mk_joint_internal_function (mk_lin_params p) globals 844 845 (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig) 845 (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) 846 (joint_if_stacksize ?? f_sig) code entry , ?»,846 (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) (joint_if_locals ?? f_sig) 847 (joint_if_stacksize ?? f_sig) code entry entry (* exit is dummy! *), ?», 847 848 sigma〉. 848 849 normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.