Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* This file was originally generated by why. It can be modified; only the generated parts will be overwritten. *) Require Export jessie_why. Require Export WhyFloatsStrictLegacy. (* Why obligation from file "Sterbenz.c", line 2, characters 12-26: *) (*Why goal*) Lemma Sterbenz_ensures_default_po_1 : forall (x_0: single), forall (y: single), forall (HW_1: (* JC_7 *) ((* JC_5 *) (Rle (Rdiv (single_value y) (2)%R) (single_value x_0)) /\ (* JC_6 *) (Rle (single_value x_0) (Rmult (2)%R (single_value y))))), forall (result: single), forall (HW_4: (sub_single_post nearest_even x_0 y result)), forall (__retres: single), forall (HW_5: __retres = result), forall (why__return: single), forall (HW_6: why__return = __retres), (* JC_9 *) (eq (single_value why__return) (Rminus (single_value x_0) (single_value y))). Proof. intros x y (H1,H2) r (H4,(H5a,H5b)) r' H6 r'' H7. rewrite H7,H6,H4; unfold single_value in *. unfold FtoRradix; rewrite <- Fminus_correct; auto with zarith. elim (mode_single_RoundingMode nearest_even); intros P (H8,H9). apply sym_eq; apply RoundedModeProjectorIdemEq with bsingle 24%nat P; try apply psGivesBound; auto with zarith. apply Sterbenz; auto with zarith; try apply FcanonicBound with radix; try now destruct x; try now destruct y. fold FtoRradix; apply Rle_trans with (2:=H1); unfold Rdiv; simpl; right; ring. Save. (* Why obligation from file "Sterbenz.c", line 6, characters 9-12: *) (*Why goal*) Lemma Sterbenz_safety_po_1 : forall (x_0: single), forall (y: single), forall (HW_1: (* JC_7 *) ((* JC_5 *) (Rle (Rdiv (single_value y) (2)%R) (single_value x_0)) /\ (* JC_6 *) (Rle (single_value x_0) (Rmult (2)%R (single_value y))))), (no_overflow_single nearest_even (Rminus (single_value x_0) (single_value y))). Proof. intros x; intros; apply bounded_real_no_overflow_single. cut (0 <= single_value y)%R; try intros. cut (0 <= single_value x)%R; try intros. case (Rle_or_lt (single_value x) (single_value y)); intros. rewrite Rabs_left1; ring_simplify. apply Rle_trans with (-0+single_value y)%R;auto with real. ring_simplify; rewrite <- (Rabs_right (single_value y));[apply single_le_strict|auto with real]. apply Rplus_le_reg_l with (single_value y); now ring_simplify. rewrite Rabs_right; ring_simplify. apply Rle_trans with (single_value x-0)%R. apply Rplus_le_compat_l; auto with real. ring_simplify; rewrite <- (Rabs_right (single_value x));[apply single_le_strict|auto with real]. apply Rle_ge; apply Rplus_le_reg_l with (single_value y); ring_simplify; auto with real. apply Rle_trans with (single_value y / 2)%R;[idtac|apply HW_1]. unfold Rdiv; apply Rmult_le_pos; auto with real. apply Rmult_le_reg_l with 3%R;[apply Rlt_le_trans with 2%R; auto with real|idtac]. apply Rplus_le_reg_l with (single_value y); apply Rmult_le_reg_l with (/2)%R; auto with real. replace (/ 2 * (single_value y + 3 * 0))%R with (single_value y / 2)%R by (unfold Rdiv; ring). apply Rle_trans with (single_value x);[eapply HW_1|idtac]. apply Rle_trans with (2 * single_value y)%R;[eapply HW_1|right;field]. Save.