Changeset 2203 for src/Clight/labelSimulation.ma
 Timestamp:
 Jul 17, 2012, 6:57:40 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/labelSimulation.ma
r2202 r2203 314 314 . 315 315 316 (* TODO: this (or something like it) ought to be elsewhere. *)317 inductive plus (ge:genv) : state → trace → state → Prop ≝318  plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2319  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.320 321 316 (* Some details are invariant under labelling. *) 322 317 lemma label_function_return : ∀f. … … 653 648 state_with_labels_partial s1 s1' → 654 649 exec_step ge s1 = Value … 〈tr,s2〉 → 655 ∃tr',s2'. plus ge' s1' tr' s2' ∧650 ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧ 656 651 trace_with_extra_labels tr tr' ∧ 657 652 state_with_labels s2 s2'. … … 669 664 lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?); 670 665 [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))} 671 % [ % [ @ plus_one whd in ⊢ (??%?); >label_function_return >E @refl666 % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E @refl 672 667  // ]  /3/ ] 673 668  *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct … … 676 671 %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)} 677 672 whd in EX:(??%%); destruct 678 % [ % [ @ plus_one @refl  // ]  /3/ ]673 % [ % [ @cl_plus_one @refl  // ]  /3/ ] 679 674  #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr} 680 675 whd in EX:(??%%); destruct 681 % [ 2: % [ % [ @ plus_one @refl  // ]  @swl_partial @swl_whilestate // ]  skip ]676 % [ 2: % [ % [ @cl_plus_one @refl  // ]  @swl_partial @swl_whilestate // ]  skip ] 682 677  #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 683 678 cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem … … 685 680 normalize in EXbrem; destruct 686 681 cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te 687 [ % [ 2: % [ 2: % [ % [ @ plus_one682 [ % [ 2: % [ 2: % [ % [ @cl_plus_one 688 683 whd in ⊢ (??%?); >EXe' in ⊢ (??%?); 689 684 whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?); … … 691 686  // ] 692 687  @swl_partial @swl_dowhilestate // ]  skip ]  skip ] 693  % [ 2: % [ 2: % [ % [ @ plus_succ [688  % [ 2: % [ 2: % [ % [ @cl_plus_succ [ 694 689 4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?); 695 690 whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?); 696 691 whd in ⊢ (??%?); @refl 697 692  skip  skip 698  5: @ plus_succ [ 4: @refl  skip  skip699  5: @ plus_one @refl  skip ]  skip ]693  5: @cl_plus_succ [ 4: @refl  skip  skip 694  5: @cl_plus_one @refl  skip ]  skip ] 700 695  <(E0_right tr) @twel_app /2/ ] 701 696  /3/ ]  skip ]  skip ] … … 703 698  #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 704 699 whd in EX:(??%?); destruct 705 %{E0} % [2: % [ % [ @ plus_one @refl  // ]  /3/ ]  skip ]700 %{E0} % [2: % [ % [ @cl_plus_one @refl  // ]  /3/ ]  skip ] 706 701  #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 707 702 whd in EX:(??%?); destruct 708 %{E0} % [2: % [ % [ @ plus_one @refl  // ]  /4/ ]  skip ]703 %{E0} % [2: % [ % [ @cl_plus_one @refl  // ]  /4/ ]  skip ] 709 704  #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct 710 705 whd in EX:(??%?); destruct 711 %{E0} % [2: % [ % [ @ plus_one @refl  // ]  /4/ ]  skip ]706 %{E0} % [2: % [ % [ @cl_plus_one @refl  // ]  /4/ ]  skip ] 712 707  #k0 #k0' #K #_ #E1 #E2 #E3 destruct 713 708 whd in EX:(??%?); destruct 714 %{E0} % [2: % [ % [ @ plus_one @refl  // ]  /4/ ]  skip ]709 %{E0} % [2: % [ % [ @cl_plus_one @refl  // ]  /4/ ]  skip ] 715 710  #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct 716 711 whd in EX:(??%?); 717 712 lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?); 718 713 [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct 719 %{E0} % [2: % [ % [ @ plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);714 %{E0} % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?); 720 715 @refl  // ]  /4/ ]  skip ] 721 716  *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct 722 717 ] 723 718  #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct 724 % [2: % [2: % [ % [ @ plus_one @refl  // ]  /3/ ] skip ] skip ]719 % [2: % [2: % [ % [ @cl_plus_one @refl  // ]  /3/ ] skip ] skip ] 725 720 ] 726 721  * #a1 #ty1 #a2 #EX … … 734 729 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2 735 730 % [2: % [2: % [ % [ 736 @ plus_one whd in ⊢ (??%?);731 @cl_plus_one whd in ⊢ (??%?); 737 732 >exec_lvalue_labelled >EX1' in ⊢ (??%?); 738 733 whd in ⊢ (??%?); >EX2' in ⊢ (??%?); … … 757 752 [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ] 758 753 % [2,4: % [2,4: % [1,3: % [1,3: 759 @ plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?);  >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)754 @cl_plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?);  >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *) 760 755 whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?);  >EX2' in ⊢ (??%?); ] 761 756 whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?); … … 766 761 whd in EX:(??%%); destruct 767 762 whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 768 %{E0} % [2: % [ % [ @ plus_one @refl  // ]  @swl_partial @swl_state /2/ ]  skip ]763 %{E0} % [2: % [ % [ @cl_plus_one @refl  // ]  @swl_partial @swl_state /2/ ]  skip ] 769 764  #a #st1 #st2 #EX 770 765 cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 777 772 whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7 778 773 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 779 % [2,4: % [2,4: % [1,3: % [1,3: @ plus_succ [ 4,9:774 % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: 780 775 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?);  >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 781 776 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?);  >EX2 in ⊢ (??%?); ] 782 777 whd in ⊢ (??%?); @refl 783 778  1,2,6,7: skip 784  5,10: @ plus_one @refl779  5,10: @cl_plus_one @refl 785 780  *: skip 786 781 ] … … 797 792 >shift_fst 798 793 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 799 % [2,4: % [2,4: % [1,3: % [1,3: @ plus_succ [ 4,9: @refl  1,2,6,7: skip800  5,10: @ plus_succ [ 4,9:794 % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl  1,2,6,7: skip 795  5,10: @cl_plus_succ [ 4,9: 801 796 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?);  >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 802 797 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?);  >EX2 in ⊢ (??%?); ] 803 798 whd in ⊢ (??%?); @refl 804 799  1,2,6,7: skip 805  5: @ plus_one @refl806  10: @ plus_succ [ 4: @refl  5: @plus_one @refl  *: skip ] *: skip ]800  5: @cl_plus_one @refl 801  10: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl  *: skip ] *: skip ] 807 802  *: skip 808 803 ] … … 815 810 whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst 816 811 whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst 817 % [2: % [2: % [ % [ @ plus_succ [ 4: @refl  1,2: skip818  5: @ plus_succ [ 4: @refl  1,2: skip  5: @plus_one //  skip ]  skip ]812 % [2: % [2: % [ % [ @cl_plus_succ [ 4: @refl  1,2: skip 813  5: @cl_plus_succ [ 4: @refl  1,2: skip  5: @cl_plus_one //  skip ]  skip ] 819 814  /2/ ]  /4/ ]  skip ]  skip ] 820 815  #st1 #a #st2 #st #EX … … 829 824 normalize in EX; destruct 830 825 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 831 % [2,4: % [2,4: % [1,3: % [1,3: @ plus_succ [ 4,9: @refl  1,2,6,7: skip832  5,10: @ plus_succ [ 4,9:826 % [2,4: % [2,4: % [1,3: % [1,3: @cl_plus_succ [ 4,9: @refl  1,2,6,7: skip 827  5,10: @cl_plus_succ [ 4,9: 833 828 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?);  >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 834 829 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?);  >EX2 in ⊢ (??%?); ] 835 830 whd in ⊢ (??%?); @refl 836 831  1,2,6,7: skip 837  5: @ plus_one @refl838  10: @ plus_succ [ 4: @refl  5: @plus_one @refl  *: skip ] *: skip ]832  5: @cl_plus_one @refl 833  10: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl  *: skip ] *: skip ] 839 834  *: skip 840 835 ] … … 842 837 ] 2,4: /4/ ]  *: skip ]  *: skip ] 843 838  whd in EX:(??%%); destruct 844 % [2: % [2: %[ %[ @ plus_succ [ 4: @refl  5: @plus_one839 % [2: % [2: %[ %[ @cl_plus_succ [ 4: @refl  5: @cl_plus_one 845 840 whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip' 846 841 >Eskip' whd in ⊢ (??%?); @refl  *: skip ] // ]  @swl_partial @swl_state /2/ ] … … 861 856 whd in match (label_statement ??); 862 857 % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: % 863 [1,11,13: @ plus_one @refl  2,12,14: //864  @ plus_succ [ 4: @refl  5: @plus_succ [ 4: @refl  5: @plus_one @refl *:skip]*:skip]  /2/865  @ plus_succ [ 4: @refl  5: @plus_succ [ 4: @refl  5: @plus_one @refl *:skip]*:skip]  /2/866  @ plus_succ [ 4: @refl  5: @plus_one @refl *:skip]  /2/867  @ plus_succ [ 4: @refl  5: @plus_succ [ 4: @refl  5: @plus_one @refl *:skip]*:skip]  /2/868 ] *: /3 / ]*: skip]*: skip ]858 [1,11,13: @cl_plus_one @refl  2,12,14: // 859  @cl_plus_succ [ 4: @refl  5: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl *:skip]*:skip]  /2/ 860  @cl_plus_succ [ 4: @refl  5: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl *:skip]*:skip]  /2/ 861  @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl *:skip]  /2/ 862  @cl_plus_succ [ 4: @refl  5: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl *:skip]*:skip]  /2/ 863 ] *: /3 by swl_partial, swl_state/ ]*: skip]*: skip ] 869 864  #EX inversion KL 870 865 [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct … … 881 876 whd in match (label_statement ??); 882 877 [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: % 883 [1,3,7,9,11: @ plus_one @refl  5: @plus_succ [4:@refl  5:@plus_one @refl  *: skip ]878 [1,3,7,9,11: @cl_plus_one @refl  5: @cl_plus_succ [4:@refl  5:@cl_plus_one @refl  *: skip ] 884 879  *: // ]  *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ] *:skip ] *: skip ] 885 880  cases (bindIO_inversion ??????? EX) EX * #v1 #tr1 * #EX1 #EX … … 887 882 normalize in EX; destruct 888 883 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1 889 % [2,4: % [2,4: % [1,3: % [1,3: [ @ plus_one  @plus_succ ] [ 1,5:884 % [2,4: % [2,4: % [1,3: % [1,3: [ @cl_plus_one  @cl_plus_succ ] [ 1,5: 890 885 whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?);  >EX1' in ⊢ (??%?); ] (* XXX repeated? *) 891 886 whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?);  >EX2 in ⊢ (??%?); ] 892 887 whd in ⊢ (??%?); @refl 893  6: @ plus_succ [ 4: @refl  5: @plus_one @refl  *: skip ] *: skip ]888  6: @cl_plus_succ [ 4: @refl  5: @cl_plus_one @refl  *: skip ] *: skip ] 894 889  //  <(E0_right tr) @twel_app /2/ 895 890 ] … … 911 906 [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ] 912 907 whd in EX:(??%%); destruct 913 % [2,4: % [2,4: % [1,3: %[1,3: @ plus_one908 % [2,4: % [2,4: % [1,3: %[1,3: @cl_plus_one 914 909 whd in ⊢ (??%?); 915 910 [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety'' … … 927 922 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1 928 923 whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2 929 % [2: % [2: % [ % [ @ plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl924 % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl 930 925  // ] cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/ 931 926 ]skip ] skip ] … … 934 929 whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst 935 930 whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst 936 %[2: %[2: %[ %[ @ plus_succ937 [ 4: @refl  5: @ plus_one @refl  *: skip ]931 %[2: %[2: %[ %[ @cl_plus_succ 932 [ 4: @refl  5: @cl_plus_one @refl  *: skip ] 938 933  /2/ ]  /3/ ] skip ] skip ] 939 934  #l #EX … … 946 941 cases (label_find_label_fn … KL F) 947 942 #u' * #cs * #k1' * #F' #K' 948 % [2: %[2: %[ %[ @ plus_succ949 [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl  5: @ plus_one @refl  *: skip ]943 % [2: %[2: %[ %[ @cl_plus_succ 944 [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl  5: @cl_plus_one @refl  *: skip ] 950 945  /2/ ]  /3/ ]  skip ]  skip ] 951 946 ] 952 947  #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1 953 % [2: % [2: % [ % [ @ plus_one @refl  // ]  /3/ ]  skip ] skip ]948 % [2: % [2: % [ % [ @cl_plus_one @refl  // ]  /3/ ]  skip ] skip ] 954 949 ] 955 950  #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX … … 959 954 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1 960 955 [ % [2: % [2: % [ % [ 961 @ plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);956 @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 962 957 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 963 5: @ plus_one @refl  *: skip ]964  <(E0_right tr) /3/ ] /4 / ] skip ] skip ]958 5: @cl_plus_one @refl  *: skip ] 959  <(E0_right tr) /3/ ] /4 by swl_partial, swl_state, cwl_while/ ] skip ] skip ] 965 960  % [2: % [2: % [ % [ 966 @ plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);961 @cl_plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 967 962 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 968  5: @ plus_succ [4: @refl969  5: @ plus_one @refl  *: skip ]  *: skip ]963  5: @cl_plus_succ [4: @refl 964  5: @cl_plus_one @refl  *: skip ]  *: skip ] 970 965  <(E0_right tr) /3/ ] /3/ ] skip ] skip ] 971 966 ] … … 973 968 whd in EX:(??%%); destruct 974 969 % [2: % [2: % [ % [ 975 @ plus_succ [4: %  5: @plus_one %  *: skip ]970 @cl_plus_succ [4: %  5: @cl_plus_one %  *: skip ] 976 971  /2/ ] /4/ ] skip ] skip ] 977 972  #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX … … 981 976 cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1 982 977 [ % [2: % [2: % [ % [ 983 @ plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);978 @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 984 979 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 985  5: whd in ⊢ (?? (??%%??)??); @plus_one @refl980  5: whd in ⊢ (?????(??%%??)??); @cl_plus_one @refl 986 981  *: skip ] <(E0_right tr) /3/ ]  /4/ ] skip ] skip ] 987 982  % [2: % [2: % [ % [ 988 @ plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);983 @cl_plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?); 989 984 whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl 990  5: whd in ⊢ (?? (??%%??)??); @plus_succ [4: @refl991  5: @ plus_one @refl ] *: skip ] <(E0_right tr) /3/ ] /3/ ] skip ] skip985  5: whd in ⊢ (?????(??%%??)??); @cl_plus_succ [4: @refl 986  5: @cl_plus_one @refl ] *: skip ] <(E0_right tr) /3/ ] /3/ ] skip ] skip 992 987 ] 993 988 ] … … 1000 995 lapply (refl ? (label_function f)) whd in ⊢ (???% → ?); 1001 996 @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef 1002 % [2: % [2: % [ % [ @ plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);997 % [2: % [2: % [ % [ @cl_plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?); 1003 998 whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl 1004  5: @ plus_one @refl  *: skip ]  /2/ ] <Ef @swl_partial @swl_state @K ] skip ] skip ]999  5: @cl_plus_one @refl  *: skip ]  /2/ ] <Ef @swl_partial @swl_state @K ] skip ] skip ] 1005 1000  #id #tys #ty #args #k #k' #m #K #EX 1006 1001 cases (bindIO_inversion ??????? EX) EX #vs * #EX1 #EX … … 1013 1008  *: normalize #A try #B try #C destruct 1014 1009 ] 1015 % [2: % [2: % [ % [ @ plus_one @refl  // ] /2/ ] skip ] skip ]1010 % [2: % [2: % [ % [ @cl_plus_one @refl  // ] /2/ ] skip ] skip ] 1016 1011  9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %; 1017 1012 [ #EX whd in EX:(??%?); destruct 1018 % [2: % [2: % [ % [ @ plus_one @refl  // ] /3/ ] skip ] skip ]1013 % [2: % [2: % [ % [ @cl_plus_one @refl  // ] /3/ ] skip ] skip ] 1019 1014  * * #b #o #ty #EX 1020 1015 cases (bindIO_inversion ??????? EX) EX #m2 * #EX1 #EX 1021 1016 whd in EX:(??%%); destruct 1022 % [2: % [2: % [ % [ @ plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl  // ] /3/ ] skip ] skip ]1017 % [2: % [2: % [ % [ @cl_plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl  // ] /3/ ] skip ] skip ] 1023 1018 ] 1024 1019  *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O … … 1034 1029 state_with_labels s1 s1' → 1035 1030 (exec_step ge s1 = Value … 〈tr,s2〉 → 1036 ∃tr',s2'. plus ge' s1' tr' s2' ∧1031 ∃tr',s2'. plus … clight_exec ge' s1' tr' s2' ∧ 1037 1032 trace_with_extra_labels tr tr' ∧ 1038 1033 state_with_labels s2 s2'). … … 1048 1043 cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX) 1049 1044 #tr' * #s2' * * #P #T #S 1050 % [2: % [2: % [ % [ @ plus_succ [4: @refl  5: @P  *: skip ]  /2/ ] @S ] skip ] skip ]1045 % [2: % [2: % [ % [ @cl_plus_succ [4: @refl  5: @P  *: skip ]  /2/ ] @S ] skip ] skip ] 1051 1046 (* but for LScase it's just like the cases in step_with_labels_partial *) 1052 1047  #sz #i #s #ls #k #k' #e #m #K #EX … … 1055 1050 @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?); 1056 1051 whd in EX:(??%?); destruct 1057 % [2: % [2: % [ % [ @ plus_succ [4: @refl  5: @plus_one @refl  *: skip ]  /2/ ] /4/ ] skip ] skip ]1052 % [2: % [2: % [ % [ @cl_plus_succ [4: @refl  5: @cl_plus_one @refl  *: skip ]  /2/ ] /4/ ] skip ] skip ] 1058 1053 ] 1059 1054 ] qed. … … 1188 1183 1189 1184 1190 lemma not_wrong_init : ∀p.1191 not_wrong state (exec_inf … clight_fullexec p) →1192 ∃s. make_initial_state … p = OK ? s.1193 #p whd in ⊢ (??% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);1194 cases (make_initial_state p)1195 [ /2/1196  normalize #m #NW @⊥1197 inversion NW #H1 #H2 #H3 #H4 try #H5 destruct1198 ] qed.1199 1185 1200 1186 lemma final_related : ∀s1,s2. … … 1204 1190 [ #s1y #s2y * // 1205 1191  // 1206 ] qed.1207 1208 lemma plus_not_final : ∀ge,s,tr,s'.1209 plus ge s tr s' →1210 is_final s = None ?.1211 #ge #s0 #tr0 #s0' *1212 [ #s1 #tr #s2 #EX  #s1 #tr #s2 #tr' #s3 #EX #PL ]1213 lapply (refl ? (is_final s1))1214 cases (is_final s1) in ⊢ (???% → %);1215 //1216 #r cases s1 in EX ⊢ %;1217 #H9 #H10 #H11 try #H12 try #H13 try #H14 try #H151218 [ 1,5: whd in H15:(??%?);  2,6: whd in H14:(??%?);  3,7: whd in H13:(??%?);  4,8: whd in H11:(??%?); ]1219 destruct1220 normalize in H10;1221 destruct1222 qed.1223 1224 lemma plus_exec : ∀ge,s,tr,s'.1225 plus ge s tr s' →1226 is_final s' = None ? →1227 steps state tr1228 (exec_inf_aux … clight_fullexec ge (exec_step ge s))1229 (exec_inf_aux … clight_fullexec ge (exec_step ge s')).1230 #ge #s0 #tr0 #s0' #P elim P1231 [ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold1232 whd in ⊢ (???%?);1233 whd in match (is_final ?????); >NF1234 %21235  #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF1236 >exec_inf_aux_unfold >EX11237 whd in ⊢ (???%?);1238 whd in match (is_final ?????); >(plus_not_final … P2)1239 %3 @IH //1240 ] qed.1241 1242 lemma plus_exec_final : ∀ge,s,tr,s',r.1243 plus ge s tr s' →1244 is_final s' = Some ? r →1245 ∃tr'. steps state tr1246 (exec_inf_aux … clight_fullexec ge (exec_step ge s))1247 (e_stop … tr' r s').1248 #ge #s0 #tr0 #s0' #r #P elim P1249 [ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold1250 %{tr} whd in ⊢ (???%?);1251 whd in match (is_final ?????); >F1252 %11253  #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #F1254 cases (IH … F)1255 #tr' #S' %{tr'}1256 >exec_inf_aux_unfold >EX11257 whd in ⊢ (???%?);1258 whd in match (is_final ?????); >(plus_not_final … P2)1259 %3 @S'1260 1192 ] qed. 1261 1193 … … 1278 1210 #tr2 * #s2' * * #PL #TWL #S' 1279 1211 lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2 1280 cases (plus_ exec_final ?????PL F2)1212 cases (plus_final … clight_fullexec … PL F2) 1281 1213 #tr2' #S2 1282 1214 @(swl_stop … S2 TWL) … … 1286 1218 cases (step_with_labels … RG … S EX1) 1287 1219 #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*) 1288 @(swl_steps … (plus_exec … EX2 ?))1289 [ <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)1220 @(swl_steps … (plus_exec … clight_fullexec … EX2 ?)) 1221 [ whd in ⊢ (??%?); <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1) 1290 1222  // 1291 1223  (* Manual rewrite to prevent guardedness condition getting upset. *) … … 1330 1262 #p 1331 1263 #NW 1332 cases (not_wrong_init p NW)1333 #s1 #I11264 cases (not_wrong_init clight_fullexec p NW) 1265 whd in ⊢ (% → ??%? → ?); #s1 #I1 1334 1266 cases (initial_state_in_simulation … I1) 1335 1267 #s2 * #I2
Note: See TracChangeset
for help on using the changeset viewer.