Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Require Export Why2Gappa. Require Export "discriminant3". Require Export "Dekker". Require Export WhyFloatsStrictLegacy. Coercion Local FtoRradix := FtoR radix. Lemma FTRr: forall x, WhyFloatsStrictLegacy.FtoRradix x= FtoRradix x. intros; reflexivity. Qed. Section Discriminant_again. 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. 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 = round radix2 (FLT_exp (-1074) 53) rndNE (x * (powerRZ radix s + 1)) -> FtoRradix q = round radix2 (FLT_exp (-1074) 53) rndNE (x-p) -> FtoRradix hx = round radix2 (FLT_exp (-1074) 53) rndNE (q+p) -> FtoRradix hx = round radix2 (FLT_exp (-1074) (53-s)) rndNE x. Proof with auto with typeclass_instances. intros. destruct equiv_RNDs_aux2 with bdouble 53%nat p as (p',(H4,H5));auto with zarith. rewrite H1; apply generic_format_round... destruct equiv_RNDs_aux2 with bdouble 53%nat q as (q',(H7,H8)); auto with zarith. rewrite H2; apply generic_format_round... destruct equiv_RNDs_aux2 with bdouble 53%nat hx as (hx',(H10,H11)); auto with zarith. rewrite H3; apply generic_format_round... generalize EvenClosestCompatible; unfold CompatibleP; intros T'. destruct VeltkampEven with radix bdouble s 53%nat x p' q' hx' as (hx'',(H13,H14)); try apply pdGivesBound; auto with zarith arith. apply T' with (x * (powerRZ radix s + 1))%R (RND_EvenClosest bdouble 2 53 (x * (powerRZ radix s + 1))%R); try apply pdGivesBound; auto with zarith. rewrite equiv_RNDs; try apply pdGivesBound; auto with zarith. apply trans_eq with p. rewrite H1; reflexivity. rewrite <- H4; reflexivity. apply T' with (x-p)%R (RND_EvenClosest bdouble 2 53 (x -p)%R); try apply pdGivesBound; auto with zarith. rewrite <- H4; reflexivity. rewrite equiv_RNDs; try apply pdGivesBound; auto with zarith. apply trans_eq with q. rewrite H2; reflexivity. rewrite <- H7; reflexivity. apply T' with (q+p)%R (RND_EvenClosest bdouble 2 53 (q+p)%R); try apply pdGivesBound; auto with zarith. rewrite <- H4, <- H7; reflexivity. rewrite equiv_RNDs; try apply pdGivesBound; auto with zarith. apply trans_eq with hx. rewrite H3; reflexivity. rewrite <- H10; reflexivity. (* *) apply trans_eq with (hx''). rewrite <- H10; unfold FtoRradix; rewrite H13; reflexivity. apply trans_eq with (RND_EvenClosest (Bound (P_of_succ_nat (Peano.pred (Zabs_nat (Zpower_nat radix (53 - s))))) (dExp bdouble)) 2 (53-s)%nat x). generalize EvenClosestUniqueP; unfold UniqueP; intros T. unfold FtoRradix; apply T with (Bound (P_of_succ_nat (Peano.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 H14. apply RND_EvenClosest_correct; try apply p''GivesBound; auto with zarith. rewrite equiv_RNDs; try apply p''GivesBound; auto with zarith. apply f_equal3; try reflexivity. apply f_equal; try reflexivity. rewrite inj_minus1; auto with arith zarith. Qed. Theorem VeltkampTail_gappa: (2 <= s <= 51)%nat -> Fcanonic radix bdouble x -> FtoRradix p = round radix2 (FLT_exp (-1074) 53) rndNE (x * (powerRZ radix s + 1)) -> FtoRradix q = round radix2 (FLT_exp (-1074) 53) rndNE (x-p) -> FtoRradix hx = round radix2 (FLT_exp (-1074) 53) rndNE (q+p) -> FtoRradix tx = round radix2 (FLT_exp (-1074) 53) rndNE (x-hx) -> (FtoRradix tx = x - round radix2 (FLT_exp (-1074) (53-s)) rndNE x)%R. Proof with auto with typeclass_instances. intros. apply trans_eq with (x-hx)%R. destruct equiv_RNDs_aux2 with bdouble 53%nat p as (p',(H6,H5));auto with zarith. rewrite H1; apply generic_format_round... destruct equiv_RNDs_aux2 with bdouble 53%nat q as (q',(H7,H8)); auto with zarith. rewrite H2; apply generic_format_round... destruct equiv_RNDs_aux2 with bdouble 53%nat hx as (hx',(H10,H11)); auto with zarith. rewrite H3; apply generic_format_round... destruct equiv_RNDs_aux2 with bdouble 53%nat tx as (tx',(H12,H13)); auto with zarith. rewrite H4; apply generic_format_round... generalize EvenClosestCompatible; unfold CompatibleP; intros T'. assert (Y:(forall b radix p r x, EvenClosest b radix p r x -> Closest b radix r x)). intros b radix p0 r x0 K; apply K. 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. apply Y with 53; apply T' with (x * (powerRZ radix s + 1))%R (RND_EvenClosest bdouble 2 53 (x * (powerRZ radix s + 1))%R); try apply pdGivesBound; auto with zarith. rewrite equiv_RNDs; try apply pdGivesBound; auto with zarith. apply trans_eq with p. rewrite H1; reflexivity. rewrite <- H6; reflexivity. apply Y with 53; apply T' with (x-p)%R (RND_EvenClosest bdouble 2 53 (x -p)%R); try apply pdGivesBound; auto with zarith. rewrite <- H6; reflexivity. rewrite equiv_RNDs; try apply pdGivesBound; auto with zarith. apply trans_eq with q. rewrite H2; reflexivity. rewrite <- H7; reflexivity. apply Y with 53; apply T' with (q+p)%R (RND_EvenClosest bdouble 2 53 (q+p)%R); try apply pdGivesBound; auto with zarith. rewrite <- H6, <- H7; reflexivity. rewrite equiv_RNDs; try apply pdGivesBound; auto with zarith. apply trans_eq with hx. rewrite H3; reflexivity. rewrite <- H10; reflexivity. apply Y with 53; apply T' with (x-hx)%R (RND_EvenClosest bdouble 2 53 (x-hx)%R); try apply pdGivesBound; auto with zarith. rewrite <- H10; reflexivity. fold FtoRradix; rewrite equiv_RNDs; try apply pdGivesBound; auto with zarith. apply trans_eq with tx. rewrite H4; reflexivity. rewrite <- H12; reflexivity. fold FtoRradix in T1, T2. rewrite <- T2, T1, <- H12, <- H10. unfold WhyFloatsStrictLegacy.FtoRradix,FtoRradix;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 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: (double_of_real_post nearest_even (134217729)%R result)), forall (C: double), forall (HW_14: C = result), (* 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: (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: (mul_double_post nearest_even x_0 C result0)), forall (px: double), forall (HW_17: px = result0), forall (result1: double), forall (HW_18: (sub_double_post nearest_even x_0 px result1)), forall (qx: double), forall (HW_19: qx = result1), forall (result2: double), forall (HW_20: (add_double_post nearest_even px qx result2)), forall (hx: double), forall (HW_21: hx = result2), forall (result3: double), forall (HW_22: (sub_double_post nearest_even x_0 hx result3)), forall (tx: double), forall (HW_23: tx = result3), forall (result4: double), forall (HW_24: (mul_double_post nearest_even y C result4)), forall (py: double), forall (HW_25: py = result4), forall (result5: double), forall (HW_26: (sub_double_post nearest_even y py result5)), forall (qy: double), forall (HW_27: qy = result5), forall (result6: double), forall (HW_28: (add_double_post nearest_even py qy result6)), forall (hy: double), forall (HW_29: hy = result6), forall (result7: double), forall (HW_30: (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: (mul_double_post nearest_even hx hy result9)), forall (result10: double), forall (HW_34: (add_double_post nearest_even result8 result9 result10)), forall (r2: double), forall (HW_35: r2 = result10), forall (result11: double), forall (HW_36: (mul_double_post nearest_even hx ty result11)), forall (result12: double), forall (HW_37: (add_double_post nearest_even r2 result11 result12)), forall (r2_0: double), forall (HW_38: r2_0 = result12), forall (result13: double), forall (HW_39: (mul_double_post nearest_even hy tx result13)), forall (result14: double), forall (HW_40: (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: (mul_double_post nearest_even tx ty result15)), forall (result16: double), forall (HW_43: (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 <- FTRr; rewrite H74; assumption. apply FcanonicBound with radix; assumption. rewrite <- FTRr; 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 <- FTRr, H71; 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 <- FTRr, H68; 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 <- FTRr, H65; 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 <- FTRr, H62; assumption. apply FcanonicBound with radix; assumption. rewrite <- FTRr, 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 <- FTRr, H59; 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 <- FTRr, H56; 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 <- FTRr, H53; 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 <- FTRr; destruct HW_32 as (Y1,_); unfold double_value in Y1; simpl in Y1. rewrite Y1, FTRr; 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 <- FTRr, H50, FTRr; 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 <- FTRr, H47, FTRr; 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 <- FTRr, H44, FTRr; unfold FtoRradix; rewrite Fopp_correct; ring. repeat rewrite Fopp_correct. apply f_equal; fold FtoRradix. rewrite <- (FTRr result16), HW_43; reflexivity. apply oppBounded. apply FcanonicBound with radix; assumption. assumption. rewrite H2,H38, H41, FTRr, (FTRr result16). rewrite <- (Ropp_involutive (FtoRradix result16)). unfold FtoRradix; rewrite <- (Fopp_correct). fold FtoRradix; rewrite Z1, Z2. simpl; ring. (* no underflow *) why2float. assert ((53 - div2 53)%nat = 27%nat) by reflexivity. unfold WhyFloatsStrictLegacy.FtoRradix; fold FtoRradix. 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. unfold WhyFloatsStrictLegacy.FtoRradix in H2; apply Rle_trans with (2:=H2). unfold Rdiv; rewrite Rmult_1_l. simpl. right; apply f_equal. rewrite Rmult_1_r. reflexivity. intro; Contradict H2. unfold WhyFloatsStrictLegacy.FtoRradix; fold FtoRradix; rewrite H81; 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 <- FTRr; rewrite H74; assumption. apply FcanonicBound with radix; assumption. rewrite <- FTRr; 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 <- FTRr, H71; 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 <- FTRr, H68; 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 <- FTRr, H65; 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. apply f_equal. rewrite <- FTRr, HW_15; simpl; ring. fold FtoRradix; apply sym_eq; rewrite <- FTRr, H62; assumption. apply FcanonicBound with radix; assumption. rewrite <- FTRr, 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 <- FTRr, H59; 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 <- FTRr, H56; 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 <- FTRr, H53; 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 <- FTRr; destruct HW_32 as (Y1,_); unfold double_value in Y1; simpl in Y1. rewrite Y1, FTRr; 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 <- FTRr, H50, FTRr; 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 <- FTRr, H47, FTRr; 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 <- FTRr, H44, FTRr; unfold FtoRradix; rewrite Fopp_correct; ring. repeat rewrite Fopp_correct. apply f_equal; fold FtoRradix. rewrite <- (FTRr why__return), H38, H41. rewrite HW_43; reflexivity. 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 70, 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. unfold WhyFloatsStrictLegacy.FtoRradix; fold FtoRradix. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite <- FTRr, H42; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H39; rewrite HW_21; rewrite <- (FTRr px), H42; reflexivity. 2: rewrite <- FTRr, H36; rewrite HW_24; rewrite <- (FTRr qx), H39. 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 <- FTRr, H30; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H27; rewrite HW_33; rewrite <- (FTRr py), H30; reflexivity. 2: rewrite <- FTRr, H24; rewrite HW_36; rewrite <- (FTRr py), H30; rewrite <- (FTRr qy), H27. 2: rewrite Rplus_comm; reflexivity. replace (53-Z_of_nat 27)%Z with 26%Z. clear -H1 H0 H3. rewrite Rmult_1_l in H1, H0, H3. unfold WhyFloatsStrictLegacy.FtoRradix in H1, H0, H3; fold FtoRradix in H1, H0, H3. assert (Rabs (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * round radix2 (FLT_exp (-1074) 26) ZnearestE 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 <= 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. assert (1 <= Rabs y <= 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. auto with zarith. 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. destruct HW_41 as (Y1,_); unfold double_value in Y1; simpl in Y1. rewrite Y1; rewrite H; rewrite HW_43. unfold WhyFloatsStrictLegacy.FtoRradix; fold FtoRradix. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite <- FTRr, H44; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H41; rewrite HW_21; rewrite <- (FTRr px), H44; reflexivity. 2: rewrite <- FTRr, H38; rewrite HW_24; rewrite <- (FTRr qx), 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 <- FTRr, H32; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H29; rewrite HW_33; rewrite <- (FTRr py), H32; reflexivity. 2: rewrite <- FTRr, H26; rewrite HW_36; rewrite <- (FTRr py), H32; rewrite <- (FTRr qy), H29. 2: rewrite Rplus_comm; reflexivity. replace (53-Z_of_nat 27)%Z with 26%Z by auto with zarith. clear -H1 H0 H3. rewrite Rmult_1_l in H1, H0, H3. unfold WhyFloatsStrictLegacy.FtoRradix in H1, H0, H3; fold FtoRradix in H1, H0, H3. assert (Rabs (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * round radix2 (FLT_exp (-1074) 26) ZnearestE 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 <= 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. assert (1 <= Rabs y <= 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R. split; assumption. clear H1 H0 H2 H4. replace (- round radix2 (FLT_exp (-1074) 53) ZnearestE (x_0 * y) + round radix2 (FLT_exp (-1074) 53) ZnearestE (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * round radix2 (FLT_exp (-1074) 26) ZnearestE y))%R with (round radix2 (FLT_exp (-1074) 53) ZnearestE (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * round radix2 (FLT_exp (-1074) 26) ZnearestE y) - round radix2 (FLT_exp (-1074) 53) ZnearestE (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. unfold WhyFloatsStrictLegacy.FtoRradix; fold FtoRradix. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite <- FTRr, H49; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H46; rewrite HW_21; rewrite <- (FTRr px), H49; reflexivity. 2: rewrite <- FTRr, H43; rewrite HW_24; rewrite <- (FTRr qx), H46. 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 <- FTRr, H37; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H34; rewrite HW_33; reflexivity. 2: rewrite <- FTRr, H31; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. 2: rewrite <- FTRr, H28; rewrite HW_39; reflexivity. clear -H1 H0 H3. replace (53-Z_of_nat 27)%Z with 26%Z by auto with zarith. unfold WhyFloatsStrictLegacy.FtoRradix in H1, H0, H3; fold FtoRradix in H1, H0, H3. 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 (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * (y - round radix2 (FLT_exp (-1074) 26) ZnearestE y))%R with (((round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * y - x_0*y) + x_0*y) * (-1) * ((round radix2 (FLT_exp (-1074) 26) ZnearestE 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 H27; rewrite HW_45; rewrite HW_48. destruct HW_41 as (Y1,_); unfold double_value in Y1; simpl in Y1. rewrite HW_43; rewrite Y1; rewrite H. unfold WhyFloatsStrictLegacy.FtoRradix; fold FtoRradix. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite <- FTRr, H51; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H48; rewrite HW_21; rewrite <- (FTRr px), H51; reflexivity. 2: rewrite <- FTRr, H45; rewrite HW_24; rewrite <- (FTRr qx), H48. 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 <- FTRr, H39; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H36; rewrite HW_33; rewrite <- (FTRr py), H39; reflexivity. 2: rewrite <- FTRr, H33; rewrite HW_36; rewrite <- (FTRr qy), H36. 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 <- FTRr, H39; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H36; rewrite HW_33; reflexivity. 2: rewrite <- FTRr, H33; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. 2: rewrite <- FTRr, H30; rewrite HW_39; reflexivity. clear -H1 H0 H3. replace (53-Z_of_nat 27)%Z with 26%Z by auto with zarith. unfold WhyFloatsStrictLegacy.FtoRradix in H1, H0, H3; fold FtoRradix in H1, H0, H3. assert (Rabs (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * round radix2 (FLT_exp (-1074) 26) ZnearestE 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 (- round radix2 (FLT_exp (-1074) 53) ZnearestE (x_0 * y) + round radix2 (FLT_exp (-1074) 53) ZnearestE (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * round radix2 (FLT_exp (-1074) 26) ZnearestE y))%R with (round radix2 (FLT_exp (-1074) 53) ZnearestE (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * round radix2 (FLT_exp (-1074) 26) ZnearestE y) - round radix2 (FLT_exp (-1074) 53) ZnearestE (x_0 * y))%R by ring. replace ((round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * (y - round radix2 (FLT_exp (-1074) 26) ZnearestE y)))%R with (((round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * y - x_0*y) +x_0*y) * (-1)*((round radix2 (FLT_exp (-1074) 26) ZnearestE 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. unfold WhyFloatsStrictLegacy.FtoRradix; fold FtoRradix. rewrite VeltkampEven_gappa with 27%nat y py qy hy. 2: split; auto with zarith arith. 2: assumption. 2: rewrite <- FTRr, H44; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H41; rewrite HW_33; rewrite <- (FTRr py), H44; reflexivity. 2: rewrite <- FTRr, H38; rewrite HW_36; rewrite <- (FTRr qy), H41. 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 <- FTRr, H56; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H53; rewrite HW_21; reflexivity. 2: rewrite <- FTRr, H50; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. 2: rewrite <- FTRr, H47; rewrite HW_27; reflexivity. clear -H1 H0 H3. replace (53-Z_of_nat 27)%Z with 26%Z by auto with zarith. unfold WhyFloatsStrictLegacy.FtoRradix in H1, H0, H3; fold FtoRradix in H1, H0, H3. 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 ((round radix2 (FLT_exp (-1074) 26) ZnearestE y * (x_0 - round radix2 (FLT_exp (-1074) 26) ZnearestE x_0)))%R with (((x_0*round radix2 (FLT_exp (-1074) 26) ZnearestE y - x_0*y) +x_0*y) * (-1)*((round radix2 (FLT_exp (-1074) 26) ZnearestE 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 H31; rewrite HW_50; rewrite HW_53. rewrite HW_48; rewrite H34; rewrite HW_45. destruct HW_41 as (Y1,_); unfold double_value in Y1; simpl in Y1. rewrite HW_43; rewrite Y1; rewrite H. unfold WhyFloatsStrictLegacy.FtoRradix; fold FtoRradix. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite <- FTRr, H58; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H55; rewrite HW_21; rewrite <- (FTRr px), H58; reflexivity. 2: rewrite <- FTRr, H52; rewrite HW_24; rewrite <- (FTRr qx), H55. 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 <- FTRr, H58; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H55; rewrite HW_21; reflexivity. 2: rewrite <- FTRr, H52; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. 2: rewrite <- FTRr, H49; rewrite HW_27; reflexivity. rewrite VeltkampEven_gappa with 27%nat y py qy hy. 2: split; auto with zarith arith. 2: assumption. 2: rewrite <- FTRr, H46; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H43; rewrite HW_33; rewrite <- (FTRr py), H46; reflexivity. 2: rewrite <- FTRr, H40; rewrite HW_36; rewrite <- (FTRr qy), H43. 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 <- FTRr, H46; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H43; rewrite HW_33; reflexivity. 2: rewrite <- FTRr, H40; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. 2: rewrite <- FTRr, H37; rewrite HW_39; reflexivity. clear -H1 H0 H3. replace (53-Z_of_nat 27)%Z with 26%Z by auto with zarith. unfold WhyFloatsStrictLegacy.FtoRradix in H1, H0, H3; fold FtoRradix in H1, H0, H3. assert (Rabs (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * round radix2 (FLT_exp (-1074) 26) ZnearestE 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 (- round radix2 (FLT_exp (-1074) 53) ZnearestE (x_0* y) + round radix2 (FLT_exp (-1074) 53) ZnearestE (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0* round radix2 (FLT_exp (-1074) 26) ZnearestE y))%R with (round radix2 (FLT_exp (-1074) 53) ZnearestE (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0* round radix2 (FLT_exp (-1074) 26) ZnearestE y) - round radix2 (FLT_exp (-1074) 53) ZnearestE (x_0* y))%R by ring. replace ((round radix2 (FLT_exp (-1074) 26) ZnearestE x_0* (y - round radix2 (FLT_exp (-1074) 26) ZnearestE y)))%R with (((round radix2 (FLT_exp (-1074) 26) ZnearestE x_0* y - x_0*y) +x_0*y) * (-1)*((round radix2 (FLT_exp (-1074) 26) ZnearestE y - y)/y))%R. replace ((round radix2 (FLT_exp (-1074) 26) ZnearestE y * (x_0- round radix2 (FLT_exp (-1074) 26) ZnearestE x_0)))%R with (((x_0*round radix2 (FLT_exp (-1074) 26) ZnearestE y - x_0*y) +x_0*y) * (-1)*((round radix2 (FLT_exp (-1074) 26) ZnearestE 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. unfold WhyFloatsStrictLegacy.FtoRradix; fold FtoRradix. rewrite VeltkampTail_gappa with 27%nat x_0 px qx hx tx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite <- FTRr, H63; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H60; rewrite HW_21; reflexivity. 2: rewrite <- FTRr, H57; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. 2: rewrite <- FTRr, H54; 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 <- FTRr, H51; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H48; rewrite HW_33; reflexivity. 2: rewrite <- FTRr, H45; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. 2: rewrite <- FTRr, H42; rewrite HW_39; reflexivity. clear -H1 H0 H3. replace (53-Z_of_nat 27)%Z with 26%Z by auto with zarith. unfold WhyFloatsStrictLegacy.FtoRradix in H1, H0, H3; fold FtoRradix in H1, H0, H3. clear -H1 H0 H3. 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 - round radix2 (FLT_exp (-1074) 26) ZnearestE x_0) * (y - round radix2 (FLT_exp (-1074) 26) ZnearestE y))%R with ((x_0*y)*((round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 - x_0)/x_0) *((round radix2 (FLT_exp (-1074) 26) ZnearestE 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 H35; rewrite HW_55; rewrite HW_58. rewrite HW_53; rewrite H38; rewrite HW_50. rewrite HW_48; rewrite H41; rewrite HW_45. destruct HW_41 as (Y1,_); unfold double_value in Y1; simpl in Y1. rewrite HW_43; rewrite Y1; rewrite H. unfold WhyFloatsStrictLegacy.FtoRradix; fold FtoRradix. rewrite VeltkampEven_gappa with 27%nat x_0 px qx hx. 2: split; auto with zarith arith. 2: assumption. 2: rewrite <- FTRr, H65; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H62; rewrite HW_21; rewrite <- (FTRr px), H65; reflexivity. 2: rewrite <- FTRr, H59; rewrite HW_24; rewrite <- (FTRr qx), H62. 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 <- FTRr, H65; rewrite HW_18, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H62; rewrite HW_21; reflexivity. 2: rewrite <- FTRr, H59; rewrite HW_24. 2: rewrite Rplus_comm; reflexivity. 2: rewrite <- FTRr, H56; rewrite HW_27; reflexivity. rewrite VeltkampEven_gappa with 27%nat y py qy hy. 2: split; auto with zarith arith. 2: assumption. 2: rewrite <- FTRr, H53; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H50; rewrite HW_33; rewrite <- (FTRr py), H53; reflexivity. 2: rewrite <- FTRr, H47; rewrite HW_36; rewrite <- (FTRr qy), H50. 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 <- FTRr, H53; rewrite HW_30, HW_16; apply f_equal; apply f_equal; simpl; ring. 2: rewrite <- FTRr, H50; rewrite HW_33; reflexivity. 2: rewrite <- FTRr, H47; rewrite HW_36. 2: rewrite Rplus_comm; reflexivity. 2: rewrite <- FTRr, H44; rewrite HW_39; reflexivity. clear -H1 H0 H3. replace (53-Z_of_nat 27)%Z with 26%Z by auto with zarith. unfold WhyFloatsStrictLegacy.FtoRradix in H1, H0, H3; fold FtoRradix in H1, H0, H3. assert (Rabs (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * round radix2 (FLT_exp (-1074) 26) ZnearestE 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 (- round radix2 (FLT_exp (-1074) 53) ZnearestE (x_0 * y) + round radix2 (FLT_exp (-1074) 53) ZnearestE (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * round radix2 (FLT_exp (-1074) 26) ZnearestE y))%R with (round radix2 (FLT_exp (-1074) 53) ZnearestE (round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * round radix2 (FLT_exp (-1074) 26) ZnearestE y) - round radix2 (FLT_exp (-1074) 53) ZnearestE (x_0 * y))%R by ring. replace ((round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * (y - round radix2 (FLT_exp (-1074) 26) ZnearestE y)))%R with (((round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 * y - x_0*y) +x_0*y) * (-1)*((round radix2 (FLT_exp (-1074) 26) ZnearestE y - y)/y))%R. replace ((round radix2 (FLT_exp (-1074) 26) ZnearestE y * (x_0 - round radix2 (FLT_exp (-1074) 26) ZnearestE x_0)))%R with (((x_0*round radix2 (FLT_exp (-1074) 26) ZnearestE y - x_0*y) +x_0*y) * (-1)*((round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 - x_0)/x_0))%R. replace ((x_0 - round radix2 (FLT_exp (-1074) 26) ZnearestE x_0) * (y - round radix2 (FLT_exp (-1074) 26) ZnearestE y))%R with ((x_0*y)*((round radix2 (FLT_exp (-1074) 26) ZnearestE x_0 - x_0)/x_0) *((round radix2 (FLT_exp (-1074) 26) ZnearestE 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.