Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* This file was originally generated by why. It can be modified; only the generated parts will be overwritten. *) Require Export jessie_why. Require Export discriminant3. Require Export Why2Gappa. Require Export WhyFloatsStrictLegacy. Coercion Local FtoRradix := WhyFloatsStrictLegacy.FtoRradix. (*Why logic*) Definition ulp : double -> R. intros f; destruct f. exact (Fulp bdouble radix 53%nat df). Defined. (*Why axiom*) Lemma ulp_normal1 : (forall (f_0_0:double), ((Rle (1 / 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304)%R (Rabs (double_value f_0_0))) -> (Rlt (Rabs (double_value f_0_0)) (Rmult (1 * 9007199254740992)%R (ulp f_0_0))))). intros f; destruct f; intros. unfold double_value in *; simpl in *. apply Rle_lt_trans with ((powerRZ radix 53%nat - 1) * Fulp bdouble radix 53 df)%R. apply FulpGe; try apply pdGivesBound; auto with zarith. apply Rmult_lt_compat_r. unfold Fulp; auto with real zarith. rewrite Rmult_1_l. apply Rlt_le_trans with (powerRZ radix 53%nat-0)%R. apply Rplus_lt_compat_l. auto with real zarith. right; simpl; ring. Qed. (*Why axiom*) Lemma ulp_normal2 : (forall (f_1:double), ((Rle (1 / 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304)%R (Rabs (double_value f_1))) -> (Rle (ulp f_1) (Rmult (1 / 4503599627370496)%R (Rabs (double_value f_1)))))). intros f; destruct f; intros. unfold double_value in *; simpl in *. apply Rle_trans with (Rabs df * powerRZ radix (Zsucc (- 53%nat)))%R. apply FulpLe2; try apply pdGivesBound; auto with zarith. rewrite FcanonicFnormalizeEq;try apply pdGivesBound; auto with zarith. case Hcandf; trivial; intros. absurd (Rabs df < FtoR radix (firstNormalPos radix bdouble 53%nat))%R. apply Rle_not_lt. apply Rle_trans with (2:=H). rewrite firstNormalPos_eq; auto with zarith. replace (Zpred 53%nat + - dExp bdouble)%Z with (-(1022))%Z. 2: unfold Zpred; reflexivity. rewrite powerRZ_Zopp; auto with real. unfold Rdiv; rewrite Rmult_1_l. right; apply f_equal; apply sym_eq. apply trans_eq with (Z2R 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304). reflexivity. replace 1022%Z with (Z_of_nat 1022) by reflexivity. unfold radix. rewrite <- Zpower_nat_Z_powerRZ. unfold Zpower_nat; simpl (iter_nat 1022%nat Z (fun x : Z => (2 * x)%Z) 1%Z). now rewrite <- Z2R_IZR. unfold FtoRradix, WhyFloatsStrictLegacy.FtoRradix; rewrite <- Fabs_correct; auto with zarith. apply FsubnormalLtFirstNormalPos;try apply pdGivesBound; auto with zarith. apply FsubnormFabs; auto with zarith. rewrite Fabs_correct; auto with real zarith. rewrite Rmult_comm. apply Rmult_le_compat_r; auto with real. replace (Zsucc (- 53%nat)) with (-(52))%Z. rewrite powerRZ_Zopp; auto with real. unfold Rdiv; rewrite Rmult_1_l; right; apply f_equal. simpl; ring. unfold Zsucc; ring. Qed. (*Why axiom*) Lemma ulp_subnormal : (forall (f_2:double), ((Rlt (Rabs (double_value f_2)) (1 / 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304)%R) -> (eq (ulp f_2) (1 / 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784)%R))). intros f; destruct f; intros. unfold double_value in H; unfold ulp; simpl in *. rewrite CanonicFulp; try apply pdGivesBound; auto with zarith. rewrite FsubnormalFexp with radix bdouble df. unfold FtoR. simpl (Float.Fnum {| Float.Fnum := 1%nat; Float.Fexp := - dExp bdouble |}). simpl (Float.Fexp {| Float.Fnum := 1%nat; Float.Fexp := - dExp bdouble |}). unfold Rdiv; repeat rewrite Rmult_1_l. replace (-1074)%Z with (-(1074))%Z by reflexivity. rewrite powerRZ_Zopp; auto with real. apply f_equal; apply sym_eq. apply trans_eq with (Z2R 202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784). reflexivity. replace 1074%Z with (Z_of_nat 1074) by reflexivity. unfold radix. rewrite <- Zpower_nat_Z_powerRZ. unfold Zpower_nat; simpl (iter_nat 1074%nat Z (fun x : Z => (2 * x)%Z) 1%Z). now rewrite <- Z2R_IZR. case Hcandf; trivial; intros. absurd (Rabs df < FtoR radix (firstNormalPos radix bdouble 53%nat))%R. apply Rle_not_lt. unfold FtoRradix, WhyFloatsStrictLegacy.FtoRradix; rewrite <- Fabs_correct; auto with zarith. apply FnormalLtFirstNormalPos;try apply pdGivesBound; auto with zarith. apply FnormalFabs; auto with zarith. rewrite Fabs_correct; auto with real zarith. apply Rlt_le_trans with (1:=H). rewrite firstNormalPos_eq; auto with zarith. replace (Zpred 53%nat + - dExp bdouble)%Z with (-(1022))%Z. 2: unfold Zpred; reflexivity. rewrite powerRZ_Zopp; auto with real. unfold Rdiv; rewrite Rmult_1_l. right; apply f_equal. apply trans_eq with (Z2R 44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304). reflexivity. replace 1022%Z with (Z_of_nat 1022) by reflexivity. unfold radix. rewrite <- Zpower_nat_Z_powerRZ. unfold Zpower_nat; simpl (iter_nat 1022%nat Z (fun x : Z => (2 * x)%Z) 1%Z). now rewrite <- Z2R_IZR. Qed. (*Why axiom*) Lemma ulp_pow : (forall (f_3:double), (exists i_1:Z, (eq (ulp f_3) (powerRZ (2)%R i_1)))). intros f; destruct f. unfold ulp, Fulp; simpl. eauto. Qed. (* Why obligation from file "discri.c", line 43, characters 12-69: *) (*Why goal*) Lemma discriminant_ensures_default_po_1 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result: double), forall (HW_9: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_10: p = result), forall (result0: double), forall (HW_11: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_12: q = result0), forall (result1: double), forall (HW_13: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_14: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_15: tmp = result2), forall (result3: double), forall (HW_16: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_17: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (result5: double), forall (HW_18: (mul_double_post nearest_even result4 tmp result5)), forall (HW_19: (Rle (double_value result3) (double_value result5))), forall (result6: double), forall (HW_20: (sub_double_post nearest_even p q result6)), forall (d: double), forall (HW_21: d = result6), forall (why__return: double), forall (HW_22: why__return = d), (* JC_45 *) ((eq (double_value why__return) (0)%R) \/ (Rle (Rabs (Rminus (double_value why__return) (Rminus (Rmult (double_value b) (double_value b)) ( Rmult (double_value a) (double_value c))))) (Rmult (2)%R (ulp why__return)))). Proof. intros. destruct HW_9; destruct HW_11; destruct HW_13; destruct HW_16; destruct HW_17; destruct HW_18; destruct HW_20. why2float. unfold ulp; simpl. apply discri16 with p q result6 (Fminus radix (Fmult b b) p) (Fminus radix (Fmult a c) q) d result5 result3; try apply pdGivesBound; auto with zarith. fold radix; fold FtoRradix; intros Y; clear -HW_19 Y; Contradict Y; now apply Rle_not_lt. fold radix; fold FtoRradix; intros Y; clear -HW_19 Y; Contradict Y; now apply Rle_not_lt. clear - HW_1; destruct HW_1 as (H,_). fold radix; fold FtoRradix. destruct H;[now left|right]. apply Rle_trans with (2:=H). replace (- dExp bdouble + 3 * 53%nat - 1)%Z with (-(916))%Z by reflexivity. rewrite powerRZ_Zopp; auto with real. unfold Rdiv; rewrite Rmult_1_l. right; apply f_equal; apply sym_eq. apply trans_eq with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). reflexivity. replace 916%Z with (Z_of_nat 916) by reflexivity. unfold radix; rewrite <- Zpower_nat_Z_powerRZ. unfold Zpower_nat; simpl (iter_nat 916%nat Z (fun x : Z => (2 * x)%Z) 1%Z). now rewrite <- Z2R_IZR. clear - HW_1; destruct HW_1 as (_,(H,_)). fold radix; fold FtoRradix. destruct H;[now left|right]. apply Rle_trans with (2:=H). replace (- dExp bdouble + 3 * 53%nat - 1)%Z with (-(916))%Z by reflexivity. rewrite powerRZ_Zopp; auto with real. unfold Rdiv; rewrite Rmult_1_l. right; apply f_equal; apply sym_eq. apply trans_eq with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). reflexivity. replace 916%Z with (Z_of_nat 916) by reflexivity. unfold radix; rewrite <- Zpower_nat_Z_powerRZ. unfold Zpower_nat; simpl (iter_nat 916%nat Z (fun x : Z => (2 * x)%Z) 1%Z). now rewrite <- Z2R_IZR. fold radix; fold FtoRradix. generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (b*b)%R (RND_EvenClosest bdouble radix 53 (b*b)); try apply pdGivesBound; auto with zarith. fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; rewrite H25; apply sym_eq; assumption. fold radix; fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (a * c)%R (RND_EvenClosest bdouble radix 53 (a * c)); try apply pdGivesBound; auto with zarith. fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; rewrite H22; apply sym_eq; assumption. fold radix; fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (p - q)%R (RND_EvenClosest bdouble radix 53 (p - q)); try apply pdGivesBound; auto with zarith. fold radix; fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (3 * Rabs result6)%R (RND_EvenClosest bdouble radix 53 (3 * Rabs result6)); try apply pdGivesBound; auto with zarith. fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; rewrite H9, H7, H19, HW_14. unfold FtoRradix; rewrite H11, H3. repeat apply f_equal; trivial. fold radix; fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (p+q)%R (RND_EvenClosest bdouble radix 53 (p+q)); try apply pdGivesBound; auto with zarith. intros _; fold radix; fold FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (p - q)%R (RND_EvenClosest bdouble radix 53 (p - q)); try apply pdGivesBound; auto with zarith. fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; rewrite H13; rewrite H16; rewrite H11; reflexivity. unfold radix; rewrite Fminus_correct; try rewrite Fmult_correct; auto with zarith. unfold radix; rewrite Fminus_correct; try rewrite Fmult_correct; auto with zarith. fold radix; fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; intros Y; clear -HW_19 Y; Contradict Y; now apply Rle_not_lt. fold radix; fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; intros Y; clear -HW_19 Y; Contradict Y; now apply Rle_not_lt. Save. (* Why obligation from file "discri.c", line 43, characters 12-69: *) (*Why goal*) Lemma discriminant_ensures_default_po_2 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result: double), forall (HW_9: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_10: p = result), forall (result0: double), forall (HW_11: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_12: q = result0), forall (result1: double), forall (HW_13: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_14: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_15: tmp = result2), forall (result3: double), forall (HW_16: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_17: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (result5: double), forall (HW_18: (mul_double_post nearest_even result4 tmp result5)), forall (HW_23: (Rgt (double_value result3) (double_value result5))), forall (result6: double), forall (HW_24: (* JC_25 *) (((eq (Rmult (double_value b) (double_value b)) (0)%R) \/ (Rle (1 / 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712)%R (Rabs (Rmult (double_value b) (double_value b)))) -> (eq (Rmult (double_value b) (double_value b)) (Rplus (double_value p) ( double_value result6)))))), forall (dp: double), forall (HW_25: dp = result6), forall (result7: double), forall (HW_26: (* JC_25 *) (((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712)%R (Rabs (Rmult (double_value a) (double_value c)))) -> (eq (Rmult (double_value a) (double_value c)) (Rplus (double_value q) ( double_value result7)))))), forall (dq: double), forall (HW_27: dq = result7), forall (result8: double), forall (HW_28: (sub_double_post nearest_even p q result8)), forall (result9: double), forall (HW_29: (sub_double_post nearest_even dp dq result9)), forall (result10: double), forall (HW_30: (add_double_post nearest_even result8 result9 result10)), forall (d: double), forall (HW_31: d = result10), forall (why__return: double), forall (HW_32: why__return = d), (* JC_45 *) ((eq (double_value why__return) (0)%R) \/ (Rle (Rabs (Rminus (double_value why__return) (Rminus (Rmult (double_value b) (double_value b)) ( Rmult (double_value a) (double_value c))))) (Rmult (2)%R (ulp why__return)))). Proof. intros. destruct HW_9; destruct HW_11; destruct HW_13; destruct HW_16; destruct HW_17; destruct HW_18; destruct HW_28; destruct HW_29; destruct HW_30. why2float. unfold ulp; simpl. apply discri16 with p q result8 dp dq result9 result5 result3; try apply pdGivesBound; auto with zarith. clear - HW_1; destruct HW_1 as (H,_). fold radix; fold FtoRradix. destruct H;[now left|right]. apply Rle_trans with (2:=H). replace (- dExp bdouble + 3 * 53%nat - 1)%Z with (-(916))%Z by reflexivity. rewrite powerRZ_Zopp; auto with real. unfold Rdiv; rewrite Rmult_1_l. right; apply f_equal; apply sym_eq. apply trans_eq with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). reflexivity. replace 916%Z with (Z_of_nat 916) by reflexivity. unfold radix; rewrite <- Zpower_nat_Z_powerRZ. unfold Zpower_nat; simpl (iter_nat 916%nat Z (fun x : Z => (2 * x)%Z) 1%Z). now rewrite <- Z2R_IZR. clear - HW_1; destruct HW_1 as (_,(H,_)). fold radix; fold FtoRradix. destruct H;[now left|right]. apply Rle_trans with (2:=H). replace (- dExp bdouble + 3 * 53%nat - 1)%Z with (-(916))%Z by reflexivity. rewrite powerRZ_Zopp; auto with real. unfold Rdiv; rewrite Rmult_1_l. right; apply f_equal; apply sym_eq. apply trans_eq with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). reflexivity. replace 916%Z with (Z_of_nat 916) by reflexivity. unfold radix; rewrite <- Zpower_nat_Z_powerRZ. unfold Zpower_nat; simpl (iter_nat 916%nat Z (fun x : Z => (2 * x)%Z) 1%Z). now rewrite <- Z2R_IZR. fold radix; fold FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (b*b)%R (RND_EvenClosest bdouble radix 53 (b*b)); try apply pdGivesBound; auto with zarith. fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; rewrite H35; apply sym_eq; assumption. fold radix; fold FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (a * c)%R (RND_EvenClosest bdouble radix 53 (a * c)); try apply pdGivesBound; auto with zarith. fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; rewrite H32; apply sym_eq; assumption. fold radix; fold FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (p - q)%R (RND_EvenClosest bdouble radix 53 (p - q)); try apply pdGivesBound; auto with zarith. fold radix; fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (3 * Rabs result8)%R (RND_EvenClosest bdouble radix 53 (3 * Rabs result8)); try apply pdGivesBound; auto with zarith. fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; rewrite H9; rewrite H7; rewrite H29, HW_14; rewrite H3. unfold FtoRradix; rewrite H11. repeat apply f_equal2; trivial. fold radix; fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (p+q)%R (RND_EvenClosest bdouble radix 53 (p+q)); try apply pdGivesBound; auto with zarith. fold radix; fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; intros Y; clear -HW_23 Y; Contradict Y; now apply Rgt_not_le. fold radix; fold WhyFloatsStrictLegacy.FtoRradix. rewrite HW_24. rewrite H26; ring. clear - HW_1; destruct HW_1 as (H,_). destruct H;[left|right]. rewrite H; ring. apply Rle_trans with (2:=H). unfold Rdiv; repeat rewrite Rmult_1_l. apply Rle_Rinv. apply Rlt_le_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). replace 0%R with (Z2R 0) by reflexivity. apply Z2R_lt; auto with zarith. right; reflexivity. apply Rle_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). right; reflexivity. apply Rle_trans with (Z2R 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712). apply Z2R_le; auto with zarith. right; reflexivity. fold radix; fold WhyFloatsStrictLegacy.FtoRradix. rewrite HW_26. rewrite H23; ring. clear - HW_1; destruct HW_1 as (_,(H,_)). destruct H;[now left|right]. apply Rle_trans with (2:=H). unfold Rdiv; repeat rewrite Rmult_1_l. apply Rle_Rinv. apply Rlt_le_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). replace 0%R with (Z2R 0) by reflexivity. apply Z2R_lt; auto with zarith. right; reflexivity. apply Rle_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). right; reflexivity. apply Rle_trans with (Z2R 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712). apply Z2R_le; auto with zarith. right; reflexivity. intros _; fold radix; fold FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (dp - dq)%R (RND_EvenClosest bdouble radix 53 (dp - dq)); try apply pdGivesBound; auto with zarith. intros _; fold radix; fold FtoRradix; generalize EvenClosestCompatible; unfold CompatibleP; intros T. apply T with (result8 + result9)%R (RND_EvenClosest bdouble radix 53 (result8 + result9)); try apply pdGivesBound; auto with zarith. fold FtoRradix WhyFloatsStrictLegacy.FtoRradix; rewrite H17; rewrite H20; rewrite H15; reflexivity. Save. (* Why obligation from file "discri.c", line 49, characters 4-7: *) (*Why goal*) Lemma discriminant_safety_po_1 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), (no_overflow_double nearest_even (Rmult (double_value b) (double_value b))). Proof. intros a b c (_,(_,(H1,_))). why2gappa; gappa. Save. (* Why obligation from file "discri.c", line 50, characters 4-7: *) (*Why goal*) Lemma discriminant_safety_po_2 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), (no_overflow_double nearest_even (Rmult (double_value a) (double_value c))). Proof. intros a b c (_,(_,(_,(_,(_,H2))))) _ _ _ _ _ . why2gappa; gappa. Save. (* Why obligation from file "discri.c", line 52, characters 20-23: *) (*Why goal*) Lemma discriminant_safety_po_3 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), (no_overflow_double nearest_even (Rminus (double_value p) (double_value q))). Proof. intros a b c (_,(_,(H1,(_,(_,H2))))). intros _ r Hr p Hp _ rr Hrr q Hq. why2gappa; gappa. Save. (* Why obligation from file "discri.c", line 52, characters 6-9: *) (*Why goal*) Lemma discriminant_safety_po_4 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), (no_overflow_double nearest_even (Rplus (double_value p) (double_value q))). Proof. intros a b c (_,(_,(H1,(_,(_,H2))))). intros _ r Hr p Hp _ rr Hrr q Hq. intros _ t Ht l Hl m Hm. why2gappa; gappa. Save. (* Why obligation from file "discri.c", line 52, characters 13-24: *) (*Why goal*) Lemma discriminant_safety_po_5 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), forall (HW_19: (no_overflow_double nearest_even (Rplus (double_value p) (double_value q)))), forall (result3: double), forall (HW_20: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_21: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), (no_overflow_double nearest_even (Rmult (double_value result4) (double_value tmp))). Proof. intros a b c (_,(_,(H1,(_,(_,H2))))). intros _ r Hr p Hp _ rr Hrr q Hq. intros _ t Ht l Hl m Hm _ n Hn k (Hk,_). why2gappa; gappa. Save. (* Why obligation from file "discri.c", line 55, characters 7-20: *) (*Why goal*) Lemma discriminant_safety_po_6 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), forall (HW_19: (no_overflow_double nearest_even (Rplus (double_value p) (double_value q)))), forall (result3: double), forall (HW_20: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_21: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (HW_22: (no_overflow_double nearest_even (Rmult (double_value result4) (double_value tmp)))), forall (result5: double), forall (HW_23: (mul_double_post nearest_even result4 tmp result5)), forall (HW_29: (Rgt (double_value result3) (double_value result5))), (* JC_15 *) (* JC_11 *) (eq (double_value p) (round_double nearest_even (Rmult (double_value b) (double_value b)))). Proof. intros. rewrite HW_11; destruct HW_10; assumption. Save. Require Import Fourier. (* Why obligation from file "discri.c", line 55, characters 7-20: *) (*Why goal*) Lemma discriminant_safety_po_7 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), forall (HW_19: (no_overflow_double nearest_even (Rplus (double_value p) (double_value q)))), forall (result3: double), forall (HW_20: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_21: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (HW_22: (no_overflow_double nearest_even (Rmult (double_value result4) (double_value tmp)))), forall (result5: double), forall (HW_23: (mul_double_post nearest_even result4 tmp result5)), forall (HW_29: (Rgt (double_value result3) (double_value result5))), (* JC_15 *) (* JC_12 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R). Proof. intros a b c (_,(_,(H1,_))); intros; clear -H1. apply Rle_trans with (1:=H1). rewrite 2!Rmult_1_l. apply Rle_trans with (Z2R 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024). right; reflexivity. apply Rle_trans with (Z2R 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168). apply Z2R_le. auto with zarith. right; reflexivity. Save. (* Why obligation from file "discri.c", line 55, characters 7-20: *) (*Why goal*) Lemma discriminant_safety_po_8 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), forall (HW_19: (no_overflow_double nearest_even (Rplus (double_value p) (double_value q)))), forall (result3: double), forall (HW_20: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_21: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (HW_22: (no_overflow_double nearest_even (Rmult (double_value result4) (double_value tmp)))), forall (result5: double), forall (HW_23: (mul_double_post nearest_even result4 tmp result5)), forall (HW_29: (Rgt (double_value result3) (double_value result5))), (* JC_15 *) (* JC_13 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R). Proof. apply discriminant_safety_po_7. Save. (* Why obligation from file "discri.c", line 55, characters 7-20: *) (*Why goal*) Lemma discriminant_safety_po_9 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), forall (HW_19: (no_overflow_double nearest_even (Rplus (double_value p) (double_value q)))), forall (result3: double), forall (HW_20: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_21: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (HW_22: (no_overflow_double nearest_even (Rmult (double_value result4) (double_value tmp)))), forall (result5: double), forall (HW_23: (mul_double_post nearest_even result4 tmp result5)), forall (HW_29: (Rgt (double_value result3) (double_value result5))), (* JC_15 *) (* JC_14 *) (Rle (Rabs (Rmult (double_value b) (double_value b))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R). Proof. intros a b c (_,(_,(H1,_))); intros; clear -H1. why2gappa; gappa. Save. (* Why obligation from file "discri.c", line 56, characters 7-20: *) (*Why goal*) Lemma discriminant_safety_po_10 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), forall (HW_19: (no_overflow_double nearest_even (Rplus (double_value p) (double_value q)))), forall (result3: double), forall (HW_20: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_21: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (HW_22: (no_overflow_double nearest_even (Rmult (double_value result4) (double_value tmp)))), forall (result5: double), forall (HW_23: (mul_double_post nearest_even result4 tmp result5)), forall (HW_29: (Rgt (double_value result3) (double_value result5))), forall (HW_30: (* JC_15 *) ((* JC_11 *) (eq (double_value p) (round_double nearest_even (Rmult (double_value b) ( double_value b)))) /\ (* JC_12 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_13 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_14 *) (Rle (Rabs (Rmult (double_value b) (double_value b))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result6: double), forall (HW_31: (* JC_25 *) (((eq (Rmult (double_value b) (double_value b)) (0)%R) \/ (Rle (1 / 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712)%R (Rabs (Rmult (double_value b) (double_value b)))) -> (eq (Rmult (double_value b) (double_value b)) (Rplus (double_value p) ( double_value result6)))))), forall (dp: double), forall (HW_32: dp = result6), (* JC_15 *) (* JC_11 *) (eq (double_value q) (round_double nearest_even (Rmult (double_value a) (double_value c)))). Proof. intros. rewrite HW_14; destruct HW_13; assumption. Save. (* Why obligation from file "discri.c", line 56, characters 7-20: *) (*Why goal*) Lemma discriminant_safety_po_11 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), forall (HW_19: (no_overflow_double nearest_even (Rplus (double_value p) (double_value q)))), forall (result3: double), forall (HW_20: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_21: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (HW_22: (no_overflow_double nearest_even (Rmult (double_value result4) (double_value tmp)))), forall (result5: double), forall (HW_23: (mul_double_post nearest_even result4 tmp result5)), forall (HW_29: (Rgt (double_value result3) (double_value result5))), forall (HW_30: (* JC_15 *) ((* JC_11 *) (eq (double_value p) (round_double nearest_even (Rmult (double_value b) ( double_value b)))) /\ (* JC_12 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_13 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_14 *) (Rle (Rabs (Rmult (double_value b) (double_value b))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result6: double), forall (HW_31: (* JC_25 *) (((eq (Rmult (double_value b) (double_value b)) (0)%R) \/ (Rle (1 / 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712)%R (Rabs (Rmult (double_value b) (double_value b)))) -> (eq (Rmult (double_value b) (double_value b)) (Rplus (double_value p) ( double_value result6)))))), forall (dp: double), forall (HW_32: dp = result6), (* JC_15 *) (* JC_12 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R). Proof. intros a b c (_,(_,(_,(H1,_)))); intros; clear -H1. exact H1. Save. (* Why obligation from file "discri.c", line 56, characters 7-20: *) (*Why goal*) Lemma discriminant_safety_po_12 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), forall (HW_19: (no_overflow_double nearest_even (Rplus (double_value p) (double_value q)))), forall (result3: double), forall (HW_20: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_21: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (HW_22: (no_overflow_double nearest_even (Rmult (double_value result4) (double_value tmp)))), forall (result5: double), forall (HW_23: (mul_double_post nearest_even result4 tmp result5)), forall (HW_29: (Rgt (double_value result3) (double_value result5))), forall (HW_30: (* JC_15 *) ((* JC_11 *) (eq (double_value p) (round_double nearest_even (Rmult (double_value b) ( double_value b)))) /\ (* JC_12 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_13 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_14 *) (Rle (Rabs (Rmult (double_value b) (double_value b))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result6: double), forall (HW_31: (* JC_25 *) (((eq (Rmult (double_value b) (double_value b)) (0)%R) \/ (Rle (1 / 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712)%R (Rabs (Rmult (double_value b) (double_value b)))) -> (eq (Rmult (double_value b) (double_value b)) (Rplus (double_value p) ( double_value result6)))))), forall (dp: double), forall (HW_32: dp = result6), (* JC_15 *) (* JC_13 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R). Proof. intros a b c (_,(_,(_,(_,(H1,_))))); intros; clear -H1. exact H1. Save. (* Why obligation from file "discri.c", line 56, characters 7-20: *) (*Why goal*) Lemma discriminant_safety_po_13 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), forall (HW_19: (no_overflow_double nearest_even (Rplus (double_value p) (double_value q)))), forall (result3: double), forall (HW_20: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_21: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (HW_22: (no_overflow_double nearest_even (Rmult (double_value result4) (double_value tmp)))), forall (result5: double), forall (HW_23: (mul_double_post nearest_even result4 tmp result5)), forall (HW_29: (Rgt (double_value result3) (double_value result5))), forall (HW_30: (* JC_15 *) ((* JC_11 *) (eq (double_value p) (round_double nearest_even (Rmult (double_value b) ( double_value b)))) /\ (* JC_12 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_13 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_14 *) (Rle (Rabs (Rmult (double_value b) (double_value b))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result6: double), forall (HW_31: (* JC_25 *) (((eq (Rmult (double_value b) (double_value b)) (0)%R) \/ (Rle (1 / 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712)%R (Rabs (Rmult (double_value b) (double_value b)))) -> (eq (Rmult (double_value b) (double_value b)) (Rplus (double_value p) ( double_value result6)))))), forall (dp: double), forall (HW_32: dp = result6), (* JC_15 *) (* JC_14 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R). Proof. intros a b c (_,(_,(_,(_,(_,H1))))); intros; clear -H1. exact H1. Save. (* Why obligation from file "discri.c", line 57, characters 13-18: *) (*Why goal*) Lemma discriminant_safety_po_14 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), forall (HW_19: (no_overflow_double nearest_even (Rplus (double_value p) (double_value q)))), forall (result3: double), forall (HW_20: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_21: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (HW_22: (no_overflow_double nearest_even (Rmult (double_value result4) (double_value tmp)))), forall (result5: double), forall (HW_23: (mul_double_post nearest_even result4 tmp result5)), forall (HW_29: (Rgt (double_value result3) (double_value result5))), forall (HW_30: (* JC_15 *) ((* JC_11 *) (eq (double_value p) (round_double nearest_even (Rmult (double_value b) ( double_value b)))) /\ (* JC_12 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_13 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_14 *) (Rle (Rabs (Rmult (double_value b) (double_value b))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result6: double), forall (HW_31: (* JC_25 *) (((eq (Rmult (double_value b) (double_value b)) (0)%R) \/ (Rle (1 / 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712)%R (Rabs (Rmult (double_value b) (double_value b)))) -> (eq (Rmult (double_value b) (double_value b)) (Rplus (double_value p) ( double_value result6)))))), forall (dp: double), forall (HW_32: dp = result6), forall (HW_33: (* JC_15 *) ((* JC_11 *) (eq (double_value q) (round_double nearest_even (Rmult (double_value a) ( double_value c)))) /\ (* JC_12 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_13 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_14 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result7: double), forall (HW_34: (* JC_25 *) (((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712)%R (Rabs (Rmult (double_value a) (double_value c)))) -> (eq (Rmult (double_value a) (double_value c)) (Rplus (double_value q) ( double_value result7)))))), forall (dq: double), forall (HW_35: dq = result7), forall (HW_36: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result8: double), forall (HW_37: (sub_double_post nearest_even p q result8)), (no_overflow_double nearest_even (Rminus (double_value dp) (double_value dq))). Proof. intros. why2gappa. replace (WhyFloatsStrictLegacy.FtoRradix dp) with (WhyFloatsStrictLegacy.FtoRradix b * WhyFloatsStrictLegacy.FtoRradix b - WhyFloatsStrictLegacy.FtoRradix p)%R. replace (WhyFloatsStrictLegacy.FtoRradix dq) with (WhyFloatsStrictLegacy.FtoRradix a * WhyFloatsStrictLegacy.FtoRradix c - WhyFloatsStrictLegacy.FtoRradix q)%R. destruct HW_33; rewrite H26. destruct HW_30; rewrite H28. clear - HW_1. destruct HW_1 as (_,(_,(H1,(_,(_,H2))))). gappa. rewrite HW_34. rewrite H11; ring. clear - HW_1. destruct HW_1 as (_,(H,_)). destruct H;[now left|right]. apply Rle_trans with (2:=H). unfold Rdiv; repeat rewrite Rmult_1_l. apply Rle_Rinv. apply Rlt_le_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). replace 0%R with (Z2R 0) by reflexivity. apply Z2R_lt; auto with zarith. right; reflexivity. apply Rle_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). right; reflexivity. apply Rle_trans with (Z2R 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712). apply Z2R_le; auto with zarith. right; reflexivity. rewrite HW_31. rewrite H14; ring. clear - HW_1. destruct HW_1 as (H,_). destruct H;[left|right]. rewrite H; ring. apply Rle_trans with (2:=H). unfold Rdiv; repeat rewrite Rmult_1_l. apply Rle_Rinv. apply Rlt_le_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). replace 0%R with (Z2R 0) by reflexivity. apply Z2R_lt; auto with zarith. right; reflexivity. apply Rle_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). right; reflexivity. apply Rle_trans with (Z2R 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712). apply Z2R_le; auto with zarith. right; reflexivity. Save. (* Why obligation from file "discri.c", line 57, characters 6-19: *) (*Why goal*) Lemma discriminant_safety_po_15 : forall (a: double), forall (b: double), forall (c: double), forall (HW_1: (* JC_43 *) ((* JC_37 *) ((eq (double_value b) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value b) (double_value b))))) /\ (* JC_38 *) ((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536)%R (Rabs (Rmult (double_value a) (double_value c))))) /\ (* JC_39 *) (Rle (Rabs (double_value b)) (1 * 3351951982485649274893506249551461531869841455148098344430890360930441007518386744200468574541725856922507964546621512713438470702986642486608412251521024)%R) /\ (* JC_40 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_41 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_42 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (HW_9: (no_overflow_double nearest_even (Rmult (double_value b) (double_value b)))), forall (result: double), forall (HW_10: (mul_double_post nearest_even b b result)), forall (p: double), forall (HW_11: p = result), forall (HW_12: (no_overflow_double nearest_even (Rmult (double_value a) (double_value c)))), forall (result0: double), forall (HW_13: (mul_double_post nearest_even a c result0)), forall (q: double), forall (HW_14: q = result0), forall (HW_15: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result1: double), forall (HW_16: (sub_double_post nearest_even p q result1)), forall (result2: double), forall (HW_17: (* JC_7 *) (eq (double_value result2) (Rabs (double_value result1)))), forall (tmp: double), forall (HW_18: tmp = result2), forall (HW_19: (no_overflow_double nearest_even (Rplus (double_value p) (double_value q)))), forall (result3: double), forall (HW_20: (add_double_post nearest_even p q result3)), forall (result4: double), forall (HW_21: (eq (double_value result4) (3)%R) /\ (eq (double_exact result4) (3)%R) /\ (eq (double_model result4) (3)%R)), forall (HW_22: (no_overflow_double nearest_even (Rmult (double_value result4) (double_value tmp)))), forall (result5: double), forall (HW_23: (mul_double_post nearest_even result4 tmp result5)), forall (HW_29: (Rgt (double_value result3) (double_value result5))), forall (HW_30: (* JC_15 *) ((* JC_11 *) (eq (double_value p) (round_double nearest_even (Rmult (double_value b) ( double_value b)))) /\ (* JC_12 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_13 *) (Rle (Rabs (double_value b)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_14 *) (Rle (Rabs (Rmult (double_value b) (double_value b))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result6: double), forall (HW_31: (* JC_25 *) (((eq (Rmult (double_value b) (double_value b)) (0)%R) \/ (Rle (1 / 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712)%R (Rabs (Rmult (double_value b) (double_value b)))) -> (eq (Rmult (double_value b) (double_value b)) (Rplus (double_value p) ( double_value result6)))))), forall (dp: double), forall (HW_32: dp = result6), forall (HW_33: (* JC_15 *) ((* JC_11 *) (eq (double_value q) (round_double nearest_even (Rmult (double_value a) ( double_value c)))) /\ (* JC_12 *) (Rle (Rabs (double_value a)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_13 *) (Rle (Rabs (double_value c)) (1 * 334846439745708537796382827831250565800439003657979252326171996365734703476542538279124493379904955664873335286735358382870982901778848138624518049209330462622955242963257218294408581408199098183686068192282702343236935664606211486223923248314908216080349889927704442739388432239144512088662677127168)%R) /\ (* JC_14 *) (Rle (Rabs (Rmult (double_value a) (double_value c))) (1 * 22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152)%R))), forall (result7: double), forall (HW_34: (* JC_25 *) (((eq (Rmult (double_value a) (double_value c)) (0)%R) \/ (Rle (1 / 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712)%R (Rabs (Rmult (double_value a) (double_value c)))) -> (eq (Rmult (double_value a) (double_value c)) (Rplus (double_value q) ( double_value result7)))))), forall (dq: double), forall (HW_35: dq = result7), forall (HW_36: (no_overflow_double nearest_even (Rminus (double_value p) (double_value q)))), forall (result8: double), forall (HW_37: (sub_double_post nearest_even p q result8)), forall (HW_38: (no_overflow_double nearest_even (Rminus (double_value dp) (double_value dq)))), forall (result9: double), forall (HW_39: (sub_double_post nearest_even dp dq result9)), (no_overflow_double nearest_even (Rplus (double_value result8) (double_value result9))). Proof. intros. why2gappa. rewrite HW_39; rewrite HW_37. replace (WhyFloatsStrictLegacy.FtoRradix dp) with (WhyFloatsStrictLegacy.FtoRradix b * WhyFloatsStrictLegacy.FtoRradix b - WhyFloatsStrictLegacy.FtoRradix p)%R. replace (WhyFloatsStrictLegacy.FtoRradix dq) with (WhyFloatsStrictLegacy.FtoRradix a * WhyFloatsStrictLegacy.FtoRradix c - WhyFloatsStrictLegacy.FtoRradix q)%R. destruct HW_30; rewrite H28. destruct HW_33; rewrite H30. clear - HW_1. destruct HW_1 as (_,(_,(H1,(_,(_,H2))))). gappa. rewrite HW_34. rewrite H13; ring. clear - HW_1. destruct HW_1 as (_,(H,_)). destruct H;[now left|right]. apply Rle_trans with (2:=H). unfold Rdiv; repeat rewrite Rmult_1_l. apply Rle_Rinv. apply Rlt_le_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). replace 0%R with (Z2R 0) by reflexivity. apply Z2R_lt; auto with zarith. right; reflexivity. apply Rle_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). right; reflexivity. apply Rle_trans with (Z2R 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712). apply Z2R_le; auto with zarith. right; reflexivity. rewrite HW_31. rewrite H16; ring. clear - HW_1. destruct HW_1 as (H,_). destruct H;[left|right]. rewrite H; ring. apply Rle_trans with (2:=H). unfold Rdiv; repeat rewrite Rmult_1_l. apply Rle_Rinv. apply Rlt_le_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). replace 0%R with (Z2R 0) by reflexivity. apply Z2R_lt; auto with zarith. right; reflexivity. apply Rle_trans with (Z2R 553956966280111321359151042308621317197106853745652161186848528428353614047320326248246548509656023453846098404449586961587736474553087989908021159880755329796288475560940755137311819879076531853615938045960455092067922915100261601864210866521544040371494407003426519343169536). right; reflexivity. apply Rle_trans with (Z2R 4989600773836799529140931782592096415168628151088643853756368106093029729672410164462394913731589252723356117110481238109931094970983984151847929495712078550800014182377714191293844303610907467956633391861359809983327026137802175972222138171120110393767802267189390104105896238075860024819712). apply Z2R_le; auto with zarith. right; reflexivity. Save.