Changeset 2428 for src/Clight/SimplifyCasts.ma
 Timestamp:
 Nov 6, 2012, 12:02:13 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/SimplifyCasts.ma
r2391 r2428 2331 2331 ] qed. 2332 2332 2333 lemma select_switch_commute : ∀sz,i,l. 2334 select_switch sz i (simplify_ls l) = simplify_ls (select_switch sz i l). 2335 #sz #i #l @(labeled_statements_ind … l) 2333 lemma select_switch_simplify_elim : ∀sz,i,l. ∀P:option labeled_statements → option labeled_statements → Prop. 2334 (P (None ?) (None ?)) → 2335 (∀l'. P (Some ? l') (Some ? (simplify_ls l'))) → 2336 P (select_switch sz i l) (select_switch sz i (simplify_ls l)). 2337 #sz #i #l #P #NONE #SOME @(labeled_statements_ind … l) 2336 2338 [ 1: #default_statement // 2337 2339  2: #sz' #i' #s #tl #Hind 2338 whd in match (simplify_ls ?) in ⊢ (??%?);2339 whd in match (select_switch ???) in ⊢ (??%%);2340 whd in match (simplify_ls ?); 2341 whd in match (select_switch ???); whd in match (select_switch ???); 2340 2342 cases (sz_eq_dec sz sz') 2341 2343 [ 1: #Hsz_eq destruct >intsize_eq_elim_true >intsize_eq_elim_true 2342 cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta 2343 whd in match (simplify_ls ?) in ⊢ (???%); 2344 [ 1: //  2: @Hind ] 2344 cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta // 2345 2345  2: #Hneq >(intsize_eq_elim_false ? sz sz' ???? Hneq) >(intsize_eq_elim_false ? sz sz' ???? Hneq) 2346 @ Hind2346 @NONE 2347 2347 ] 2348 2348 ] qed. … … 2931 2931 cases (\fst a) normalize nodelta 2932 2932 [ 1,3,4,5: #a destruct (a) #b destruct (b) 2933  2: #sz #i whd in match (ret ??) in ⊢ (% → %); #Heq destruct (Heq) 2933  2: #sz #i <Htype_eq_cond cases (typeof cond) 2934 [ 1,3,4,5,6,7,8,9: normalize nodelta #a try #b try #c destruct] 2935 #sz' #sg normalize nodelta cases (sz_eq_dec sz sz') 2936 #SZ [2: normalize nodelta #E destruct ] 2937 normalize nodelta @select_switch_simplify_elim 2938 [ #H whd in H:(??%?); destruct ] 2939 #l' whd in ⊢ (??%? → ??(λ_.?(??%?)?)); 2940 #Heq destruct (Heq) 2934 2941 %{(State (simplify_function f) 2935 (seq_of_labeled_statement (s elect_switch sz i (simplify_ls switchcases)))2942 (seq_of_labeled_statement (simplify_ls l')) 2936 2943 (Kswitch k') en m)} @conj 2937 2944 [ 1: // 2938  2: @(labeled_statements_ind … switchcases)2945  2: @(labeled_statements_ind … l') 2939 2946 [ 1: #default_s 2940 2947 whd in match (simplify_ls ?); … … 2943 2950 %1 @cc_switch // 2944 2951  2: #sz' #i' #top_case #tail #Hind 2945 cut ((seq_of_labeled_statement (select_switch sz i (simplify_ls (LScase sz' i' top_case tail)))) 2946 = (simplify_statement (seq_of_labeled_statement (select_switch sz i (LScase sz' i' top_case tail))))) 2947 [ 1: >select_switch_commute >simplify_ls_commute @refl 2948  2: #Hrewrite >Hrewrite 2949 %1 @cc_switch // 2950 ] ] ] ] ] ] 2952 <simplify_ls_commute 2953 %1 @cc_switch // 2954 ] ] ] ] ] 2951 2955  13: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 2952 2956 whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
Note: See TracChangeset
for help on using the changeset viewer.