Changeset 2263 for src/Clight
 Timestamp:
 Jul 25, 2012, 6:55:36 PM (8 years ago)
 Location:
 src/Clight
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Csem.ma
r2177 r2263 327 327 let rec sem_cmp (c:comparison) 328 328 (v1: val) (t1: type) (v2: val) (t2: type) 329 (m: mem) : option val ≝329 (m: mem) on m: option val ≝ 330 330 match classify_cmp t1 t2 with 331 331 [ cmp_case_ii _ sg ⇒ 
src/Clight/switchRemoval.ma
r2255 r2263 2743 2743 ] qed. 2744 2744 2745 lemma monotonic_Zlt_Zsucc: monotonic Z Zlt Zsucc. 2746 whd #x #y #Hlt lapply (Zlt_to_Zle … Hlt) #Hle lapply (Zle_to_Zlt … Hle) 2747 /3 by monotonic_Zle_Zplus_r, Zle_to_Zlt/ qed. 2748 2749 lemma monotonic_Zlt_Zpred: monotonic Z Zlt Zpred. 2750 whd #x #y #Hlt lapply (Zlt_to_Zle … Hlt) #Hle lapply (Zle_to_Zlt … Hle) 2751 /3 by monotonic_Zle_Zpred, Zle_to_Zlt/ qed. 2752 2753 lemma antimonotonic_Zle_Zsucc: ∀x,y. Zsucc x ≤ Zsucc y → x ≤ y. 2754 #x #y #H lapply (monotonic_Zle_Zpred … H) >Zpred_Zsucc >Zpred_Zsucc #H @H 2755 qed. 2756 2757 (* 2758 lemma antimonotonic_Zle_Zpred: ∀x,y. Zpred x ≤ Zpred y → x ≤ y. 2759 #x #y #H lapply (monotonic_Zle_Zsucc … H) >Zsucc_Zpred >Zsucc_Zpred #H @H 2760 qed. *) 2761 2762 lemma antimonotonic_Zlt_Zsucc: ∀x,y. Zsucc x < Zsucc y → x < y. 2763 #x #y #Hlt lapply (Zle_to_Zlt … (antimonotonic_Zle_Zsucc … (Zlt_to_Zle … Hlt))) 2764 >Zpred_Zsucc #H @H 2765 qed. 2766 2767 lemma antimonotonic_Zlt_Zpred: ∀x,y. Zpred x < Zpred y → x < y. 2768 #x #y #Hlt lapply (monotonic_Zlt_Zsucc … Hlt) >Zsucc_Zpred >Zsucc_Zpred #H @H 2769 qed. 2770 2771 lemma not_Zlt_to_Zltb_false : ∀n,m. n ≮ m → Zltb n m = false. 2772 #n #m #Hnlt 2773 @Zltb_elim_Type0 2774 [ 1: elim Hnlt #H0 #H1 @(False_ind … (H0 H1)) 2775  2: #_ @refl ] qed. 2776 2745 2777 lemma Zplus_eq_eq : ∀x,y,delta:Z. eqZb x y = eqZb (x + delta) (y + delta). 2746 2778 #x #y #delta … … 2750 2782 [ 1: % #H cut (x = y) [ 1: @(injective_Zplus_l delta) @H ] #H' @Hneq @H' ] 2751 2783 #H @sym_eq @eqZb_false @H ] qed. 2784 2785 lemma Zltb_Zsucc : ∀x,y. Zltb x y = Zltb (Zsucc x) (Zsucc y). 2786 #x #y 2787 @(Zltb_elim_Type0 … x y) 2788 [ 1: #Hlt @sym_eq lapply (monotonic_Zlt_Zsucc … Hlt) #Hlt' @(Zlt_to_Zltb_true … Hlt') 2789  2: #Hnlt @sym_eq @not_Zlt_to_Zltb_false % #Hltsucc 2790 lapply (antimonotonic_Zlt_Zsucc … Hltsucc) #Hlt 2791 @(absurd … Hlt Hnlt) 2792 ] qed. 2793 2794 lemma Zltb_Zpred : ∀x,y. Zltb x y = Zltb (Zpred x) (Zpred y). 2795 #x #y 2796 @(Zltb_elim_Type0 … x y) 2797 [ 1: #Hlt @sym_eq 2798 lapply (monotonic_Zlt_Zpred … Hlt) #Hlt' @(Zlt_to_Zltb_true … Hlt') 2799  2: #Hnlt @sym_eq @not_Zlt_to_Zltb_false % #Hltsucc 2800 lapply (antimonotonic_Zlt_Zpred … Hltsucc) #Hlt 2801 @(absurd … Hlt Hnlt) 2802 ] qed. 2803 2804 lemma Zplus_pos_lt_lt : ∀x,y.∀delta. Zltb x y = Zltb (x + (pos delta)) (y + (pos delta)). 2805 #x #y #delta @(pos_elim … delta) 2806 [ 1: >(sym_Zplus x) >(sym_Zplus y) <Zsucc_Zplus_pos_O <Zsucc_Zplus_pos_O 2807 >Zltb_Zsucc @refl 2808  2: #n #Hind >Hind >Zltb_Zsucc 2809 >(sym_Zplus x) >(sym_Zplus y) 2810 <Zplus_Zsucc <Zplus_Zsucc 2811 >(sym_Zplus ? x) >(sym_Zplus ? y) 2812 normalize in match (Zsucc ?); @refl 2813 ] qed. 2814 2815 lemma Zplus_neg_lt_lt : ∀x,y.∀delta. Zltb x y = Zltb (x + (neg delta)) (y + (neg delta)). 2816 #x #y #delta @(pos_elim … delta) 2817 [ 1: >(sym_Zplus x) >(sym_Zplus y) <Zpred_Zplus_neg_O <Zpred_Zplus_neg_O 2818 >Zltb_Zpred @refl 2819  2: #n #Hind >Hind >Zltb_Zpred 2820 >(sym_Zplus x) >(sym_Zplus y) 2821 <Zplus_Zpred <Zplus_Zpred 2822 >(sym_Zplus ? x) >(sym_Zplus ? y) 2823 normalize in match (Zpred ?); @refl 2824 ] qed. 2825 2826 (* I would not be surprised for a simpler proof that mine to exist. *) 2827 lemma Zplus_lt_lt : ∀x,y,delta:Z. Zltb x y = Zltb (x + delta) (y + delta). 2828 #x #y #delta 2829 cases delta 2830 [ 1: >Zplus_z_OZ >Zplus_z_OZ @refl 2831  2: #p @Zplus_pos_lt_lt 2832  3: #p @Zplus_neg_lt_lt 2833 ] qed. 2752 2834 2753 2835 (* offset equality is invariant by translation *) … … 2760 2842 elim delta #zdelta @sym_eq <Zplus_eq_eq @refl qed. 2761 2843 2762 (* The key problem is that [sem_cmp] is a letrec defined on [op], but we /don't want/ to 2763 perform a caseanalysis on [op]. TODO: try and see if specifying another pseudodecreasing 2764 argument is ok. This just won't cut it.. *) 2765 lemma sem_cmp_value_eq : 2766 ∀E,v1,v2,v1',v2',ty,ty',m1,m2. 2767 value_eq E v1 v2 → 2768 value_eq E v1' v2' → 2769 memory_inj E m1 m2 → 2770 ∀op,r1. (sem_cmp op v1 ty v1' ty' m1 = Some val r1→ 2771 ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2). 2772 @cthulhu qed. 2773 2774 (* 2775 #E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1 2776 elim m1 in Hinj; #contents_map1 #nextblock1 #Hnextblock1 #Hinj 2777 cases op whd in match (sem_cmp ??????) in ⊢ (% → ?); 2778 cases (classify_cmp ty ty') normalize nodelta 2779 [ 1,9,17: #sz #sg 2780 @(value_eq_inversion E … Hvalue_eq1) normalize nodelta 2781 [ 1,6,11: #v #Habsurd destruct (Habsurd) 2782  2,7,12: #sz #i @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2783 [ 1,6,11: #v' #Habsurd destruct (Habsurd) 2784  2,7,12: #sz' #i' 2785  3,8,13: #f #Habsurd destruct (Habsurd) 2786  4,9,14: #Habsurd destruct (Habsurd) 2787  5,10,15: #p1 #p2 #Hembed destruct (Habsurd) ] 2788 2789  3,8,13: #f #Habsurd destruct (Habsurd) 2790  4,9,14: #Habsurd destruct (Habsurd) 2791  5,10,15: #p1 #p2 #Hembed destruct (Habsurd) ] 2792  2,10,18: #n #ty0  3,11,19: #fsz  4,12,20: #ty0 #ty0' #Habsurd destruct (Habsurd) ] 2793 [ 1,6,11,16,21,26,31,36,41,46,51,56,61,66,71,76,81,86,91,96: #v #Habsurd destruct (Habsurd) 2794  2,7,12,17,22,27,32,37,42,47,52,57,62,67,72,77,82,87,92,97: #sz' #i 2795 2796  2797  2,7,12: #sz #i  3,8,13: #f  4,9,14:  5,10,15: #p1 #p2 #Hembed ] 2798 *) 2799 2800 2801 (* The proof of the following lemma begs for factorization. *) 2802 (* 2803 lemma sem_cmp_value_eq : 2844 lemma cmp_offset_translation : ∀op,delta,x,y. 2845 cmp_offset op x y = cmp_offset op (offset_plus x delta) (offset_plus y delta). 2846 * #delta #x #y normalize 2847 elim delta #zdelta 2848 [ 1: @Zplus_eq_eq 2849  2: <Zplus_eq_eq @refl 2850  3: @Zplus_lt_lt 2851  4: <Zplus_lt_lt @refl 2852  5: @Zplus_lt_lt 2853  6: <Zplus_lt_lt @refl 2854 qed. 2855 2856 lemma cmp_value_eq : 2804 2857 ∀E,v1,v2,v1',v2',ty,ty',m1,m2. 2805 2858 value_eq E v1 v2 → … … 2809 2862 ∃r2:val.sem_cmp op v2 ty v2' ty' m2 = Some val r2∧value_eq E r1 r2). 2810 2863 #E #v1 #v2 #v1' #v2' #ty #ty' #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #op #r1 2811 cases op whd in match (sem_cmp ??????); whd in match (sem_cmp ??????); 2812 [ 1: (* Equality *) 2813 cases (classify_cmp ty ty') normalize nodelta 2814 [ 1: #sz #sg  2: #n #ty0  3: #fsz  4: #ty0 #ty0' #Habsurd destruct (Habsurd) ] 2815 @(value_eq_inversion E … Hvalue_eq1) 2816 [ 1,6,11: #v  2,7,12: #sz #i  3,8,13: #f  4,9,14:  5,10,15: #p1 #p2 #Hembed ] 2817 normalize nodelta 2818 [ 1,2,3,5,6,7,8,10,12,13,15: #Habsurd destruct (Habsurd) ] 2819 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2820 [ 1,6,11,16: #v'  2,7,12,17: #sz' #i'  3,8,13,18: #f'  4,9,14,19:  5,10,15,20: #p1' #p2' #Hembed' ] 2821 [ 5: elim sg normalize nodelta 2822 @intsize_eq_elim_elim 2823 [ 1,3: #_ #Habsurd destruct (Habsurd) 2824  2,4: #Heq destruct (Heq) normalize nodelta 2825 [ 1: cases (cmp_int ????) whd in match (of_bool ?); #Heq destruct (Heq) 2826  2: cases (cmpu_int ????) whd in match (of_bool ?); #Heq destruct (Heq) ] 2864 elim m1 in Hinj; #contmap1 #nextblock1 #Hnextblock1 elim m2 #contmap2 #nextblock2 #Hnextblock2 #Hinj 2865 whd in match (sem_cmp ??????) in ⊢ ((??%?) → %); 2866 cases (classify_cmp ty ty') normalize nodelta 2867 [ 1: #tsz #tsg 2868 @(value_eq_inversion E … Hvalue_eq1) normalize nodelta 2869 [ 1: #v #Habsurd destruct (Habsurd) 2870  3: #f #Habsurd destruct (Habsurd) 2871  4: #Habsurd destruct (Habsurd) 2872  5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 2873 #sz #i 2874 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2875 [ 1: #v #Habsurd destruct (Habsurd) 2876  3: #f #Habsurd destruct (Habsurd) 2877  4: #Habsurd destruct (Habsurd) 2878  5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 2879 #sz' #i' cases tsg normalize nodelta 2880 @intsize_eq_elim_elim 2881 [ 1,3: #Hneq #Habsurd destruct (Habsurd) 2882  2,4: #Heq destruct (Heq) normalize nodelta 2883 #Heq destruct (Heq) 2884 [ 1: cases (cmp_int ????) whd in match (of_bool ?); 2885  2: cases (cmpu_int ????) whd in match (of_bool ?); ] 2827 2886 /3 by ex_intro, conj, vint_eq/ ] 2828  10: #Heq destruct (Heq) cases (Fcmp Ceq f f') /3 by ex_intro, conj, vint_eq/ 2829  15: whd in match (sem_cmp_match ?); #Heq destruct (Heq) 2830 /3 by ex_intro, conj, vint_eq/ 2831  16,19: whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq) 2832 /3 by ex_intro, conj, vint_eq/ 2833  20: lapply (mi_valid_pointers … Hinj p1' p2') 2834 lapply (mi_valid_pointers … Hinj p1 p2) 2835 cases (valid_pointer m1 p1') 2836 [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 2837 cases (valid_pointer m1 p1) 2838 [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 2839 #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2 2840 >Hvalid1 >Hvalid2 normalize nodelta H1 H2 2841 elim p1 in Hembed; #b1 #o1 2842 elim p1' in Hembed'; #b1' #o1' 2843 whd in match (pointer_translation ??); 2844 whd in match (pointer_translation ??); 2845 @(eq_block_elim … b1 b1') 2846 [ 1: #Heq destruct (Heq) 2847 cases (E b1') 2848 [ 1: normalize nodelta #Habsurd destruct (Habsurd) ] 2849 * #eb1' #eo1' normalize nodelta 2850 #Heq1 #Heq2 #Heq3 destruct 2851 >eq_block_identity normalize nodelta 2852 >eq_offset_translation cases (cmp_offset ???) 2853 /3 by ex_intro, conj, vint_eq/ 2854  2: #Hneq lapply (mi_disjoint … Hinj b1 b1') 2855 cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2856 * #eb1 #eo1 2857 cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ] 2858 * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct 2859 lapply (H ???? Hneq (refl ??) (refl ??)) 2860 #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta 2861 #Heq destruct (Heq) whd in match (sem_cmp_mismatch Ceq); 2862 %{Vfalse} @conj try @refl normalize in Heq; destruct (Heq) 2863 @vint_eq ] 2864  *: #Habsurd destruct (Habsurd) ] 2865  2: (* Inequality *) 2866 cases (classify_cmp ty ty') normalize nodelta 2867 [ 1: #sz #sg  2: #n #ty0  3: #fsz  4: #ty0 #ty0' #Habsurd destruct (Habsurd) ] 2868 @(value_eq_inversion E … Hvalue_eq1) 2869 [ 1,6,11: #v  2,7,12: #sz #i  3,8,13: #f  4,9,14:  5,10,15: #p1 #p2 #Hembed ] 2870 normalize nodelta 2871 [ 1,2,3,5,6,7,8,10,12,13,15: #Habsurd destruct (Habsurd) ] 2872 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2873 [ 1,6,11,16: #v'  2,7,12,17: #sz' #i'  3,8,13,18: #f'  4,9,14,19:  5,10,15,20: #p1' #p2' #Hembed' ] 2874 [ 5: cases sg normalize nodelta 2875 @intsize_eq_elim_elim 2876 [ 1,3: #_ #Habsurd destruct (Habsurd) 2877  2,4: #Heq destruct (Heq) normalize nodelta 2878 [ 1: cases (cmp_int ????) whd in match (of_bool ?); #Heq destruct (Heq) 2879  2: cases (cmpu_int ????) whd in match (of_bool ?); #Heq destruct (Heq) ] 2880 /3 by ex_intro, conj, vint_eq/ ] 2881  10: #Heq destruct (Heq) cases (Fcmp Cne f f') /3 by ex_intro, conj, vint_eq/ 2882  15: whd in match (sem_cmp_match ?) in ⊢ (% → %); #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/ 2883  16,19: whd in match (sem_cmp_mismatch ?) in ⊢ (% → %); #Heq destruct (Heq) /3 by ex_intro, conj, vint_eq/ 2884  20: lapply (mi_valid_pointers … Hinj p1' p2') 2885 lapply (mi_valid_pointers … Hinj p1 p2) 2886 cases (valid_pointer m1 p1') 2887 [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 2888 cases (valid_pointer m1 p1) 2889 [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 2890 #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2 2891 >Hvalid1 >Hvalid2 normalize nodelta H1 H2 2892 elim p1 in Hembed; #b1 #o1 2893 elim p1' in Hembed'; #b1' #o1' 2894 whd in match (pointer_translation ??); 2895 whd in match (pointer_translation ??); 2896 @(eq_block_elim … b1 b1') 2897 [ 1: #Heq destruct (Heq) 2898 cases (E b1') 2899 [ 1: normalize nodelta #Habsurd destruct (Habsurd) ] 2900 * #eb1' #eo1' normalize nodelta 2901 #Heq1 #Heq2 #Heq3 destruct 2902 >eq_block_identity normalize nodelta 2903 >neq_offset_translation cases (cmp_offset ???) 2904 /3 by ex_intro, conj, vint_eq/ 2905  2: #Hneq lapply (mi_disjoint … Hinj b1 b1') 2906 cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2907 * #eb1 #eo1 2908 cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ] 2909 * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct 2910 lapply (H ???? Hneq (refl ??) (refl ??)) 2911 #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta 2912 #Heq destruct (Heq) whd in match (sem_cmp_mismatch Cne); 2913 %{Vtrue} @conj try @refl normalize in Heq; destruct (Heq) 2914 @vint_eq ] 2915  *: #Habsurd destruct (Habsurd) ] 2916  3: (* Lessthan *) 2917 2918  3: *: @cthulhu ] 2919 qed.*) 2887  3: #fsz 2888 @(value_eq_inversion E … Hvalue_eq1) normalize nodelta 2889 [ 1: #v #Habsurd destruct (Habsurd) 2890  2: #sz #i #Habsurd destruct (Habsurd) 2891  4: #Habsurd destruct (Habsurd) 2892  5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 2893 #f 2894 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2895 [ 1: #v #Habsurd destruct (Habsurd) 2896  2: #sz #i #Habsurd destruct (Habsurd) 2897  4: #Habsurd destruct (Habsurd) 2898  5: #p1 #p2 #Hembed #Habsurd destruct (Habsurd) ] 2899 #f' 2900 #Heq destruct (Heq) cases (Fcmp op f f') 2901 /3 by ex_intro, conj, vint_eq/ 2902  4: #ty1 #ty2 #Habsurd destruct (Habsurd) 2903  2: #optn #typ 2904 @(value_eq_inversion E … Hvalue_eq1) normalize nodelta 2905 [ 1: #v #Habsurd destruct (Habsurd) 2906  2: #sz #i #Habsurd destruct (Habsurd) 2907  3: #f #Habsurd destruct (Habsurd) 2908  5: #p1 #p2 #Hembed ] 2909 @(value_eq_inversion E … Hvalue_eq2) normalize nodelta 2910 [ 1,6: #v #Habsurd destruct (Habsurd) 2911  2,7: #sz #i #Habsurd destruct (Habsurd) 2912  3,8: #f #Habsurd destruct (Habsurd) 2913  5,10: #p1' #p2' #Hembed' ] 2914 [ 2,3: cases op whd in match (sem_cmp_mismatch ?); 2915 #Heq destruct (Heq) 2916 [ 1,3: %{Vfalse} @conj try @refl @vint_eq 2917  2,4: %{Vtrue} @conj try @refl @vint_eq ] 2918  4: cases op whd in match (sem_cmp_match ?); 2919 #Heq destruct (Heq) 2920 [ 2,4: %{Vfalse} @conj try @refl @vint_eq 2921  1,3: %{Vtrue} @conj try @refl @vint_eq ] ] 2922 lapply (mi_valid_pointers … Hinj p1' p2') 2923 lapply (mi_valid_pointers … Hinj p1 p2) 2924 cases (valid_pointer (mk_mem ???) p1') 2925 [ 2: #_ #_ >commutative_andb normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 2926 cases (valid_pointer (mk_mem ???) p1) 2927 [ 2: #_ #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ] 2928 #H1 #H2 lapply (H1 (refl ??) Hembed) #Hvalid1 lapply (H2 (refl ??) Hembed') #Hvalid2 2929 >Hvalid1 >Hvalid2 normalize nodelta H1 H2 2930 elim p1 in Hembed; #b1 #o1 2931 elim p1' in Hembed'; #b1' #o1' 2932 whd in match (pointer_translation ??); 2933 whd in match (pointer_translation ??); 2934 @(eq_block_elim … b1 b1') 2935 [ 1: #Heq destruct (Heq) 2936 cases (E b1') normalize nodelta 2937 [ 1: #Habsurd destruct (Habsurd) ] 2938 * #eb1' #eo1' normalize nodelta 2939 #Heq1 #Heq2 #Heq3 destruct 2940 >eq_block_identity normalize nodelta 2941 <cmp_offset_translation 2942 cases (cmp_offset ???) normalize nodelta 2943 /3 by ex_intro, conj, vint_eq/ 2944  2: #Hneq lapply (mi_disjoint … Hinj b1 b1') 2945 cases (E b1') [ 1: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2946 * #eb1 #eo1 2947 cases (E b1) [ 1: #_ normalize nodelta #_ #Habsurd destruct (Habsurd) ] 2948 * #eb1' #eo1' normalize nodelta #H #Heq1 #Heq2 destruct 2949 lapply (H ???? Hneq (refl ??) (refl ??)) 2950 #Hneq_block >(neq_block_eq_block_false … Hneq_block) normalize nodelta 2951 elim op whd in match (sem_cmp_mismatch ?); #Heq destruct (Heq) 2952 /3 by ex_intro, conj, vint_eq/ 2953 ] 2954 ] qed. 2920 2955 2921 2956 (* Commutation result for binary operators. *) … … 2932 2967 whd in match (sem_binary_operation ??????); 2933 2968 whd in match (sem_binary_operation ??????); 2934 @cthulhu 2935 qed. 2969 [ 1: @add_value_eq try assumption 2970  2: @sub_value_eq try assumption 2971  3: @mul_value_eq try assumption 2972  4: @div_value_eq try assumption 2973  5: @mod_value_eq try assumption 2974  6: @and_value_eq try assumption 2975  7: @or_value_eq try assumption 2976  8: @xor_value_eq try assumption 2977  9: @shl_value_eq try assumption 2978  10: @shr_value_eq try assumption 2979  *: @cmp_value_eq try assumption 2980 ] qed. 2936 2981 2937 2982 … … 3039 3084  2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq 3040 3085 normalize /2/ ] 3086  8: #ty #op #e1 #e2 #Hsim1 #Hsim2 3087 @(exec_expr_expr_elim … Hsim1) #v1 #v2 #trace #Hvalue_eq 3088 cases (exec_expr ge en1 m1 e2) in Hsim2; 3089 [ 2: #error // ] 3090 * #val #trace normalize in ⊢ (% → ?); #Hsim2 3091 elim (Hsim2 ? (refl ??)) * #val2 #trace2 * #Hexec2 * #Hvalue_eq2 #Htrace >Hexec2 3092 whd in match (m_bind ?????); whd in match (m_bind ?????); 3093 lapply (binary_operation_value_eq E op … (typeof e1) (typeof e2) ?? Hvalue_eq Hvalue_eq2 (me_inj … Hext)) 3094 cases (sem_binary_operation op v1 (typeof e1) val (typeof e2) m1) 3095 [ 1: #_ // ] 3096 #opval #Hop elim (Hop ? (refl ??)) #opval' * #Hopval_eq #Hvalue_eq_opval 3097 >Hopval_eq normalize destruct /2 by conj/ 3098  9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim) 3099 #v1 #v2 #trace #Hvalue_eq (* TODO ... *) @cthulhu 3041 3100  *: @cthulhu ] qed. 3042 3101
Note: See TracChangeset
for help on using the changeset viewer.