Require Export "discriminant3". Require Export "Dekker". Require Export WhyFloatsStrictLegacy. Section Discriminant_again. Coercion Local FtoRradix := FtoR radix. Variables x y p q hx tx p' q' hy ty x1y1 x1y2 x2y1 x2y2 r t1 t2 t3 t4: float. Hypotheses Cx: Fcanonic radix bdouble x. Hypotheses Cy: Fcanonic radix bdouble y. Hypothesis A1: (Closest bdouble radix (x*((powerRZ radix 27)+1))%R p). Hypothesis A2: (Closest bdouble radix (x-p)%R q). Hypothesis A3: (Closest bdouble radix (q+p)%R hx). Hypothesis A4: (Closest bdouble radix (x-hx)%R tx). Hypothesis B1: (Closest bdouble radix (y*((powerRZ radix 27)+1))%R p'). Hypothesis B2: (Closest bdouble radix (y-p')%R q'). Hypothesis B3: (Closest bdouble radix (q'+p')%R hy). Hypothesis B4: (Closest bdouble radix (y-hy)%R ty). Hypothesis C1: (Closest bdouble radix (hx*hy)%R x1y1). Hypothesis C2: (Closest bdouble radix (hx*ty)%R x1y2). Hypothesis C3: (Closest bdouble radix (tx*hy)%R x2y1). Hypothesis C4: (Closest bdouble radix (tx*ty)%R x2y2). Hypothesis D1: (Closest bdouble radix (x*y)%R r). Hypothesis D2: (Closest bdouble radix (r-x1y1)%R t1). Hypothesis D3: (Closest bdouble radix (t1-x1y2)%R t2). Hypothesis D4: (Closest bdouble radix (t2-x2y1)%R t3). Hypothesis D5: (Closest bdouble radix (t3-x2y2)%R t4). Hypothesis U1: (x*y=0)%R \/ (powerRZ radix (-969) <= Rabs (x*y))%R. Hypothesis O1: (Rabs x <= powerRZ radix 995)%R. Hypothesis O2: (Rabs y <= powerRZ radix 995)%R. Hypothesis O3: (Rabs (x*y) <= powerRZ radix 1022)%R. Lemma FexpxFexpyge: ~(x*y = 0)%R -> (-dExp bdouble <= Fexp x +Fexp y)%Z. intros KK; case U1; intros U1'. absurd (x*y=0)%R; auto with real. apply Zle_trans with (-1074)%Z; auto with zarith. assert (-969 < ((53+Fexp x)) + (53+Fexp y))%Z; auto with zarith. apply Zlt_powerRZ with radix. unfold radix; simpl; auto with real zarith. apply Rle_lt_trans with (1:=U1'). rewrite Rabs_mult. assert (0 <= Rabs y)%R; auto with real. case H; intros. rewrite powerRZ_add; auto with real zarith. apply Rlt_le_trans with (powerRZ radix (53 + Fexp x)* Rabs y)%R. apply Rmult_lt_compat_r; auto with real. rewrite powerRZ_add; auto with real zarith. replace (powerRZ radix 53) with (IZR (Zpos (vNum bdouble))). 2: rewrite pdGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith. unfold FtoR, Fabs. simpl (Fnum (Float (Zabs (Fnum x)) (Fexp x)) * powerRZ radix (Fexp (Float (Zabs (Fnum x)) (Fexp x))))%R. unfold radix; apply Rmult_lt_compat_r. auto with real zarith. assert (Fbounded bdouble x). apply FcanonicBound with radix; auto with zarith. apply Rlt_IZR; elim H1; auto. apply Rmult_le_compat_l; auto with real. rewrite powerRZ_add; auto with real zarith. replace (powerRZ radix 53) with (IZR (Zpos (vNum bdouble))). 2: rewrite pdGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith. unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith. unfold FtoR, Fabs. simpl (Fnum (Float (Zabs (Fnum y)) (Fexp y)) * powerRZ radix (Fexp (Float (Zabs (Fnum y)) (Fexp y))))%R. unfold radix; apply Rmult_le_compat_r. auto with real zarith. assert (Fbounded bdouble y). apply FcanonicBound with radix; auto with zarith. left;apply Rlt_IZR; elim H1; auto. rewrite <- H0; ring_simplify (Rabs x * 0)%R; auto with real zarith. Qed. Theorem Zero_ok_aux : (x*y=0)%R -> (FtoRradix r=0) /\ (hx*hy=0)%R /\ (hx*ty=0)%R /\ (tx*hy=0)%R /\ (tx*ty=0)%R. intros I; split. unfold FtoRradix; apply ClosestZero with (4:=D1) (p:=53%nat); try apply pdGivesBound; auto with zarith float. assert ((FtoRradix x=0) \/ (FtoRradix y=0))%R. case (Req_dec x 0); auto with real. intros I1; case (Req_dec y 0); auto with real. intros I2; absurd (x*y=0)%R; auto with real. case H; clear H; intros H. assert (FtoRradix hx=0)%R. assert (FtoRradix p=0)%R. unfold FtoRradix; apply ClosestZero with bdouble 53%nat (x * (powerRZ radix 27 + 1))%R;try apply pdGivesBound; auto with real zarith float. assert (FtoRradix q=0)%R. unfold FtoRradix; apply ClosestZero with bdouble 53%nat (x -p)%R;try apply pdGivesBound; auto with real zarith float. rewrite H; rewrite H0; ring. unfold FtoRradix; apply ClosestZero with bdouble 53%nat (q +p)%R;try apply pdGivesBound; auto with real zarith float. rewrite H0; rewrite H1; ring. assert (FtoRradix tx=0)%R. unfold FtoRradix; apply ClosestZero with bdouble 53%nat (x-hx)%R;try apply pdGivesBound; auto with real zarith float. rewrite H; rewrite H0; ring. rewrite H0; rewrite H1; repeat split; ring. assert (FtoRradix hy=0)%R. assert (FtoRradix p'=0)%R. unfold FtoRradix; apply ClosestZero with bdouble 53%nat (y * (powerRZ radix 27 + 1))%R;try apply pdGivesBound; auto with real zarith float. assert (FtoRradix q'=0)%R. unfold FtoRradix; apply ClosestZero with bdouble 53%nat (y -p')%R;try apply pdGivesBound; auto with real zarith float. rewrite H; rewrite H0; ring. unfold FtoRradix; apply ClosestZero with bdouble 53%nat (q' +p')%R;try apply pdGivesBound; auto with real zarith float. rewrite H0; rewrite H1; ring. assert (FtoRradix ty=0)%R. unfold FtoRradix; apply ClosestZero with bdouble 53%nat (y-hy)%R;try apply pdGivesBound; auto with real zarith float. rewrite H; rewrite H0; ring. rewrite H0; rewrite H1; repeat split; ring. Qed. Theorem Zero_ok : (x*y=0)%R -> (FtoRradix r=0) /\ (FtoRradix t4=0)%R. intros I. destruct (Zero_ok_aux I) as (Z1,(Z2,(Z3,(Z4,Z5)))). split; trivial. unfold FtoRradix; apply ClosestZero with bdouble 53%nat (t3-x2y2)%R;try apply pdGivesBound; auto with real zarith float. unfold FtoRradix; rewrite ClosestZero with bdouble radix 53%nat (tx*ty)%R x2y2; try apply pdGivesBound; auto with real zarith float. rewrite ClosestZero with bdouble radix 53%nat (t2-x2y1)%R t3; try apply pdGivesBound; auto with real zarith float. unfold FtoRradix; rewrite ClosestZero with bdouble radix 53%nat (tx*hy)%R x2y1; try apply pdGivesBound; auto with real zarith float. rewrite ClosestZero with bdouble radix 53%nat (t1-x1y2)%R t2; try apply pdGivesBound; auto with real zarith float. unfold FtoRradix; rewrite ClosestZero with bdouble radix 53%nat (hx*ty)%R x1y2; try apply pdGivesBound; auto with real zarith float. rewrite ClosestZero with bdouble radix 53%nat (r-x1y1)%R t1; try apply pdGivesBound; auto with real zarith float. rewrite Z1; unfold FtoRradix; rewrite ClosestZero with bdouble radix 53%nat (hx*hy)%R x1y1; try apply pdGivesBound; auto with real zarith float. Qed. End Discriminant_again. (* Require Export Why2Gappa. Section Veltkamp_again. Variables s:nat. Variables x p q hx tx: float. Theorem VeltkampEven_gappa: (2 <= s <= 51)%nat -> Fcanonic radix bdouble x -> FtoRradix p = gappa_rounding (rounding_float roundNE 53 1074) (x * (powerRZ radix s + 1)) -> FtoRradix q = gappa_rounding (rounding_float roundNE 53 1074) (x-p) -> FtoRradix hx = gappa_rounding (rounding_float roundNE 53 1074) (q+p) -> FtoRradix hx = gappa_rounding (rounding_float roundNE (P_of_succ_nat (52- s)) 1074) x. intros. destruct equiv_RNDs_aux9 with bdouble 53%nat (x * (powerRZ radix s + 1))%R as (p',(H4,(H5,H6))); try apply pdGivesBound; auto with zarith. destruct equiv_RNDs_aux9 with bdouble 53%nat (x-p')%R as (q',(H7,(H8,H9))); try apply pdGivesBound; auto with zarith. destruct equiv_RNDs_aux9 with bdouble 53%nat (q'+p')%R as (hx',(H10,(H11,H12))); try apply pdGivesBound; auto with zarith. destruct VeltkampEven with radix bdouble s 53%nat x p' q' hx' as (hx'',(H13,H14)); try apply pdGivesBound; auto with zarith arith. fold FtoRradix in H13, H14. destruct equiv_RNDs_aux9 with (Bound (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (53 - s))))) (dExp bdouble)) (53-s)%nat x as (hx''',(H15,(H16,H17))). apply p''GivesBound; auto with zarith. auto with zarith arith. apply sym_eq. apply trans_eq with (hx'''). rewrite H16. replace (53 - s - 1) with (52-s). reflexivity. clear -H; destruct H; omega. apply trans_eq with (FtoRradix hx''). generalize EvenClosestUniqueP; unfold UniqueP; intros T. unfold FtoRradix; apply T with (Bound (P_of_succ_nat (pred (Zabs_nat (Zpower_nat radix (53 - s))))) (dExp bdouble)) (53-s)%nat x; clear T. auto with zarith. auto with zarith. apply p''GivesBound; auto with zarith. exact H17. exact H14. rewrite H13. rewrite H3; rewrite H11. assert (FtoRradix p' = FtoRradix p). rewrite H5; rewrite H1; reflexivity. rewrite H18. replace (FtoRradix q') with (FtoRradix q). reflexivity. rewrite H2; rewrite H8; rewrite H18; reflexivity. Qed. Theorem VeltkampTail_gappa: (2 <= s <= 51)%nat -> Fcanonic radix bdouble x -> FtoRradix p = gappa_rounding (rounding_float roundNE 53 1074) (x * (powerRZ radix s + 1)) -> FtoRradix q = gappa_rounding (rounding_float roundNE 53 1074) (x-p) -> FtoRradix hx = gappa_rounding (rounding_float roundNE 53 1074) (q+p) -> FtoRradix tx = gappa_rounding (rounding_float roundNE 53 1074) (x-hx) -> (FtoRradix tx = x - gappa_rounding (rounding_float roundNE (P_of_succ_nat (52- s)) 1074) x)%R. intros. apply trans_eq with (x-hx)%R. destruct equiv_RNDs_aux9 with bdouble 53%nat (x * (powerRZ radix s + 1))%R as (p',(H15,(H5,H6))); try apply pdGivesBound; auto with zarith. destruct equiv_RNDs_aux9 with bdouble 53%nat (x-p')%R as (q',(H7,(H8,H9))); try apply pdGivesBound; auto with zarith. destruct equiv_RNDs_aux9 with bdouble 53%nat (q'+p')%R as (hx',(H10,(H11,H12))); try apply pdGivesBound; auto with zarith. destruct equiv_RNDs_aux9 with bdouble 53%nat (x-hx')%R as (tx',(H13,(H14,H16))); try apply pdGivesBound; auto with zarith. destruct Veltkamp_tail with radix bdouble s 53%nat x p' q' hx' tx' as (tx'',(T1,(T2,_))); try apply pdGivesBound; auto with zarith arith. eapply H6. eapply H9. eapply H12. eapply H16. assert (FtoRradix p' = FtoRradix p). rewrite H5; rewrite H1; reflexivity. fold FtoRradix in T1,T2. rewrite <- T2; rewrite T1. assert (FtoRradix hx = FtoRradix hx'). rewrite H11; rewrite H3. rewrite H17. replace (FtoRradix q') with (FtoRradix q). reflexivity. rewrite H2; rewrite H8; rewrite H17; reflexivity. assert (FtoRradix tx = FtoRradix tx'). rewrite H14; rewrite H4; rewrite H18; reflexivity. rewrite H19; rewrite H18; ring. now rewrite VeltkampEven_gappa. Qed. End Veltkamp_again. *) (* This file was originally generated by why. It can be modified; only the generated parts will be overwritten. *) Require Export jessie_why. (*Why type*) Definition char_P: Set. Admitted. (*Why type*) Definition int8: Set. Admitted. (*Why type*) Definition padding: Set. Admitted. (*Why type*) Definition void_P: Set. Admitted. (*Why logic*) Definition char_P_tag : (tag_id char_P). Admitted. (*Why axiom*) Lemma char_P_int : (int_of_tag char_P_tag) = 1. Admitted. (*Why logic*) Definition char_P_of_pointer_address : (pointer unit) -> (pointer char_P). Admitted. (*Why axiom*) Lemma char_P_of_pointer_address_of_pointer_addr : (forall (p:(pointer char_P)), p = (char_P_of_pointer_address (pointer_address p))). Admitted. (*Why axiom*) Lemma char_P_parenttag_bottom : (parenttag char_P_tag (@bottom_tag char_P)). Admitted. (*Why axiom*) Lemma char_P_tags : (forall (x:(pointer char_P)), (forall (char_P_tag_table:(tag_table char_P)), (instanceof char_P_tag_table x char_P_tag))). Admitted. (*Why logic*) Definition integer_of_int8 : int8 -> Z. Admitted. (*Why predicate*) Definition eq_int8 (x:int8) (y:int8) := (integer_of_int8 x) = (integer_of_int8 y). (*Why logic*) Definition int8_of_integer : Z -> int8. Admitted. (*Why axiom*) Lemma int8_coerce : (forall (x:Z), ((-128) <= x /\ x <= 127 -> (integer_of_int8 (int8_of_integer x)) = x)). Admitted. (*Why axiom*) Lemma int8_range : (forall (x:int8), (-128) <= (integer_of_int8 x) /\ (integer_of_int8 x) <= 127). Admitted. (*Why predicate*) Definition left_valid_struct_char_P (p:(pointer char_P)) (a:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_min char_P_alloc_table p) <= a. (*Why predicate*) Definition left_valid_struct_void_P (p:(pointer void_P)) (a:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_min void_P_alloc_table p) <= a. (*Why axiom*) Lemma pointer_addr_of_char_P_of_pointer_address : (forall (p:(pointer unit)), p = (pointer_address (char_P_of_pointer_address p))). Admitted. (*Why logic*) Definition void_P_of_pointer_address : (pointer unit) -> (pointer void_P). Admitted. (*Why axiom*) Lemma pointer_addr_of_void_P_of_pointer_address : (forall (p:(pointer unit)), p = (pointer_address (void_P_of_pointer_address p))). Admitted. (*Why predicate*) Definition right_valid_struct_char_P (p:(pointer char_P)) (b:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_max char_P_alloc_table p) >= b. (*Why predicate*) Definition right_valid_struct_void_P (p:(pointer void_P)) (b:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_max void_P_alloc_table p) >= b. (*Why predicate*) Definition strict_valid_root_char_P (p:(pointer char_P)) (a:Z) (b:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_min char_P_alloc_table p) = a /\ (offset_max char_P_alloc_table p) = b. (*Why predicate*) Definition strict_valid_root_void_P (p:(pointer void_P)) (a:Z) (b:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_min void_P_alloc_table p) = a /\ (offset_max void_P_alloc_table p) = b. (*Why predicate*) Definition strict_valid_struct_char_P (p:(pointer char_P)) (a:Z) (b:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_min char_P_alloc_table p) = a /\ (offset_max char_P_alloc_table p) = b. (*Why predicate*) Definition strict_valid_struct_void_P (p:(pointer void_P)) (a:Z) (b:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_min void_P_alloc_table p) = a /\ (offset_max void_P_alloc_table p) = b. (*Why predicate*) Definition valid_bitvector_struct_char_P (p:(pointer unit)) (a:Z) (b:Z) (bitvector_alloc_table:(alloc_table unit)) := (offset_min bitvector_alloc_table p) = a /\ (offset_max bitvector_alloc_table p) = b. (*Why predicate*) Definition valid_bitvector_struct_void_P (p:(pointer unit)) (a:Z) (b:Z) (bitvector_alloc_table:(alloc_table unit)) := (offset_min bitvector_alloc_table p) = a /\ (offset_max bitvector_alloc_table p) = b. (*Why predicate*) Definition valid_root_char_P (p:(pointer char_P)) (a:Z) (b:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_min char_P_alloc_table p) <= a /\ (offset_max char_P_alloc_table p) >= b. (*Why predicate*) Definition valid_root_void_P (p:(pointer void_P)) (a:Z) (b:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_min void_P_alloc_table p) <= a /\ (offset_max void_P_alloc_table p) >= b. (*Why predicate*) Definition valid_struct_char_P (p:(pointer char_P)) (a:Z) (b:Z) (char_P_alloc_table:(alloc_table char_P)) := (offset_min char_P_alloc_table p) <= a /\ (offset_max char_P_alloc_table p) >= b. (*Why predicate*) Definition valid_struct_void_P (p:(pointer void_P)) (a:Z) (b:Z) (void_P_alloc_table:(alloc_table void_P)) := (offset_min void_P_alloc_table p) <= a /\ (offset_max void_P_alloc_table p) >= b. (*Why logic*) Definition void_P_tag : (tag_id void_P). Admitted. (*Why axiom*) Lemma void_P_int : (int_of_tag void_P_tag) = 1. Admitted. (*Why axiom*) Lemma void_P_of_pointer_address_of_pointer_addr : (forall (p:(pointer void_P)), p = (void_P_of_pointer_address (pointer_address p))). Admitted. (*Why axiom*) Lemma void_P_parenttag_bottom : (parenttag void_P_tag (@bottom_tag void_P)). Admitted. (*Why axiom*) Lemma void_P_tags : (forall (x:(pointer void_P)), (forall (void_P_tag_table:(tag_table void_P)), (instanceof void_P_tag_table x void_P_tag))). Admitted. (* Why obligation from file "Dekker.c", line 12, characters 13-26: *) (*Why goal*) Lemma Dekker_ensures_default_po_1 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result: double), forall (HW_13: (no_overflow_double nearest_even (134217729)%R) /\ (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_14: C = result), (* JC_36 *) (* JC_36 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R)). Proof. intros _ _ _ _; intros r1 (H1,H2) r2 H3. why2gappa. gappa. Save. (* Why obligation from file "Dekker.c", line 5, characters 12-92: *) (*Why goal*) Lemma Dekker_ensures_default_po_2 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result: double), forall (HW_13: (no_overflow_double nearest_even (134217729)%R) /\ (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_14: C = result), forall (HW_15: (* JC_36 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (result0: double), forall (HW_16: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C))) /\ (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_17: px = result0), forall (result1: double), forall (HW_18: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px))) /\ (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_19: qx = result1), forall (result2: double), forall (HW_20: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx))) /\ (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_21: hx = result2), forall (result3: double), forall (HW_22: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx))) /\ (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_23: tx = result3), forall (result4: double), forall (HW_24: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C))) /\ (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_25: py = result4), forall (result5: double), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value y) (double_value py))) /\ (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_27: qy = result5), forall (result6: double), forall (HW_28: (no_overflow_double nearest_even (Rplus (double_value py) (double_value qy))) /\ (add_double_post nearest_even py qy result6)), forall (hy: double), forall (HW_29: hy = result6), forall (result7: double), forall (HW_30: (no_overflow_double nearest_even (Rminus (double_value y) (double_value hy))) /\ (sub_double_post nearest_even y hy result7)), forall (ty: double), forall (HW_31: ty = result7), forall (result8: double), forall (HW_32: (neg_double_post xy result8)), forall (result9: double), forall (HW_33: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value hy))) /\ (mul_double_post nearest_even hx hy result9)), forall (result10: double), forall (HW_34: (no_overflow_double nearest_even (Rplus (double_value result8) (double_value result9))) /\ (add_double_post nearest_even result8 result9 result10)), forall (r2: double), forall (HW_35: r2 = result10), forall (result11: double), forall (HW_36: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value ty))) /\ (mul_double_post nearest_even hx ty result11)), forall (result12: double), forall (HW_37: (no_overflow_double nearest_even (Rplus (double_value r2) (double_value result11))) /\ (add_double_post nearest_even r2 result11 result12)), forall (r2_0: double), forall (HW_38: r2_0 = result12), forall (result13: double), forall (HW_39: (no_overflow_double nearest_even (Rmult (double_value hy) (double_value tx))) /\ (mul_double_post nearest_even hy tx result13)), forall (result14: double), forall (HW_40: (no_overflow_double nearest_even (Rplus (double_value r2_0) (double_value result13))) /\ (add_double_post nearest_even r2_0 result13 result14)), forall (r2_1: double), forall (HW_41: r2_1 = result14), forall (result15: double), forall (HW_42: (no_overflow_double nearest_even (Rmult (double_value tx) (double_value ty))) /\ (mul_double_post nearest_even tx ty result15)), forall (result16: double), forall (HW_43: (no_overflow_double nearest_even (Rplus (double_value r2_1) (double_value result15))) /\ (add_double_post nearest_even r2_1 result15 result16)), forall (r2_2: double), forall (HW_44: r2_2 = result16), forall (why__return: double), forall (HW_45: why__return = r2_2), forall (HW_46: (eq (Rmult (double_value x_0) (double_value y)) (0)%R) \/ (Rle (1 / 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712)%R (Rabs (Rmult (double_value x_0) (double_value y))))), (* JC_13 *) (eq (Rmult (double_value x_0) (double_value y)) (Rplus (double_value xy) ( double_value why__return))). Proof. intuition. (* x*y = 0 *) why2float. assert ((53 - div2 53)%nat = 27%nat) by reflexivity. generalize ClosestCompatible; unfold CompatibleP; intros T. destruct Zero_ok with x_0 y (* x/2 *) px qx hx tx (* y/2 *) py qy hy ty (* mul *) result9 result11 result13 result15 (* *) xy (* add *) (Fopp result10) (Fopp result12) (Fopp result14) (Fopp result16) as (Z1,Z2). replace (powerRZ radix 27 + 1)%R with (FtoRradix C). apply T with (x_0*C)%R (RND_EvenClosest bdouble radix 53 (x_0*C)); try reflexivity. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. fold FtoRradix; apply sym_eq; rewrite H110; assumption. apply FcanonicBound with radix; assumption. rewrite HW_15; simpl; ring. apply T with (x_0 - px)%R (RND_EvenClosest bdouble radix 53 (x_0 - px)); try reflexivity. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith real. fold FtoRradix; apply sym_eq; rewrite H107; assumption. apply FcanonicBound with radix; assumption. apply T with (px + qx)%R (RND_EvenClosest bdouble radix 53 (px + qx)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. apply Rplus_comm. fold FtoRradix; apply sym_eq; rewrite H104; assumption. apply FcanonicBound with radix; assumption. apply T with (x_0 - hx)%R (RND_EvenClosest bdouble radix 53 (x_0 - hx)); try reflexivity. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. fold FtoRradix; apply sym_eq; rewrite H101; assumption. apply FcanonicBound with radix; assumption. replace (powerRZ radix 27 + 1)%R with (FtoRradix C). apply T with (y * C)%R (RND_EvenClosest bdouble radix 53 (y * C)); try reflexivity. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. fold FtoRradix; apply sym_eq; rewrite H98; assumption. apply FcanonicBound with radix; assumption. rewrite HW_15; simpl; ring. apply T with (y - py)%R (RND_EvenClosest bdouble radix 53 (y - py)); try reflexivity. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. fold FtoRradix; apply sym_eq; rewrite H95; assumption. apply FcanonicBound with radix; assumption. apply T with (py + qy)%R (RND_EvenClosest bdouble radix 53 (py + qy)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. apply Rplus_comm. fold FtoRradix; apply sym_eq; rewrite H92; assumption. apply FcanonicBound with radix; assumption. apply T with (y - hy)%R (RND_EvenClosest bdouble radix 53 (y - hy)); try reflexivity. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. fold FtoRradix; apply sym_eq; rewrite H89; assumption. apply FcanonicBound with radix; assumption. apply T with (hx*hy)%R (RND_EvenClosest bdouble radix 53 (hx*hy)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. reflexivity. fold FtoRradix; apply sym_eq; assumption. apply FcanonicBound with radix; assumption. apply T with (hx*ty)%R (RND_EvenClosest bdouble radix 53 (hx*ty)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. reflexivity. fold FtoRradix; apply sym_eq; assumption. apply FcanonicBound with radix; assumption. apply T with (hy*tx)%R (RND_EvenClosest bdouble radix 53 (hy*tx)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. apply Rmult_comm. fold FtoRradix; apply sym_eq; assumption. apply FcanonicBound with radix; assumption. apply T with (tx*ty)%R (RND_EvenClosest bdouble radix 53 (tx*ty)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. reflexivity. fold FtoRradix; apply sym_eq; assumption. apply FcanonicBound with radix; assumption. apply T with (x_0*y)%R (RND_EvenClosest bdouble radix 53 (x_0*y)); try reflexivity. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. fold FtoRradix; apply sym_eq; assumption. apply FcanonicBound with radix; assumption. apply T with (-(result8+result9))%R (Fopp (RND_EvenClosest bdouble radix 53 (result8+result9))). apply ClosestOpp. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. rewrite HW_32; ring. repeat rewrite Fopp_correct. apply f_equal; fold FtoRradix; apply sym_eq; assumption. apply oppBounded. apply FcanonicBound with radix; assumption. apply T with (-(r2+result11))%R (Fopp (RND_EvenClosest bdouble radix 53 (r2+result11))). apply ClosestOpp. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. rewrite H86; unfold FtoRradix; rewrite Fopp_correct; ring. repeat rewrite Fopp_correct. apply f_equal; fold FtoRradix; apply sym_eq; assumption. apply oppBounded. apply FcanonicBound with radix; assumption. apply T with (-(r2_0+result13))%R (Fopp (RND_EvenClosest bdouble radix 53 (r2_0+result13))). apply ClosestOpp. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. rewrite H83; unfold FtoRradix; rewrite Fopp_correct; ring. repeat rewrite Fopp_correct. apply f_equal; fold FtoRradix; apply sym_eq; assumption. apply oppBounded. apply FcanonicBound with radix; assumption. apply T with (-(r2_1+result15))%R (Fopp (RND_EvenClosest bdouble radix 53 (r2_1+result15))). apply ClosestOpp. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. rewrite H80; unfold FtoRradix; rewrite Fopp_correct; ring. repeat rewrite Fopp_correct. apply f_equal; fold FtoRradix; now rewrite <- H36. apply oppBounded. apply FcanonicBound with radix; assumption. left; assumption. assumption. rewrite H37; rewrite Z1. rewrite H74; rewrite H77. rewrite <- (Ropp_involutive (FtoRradix result16)). unfold FtoRradix; rewrite <- (Fopp_correct). fold FtoRradix; rewrite Z2. simpl; ring. (* no underflow *) why2float. assert ((53 - div2 53)%nat = 27%nat) by reflexivity. replace (xy+why__return)%R with (xy - (Fopp why__return))%R. 2: unfold FtoRradix; rewrite Fopp_correct; ring. unfold FtoRradix. generalize ClosestCompatible; unfold CompatibleP; intros T. apply Dekker1 with bdouble 53%nat (* x/2 *) px qx hx tx (* y/2 *) py qy hy ty (* mul *) result9 result11 result13 result15 (* add *) (Fopp result10) (Fopp result12) (Fopp result14); try assumption; fold FtoRradix. auto with zarith. apply pdGivesBound. clear; auto with arith. apply FexpxFexpyge; try assumption. right. apply Rle_trans with (2:=H37). unfold Rdiv; rewrite Rmult_1_l. simpl. right; apply f_equal. rewrite Rmult_1_r. reflexivity. intro; Contradict H37. rewrite H117; rewrite Rabs_R0. clear; apply Rlt_not_le. unfold Rdiv; rewrite Rmult_1_l; apply Rinv_0_lt_compat. assert (0 < 2)%R; auto with real. repeat apply Rmult_lt_0_compat; try assumption. replace (powerRZ radix (53 - div2 53)%nat + 1)%R with (FtoRradix C). apply T with (x_0 * C)%R (RND_EvenClosest bdouble radix 53 (x_0 * C)); try reflexivity. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. fold FtoRradix; apply sym_eq; rewrite H110; assumption. apply FcanonicBound with radix; assumption. rewrite H116, HW_15; simpl; ring. apply T with (x_0 - px)%R (RND_EvenClosest bdouble radix 53 (x_0 - px)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. reflexivity. fold FtoRradix; apply sym_eq; rewrite H107; assumption. apply FcanonicBound with radix; assumption. apply T with (px + qx)%R (RND_EvenClosest bdouble radix 53 (px + qx)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. apply Rplus_comm. fold FtoRradix; apply sym_eq; rewrite H104; assumption. apply FcanonicBound with radix; assumption. apply T with (x_0 - hx)%R (RND_EvenClosest bdouble radix 53 (x_0 - hx)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. reflexivity. fold FtoRradix; apply sym_eq; rewrite H101; assumption. apply FcanonicBound with radix; assumption. replace (powerRZ radix (53 - div2 53)%nat + 1)%R with (FtoRradix C). apply T with (y * C)%R (RND_EvenClosest bdouble radix 53 (y * C)); try reflexivity. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. fold FtoRradix; apply sym_eq; rewrite H98; assumption. apply FcanonicBound with radix; assumption. rewrite H116, HW_15; simpl; ring. apply T with (y - py)%R (RND_EvenClosest bdouble radix 53 (y - py)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. reflexivity. fold FtoRradix; apply sym_eq; rewrite H95; assumption. apply FcanonicBound with radix; assumption. apply T with (py + qy)%R (RND_EvenClosest bdouble radix 53 (py + qy)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. apply Rplus_comm. fold FtoRradix; apply sym_eq; rewrite H92; assumption. apply FcanonicBound with radix; assumption. apply T with (y - hy)%R (RND_EvenClosest bdouble radix 53 (y - hy)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. reflexivity. fold FtoRradix; apply sym_eq; rewrite H89; assumption. apply FcanonicBound with radix; assumption. apply T with (hx*hy)%R (RND_EvenClosest bdouble radix 53 (hx*hy)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. reflexivity. fold FtoRradix; apply sym_eq; assumption. apply FcanonicBound with radix; assumption. apply T with (hx*ty)%R (RND_EvenClosest bdouble radix 53 (hx*ty)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. reflexivity. fold FtoRradix; apply sym_eq; assumption. apply FcanonicBound with radix; assumption. apply T with (hy*tx)%R (RND_EvenClosest bdouble radix 53 (hy*tx)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. apply Rmult_comm. fold FtoRradix; apply sym_eq; assumption. apply FcanonicBound with radix; assumption. apply T with (tx*ty)%R (RND_EvenClosest bdouble radix 53 (tx*ty)). eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. reflexivity. fold FtoRradix; apply sym_eq; assumption. apply FcanonicBound with radix; assumption. apply T with (x_0*y)%R (RND_EvenClosest bdouble radix 53 (x_0*y)); try reflexivity. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. fold FtoRradix; apply sym_eq; assumption. apply FcanonicBound with radix; assumption. apply T with (-(result8+result9))%R (Fopp (RND_EvenClosest bdouble radix 53 (result8+result9))). apply ClosestOpp. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. rewrite HW_32; ring. repeat rewrite Fopp_correct. apply f_equal; fold FtoRradix; apply sym_eq; assumption. apply oppBounded. apply FcanonicBound with radix; assumption. apply T with (-(r2+result11))%R (Fopp (RND_EvenClosest bdouble radix 53 (r2+result11))). apply ClosestOpp. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. rewrite H86; unfold FtoRradix; rewrite Fopp_correct; ring. repeat rewrite Fopp_correct. apply f_equal; fold FtoRradix; apply sym_eq; assumption. apply oppBounded. apply FcanonicBound with radix; assumption. apply T with (-(r2_0+result13))%R (Fopp (RND_EvenClosest bdouble radix 53 (r2_0+result13))). apply ClosestOpp. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. rewrite H83; unfold FtoRradix; rewrite Fopp_correct; ring. repeat rewrite Fopp_correct. apply f_equal; fold FtoRradix; apply sym_eq; assumption. apply oppBounded. apply FcanonicBound with radix; assumption. apply T with (-(r2_1+result15))%R (Fopp (RND_EvenClosest bdouble radix 53 (r2_1+result15))). apply ClosestOpp. eapply RND_EvenClosest_correct; try apply pdGivesBound; auto with zarith. rewrite H80; unfold FtoRradix; rewrite Fopp_correct; ring. repeat rewrite Fopp_correct. apply f_equal; fold FtoRradix; rewrite <- H36. rewrite H74; apply sym_eq; assumption. apply oppBounded. apply FcanonicBound with radix; assumption. simpl; clear; auto with zarith. clear; left; auto with zarith. Save. (* Why obligation from file "Dekker.jc", line 62, characters 18-41: *) (*Why goal*) Lemma Dekker_safety_po_1 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), (no_overflow_double nearest_even (134217729)%R). Proof. intros; clear. why2gappa; gappa. Save. (* Why obligation from file "Dekker.c", line 14, characters 5-8: *) (*Why goal*) Lemma Dekker_safety_po_2 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C))). Proof. intuition;why2gappa; gappa. Save. (* Why obligation from file "Dekker.c", line 15, characters 5-9: *) (*Why goal*) Lemma Dekker_safety_po_3 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px))). Proof. intuition; why2gappa. gappa. Qed. (* Why obligation from file "Dekker.c", line 16, characters 5-10: *) (*Why goal*) Lemma Dekker_safety_po_4 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx))). Proof. intuition; why2gappa; gappa. Qed. (* Why obligation from file "Dekker.c", line 17, characters 5-9: *) (*Why goal*) Lemma Dekker_safety_po_5 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx))). Proof. intuition; why2gappa; gappa. Qed. (* Why obligation from file "Dekker.c", line 19, characters 5-8: *) (*Why goal*) Lemma Dekker_safety_po_6 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), (no_overflow_double nearest_even (Rmult (double_value y) (double_value C))). Proof. intuition; why2gappa; gappa. Qed. (* Why obligation from file "Dekker.c", line 20, characters 5-9: *) (*Why goal*) Lemma Dekker_safety_po_7 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), forall (HW_29: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C)))), forall (result4: double), forall (HW_30: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_31: py = result4), (no_overflow_double nearest_even (Rminus (double_value y) (double_value py))). Proof. intuition; why2gappa; gappa. Qed. (* Why obligation from file "Dekker.c", line 21, characters 5-10: *) (*Why goal*) Lemma Dekker_safety_po_8 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), forall (HW_29: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C)))), forall (result4: double), forall (HW_30: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_31: py = result4), forall (HW_32: (no_overflow_double nearest_even (Rminus (double_value y) (double_value py)))), forall (result5: double), forall (HW_33: (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_34: qy = result5), (no_overflow_double nearest_even (Rplus (double_value py) (double_value qy))). Proof. intuition; why2gappa; gappa. Qed. (* Why obligation from file "Dekker.c", line 22, characters 5-9: *) (*Why goal*) Lemma Dekker_safety_po_9 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), forall (HW_29: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C)))), forall (result4: double), forall (HW_30: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_31: py = result4), forall (HW_32: (no_overflow_double nearest_even (Rminus (double_value y) (double_value py)))), forall (result5: double), forall (HW_33: (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_34: qy = result5), forall (HW_35: (no_overflow_double nearest_even (Rplus (double_value py) (double_value qy)))), forall (result6: double), forall (HW_36: (add_double_post nearest_even py qy result6)), forall (hy: double), forall (HW_37: hy = result6), (no_overflow_double nearest_even (Rminus (double_value y) (double_value hy))). Proof. intuition; why2gappa; gappa. Qed. (* Why obligation from file "Dekker.c", line 24, characters 9-14: *) (*Why goal*) Lemma Dekker_safety_po_10 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), forall (HW_29: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C)))), forall (result4: double), forall (HW_30: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_31: py = result4), forall (HW_32: (no_overflow_double nearest_even (Rminus (double_value y) (double_value py)))), forall (result5: double), forall (HW_33: (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_34: qy = result5), forall (HW_35: (no_overflow_double nearest_even (Rplus (double_value py) (double_value qy)))), forall (result6: double), forall (HW_36: (add_double_post nearest_even py qy result6)), forall (hy: double), forall (HW_37: hy = result6), forall (HW_38: (no_overflow_double nearest_even (Rminus (double_value y) (double_value hy)))), forall (result7: double), forall (HW_39: (sub_double_post nearest_even y hy result7)), forall (ty: double), forall (HW_40: ty = result7), forall (result8: double), forall (HW_41: (neg_double_post xy result8)), (no_overflow_double nearest_even (Rmult (double_value hx) (double_value hy))). Proof. intuition; why2gappa. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H44; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H41; rewrite HW_21; rewrite H44; reflexivity. 2: rewrite H38; rewrite HW_24; rewrite H41. 2: rewrite Rplus_comm; reflexivity. rewrite VeltkampEven_gappa with 27%nat y py qy hy. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H32; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H29; rewrite HW_33; rewrite H32; reflexivity. 2: rewrite H26; rewrite HW_36; rewrite H32; rewrite H29. 2: rewrite Rplus_comm; reflexivity. simpl (P_of_succ_nat (52 - 27)). clear -H1 H0 H3. assert (Rabs (gappa_rounding (rounding_float roundNE 26 1074) x_0 * gappa_rounding (rounding_float roundNE 26 1074) y -x_0*y) <= powerRZ 2 2000)%R. gappa. case (Rle_or_lt 1 (Rabs x_0)). case (Rle_or_lt 1 (Rabs y)); intros. assert (1 <= Rabs x_0 <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. assert (1 <= Rabs y <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. clear H1 H0 H2 H4. gappa. assert (Rabs y <= 1)%R by (apply Rlt_le; exact H2). gappa. intros H4; assert (Rabs x_0 <= 1)%R by (apply Rlt_le; exact H4). gappa. Qed. (* Why obligation from file "Dekker.c", line 24, characters 5-14: *) (*Why goal*) Lemma Dekker_safety_po_11 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), forall (HW_29: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C)))), forall (result4: double), forall (HW_30: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_31: py = result4), forall (HW_32: (no_overflow_double nearest_even (Rminus (double_value y) (double_value py)))), forall (result5: double), forall (HW_33: (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_34: qy = result5), forall (HW_35: (no_overflow_double nearest_even (Rplus (double_value py) (double_value qy)))), forall (result6: double), forall (HW_36: (add_double_post nearest_even py qy result6)), forall (hy: double), forall (HW_37: hy = result6), forall (HW_38: (no_overflow_double nearest_even (Rminus (double_value y) (double_value hy)))), forall (result7: double), forall (HW_39: (sub_double_post nearest_even y hy result7)), forall (ty: double), forall (HW_40: ty = result7), forall (result8: double), forall (HW_41: (neg_double_post xy result8)), forall (HW_42: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value hy)))), forall (result9: double), forall (HW_43: (mul_double_post nearest_even hx hy result9)), (no_overflow_double nearest_even (Rplus (double_value result8) (double_value result9))). Proof. intuition;why2gappa. rewrite HW_41; rewrite H; rewrite HW_43. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H46; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H43; rewrite HW_21; rewrite H46; reflexivity. 2: rewrite H40; rewrite HW_24; rewrite H43; rewrite H46. 2: rewrite Rplus_comm; reflexivity. rewrite VeltkampEven_gappa with 27%nat y py qy hy. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H34; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H31; rewrite HW_33; rewrite H34; reflexivity. 2: rewrite H28; rewrite HW_36; rewrite H34; rewrite H31. 2: rewrite Rplus_comm; reflexivity. clear -H1 H0 H3. simpl (P_of_succ_nat (52 - 27)). assert (Rabs (gappa_rounding (rounding_float roundNE 26 1074) x_0 * gappa_rounding (rounding_float roundNE 26 1074) y -x_0*y) <= powerRZ 2 2000)%R. gappa. case (Rle_or_lt 1 (Rabs x_0)). case (Rle_or_lt 1 (Rabs y)); intros. assert (1 <= Rabs x_0 <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. assert (1 <= Rabs y <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. clear H1 H0 H2 H4. replace (- gappa_rounding (rounding_float roundNE 53 1074) (x_0 * y) + gappa_rounding (rounding_float roundNE 53 1074) (gappa_rounding (rounding_float roundNE 26 1074) x_0 * gappa_rounding (rounding_float roundNE 26 1074) y))%R with (gappa_rounding (rounding_float roundNE 53 1074) (gappa_rounding (rounding_float roundNE 26 1074) x_0 * gappa_rounding (rounding_float roundNE 26 1074) y) - gappa_rounding (rounding_float roundNE 53 1074) (x_0 * y))%R by ring. gappa. assert (Rabs y <= 1)%R by (apply Rlt_le; exact H2). gappa. intros H4; assert (Rabs x_0 <= 1)%R by (apply Rlt_le; exact H4). gappa. Save. (* Why obligation from file "Dekker.c", line 25, characters 6-11: *) (*Why goal*) Lemma Dekker_safety_po_12 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), forall (HW_29: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C)))), forall (result4: double), forall (HW_30: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_31: py = result4), forall (HW_32: (no_overflow_double nearest_even (Rminus (double_value y) (double_value py)))), forall (result5: double), forall (HW_33: (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_34: qy = result5), forall (HW_35: (no_overflow_double nearest_even (Rplus (double_value py) (double_value qy)))), forall (result6: double), forall (HW_36: (add_double_post nearest_even py qy result6)), forall (hy: double), forall (HW_37: hy = result6), forall (HW_38: (no_overflow_double nearest_even (Rminus (double_value y) (double_value hy)))), forall (result7: double), forall (HW_39: (sub_double_post nearest_even y hy result7)), forall (ty: double), forall (HW_40: ty = result7), forall (result8: double), forall (HW_41: (neg_double_post xy result8)), forall (HW_42: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value hy)))), forall (result9: double), forall (HW_43: (mul_double_post nearest_even hx hy result9)), forall (HW_44: (no_overflow_double nearest_even (Rplus (double_value result8) (double_value result9)))), forall (result10: double), forall (HW_45: (add_double_post nearest_even result8 result9 result10)), forall (r2: double), forall (HW_46: r2 = result10), (no_overflow_double nearest_even (Rmult (double_value hx) (double_value ty))). Proof. intuition; why2gappa. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H51; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H48; rewrite HW_21; rewrite H51; reflexivity. 2: rewrite H45; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. rewrite VeltkampTail_gappa with 27%nat y py qy hy ty. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H39; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H36; rewrite HW_33; reflexivity. 2: rewrite H33; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. 2: rewrite H30; rewrite HW_39; reflexivity. clear -H1 H0 H3. simpl ((P_of_succ_nat (52 - 27))). case (Rle_or_lt 1 (Rabs x_0)). case (Rle_or_lt 1 (Rabs y)); intros. assert (1 <= Rabs x_0 <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. assert (1 <= Rabs y <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. clear H1 H0 H2 H. replace ((gappa_rounding (rounding_float roundNE 26 1074) x_0 * (y - gappa_rounding (rounding_float roundNE 26 1074) y)))%R with (((gappa_rounding (rounding_float roundNE 26 1074) x_0 * y - x_0*y) +x_0*y) * (-1)*((gappa_rounding (rounding_float roundNE 26 1074) y - y)/y))%R. gappa. field. intro. absurd (1 <= Rabs y)%R. rewrite H; rewrite Rabs_R0; auto with real. apply H5. assert (Rabs y <= 1)%R by (apply Rlt_le; exact H). gappa. intros H; assert (Rabs x_0 <= 1)%R by (apply Rlt_le; exact H). gappa. Save. (* Why obligation from file "Dekker.c", line 25, characters 2-11: *) (*Why goal*) Lemma Dekker_safety_po_13 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), forall (HW_29: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C)))), forall (result4: double), forall (HW_30: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_31: py = result4), forall (HW_32: (no_overflow_double nearest_even (Rminus (double_value y) (double_value py)))), forall (result5: double), forall (HW_33: (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_34: qy = result5), forall (HW_35: (no_overflow_double nearest_even (Rplus (double_value py) (double_value qy)))), forall (result6: double), forall (HW_36: (add_double_post nearest_even py qy result6)), forall (hy: double), forall (HW_37: hy = result6), forall (HW_38: (no_overflow_double nearest_even (Rminus (double_value y) (double_value hy)))), forall (result7: double), forall (HW_39: (sub_double_post nearest_even y hy result7)), forall (ty: double), forall (HW_40: ty = result7), forall (result8: double), forall (HW_41: (neg_double_post xy result8)), forall (HW_42: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value hy)))), forall (result9: double), forall (HW_43: (mul_double_post nearest_even hx hy result9)), forall (HW_44: (no_overflow_double nearest_even (Rplus (double_value result8) (double_value result9)))), forall (result10: double), forall (HW_45: (add_double_post nearest_even result8 result9 result10)), forall (r2: double), forall (HW_46: r2 = result10), forall (HW_47: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value ty)))), forall (result11: double), forall (HW_48: (mul_double_post nearest_even hx ty result11)), (no_overflow_double nearest_even (Rplus (double_value r2) (double_value result11))). Proof. intuition; why2gappa. rewrite H29; rewrite HW_45; rewrite HW_48. rewrite HW_43; rewrite HW_41; rewrite H. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H53; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H50; rewrite HW_21; rewrite H53; reflexivity. 2: rewrite H47; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. rewrite VeltkampEven_gappa with 27%nat y py qy hy. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H41; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H38; rewrite HW_33; reflexivity. 2: rewrite H35; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. rewrite VeltkampTail_gappa with 27%nat y py qy hy ty. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H41; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H38; rewrite HW_33; reflexivity. 2: rewrite H35; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. 2: rewrite H32; rewrite HW_39; reflexivity. clear -H1 H0 H3. simpl ((P_of_succ_nat (52 - 27))). assert (Rabs (gappa_rounding (rounding_float roundNE 26 1074) x_0 * gappa_rounding (rounding_float roundNE 26 1074) y -x_0*y) <= powerRZ 2 2000)%R. gappa. case (Rle_or_lt 1 (Rabs x_0)). case (Rle_or_lt 1 (Rabs y)); intros. assert (1 <= Rabs x_0 <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. assert (1 <= Rabs y <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. clear H1 H0 H2 H4. replace (- gappa_rounding (rounding_float roundNE 53 1074) (x_0 * y) + gappa_rounding (rounding_float roundNE 53 1074) (gappa_rounding (rounding_float roundNE 26 1074) x_0 * gappa_rounding (rounding_float roundNE 26 1074) y))%R with (gappa_rounding (rounding_float roundNE 53 1074) (gappa_rounding (rounding_float roundNE 26 1074) x_0 * gappa_rounding (rounding_float roundNE 26 1074) y) - gappa_rounding (rounding_float roundNE 53 1074) (x_0 * y))%R by ring. replace ((gappa_rounding (rounding_float roundNE 26 1074) x_0 * (y - gappa_rounding (rounding_float roundNE 26 1074) y)))%R with (((gappa_rounding (rounding_float roundNE 26 1074) x_0 * y - x_0*y) +x_0*y) * (-1)*((gappa_rounding (rounding_float roundNE 26 1074) y - y)/y))%R. gappa. field. intro. absurd (1 <= Rabs y)%R. rewrite H0; rewrite Rabs_R0; auto with real. apply H6. assert (Rabs y <= 1)%R by (apply Rlt_le; exact H2). gappa. intros H4; assert (Rabs x_0 <= 1)%R by (apply Rlt_le; exact H4). gappa. Save. (* Why obligation from file "Dekker.c", line 26, characters 6-11: *) (*Why goal*) Lemma Dekker_safety_po_14 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), forall (HW_29: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C)))), forall (result4: double), forall (HW_30: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_31: py = result4), forall (HW_32: (no_overflow_double nearest_even (Rminus (double_value y) (double_value py)))), forall (result5: double), forall (HW_33: (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_34: qy = result5), forall (HW_35: (no_overflow_double nearest_even (Rplus (double_value py) (double_value qy)))), forall (result6: double), forall (HW_36: (add_double_post nearest_even py qy result6)), forall (hy: double), forall (HW_37: hy = result6), forall (HW_38: (no_overflow_double nearest_even (Rminus (double_value y) (double_value hy)))), forall (result7: double), forall (HW_39: (sub_double_post nearest_even y hy result7)), forall (ty: double), forall (HW_40: ty = result7), forall (result8: double), forall (HW_41: (neg_double_post xy result8)), forall (HW_42: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value hy)))), forall (result9: double), forall (HW_43: (mul_double_post nearest_even hx hy result9)), forall (HW_44: (no_overflow_double nearest_even (Rplus (double_value result8) (double_value result9)))), forall (result10: double), forall (HW_45: (add_double_post nearest_even result8 result9 result10)), forall (r2: double), forall (HW_46: r2 = result10), forall (HW_47: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value ty)))), forall (result11: double), forall (HW_48: (mul_double_post nearest_even hx ty result11)), forall (HW_49: (no_overflow_double nearest_even (Rplus (double_value r2) (double_value result11)))), forall (result12: double), forall (HW_50: (add_double_post nearest_even r2 result11 result12)), forall (r2_0: double), forall (HW_51: r2_0 = result12), (no_overflow_double nearest_even (Rmult (double_value hy) (double_value tx))). Proof. intuition; why2gappa. rewrite VeltkampEven_gappa with 27%nat y py qy hy. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H46; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H43; rewrite HW_33; reflexivity. 2: rewrite H40; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. rewrite VeltkampTail_gappa with 27%nat x_0 px qx hx tx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H58; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H55; rewrite HW_21; rewrite H58; reflexivity. 2: rewrite H52; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. 2: rewrite H49; rewrite HW_27; reflexivity. clear -H1 H0 H3. simpl ((P_of_succ_nat (52 - 27))). case (Rle_or_lt 1 (Rabs x_0)). case (Rle_or_lt 1 (Rabs y)); intros. assert (1 <= Rabs x_0 <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. assert (1 <= Rabs y <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. clear H1 H0 H2 H. replace ((gappa_rounding (rounding_float roundNE 26 1074) y * (x_0 - gappa_rounding (rounding_float roundNE 26 1074) x_0)))%R with (((x_0*gappa_rounding (rounding_float roundNE 26 1074) y - x_0*y) +x_0*y) * (-1)*((gappa_rounding (rounding_float roundNE 26 1074) x_0 - x_0)/x_0))%R. gappa. field. intro. absurd (1 <= Rabs x_0)%R. rewrite H; rewrite Rabs_R0; auto with real. apply H4. assert (Rabs y <= 1)%R by (apply Rlt_le; exact H). gappa. intros H2; assert (Rabs x_0 <= 1)%R by (apply Rlt_le; exact H2). gappa. Save. (* Why obligation from file "Dekker.c", line 26, characters 2-11: *) (*Why goal*) Lemma Dekker_safety_po_15 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), forall (HW_29: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C)))), forall (result4: double), forall (HW_30: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_31: py = result4), forall (HW_32: (no_overflow_double nearest_even (Rminus (double_value y) (double_value py)))), forall (result5: double), forall (HW_33: (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_34: qy = result5), forall (HW_35: (no_overflow_double nearest_even (Rplus (double_value py) (double_value qy)))), forall (result6: double), forall (HW_36: (add_double_post nearest_even py qy result6)), forall (hy: double), forall (HW_37: hy = result6), forall (HW_38: (no_overflow_double nearest_even (Rminus (double_value y) (double_value hy)))), forall (result7: double), forall (HW_39: (sub_double_post nearest_even y hy result7)), forall (ty: double), forall (HW_40: ty = result7), forall (result8: double), forall (HW_41: (neg_double_post xy result8)), forall (HW_42: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value hy)))), forall (result9: double), forall (HW_43: (mul_double_post nearest_even hx hy result9)), forall (HW_44: (no_overflow_double nearest_even (Rplus (double_value result8) (double_value result9)))), forall (result10: double), forall (HW_45: (add_double_post nearest_even result8 result9 result10)), forall (r2: double), forall (HW_46: r2 = result10), forall (HW_47: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value ty)))), forall (result11: double), forall (HW_48: (mul_double_post nearest_even hx ty result11)), forall (HW_49: (no_overflow_double nearest_even (Rplus (double_value r2) (double_value result11)))), forall (result12: double), forall (HW_50: (add_double_post nearest_even r2 result11 result12)), forall (r2_0: double), forall (HW_51: r2_0 = result12), forall (HW_52: (no_overflow_double nearest_even (Rmult (double_value hy) (double_value tx)))), forall (result13: double), forall (HW_53: (mul_double_post nearest_even hy tx result13)), (no_overflow_double nearest_even (Rplus (double_value r2_0) (double_value result13))). Proof. intuition; why2gappa. rewrite H33; rewrite HW_50; rewrite HW_53. rewrite HW_48; rewrite H36; rewrite HW_45. rewrite HW_43; rewrite HW_41; rewrite H. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H60; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H57; rewrite HW_21; rewrite H60; reflexivity. 2: rewrite H54; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. rewrite VeltkampTail_gappa with 27%nat x_0 px qx hx tx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H60; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H57; rewrite HW_21; rewrite H60; reflexivity. 2: rewrite H54; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. 2: rewrite H51; rewrite HW_27; reflexivity. rewrite VeltkampEven_gappa with 27%nat y py qy hy. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H48; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H45; rewrite HW_33; reflexivity. 2: rewrite H42; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. rewrite VeltkampTail_gappa with 27%nat y py qy hy ty. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H48; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H45; rewrite HW_33; reflexivity. 2: rewrite H42; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. 2: rewrite H39; rewrite HW_39; reflexivity. clear -H1 H0 H3. simpl ((P_of_succ_nat (52 - 27))). assert (Rabs (gappa_rounding (rounding_float roundNE 26 1074) x_0 * gappa_rounding (rounding_float roundNE 26 1074) y -x_0*y) <= powerRZ 2 2000)%R. gappa. case (Rle_or_lt 1 (Rabs x_0)). case (Rle_or_lt 1 (Rabs y)); intros. assert (1 <= Rabs x_0 <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. assert (1 <= Rabs y <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. clear H1 H0 H2 H4. replace (- gappa_rounding (rounding_float roundNE 53 1074) (x_0* y) + gappa_rounding (rounding_float roundNE 53 1074) (gappa_rounding (rounding_float roundNE 26 1074) x_0* gappa_rounding (rounding_float roundNE 26 1074) y))%R with (gappa_rounding (rounding_float roundNE 53 1074) (gappa_rounding (rounding_float roundNE 26 1074) x_0* gappa_rounding (rounding_float roundNE 26 1074) y) - gappa_rounding (rounding_float roundNE 53 1074) (x_0* y))%R by ring. replace ((gappa_rounding (rounding_float roundNE 26 1074) x_0* (y - gappa_rounding (rounding_float roundNE 26 1074) y)))%R with (((gappa_rounding (rounding_float roundNE 26 1074) x_0* y - x_0*y) +x_0*y) * (-1)*((gappa_rounding (rounding_float roundNE 26 1074) y - y)/y))%R. replace ((gappa_rounding (rounding_float roundNE 26 1074) y * (x_0- gappa_rounding (rounding_float roundNE 26 1074) x_0)))%R with (((x_0*gappa_rounding (rounding_float roundNE 26 1074) y - x_0*y) +x_0*y) * (-1)*((gappa_rounding (rounding_float roundNE 26 1074) x_0- x_0)/x_0))%R. gappa. field. intro. absurd (1 <= Rabs x_0)%R. rewrite H0; rewrite Rabs_R0; auto with real. apply H5. field. intro. absurd (1 <= Rabs y)%R. rewrite H0; rewrite Rabs_R0; auto with real. apply H6. assert (Rabs y <= 1)%R by (apply Rlt_le; exact H2). gappa. intros. assert (Rabs x_0<= 1)%R by (apply Rlt_le; exact H2). gappa. Save. (* Why obligation from file "Dekker.c", line 27, characters 6-11: *) (*Why goal*) Lemma Dekker_safety_po_16 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), forall (HW_29: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C)))), forall (result4: double), forall (HW_30: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_31: py = result4), forall (HW_32: (no_overflow_double nearest_even (Rminus (double_value y) (double_value py)))), forall (result5: double), forall (HW_33: (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_34: qy = result5), forall (HW_35: (no_overflow_double nearest_even (Rplus (double_value py) (double_value qy)))), forall (result6: double), forall (HW_36: (add_double_post nearest_even py qy result6)), forall (hy: double), forall (HW_37: hy = result6), forall (HW_38: (no_overflow_double nearest_even (Rminus (double_value y) (double_value hy)))), forall (result7: double), forall (HW_39: (sub_double_post nearest_even y hy result7)), forall (ty: double), forall (HW_40: ty = result7), forall (result8: double), forall (HW_41: (neg_double_post xy result8)), forall (HW_42: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value hy)))), forall (result9: double), forall (HW_43: (mul_double_post nearest_even hx hy result9)), forall (HW_44: (no_overflow_double nearest_even (Rplus (double_value result8) (double_value result9)))), forall (result10: double), forall (HW_45: (add_double_post nearest_even result8 result9 result10)), forall (r2: double), forall (HW_46: r2 = result10), forall (HW_47: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value ty)))), forall (result11: double), forall (HW_48: (mul_double_post nearest_even hx ty result11)), forall (HW_49: (no_overflow_double nearest_even (Rplus (double_value r2) (double_value result11)))), forall (result12: double), forall (HW_50: (add_double_post nearest_even r2 result11 result12)), forall (r2_0: double), forall (HW_51: r2_0 = result12), forall (HW_52: (no_overflow_double nearest_even (Rmult (double_value hy) (double_value tx)))), forall (result13: double), forall (HW_53: (mul_double_post nearest_even hy tx result13)), forall (HW_54: (no_overflow_double nearest_even (Rplus (double_value r2_0) (double_value result13)))), forall (result14: double), forall (HW_55: (add_double_post nearest_even r2_0 result13 result14)), forall (r2_1: double), forall (HW_56: r2_1 = result14), (no_overflow_double nearest_even (Rmult (double_value tx) (double_value ty))). Proof. intuition; why2gappa. rewrite VeltkampTail_gappa with 27%nat x_0 px qx hx tx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H65; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H62; rewrite HW_21; rewrite H65; reflexivity. 2: rewrite H59; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. 2: rewrite H56; rewrite HW_27; reflexivity. rewrite VeltkampTail_gappa with 27%nat y py qy hy ty. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H53; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H50; rewrite HW_33; reflexivity. 2: rewrite H47; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. 2: rewrite H44; rewrite HW_39; reflexivity. clear -H1 H0 H3. simpl ((P_of_succ_nat (52 - 27))). case (Rle_or_lt 1 (Rabs x_0)). case (Rle_or_lt 1 (Rabs y)); intros. assert (1 <= Rabs x_0 <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. assert (1 <= Rabs y <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. clear H1 H0 H2 H. replace ((x_0 - gappa_rounding (rounding_float roundNE 26 1074) x_0) * (y - gappa_rounding (rounding_float roundNE 26 1074) y))%R with ((x_0*y)*((gappa_rounding (rounding_float roundNE 26 1074) x_0 - x_0)/x_0) *((gappa_rounding (rounding_float roundNE 26 1074) y - y)/y))%R. gappa. field. split; intro. absurd (1 <= Rabs y)%R. rewrite H; rewrite Rabs_R0; auto with real. apply H5. absurd (1 <= Rabs x_0)%R. rewrite H; rewrite Rabs_R0; auto with real. apply H4. assert (Rabs y <= 1)%R by (apply Rlt_le; exact H). gappa. intros. assert (Rabs x_0 <= 1)%R by (apply Rlt_le; exact H). gappa. Save. (* Why obligation from file "Dekker.c", line 27, characters 2-11: *) (*Why goal*) Lemma Dekker_safety_po_17 : forall (x_0: double), forall (y: double), forall (xy: double), forall (HW_1: (* JC_11 *) ((* JC_7 *) (eq (double_value xy) (round_double nearest_even (Rmult (double_value x_0) ( double_value y)))) /\ (* JC_8 *) (Rle (Rabs (double_value x_0)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_9 *) (Rle (Rabs (double_value y)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_10 *) (Rle (Rabs (Rmult (double_value x_0) (double_value y))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_13: (no_overflow_double nearest_even (134217729)%R)), forall (result: double), forall (HW_14: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_15: C = result), forall (HW_16: (* JC_18 *) (eq (double_value C) (Rplus (1 * 134217728)%R (1)%R))), forall (HW_17: (no_overflow_double nearest_even (Rmult (double_value x_0) (double_value C)))), forall (result0: double), forall (HW_18: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_19: px = result0), forall (HW_20: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value px)))), forall (result1: double), forall (HW_21: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_22: qx = result1), forall (HW_23: (no_overflow_double nearest_even (Rplus (double_value px) (double_value qx)))), forall (result2: double), forall (HW_24: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_25: hx = result2), forall (HW_26: (no_overflow_double nearest_even (Rminus (double_value x_0) (double_value hx)))), forall (result3: double), forall (HW_27: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_28: tx = result3), forall (HW_29: (no_overflow_double nearest_even (Rmult (double_value y) (double_value C)))), forall (result4: double), forall (HW_30: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_31: py = result4), forall (HW_32: (no_overflow_double nearest_even (Rminus (double_value y) (double_value py)))), forall (result5: double), forall (HW_33: (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_34: qy = result5), forall (HW_35: (no_overflow_double nearest_even (Rplus (double_value py) (double_value qy)))), forall (result6: double), forall (HW_36: (add_double_post nearest_even py qy result6)), forall (hy: double), forall (HW_37: hy = result6), forall (HW_38: (no_overflow_double nearest_even (Rminus (double_value y) (double_value hy)))), forall (result7: double), forall (HW_39: (sub_double_post nearest_even y hy result7)), forall (ty: double), forall (HW_40: ty = result7), forall (result8: double), forall (HW_41: (neg_double_post xy result8)), forall (HW_42: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value hy)))), forall (result9: double), forall (HW_43: (mul_double_post nearest_even hx hy result9)), forall (HW_44: (no_overflow_double nearest_even (Rplus (double_value result8) (double_value result9)))), forall (result10: double), forall (HW_45: (add_double_post nearest_even result8 result9 result10)), forall (r2: double), forall (HW_46: r2 = result10), forall (HW_47: (no_overflow_double nearest_even (Rmult (double_value hx) (double_value ty)))), forall (result11: double), forall (HW_48: (mul_double_post nearest_even hx ty result11)), forall (HW_49: (no_overflow_double nearest_even (Rplus (double_value r2) (double_value result11)))), forall (result12: double), forall (HW_50: (add_double_post nearest_even r2 result11 result12)), forall (r2_0: double), forall (HW_51: r2_0 = result12), forall (HW_52: (no_overflow_double nearest_even (Rmult (double_value hy) (double_value tx)))), forall (result13: double), forall (HW_53: (mul_double_post nearest_even hy tx result13)), forall (HW_54: (no_overflow_double nearest_even (Rplus (double_value r2_0) (double_value result13)))), forall (result14: double), forall (HW_55: (add_double_post nearest_even r2_0 result13 result14)), forall (r2_1: double), forall (HW_56: r2_1 = result14), forall (HW_57: (no_overflow_double nearest_even (Rmult (double_value tx) (double_value ty)))), forall (result15: double), forall (HW_58: (mul_double_post nearest_even tx ty result15)), (no_overflow_double nearest_even (Rplus (double_value r2_1) (double_value result15))). Proof. intuition; why2gappa. rewrite H37; rewrite HW_55; rewrite HW_58. rewrite HW_53; rewrite H40; rewrite HW_50. rewrite HW_48; rewrite H43; rewrite HW_45. rewrite HW_43; rewrite HW_41; rewrite H. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H67; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H64; rewrite HW_21; rewrite H67; reflexivity. 2: rewrite H61; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. rewrite VeltkampTail_gappa with 27%nat x_0 px qx hx tx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H67; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H64; rewrite HW_21; rewrite H67; reflexivity. 2: rewrite H61; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. 2: rewrite H58; rewrite HW_27; reflexivity. rewrite VeltkampEven_gappa with 27%nat y py qy hy. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H55; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H52; rewrite HW_33; reflexivity. 2: rewrite H49; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. rewrite VeltkampTail_gappa with 27%nat y py qy hy ty. 2: split; auto with zarith arith. 2: assumption. 2: rewrite H55; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite H52; rewrite HW_33; reflexivity. 2: rewrite H49; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. 2: rewrite H46; rewrite HW_39; reflexivity. clear -H1 H0 H3. simpl ((P_of_succ_nat (52 - 27))). assert (Rabs (gappa_rounding (rounding_float roundNE 26 1074) x_0 * gappa_rounding (rounding_float roundNE 26 1074) y -x_0*y) <= powerRZ 2 2000)%R. gappa. case (Rle_or_lt 1 (Rabs x_0)). case (Rle_or_lt 1 (Rabs y)); intros. assert (1 <= Rabs x_0 <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. assert (1 <= Rabs y <= 1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. clear H1 H0 H2 H4. replace (- gappa_rounding (rounding_float roundNE 53 1074) (x_0 * y) + gappa_rounding (rounding_float roundNE 53 1074) (gappa_rounding (rounding_float roundNE 26 1074) x_0 * gappa_rounding (rounding_float roundNE 26 1074) y))%R with (gappa_rounding (rounding_float roundNE 53 1074) (gappa_rounding (rounding_float roundNE 26 1074) x_0 * gappa_rounding (rounding_float roundNE 26 1074) y) - gappa_rounding (rounding_float roundNE 53 1074) (x_0 * y))%R by ring. replace ((gappa_rounding (rounding_float roundNE 26 1074) x_0 * (y - gappa_rounding (rounding_float roundNE 26 1074) y)))%R with (((gappa_rounding (rounding_float roundNE 26 1074) x_0 * y - x_0*y) +x_0*y) * (-1)*((gappa_rounding (rounding_float roundNE 26 1074) y - y)/y))%R. replace ((gappa_rounding (rounding_float roundNE 26 1074) y * (x_0 - gappa_rounding (rounding_float roundNE 26 1074) x_0)))%R with (((x_0*gappa_rounding (rounding_float roundNE 26 1074) y - x_0*y) +x_0*y) * (-1)*((gappa_rounding (rounding_float roundNE 26 1074) x_0 - x_0)/x_0))%R. replace ((x_0 - gappa_rounding (rounding_float roundNE 26 1074) x_0) * (y - gappa_rounding (rounding_float roundNE 26 1074) y))%R with ((x_0*y)*((gappa_rounding (rounding_float roundNE 26 1074) x_0 - x_0)/x_0) *((gappa_rounding (rounding_float roundNE 26 1074) y - y)/y))%R. gappa. field. split; intro. absurd (1 <= Rabs y)%R. rewrite H0; rewrite Rabs_R0; auto with real. apply H6. absurd (1 <= Rabs x_0)%R. rewrite H0; rewrite Rabs_R0; auto with real. apply H5. field; intro. absurd (1 <= Rabs x_0)%R. rewrite H0; rewrite Rabs_R0; auto with real. apply H5. field; intro. absurd (1 <= Rabs y)%R. rewrite H0; rewrite Rabs_R0; auto with real. apply H6. assert (Rabs y <= 1)%R by (apply Rlt_le; exact H2). gappa. intros. assert (Rabs x_0 <= 1)%R by (apply Rlt_le; exact H2). gappa. Save.