Changeset 3403
- Timestamp:
- Dec 19, 2013, 6:42:35 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Language.ma
r3402 r3403 438 438 qed. 439 439 440 lemma get_element_append_l1 : 441 ∀A,B. ∀l1,l2: associative_list A B. ∀x. 442 ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l2)) → 443 get_element ?? (l1@l2) x = get_element … l1 x. 444 #A #B #l1 elim l1 normalize [2: #x #xs #IH #l2 #a #H >IH // ] 445 #l2 elim l2 // #y #ys #IH #a normalize cases(a == \fst y) normalize 446 [ * #H @⊥ @H % ] #H @IH assumption 447 qed. 448 440 449 definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝ 441 450 λx.〈a_non_functional_label x,S x〉. … … 752 761 qed. 753 762 763 lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A . 764 no_duplicates … (l1 @ l2) → x ∈ l1 → x ∈ l2 → False. 765 #A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???); 766 inversion (x == x1) normalize nodelta 767 [ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H % 768 | #_ @IH // 769 ] 770 qed. 771 772 773 lemma same_to_keep_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l. 774 no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → x ∈ dom1) → 775 (∀x.x ∈ l3 → x ∈ dom3) → 776 same_to_keep_on (dom1@dom2@dom3) (l1@l2@l3) l → 777 same_to_keep_on dom2 l2 l. 778 #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #sub_set1 #sub_set3 #H2 779 #x #Hx inversion (x ∈ l2) 780 [ #EQkeep <H2 [> memb_append_l2 // >memb_append_l1 // ] 781 >memb_append_l2 // >memb_append_l1 // >Hx // 782 | #EQno_keep <H2 783 [2: >memb_append_l2 // >memb_append_l1 // >Hx // 784 | @sym_eq @memb_not_append [2: @memb_not_append //] 785 [ <associative_append in no_dup; #no_dup ] 786 lapply(memb_no_duplicates_append … x … no_dup) #H 787 inversion(memb ???) // #H1 cases H 788 [1,4: [>memb_append_l2 | >memb_append_l1] // >Hx // 789 | @sub_set3 >H1 // 790 | @sub_set1 >H1 // 791 ] 792 ] 793 ] 794 qed. 795 796 lemma same_fresh_map_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l. 797 no_duplicates … (dom1 @dom2 @ dom3) → (∀x.x ∈ domain_of_associative_list … l1 → x ∈ dom1) → 798 (∀x.x ∈ domain_of_associative_list … l3 → x ∈ dom3) → 799 same_fresh_map_on … (dom1 @dom2 @dom3) (l1 @l2 @ l3) l → 800 same_fresh_map_on … dom2 l2 l. 801 #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #subset1 #subset3 whd in ⊢ (% → ?); #H1 802 whd #x #Hx <H1 803 [2: >memb_append_l2 // >memb_append_l1 // >Hx //] 804 >get_element_append_r [ >get_element_append_l1 // ] % #K 805 [ lapply(subset3 … K) | lapply(subset1 … K) ] #ABS 806 [ <associative_append in no_dup; #no_dup] @(memb_no_duplicates_append … x … no_dup) 807 // [>memb_append_l2 | >memb_append_l1 ] // >Hx // 808 qed. 809 810 754 811 lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p. 755 812 ∀x,n,l. … … 826 883 qed. 827 884 828 lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A . 829 no_duplicates … (l1 @ l2) → x ∈ l1 → x ∈ l2 → False. 830 #A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???); 831 inversion (x == x1) normalize nodelta 832 [ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H % 833 | #_ @IH // 834 ] 835 qed. 885 836 886 837 887 lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ. … … 868 918 #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); 869 919 #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%?); >IH3 // 870 [2: #x #Hx whd in H2; inversion(x ∈ lab_to_keep … (call_post_trans …)) 871 [ #EQkeep <H2 [ >memb_append_l2 // >memb_append_l2 // ] 872 whd in match (get_labels_of_code ??); @orb_Prop_r @orb_Prop_r >memb_append_l2 // 873 >memb_append_l2 // >Hx % 874 | #EQno_keep <H2 875 [2: whd in match (get_labels_of_code ??); @orb_Prop_r @orb_Prop_r 876 >memb_append_l2 // >memb_append_l2 // >Hx % ] @sym_eq @memb_not_append 877 [| @memb_not_append //] inversion(x ∈ lab_to_keep ??) // #Hlab @⊥ 878 lapply(lab_to_keep_in_domain ????? (eq_true_to_b … Hlab)) #ABS 879 cases no_dup #_ * #_ #ABS1 880 [ @(memb_no_duplicates_append … x … ABS1) // >memb_append_l2 // 881 | <associative_append in ABS1; #ABS1 882 @(memb_no_duplicates_append … x … ABS1) // >memb_append_l2 // >ABS % 920 [2: whd in match (get_labels_of_code ??) in H2; 921 change with ([?;?]@?) in match (?::?) in H2; 922 <associative_append in H2; <associative_append 923 <(append_nil … (?@?)) <associative_append in ⊢ (??%? → ?); 924 <(append_nil … (?@?)) in ⊢ (??%? → ?); >associative_append 925 >associative_append in ⊢ (??%? → ?); #H2 926 @(same_to_keep_on_append … H2) // [ >append_nil 927 whd in ⊢ (??%); whd in no_dup:(??%); >associative_append // ] 928 #x #Hx cases (memb_append … Hx) -Hx #Hx @orb_Prop_r @orb_Prop_r 929 [ >memb_append_l1 | >memb_append_l2 ] // 930 @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) 931 |3: -H2 whd in match (get_labels_of_code ??) in H1; 932 change with ([?;?]@?) in match (?::?) in H1; 933 <associative_append in H1; <associative_append 934 <(append_nil … (?@?)) >associative_append 935 change with ([?;?]@?) in match (?::?::?) in ⊢ (??%? → ?); 936 <associative_append in ⊢ (??%? → ?); 937 <associative_append in ⊢ (??%? → ?); 938 <(append_nil … (?@?)) in ⊢ (??%? → ?); 939 >associative_append in ⊢ (??%? → ?); #H1 940 @(same_fresh_map_on_append … H1) // 941 [ >append_nil >associative_append // ] 942 #x whd in match (memb ???); inversion(x == ltrue) 943 [ #Hltrue normalize nodelta #_ whd in match (memb ???); >Hltrue % 944 | #Hltrue normalize nodelta whd in match (memb ???); inversion(x == lfalse) 945 [ #Hlfalse #_ @orb_Prop_r @orb_Prop_l >Hlfalse % 946 | #Hlfalse normalize nodelta #Hx @orb_Prop_r @orb_Prop_r 947 >domain_of_associative_list_append in Hx; #H 948 cases(memb_append … H) #H2 [ >memb_append_l1 | >memb_append_l2 ] 949 // @(lab_map_in_domain … (eq_true_to_b … H2)) 883 950 ] 884 >Hx % 885 ] 886 |3: whd in H1; #x #Hx <H1 887 [2: >memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l2 // >Hx // ] 888 whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%); 889 >get_element_append_r [ >get_element_append_r // % #K lapply (lab_map_in_domain … K) 890 #K2 cases no_dup; #_ * #_ #no_dup3 891 @(memb_no_duplicates_append … x … (no_duplicates_append_r … no_dup3)) // ] 892 % #K lapply (lab_map_in_domain … K) #K2 cases no_dup; #_ * #_ #dup3 893 @(memb_no_duplicates_append … x … dup3) // >memb_append_l2 // >Hx // ] 894 cases no_dup #_ * #A1 #_ % #A2 <A2 in A1; * #K @K >memb_append_l2 // 895 >memb_append_l2 // @Hx ] cases no_dup #A1 #_ % #A2 <A2 in A1; * #K @K 896 >memb_cons // >memb_append_l2 // >memb_append_l2 // @Hx 951 ] 897 952 |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |] 898 953 ] 899 954 normalize nodelta >IH2 // 900 [2: #x #Hx <H2 901 [2: >memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l1 // >Hx // ] 902 whd in ⊢ (???%); >memb_append_l2 [2: >memb_append_l1] // 903 cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*) 904 |3: (*no duplicates ok *) cases daemon 955 [2: whd in match (get_labels_of_code ??) in H2; 956 change with ([?;?]@?) in match (?::?) in H2; 957 <associative_append in H2; #H2 958 @(same_to_keep_on_append … H2) // #x #Hx [ @orb_Prop_r @orb_Prop_r ] 959 @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) 960 |3: whd in match (get_labels_of_code ??) in H1; 961 change with ([?;?]@?) in match (?::?) in H1; 962 change with ([?;?]@?) in match (?::?::?) in H1 : (??%?); 963 <associative_append in H1; <associative_append in ⊢ (??%? → ?); #H1 964 @(same_fresh_map_on_append … H1) // [2: /2 by lab_map_in_domain/ ] 965 #x >domain_of_associative_list_append #H cases(memb_append … H) 966 [ whd in ⊢ (??%? → ?%); cases(x == ltrue) // normalize nodelta 967 whd in ⊢ (??%? → ?%); cases(x == lfalse) // normalize nodelta 968 normalize #EQ destruct 969 | #H1 @orb_Prop_r @orb_Prop_r 970 @(lab_map_in_domain … (eq_true_to_b … H1)) 971 ] 905 972 |4: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l 906 973 ] 907 974 >m_return_bind >IH1 // 908 [2: #x #Hx <H2 909 [2: >memb_cons // >memb_cons // >memb_append_l1 // @Hx ] 910 >memb_append_l1 911 cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*) 912 |3: cases daemon (*come sopra*) 975 [2: whd in match (get_labels_of_code ??) in H2; 976 change with ([?;?]@?) in match (?::?) in H2; 977 change with ([ ] @ ?) in match (lab_to_keep ??) in H2; 978 >associative_append in H2 : (??%?); #H2 979 @(same_to_keep_on_append … H2) // [ #x *] #x #Hx cases(memb_append … Hx) 980 -Hx #Hx [ >memb_append_l1 | >memb_append_l2] // 981 @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) 982 |3: whd in match (get_labels_of_code ??) in H1; 983 change with ([?;?]@?) in match (?::?) in H1; 984 change with ([?;?]@?) in match (?::?::?) in H1 : (??%?); 985 @(same_fresh_map_on_append … H1) // #x >domain_of_associative_list_append 986 #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2 ] 987 // @(lab_map_in_domain … (eq_true_to_b … Hx)) 913 988 |4: cases no_dup #_ * #_ @no_duplicates_append_l 914 989 ]
Note: See TracChangeset
for help on using the changeset viewer.