Changeset 2588 for src/Clight/frontend_misc.ma
 Timestamp:
 Jan 23, 2013, 2:38:06 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2582 r2588 666 666 qed. 667 667 668 lemma zero_ext_same_size : ∀n,v. zero_ext n n v = v. 669 #n #v whd in match (zero_ext ???); >nat_compare_eq @refl 670 qed. 671 668 672 axiom sign_ext_zero : ∀sz1,sz2. sign_ext sz1 sz2 (zero sz1) = zero sz2. 669 673 670 674 axiom zero_ext_zero : ∀sz1,sz2. zero_ext sz1 sz2 (zero sz1) = zero sz2. 675 676 (* notice that we restrict source and target sizes to be ≠ 0 *) 677 axiom zero_ext_one : ∀sz1,sz2. zero_ext (bitsize_of_intsize sz1) (bitsize_of_intsize sz2) (repr sz1 1) = (repr sz2 1). 671 678 672 679 axiom multiplication_zero : ∀n:nat. ∀v : BitVector n. multiplication … (zero ?) v = (zero ?). … … 2435 2442 qed. 2436 2443 2444 (*  *) 2445 (* Inversion principles for binary operations *) 2446 (*  *) 2447 2448 lemma sem_add_ip_inversion : 2449 ∀sz,sg,ty',optlen. 2450 ∀v1,v2,res. 2451 sem_add v1 (Tint sz sg) v2 (ptr_type ty' optlen) = Some ? res → 2452 ∃sz',i. v1 = Vint sz' i ∧ 2453 ((∃p. v2 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨ 2454 (v2 = Vnull ∧ i = (zero ?) ∧ res = Vnull)). 2455 #tsz #tsg #ty' * [  #n ] 2456 * 2457 [  #sz' #i'   #p' 2458   #sz' #i'   #p' ] 2459 #v2 #res 2460 whd in ⊢ ((??%?) → ?); 2461 #H destruct 2462 cases v2 in H; 2463 [  #sz2' #i2'   #p2' 2464   #sz2' #i2'   #p2' ] normalize nodelta 2465 #H destruct 2466 [ 1,3: 2467 lapply H H 2468 @(eq_bv_elim … i' (zero ?)) normalize nodelta 2469 #Hi #Heq destruct (Heq) 2470 %{sz'} %{(zero ?)} @conj destruct try @refl 2471 %2 @conj try @conj try @refl 2472  *: %{sz'} %{i'} @conj try @refl 2473 %1 %{p2'} @conj try @refl 2474 ] qed. 2475 2476 (* symmetric of the upper one *) 2477 lemma sem_add_pi_inversion : 2478 ∀sz,sg,ty',optlen. 2479 ∀v1,v2,res. 2480 sem_add v1 (ptr_type ty' optlen) v2 (Tint sz sg) = Some ? res → 2481 ∃sz',i. v2 = Vint sz' i ∧ 2482 ((∃p. v1 = Vptr p ∧ res = Vptr (shift_pointer_n ? p (sizeof ty') sg i)) ∨ 2483 (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)). 2484 #tsz #tsg #ty' * [  #n ] 2485 * 2486 [  #sz' #i'   #p' 2487   #sz' #i'   #p' ] 2488 #v2 #res 2489 whd in ⊢ ((??%?) → ?); 2490 #H destruct 2491 cases v2 in H; normalize nodelta 2492 [  #sz2' #i2'   #p2'   #sz2' #i2'   #p2'   #sz2' #i2'   #p2'   #sz2' #i2'   #p2' ] 2493 #H destruct 2494 [ 2,4: %{sz2'} %{i2'} @conj try @refl %1 2495 %{p'} @conj try @refl 2496  *: lapply H H 2497 @(eq_bv_elim … i2' (zero ?)) normalize nodelta 2498 #Hi #Heq destruct (Heq) 2499 %{sz2'} %{(zero ?)} @conj destruct try @refl 2500 %2 @conj try @conj try @refl 2501 ] qed. 2502 2503 (* Know that addition on integers gives an integer. Notice that there is no correlation 2504 between the size in the types and the size of the integer values. *) 2505 lemma sem_add_ii_inversion : 2506 ∀sz,sg. 2507 ∀v1,v2,res. 2508 sem_add v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res → 2509 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 2510 res = Vint sz' (addition_n (bitsize_of_intsize sz') i1 i2). 2511 #sz #sg 2512 * 2513 [  #sz' #i'   #p' ] 2514 #v2 #res 2515 whd in ⊢ ((??%?) → ?); normalize in match (classify_add ??); 2516 cases sz cases sg normalize nodelta 2517 #H destruct 2518 cases v2 in H; normalize nodelta 2519 #H1 destruct 2520 #H2 destruct #Heq %{sz'} lapply Heq Heq 2521 cases sz' in i'; #i' 2522 whd in match (intsize_eq_elim ???????); 2523 cases H1 in H2; #j' normalize nodelta 2524 #Heq destruct (Heq) 2525 %{i'} %{j'} @conj try @conj try @conj try @refl 2526 qed. 2527 2528 lemma sem_sub_pp_inversion : 2529 ∀ty1,ty2,n1,n2,target. 2530 ∀v1,v2,res. 2531 sem_sub v1 (ptr_type ty1 n1) v2 (ptr_type ty2 n2) target = Some ? res → 2532 ∃sz,sg. 2533 target = Tint sz sg ∧ 2534 ((∃p1,p2,i. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧ pblock p1 = pblock p2 ∧ 2535 division_u ? (sub_offset ? (poff p1) (poff p2)) (repr (sizeof ty1)) = Some ? i ∧ 2536 res = Vint sz (zero_ext ?? i)) ∨ 2537 (v1 = Vnull ∧ v2 = Vnull ∧ res = Vint sz (zero ?))). 2538 #ty1 #ty2 #n1 #n2 #target 2539 cut (classify_sub (ptr_type ty1 n1) (ptr_type ty2 n2) = 2540 sub_case_pp n1 n2 ty1 ty2) 2541 [ cases n1 cases n2 2542 [  #n1  #n2  #n2 #n1 ] try @refl ] 2543 #Hclassify 2544 * 2545 [  #sz #i   #p ] 2546 #v2 #res 2547 whd in ⊢ ((??%?) → ?); normalize nodelta 2548 #H1 destruct 2549 lapply H1 H1 2550 >Hclassify normalize nodelta 2551 [ 1,2: #H destruct ] 2552 cases v2 normalize nodelta 2553 [  #sz' #i'   #p' 2554   #sz' #i'   #p' ] 2555 #H2 destruct 2556 cases target in H2; 2557 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain  #structname #fieldspec  #unionname #fieldspec  #id 2558   #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain  #structname #fieldspec  #unionname #fieldspec  #id ] 2559 normalize nodelta 2560 #H destruct 2561 [ 2,4,5,6,7,8,9: 2562 cases (eq_block (pblock p) (pblock p')) in H; 2563 normalize nodelta #H destruct 2564 cases (eqb (sizeof ty1) O) in H; 2565 normalize nodelta #H destruct ] 2566 %{sz} %{sg} @conj try @refl 2567 try /4 by or_introl, or_intror, conj, refl/ 2568 cases (if_opt_inversion ???? H) 2569 #Hblocks_eq H 2570 @(eqb_elim … (sizeof ty1) 0) normalize nodelta 2571 [ #Heq_sizeof #Habsurd destruct ] 2572 #_ #Hdiv 2573 %1 %{p} %{p'} 2574 cases (division_u ???) in Hdiv; normalize nodelta 2575 [ #Habsurd destruct ] #i #Heq destruct 2576 %{i} try @conj try @conj try @conj try @conj try @refl 2577 try @(eq_block_to_refl … Hblocks_eq) 2578 qed. 2579 2580 lemma sem_sub_pi_inversion : 2581 ∀sz,sg,ty',optlen,target. 2582 ∀v1,v2,res. 2583 sem_sub v1 (ptr_type ty' optlen) v2 (Tint sz sg) target = Some ? res → 2584 ∃sz',i. v2 = Vint sz' i ∧ 2585 ((∃p. v1 = Vptr p ∧ res = Vptr (neg_shift_pointer_n ? p (sizeof ty') sg i)) ∨ 2586 (v1 = Vnull ∧ i = (zero ?) ∧ res = Vnull)). 2587 #tsz #tsg #ty' * [  #n ] #target 2588 * 2589 [  #sz' #i'   #p' 2590   #sz' #i'   #p' ] 2591 #v2 #res 2592 whd in ⊢ ((??%?) → ?); 2593 #H destruct 2594 cases v2 in H; normalize nodelta 2595 [  #sz2' #i2'   #p2'   #sz2' #i2'   #p2'   #sz2' #i2'   #p2'   #sz2' #i2'   #p2' ] 2596 #H destruct 2597 [ 2,4: %{sz2'} %{i2'} @conj try @refl %1 2598 %{p'} @conj try @refl 2599  *: lapply H H 2600 @(eq_bv_elim … i2' (zero ?)) normalize nodelta 2601 #Hi #Heq destruct (Heq) 2602 %{sz2'} %{(zero ?)} @conj destruct try @refl 2603 %2 @conj try @conj try @refl 2604 ] qed. 2605 2606 lemma sem_sub_ii_inversion : 2607 ∀sz,sg,ty. 2608 ∀v1,v2,res. 2609 sem_sub v1 (Tint sz sg) v2 (Tint sz sg) ty = Some ? res → 2610 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 2611 res = Vint sz' (subtraction (bitsize_of_intsize sz') i1 i2). 2612 #sz #sg #ty * 2613 [  #sz' #i'   #p' ] 2614 #v2 #res 2615 whd in ⊢ ((??%?) → ?); whd in match (classify_sub ??); 2616 cases sz cases sg normalize nodelta 2617 #H destruct 2618 cases v2 in H; normalize nodelta 2619 #H1 destruct 2620 #H2 destruct #Heq %{sz'} lapply Heq Heq 2621 cases sz' in i'; #i' 2622 whd in match (intsize_eq_elim ???????); 2623 cases H1 in H2; #j' normalize nodelta 2624 #Heq destruct (Heq) 2625 %{i'} %{j'} @conj try @conj try @conj try @refl 2626 qed. 2627 2628 2629 lemma sem_mul_inversion : 2630 ∀sz,sg. 2631 ∀v1,v2,res. 2632 sem_mul v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res → 2633 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 2634 res = Vint sz' (short_multiplication ? i1 i2). 2635 #sz #sg * 2636 [  #sz' #i'   #p' ] 2637 #v2 #res 2638 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??); 2639 cases sz cases sg normalize nodelta 2640 #H destruct 2641 cases v2 in H; normalize nodelta 2642 #H1 destruct 2643 #H2 destruct #Heq %{sz'} lapply Heq Heq 2644 cases sz' in i'; #i' 2645 whd in match (intsize_eq_elim ???????); 2646 cases H1 in H2; #j' normalize nodelta 2647 #Heq destruct (Heq) 2648 %{i'} %{j'} @conj try @conj try @conj try @refl 2649 qed. 2650 2651 2652 lemma sem_div_inversion_s : 2653 ∀sz. 2654 ∀v1,v2,res. 2655 sem_div v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res → 2656 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 2657 match division_s ? i1 i2 with 2658 [ Some q ⇒ res = (Vint sz' q) 2659  None ⇒ False ]. 2660 #sz * 2661 [  #sz' #i'   #p' ] 2662 #v2 #res 2663 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??); 2664 >type_eq_dec_true normalize nodelta 2665 #H destruct 2666 cases v2 in H; normalize nodelta 2667 [  #sz2' #i2'   #p2' ] 2668 #Heq destruct 2669 %{sz'} 2670 lapply Heq Heq 2671 cases sz' in i'; #i' 2672 whd in match (intsize_eq_elim ???????); 2673 cases sz2' in i2'; #i2' normalize nodelta 2674 whd in match (option_map ????); #Hdiv destruct 2675 %{i'} %{i2'} @conj try @conj try @conj try @refl 2676 cases (division_s ???) in Hdiv; 2677 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl 2678 qed. 2679 2680 lemma sem_div_inversion_u : 2681 ∀sz. 2682 ∀v1,v2,res. 2683 sem_div v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res → 2684 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 2685 match division_u ? i1 i2 with 2686 [ Some q ⇒ res = (Vint sz' q) 2687  None ⇒ False ]. 2688 #sz * 2689 [  #sz' #i'   #p' ] 2690 #v2 #res 2691 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??); 2692 >type_eq_dec_true normalize nodelta 2693 #H destruct 2694 cases v2 in H; normalize nodelta 2695 [  #sz2' #i2'   #p2' ] 2696 #Heq destruct 2697 %{sz'} 2698 lapply Heq Heq 2699 cases sz' in i'; #i' 2700 whd in match (intsize_eq_elim ???????); 2701 cases sz2' in i2'; #i2' normalize nodelta 2702 whd in match (option_map ????); #Hdiv destruct 2703 %{i'} %{i2'} @conj try @conj try @conj try @refl 2704 cases (division_u ???) in Hdiv; 2705 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl 2706 qed. 2707 2708 lemma sem_mod_inversion_s : 2709 ∀sz. 2710 ∀v1,v2,res. 2711 sem_mod v1 (Tint sz Signed) v2 (Tint sz Signed) = Some ? res → 2712 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 2713 match modulus_s ? i1 i2 with 2714 [ Some q ⇒ res = (Vint sz' q) 2715  None ⇒ False ]. 2716 #sz * 2717 [  #sz' #i'   #p' ] 2718 #v2 #res 2719 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??); 2720 >type_eq_dec_true normalize nodelta 2721 #H destruct 2722 cases v2 in H; normalize nodelta 2723 [  #sz2' #i2'   #p2' ] 2724 #Heq destruct 2725 %{sz'} 2726 lapply Heq Heq 2727 cases sz' in i'; #i' 2728 whd in match (intsize_eq_elim ???????); 2729 cases sz2' in i2'; #i2' normalize nodelta 2730 whd in match (option_map ????); #Hdiv destruct 2731 %{i'} %{i2'} @conj try @conj try @conj try @refl 2732 cases (modulus_s ???) in Hdiv; 2733 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl 2734 qed. 2735 2736 lemma sem_mod_inversion_u : 2737 ∀sz. 2738 ∀v1,v2,res. 2739 sem_mod v1 (Tint sz Unsigned) v2 (Tint sz Unsigned) = Some ? res → 2740 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 2741 match modulus_u ? i1 i2 with 2742 [ Some q ⇒ res = (Vint sz' q) 2743  None ⇒ False ]. 2744 #sz * 2745 [  #sz' #i'   #p' ] 2746 #v2 #res 2747 whd in ⊢ ((??%?) → ?); whd in match (classify_aop ??); 2748 >type_eq_dec_true normalize nodelta 2749 #H destruct 2750 cases v2 in H; normalize nodelta 2751 [  #sz2' #i2'   #p2' ] 2752 #Heq destruct 2753 %{sz'} 2754 lapply Heq Heq 2755 cases sz' in i'; #i' 2756 whd in match (intsize_eq_elim ???????); 2757 cases sz2' in i2'; #i2' normalize nodelta 2758 whd in match (option_map ????); #Hdiv destruct 2759 %{i'} %{i2'} @conj try @conj try @conj try @refl 2760 cases (modulus_u ???) in Hdiv; 2761 [ 2,4,6: #bv ] normalize #H destruct (H) try @refl 2762 qed. 2763 2764 lemma sem_and_inversion : 2765 ∀v1,v2,res. 2766 sem_and v1 v2 = Some ? res → 2767 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 2768 res = Vint sz' (conjunction_bv ? i1 i2). 2769 * 2770 [  #sz' #i'   #p' ] 2771 #v2 #res 2772 whd in ⊢ ((??%?) → ?); 2773 #H destruct 2774 cases v2 in H; normalize nodelta 2775 [  #sz2' #i2'   #p2' ] 2776 #Heq destruct 2777 %{sz'} 2778 lapply Heq Heq 2779 cases sz' in i'; #i' 2780 whd in match (intsize_eq_elim ???????); 2781 cases sz2' in i2'; #i2' normalize nodelta 2782 #H destruct 2783 %{i'} %{i2'} @conj try @conj try @conj try @refl 2784 qed. 2785 2786 lemma sem_or_inversion : 2787 ∀v1,v2,res. 2788 sem_or v1 v2 = Some ? res → 2789 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 2790 res = Vint sz' (inclusive_disjunction_bv ? i1 i2). 2791 * 2792 [  #sz' #i'   #p' ] 2793 #v2 #res 2794 whd in ⊢ ((??%?) → ?); 2795 #H destruct 2796 cases v2 in H; normalize nodelta 2797 [  #sz2' #i2'   #p2' ] 2798 #Heq destruct 2799 %{sz'} 2800 lapply Heq Heq 2801 cases sz' in i'; #i' 2802 whd in match (intsize_eq_elim ???????); 2803 cases sz2' in i2'; #i2' normalize nodelta 2804 #H destruct 2805 %{i'} %{i2'} @conj try @conj try @conj try @refl 2806 qed. 2807 2808 lemma sem_xor_inversion : 2809 ∀v1,v2,res. 2810 sem_xor v1 v2 = Some ? res → 2811 ∃sz',i1,i2. v1 = Vint sz' i1 ∧ v2 = Vint sz' i2 ∧ 2812 res = Vint sz' (exclusive_disjunction_bv ? i1 i2). 2813 * 2814 [  #sz' #i'   #p' ] 2815 #v2 #res 2816 whd in ⊢ ((??%?) → ?); 2817 #H destruct 2818 cases v2 in H; normalize nodelta 2819 [  #sz2' #i2'   #p2' ] 2820 #Heq destruct 2821 %{sz'} 2822 lapply Heq Heq 2823 cases sz' in i'; #i' 2824 whd in match (intsize_eq_elim ???????); 2825 cases sz2' in i2'; #i2' normalize nodelta 2826 #H destruct 2827 %{i'} %{i2'} @conj try @conj try @conj try @refl 2828 qed. 2829 2830 lemma sem_shl_inversion : 2831 ∀v1,v2,res. 2832 sem_shl v1 v2 = Some ? res → 2833 ∃sz1,sz2,i1,i2. 2834 v1 = Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧ 2835 res = Vint sz1 (shift_left bool (bitsize_of_intsize sz1) 2836 (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false) ∧ 2837 lt_u (bitsize_of_intsize sz2) i2 2838 (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true. 2839 * 2840 [  #sz' #i'   #p' ] 2841 #v2 #res 2842 whd in ⊢ ((??%?) → ?); 2843 #H destruct 2844 cases v2 in H; normalize nodelta 2845 [  #sz2' #i2'   #p2' ] 2846 #Heq destruct 2847 %{sz'} %{sz2'} 2848 lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres 2849 %{i'} %{i2'} 2850 >Hlt_u destruct (Hres) @conj try @conj try @conj try @refl 2851 qed. 2852 2853 lemma sem_shr_inversion : 2854 ∀v1,v2,sz,sg,res. 2855 sem_shr v1 (Tint sz sg) v2 (Tint sz sg) = Some ? res → 2856 ∃sz1,sz2,i1,i2. 2857 v1 = Vint sz1 i1 ∧ v2 = Vint sz2 i2 ∧ 2858 lt_u (bitsize_of_intsize sz2) i2 2859 (bitvector_of_nat (bitsize_of_intsize sz2) (bitsize_of_intsize sz1)) = true ∧ 2860 match sg with 2861 [ Signed ⇒ 2862 res = 2863 (Vint sz1 2864 (shift_right bool (7+pred_size_intsize sz1*8) 2865 (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 2866 (head' bool (7+pred_size_intsize sz1*8) i1))) 2867  Unsigned ⇒ 2868 res = 2869 (Vint sz1 2870 (shift_right bool (7+pred_size_intsize sz1*8) 2871 (nat_of_bitvector (bitsize_of_intsize sz2) i2) i1 false)) 2872 ]. 2873 * 2874 [  #sz' #i'   #p' ] 2875 #v2 #sz * #res 2876 whd in ⊢ ((??%?) → ?); 2877 whd in match (classify_aop ??); 2878 >type_eq_dec_true normalize nodelta 2879 #H destruct 2880 cases v2 in H; normalize nodelta 2881 [  #sz2' #i2'   #p2' 2882   #sz2' #i2'   #p2' ] 2883 #Heq destruct 2884 %{sz'} %{sz2'} 2885 lapply (if_opt_inversion ???? Heq) * #Hlt_u #Hres 2886 %{i'} %{i2'} 2887 >Hlt_u destruct (Hres) @conj try @conj try @conj try @refl 2888 qed. 2889 2890 2891 2892 lemma sem_cmp_int_inversion : 2893 ∀v1,v2,sz,sg,op,m,res. 2894 sem_cmp op v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? res → 2895 ∃sz,i1,i2. v1 = Vint sz i1 ∧ 2896 v2 = Vint sz i2 ∧ 2897 match sg with 2898 [ Unsigned ⇒ of_bool (cmpu_int ? op i1 i2) = res 2899  Signed ⇒ of_bool (cmp_int ? op i1 i2) = res 2900 ]. 2901 #v1 #v2 #sz0 #sg #op * #contents #next #Hnext #res 2902 whd in ⊢ ((??%?) → ?); 2903 whd in match (classify_cmp ??); >type_eq_dec_true normalize nodelta 2904 cases v1 2905 [  #sz #i   #p ] normalize nodelta 2906 #H destruct 2907 cases v2 in H; 2908 [  #sz' #i'   #p' ] normalize nodelta 2909 #H destruct lapply H H 2910 cases sz in i; #i 2911 cases sz' in i'; #i' cases sg normalize nodelta 2912 whd in match (intsize_eq_elim ???????); #H destruct 2913 [ 1,2: %{I8} 2914  3,4: %{I16} 2915  5,6: %{I32} ] 2916 %{i} %{i'} @conj try @conj try @refl 2917 qed. 2918 2919 2920 lemma sem_cmp_ptr_inversion : 2921 ∀v1,v2,ty',n,op,m,res. 2922 sem_cmp op v1 (ptr_type ty' n) v2 (ptr_type ty' n) m = Some ? res → 2923 (∃p1,p2. v1 = Vptr p1 ∧ v2 = Vptr p2 ∧ 2924 valid_pointer m p1 = true ∧ 2925 valid_pointer m p2 = true ∧ 2926 (if eq_block (pblock p1) (pblock p2) 2927 then Some ? (of_bool (cmp_offset op (poff p1) (poff p2))) 2928 else sem_cmp_mismatch op) = Some ? res) ∨ 2929 (∃p1. v1 = Vptr p1 ∧ v2 = Vnull ∧ sem_cmp_mismatch op = Some ? res) ∨ 2930 (∃p2. v1 = Vnull ∧ v2 = Vptr p2 ∧ sem_cmp_mismatch op = Some ? res) ∨ 2931 (v1 = Vnull ∧ v2 = Vnull ∧ sem_cmp_match op = Some ? res). 2932 * [  #sz #i   #p ] normalize nodelta 2933 #v2 #ty' #n #op 2934 * #contents #nextblock #Hnextblock #res whd in ⊢ ((??%?) → ?); 2935 whd in match (classify_cmp ??); cases n normalize nodelta 2936 [ 2,4,6,8: #array_len ] 2937 whd in match (ptr_type ty' ?); 2938 whd in match (if_type_eq ?????); 2939 >type_eq_dec_true normalize nodelta 2940 #H destruct 2941 cases v2 in H; normalize nodelta 2942 [  #sz' #i'   #p' 2943   #sz' #i'   #p' 2944   #sz' #i'   #p' 2945   #sz' #i'   #p' ] 2946 #H destruct 2947 try /6 by or_introl, or_intror, ex_intro, conj/ 2948 [ 1: %1 %1 %2 %{p} @conj try @conj // 2949  3: %1 %1 %2 %{p} @conj try @conj // 2950  *: %1 %1 %1 %{p} %{p'} 2951 cases (valid_pointer (mk_mem ???) p) in H; normalize nodelta 2952 cases (valid_pointer (mk_mem contents nextblock Hnextblock) p') normalize nodelta #H 2953 try @conj try @conj try @conj try @conj try @conj try @refl try @H 2954 destruct 2955 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.