Commit d27a393b9c8fe0af19601c2aadcd54b464d391c9 - coq-float

Imported Upstream version 8.2-1.2 Stephane Glondu 15 years ago

17 changed file(s) with 1600 addition(s) and 1373 deletion(s). Raw diff Collapse all Expand all

-1

AllFloat.v less more

0		Require Export ClosestMult.
	0	Require Export RND.
1	1	Require Export Closest2Plus.
2	2

-4

ClosestProp.v less more

45	45	replace (Fabs p) with p; auto.
46	46	unfold Fabs in \|- ; apply floatEq; simpl in \|- ; auto.
47	47	cut (0 <= Fnum p)%Z.
48		case (Fnum p); simpl in \|- *; auto; intros p' H0; Contradict H0;
49		apply Zlt_not_le; red in \|- ; simpl in \|- ; auto with zarith.
	48	case (Fnum p); simpl in \|- *; auto; intros p' H0.
	49	absurd ((0 <= Zneg p')%Z); trivial.
	50	apply Zlt_not_le; red in \|- ; simpl in \|- ; auto with zarith.
50	51	apply LeR0Fnum with (radix := radix); auto.
51	52	apply
52	53	RleRoundedR0

58	59	apply ClosestOpp; auto.
59	60	unfold Fabs in \|- ; apply floatEq; simpl in \|- ; auto.
60	61	cut (Fnum p <= 0)%Z.
61		case (Fnum p); simpl in \|- *; auto; intros p' H0; Contradict H0;
62		apply Zlt_not_le; red in \|- ; simpl in \|- ; auto with zarith.
	62	case (Fnum p); simpl in \|- *; auto; intros p' H0.
	63	absurd (Zpos p' <= 0)%Z; trivial.
	64	apply Zlt_not_le; red in \|- ; simpl in \|- ; auto with zarith.
63	65	apply R0LeFnum with (radix := radix); auto.
64	66	apply
65	67	RleRoundedLessR0

-3

Digit.v less more

61	61	Theorem Zpower_nat_anti_monotone_le :
62	62	forall p q : nat, (Zpower_nat n p <= Zpower_nat n q)%Z -> p <= q.
63	63	intros p q H'; case (le_or_lt p q); intros H'0; auto with arith.
64		Contradict H'; auto with zarith.
	64	absurd ((Zpower_nat n p <= Zpower_nat n q)%Z); auto with zarith.
65	65	Qed.
66	66
67	67	Theorem Zpower_nat_anti_eq :

274	274
275	275	Theorem digit_monotone :
276	276	forall p q : Z, (Zabs p <= Zabs q)%Z -> digit p <= digit q.
277		intros p q H; case (le_or_lt (digit p) (digit q)); auto; intros H1;
278		Contradict H.
	277	intros p q H; case (le_or_lt (digit p) (digit q)); auto; intros H1.
	278	absurd ((Zabs p <= Zabs q)%Z); trivial.
279	279	apply Zlt_not_le.
280	280	cut (p <> 0%Z); [ intros H2 \| idtac ].
281	281	apply Zlt_le_trans with (2 := digitLess p H2).

-3

Faux.v less more

293	293	Theorem ZleLe : forall x y : nat, (Z_of_nat x <= Z_of_nat y)%Z -> x <= y.
294	294	intros x y H'.
295	295	case (le_or_lt x y); auto with arith.
296		intros H'0; Contradict H'; auto with zarith.
	296	intros H'0; Contradict H'0; auto with zarith.
297	297	Qed.
298	298
299	299	Theorem inject_nat_eq : forall x y : nat, Z_of_nat x = Z_of_nat y -> x = y.

693	693	(- Z_of_nat n <= z)%Z -> (z <= Z_of_nat n)%Z -> Zabs_nat z <= n.
694	694	intros z n H' H'0; case (le_or_lt (Zabs_nat z) n); auto; intros lt.
695	695	case (Zle_or_lt 0 z); intros Zle0.
696		Contradict H'0.
	696	absurd ((z <= Z_of_nat n)%Z); auto.
697	697	apply Zlt_not_le; auto.
698	698	rewrite <- (inj_abs z); auto with zarith.
699		Contradict H'.
	699	absurd ((- Z_of_nat n <= z)%Z); trivial.
700	700	apply Zlt_not_le; auto.
701	701	replace z with (- Z_of_nat (Zabs_nat z))%Z.
702	702	apply Zlt_Zopp; auto with zarith.

-1

Fbound.v less more

37	37	forall (b : Fbound) (p : float), {Fbounded b p} + {~ Fbounded b p}.
38	38	intros b p; case (Z_le_gt_dec (Zpos (vNum b)) (Zabs (Fnum p)));
39	39	intros H'.
40		right; red in \|- *; intros H'3; Contradict H'; auto with float zarith.
	40	right; red in \|- *; intros H'3.
	41	absurd ((Zpos (vNum b) <= Zabs (Fnum p))%Z); auto with zarith float.
41	42	case (Z_le_gt_dec (- dExp b) (Fexp p)); intros H'1.
42	43	left; repeat split; auto with zarith.
43	44	right; red in \|- *; intros H'3; Contradict H'1; auto with float zarith.

+327

-131

FnElem/FArgReduct2.v less more

189	189	rewrite inj_pred; auto with arith zarith.
190	190	rewrite <- minus_Zminus_precq.
191	191	unfold Zpred, Zsucc in \|- *.
192		ring_simplify (prec - q + -1 + (q + 1 + - (Fexp alpha + (prec + prec))))%Z.
193		replace (-1 * prec + -1 * Fexp alpha)%Z with (- (prec + Fexp alpha))%Z;
194		[ idtac \| unfold Zpred in \|- *; ring ].
	192	replace (prec - q + -1 + (q + 1 + - (Fexp alpha + (prec + prec))))%Z
	193	with (- (prec + Fexp alpha))%Z; [ idtac \| unfold Zpred in \|- *; ring ].
195	194	rewrite <- Rinv_powerRZ; auto with real zarith.
196	195	apply Rle_Rinv; auto with real zarith.
197	196	rewrite powerRZ_add; auto with real zarith.

320	319	unfold FtoRradix, FtoR in \|- *.
321	320	rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith;
322	321	unfold Zsucc in \|- *.
323		ring_simplify (Fexp alpha + (q + 1 + - (Fexp alpha + (prec + prec))))%Z.
	322	replace (Fexp alpha + (q + 1 + - (Fexp alpha + (prec + prec))))%Z
	323	with (q-2*prec+1)%Z by ring.
324	324	apply Rmult_le_reg_l with (powerRZ radix (- (1 + (-2 * prec + q))));
325	325	auto with real zarith.
326	326	rewrite <- powerRZ_add; auto with real zarith.
327	327	rewrite Rmult_comm; rewrite Rmult_assoc; rewrite <- powerRZ_add;
328	328	auto with real zarith; unfold Zsucc in \|- *.
329		ring_simplify (q + -2 * prec + 1 + - (1 + (-2 * prec + q)))%Z.
330		ring_simplify (- (1 + (-2 * prec + q)) + (1 + (q - prec)))%Z.
	329	replace (q - 2 * prec + 1 + - (1 + (-2 * prec + q)))%Z with 0%Z by ring.
	330	replace (- (1 + (-2 * prec + q)) + (1 + (q - prec)))%Z with
	331	(Z_of_nat prec) by ring.
331	332	apply Rle_trans with (Fnum alpha); [ right; simpl in \|- *; ring \| idtac ].
332	333	apply Rle_trans with (Zabs (Fnum alpha)); auto with real zarith.
333	334	apply Rle_trans with (Zpos (vNum b)); auto with zarith real.

543	544	ring_simplify.
544	545	repeat rewrite <- powerRZ_add; auto with real zarith.
545	546	unfold Zsucc in \|- *.
546		ring_simplify (k + N + 1 + (q - (k + N + 1 + 1)))%Z.
	547	replace (k + N + 1 + (q - (k + N + 1 + 1)))%Z with (q-1)%Z by ring.
547	548	ring_simplify (k + N + 1 + - (k + N + 1 - q))%Z.
548	549	ring_simplify (k + N + 1 + - (k + N + 1))%Z.
549	550	ring_simplify (k + N + 1 + (- (k + N + 1 - q) + - (k + N + 1)))%Z.
550		pattern (Z_of_nat q) at 2 in \|- *; replace (Z_of_nat q) with (1 + (q+-1))%Z;
	551	pattern (Z_of_nat q) at 2 in \|- *; replace (Z_of_nat q) with (1 + (q-1))%Z;
551	552	[ idtac \| ring ].
552	553	rewrite powerRZ_add with (n := 1%Z); auto with real zarith.
553		apply Rplus_le_reg_l with (- powerRZ radix (q+-1))%R.
554		ring_simplify (- powerRZ radix (q+-1) + powerRZ radix (q+ -1))%R.
	554	apply Rplus_le_reg_l with (- powerRZ radix (q-1))%R.
	555	ring_simplify (- powerRZ radix (q-1) + powerRZ radix (q -1))%R.
555	556	simpl (powerRZ radix 1) in \|- *.
556	557	simpl (powerRZ radix 0) in \|- *.
557		ring_simplify (- powerRZ radix (q + -1) +
558		(2 * 1 * powerRZ radix (q + -1) - 1 -
559		powerRZ radix (-1 * k + -1 * N + q + -1)))%R.
560		apply
561		Rle_trans with (powerRZ radix (q+ -1) - powerRZ radix (q+ -2) -1)%R;
562		[ idtac \| unfold Rminus; apply Rplus_le_compat_r; apply Rplus_le_compat_l ].
563		replace (q+ -1)%Z with (1 + (q+ -2))%Z; [ idtac \| ring ].
	558	replace (- powerRZ radix (q -1) +
	559	(2 * 1 * powerRZ radix (q -1) - 1 -
	560	powerRZ radix (- k - N + q -1)))%R with
	561	(powerRZ radix (q -1) - 1 -
	562	powerRZ radix (- k - N + q -1))%R by ring.
	563	apply
	564	Rle_trans with (powerRZ radix (q -1) - 1- powerRZ radix (q-2) )%R;
	565	[ idtac \| unfold Rminus; apply Rplus_le_compat_l ].
	566	replace (q -1)%Z with (1 + (q -2))%Z; [ idtac \| ring ].
564	567	rewrite powerRZ_add with (n := 1%Z); auto with real zarith.
565	568	simpl (powerRZ radix 1) in \|- *.
566	569	apply Rplus_le_reg_l with 1%R.

993	996	Closest b radix (u - 3%nat * powerRZ radix (Zpred (Zpred (prec - N))))
994	997	zH1.
995	998
996
997		Hypothesis xPos : (0 <= x)%R.
998	999	Hypothesis p_enough : (3 < prec)%Z.
999	1000	Hypothesis N_not_too_big : (N <= dExp b)%Z.
1000	1001
1001	1002	(** As before, zH shall no be 2^(-N) *)
1002		Hypothesis zH_not_too_small : (powerRZ radix (2 - Zsucc N) <= zH1)%R.
	1003	Hypothesis zH_not_too_small : (powerRZ radix (2 - Zsucc N) <= Rabs zH1)%R.
1003	1004
1004	1005	(** And x must not be too big *)
1005	1006	Hypothesis
1006	1007	xalpha_small :
1007		(x * alpha <=
	1008	(Rabs (x * alpha) <=
1008	1009	powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N))%R.
1009	1010
1010	1011

1029	1030	Hint Resolve vNum_eq_Zpower_bzH_fn vNum_eq_Zpower_bzH2_fn: zarith.
1030	1031
1031	1032
1032		Theorem zH1Pos : (0 <= zH1)%R.
	1033	Theorem zH1Pos : (0 <= x)%R -> (0 <= zH1)%R.
	1034	intros L.
1033	1035	unfold FtoRradix in \|- *;
1034	1036	apply
1035	1037	RleRoundedR0

1068	1070	apply Rplus_le_compat_l; apply Rmult_le_pos; auto with real.
1069	1071	Qed.
1070	1072
	1073
	1074	Theorem zH1Neg : (x <= 0)%R -> (zH1 <= 0)%R.
	1075	intros L.
	1076	unfold FtoRradix in \|- *;
	1077	apply
	1078	RleRoundedLessR0
	1079	with
	1080	b
	1081	prec
	1082	(Closest b radix)
	1083	(u - 3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R;
	1084	auto with zarith.
	1085	apply ClosestRoundedModeP with prec; auto with zarith.
	1086	replace (3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R with
	1087	(FtoRradix (Float 3%nat (Zpred (Zpred (prec - N)))));
	1088	[ idtac \| unfold FtoRradix, FtoR in \|- ; simpl in \|- ; ring ].
	1089	apply
	1090	Rplus_le_reg_l with (FtoRradix (Float 3%nat (Zpred (Zpred (prec - N))))).
	1091	ring_simplify.
	1092	unfold FtoRradix in \|- *;
	1093	apply
	1094	RleBoundRoundr
	1095	with
	1096	b
	1097	prec
	1098	(Closest b radix)
	1099	(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha)%R;
	1100	auto with zarith.
	1101	apply ClosestRoundedModeP with prec; auto with zarith.
	1102	split; simpl in \|- *; auto with zarith.
	1103	rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 2);
	1104	auto with zarith arith.
	1105	apply Zle_trans with (- N)%Z; auto with zarith arith.
	1106	apply Zplus_le_reg_r with (N + 2)%Z; unfold Zpred in \|- *.
	1107	ring_simplify; auto with arith zarith.
	1108	replace (FtoR radix (Float 3%nat (Zpred (Zpred (prec - N))))) with
	1109	(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + 0)%R;
	1110	[ auto with real \| unfold FtoRradix, FtoR in \|- ; simpl in \|- ; ring ].
	1111	apply Rplus_le_compat_l; auto with real.
	1112	apply Rle_trans with (0*alpha)%R; auto with real.
	1113	Qed.
	1114
	1115
	1116
	1117
	1118
	1119
1071	1120	(** First computation correct *)
1072	1121
1073	1122	Theorem zH1_eq :

1099	1148	split; simpl in \|- *; auto with zarith.
1100	1149	rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 2);
1101	1150	auto with zarith arith.
1102		apply Rle_trans with (FtoR radix (Float 3%nat (Zpred (Zpred (prec - N))))).
1103		apply
1104		Rle_trans with (1 * FtoR radix (Float 3%nat (Zpred (Zpred (prec - N)))))%R;
1105		[ apply Rmult_le_compat_r \| right; ring ].
1106		unfold FtoR in \|- *; apply Rmult_le_pos; auto with real zarith.
1107		rewrite <- Rinv_1; apply Rle_Rinv; auto with real zarith.
	1151	apply Rle_trans with (FtoR radix (Float 2%nat (Zpred (Zpred (prec - N))))).
	1152	unfold FtoRradix, FtoR; simpl.
	1153	rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real zarith.
	1154	apply Rle_trans with (/2*(2+1+1))%R; auto with real.
	1155	right; field.
1108	1156	apply
1109	1157	RleBoundRoundl
1110	1158	with

1117	1165	split; simpl in \|- *; auto with zarith.
1118	1166	rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 2);
1119	1167	auto with zarith arith.
1120		replace (FtoR radix (Float 3%nat (Zpred (Zpred (prec - N))))) with
1121		(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + 0)%R;
	1168	replace (FtoR radix (Float 2%nat (Zpred (Zpred (prec - N))))) with
	1169	(2%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R;
1122	1170	[ auto with real \| unfold FtoRradix, FtoR in \|- ; simpl in \|- ; ring ].
1123		apply Rplus_le_compat_l; apply Rmult_le_pos; auto with real.
	1171	apply Rplus_le_reg_l with (-x*alpha
	1172	- 2%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R.
	1173	simpl; ring_simplify.
	1174	apply Rle_trans with (-(x*alpha))%R; auto with real.
	1175	apply Rle_trans with (Rabs (-(x*alpha)));[apply RRle_abs\|idtac].
	1176	rewrite Rabs_Ropp; apply Rle_trans with (1:=xalpha_small).
	1177	simpl; unfold Rminus; apply Rle_trans with
	1178	(powerRZ radix (Zpred (Zpred (prec - N))) +-0)%R; auto with real zarith.
	1179	unfold radix; simpl; right; ring.
1124	1180	cut
1125	1181	(FtoR radix (Float 2%nat (Zpred (prec - N))) =
1126	1182	(4%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R);

1143	1199	with
1144	1200	(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) +
1145	1201	powerRZ radix (Zpred (Zpred (prec - N))))%R; auto with real.
1146		apply Rplus_le_compat_l; apply Rle_trans with (1 := xalpha_small);
	1202	apply Rplus_le_compat_l.
	1203	apply Rle_trans with (Rabs (x*alpha));[apply RRle_abs\|idtac].
	1204	apply Rle_trans with (1 := xalpha_small);
1147	1205	apply Rle_trans with (powerRZ radix (Zpred (Zpred (prec - N))) - 0)%R;
1148	1206	auto with real zarith; unfold Rminus in \|- *; apply Rplus_le_compat_l;
1149	1207	auto with real zarith.

1217	1275	auto with zarith arith.
1218	1276	apply Zle_trans with (- N)%Z; auto with zarith arith.
1219	1277	rewrite <- inj_pred; auto with zarith arith.
1220		apply Rle_trans with (powerRZ radix (Zpred prec + - N) + 0)%R;
	1278	apply Rle_trans with (powerRZ radix (Zpred prec + - N))%R;
1221	1279	[ right; unfold FtoRradix, FtoR in \|- ; simpl in \|- ; ring \| idtac ].
1222		apply Rplus_le_compat; [ idtac \| apply Rmult_le_pos; auto with real ].
1223		apply Rle_trans with (2%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R;
1224		auto with real zarith arith.
1225		replace (Zpred prec + - N)%Z with (1 + Zpred (Zpred (prec - N)))%Z;
1226		[ idtac \| unfold Zpred in \|- *; ring ].
1227		rewrite powerRZ_add; auto with zarith real; simpl in \|- *; right; ring.
	1280	apply Rle_trans with (2%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R.
	1281	unfold Zpred, Zminus; repeat rewrite powerRZ_add; auto with real zarith.
	1282	simpl; right; field.
	1283	apply Rplus_le_reg_l with (-x*alpha-
	1284	2%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R; simpl; ring_simplify.
	1285	apply Rle_trans with (-(x*alpha))%R; auto with real.
	1286	apply Rle_trans with (Rabs (-(x*alpha)))%R; try apply RRle_abs.
	1287	rewrite Rabs_Ropp;apply Rle_trans with (1:=xalpha_small).
	1288	unfold Rminus, radix; simpl.
	1289	apply Rle_trans with (powerRZ 2 (Zpred (Zpred (prec - N))) + - 0)%R; auto with real zarith.
	1290	right; ring.
1228	1291	apply Rle_lt_trans with (FtoRradix (Float (Zpower_nat radix prec - 1) (- N))).
1229	1292	unfold FtoRradix in \|- *;
1230	1293	apply

1244	1307	(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) +
1245	1308	(powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N)))%R;
1246	1309	auto with real.
	1310	apply Rplus_le_compat_l; apply Rle_trans with (Rabs (x*alpha)); auto.
	1311	apply RRle_abs.
1247	1312	right; unfold FtoR in \|- ; simpl in \|- .
1248	1313	rewrite <- Z_R_minus; rewrite Zpower_nat_Z_powerRZ; ring_simplify.
1249	1314	rewrite <- powerRZ_add; auto with real zarith.

1269	1334	1 < p ->
1270	1335	(- dExp d <= e)%Z ->
1271	1336	f = Float m e :>R ->
1272		(powerRZ radix (Zpred p + e) <= f)%R ->
1273		(f < powerRZ radix (p + e))%R ->
	1337	(powerRZ radix (Zpred p + e) <= Rabs f)%R ->
	1338	(Rabs f < powerRZ radix (p + e))%R ->
1274	1339	ex (fun g : float => g = f :>R /\ Fnormal radix d g /\ Fexp g = e).
1275	1340	intros f d e m p H1 H2 H3 H4 H5 H6.
1276		cut (0 <= m)%Z; [ intros H8 \| idtac ].
1277	1341	cut (Fbounded d (Float m e)); [ intros H7 \| idtac ].
1278	1342	exists (Float m e).
1279	1343	split; auto with real; split; auto; split; auto.
1280	1344	rewrite H1; simpl (Fnum (Float m e)) in \|- *.
1281		rewrite Zabs_Zmult; rewrite Zabs_eq; auto with zarith; rewrite Zabs_eq;
1282		auto with zarith.
	1345	rewrite Zabs_Zmult; rewrite Zabs_eq; auto with zarith.
1283	1346	apply le_IZR; rewrite Zpower_nat_Z_powerRZ; rewrite mult_IZR.
1284	1347	apply Rmult_le_reg_l with (powerRZ radix (Zpred e)); auto with real zarith.
1285	1348	rewrite <- powerRZ_add; auto with real zarith.
1286	1349	replace (Zpred e + p)%Z with (Zpred p + e)%Z;
1287	1350	[ idtac \| unfold Zpred in \|- *; ring ].
	1351	rewrite <- Rabs_Zabs.
1288	1352	apply Rle_trans with (1 := H5); rewrite H4; unfold FtoRradix, FtoR in \|- *;
1289	1353	simpl in \|- *.
	1354	rewrite Rabs_mult; rewrite Rabs_right with (powerRZ 2 e);[idtac\|
	1355	apply Rle_ge; auto with real zarith].
1290	1356	pattern e at 1 in \|- *; replace e with (1 + Zpred e)%Z;
1291	1357	[ idtac \| unfold Zpred in \|- *; ring ].
1292	1358	rewrite powerRZ_add; auto with zarith real; simpl in \|- *; right; ring.
1293	1359	split; auto with zarith.
1294		rewrite H1; simpl (Fnum (Float m e)) in \|- *; rewrite Zabs_eq;
1295		auto with zarith.
	1360	rewrite H1; simpl (Fnum (Float m e)) in \|- *.
1296	1361	apply lt_IZR; rewrite Zpower_nat_Z_powerRZ.
1297	1362	apply Rmult_lt_reg_l with (powerRZ radix e); auto with real zarith.
1298	1363	rewrite <- powerRZ_add; auto with real zarith.
1299	1364	rewrite Zplus_comm; apply Rle_lt_trans with (2 := H6); rewrite H4.
1300		unfold FtoRradix, FtoR in \|- ; simpl in \|- ; right; ring.
1301		replace m with (Fnum (Float m e)); auto.
1302		apply LeR0Fnum with radix; auto with real zarith.
1303		fold FtoRradix in \|- *; rewrite <- H4;
1304		apply Rle_trans with (powerRZ radix (Zpred p + e));
1305		auto with real zarith.
	1365	unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
	1366	unfold Fabs, FtoR in \|- ; simpl in \|- ; right; ring.
1306	1367	Qed.
1307	1368
1308	1369
1309	1370	Theorem u_bounds :
1310		(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) +
1311		powerRZ radix (Zsucc (- N)) <= u)%R /\
	1371	(2%nat * powerRZ radix (Zpred (Zpred (prec - N))) +
	1372	powerRZ radix (- N) <= u)%R /\
1312	1373	(u <= powerRZ radix (prec - N) - powerRZ radix (- N))%R.
1313	1374	split.
1314		replace (FtoRradix u) with
1315		(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + zH1)%R;
1316		[ apply Rplus_le_compat_l \| rewrite zH1_eq; ring ].
1317		apply Rle_trans with (2 := zH_not_too_small); apply Rle_powerRZ;
1318		auto with real zarith.
	1375	apply Rle_trans with (FtoRradix (Float (Zpower_nat radix (prec-1) + 1) (- N))).
	1376	right; unfold FtoRradix, FtoR in \|- ; simpl in \|- .
	1377	rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; ring_simplify.
	1378	rewrite <- powerRZ_add; auto with real zarith.
	1379	replace (- N + (prec-1)%nat)%Z with (1 + Zpred (Zpred (prec - N)))%Z.
	1380	rewrite powerRZ_add; auto with real zarith; simpl in \|- *; ring.
	1381	apply trans_eq with (-N+pred prec)%Z; auto with zarith.
	1382	rewrite inj_pred; auto with zarith; unfold Zpred; ring.
	1383	unfold FtoRradix in \|- *;
	1384	apply
	1385	RleBoundRoundl
	1386	with
	1387	b
	1388	prec
	1389	(Closest b radix)
	1390	(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) + x * alpha)%R;
	1391	auto with zarith float.
	1392	apply ClosestRoundedModeP with prec; auto with zarith.
	1393	split; simpl in \|- *; auto with zarith.
	1394	rewrite pGivesBound; rewrite Zabs_eq; auto with zarith arith.
	1395	apply Zlt_le_trans with (Zpower_nat radix (prec - 1)+Zpower_nat radix (prec - 1))%Z;
	1396	auto with zarith.
	1397	assert (1 < Zpower_nat radix (prec - 1))%Z; auto with zarith.
	1398	apply Zle_lt_trans with (Zpower_nat radix 0); auto with zarith.
	1399	pattern prec at 3; replace prec with (1+(prec-1))%nat; auto with zarith.
	1400	rewrite Zpower_nat_is_exp.
	1401	replace (Zpower_nat radix 1) with 2%Z; auto with zarith.
	1402	apply
	1403	Rle_trans
	1404	with
	1405	(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) -
	1406	(powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N)))%R;
	1407	auto with real.
	1408	unfold FtoRradix, FtoR in \|- ; simpl in \|- ; rewrite plus_IZR;
	1409	rewrite Zpower_nat_Z_powerRZ.
	1410	simpl; ring_simplify.
	1411	rewrite Rplus_comm; apply Rplus_le_compat_l.
	1412	replace (Z_of_nat (prec -1)%nat) with (prec -1)%Z; auto with zarith.
	1413	unfold Zpred, Zminus; repeat rewrite powerRZ_add; auto with real zarith.
	1414	simpl; right; field; auto with real.
	1415	apply trans_eq with (Z_of_nat (pred prec)); auto with zarith.
	1416	rewrite inj_pred; auto with zarith.
	1417	unfold Rminus; apply Rplus_le_compat_l.
	1418	apply Rle_trans with (-(-(x*alpha)))%R; auto with real.
	1419	apply Ropp_le_contravar.
	1420	apply Rle_trans with (Rabs (-(x*alpha))); try apply RRle_abs; rewrite Rabs_Ropp.
	1421	apply Rle_trans with (1:=xalpha_small); auto with real.
1319	1422	apply Rle_trans with (FtoRradix (Float (Zpower_nat radix prec - 1) (- N))).
1320	1423	unfold FtoRradix in \|- *;
1321	1424	apply

1335	1438	(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) +
1336	1439	(powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N)))%R;
1337	1440	auto with real.
	1441	apply Rplus_le_compat_l; apply Rle_trans with (Rabs (x*alpha)); auto.
	1442	apply RRle_abs.
1338	1443	right; unfold FtoR in \|- ; simpl in \|- .
1339	1444	rewrite <- Z_R_minus; rewrite Zpower_nat_Z_powerRZ; ring_simplify.
1340	1445	rewrite <- powerRZ_add; auto with real zarith.

1354	1459	Theorem exists_k :
1355	1460	ex
1356	1461	(fun k : Z =>
1357		(powerRZ radix k <= zH1)%R /\
1358		(zH1 < powerRZ radix (Zsucc k))%R /\
	1462	(powerRZ radix k <= Rabs zH1)%R /\
	1463	(Rabs zH1 < powerRZ radix (Zsucc k))%R /\
1359	1464	(Zsucc (k + N) <= Zpred (Zpred prec))%Z /\
1360	1465	(0 <= Zsucc (k + N))%Z /\
1361	1466	1 < Zabs_nat (Zsucc (k + N)) /\ (2 <= Zsucc (k + N))%Z).
1362		generalize zH1Pos; intros H1.
1363	1467	generalize u_bounds; intros T; elim T; intros H'1 H'2; clear T.
1364	1468	exists (pred (digit radix (Fnum zH1)) + Fexp zH1)%Z.
1365		cut (powerRZ radix (pred (digit radix (Fnum zH1)) + Fexp zH1) <= zH1)%R;
	1469	cut (powerRZ radix (pred (digit radix (Fnum zH1)) + Fexp zH1) <= Rabs zH1)%R;
1366	1470	[ intros H2 \| idtac ].
1367	1471	cut
1368		(zH1 < powerRZ radix (Zsucc (pred (digit radix (Fnum zH1)) + Fexp zH1)))%R;
	1472	(Rabs zH1 < powerRZ radix (Zsucc (pred (digit radix (Fnum zH1)) + Fexp zH1)))%R;
1369	1473	[ intros H3 \| idtac ].
1370	1474	2: replace (Zsucc (pred (digit radix (Fnum zH1)) + Fexp zH1)) with
1371	1475	(Zsucc (pred (digit radix (Fnum zH1))) + Fexp zH1)%Z;
1372	1476	[ idtac \| unfold Zsucc in \|- *; ring ].
1373		2: unfold FtoRradix, FtoR in \|- *; rewrite powerRZ_add; auto with real zarith.
	1477	2: rewrite powerRZ_add; auto with real zarith.
	1478	2: unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith; unfold Fabs, FtoR in \|- *; simpl.
1374	1479	2: apply Rmult_lt_compat_r; auto with real zarith.
1375	1480	2: replace (Zsucc (pred (digit radix (Fnum zH1)))) with
1376	1481	(Z_of_nat (S (pred (digit radix (Fnum zH1)))));
1377	1482	auto with arith zarith.
	1483	2: replace 2%R with (IZR radix); auto with real zarith.
1378	1484	2: rewrite <- Zpower_nat_Z_powerRZ; apply Rlt_IZR.
1379		2: apply Zle_lt_trans with (Zabs (Fnum zH1)); auto with zarith.
1380	1485	2: apply Zlt_le_trans with (Zpower_nat radix (digit radix (Fnum zH1)));
1381	1486	auto with arith zarith.
1382	1487	2: unfold Zsucc in \|- *; replace 1%Z with (Z_of_nat 1);

1391	1496	(pred (digit radix (Fnum zH1)) + Fexp zH1)%Z; [ idtac \| ring ].
1392	1497	apply Zlt_powerRZ with radix; auto with real zarith.
1393	1498	apply Rle_lt_trans with (1 := H2); rewrite zH1_eq.
	1499	unfold Rabs; case Rcase_abs; intros.
	1500	apply Rplus_lt_reg_r with (u-powerRZ radix (Zpred (Zpred prec) + - N))%R;
	1501	ring_simplify.
	1502	apply Rlt_le_trans with (2:=H'1).
	1503	apply Rle_lt_trans with (2%nat * powerRZ radix (Zpred (Zpred (prec - N)))
	1504	+ 0)%R;[right\|auto with real zarith].
	1505	replace (Zpred (Zpred prec) + - N)%Z with (Zpred (Zpred (prec - N)));
	1506	[idtac\|unfold Zpred]; simpl; ring.
1394	1507	apply
1395	1508	Rplus_lt_reg_r with (3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R.
1396	1509	ring_simplify

1421	1534	replace (- N + 1)%Z with (Zsucc (- N));
1422	1535	[ idtac \| unfold Zsucc in \|- *; ring ].
1423	1536	apply Zlt_powerRZ with radix; auto with real zarith.
1424		apply Rle_lt_trans with (2 := H3); rewrite zH1_eq.
1425		apply
1426		Rle_trans
1427		with
1428		(3%nat * powerRZ radix (Zpred (Zpred (prec - N))) +
1429		powerRZ radix (Zsucc (- N)) -
1430		3%nat * powerRZ radix (Zpred (Zpred (prec - N))))%R;
1431		auto with real.
1432		right; ring.
1433		unfold Rminus in \|- *; apply Rplus_le_compat_r; auto with real.
1434		unfold FtoRradix, FtoR in \|- *; rewrite powerRZ_add; auto with real zarith.
1435		apply Rmult_le_compat_r; auto with real zarith; rewrite <- Zpower_nat_Z_powerRZ;
1436		apply Rle_IZR.
1437		apply Zle_trans with (Zabs (Fnum zH1)).
	1537	apply Rle_lt_trans with (2 := H3).
	1538	apply Rle_trans with (2:=zH_not_too_small).
	1539	apply Rle_powerRZ; unfold Zsucc; auto with real zarith.
	1540	unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
	1541	unfold Fabs, FtoR in \|- *; rewrite powerRZ_add; auto with real zarith; simpl.
	1542	apply Rmult_le_compat_r; auto with real zarith.
	1543	replace 2%R with (IZR radix); auto with real zarith.
	1544	rewrite <- Zpower_nat_Z_powerRZ; apply Rle_IZR.
1438	1545	apply digitLess.
1439		cut (0 < Fnum zH1)%Z; auto with real zarith float.
1440		apply LtR0Fnum with radix; auto with real zarith.
1441		fold FtoRradix in \|- *; apply Rlt_le_trans with (2 := zH_not_too_small);
1442		auto with real zarith.
1443		rewrite Zabs_eq; auto with float zarith.
1444		apply LeR0Fnum with radix; auto with real zarith.
	1546	unfold not; intros.
	1547	Contradict zH_not_too_small.
	1548	apply Rlt_not_le; apply Rle_lt_trans with 0%R; auto with real.
	1549	replace (FtoRradix zH1) with 0%R.
	1550	rewrite Rabs_R0; auto with real.
	1551	unfold FtoRradix, FtoR; rewrite H; simpl; ring.
1445	1552	Qed.
1446	1553
1447	1554	(** Not very readable, I know, but those are the hypotheses I will

1454	1561	(fun k : Z =>
1455	1562	ex
1456	1563	(fun zH : float =>
1457		(0 <= zH)%R /\
1458	1564	zH1 = zH :>R /\
1459	1565	(Zsucc (k + N) <= Zpred (Zpred prec))%Z /\
1460	1566	(0 <= Zsucc (k + N))%Z /\

1462	1568	N = (- Fexp zH)%Z /\
1463	1569	Fnormal radix (bzH k) zH /\
1464	1570	(Rabs (x * alpha - zH) <= powerRZ radix (Zpred (- N)))%R /\
1465		(powerRZ radix k <= zH1)%R /\ (zH1 < powerRZ radix (Zsucc k))%R)).
	1571	(powerRZ radix k <= Rabs zH1)%R /\ (Rabs zH1 < powerRZ radix (Zsucc k))%R)).
1466	1572	generalize exists_k; intros T1.
1467	1573	elim T1; intros k T2; elim T2; intros H1 T3; elim T3; intros H2 T4; elim T4;
1468	1574	intros H3 T5; elim T5; intros H4 T6; elim T6; intros H5 H6;

1481	1587	elim T; intros zH T1.
1482	1588	elim T1; intros H9 T2; elim T2; intros H10 H11; clear T T1 T2.
1483	1589	exists k; exists zH.
1484		split; [ rewrite H9; apply zH1Pos \| idtac ].
1485	1590	split; auto with real.
1486	1591	split; auto with zarith.
1487	1592	split; auto.

1553	1658
1554	1659	Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
1555	1660	Hypothesis Fboundedx : Fbounded b x.
1556		Hypothesis xPos : (0 <= x)%R.
	1661
1557	1662
1558	1663	(** alpha (the constant, such as pi) and gamma (its inverse) *)
1559	1664	Hypothesis alphaNormal : Fnormal radix b alpha.

1586	1691	(** x not too big *)
1587	1692	Hypothesis
1588	1693	xalpha_small :
1589		(x * alpha <=
	1694	(Rabs (x * alpha) <=
1590	1695	powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N))%R.
1591	1696
1592	1697	(** No underflow *)

1628	1733	apply Rle_ge; apply Rplus_le_reg_l with y; apply Rle_trans with y; auto with real.
1629	1734	apply Rle_trans with x0; auto with real.
1630	1735	Qed.
	1736
	1737
	1738	Lemma Sterbenzter: forall (x y :float),
	1739	Fbounded b x ->
	1740	Fbounded b y ->
	1741	(/ S 1 * Rabs y <= Rabs x)%R ->
	1742	(Rabs x <= S 1 * Rabs y)%R ->
	1743	(0 <= x*y)%R ->
	1744	Fbounded b (Fminus radix x y) /\
	1745	(Rabs (x - y) <= Rabs y)%R.
	1746	intros r1 r2; intros.
	1747	case (Rle_or_lt 0 r1); case (Rle_or_lt 0 r2); intros.
	1748	rewrite (Rabs_right r2); try apply Rle_ge; auto with real.
	1749	apply Sterbenzbis; auto.
	1750	rewrite Rabs_right in H1; rewrite Rabs_right in H1; try apply Rle_ge; auto with real.
	1751	rewrite Rabs_right in H2; rewrite Rabs_right in H2; try apply Rle_ge; auto with real.
	1752	case H5; intros.
	1753	Contradict H3; auto with real.
	1754	apply Rlt_not_le; apply Rlt_le_trans with (r1*0)%R; auto with real.
	1755	assert (FtoRradix r2=0)%R.
	1756	assert (Rabs r2=0)%R; auto with real.
	1757	assert (Rabs r2 <=0)%R; auto with real.
	1758	apply Rmult_le_reg_l with (/2%nat)%R; auto with real zarith.
	1759	apply Rle_trans with (1:=H1); rewrite <- H6; rewrite Rabs_R0; right; ring.
	1760	case (Req_dec r2 0); auto.
	1761	intros; Contradict H7; apply Rabs_no_R0; auto.
	1762	rewrite (Rabs_right r2).
	1763	apply Sterbenzbis; auto.
	1764	rewrite <- H6; rewrite H7; auto with real.
	1765	rewrite <- H6; rewrite H7; auto with real.
	1766	rewrite H7; auto with real.
	1767	case H4; intros.
	1768	Contradict H3; auto with real.
	1769	apply Rlt_not_le; apply Rlt_le_trans with (0*r2)%R; auto with real.
	1770	assert (FtoRradix r1=0)%R.
	1771	assert (Rabs r1=0)%R; auto with real.
	1772	assert (Rabs r1 <=0)%R; auto with real.
	1773	apply Rle_trans with (1:=H2); rewrite <- H6; rewrite Rabs_R0; right; ring.
	1774	case (Req_dec r1 0); auto.
	1775	intros; Contradict H7; apply Rabs_no_R0; auto.
	1776	rewrite (Rabs_right r2).
	1777	apply Sterbenzbis; auto.
	1778	rewrite <- H6; rewrite H7; auto with real.
	1779	rewrite <- H6; rewrite H7; auto with real.
	1780	rewrite <- H6; auto with real.
	1781	assert (Fbounded b (Fminus radix (Fopp r1) (Fopp r2))
	1782	/\ (Rabs (Fopp r1 - Fopp r2) <= (Fopp r2))%R).
	1783	apply Sterbenzbis; auto with zarith float.
	1784	unfold FtoRradix; repeat rewrite Fopp_correct; fold FtoRradix.
	1785	rewrite Rabs_left1 in H1; rewrite Rabs_left1 in H1; auto with real.
	1786	unfold FtoRradix; repeat rewrite Fopp_correct; fold FtoRradix.
	1787	rewrite Rabs_left1 in H2; rewrite Rabs_left1 in H2; auto with real.
	1788	elim H6; intros; split.
	1789	apply oppBoundedInv.
	1790	rewrite Fopp_Fminus_dist; auto with zarith float.
	1791	replace (r1-r2)%R with (-(Fopp r1-Fopp r2))%R.
	1792	rewrite Rabs_Ropp; apply Rle_trans with (1:=H8).
	1793	right; rewrite Rabs_left1; auto with real.
	1794	unfold FtoRradix; rewrite Fopp_correct; auto.
	1795	unfold FtoRradix; repeat rewrite Fopp_correct; ring.
	1796	Qed.
	1797
	1798
1631	1799
1632	1800	(** Main result: q can be anything but we need alpha * gamma <= 1 *)
1633	1801	Theorem Fmac_arg_reduct_correct2 :

1720	1888	unfold FtoRradix; apply FnormalBoundAbs2 with prec; auto with zarith.
1721	1889	unfold FtoRradix; rewrite Fabs_correct; auto with zarith;
1722	1890	rewrite Rabs_right; try apply Rle_ge; auto with zarith real.
1723		case (Rle_or_lt (powerRZ radix (q - Zsucc N)) zH1); intros H'.
	1891	case (Rle_or_lt (powerRZ radix (q - Zsucc N)) (Rabs zH1)); intros H'.
1724	1892	cut
1725	1893	(exists k : Z,
1726	1894	(exists zH : float,
1727		(0 <= FtoR 2 zH)%R /\
1728	1895	FtoR 2 zH1 = FtoR 2 zH /\
1729	1896	(Zsucc (k + N) <= Zpred (Zpred prec))%Z /\
1730	1897	(0 <= Zsucc (k + N))%Z /\

1738	1905	(dExp b)) k) zH /\
1739	1906	(Rabs (FtoR 2 x * FtoR 2 alpha - FtoR 2 zH) <=
1740	1907	powerRZ 2%Z (Zpred (- N)))%R /\
1741		(powerRZ 2%Z k <= FtoR 2 zH1 < powerRZ 2%Z (Zsucc k))%R)).
	1908	(powerRZ 2%Z k <= Rabs (FtoR 2 zH1) < powerRZ 2%Z (Zsucc k))%R)).
1742	1909	2: apply arg_reduct_exists_k_zH with u; auto with real zarith.
1743	1910	fold radix FtoRradix in \|- *.
1744		intros T1; elim T1; intros k T2; elim T2; intros zH T3; elim T3; intros H2 T4;
1745		elim T4; intros H3 T5; elim T5; intros H4 T6; elim T6;
1746		intros H5 T7; elim T7; intros H6 T8; elim T8; intros H7 T9;
1747		elim T9; intros H8 T10; elim T10; intros H9 T11; elim T11;
1748		intros H10 H11; clear T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11.
	1911	intros T1; elim T1; intros k T2; elim T2; intros zH T3; elim T3; intros H3 T4;
	1912	elim T4; intros H4 T5; elim T5; intros H5 T6; elim T6;
	1913	intros H6 T7; elim T7; intros H7 T8; elim T8; intros H8 T9;
	1914	elim T9; intros H9 T10; elim T10; intros H10 H11;
	1915	clear T1 T2 T3 T4 T5 T6 T7 T8 T9 T10.
1749	1916	rewrite H3.
1750	1917	apply Fmac_arg_reduct_correct1 with q k alpha (x * alpha - zH)%R;
1751	1918	auto with zarith real arith.

1766	1933	cut
1767	1934	(exists zH : float,
1768	1935	FtoRradix zH1 = zH /\
1769		Fexp zH = (- N)%Z /\ (Fnum zH < powerRZ radix (Zpred q))%R /\ (0 < zH)%R).
	1936	Fexp zH = (- N)%Z /\ (Zabs (Fnum zH) < powerRZ radix (Zpred q))%R /\ (0 < Rabs zH)%R).
1770	1937	intros V; elim V; intros zH V1; elim V1; intros H2 V2; elim V2; intros H3 V3;
1771	1938	elim V3; intros H4 H5; clear V V1 V2 V3.
1772	1939	assert ((Fbounded b (Fminus radix x (Fmult zH gamma))
1773		/\ (Rabs (x - (Fmult zH gamma)) <= (Fmult zH gamma))%R)).
1774		apply Sterbenzbis; auto with zarith.
	1940	/\ (Rabs (x - (Fmult zH gamma)) <= Rabs (Fmult zH gamma))%R)).
	1941	apply Sterbenzter; auto with zarith.
1775	1942	split; unfold Fmult in \|- ; simpl in \|- .
1776	1943	apply Zlt_Rlt; rewrite <- Faux.Rabsolu_Zabs; rewrite Rmult_IZR;
1777	1944	rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.

1779	1946	[ rewrite powerRZ_add \| rewrite inj_minus1 ];
1780	1947	auto with arith zarith real.
1781	1948	rewrite Rabs_mult; apply Rmult_le_0_lt_compat; auto with real.
1782		rewrite Rabs_right; [ apply Rlt_trans with (1 := H4) \| idtac ];
	1949	rewrite Rabs_Zabs; apply Rlt_trans with (1 := H4);
1783	1950	auto with real zarith.
1784		apply Rle_ge; replace 0%R with (IZR 0); auto with real zarith; apply Rle_IZR.
1785		apply LeR0Fnum with radix; auto with zarith real.
1786	1951	apply Rlt_le_trans with (IZR (Zpos (vNum bmoinsq)));
1787	1952	auto with real zarith.
1788	1953	rewrite Faux.Rabsolu_Zabs; elim gammaNormal; intros T1 T2; elim T1;

1806	1971	rewrite minus_Zminus_precq; auto with real zarith.
1807	1972	unfold FtoRradix; rewrite Fmult_correct; auto with zarith; fold FtoRradix in \|- *;
1808	1973	apply Rmult_le_reg_l with alpha; auto with real.
1809		apply Rle_trans with (/ 2%nat * zH * (alpha * gamma))%R;
	1974	rewrite Rabs_mult; rewrite Rabs_right with gamma; try apply Rle_ge; auto with real.
	1975	apply Rle_trans with (/ 2%nat * Rabs zH * (alpha * gamma))%R;
1810	1976	[ right; ring \| idtac ].
1811		apply Rle_trans with (/ 2%nat * zH * 1)%R;
	1977	apply Rle_trans with (/ 2%nat * Rabs zH * 1)%R;
1812	1978	[ apply Rmult_le_compat_l; auto \| idtac ].
1813	1979	apply Rmult_le_pos; auto with real zarith arith real.
1814		apply Rplus_le_reg_l with (/ 2%nat * zH - alpha * x)%R.
	1980	apply Rplus_le_reg_l with (/ 2%nat * Rabs zH - alpha * Rabs x)%R.
1815	1981	ring_simplify.
1816		apply Rle_trans with (zH - x * alpha)%R; [ right \| idtac ].
	1982	apply Rle_trans with (Rabs zH - Rabs x * alpha)%R; [ right \| idtac ].
1817	1983	simpl; field; auto with real.
1818		apply Rle_trans with (Rabs (zH - x * alpha)); [ apply RRle_abs \| idtac ].
	1984	replace (Rabs xalpha)%R with (Rabs (xalpha));[idtac\|rewrite Rabs_mult;
	1985	rewrite Rabs_right with alpha; try apply Rle_ge; auto with real].
	1986	apply Rle_trans with (Rabs (zH - x * alpha)); [ apply Rabs_triang_inv \| idtac ].
1819	1987	rewrite <- H2; unfold FtoRradix, radix in \|- *;
1820	1988	rewrite zH1_eq with b prec N alpha x u zH1; auto with real zarith.
1821	1989	fold radix FtoRradix in \|- *; rewrite <- Rabs_Ropp.

1835	2003	unfold FtoRradix, FtoR in \|- *; auto with real zarith.
1836	2004	apply Rle_trans with (1 * (1 * powerRZ radix (Fexp zH)))%R;
1837	2005	[ right; ring \| idtac ].
	2006	rewrite Rabs_mult.
	2007	rewrite Rabs_right with (powerRZ radix (Fexp zH)); try apply Rle_ge; auto with real zarith.
1838	2008	apply Rmult_le_compat_l; auto with real; apply Rmult_le_compat_r;
1839	2009	auto with real zarith.
1840		cut (0 < Fnum zH)%Z; auto with real float zarith.
	2010	rewrite Rabs_Zabs.
	2011	cut (0 < Zabs (Fnum zH))%Z; auto with real float zarith.
	2012	apply Zlt_le_trans with (Fnum (Fabs (zH))); auto with zarith.
1841	2013	apply LtR0Fnum with radix; auto with real zarith.
	2014	rewrite Fabs_correct; auto with real zarith.
1842	2015	unfold FtoRradix; rewrite Fmult_correct; auto with zarith; fold FtoRradix in \|- *;
1843	2016	apply Rmult_le_reg_l with alpha; auto with real.
1844		apply Rplus_le_reg_l with (- zH)%R.
1845		apply Rle_trans with (x * alpha - zH)%R; [ right; ring \| idtac ].
1846		apply Rle_trans with (Rabs (x * alpha - zH)); [ apply RRle_abs \| idtac ].
	2017	apply Rplus_le_reg_l with (- Rabs zH)%R.
	2018	replace (alphaRabs x)%R with (Rabs (xalpha));[idtac\|
	2019	rewrite Rabs_mult; rewrite (Rabs_right alpha); try apply Rle_ge; auto with real].
	2020	apply Rle_trans with (Rabs (x * alpha) - Rabs zH)%R; [ right; ring \| idtac ].
	2021	apply Rle_trans with (Rabs (x * alpha - zH)); [ apply Rabs_triang_inv \| idtac ].
1847	2022	pattern (FtoRradix zH) at 1 in \|- *; rewrite <- H2.
1848	2023	unfold FtoRradix, radix in \|- *; rewrite zH1_eq with b prec N alpha x u zH1;
1849	2024	auto with real zarith.

1857	2032	unfold FtoRradix in \|- *; apply ClosestUlp; auto with zarith real.
1858	2033	unfold Fulp, radix in \|- *; rewrite Fexp_u with b prec N alpha x u;
1859	2034	auto with real zarith; fold radix in \|- *.
1860		apply Rle_trans with (2%nat * zH * (2%nat * (alpha * gamma) - 1))%R;
1861		[ idtac \| right; ring ].
	2035	apply Rle_trans with (2%nat * Rabs zH * (2%nat * (alpha * gamma) - 1))%R;
	2036	[ idtac \| rewrite Rabs_mult; rewrite (Rabs_right gamma); try apply Rle_ge; auto with real;
	2037	right; ring ].
1862	2038	apply
1863	2039	Rle_trans
1864	2040	with (powerRZ radix (- N) * (2%nat * (2%nat * (alpha * gamma) - 1)))%R.

1881	2057	apply Rle_trans with (powerRZ radix (q - prec)).
1882	2058	unfold FtoRradix, radix in \|- *; apply delta_inf with b; auto with zarith.
1883	2059	apply Rle_powerRZ; auto with real zarith.
1884		apply Rle_trans with (zH * (2%nat * (2%nat * (alpha * gamma) - 1)))%R;
	2060	apply Rle_trans with (Rabs zH * (2%nat * (2%nat * (alpha * gamma) - 1)))%R;
1885	2061	[ apply Rmult_le_compat_r \| right; ring ].
1886	2062	apply Rmult_le_pos; auto with real arith zarith.
1887	2063	apply Rplus_le_reg_l with (-1)%R.

1896	2072	apply Rle_trans with (powerRZ radix (-1));
1897	2073	[ apply Rle_powerRZ; auto with real zarith \| idtac ].
1898	2074	right; simpl in \|- *; field; auto with real zarith.
1899		replace 4%R with (INR 4); auto with real arith; simpl in \|- *.
1900		2: ring.
1901		unfold FtoRradix, FtoR in \|- *; rewrite <- H3.
1902		apply Rle_trans with (1 * powerRZ radix (Fexp zH))%R; [ right; simpl ; ring \| idtac ].
	2075	unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
	2076	unfold Fabs, FtoR in \|- *; simpl; rewrite <- H3.
	2077	apply Rle_trans with (1 * powerRZ 2 (Fexp zH))%R; [ right; simpl ; ring \| idtac ].
1903	2078	apply Rmult_le_compat_r; auto with real zarith.
1904		cut (0 < Fnum zH)%Z; auto with real float zarith.
	2079	cut (0 < Zabs (Fnum zH))%Z; auto with real float zarith.
	2080	apply Zlt_le_trans with (Fnum (Fabs zH)); auto with zarith.
1905	2081	apply LtR0Fnum with radix; auto with real zarith.
	2082	rewrite Fabs_correct; auto with real zarith.
	2083	unfold FtoRradix; rewrite Fmult_correct; auto with zarith; fold FtoRradix.
	2084	cut (0 <= x*zH)%R.
	2085	intros; rewrite <- Rmult_assoc.
	2086	apply Rle_trans with (0*gamma)%R; auto with real.
	2087	case (Rle_or_lt 0 x); intros.
	2088	assert (0 <= zH)%R; auto with real.
	2089	rewrite <- H2; apply zH1Pos with b prec N alpha x u; auto with zarith.
	2090	apply Rle_trans with (x*0)%R; auto with real.
	2091	assert (zH <= 0)%R; auto with real.
	2092	rewrite <- H2; apply zH1Neg with b prec N alpha x u; auto with zarith real.
	2093	apply Rle_trans with ((-x)*(-zH))%R; auto with real.
	2094	apply Rle_trans with ((-x)*0)%R; auto with real.
1906	2095	elim H; intros; split.
1907	2096	exists (Fminus radix x (Fmult zH gamma)).
1908	2097	split;

1913	2102	rewrite H2; unfold FtoRradix; rewrite <- Fmult_correct; auto with zarith.
1914	2103	apply Rle_lt_trans with (1:=H6).
1915	2104	unfold FtoRradix; rewrite Fmult_correct; auto with zarith.
	2105	fold FtoRradix; rewrite Rabs_mult; rewrite (Rabs_right gamma).
	2106	2: apply Rle_ge; auto with real.
1916	2107	apply Rlt_le_trans with (powerRZ radix (q-Zsucc N)*powerRZ radix ((prec-q)+Fexp gamma))%R.
1917		apply Rlt_le_trans with (powerRZ radix (q - Zsucc N)*FtoR radix gamma)%R.
	2108	apply Rlt_le_trans with (powerRZ radix (q - Zsucc N)* gamma)%R.
1918	2109	apply Rmult_lt_compat_r; auto with real.
1919	2110	fold FtoRradix; rewrite <- H2; exact H'.
1920	2111	apply Rmult_le_compat_l; auto with real zarith.
1921		unfold FtoR; rewrite powerRZ_add; auto with real zarith.
	2112	unfold FtoRradix, FtoR; rewrite powerRZ_add; auto with real zarith.
1922	2113	apply Rmult_le_compat_r; auto with real zarith.
1923	2114	elim gammaNormal; intros T1 T2; elim T1; intros T3 T4.
1924	2115	apply Rle_trans with (Rabs (Fnum gamma));[apply RRle_abs\|rewrite Rabs_Zabs].

1941	2132	split; [ simpl in \|- *; auto \| idtac ].
1942	2133	split.
1943	2134	apply Rmult_lt_reg_l with (powerRZ radix (- N)); auto with real zarith.
1944		apply Rle_lt_trans with (FtoRradix zH1);
1945		[ right; rewrite V; unfold FtoRradix, FtoR in \|- *; simpl; ring \| idtac ].
	2135	apply Rle_lt_trans with (Rabs (FtoRradix zH1)).
	2136	right; rewrite V; unfold FtoRradix, Fabs, FtoR.
	2137	apply trans_eq with (Rabs ((Fnum (Fnormalize radix b prec u) -
	2138	3%nat * Zpower_nat radix (pred (pred prec)))%Z*powerRZ radix (-N))); auto with real.
	2139	rewrite Rabs_mult.
	2140	rewrite Rabs_right with (powerRZ radix (-N)); try apply Rle_ge; auto with real zarith.
	2141	rewrite Rabs_Zabs; auto with real zarith.
1946	2142	rewrite <- powerRZ_add; auto with real zarith.
1947	2143	replace (- N + Zpred q)%Z with (q - Zsucc N)%Z; auto;
1948	2144	unfold Zsucc, Zpred in \|- *; ring.
1949		rewrite <- V; cut (0 <= zH1)%R; auto with real.
1950		intros H''; case H''; auto with real; intros H2.
1951		absurd (0%R = zH1); auto with real.
1952		unfold FtoRradix, radix in \|- *; apply zH1Pos with b prec N alpha x u;
1953		auto with zarith.
	2145	rewrite <- V.
	2146	assert (0 <= Rabs zH1)%R; auto with real.
	2147	case H; auto; intros.
	2148	absurd (Rabs zH1 =0)%R; auto with real.
	2149	apply Rabs_no_R0; auto with real.
1954	2150	unfold FtoRradix, radix in \|- *; rewrite zH1_eq with b prec N alpha x u zH1;
1955	2151	auto with zarith.
1956	2152	rewrite <- FnormalizeCorrect with 2%Z b prec u; auto with zarith;

+135

-71

FnElem/FArgReduct3.v less more

36	36	Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
37	37	Hypothesis Fboundedx : Fbounded b x.
38	38	Hypothesis xCanonic : Fcanonic radix b x.
39		Hypothesis xPos : (0 <= x)%R.
40	39
41	40	(** alpha (the constant, such as pi) and gamma (its inverse) *)
42	41	Hypothesis alphaNormal : Fnormal radix b alpha.

64	63	(** x not too big *)
65	64	Hypothesis
66	65	xalpha_small :
67		(x * alpha <=
	66	(Rabs (x * alpha) <=
68	67	powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N))%R.
69	68
70	69	(** No underflow *)

306	305	replace (Zsucc (S 1)) with 3%Z; ring; simpl; ring.
307	306	apply Zle_trans with (1:=exp_alpha_le).
308	307	replace (Zsucc (S 1)) with 3%Z; auto with zarith.
309		case (Rle_or_lt (powerRZ radix (2 - Zsucc N)) zH1); intros H'.
	308	case (Rle_or_lt (powerRZ radix (2 - Zsucc N)) (Rabs zH1)); intros H'.
310	309	cut
311	310	(exists k : Z,
312	311	(exists zH : float,
313		(0 <= FtoR 2 zH)%R /\
314	312	FtoR 2 zH1 = FtoR 2 zH /\
315	313	(Zsucc (k + N) <= Zpred (Zpred prec))%Z /\
316	314	(0 <= Zsucc (k + N))%Z /\

324	322	(dExp b)) k) zH /\
325	323	(Rabs (FtoR 2 x * FtoR 2 alpha - FtoR 2 zH) <=
326	324	powerRZ 2%Z (Zpred (- N)))%R /\
327		(powerRZ 2%Z k <= FtoR 2 zH1 < powerRZ 2%Z (Zsucc k))%R)).
	325	(powerRZ 2%Z k <= (Rabs (FtoR 2 zH1)) < powerRZ 2%Z (Zsucc k))%R)).
328	326	2: apply arg_reduct_exists_k_zH with u; auto with real zarith.
329	327	fold radix FtoRradix in \|- *.
330		intros T1; elim T1; intros k T2; elim T2; intros zH T3; elim T3; intros H2 T4;
331		elim T4; intros H3 T5; elim T5; intros H4 T6; elim T6;
332		intros H5 T7; elim T7; intros H6 T8; elim T8; intros H7 T9;
333		elim T9; intros H8 T10; elim T10; intros H9 T11; elim T11;
334		intros H10 H11; clear T1 T2 T3 T4 T5 T6 T7 T8 T9 T10 T11.
	328	intros T1; elim T1; intros k T2; elim T2; intros zH T3; elim T3; intros H3 T4;
	329	elim T4; intros H4 T5; elim T5; intros H5 T6; elim T6;
	330	intros H6 T7; elim T7; intros H7 T8; elim T8; intros H8 T9;
	331	elim T9; intros H9 T10; elim T10; intros H10 H11;
	332	clear T1 T2 T3 T4 T5 T6 T7 T8 T9 T10.
335	333	rewrite H3.
336	334	apply Fmac_arg_reduct_correct1 with 2 k alpha (x * alpha - zH)%R;
337	335	auto with zarith real arith.

374	372	cut
375	373	(exists zH : float,
376	374	FtoRradix zH1 = zH /\
377		Fexp zH = (- N)%Z /\ (Fnum zH < powerRZ radix (Zpred 2))%R /\ (0 < zH)%R).
	375	Fexp zH = (- N)%Z /\ (Zabs (Fnum zH) < powerRZ radix (Zpred 2))%R /\ (0 < Rabs zH)%R).
378	376	2:exists
379	377	(Float
380	378	(Fnum (Fnormalize radix b prec u) -

384	382	2:split; [ simpl in \|- *; auto \| idtac ].
385	383	2:split.
386	384	2:apply Rmult_lt_reg_l with (powerRZ radix (- N)); auto with real zarith.
387		2:apply Rle_lt_trans with (FtoRradix zH1);
388		[ right; rewrite H'1; unfold FtoRradix, FtoR in \|- *; simpl; ring \| idtac ].
	385	2:apply Rle_lt_trans with (Rabs (FtoRradix zH1)).
	386	2: right; rewrite H'1; unfold FtoRradix, FtoR; simpl.
	387	2: rewrite Rabs_mult; rewrite Rabs_Zabs.
	388	2: rewrite Rabs_right; try apply Rle_ge; auto with real zarith.
389	389	2:rewrite <- powerRZ_add; auto with real zarith.
390	390	2:replace (- N + Zpred 2)%Z with (2 - Zsucc N)%Z; auto;
391	391	unfold Zsucc, Zpred in \|- *; ring.
392		2:rewrite <- H'1; cut (0 <= zH1)%R; auto with real.
	392	2:rewrite <- H'1; cut (0 <= Rabs zH1)%R; auto with real.
393	393	2:intros H''; case H''; auto with real; intros H2.
394		2:absurd (0%R = zH1); auto with real.
395		2:unfold FtoRradix, radix in \|- *; apply zH1Pos with b prec N alpha x u;
396		auto with zarith.
	394	2:absurd (Rabs zH1=0); auto with real.
	395	2: apply Rabs_no_R0; auto.
397	396	intros V; elim V; intros zH V1; elim V1; intros H2 V2; elim V2; intros H3 V3;
398	397	elim V3; intros H4 H5; clear V V1 V2 V3.
399		cut ((Fnum zH)=1)%Z;[intros H6\|idtac].
400		2: cut (0 < (Fnum zH))%Z;[intros H'3\|apply LtR0Fnum with radix];auto with real zarith.
401		2: cut ((Fnum zH) < 2)%Z;[intros H'4\|idtac];auto with real zarith.
	398	cut (Zabs (Fnum zH)=1)%Z;[intros H6\|idtac].
	399	2: cut (0 < (Zabs (Fnum zH)))%Z;[intros H'3\|
	400	apply Zlt_le_trans with (Fnum (Fabs zH)); auto with zarith;
	401	apply LtR0Fnum with radix];auto with real zarith.
	402	2: cut (Zabs (Fnum zH) < 2)%Z;[intros H'4\|idtac];auto with real zarith.
402	403	2:apply Zlt_Rlt; apply Rlt_le_trans with (1:=H4);auto with real zarith.
403		cut ((((powerRZ radix (Zpred (-N))) <= xalpha)%R) /\ ((xalpha <=3*(powerRZ radix (Zpred (-N))))%R)).
	404	2: rewrite Fabs_correct; auto with real zarith.
	405	cut ((((powerRZ radix (Zpred (-N))) <= (Rabs x)alpha)%R) /\ (((Rabs x)alpha <=3*(powerRZ radix (Zpred (-N))))%R)).
404	406	intros T;elim T; intros W1 W2;clear T.
405		case (Rle_or_lt (/2%nat*(Float (Fnum gamma) ((Fexp gamma)-N)%Z)) x);intros H7.
406		assert (Fbounded b (Fminus 2 x (Float (Fnum gamma) ((Fexp gamma)-N)%Z)) /\
407		(Rabs (x - (Float (Fnum gamma) ((Fexp gamma)-N)%Z))
408		<= (Float (Fnum gamma) ((Fexp gamma)-N)%Z))%R).
409		apply Sterbenzbis; auto with zarith.
	407	case (Rle_or_lt (/2%nat*(Rabs (Fmult zH gamma))) (Rabs x));intros H7.
	408	assert (Fbounded b (Fminus 2 x (Fmult zH gamma)) /\
	409	(Rabs (x - (Fmult zH gamma))
	410	<= Rabs (Fmult zH gamma))%R).
	411	unfold FtoRradix; apply Sterbenzter; auto with zarith.
410	412	split; simpl in \|- *;auto with zarith.
	413	rewrite Zabs_Zmult; rewrite H6.
	414	apply Zle_lt_trans with (Zabs (Fnum gamma)); auto with zarith.
411	415	apply Zlt_trans with (Zpos (vNum bmoinsq)).
412	416	elim gammaNormal;intros W;elim W;auto.
413	417	rewrite pGivesBound;unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq;auto with zarith.

433	437	replace (2-prec)%Z with (2%nat-prec)%Z;auto with zarith.
434	438	apply delta_inf with b;auto with zarith.
435	439	apply exp_alpha_le.
436		right; unfold FtoRradix, FtoR;simpl.
437		unfold Zminus; rewrite powerRZ_add; auto with real zarith.
438		replace (powerRZ 2 (- N))%R with (2*(powerRZ 2 (Zpred (- N))))%R;[ring\|idtac].
439		pattern (-N)%Z at 2; replace (-N)%Z with (1+(Zpred (-N)))%Z;
440		[rewrite powerRZ_add;auto with real zarith;simpl;ring\|unfold Zpred;ring].
	440	rewrite Fmult_correct; auto with zarith; rewrite Rabs_mult.
	441	replace (Rabs (FtoR 2 zH) ) with (powerRZ radix (-N)).
	442	rewrite Rabs_right.
	443	unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith.
	444	fold radix; fold FtoRradix; simpl; right; field; auto with real.
	445	apply Rle_ge; auto with real.
	446	rewrite <- Fabs_correct; auto with zarith;unfold FtoR, Fabs; simpl.
	447	rewrite H6; rewrite H3; simpl; ring.
	448	rewrite Fmult_correct; auto with zarith; fold radix; fold FtoRradix.
	449	cut (0 <= x*zH)%R.
	450	intros; rewrite <- Rmult_assoc; apply Rle_trans with (0*gamma)%R; auto with real.
	451	case (Rle_or_lt 0 x); intros.
	452	assert (0 <= zH)%R.
	453	rewrite <- H2; apply zH1Pos with b prec N alpha x u; auto with zarith.
	454	apply Rle_trans with (0*zH)%R; auto with real.
	455	assert (zH <= 0)%R.
	456	rewrite <- H2; apply zH1Neg with b prec N alpha x u; auto with zarith real.
	457	apply Rle_trans with ((-x)*(-zH))%R; auto with real.
	458	apply Rmult_le_pos; auto with real.
441	459	elim H; intros; split.
442		exists (Fminus radix x (Float (Fnum gamma) ((Fexp gamma)-N)%Z));split; auto.
	460	exists (Fminus radix x (Fmult zH gamma));split; auto.
443	461	rewrite H2; unfold FtoRradix in \|- *; rewrite Fminus_correct; auto with zarith.
444		unfold FtoR; simpl; rewrite H6; rewrite H3; unfold Zminus;rewrite powerRZ_add; auto with real zarith;simpl; ring.
445		replace (zH1 * gamma)%R with (FtoRradix (Float (Fnum gamma) (Fexp gamma - N))).
	462	rewrite Fmult_correct; auto with zarith real.
	463	replace (zH1 * gamma)%R with (FtoRradix (Fmult zH gamma)).
446	464	apply Rle_lt_trans with (1:=H8).
447		unfold FtoRradix, FtoR; simpl.
448		replace (prec-N+Fexp gamma)%Z with (prec+(Fexp gamma-N))%Z;
	465	unfold FtoRradix; rewrite Fmult_correct; auto with zarith.
	466	rewrite Rabs_mult.
	467	replace (prec-N+Fexp gamma)%Z with (-N+(prec+Fexp gamma))%Z;
449	468	[rewrite powerRZ_add; auto with real zarith\|ring].
	469	replace (Rabs (FtoR radix zH)) with (powerRZ radix (- N)).
	470	apply Rmult_lt_compat_l; auto with real zarith.
	471	rewrite <- Fabs_correct; auto with zarith; unfold FtoR, Fabs; simpl.
	472	rewrite powerRZ_add; auto with real zarith.
450	473	apply Rmult_lt_compat_r; auto with real zarith.
451	474	elim gammaNormal; intros T1 T2; elim T1; intros.
452		apply Rlt_le_trans with (Zpos (vNum bmoinsq)).
453		apply Rle_lt_trans with (Rabs (Fnum gamma));[apply RRle_abs\|
454		rewrite Rabs_Zabs; auto with real zarith].
	475	apply Rlt_le_trans with (Zpos (vNum bmoinsq)); auto with real zarith.
455	476	unfold bmoinsq; rewrite vNum_eq_Zpower_bmoinsq;
456	477	rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
457		rewrite H2; unfold FtoRradix, FtoR; simpl.
458		rewrite H3; rewrite H6; unfold Zminus; rewrite powerRZ_add; auto with real zarith.
459		simpl; ring.
	478	rewrite <- Fabs_correct; auto with zarith; unfold FtoR, Fabs; simpl.
	479	rewrite H3; rewrite H6; simpl; ring.
	480	rewrite H2; unfold FtoRradix; rewrite Fmult_correct; auto with real zarith.
460	481	generalize gamma_p; intros T1; elim T1; intros gam2 T2;elim T2; intros W3 T3;elim T3; intros W4 T4;
461	482	elim T4; intros W5 T5; elim T5; intros W6 W7; clear T1 T2 T3 T4 T5.
462	483	rewrite H2; rewrite <- W3.
463	484	cut (0 < (1 + powerRZ radix (2 - prec)))%R;[intros W8\|idtac].
464	485	2: apply Rlt_trans with 1%R; auto with real zarith.
465	486	2: apply Rle_lt_trans with (1+0)%R; auto with real zarith.
466		cut ((powerRZ radix (Zpred (-N)))*gamma/(1+(powerRZ radix (Zminus 2 prec))) <= x)%R;[intros H9\|idtac].
	487	cut ((powerRZ radix (Zpred (-N)))*gamma/(1+(powerRZ radix (Zminus 2 prec))) <= Rabs x)%R;[intros H9\|idtac].
467	488	cut ((Fexp x)=(Fexp gam2)-N-1)%Z;[intros H8\|idtac].
468	489	assert (Rabs (x - zH * gam2) < powerRZ radix (Fexp gam2 - N - 1) * Zpos (vNum b))%R.
469		rewrite Rabs_left1; ring_simplify (- (x - zH * gam2))%R.
470		apply Rle_lt_trans with (- (powerRZ radix (Zpred (- N)) * gamma / (1 + powerRZ radix (2 - prec)))+zH*gam2)%R;auto with real.
	490	apply Rle_lt_trans with (- Rabs x+Rabs zH*gam2)%R.
	491	assert (forall (r1 r2:R), ((0 <= r1)%R -> (0 <= r2)%R)
	492	-> ((r1<=0)%R -> (r2 <= 0)%R) -> (Rabs r1 <= Rabs r2)%R
	493	-> (Rabs (r1-r2) = - Rabs r1 + Rabs r2)%R).
	494	intros r1 r2 L1 L2; case (Rle_or_lt 0 r1); intros L3.
	495	rewrite (Rabs_right r1); try apply Rle_ge; auto with real.
	496	rewrite (Rabs_right r2); try apply Rle_ge; auto with real.
	497	intros; rewrite Rabs_left1; auto with real.
	498	ring.
	499	apply Rplus_le_reg_l with r2; ring_simplify; auto with real.
	500	rewrite (Rabs_left1 r1); try apply Rle_ge; auto with real.
	501	rewrite (Rabs_left1 r2); try apply Rle_ge; auto with real.
	502	intros; rewrite Rabs_right; auto with real.
	503	ring.
	504	apply Rle_ge; apply Rplus_le_reg_l with (-r1)%R; ring_simplify; auto with real.
	505	rewrite H; auto.
	506	rewrite Rabs_mult; rewrite (Rabs_right gam2); auto with real.
	507	apply Rle_ge; rewrite W3; auto with real.
	508	intros; assert (0 <= zH)%R.
	509	rewrite <- H2; apply zH1Pos with b prec N alpha x u; auto with zarith.
	510	apply Rmult_le_pos; auto with real.
	511	rewrite W3; auto with real.
	512	intros; assert (zH <= 0)%R.
	513	rewrite <- H2; apply zH1Neg with b prec N alpha x u; auto with zarith.
	514	assert (0 < gam2)%R;[rewrite W3\|idtac]; auto with real.
	515	apply Rle_trans with (0*gam2)%R; auto with real.
	516	apply Rlt_le; apply Rlt_le_trans with (1:=H7).
	517	apply Rle_trans with (1*Rabs (Fmult zH gamma))%R.
	518	apply Rmult_le_compat_r; auto with real zarith.
	519	simpl; apply Rmult_le_reg_l with 2%R; auto with real;apply Rle_trans with 1%R;[right;field\|idtac];auto with real.
	520	rewrite W3; unfold FtoRradix; rewrite Fmult_correct; auto with zarith real.
	521	apply Rle_lt_trans with (- (powerRZ radix (Zpred (- N)) * gamma / (1 + powerRZ radix (2 - prec)))+Rabs zH*gam2)%R;auto with real.
471	522	rewrite <- W3; apply Rmult_lt_reg_l with (1 + powerRZ radix (2 - prec))%R; auto with real zarith.
472		apply Rle_lt_trans with ((1 + powerRZ radix (2 - prec)) * gam2 * zH
	523	apply Rle_lt_trans with ((1 + powerRZ radix (2 - prec)) * gam2 * Rabs zH
473	524	- (powerRZ radix (Zpred (- N)) * gam2))%R.
474	525	right; field; auto with real zarith.
475	526	rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.
476		replace (FtoRradix zH) with (powerRZ radix (-N))%R;[idtac\|unfold FtoRradix, FtoR;rewrite H6; rewrite H3;simpl; ring].
	527	replace (Rabs zH) with (powerRZ radix (-N))%R.
477	528	apply Rle_lt_trans with (gam2(powerRZ radix (-N-1))(1+(powerRZ radix (3-prec))))%R;[right\|idtac].
478	529	pattern (-N)%Z at 1; replace (-N)%Z with (1+(-N-1))%Z; [rewrite powerRZ_add; auto with real zarith\|ring].
479	530	replace (2%nat-prec)%Z with (2-prec)%Z;auto with zarith.

502	553	apply Ropp_lt_contravar;auto with real zarith.
503	554	right;ring_simplify; rewrite <- powerRZ_add; auto with real zarith.
504	555	ring_simplify (prec+(2-prec))%Z;simpl;ring.
505		apply Rplus_le_reg_l with (zH*gam2)%R.
506		ring_simplify.
507		apply Rlt_le; apply Rlt_le_trans with (1:=H7).
508		apply Rle_trans with (1*(Float (Fnum gamma) (Fexp gamma - N)))%R.
509		apply Rmult_le_compat_r; [unfold FtoRradix, FtoR; simpl;auto with real zarith\|idtac].
510		apply Rlt_le; apply Rmult_lt_0_compat; auto with real zarith.
511		assert (0 < (Fnum gamma))%Z;[apply LtR0Fnum with radix\|idtac];auto with real zarith.
512		simpl; apply Rmult_le_reg_l with 2%R; auto with real;apply Rle_trans with 1%R;[right;field\|idtac];auto with real.
513		rewrite W3; unfold FtoRradix, FtoR; rewrite H3 ; rewrite H6;simpl.
514		unfold Zminus; rewrite powerRZ_add; auto with real zarith; right; ring.
	556	unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
	557	unfold FtoR, Fabs; simpl; rewrite H3; rewrite H6; simpl; ring.
515	558	split.
516	559	exists (Fminus radix x (Fmult zH gam2));split.
517	560	unfold FtoRradix; rewrite Fminus_correct;auto with zarith; rewrite Fmult_correct;auto with real zarith.

540	583	apply Rle_trans with (FtoR radix(Float 1%nat (Fexp (Float (Fnum gam2) (Fexp gam2-N-1)))))%R;[idtac\|right; unfold FtoR;simpl;ring].
541	584	cut (Fcanonic radix b (Float (Fnum gam2) (Fexp gam2-N-1)));[intros W'\|idtac].
542	585	rewrite <- CanonicFulp with b radix prec (Float (Fnum gam2) (Fexp gam2-N-1)); auto with zarith.
	586	rewrite FulpFabs; auto with zarith.
543	587	apply LeFulpPos; auto with real float zarith.
544	588	apply FcanonicBound with radix;auto.
	589	rewrite Fabs_correct; auto with zarith real.
	590	rewrite Fabs_correct; auto with zarith.
545	591	fold FtoRradix; apply Rlt_le; apply Rlt_le_trans with (1:=H7).
546		simpl; right; unfold FtoRradix, FtoR;simpl; unfold Zminus;repeat rewrite powerRZ_add;auto with real zarith.
547		apply trans_eq with (((Fnum gam2 * (powerRZ 2 (Fexp gam2))))( powerRZ 2 (- N) powerRZ 2 (- (1))))%R;[idtac\|ring].
548		replace ((Fnum gam2 * (powerRZ 2 (Fexp gam2))))%R with ((Fnum gamma * (powerRZ 2 (Fexp gamma))))%R.
	592	unfold FtoRradix; rewrite Fmult_correct; auto with zarith.
	593	fold FtoRradix; rewrite <- W3; rewrite Rabs_mult.
	594	rewrite (Rabs_right gam2);[idtac\|apply Rle_ge; rewrite W3; auto with real].
	595	unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
	596	right; unfold FtoRradix, FtoR;simpl; unfold Zminus;repeat rewrite powerRZ_add;auto with real zarith.
	597	rewrite H3; rewrite H6.
549	598	simpl; field;auto with real.
550	599	elim W4; intros T3 T2; elim T3; intros T4 T5.
551	600	left;split;simpl; auto with zarith.

559	608	apply Rle_trans with (FtoR radix(Float 1%nat (Fexp (Float ((Fnum gam2)-4) (Fexp gam2-N-1)))))%R;[right; unfold FtoR;simpl;ring\|idtac].
560	609	cut (0 < FtoR radix (Float ((Fnum gam2)-4) (Fexp gam2 - N - 1)))%R; [intros W''\|idtac].
561	610	rewrite <- CanonicFulp with b radix prec (Float ((Fnum gam2)-4) (Fexp gam2-N-1)); auto with zarith.
	611	rewrite FulpFabs with b radix prec x; auto with zarith.
562	612	apply LeFulpPos; auto with real float zarith.
563	613	apply FcanonicBound with radix;auto.
	614	rewrite Fabs_correct; auto with zarith.
564	615	fold FtoRradix; apply Rle_trans with (2:=H9).
565	616	fold FtoRradix; rewrite <- W3.
566	617	apply Rle_trans with (powerRZ radix (Zpred (- N))(((Fnum gam2)-4)(powerRZ radix (Fexp gam2))))%R.

612	663	field; auto with real.
613	664	apply Rmult_le_reg_l with (1 + powerRZ radix (2 - prec))%R;auto with real.
614	665	apply Rle_trans with ((powerRZ radix (Zpred (- N)) * gamma))%R;[right;field;auto with real\|idtac].
615		apply Rle_trans with ((xalpha)gamma)%R;auto with real.
616		apply Rle_trans with ((alphagamma)x)%R;[right;ring\|apply Rmult_le_compat_r;auto with real].
	666	apply Rle_trans with ((Rabs xalpha)gamma)%R;auto with real.
	667	apply Rle_trans with ((alphagamma)Rabs x)%R;[right;ring\|apply Rmult_le_compat_r;auto with real].
617	668	apply Rplus_le_reg_l with (-1)%R.
618	669	apply Rle_trans with (Rabs (-1 + alpha * gamma ))%R;[apply RRle_abs\|idtac].
619	670	rewrite <- Rabs_Ropp.

622	673	replace (2-prec)%Z with (2%nat-prec)%Z;auto with zarith.
623	674	apply delta_inf with b;auto with zarith.
624	675	apply exp_alpha_le.
625		cut (Rabs (xalpha-2(powerRZ radix (Zpred (- N)))) <= (powerRZ radix (Zpred (- N))))%R;[intros H7\|idtac].
	676	cut (Rabs (Rabs xalpha-2(powerRZ radix (Zpred (- N)))) <= (powerRZ radix (Zpred (- N))))%R;[intros H7\|idtac].
626	677	split.
627		apply Rplus_le_reg_l with (-x*alpha+(powerRZ radix (Zpred (- N))))%R.
	678	apply Rplus_le_reg_l with (- Rabs x*alpha+(powerRZ radix (Zpred (- N))))%R.
628	679	ring_simplify.
629		apply Rle_trans with (2:=H7); rewrite <- Rabs_Ropp.
630		apply Rle_trans with (- (x * alpha - 2 * powerRZ radix (Zpred (- N))))%R;
	680	apply Rle_trans with (2:=H7).
	681	rewrite <- (Rabs_Ropp (Rabs x * alpha - 2 * powerRZ radix (Zpred (- N)))).
	682	apply Rle_trans with (- (Rabs x * alpha - 2 * powerRZ radix (Zpred (- N))))%R;
631	683	[right;ring\|apply RRle_abs].
632	684	apply Rplus_le_reg_l with (-2*(powerRZ radix (Zpred (-N))))%R.
633	685	ring_simplify (-2 * powerRZ radix (Zpred (- N)) + 3 * powerRZ radix (Zpred (- N)))%R.
634	686	apply Rle_trans with (2:=H7).
635		apply Rle_trans with (x * alpha - 2 * powerRZ radix (Zpred (- N)))%R;
	687	apply Rle_trans with (Rabs x * alpha - 2 * powerRZ radix (Zpred (- N)))%R;
636	688	[right;ring\|apply RRle_abs].
637		replace (2 * powerRZ radix (Zpred (- N)))%R with (FtoRradix zH).
638		2: unfold FtoRradix, FtoR; rewrite H3; rewrite H6.
	689	replace (2 * powerRZ radix (Zpred (- N)))%R with (Rabs zH).
	690	2: unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
	691	2: unfold Fabs, FtoR; simpl; rewrite H3; rewrite H6.
639	692	2: simpl; unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith;simpl.
640	693	2: field; auto with real.
	694	assert (forall (r1 r2 C:R), ((0 <= r1)%R -> (0 <= r2)%R)
	695	-> ((r1<=0)%R -> (r2 <= 0)%R)
	696	-> (Rabs (Rabs r1C- Rabs r2) = Rabs (r1C- r2))%R).
	697	intros r1 r2 C L1 L2; case (Rle_or_lt 0 r1); intros L3.
	698	rewrite (Rabs_right r1); try apply Rle_ge; auto with real.
	699	rewrite (Rabs_right r2); try apply Rle_ge; auto with real.
	700	rewrite (Rabs_left1 r1); try apply Rle_ge; auto with real.
	701	rewrite (Rabs_left1 r2); try apply Rle_ge; auto with real.
	702	replace (-r1C-(-r2))%R with (-(r1C-r2))%R;
	703	[apply Rabs_Ropp\| ring].
	704	rewrite H.
	705	2: intros; rewrite <- H2; apply zH1Pos with b prec N alpha x u; auto with zarith.
	706	2: intros; rewrite <- H2; apply zH1Neg with b prec N alpha x u; auto with zarith.
641	707	rewrite <- H2; unfold FtoRradix, radix.
642	708	rewrite zH1_eq with b prec N alpha x u zH1; auto with zarith.
643	709	fold radix; fold FtoRradix.

652	718	field; auto with real.
653	719	Qed.
654	720	End Total.
655
656

+136

-103

FnElem/FArgReduct4.v less more

41	41	Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.
42	42	Hypothesis Fboundedx : Fbounded b x.
43	43	Hypothesis xCanonic : Fcanonic radix b x.
44		Hypothesis xPos : (0 <= x)%R.
45	44
46	45
47	46

73	72	(** x not too big *)
74	73	Hypothesis
75	74	xalpha_small :
76		(x * alpha <=
	75	(Rabs (x * alpha) <=
77	76	powerRZ radix (Zpred (Zpred (prec - N))) - powerRZ radix (- N))%R.
78	77
79	78	(** No underflow *)

138	137
139	138
140	139	Theorem Fexp_x_aprox_zh_gamma:
141		(0 < zH1)%R ->
	140	(0 <> zH1)%R ->
142	141	(exists k:Z,
143		(powerRZ radix k <= zH1 < powerRZ radix (k+1))%R /\
	142	(powerRZ radix k <= Rabs zH1 < powerRZ radix (k+1))%R /\
144	143	(Fexp gamma+k-3 <= Fexp x)%Z /\ (-N <= k <= prec-3-N)%Z
145		/\ ((Fexp gamma-N-2 <= Fexp x)%Z \/ (FtoRradix zH1=powerRZ radix (-N))%R)).
	144	/\ ((Fexp gamma-N-2 <= Fexp x)%Z \/ (Rabs zH1=powerRZ radix (-N))%R)).
146	145	intros P.
147		case (Rle_or_lt (powerRZ (Zpos 2) (2 - Zsucc N)) zH1); intros M.
	146	case (Rle_or_lt (powerRZ (Zpos 2) (2 - Zsucc N)) (Rabs zH1)); intros M.
148	147	elim (arg_reduct_exists_k_zH b prec N alpha x u zH1); auto with zarith.
149		intros k (zH, (L1,(L2,(L3,(L4,(L5,(L6,(L7,(L8,(L9,L10)))))))))).
	148	intros k (zH, (L2,(L3,(L4,(L5,(L6,(L7,(L8,(L9,L10))))))))).
150	149	exists k.
151	150	split; auto with real zarith.
152	151	assert (Fexp gamma + k - 3 <= Fexp x)%Z.
153	152	assert (k-1+Fexp gamma+(prec-3) < Fexp x+prec)%Z; auto with zarith.
	153	apply Zlt_le_trans with (Fexp (Fabs x) + prec)%Z; auto with zarith.
154	154	apply Zlt_powerRZ with radix; auto with real zarith.
155		apply Rle_lt_trans with x.
156		2: unfold FtoRradix, FtoR; simpl; rewrite powerRZ_add; auto with real zarith.
	155	apply Rle_lt_trans with (Rabs x).
	156	2: unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
	157	2: unfold Fabs, FtoR; simpl; rewrite powerRZ_add; auto with real zarith.
157	158	2: rewrite Rmult_comm; apply Rmult_lt_compat_l; auto with real zarith.
158	159	2: elim Fboundedx; intros.
159		2: apply Rle_lt_trans with (IZR (Zabs (Fnum x))); auto with zarith real.
160	160	2: replace (powerRZ 2 prec) with (IZR ( Zpos (vNum b))); auto with zarith real.
161	161	2: rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real.
162	162	apply Rle_trans with (gamma*powerRZ radix (k-1))%R.

216	216	replace (2 + - (prec - S 1))%Z with (4-prec)%Z; auto with zarith.
217	217	replace (Z_of_nat (S 1)) with 2%Z; auto with zarith.
218	218	repeat apply prod_neq_R0; auto with real.
219		apply Rle_trans with (zH-/4*zH)%R.
	219	apply Rle_trans with (Rabs zH-/4*Rabs zH)%R.
220	220	apply Rle_trans with (3/4* powerRZ radix k)%R.
221	221	unfold Zminus; rewrite powerRZ_add; auto with real zarith.
222	222	simpl; right;field; auto with real.
223		repeat apply prod_neq_R0; auto with real zarith.
224		apply Rle_trans with (3/4* zH)%R.
	223	apply Rle_trans with (3/4* Rabs zH)%R.
225	224	apply Rmult_le_compat_l; auto with real.
226	225	left; unfold Rdiv; apply Rmult_lt_0_compat; auto with real.
227	226	assert (0 < 4)%R; try apply Rmult_lt_0_compat; auto with real.
228	227	unfold FtoRradix, radix; rewrite <- L2; auto with real.
229	228	right; field; auto with real.
230		apply Rplus_le_reg_l with (-alphax+/4zH)%R.
231		apply Rle_trans with (-(x*alpha-zH))%R;[right; ring\|idtac].
232		apply Rle_trans with (Rabs (-(x*alpha-zH)));[apply RRle_abs\|rewrite Rabs_Ropp].
	229	apply Rplus_le_reg_l with (-alphaRabs x+/4Rabs zH)%R.
	230	apply Rle_trans with (-(Rabs x*alpha-Rabs zH))%R;[right; ring\|idtac].
	231	apply Rle_trans with (Rabs (-(Rabs x*alpha-Rabs zH)));[apply RRle_abs\|rewrite Rabs_Ropp].
	232	assert (forall (r1 r2 C:R), ((0 <= r1)%R -> (0 <= r2)%R)
	233	-> ((r1<=0)%R -> (r2 <= 0)%R)
	234	-> (Rabs (Rabs r1C-Rabs r2) = Rabs (r1C- r2))%R).
	235	intros r1 r2 C G1 G2; case (Rle_or_lt 0 r1); intros G3.
	236	rewrite (Rabs_right r1); try apply Rle_ge; auto with real.
	237	rewrite (Rabs_right r2); try apply Rle_ge; auto with real.
	238	rewrite (Rabs_left1 r1); try apply Rle_ge; auto with real.
	239	rewrite (Rabs_left1 r2); try apply Rle_ge; auto with real.
	240	replace (-r1C-(-r2))%R with (-(r1C-r2))%R;
	241	[apply Rabs_Ropp\| ring].
	242	rewrite H1.
	243	2: intros; unfold FtoRradix, radix; rewrite <- L2;
	244	apply zH1Pos with b prec N alpha x u; auto with zarith.
	245	2: intros; unfold FtoRradix, radix; rewrite <- L2;
	246	apply zH1Neg with b prec N alpha x u; auto with zarith.
233	247	apply Rle_trans with (powerRZ (Zpos 2) (Zpred (- N))); auto with real.
234		apply Rle_trans with (/4*zH)%R;[idtac\|right; ring].
	248	apply Rle_trans with (/4*Rabs zH)%R;[idtac\|right; ring].
235	249	apply Rle_trans with (/4*powerRZ radix (2 - Zsucc N))%R;[idtac\|
236	250	apply Rmult_le_compat_l; auto with real].
237	251	2: assert (0 < 4)%R; auto with real.

257	271	assert (2 - Zsucc N < Zsucc k)%Z; [idtac\|unfold Zsucc; auto with zarith].
258	272	apply Zlt_powerRZ with (Zpos 2); auto with real zarith.
259	273	apply Rle_lt_trans with (1:=M); auto with real.
260		assert (FtoRradix zH1=powerRZ radix (-N))%R.
	274	assert (Rabs zH1=powerRZ radix (-N))%R.
261	275	cut (zH1 = Float
262	276	(Fnum (Fnormalize radix b prec u) -
263	277	3%nat * Zpower_nat radix (pred (pred prec))) (

281	295	cut
282	296	(exists zH : float,
283	297	FtoRradix zH1 = zH /\
284		Fexp zH = (- N)%Z /\ (Fnum zH < powerRZ radix (Zpred 2))%R /\ (0 < zH)%R).
	298	Fexp zH = (- N)%Z /\ (Zabs (Fnum zH) < powerRZ radix (Zpred 2))%R /\ (0 < Rabs zH)%R).
285	299	2:exists
286	300	(Float
287	301	(Fnum (Fnormalize radix b prec u) -

291	305	2:split; [ simpl in \|- *; auto \| idtac ].
292	306	2:split.
293	307	2:apply Rmult_lt_reg_l with (powerRZ radix (- N)); auto with real zarith.
294		2:apply Rle_lt_trans with (FtoRradix zH1);
295		[ right; rewrite H'1; unfold FtoRradix, FtoR in \|- *; simpl; ring \| idtac ].
	308	2:apply Rle_lt_trans with (Rabs zH1);
	309	[ right; rewrite H'1; unfold FtoRradix, FtoR; simpl \| idtac].
	310	2: rewrite Rabs_mult; rewrite Rabs_Zabs; rewrite Rabs_right; auto with real.
	311	2: apply Rle_ge; auto with real zarith.
296	312	2:rewrite <- powerRZ_add; auto with real zarith.
297	313	2:replace (- N + Zpred 2)%Z with (2 - Zsucc N)%Z; auto;
298	314	unfold Zsucc, Zpred in \|- *; ring.
299		2:rewrite <- H'1; cut (0 <= zH1)%R; auto with real.
	315	2:rewrite <- H'1; cut (0 <= Rabs zH1)%R; auto with real.
	316	2: intros L; case L; auto with real.
	317	2: intros; absurd (Rabs zH1=0)%R; auto with real;
	318	apply Rabs_no_R0; auto with real.
300	319	intros V; elim V; intros zH V1; elim V1; intros H2 V2; elim V2; intros H3 V3;
301	320	elim V3; intros H4 H5; clear V V1 V2 V3.
302		cut ((Fnum zH)=1)%Z;[intros H6\|idtac].
303		2: cut (0 < (Fnum zH))%Z;[intros H'3\|apply LtR0Fnum with radix];auto with real zarith.
304		2: cut ((Fnum zH) < 2)%Z;[intros H'4\|idtac];auto with real zarith.
	321	cut (Zabs (Fnum zH)=1)%Z;[intros H6\|idtac].
	322	2: cut (0 < Zabs (Fnum zH))%Z;[intros H'3\|
	323	apply Zlt_le_trans with (Fnum (Fabs zH)); auto with zarith;
	324	apply LtR0Fnum with radix];auto with real zarith.
	325	2: cut (Zabs (Fnum zH) < 2)%Z;[intros H'4\|idtac];auto with real zarith.
305	326	2:apply Zlt_Rlt; apply Rlt_le_trans with (1:=H4);auto with real zarith.
306		rewrite H2; unfold FtoRradix, FtoR; rewrite H6; rewrite H3; simpl; ring.
	327	rewrite H2; unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
	328	unfold Fabs, FtoR; rewrite H6; rewrite H3; simpl; ring.
	329	rewrite Fabs_correct; auto with real zarith.
307	330	exists (-N)%Z.
308	331	split.
309	332	rewrite H;split;auto with real zarith.
310	333	split;[idtac\|auto with zarith].
311		cut ((((powerRZ radix (Zpred (-N))) <= xalpha)%R) /\ ((xalpha <=3*(powerRZ radix (Zpred (-N))))%R)).
	334	cut ((((powerRZ radix (Zpred (-N))) <= Rabs xalpha)%R) /\ ((Rabs xalpha <=3*(powerRZ radix (Zpred (-N))))%R)).
312	335	intros T;elim T; intros W1 W2;clear T.
313	336	elim (gamma_p b prec N gamma); auto with zarith.
314	337	fold radix; fold FtoRradix.

317	340	cut (0 < (1 + powerRZ radix (2 - prec)))%R;[intros W8\|idtac].
318	341	2: apply Rlt_trans with 1%R; auto with real zarith.
319	342	2: apply Rle_lt_trans with (1+0)%R; auto with real zarith.
320		cut ((powerRZ radix (Zpred (-N)))*gamma/(1+(powerRZ radix (Zminus 2 prec))) <= x)%R;[intros H9\|idtac].
	343	cut ((powerRZ radix (Zpred (-N)))*gamma/(1+(powerRZ radix (Zminus 2 prec))) <= Rabs x)%R;[intros H9\|idtac].
321	344	cut ((Fexp gam2 - N - 1) <= Fexp x)%Z.
322	345	rewrite W5; unfold Zpred; auto with zarith.
323	346	apply Zle_powerRZ with radix; auto with zarith real.

327	350	apply Rle_trans with (FtoR radix(Float 1%nat (Fexp (Float ((Fnum gam2)-4) (Fexp gam2-N-1)))))%R;[right; unfold FtoR;simpl;ring\|idtac].
328	351	cut (0 < FtoR radix (Float ((Fnum gam2)-4) (Fexp gam2 - N - 1)))%R; [intros W''\|idtac].
329	352	rewrite <- CanonicFulp with b radix prec (Float ((Fnum gam2)-4) (Fexp gam2-N-1)); auto with zarith.
	353	rewrite FulpFabs with b radix prec x; auto with zarith.
330	354	apply LeFulpPos; auto with real float zarith.
331	355	apply FcanonicBound with radix;auto.
	356	rewrite Fabs_correct; auto with zarith.
332	357	fold FtoRradix; apply Rle_trans with (2:=H9).
333	358	fold FtoRradix; rewrite <- W3.
334	359	apply Rle_trans with (powerRZ radix (Zpred (- N))(((Fnum gam2)-4)(powerRZ radix (Fexp gam2))))%R.

383	408	field; auto with real.
384	409	apply Rmult_le_reg_l with (1 + powerRZ radix (2 - prec))%R;auto with real.
385	410	apply Rle_trans with ((powerRZ radix (Zpred (- N)) * gamma))%R;[right;field;auto with real\|idtac].
386		apply Rle_trans with ((xalpha)gamma)%R;auto with real.
387		apply Rle_trans with ((alphagamma)x)%R;[right;ring\|apply Rmult_le_compat_r;auto with real].
	411	apply Rle_trans with ((Rabs xalpha)gamma)%R;auto with real.
	412	apply Rle_trans with ((alphagamma)Rabs x)%R;[right;ring\|apply Rmult_le_compat_r;auto with real].
388	413	apply Rplus_le_reg_l with (-1)%R.
389	414	apply Rle_trans with (Rabs (-1 + alpha * gamma ))%R;[apply RRle_abs\|idtac].
390	415	rewrite <- Rabs_Ropp.

395	420	apply exp_alpha_le with N gamma; auto with zarith.
396	421	apply gamma_ge2.
397	422	apply gamma_ge2.
398		cut (Rabs (xalpha-2(powerRZ radix (Zpred (- N)))) <= (powerRZ radix (Zpred (- N))))%R;[intros H7\|idtac].
	423	cut (Rabs (Rabs xalpha-2(powerRZ radix (Zpred (- N)))) <= (powerRZ radix (Zpred (- N))))%R;[intros H7\|idtac].
399	424	split.
400		apply Rplus_le_reg_l with (-x*alpha+(powerRZ radix (Zpred (- N))))%R.
	425	apply Rplus_le_reg_l with (-Rabs x*alpha+(powerRZ radix (Zpred (- N))))%R.
401	426	ring_simplify.
402		apply Rle_trans with (2:=H7); rewrite <- Rabs_Ropp.
403		apply Rle_trans with (- (x * alpha - 2 * powerRZ radix (Zpred (- N))))%R;
	427	apply Rle_trans with (2:=H7).
	428	rewrite <- (Rabs_Ropp (Rabs x * alpha - 2 * powerRZ radix (Zpred (- N)))).
	429	apply Rle_trans with (- (Rabs x * alpha - 2 * powerRZ radix (Zpred (- N))))%R;
404	430	[right;ring\|apply RRle_abs].
405	431	apply Rplus_le_reg_l with (-2*(powerRZ radix (Zpred (-N))))%R.
406	432	ring_simplify (-2 * powerRZ radix (Zpred (- N)) + 3 * powerRZ radix (Zpred (- N)))%R.
407	433	apply Rle_trans with (2:=H7).
408		apply Rle_trans with (x * alpha - 2 * powerRZ radix (Zpred (- N)))%R;
	434	apply Rle_trans with (Rabs x * alpha - 2 * powerRZ radix (Zpred (- N)))%R;
409	435	[right;ring\|apply RRle_abs].
410		replace (2 * powerRZ radix (Zpred (- N)))%R with (FtoRradix zH1).
	436	replace (2 * powerRZ radix (Zpred (- N)))%R with (Rabs zH1).
411	437	2: rewrite H; unfold Zpred, Zminus; rewrite powerRZ_add; auto with real zarith;simpl.
412	438	2: field; auto with real.
413		unfold FtoRradix, radix; rewrite zH1_eq with b prec N alpha x u zH1; auto with zarith.
	439	assert (forall (r1 r2 C:R), ((0 <= r1)%R -> (0 <= r2)%R)
	440	-> ((r1<=0)%R -> (r2 <= 0)%R)
	441	-> (Rabs (Rabs r1C-Rabs r2) = Rabs (r1C- r2))%R).
	442	intros r1 r2 C L1 L2; case (Rle_or_lt 0 r1); intros L3.
	443	rewrite (Rabs_right r1); try apply Rle_ge; auto with real.
	444	rewrite (Rabs_right r2); try apply Rle_ge; auto with real.
	445	rewrite (Rabs_left1 r1); try apply Rle_ge; auto with real.
	446	rewrite (Rabs_left1 r2); try apply Rle_ge; auto with real.
	447	replace (-r1C-(-r2))%R with (-(r1C-r2))%R;
	448	[apply Rabs_Ropp\| ring].
	449	rewrite H0; auto with real.
	450	2: intros; apply zH1Pos with b prec N alpha x u; auto with zarith.
	451	2: intros; apply zH1Neg with b prec N alpha x u; auto with zarith.
	452	unfold FtoRradix, radix.
	453	rewrite zH1_eq with b prec N alpha x u zH1; auto with zarith.
414	454	fold radix; fold FtoRradix.
415	455	replace (x * alpha - (u - 3%nat * powerRZ radix (Zpred (Zpred (prec - N)))))%R with
416	456	(((3%nat * powerRZ radix (Zpred (Zpred (prec - N))))+x*alpha)-u)%R;[idtac\|ring].

425	465
426	466
427	467	Lemma zH_exp_N: exists f:float, (FtoRradix f=zH1)%R /\ Fbounded b f /\ (Fexp f=-N)%Z.
428		case (Rle_or_lt (powerRZ (Zpos 2) (2 - Zsucc N)) zH1); intros M.
	468	case (Rle_or_lt (powerRZ (Zpos 2) (2 - Zsucc N)) (Rabs zH1)); intros M.
429	469	elim (arg_reduct_exists_k_zH b prec N alpha x u zH1); auto with zarith.
430	470	fold radix; fold FtoRradix.
431		intros k (zH, (L1,(L2,(L3,(L4,(L5,(L6,(L7,(L8,(L9,L10)))))))))).
	471	intros k (zH, (L2,(L3,(L4,(L5,(L6,(L7,(L8,(L9,L10))))))))).
432	472	exists zH; split; auto with real; split.
433	473	elim L7; intros T1 T2; elim T1; rewrite vNum_eq_Zpower_bzH; intros T3 T4; clear T1 T2.
434	474	split;[idtac\|simpl in T4; auto].

438	478	apply Zle_lt_trans with (Zpred (Zpred prec)); auto with zarith.
439	479	rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.
440	480	rewrite L6; ring.
441		assert (M':(0 <= zH1)%R).
442		unfold FtoRradix, radix; apply zH1Pos with b prec N alpha x u; auto with zarith.
443		case M'; clear M'; intros M'.
444		assert (FtoRradix zH1=powerRZ radix (-N))%R.
	481	case (Req_dec zH1 0); intros M'.
	482	exists (Float 0 (-N)).
	483	split;[rewrite M'; unfold FtoRradix, FtoR; simpl; ring\|split; auto].
	484	split; simpl; auto with zarith.
	485	assert (Rabs zH1=powerRZ radix (-N))%R.
445	486	cut (zH1 = Float
446	487	(Fnum (Fnormalize radix b prec u) -
447	488	3%nat * Zpower_nat radix (pred (pred prec))) (

465	506	cut
466	507	(exists zH : float,
467	508	FtoRradix zH1 = zH /\
468		Fexp zH = (- N)%Z /\ (Fnum zH < powerRZ radix (Zpred 2))%R /\ (0 < zH)%R).
	509	Fexp zH = (- N)%Z /\ (Zabs (Fnum zH) < powerRZ radix (Zpred 2))%R /\ (0 < Rabs zH)%R).
469	510	2:exists
470	511	(Float
471	512	(Fnum (Fnormalize radix b prec u) -

475	516	2:split; [ simpl in \|- *; auto \| idtac ].
476	517	2:split.
477	518	2:apply Rmult_lt_reg_l with (powerRZ radix (- N)); auto with real zarith.
478		2:apply Rle_lt_trans with (FtoRradix zH1);
479		[ right; rewrite H'1; unfold FtoRradix, FtoR in \|- *; simpl; ring \| idtac ].
	519	2:apply Rle_lt_trans with (Rabs zH1);
	520	[ right; rewrite H'1; unfold FtoRradix, FtoR in \|- *; simpl \| idtac ].
	521	2: rewrite Rabs_mult; rewrite Rabs_Zabs; rewrite Rabs_right;
	522	try apply Rle_ge; auto with real zarith.
480	523	2:rewrite <- powerRZ_add; auto with real zarith.
481	524	2:replace (- N + Zpred 2)%Z with (2 - Zsucc N)%Z; auto;
482	525	unfold Zsucc, Zpred in \|- *; ring.
483	526	2:rewrite <- H'1; auto with real.
484	527	intros V; elim V; intros zH V1; elim V1; intros H2' V2; elim V2; intros H3 V3;
485	528	elim V3; intros H4 H5; clear V V1 V2 V3.
486		cut ((Fnum zH)=1)%Z;[intros H6\|idtac].
487		2: cut (0 < (Fnum zH))%Z;[intros H'3\|apply LtR0Fnum with radix];auto with real zarith.
488		2: cut ((Fnum zH) < 2)%Z;[intros H'4\|idtac];auto with real zarith.
	529	cut (Zabs (Fnum zH)=1)%Z;[intros H6\|idtac].
	530	2: cut (0 < Zabs (Fnum zH))%Z;[intros H'3\|
	531	apply Zlt_le_trans with (Fnum (Fabs zH)); auto with zarith;
	532	apply LtR0Fnum with radix];auto with real zarith.
	533	2: cut (Zabs (Fnum zH) < 2)%Z;[intros H'4\|idtac];auto with real zarith.
489	534	2:apply Zlt_Rlt; apply Rlt_le_trans with (1:=H4);auto with real zarith.
490		rewrite H2'; unfold FtoRradix, FtoR; rewrite H6; rewrite H3; simpl; ring.
491		exists (Float 1 (-N)).
492		split;[rewrite H; unfold FtoRradix, FtoR; simpl; ring\|split; auto].
	535	2: rewrite Fabs_correct; auto with real zarith.
	536	rewrite H2'; unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
	537	unfold Fabs, FtoR; rewrite H6; rewrite H3; simpl; ring.
	538	assert (0 <= Rabs zH1)%R; auto with real.
	539	case H; auto.
	540	intros; absurd (Rabs zH1=0)%R; auto with real; apply Rabs_no_R0; auto.
	541	generalize H; unfold Rabs; case Rcase_abs; intros.
	542	exists (Float (-1) (-N)).
	543	split;[apply trans_eq with (-(-zH1))%R; auto with real;
	544	rewrite H0; unfold FtoRradix, FtoR; simpl; ring\|split; auto].
493	545	split; simpl; auto with zarith.
494	546	apply vNumbMoreThanOne with radix prec; auto with zarith.
495		exists (Float 0 (-N)).
496		split;[rewrite <- M'; unfold FtoRradix, FtoR; simpl; ring\|split; auto].
	547	exists (Float 1 (-N)).
	548	split;[ rewrite H0; unfold FtoRradix, FtoR; simpl; ring\|split; auto].
497	549	split; simpl; auto with zarith.
	550	apply vNumbMoreThanOne with radix prec; auto with zarith.
498	551	Qed.
499	552
500	553

506	559	FtoRradix ff = (x - zH1 * gamma)%R /\ Fbounded b ff /\
507	560	(Fexp (Fnormalize radix b prec v) <= -N + Fexp gamma -2)%Z /\
508	561	(-N + Fexp gamma -3 <= Fexp ff)%Z /\
509		(~(FtoRradix zH1) = powerRZ radix (-N)
	562	(~(Rabs zH1) = powerRZ radix (-N)
510	563	-> (-N + Fexp gamma -2 <= Fexp ff)%Z) /\
511		((FtoRradix zH1) = powerRZ radix (-N)
	564	((Rabs zH1) = powerRZ radix (-N)
512	565	-> (Fexp (Fnormalize radix b prec v) <= Fexp ff)%Z).
513		assert (L:(0 <= zH1)%R).
514		unfold FtoRradix; apply zH1Pos with b prec N alpha x u; auto with zarith.
515		case L; auto; clear L; intros L.
	566	case (Req_dec zH1 0); auto with real; intros L.
516	567	case (Req_dec v 0); auto with real; intros LL;right.
517	568	elim Fexp_x_aprox_zh_gamma; auto.
518	569	intros k (H1,(H2,(K1,K2))).

523	574	apply gamma_ge2.
524	575	elim H;intros T' M; elim T'; intros f T; elim T; intros H3 H4; clear H T T'.
525	576	assert (exists zH:float, FtoRradix zH=zH1 /\ (Fexp zH=-N)%Z /\
526		(zH <= (powerRZ radix prec -1)*powerRZ radix (-N-2))%R).
	577	(Rabs zH <= (powerRZ radix prec -1)*powerRZ radix (-N-2))%R).
527	578	exists (Fminus radix (Fnormalize radix b prec u)
528	579	(Float 3 (Zpred (Zpred (prec - N))))).
529	580	split.

532	583	split;[simpl\|idtac].
533	584	unfold radix; rewrite Fexp_u with b prec N alpha x u; auto with zarith.
534	585	apply Zmin_le1; unfold Zpred; auto with zarith.
535		apply Rle_trans with (FtoRradix zH1).
	586	apply Rle_trans with (Rabs zH1).
536	587	unfold FtoRradix,radix.
537	588	rewrite Fminus_correct; auto with zarith; rewrite FnormalizeCorrect; auto with zarith.
538	589	rewrite zH1_eq with b prec N alpha x u zH1; auto with zarith.
539	590	unfold FtoR; simpl; right; ring.
540		case (Rle_or_lt (powerRZ (Zpos 2) (2 - Zsucc N)) zH1); intros L'.
	591	case (Rle_or_lt (powerRZ (Zpos 2) (2 - Zsucc N)) (Rabs zH1)); intros L'.
541	592	elim arg_reduct_exists_k_zH with b prec N alpha x u zH1; auto with zarith.
542		intros k' (zH', (L1,(L2,(L3,(L4,(L5,(L6,(L7,(L8,(L9,L10)))))))))).
543		apply Rle_trans with (Fnormalize radix b prec zH1).
	593	intros k' (zH',(L2,(L3,(L4,(L5,(L6,(L7,(L8,(L9,L10))))))))).
	594	apply Rle_trans with (Rabs (Fnormalize radix b prec zH1)).
544	595	unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith real.
545	596	apply Rle_trans with (FPred b radix prec (Float (nNormMin radix prec) (k'-prec+2))).
546		unfold FtoRradix; apply FPredProp; auto with zarith.
	597	unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.
	598	apply FPredProp; auto with zarith.
	599	apply FcanonicFabs; auto with zarith.
547	600	apply FnormalizeCanonic; auto with zarith.
548	601	elim zH1Def; auto.
549	602	left; split; try split.

554	607	apply Zle_trans with (k'-prec+2)%Z; auto with zarith.
555	608	apply Zle_trans with (Zabs (radix*(nNormMin radix prec))); auto with zarith.
556	609	rewrite <- PosNormMin with radix b prec; auto with zarith.
	610	rewrite Fabs_correct; auto with zarith.
557	611	rewrite FnormalizeCorrect; auto with zarith.
558	612	apply Rlt_le_trans with (powerRZ radix (Zsucc k')); auto with real.
559	613	unfold FtoR; simpl; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

636	690	apply Rle_trans with (((powerRZ radix prec - 1) * powerRZ radix (- N - 2))
637	691	* (powerRZ radix (Fexp gamma)))%R.
638	692	rewrite Rabs_mult;apply Rmult_le_compat; auto with real zarith.
639		rewrite Rabs_right;[rewrite <- H3';auto with real\|apply Rle_ge; auto with real].
	693	rewrite <- H3';auto with real.
640	694	rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
641	695	fold (pPred (vNum b)); right; unfold FtoRradix, FtoR; simpl.
642	696	replace (- N - 2 + Fexp gamma)%Z with (- N + Fexp gamma - 2)%Z;[idtac\|ring].

654	708	apply Zle_trans with (Fexp gamma -N -3)%Z; auto with zarith.
655	709	apply exp_gamma_enough3 with prec; auto with zarith.
656	710	apply gamma_ge2.
657		case (Req_dec zH1 (powerRZ radix (- N))); intros I1.
	711	case (Req_dec (Rabs zH1) (powerRZ radix (- N))); intros I1.
658	712	split.
659	713	intros I2; Contradict I1; auto with real.
660	714	intros I2; clear I2.

693	747	apply exp_gamma_enough; auto with zarith.
694	748	apply Rle_trans with (powerRZ radix (- N)*(powerRZ radix (Fexp gamma)))%R.
695	749	rewrite Rabs_mult;apply Rmult_le_compat; auto with real zarith.
696		rewrite I1; rewrite Rabs_right; try apply Rle_ge; auto with real zarith.
697	750	right; unfold FtoR; simpl.
698	751	unfold Zminus; rewrite powerRZ_add; auto with real zarith; ring.
699	752	right; unfold FtoRradix, FtoR; simpl; ring.

716	769	case H; auto.
717	770	elim H; intros ff (T1,(T2,(T3,(T4,(T5,T6))))).
718	771	right; exists ff; split; trivial; split; trivial.
719		case (Req_dec zH1 (powerRZ radix (-N))); intros I.
	772	case (Req_dec (Rabs zH1) (powerRZ radix (-N))); intros I.
720	773	apply T6; auto.
721	774	apply Zle_trans with (- N + Fexp gamma - 2)%Z; auto with zarith.
722	775	Qed.
723	776
724		Theorem v_neq_zero: (0 < zH1)%R -> (FtoRradix gamma2<>0)%R -> (FtoRradix v<>0)%R.
	777	Theorem v_neq_zero: (0 <> zH1)%R -> (FtoRradix gamma2<>0)%R -> (FtoRradix v<>0)%R.
725	778	generalize exp_gamma_enough; intros.
726	779	cut (0 < Rabs v)%R.
727	780	intros L; Contradict L.

822	875	intros G; Contradict G; auto with real.
823	876	intros G; Contradict G.
824	877	apply v_neq_zero; auto.
825		case (zH1Pos b prec N alpha x u zH1); auto with zarith;
826		fold radix; fold FtoRradix; intros H0'; Contradict H0'; auto with real.
827	878	intros (f,(H1,(H2,(H3,(H4, H4'))))).
828	879	case (Req_dec t1 res).
829	880	intros T; rewrite T.

837	888	unfold Fopp; simpl; intros t1' (M1,(M2,M3)); fold FtoRradix in M2.
838	889	rewrite Zmin_le2 in M3; auto with zarith.
839	890	2: elim H4'; intros T1 T2.
840		2: case (Req_dec zH1 (powerRZ radix (-N))); intros I; auto with zarith.
	891	2: case (Req_dec (Rabs zH1) (powerRZ radix (-N))); intros I; auto with zarith real.
841	892	2: apply Zle_trans with (- N + Fexp gamma - 2)%Z; auto with zarith.
842	893	elim zH_exp_N; intros zH (N1,(N2,N3)).
843	894	elim plusExpMin with b radix prec (EvenClosest b radix prec)

935	986	fold radix; fold FtoRradix; intros T1 M; clear T1.
936	987	assert (Rabs (zH1*gamma2) <= powerRZ radix (prec+Fexp gamma-N-2))%R.
937	988	elim Fexp_x_aprox_zh_gamma; auto.
938		2: assert (M':(0 <= zH1)%R).
939		2: unfold FtoRradix, radix; apply zH1Pos with b prec N alpha x u; auto with zarith.
940		2:case M'; clear M'; auto with real.
941		2: intros; absurd (0%R = zH1)%R; auto with real.
942	989	intros k ((Q1,Q2),(Q3,Q4)).
943	990	replace (prec + Fexp gamma - N - 2)%Z with (((prec-3-N)+1)+Fexp gamma)%Z;[idtac\|ring].
944	991	rewrite powerRZ_add; auto with real zarith.
945	992	rewrite Rabs_mult; apply Rmult_le_compat; auto with real zarith.
946		rewrite Rabs_right.
947		2: apply Rle_ge; unfold FtoRradix, radix;
948		apply zH1Pos with b prec N alpha x u; auto with zarith.
949	993	apply Rle_trans with (powerRZ radix (k+1)); auto with real zarith.
950	994	apply Rle_powerRZ; auto with real zarith.
951	995	assert (forall (r : R) (g: float),

1069	1113	intros G; Contradict G; auto with real.
1070	1114	intros G; Contradict G.
1071	1115	apply v_neq_zero; auto.
1072		case (zH1Pos b prec N alpha x u zH1); auto with zarith;
1073		fold radix; fold FtoRradix; intros H0'; Contradict H0'; auto with real.
1074	1116	intros (f,(H1,(H2,(H3,(H4,(H4',H4'')))))).
1075	1117	case (Req_dec t1 res).
1076	1118	intros T; rewrite <- T.

1179	1221	fold radix; fold FtoRradix; intros T1 M; clear T1.
1180	1222	assert (Rabs (zH1*gamma2) <= powerRZ radix (prec+Fexp gamma-N-2))%R.
1181	1223	elim Fexp_x_aprox_zh_gamma; auto.
1182		2: assert (M':(0 <= zH1)%R).
1183		2: unfold FtoRradix, radix; apply zH1Pos with b prec N alpha x u; auto with zarith.
1184		2:case M'; clear M'; auto with real.
1185		2: intros; absurd (0%R = zH1)%R; auto with real.
1186	1224	intros k ((Q1,Q2),(Q3,Q4)).
1187	1225	replace (prec + Fexp gamma - N - 2)%Z with (((prec-3-N)+1)+(Fexp gamma))%Z;[idtac\|ring].
1188	1226	rewrite powerRZ_add; auto with real zarith.
1189	1227	rewrite Rabs_mult; apply Rmult_le_compat; auto with real zarith.
1190		rewrite Rabs_right.
1191		2: apply Rle_ge; unfold FtoRradix, radix;
1192		apply zH1Pos with b prec N alpha x u; auto with zarith.
1193	1228	apply Rle_trans with (powerRZ radix (k+1)); auto with real zarith.
1194	1229	apply Rle_powerRZ; auto with real zarith.
1195	1230	assert (forall (r : R) (g: float),

1319	1354	prec (EvenClosest b radix prec); auto with zarith float.
1320	1355	replace (FtoR radix f) with (x - zH1 * gamma - zH1 * gamma2)%R; auto with real.
1321	1356	fold FtoRradix; rewrite H3; rewrite H; ring.
1322		case (zH1Pos b prec N alpha x u zH1); auto with zarith;
1323		fold radix; fold FtoRradix; intros H0.
	1357	case (Req_dec zH1 0); intros.
	1358	exists (Fzero (- dExp b)); split;[idtac\|apply FboundedFzero].
	1359	unfold FtoRradix; rewrite FzeroisReallyZero; fold FtoRradix.
	1360	replace (FtoRradix res) with (FtoRradix x).
	1361	repeat rewrite H0; ring.
	1362	unfold FtoRradix; apply RoundedModeProjectorIdemEq with b
	1363	prec (Closest b radix); auto with zarith.
	1364	apply ClosestRoundedModeP with prec; auto with zarith.
	1365	replace (FtoR radix x) with (x - zH1 * gamma - zH1 * gamma2)%R; auto with real.
	1366	elim resDef; auto.
	1367	fold FtoRradix; repeat rewrite H0; ring.
1324	1368	case FTS_correct.
1325	1369	intros T; case T; intros.
1326	1370	absurd (FtoRradix zH1=0)%R; auto with real.
1327		absurd (FtoRradix v=0)%R; trivial; apply v_neq_zero; trivial.
	1371	absurd (FtoRradix v=0)%R; trivial; apply v_neq_zero; auto with real.
1328	1372	intros T; elim T; intros f (H1,(H2,H3)); clear T.
1329	1373	generalize exp_gamma_enough; intros H4.
1330	1374	elim Fexp_x_aprox_zh_gamma; auto; intros k ((M1,M2),(M3,(M4,M5))).

1360	1404	rewrite Rabs_mult; rewrite Rabs_Ropp; rewrite powerRZ_add; auto with real zarith.
1361	1405	apply Rmult_le_compat; auto with real.
1362	1406	apply Rle_trans with (powerRZ radix (k+1)); auto with real zarith.
1363		rewrite Rabs_right; try apply Rle_ge; auto with real.
1364	1407	apply Rle_powerRZ; auto with real zarith.
1365	1408	replace (prec + 1 - N + Fexp gamma)%Z with ((prec - N + Fexp gamma)+1)%Z;
1366	1409	[idtac\|ring].
1367	1410	apply powerRZSumRle; auto with zarith.
1368		exists (Fzero (- dExp b)); split;[idtac\|apply FboundedFzero].
1369		unfold FtoRradix; rewrite FzeroisReallyZero; fold FtoRradix.
1370		replace (FtoRradix res) with (FtoRradix x).
1371		repeat rewrite <- H0; ring.
1372		unfold FtoRradix; apply RoundedModeProjectorIdemEq with b
1373		prec (Closest b radix); auto with zarith.
1374		apply ClosestRoundedModeP with prec; auto with zarith.
1375		replace (FtoR radix x) with (x - zH1 * gamma - zH1 * gamma2)%R; auto with real.
1376		elim resDef; auto.
1377		fold FtoRradix; repeat rewrite <- H0; ring.
1378	1411	Qed.
1379	1412
1380	1413	End Total.

+79

-158

Makefile less more

0		##############################################################################
1		## The Calculus of Inductive Constructions ##
2		## ##
3		## Projet Coq ##
4		## ##
5		## INRIA ENS-CNRS ##
6		## Rocquencourt Lyon ##
7		## ##
8		## Coq V7 ##
9		## ##
10		## ##
11		##############################################################################
	0	##########################################################################
	1	## v # The Coq Proof Assistant ##
	2	## <O___,, # CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ##
	3	## \VV/ # ##
	4	## // # Makefile automagically generated by coq_makefile V8.2 ##
	5	##########################################################################
12	6
13	7	# WARNING
14	8	#
15		# This Makefile has been automagically generated by coq_makefile
	9	# This Makefile has been automagically generated
16	10	# Edit at your own risks !
17	11	#
18	12	# END OF WARNING
19	13
20	14	#
21	15	# This Makefile was generated by the command line :
22		# coq_makefile AllFloat.v Closest2Plus.v Closest2Prop.v ClosestMult.v ClosestPlus.v ClosestProp.v Closest.v Digit.v Faux.v Fbound.v Fcomp.v Finduct.v Float.v Fmin.v Fnorm.v Fodd.v Fop.v FPred.v Fprop.v FroundMult.v FroundPlus.v FroundProp.v Fround.v FSucc.v MSBProp.v MSB.v Option.v Paux.v Rpow.v sTactic.v Zdivides.v Zenum.v Ct2/FboundI.v Ct2/FnormI.v Expansions/EFast2Sum.v Expansions/Fast2Diff.v Expansions/Fast2Sum.v Expansions/Fexp2.v Expansions/FexpAdd.v Expansions/FexpDiv.v Expansions/FexpPlus.v Expansions/Fexp.v Expansions/ThreeSum2.v Expansions/ThreeSumProps.v Expansions/TwoSum.v FnElem/Axpy.v FnElem/DoubleRound.v FnElem/FArgReduct2.v FnElem/FArgReduct3.v FnElem/FArgReduct4.v FnElem/FArgReduct.v FnElem/FIA64elem.v FnElem/FmaErrApprox.v FnElem/FmaErr.v FnElem/MinOrMax.v Others/DblRndOdd.v Others/Dekker.v Others/discriminant2.v Others/discriminant3.v Others/discriminant.v Others/Divnk.v Others/FmaEmul.v Others/FminOp.v Others/FroundDivSqrt.v Others/IEEE.v Others/PradixE.v Others/RND.v Others/Veltkamp.v
23		#
	16	# coq_makefile AllFloat.v Closest2Plus.v Closest2Prop.v ClosestMult.v ClosestPlus.v ClosestProp.v Closest.v Digit.v Faux.v Fbound.v Fcomp.v Finduct.v Float.v Fmin.v Fnorm.v Fodd.v Fop.v FPred.v Fprop.v FroundMult.v FroundPlus.v FroundProp.v Fround.v FSucc.v MSBProp.v MSB.v Option.v Paux.v RND.v Rpow.v sTactic.v Zdivides.v Zenum.v Ct2/FboundI.v Ct2/FnormI.v Expansions/EFast2Sum.v Expansions/Fast2Diff.v Expansions/Fast2Sum.v Expansions/Fexp2.v Expansions/FexpAdd.v Expansions/FexpDiv.v Expansions/FexpPlus.v Expansions/Fexp.v Expansions/ThreeSum2.v Expansions/ThreeSumProps.v Expansions/TwoSum.v FnElem/Axpy.v FnElem/DoubleRound.v FnElem/FArgReduct2.v FnElem/FArgReduct3.v FnElem/FArgReduct4.v FnElem/FArgReduct.v FnElem/FIA64elem.v FnElem/FmaErrApprox.v FnElem/FmaErr.v FnElem/MinOrMax.v Others/DblRndOdd.v Others/Dekker.v Others/discriminant2.v Others/discriminant3.v Others/discriminant.v Others/Divnk.v Others/FmaEmul.v Others/FminOp.v Others/FroundDivSqrt.v Others/IEEE.v Others/PradixE.v Others/Veltkamp.v
	17	#
	18
	19	#########################
	20	# #
	21	# Libraries definition. #
	22	# #
	23	#########################
	24
	25	CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null \|\| $(CAMLBIN)camlp4 -where)
	26	OCAMLLIBS:=-I $(CAMLP4LIB) -I .
	27	COQLIBS:=-I . -I ./Ct2 -I ./Expansions -I ./FnElem -I ./Others
	28	COQDOCLIBS:=
24	29
25	30	##########################
26	31	# #

28	33	# #
29	34	##########################
30	35
31		CAMLP4LIB=`camlp4 -where`
32		COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
33		-I $(COQTOP)/library -I $(COQTOP)/parsing \
34		-I $(COQTOP)/pretyping -I $(COQTOP)/interp \
35		-I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
36		-I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \
37		-I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \
38		-I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/graphs \
39		-I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \
40		-I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \
41		-I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \
42		-I $(CAMLP4LIB)
43		ZFLAGS=$(OCAMLLIBS) $(COQSRC)
44		OPT=
45		COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
46		COQC=$(COQBIN)coqc
47		GALLINA=gallina
48		COQDOC=coqdoc
49		CAMLC=ocamlc -c
50		CAMLOPTC=ocamlopt -c
51		CAMLLINK=ocamlc
52		CAMLOPTLINK=ocamlopt
53		COQDEP=$(COQBIN)coqdep -c
54		GRAMMARS=grammar.cma
55		CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo
56		PP=-pp "camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl"
57
58		#########################
59		# #
60		# Libraries definition. #
61		# #
62		#########################
63
64		OCAMLLIBS=-I .
65		COQLIBS=-I . -I ./Ct2/ -I ./FnElem/ -I ./Expansions/ -I ./Others/
	36	CAMLP4:=$(notdir $(CAMLP4LIB))
	37	COQSRC:=$(shell $(COQBIN)coqc -where)
	38	COQSRCLIBS:=-I $(COQSRC)
	39	ZFLAGS:=$(OCAMLLIBS) $(COQSRCLIBS)
	40	OPT:=
	41	COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
	42	COQC:=$(COQBIN)coqc
	43	COQDEP:=$(COQBIN)coqdep -c
	44	GALLINA:=$(COQBIN)gallina
	45	COQDOC:=$(COQBIN)coqdoc
	46	CAMLC:=$(CAMLBIN)ocamlc -rectypes -c
	47	CAMLOPTC:=$(CAMLBIN)ocamlopt -rectypes -c
	48	CAMLLINK:=$(CAMLBIN)ocamlc -rectypes
	49	CAMLOPTLINK:=$(CAMLBIN)ocamlopt -rectypes
	50	GRAMMARS:=grammar.cma
	51	CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo
	52	PP:=-pp "$(CAMLBIN)$(CAMLP4)o -I . -I $(COQSRC) $(CAMLP4EXTEND) $(GRAMMARS) -impl"
66	53
67	54	###################################
68	55	# #

70	57	# #
71	58	###################################
72	59
73		VFILES=AllFloat.v\
	60	VFILES:=AllFloat.v\
74	61	Closest2Plus.v\
75	62	Closest2Prop.v\
76	63	ClosestMult.v\

98	85	MSB.v\
99	86	Option.v\
100	87	Paux.v\
	88	RND.v\
101	89	Rpow.v\
102	90	sTactic.v\
103	91	Zdivides.v\

136	124	Others/FroundDivSqrt.v\
137	125	Others/IEEE.v\
138	126	Others/PradixE.v\
139		Others/RND.v\
140	127	Others/Veltkamp.v
141		VOFILES=$(VFILES:.v=.vo)
142		VIFILES=$(VFILES:.v=.vi)
143		GFILES=$(VFILES:.v=.g)
144		HTMLFILES=$(VFILES:.v=.html)
145		GHTMLFILES=$(VFILES:.v=.g.html)
146
147		all: AllFloat.vo\
148		Closest2Plus.vo\
149		Closest2Prop.vo\
150		ClosestMult.vo\
151		ClosestPlus.vo\
152		ClosestProp.vo\
153		Closest.vo\
154		Digit.vo\
155		Faux.vo\
156		Fbound.vo\
157		Fcomp.vo\
158		Finduct.vo\
159		Float.vo\
160		Fmin.vo\
161		Fnorm.vo\
162		Fodd.vo\
163		Fop.vo\
164		FPred.vo\
165		Fprop.vo\
166		FroundMult.vo\
167		FroundPlus.vo\
168		FroundProp.vo\
169		Fround.vo\
170		FSucc.vo\
171		MSBProp.vo\
172		MSB.vo\
173		Option.vo\
174		Paux.vo\
175		Rpow.vo\
176		sTactic.vo\
177		Zdivides.vo\
178		Zenum.vo\
179		Ct2/FboundI.vo\
180		Ct2/FnormI.vo\
181		Expansions/EFast2Sum.vo\
182		Expansions/Fast2Diff.vo\
183		Expansions/Fast2Sum.vo\
184		Expansions/Fexp2.vo\
185		Expansions/FexpAdd.vo\
186		Expansions/FexpDiv.vo\
187		Expansions/FexpPlus.vo\
188		Expansions/Fexp.vo\
189		Expansions/ThreeSum2.vo\
190		Expansions/ThreeSumProps.vo\
191		Expansions/TwoSum.vo\
192		FnElem/Axpy.vo\
193		FnElem/DoubleRound.vo\
194		FnElem/FArgReduct2.vo\
195		FnElem/FArgReduct3.vo\
196		FnElem/FArgReduct4.vo\
197		FnElem/FArgReduct.vo\
198		FnElem/FIA64elem.vo\
199		FnElem/FmaErrApprox.vo\
200		FnElem/FmaErr.vo\
201		FnElem/MinOrMax.vo\
202		Others/DblRndOdd.vo\
203		Others/Dekker.vo\
204		Others/discriminant2.vo\
205		Others/discriminant3.vo\
206		Others/discriminant.vo\
207		Others/Divnk.vo\
208		Others/FmaEmul.vo\
209		Others/FminOp.vo\
210		Others/FroundDivSqrt.vo\
211		Others/IEEE.vo\
212		Others/PradixE.vo\
213		Others/RND.vo\
214		Others/Veltkamp.vo
215
	128	VOFILES:=$(VFILES:.v=.vo)
	129	GLOBFILES:=$(VFILES:.v=.glob)
	130	VIFILES:=$(VFILES:.v=.vi)
	131	GFILES:=$(VFILES:.v=.g)
	132	HTMLFILES:=$(VFILES:.v=.html)
	133	GHTMLFILES:=$(VFILES:.v=.g.html)
	134
	135	all: $(VOFILES)
216	136	spec: $(VIFILES)
217	137
218	138	gallina: $(GFILES)
219	139
220		html: $(HTMLFILES)
221
222		gallinahtml: $(GHTMLFILES)
	140	html: $(GLOBFILES) $(VFILES)
	141	- mkdir html
	142	$(COQDOC) -toc -html $(COQDOCLIBS) -d html $(VFILES)
	143
	144	gallinahtml: $(GLOBFILES) $(VFILES)
	145	- mkdir html
	146	$(COQDOC) -toc -html -g $(COQDOCLIBS) -d html $(VFILES)
223	147
224	148	all.ps: $(VFILES)
225		$(COQDOC) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
	149	$(COQDOC) -toc -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
226	150
227	151	all-gal.ps: $(VFILES)
228		$(COQDOC) -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
	152	$(COQDOC) -toc -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
229	153
230	154
231	155

237	161
238	162	.PHONY: all opt byte archclean clean install depend html
239	163
240		.SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
241
242		.v.vo:
243		$(COQC) $(COQDEBUG) $(COQFLAGS) $*
244
245		.v.vi:
	164	%.vo %.glob: %.v
	165	$(COQC) -dump-glob $.glob $(COQDEBUG) $(COQFLAGS) $
	166
	167	%.vi: %.v
246	168	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
247	169
248		.v.g:
	170	%.g: %.v
249	171	$(GALLINA) $<
250	172
251		.v.tex:
	173	%.tex: %.v
252	174	$(COQDOC) -latex $< -o $@
253	175
254		.v.html:
255		$(COQDOC) -html $< -o $@
256
257		.v.g.tex:
	176	%.html: %.v %.glob
	177	$(COQDOC) -glob-from $*.glob -html $< -o $@
	178
	179	%.g.tex: %.v
258	180	$(COQDOC) -latex -g $< -o $@
259	181
260		.v.g.html:
261		$(COQDOC) -html -g $< -o $@
	182	%.g.html: %.v %.glob
	183	$(COQDOC) -glob-from $*.glob -html -g $< -o $@
	184
	185	%.v.d: %.v
	186	$(COQDEP) -glob -slash $(COQLIBS) "$<" > "$@" \|\| ( RV=$$?; rm -f "$@"; exit $${RV} )
262	187
263	188	byte:
264		$(MAKE) all "OPT=-byte"
	189	$(MAKE) all "OPT:=-byte"
265	190
266	191	opt:
267		$(MAKE) all "OPT=-opt"
268
269		include .depend
270
271		.depend depend:
272		rm -f .depend
273		$(COQDEP) -i $(COQLIBS) $(VFILES) .ml .mli >.depend
274		$(COQDEP) $(COQLIBS) -suffix .html $(VFILES) >>.depend
	192	$(MAKE) all "OPT:=-opt"
275	193
276	194	install:
277	195	mkdir -p `$(COQC) -where`/user-contrib

279	197
280	198	clean:
281	199	rm -f .cmo .cmi .cmx .o $(VOFILES) $(VIFILES) $(GFILES) *~
282		rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)
	200	rm -f all.ps all-gal.ps all.glob $(VFILES:.v=.glob) $(HTMLFILES) $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)
	201	- rm -rf html
283	202
284	203	archclean:
285	204	rm -f .cmx .o
286	205
287		html:
	206
	207	-include $(VFILES:.v=.v.d)
	208	.SECONDARY: $(VFILES:.v=.v.d)
288	209
289	210	# WARNING
290	211	#
291		# This Makefile has been automagically generated by coq_makefile
	212	# This Makefile has been automagically generated
292	213	# Edit at your own risks !
293	214	#
294	215	# END OF WARNING

-2

Others/FroundDivSqrt.v less more

570	570	[ intros V \| rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto ].
571	571	cut (Fcanonic radix b (Fnormalize radix b precision x));
572	572	[ intros H1; case H1; intros H2 \| apply FnormalizeCanonic; auto with arith ].
573		2: elim H2; intros H3 H4; elim H4; intros H5 H6; Contradict H; rewrite H5;
574		auto with zarith.
575	573	apply Zle_trans with (1 := H); apply Zlt_succ_le.
576	574	apply Zplus_lt_reg_l with (-1 + (precision + - Fexp y))%Z;
577	575	unfold Zsucc in \|- *.

647	645	apply Rle_powerRZ; auto with zarith real.
648	646	apply FcanonicLeastExp with radix b precision; auto with zarith float real.
649	647	apply sym_eq; apply FnormalizeCorrect; auto.
	648	elim H2; intros H3 H4; elim H4; intros H5 H6.
	649	absurd (- dExp b <= Fexp (Fnormalize radix b precision x) - precision)%Z;
	650	auto with zarith.
650	651	Qed.
651	652
652	653	Theorem errorBoundedDivClosest :

+10

-3

Others/IEEE.v less more

614	614	unfold radix in \|- *; auto with zarith.
615	615	replace (Zpower_nat radix (pred (precision p)) * radix)%Z with
616	616	(Zpos (vNum b)).
617		replace (-1 * Fnum (Fnormalize radix b (precision p) f) * radix)%Z with
	617	replace (- Fnum (Fnormalize radix b (precision p) f) * radix)%Z with
618	618	(Zabs (radix * Fnum (Fnormalize radix b (precision p) f)));
619	619	auto.
620	620	rewrite <- Zabs_Zopp; rewrite Zabs_eq; auto with zarith; [ ring \| idtac ].

1009	1009	(0 <=
1010	1010	Fnum (Float (- binary_value (pred (precision p)) (IEEE_Frac x)) (- dExp b)))%Z;
1011	1011	auto with zarith; intros H7.
1012		Contradict H7; apply Zgt_not_le; apply Zlt_gt; simpl in \|- *.
	1012	absurd ((0 <= Fnum
	1013	(Float (- binary_value (pred (precision p))
	1014	(IEEE_Frac x)) (- dExp b)))%Z); trivial.
	1015	apply Zgt_not_le; apply Zlt_gt; simpl in \|- *.
1013	1016	cut (0 <= binary_value (pred (precision p)) (IEEE_Frac x))%Z;
1014	1017	[ intros T1 \| apply Zge_le; apply binary_value_pos ].
1015	1018	cut (binary_value (pred (precision p)) (IEEE_Frac x) <> 0%Z);

1103	1106	-
1104	1107	(Zpower_nat radix (pred (precision p)) +
1105	1108	binary_value (pred (precision p)) (IEEE_Frac x)))%Z;
1106		auto with zarith; intros H5; Contradict H5.
	1109	auto with zarith; intros H5.
	1110	absurd ((0 <=
	1111	-
	1112	(Zpower_nat radix (pred (precision p)) +
	1113	binary_value (pred (precision p)) (IEEE_Frac x)))%Z); trivial.
1107	1114	apply Zgt_not_le; apply Zlt_gt.
1108	1115	apply Zplus_lt_reg_r with (Zpower_nat radix (pred (precision p))).
1109	1116	ring_simplify

-884

~~Others/RND.v~~ less more

0		Require Export AllFloat.
1
2		Section Round.
3		Variable b : Fbound.
4		Variable radix : Z.
5		Variable p : nat.
6
7		Coercion Local FtoRradix := FtoR radix.
8		Hypothesis radixMoreThanOne : (1 < radix)%Z.
9		Hypothesis pGreaterThanOne : 1 < p.
10		Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix p.
11
12
13		(** Various lemmas about exp, ln *)
14
15		Theorem exp_ln_powerRZ :
16		forall u v : Z, (0 < u)%Z -> exp (ln u * v) = powerRZ u v.
17		intros u v H1.
18		cut (forall e f : nat, (0 < e)%Z -> exp (ln e * f) = powerRZ e f).
19		intros H2.
20		case (Zle_or_lt 0 v); intros H3.
21		replace u with (Z_of_nat (Zabs_nat u));
22		[ idtac \| apply inj_abs; auto with zarith ].
23		replace v with (Z_of_nat (Zabs_nat v)); [ idtac \| apply inj_abs; auto ].
24		repeat rewrite <- INR_IZR_INZ; apply H2.
25		rewrite inj_abs; auto with zarith.
26		replace v with (- Zabs_nat v)%Z.
27		rewrite <- Rinv_powerRZ; auto with zarith real.
28		replace u with (Z_of_nat (Zabs_nat u));
29		[ idtac \| apply inj_abs; auto with zarith ].
30		rewrite Ropp_Ropp_IZR; rewrite Ropp_mult_distr_r_reverse; rewrite exp_Ropp;
31		repeat rewrite <- INR_IZR_INZ.
32		rewrite H2; auto with real.
33		rewrite inj_abs; auto with zarith.
34		rewrite <- Zabs_absolu; rewrite <- Zabs_Zopp.
35		rewrite Zabs_eq; auto with zarith.
36		intros e f H2.
37		induction f as [\| f Hrecf].
38		simpl in \|- ; ring_simplify (ln e 0)%R; apply exp_0.
39		replace (ln e * S f)%R with (ln e * f + ln e)%R.
40		rewrite exp_plus; rewrite Hrecf; rewrite exp_ln; auto with real zarith.
41		replace (Z_of_nat (S f)) with (f + 1)%Z.
42		rewrite powerRZ_add; auto with real zarith.
43		rewrite inj_S; auto with zarith.
44		replace (INR (S f)) with (f + 1)%R; [ ring \| idtac ].
45		apply trans_eq with (IZR (f + 1)).
46		rewrite plus_IZR; simpl in \|- *; rewrite <- INR_IZR_INZ; auto with real.
47		apply trans_eq with (IZR (Zsucc f)); auto with zarith real.
48		rewrite <- inj_S; rewrite <- INR_IZR_INZ; auto with zarith real.
49		Qed.
50
51		Theorem ln_radix_pos : (0 < ln radix)%R.
52		rewrite <- ln_1.
53		apply ln_increasing; auto with real zarith.
54		Qed.
55
56		Theorem exp_le_inv : forall x y : R, (exp x <= exp y)%R -> (x <= y)%R.
57		intros x y H; case H; intros H2.
58		left; apply exp_lt_inv; auto.
59		right; apply exp_inv; auto.
60		Qed.
61
62		Theorem exp_monotone : forall x y : R, (x <= y)%R -> (exp x <= exp y)%R.
63		intros x y H; case H; intros H2.
64		left; apply exp_increasing; auto.
65		right; auto with real.
66		Qed.
67
68		Theorem firstNormalPos_eq :
69		FtoRradix (firstNormalPos radix b p) = powerRZ radix (Zpred p + - dExp b).
70		unfold firstNormalPos, nNormMin, FtoRradix, FtoR in \|- ; simpl in \|- .
71		rewrite Zpower_nat_Z_powerRZ; rewrite powerRZ_add; auto with real zarith.
72		replace (Z_of_nat (pred p)) with (Zpred p);
73		[ ring \| rewrite inj_pred; auto with zarith ].
74		Qed.
75
76
77		(** Results about the ineger rounding down *)
78
79		Definition IRNDD (r : R) := Zpred (up r).
80
81		Theorem IRNDD_correct1 : forall r : R, (IRNDD r <= r)%R.
82		intros r; unfold IRNDD in \|- *.
83		generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
84		unfold Zpred in \|- *; apply Rplus_le_reg_l with (1 + - r)%R.
85		ring_simplify (1 + - r + r)%R.
86		apply Rle_trans with (2 := H2).
87		rewrite plus_IZR; right; simpl in \|- *; ring.
88		Qed.
89
90		Theorem IRNDD_correct2 : forall r : R, (r < Zsucc (IRNDD r))%R.
91		intros r; unfold IRNDD in \|- *.
92		generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
93		rewrite <- Zsucc_pred; auto.
94		Qed.
95
96		Theorem IRNDD_correct3 : forall r : R, (r - 1 < IRNDD r)%R.
97		intros r; unfold IRNDD in \|- *.
98		generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
99		unfold Zpred, Rminus in \|- ; rewrite plus_IZR; simpl in \|- ; auto with real.
100		Qed.
101
102		Hint Resolve IRNDD_correct1 IRNDD_correct2 IRNDD_correct3: real.
103
104
105		Theorem IRNDD_pos : forall r : R, (0 <= r)%R -> (0 <= IRNDD r)%R.
106		intros r H1; unfold IRNDD in \|- *.
107		generalize (archimed r); intros T; elim T; intros H3 H2; clear T.
108		replace 0%R with (IZR 0); auto with real; apply IZR_le.
109		apply Zle_Zpred.
110		apply lt_IZR; apply Rle_lt_trans with r; auto with real zarith.
111		Qed.
112
113
114		Theorem IRNDD_monotone : forall r s : R, (r <= s)%R -> (IRNDD r <= IRNDD s)%R.
115		intros r s H.
116		apply Rle_IZR; apply Zgt_succ_le; apply Zlt_gt; apply lt_IZR.
117		apply Rle_lt_trans with r; auto with real.
118		apply Rle_lt_trans with s; auto with real.
119		Qed.
120
121
122		Theorem IRNDD_eq :
123		forall (r : R) (z : Z), (z <= r)%R -> (r < Zsucc z)%R -> IRNDD r = z.
124		intros r z H1 H2.
125		cut (IRNDD r - z < 1)%Z;
126		[ intros H3 \| apply lt_IZR; rewrite <- Z_R_minus; simpl in \|- * ].
127		cut (z - IRNDD r < 1)%Z;
128		[ intros H4; auto with zarith
129		\| apply lt_IZR; rewrite <- Z_R_minus; simpl in \|- * ].
130		unfold Rminus in \|- *; apply Rle_lt_trans with (r + - IRNDD r)%R;
131		auto with real.
132		apply Rlt_le_trans with (r + - (r - 1))%R; auto with real; right; ring.
133		unfold Rminus in \|- *; apply Rle_lt_trans with (r + - z)%R; auto with real.
134		apply Rlt_le_trans with (Zsucc z + - z)%R; auto with real; right;
135		unfold Zsucc in \|- ; rewrite plus_IZR; simpl in \|- ;
136		ring.
137		Qed.
138
139		Theorem IRNDD_projector : forall z : Z, IRNDD z = z.
140		intros z.
141		apply IRNDD_eq; auto with zarith real.
142		Qed.
143
144
145		(** Rounding down of a positive real *)
146
147		Definition RND_Min_Pos (r : R) :=
148		match Rle_dec (firstNormalPos radix b p) r with
149		\| left _ =>
150		let e := IRNDD (ln r / ln radix + (- Zpred p)%Z) in
151		Float (IRNDD (r * powerRZ radix (- e))) e
152		\| right _ => Float (IRNDD (r * powerRZ radix (dExp b))) (- dExp b)
153		end.
154
155
156		Theorem RND_Min_Pos_bounded_aux :
157		forall (r : R) (e : Z),
158		(0 <= r)%R ->
159		(- dExp b <= e)%Z ->
160		(r < powerRZ radix (e + p))%R ->
161		Fbounded b (Float (IRNDD (r * powerRZ radix (- e))) e).
162		intros r e H1 H2 H3.
163		split; auto.
164		simpl in \|- *; rewrite pGivesBound; apply lt_IZR.
165		rewrite Zpower_nat_Z_powerRZ; rewrite <- Faux.Rabsolu_Zabs.
166		rewrite Rabs_right;
167		[ idtac
168		\| apply Rle_ge; apply IRNDD_pos; apply Rmult_le_pos; auto with real zarith ].
169		apply Rle_lt_trans with (1 := IRNDD_correct1 (r * powerRZ radix (- e))).
170		apply Rmult_lt_reg_l with (powerRZ radix e); auto with zarith real.
171		rewrite Rmult_comm; rewrite Rmult_assoc.
172		rewrite <- powerRZ_add; auto with zarith real.
173		rewrite <- powerRZ_add; auto with zarith real.
174		apply Rle_lt_trans with (2 := H3); ring_simplify (- e + e)%Z; simpl in \|- *; right;
175		ring.
176		Qed.
177
178
179		Theorem RND_Min_Pos_canonic :
180		forall r : R, (0 <= r)%R -> Fcanonic radix b (RND_Min_Pos r).
181		intros r H1; unfold RND_Min_Pos in \|- *.
182		generalize ln_radix_pos; intros W.
183		case (Rle_dec (firstNormalPos radix b p) r); intros H2.
184		cut (0 < r)%R; [ intros V \| idtac ].
185		2: apply Rlt_le_trans with (2 := H2); rewrite firstNormalPos_eq;
186		auto with real zarith.
187		left; split.
188		apply RND_Min_Pos_bounded_aux; auto.
189		apply Zgt_succ_le; apply Zlt_gt.
190		apply lt_IZR.
191		apply
192		Rle_lt_trans with (2 := IRNDD_correct2 (ln r / ln radix + (- Zpred p)%Z)).
193		apply Rplus_le_reg_l with (Zpred p).
194		apply Rmult_le_reg_l with (ln radix).
195		apply ln_radix_pos.
196		apply Rle_trans with (ln r).
197		apply exp_le_inv.
198		rewrite exp_ln; auto.
199		replace (Zpred p + (- dExp b)%Z)%R with (IZR (Zpred p + - dExp b)).
200		rewrite exp_ln_powerRZ; auto with zarith.
201		apply Rle_trans with (2 := H2).
202		rewrite firstNormalPos_eq; auto with real.
203		rewrite plus_IZR; rewrite Ropp_Ropp_IZR; ring.
204		rewrite Ropp_Ropp_IZR; right; field; auto with real.
205		rewrite <- exp_ln_powerRZ; auto with zarith.
206		pattern r at 1 in \|- *; rewrite <- (exp_ln r); auto.
207		apply exp_increasing.
208		rewrite plus_IZR.
209		apply
210		Rle_lt_trans with (ln radix * (ln r / ln radix + (- Zpred p)%Z - 1 + p))%R.
211		rewrite Ropp_Ropp_IZR; unfold Zpred in \|- ; rewrite plus_IZR; simpl in \|- .
212		repeat rewrite <- INR_IZR_INZ; right; field; auto with real.
213		apply Rmult_lt_compat_l; auto with real.
214		repeat rewrite <- INR_IZR_INZ.
215		apply Rplus_lt_compat_r; auto with real.
216		simpl in \|- ; rewrite pGivesBound; apply le_IZR; simpl in \|- .
217		rewrite Zpower_nat_Z_powerRZ; rewrite Zabs_eq.
218		2: apply le_IZR; rewrite Rmult_IZR; simpl in \|- *.
219		2: apply Rmult_le_pos; auto with real zarith; apply IRNDD_pos;
220		apply Rmult_le_pos; auto with real zarith.
221		rewrite Rmult_IZR; pattern (Z_of_nat p) at 1 in \|- *;
222		replace (Z_of_nat p) with (1 + Zpred p)%Z.
223		2: unfold Zpred in \|- *; ring.
224		rewrite powerRZ_add; auto with zarith real; simpl in \|- ; ring_simplify (radix 1)%R.
225		apply Rmult_le_compat_l; auto with zarith real.
226		rewrite <- inj_pred; auto with zarith.
227		rewrite <- Zpower_nat_Z_powerRZ; apply IZR_le.
228		apply Zgt_succ_le; apply Zlt_gt; apply lt_IZR; rewrite Ropp_Ropp_IZR.
229		apply
230		Rle_lt_trans
231		with (r * powerRZ radix (- IRNDD (ln r / ln radix + - pred p)))%R.
232		2: repeat rewrite <- INR_IZR_INZ; apply IRNDD_correct2.
233		rewrite <- exp_ln_powerRZ; auto with zarith.
234		rewrite Zpower_nat_Z_powerRZ; rewrite Ropp_Ropp_IZR.
235		apply Rle_trans with (r * exp (ln radix * - (ln r / ln radix + - pred p)))%R.
236		pattern r at 1 in \|- *; rewrite <- (exp_ln r); auto; rewrite <- exp_plus.
237		replace (ln r + ln radix * - (ln r / ln radix + - pred p))%R with
238		(ln radix * pred p)%R.
239		2: field; auto with real.
240		rewrite INR_IZR_INZ; rewrite exp_ln_powerRZ; auto with real zarith.
241		apply Rmult_le_compat_l; auto with real.
242		apply exp_monotone; auto with real.
243		cut (r < powerRZ radix (Zpred p + - dExp b))%R; [ intros H3 \| idtac ].
244		2: rewrite <- firstNormalPos_eq; auto with real.
245		right; split.
246		pattern (dExp b) at 2 in \|- *;
247		replace (Z_of_N (dExp b)) with (- - dExp b)%Z; auto with zarith.
248		apply RND_Min_Pos_bounded_aux; auto with zarith.
249		apply Rlt_trans with (1 := H3); apply Rlt_powerRZ; auto with real zarith.
250		rewrite Zplus_comm; auto with zarith.
251		split; [ simpl in \|- *; auto \| idtac ].
252		simpl in \|- *; rewrite pGivesBound; apply lt_IZR.
253		rewrite Zpower_nat_Z_powerRZ; rewrite <- Faux.Rabsolu_Zabs.
254		rewrite mult_IZR; rewrite Rabs_right;
255		[ idtac
256		\| apply Rle_ge; apply Rmult_le_pos; auto with real zarith; apply IRNDD_pos;
257		apply Rmult_le_pos; auto with real zarith ].
258		apply Rle_lt_trans with (radix * (r * powerRZ radix (dExp b)))%R;
259		auto with real zarith.
260		apply
261		Rlt_le_trans
262		with
263		(radix * (powerRZ radix (Zpred p + - dExp b) * powerRZ radix (dExp b)))%R;
264		auto with real zarith.
265		rewrite <- powerRZ_add; auto with zarith real.
266		pattern (IZR radix) at 1 in \|- *; replace (IZR radix) with (powerRZ radix 1);
267		[ rewrite <- powerRZ_add \| simpl in \|- * ]; auto with zarith real;
268		unfold Zpred in \|- *.
269		ring_simplify (1 + (p + -1 + - dExp b + dExp b))%Z; auto with real.
270		Qed.
271
272		Theorem RND_Min_Pos_Rle : forall r : R, (0 <= r)%R -> (RND_Min_Pos r <= r)%R.
273		intros r H.
274		unfold RND_Min_Pos in \|- *; case (Rle_dec (firstNormalPos radix b p) r);
275		intros H2.
276		unfold FtoRradix, FtoR in \|- ; simpl in \|- .
277		apply
278		Rle_trans
279		with
280		(r * powerRZ radix (- IRNDD (ln r / ln radix + (- Zpred p)%Z)) *
281		powerRZ radix (IRNDD (ln r / ln radix + (- Zpred p)%Z)))%R;
282		auto with real.
283		rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
284		ring_simplify
285		(- IRNDD (ln r / ln radix + (- Zpred p)%Z) +
286		IRNDD (ln r / ln radix + (- Zpred p)%Z))%Z; simpl in \|- *;
287		auto with real.
288		unfold FtoRradix, FtoR in \|- ; simpl in \|- .
289		apply
290		Rle_trans with (r * powerRZ radix (dExp b) * powerRZ radix (- dExp b))%R;
291		auto with real.
292		rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
293		ring_simplify (dExp b + - dExp b)%Z; simpl in \|- *; auto with real.
294		Qed.
295
296
297
298		Theorem RND_Min_Pos_monotone :
299		forall r s : R,
300		(0 <= r)%R -> (r <= s)%R -> (RND_Min_Pos r <= RND_Min_Pos s)%R.
301		intros r s V1 H.
302		cut (0 <= s)%R;
303		[ intros V2 \| apply Rle_trans with (1 := V1); auto with real ].
304		rewrite <-
305		FPredSuc
306		with
307		(x := RND_Min_Pos s)
308		(precision := p)
309		(b := b)
310		(radix := radix); auto with arith.
311		2: apply RND_Min_Pos_canonic; auto.
312		unfold FtoRradix in \|- *; apply FPredProp; auto with arith;
313		fold FtoRradix in \|- *.
314		apply RND_Min_Pos_canonic; auto.
315		apply FSuccCanonic; auto with arith; apply RND_Min_Pos_canonic; auto.
316		apply Rle_lt_trans with r; auto with real.
317		apply RND_Min_Pos_Rle; auto.
318		apply Rle_lt_trans with (1 := H).
319		replace (FtoRradix (FSucc b radix p (RND_Min_Pos s))) with
320		(RND_Min_Pos s + powerRZ radix (Fexp (RND_Min_Pos s)))%R.
321		unfold RND_Min_Pos in \|- *; case (Rle_dec (firstNormalPos radix b p) s);
322		intros H1.
323		unfold FtoRradix, FtoR in \|- ; simpl in \|- .
324		apply
325		Rle_lt_trans
326		with
327		((s * powerRZ radix (- IRNDD (ln s / ln radix + (- Zpred p)%Z)) - 1) *
328		powerRZ radix (IRNDD (ln s / ln radix + (- Zpred p)%Z)) +
329		powerRZ radix (IRNDD (ln s / ln radix + (- Zpred p)%Z)))%R;
330		auto with real.
331		right; ring_simplify.
332		rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with zarith real.
333		ring_simplify
334		(-IRNDD (ln s / ln radix + (- Zpred p)%Z) +
335		IRNDD (ln s / ln radix + (- Zpred p)%Z))%Z;
336		simpl; ring.
337		unfold FtoRradix, FtoR in \|- ; simpl in \|- .
338		apply
339		Rle_lt_trans
340		with
341		((s * powerRZ radix (dExp b) - 1) * powerRZ radix (- dExp b) +
342		powerRZ radix (- dExp b))%R; auto with real.
343		right; ring_simplify.
344		rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with zarith real.
345		ring_simplify (dExp b + -dExp b)%Z; simpl in \|- *; ring.
346		replace (powerRZ radix (Fexp (RND_Min_Pos s))) with
347		(FtoR radix (Float 1%nat (Fexp (RND_Min_Pos s))));
348		[ idtac \| unfold FtoR in \|- ; simpl in \|- ; ring ].
349		rewrite <- FSuccDiff1 with b radix p (RND_Min_Pos s); auto with arith.
350		rewrite Fminus_correct; auto with zarith; fold FtoRradix in \|- *; ring.
351		cut (- nNormMin radix p < Fnum (RND_Min_Pos s))%Z; auto with zarith.
352		apply Zlt_le_trans with 0%Z.
353		replace 0%Z with (- (0))%Z; unfold nNormMin in \|- *; auto with arith zarith.
354		apply le_IZR; unfold RND_Min_Pos in \|- *;
355		case (Rle_dec (firstNormalPos radix b p) s); intros H1;
356		simpl in \|- *; apply IRNDD_pos; apply Rmult_le_pos;
357		auto with real zarith.
358		Qed.
359
360
361		Theorem RND_Min_Pos_projector :
362		forall f : float,
363		(0 <= f)%R -> Fcanonic radix b f -> FtoRradix (RND_Min_Pos f) = f.
364		intros f H1 H2.
365		unfold RND_Min_Pos in \|- *; case (Rle_dec (firstNormalPos radix b p) f);
366		intros H3.
367		replace (IRNDD (ln f / ln radix + (- Zpred p)%Z)) with (Fexp f).
368		replace (f * powerRZ radix (- Fexp f))%R with (IZR (Fnum f)).
369		rewrite IRNDD_projector; unfold FtoRradix, FtoR in \|- ; simpl in \|- ; ring.
370		unfold FtoRradix, FtoR in \|- ; simpl in \|- .
371		rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
372		ring_simplify (Fexp f + - Fexp f)%Z; simpl in \|- *; ring.
373		generalize ln_radix_pos; intros V1.
374		cut (0 < Fnum f)%R; [ intros V2 \| idtac ].
375		apply sym_eq; apply IRNDD_eq.
376		unfold FtoRradix, FtoR in \|- ; simpl in \|- .
377		rewrite ln_mult; auto with real zarith.
378		unfold Rdiv in \|- *; rewrite Rmult_plus_distr_r.
379		apply Rle_trans with (Zpred p + Fexp f + (- Zpred p)%Z)%R;
380		[ rewrite Ropp_Ropp_IZR; right; ring \| idtac ].
381		apply Rplus_le_compat_r; apply Rplus_le_compat.
382		apply Rmult_le_reg_l with (ln radix); [ auto with real \| idtac ].
383		apply Rle_trans with (ln (Fnum f)); [ idtac \| right; field; auto with real ].
384		apply exp_le_inv.
385		rewrite exp_ln; auto.
386		rewrite exp_ln_powerRZ; auto with zarith.
387		case H2; intros T; elim T; intros C1 C2.
388		apply Rmult_le_reg_l with radix; auto with real zarith.
389		apply Rle_trans with (IZR (Zpos (vNum b)));
390		[ right; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ \| idtac ].
391		pattern (Z_of_nat p) at 2 in \|- *; replace (Z_of_nat p) with (1 + Zpred p)%Z;
392		[ rewrite powerRZ_add; auto with real zarith; simpl in \|- *; ring
393		\| unfold Zpred in \|- *; ring ].
394		rewrite <- (Rabs_right (radix * Fnum f)); auto with real zarith.
395		rewrite <- mult_IZR; rewrite Faux.Rabsolu_Zabs; auto with real zarith.
396		apply Rle_ge; apply Rmult_le_pos; auto with real zarith.
397		Contradict H3; apply Rlt_not_le; unfold FtoRradix in \|- *;
398		apply FsubnormalLtFirstNormalPos; auto with zarith.
399		apply Rmult_le_reg_l with (ln radix); [ auto with real \| idtac ].
400		apply Rle_trans with (ln (powerRZ radix (Fexp f)));
401		[ idtac \| right; field; auto with real ].
402		rewrite <- exp_ln_powerRZ; auto with zarith.
403		rewrite ln_exp; auto with real.
404		unfold FtoRradix, FtoR in \|- ; simpl in \|- .
405		rewrite ln_mult; auto with real zarith.
406		rewrite <- exp_ln_powerRZ; auto with zarith.
407		rewrite ln_exp; auto with real.
408		unfold Rdiv in \|- *; rewrite Rmult_plus_distr_r.
409		apply Rlt_le_trans with (p + Fexp f + (- Zpred p)%Z)%R.
410		2: rewrite Ropp_Ropp_IZR; unfold Zsucc, Zpred in \|- *;
411		repeat rewrite plus_IZR; repeat rewrite <- INR_IZR_INZ;
412		simpl in \|- *; right; ring.
413		replace (ln radix * Fexp f * / ln radix)%R with (IZR (Fexp f));
414		[ idtac \| field; auto with real ].
415		apply Rplus_lt_compat_r; apply Rplus_lt_compat_r.
416		apply Rmult_lt_reg_l with (ln radix); [ auto with real \| idtac ].
417		apply Rle_lt_trans with (ln (Fnum f));
418		[ right; field; auto with real \| idtac ].
419		apply exp_lt_inv.
420		rewrite exp_ln; auto.
421		rewrite INR_IZR_INZ; rewrite exp_ln_powerRZ; auto with zarith.
422		apply Rlt_le_trans with (IZR (Zpos (vNum b))).
423		rewrite <- (Rabs_right (IZR (Fnum f))); auto with real.
424		rewrite Faux.Rabsolu_Zabs; apply Rlt_IZR; cut (Fbounded b f);
425		auto with real zarith float.
426		apply FcanonicBound with radix; auto.
427		apply Rle_ge; auto with real.
428		right; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
429		replace 0%R with (IZR 0); auto with real zarith; apply Rlt_IZR.
430		apply LtR0Fnum with radix; auto with zarith; fold FtoRradix in \|- *.
431		apply Rlt_le_trans with (2 := H3); rewrite firstNormalPos_eq;
432		auto with real zarith.
433		case H2; intros T; elim T; intros C1 C2.
434		absurd (firstNormalPos radix b p <= f)%R; auto with real.
435		unfold FtoRradix in \|- *; apply FnormalLtFirstNormalPos; auto with arith.
436		elim C2; intros C3 C4.
437		replace (f * powerRZ radix (dExp b))%R with (IZR (Fnum f)).
438		rewrite IRNDD_projector; rewrite <- C3; unfold FtoRradix, FtoR in \|- *;
439		simpl in \|- *; ring.
440		unfold FtoRradix, FtoR in \|- *; rewrite C3.
441		rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
442		ring_simplify (- dExp b + dExp b)%Z; simpl in \|- *; ring.
443		Qed.
444
445		Theorem RND_Min_Pos_correct :
446		forall r : R, (0 <= r)%R -> isMin b radix r (RND_Min_Pos r).
447		intros r H1.
448		split.
449		apply FcanonicBound with radix; apply RND_Min_Pos_canonic; auto.
450		split.
451		apply RND_Min_Pos_Rle; auto.
452		fold FtoRradix in \|- *; intros f H2 H3.
453		case (Rle_or_lt 0 f); intros H4.
454		unfold FtoRradix in \|- *; rewrite <- FnormalizeCorrect with radix b p f; auto;
455		fold FtoRradix in \|- *.
456		rewrite <- RND_Min_Pos_projector.
457		apply RND_Min_Pos_monotone; unfold FtoRradix in \|- *;
458		rewrite FnormalizeCorrect; auto.
459		unfold FtoRradix in \|- *; rewrite FnormalizeCorrect; auto.
460		apply FnormalizeCanonic; auto with arith.
461		apply Rle_trans with 0%R; auto with real.
462		unfold RND_Min_Pos in \|- *; case (Rle_dec (firstNormalPos radix b p) r);
463		intros H5; unfold FtoRradix, FtoR in \|- ; simpl in \|- ;
464		apply Rmult_le_pos; auto with real zarith; apply IRNDD_pos;
465		apply Rmult_le_pos; auto with real zarith.
466		Qed.
467
468
469		(** Easily deduced, the rounding up of a positive real *)
470
471		Definition RND_Max_Pos (r : R) :=
472		match Req_EM_T r (RND_Min_Pos r) with
473		\| left _ => RND_Min_Pos r
474		\| right _ => FSucc b radix p (RND_Min_Pos r)
475		end.
476
477		Theorem RND_Max_Pos_canonic :
478		forall r : R, (0 <= r)%R -> Fcanonic radix b (RND_Max_Pos r).
479		intros r H; unfold RND_Max_Pos in \|- *.
480		case (Req_EM_T r (RND_Min_Pos r)); intros H1.
481		apply RND_Min_Pos_canonic; auto.
482		apply FSuccCanonic; auto with arith; apply RND_Min_Pos_canonic; auto.
483		Qed.
484
485		Theorem RND_Max_Pos_Rle : forall r : R, (0 <= r)%R -> (r <= RND_Max_Pos r)%R.
486		intros r H.
487		unfold RND_Max_Pos in \|- *; case (Req_EM_T r (RND_Min_Pos r)); intros H1.
488		rewrite <- H1; auto with real.
489		case (Rle_or_lt r (FSucc b radix p (RND_Min_Pos r))); auto; intros H2.
490		generalize (RND_Min_Pos_correct r H); intros T; elim T; intros H3 T1; elim T1;
491		intros H4 H5; clear T T1.
492		absurd (FSucc b radix p (RND_Min_Pos r) <= RND_Min_Pos r)%R;
493		auto with float zarith real.
494		apply Rlt_not_le; auto with float zarith.
495		unfold FtoRradix in \|- *; apply FSuccLt; auto with arith.
496		Qed.
497
498		Theorem RND_Max_Pos_correct :
499		forall r : R, (0 <= r)%R -> isMax b radix r (RND_Max_Pos r).
500		intros r H.
501		split.
502		apply FcanonicBound with radix; apply RND_Max_Pos_canonic; auto.
503		split.
504		apply RND_Max_Pos_Rle; auto.
505		unfold RND_Max_Pos in \|- *; case (Req_EM_T r (RND_Min_Pos r)); intros H1.
506		fold FtoRradix in \|- *; intros f H2 H3; rewrite <- H1; auto with real.
507		fold FtoRradix in \|- *; intros f H2 H3.
508		case H3; intros V.
509		case (Rle_or_lt (FSucc b radix p (RND_Min_Pos r)) f); auto; intros H4.
510		absurd (f < f)%R; auto with real.
511		apply Rle_lt_trans with (RND_Min_Pos r).
512		rewrite <- FPredSuc with b radix p (RND_Min_Pos r); auto with arith.
513		2: apply RND_Min_Pos_canonic; auto.
514		unfold FtoRradix in \|- *; rewrite <- FnormalizeCorrect with radix b p f; auto.
515		apply FPredProp; auto with arith float zarith.
516		apply FSuccCanonic; auto with arith; apply RND_Min_Pos_canonic; auto.
517		rewrite FnormalizeCorrect; auto with real.
518		apply Rle_lt_trans with (2 := V).
519		apply RND_Min_Pos_Rle; auto.
520		Contradict H1.
521		rewrite V; unfold FtoRradix in \|- *;
522		rewrite <- FnormalizeCorrect with radix b p f; auto.
523		fold FtoRradix in \|- *; apply sym_eq; apply RND_Min_Pos_projector;
524		auto with zarith float.
525		unfold FtoRradix in \|- ; rewrite FnormalizeCorrect; fold FtoRradix in \|- ;
526		auto with real.
527		apply Rle_trans with r; auto with real.
528		Qed.
529
530		(** Roundings up and down of any real *)
531
532		Definition RND_Min (r : R) :=
533		match Rle_dec 0 r with
534		\| left _ => RND_Min_Pos r
535		\| right _ => Fopp (RND_Max_Pos (- r))
536		end.
537
538		Theorem RND_Min_canonic : forall r : R, Fcanonic radix b (RND_Min r).
539		intros r.
540		unfold RND_Min in \|- *; case (Rle_dec 0 r); intros H.
541		apply RND_Min_Pos_canonic; auto.
542		apply FcanonicFopp; apply RND_Max_Pos_canonic; auto with real.
543		Qed.
544
545		Theorem RND_Min_correct : forall r : R, isMin b radix r (RND_Min r).
546		intros r.
547		unfold RND_Min in \|- *; case (Rle_dec 0 r); intros H.
548		apply RND_Min_Pos_correct; auto.
549		pattern r at 1 in \|- *; rewrite <- (Ropp_involutive r).
550		apply MaxOppMin; apply RND_Max_Pos_correct; auto with real.
551		Qed.
552
553		Definition RND_Max (r : R) :=
554		match Rle_dec 0 r with
555		\| left _ => RND_Max_Pos r
556		\| right _ => Fopp (RND_Min_Pos (- r))
557		end.
558
559		Theorem RND_Max_canonic : forall r : R, Fcanonic radix b (RND_Max r).
560		intros r.
561		unfold RND_Max in \|- *; case (Rle_dec 0 r); intros H.
562		apply RND_Max_Pos_canonic; auto.
563		apply FcanonicFopp; apply RND_Min_Pos_canonic; auto with real.
564		Qed.
565
566		Theorem RND_Max_correct : forall r : R, isMax b radix r (RND_Max r).
567		intros r.
568		unfold RND_Max in \|- *; case (Rle_dec 0 r); intros H.
569		apply RND_Max_Pos_correct; auto.
570		pattern r at 1 in \|- *; rewrite <- (Ropp_involutive r).
571		apply MinOppMax; apply RND_Min_Pos_correct; auto with real.
572		Qed.
573
574		Definition RND_Zero (r : R) :=
575		match Rle_dec 0 r with
576		\| left _ => RND_Min r
577		\| right _ => RND_Max r
578		end.
579
580		Theorem RND_Zero_canonic : forall r : R, Fcanonic radix b (RND_Zero r).
581		intros r.
582		unfold RND_Zero in \|- *; case (Rle_dec 0 r); intros H.
583		apply RND_Min_canonic; auto.
584		apply RND_Max_canonic; auto.
585		Qed.
586
587		Theorem RND_Zero_correct : forall r : R, ToZeroP b radix r (RND_Zero r).
588		intros r.
589		unfold ToZeroP, RND_Zero.
590		case (Rle_dec 0 r); intros H.
591		left; split; auto with real; apply RND_Min_correct; auto with real.
592		right; split; auto with real;apply RND_Max_correct; auto with real.
593		Qed.
594
595
596		(** Rounding to the nearest of any real
597		First, ClosestUp (when equality, the biggest is returned)
598		Then, EvenClosest (when equality, the even is returned)
599		*)
600
601		Definition RND_ClosestUp (r : R) :=
602		match Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) with
603		\| left _ => RND_Max r
604		\| right _ => RND_Min r
605		end.
606
607
608		Theorem RND_ClosestUp_canonic :
609		forall r : R, Fcanonic radix b (RND_ClosestUp r).
610		intros r.
611		unfold RND_ClosestUp in \|- *;
612		case (Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)));
613		intros H; [ apply RND_Max_canonic \| apply RND_Min_canonic ].
614		Qed.
615
616		Theorem RND_ClosestUp_correct :
617		forall r : R, Closest b radix r (RND_ClosestUp r).
618		intros r.
619		cut (RND_Min r <= r)%R; [ intros V1 \| idtac ].
620		2: generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
621		intros T3 T4; auto with real.
622		cut (r <= RND_Max r)%R; [ intros V2 \| idtac ].
623		2: generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
624		intros T3 T4; auto with real.
625		cut (forall v w : R, (v <= w)%R -> (0 <= w - v)%R); [ intros V3 \| idtac ].
626		2: intros v w H; apply Rplus_le_reg_l with v; ring_simplify (v + (w - v))%R;
627		ring_simplify (v + 0)%R; auto with real.
628		cut (forall v w : R, (v <= w)%R -> (v - w <= 0)%R); [ intros V4 \| idtac ].
629		2: intros v w H; apply Rplus_le_reg_l with w; ring_simplify; auto with real.
630		unfold RND_ClosestUp in \|- *;
631		case (Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)));
632		intros H; split;
633		[ apply FcanonicBound with radix; apply RND_Max_canonic
634		\| intros f H1; fold FtoRradix in \|- *
635		\| apply FcanonicBound with radix; apply RND_Min_canonic
636		\| intros f H1; fold FtoRradix in \|- * ].
637		rewrite Rabs_right in H; [ idtac \| apply Rle_ge; apply V3; auto with real ].
638		rewrite Faux.Rabsolu_left1 in H; [ idtac \| apply V4; auto with real ].
639		rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
640		case (Rle_or_lt f r); intros H2.
641		rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
642		apply Rle_trans with (1 := H); apply Ropp_le_contravar; unfold Rminus in \|- *;
643		apply Rplus_le_compat_r.
644		generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
645		intros T3 T4; auto with real.
646		rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
647		unfold Rminus in \|- *; apply Rplus_le_compat_r.
648		generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
649		intros T3 T4; auto with real.
650		cut (Rabs (RND_Min r - r) < Rabs (RND_Max r - r))%R; auto with real;
651		intros H'.
652		rewrite Faux.Rabsolu_left1 in H'; [ idtac \| apply V4; auto with real ].
653		rewrite Rabs_right in H'; [ idtac \| apply Rle_ge; apply V3; auto with real ].
654		rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
655		case (Rle_or_lt f r); intros H2.
656		rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
657		apply Ropp_le_contravar; unfold Rminus in \|- *; apply Rplus_le_compat_r.
658		generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
659		intros T3 T4; auto with real.
660		rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
661		apply Rle_trans with (RND_Max r - r)%R; auto with real; unfold Rminus in \|- *;
662		apply Rplus_le_compat_r.
663		generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
664		intros T3 T4; auto with real.
665		Qed.
666
667
668
669		Definition RND_EvenClosest (r : R) :=
670		match Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) with
671		\| left H =>
672		match
673		Rle_lt_or_eq_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) H
674		with
675		\| left _ => RND_Max r
676		\| right _ =>
677		match OddEvenDec (Fnum (RND_Min r)) with
678		\| left _ => RND_Max r
679		\| right _ => RND_Min r
680		end
681		end
682		\| right _ => RND_Min r
683		end.
684
685
686		Theorem RND_EvenClosest_canonic :
687		forall r : R, Fcanonic radix b (RND_EvenClosest r).
688		intros r; unfold RND_EvenClosest in \|- *.
689		case (Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r))); intros H1.
690		case (Rle_lt_or_eq_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) H1);
691		intros H2.
692		apply RND_Max_canonic.
693		case (OddEvenDec (Fnum (RND_Min r))); intros H3.
694		apply RND_Max_canonic.
695		apply RND_Min_canonic.
696		apply RND_Min_canonic.
697		Qed.
698
699		Theorem RND_EvenClosest_correct :
700		forall r : R, EvenClosest b radix p r (RND_EvenClosest r).
701		intros r.
702		cut (RND_Min r <= r)%R; [ intros V1 \| idtac ].
703		2: generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
704		intros T3 T4; auto with real.
705		cut (r <= RND_Max r)%R; [ intros V2 \| idtac ].
706		2: generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
707		intros T3 T4; auto with real.
708		cut (forall v w : R, (v <= w)%R -> (0 <= w - v)%R); [ intros V3 \| idtac ].
709		2: intros v w H; apply Rplus_le_reg_l with v; ring_simplify; auto with real.
710		cut (forall v w : R, (v <= w)%R -> (v - w <= 0)%R); [ intros V4 \| idtac ].
711		2: intros v w H; apply Rplus_le_reg_l with w; ring_simplify; auto with real.
712		unfold RND_EvenClosest in \|- *;
713		case (Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)));
714		intros H1.
715		case (Rle_lt_or_eq_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) H1);
716		intros H2.
717		split.
718		split.
719		apply FcanonicBound with radix; apply RND_Max_canonic.
720		intros f H3; fold FtoRradix in \|- *.
721		rewrite Rabs_right in H1; [ idtac \| apply Rle_ge; apply V3; auto with real ].
722		rewrite Faux.Rabsolu_left1 in H1; [ idtac \| apply V4; auto with real ].
723		rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
724		case (Rle_or_lt f r); intros H4.
725		rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
726		apply Rle_trans with (1 := H1); apply Ropp_le_contravar;
727		unfold Rminus in \|- *; apply Rplus_le_compat_r.
728		generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
729		intros T3 T4; auto with real.
730		rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
731		unfold Rminus in \|- *; apply Rplus_le_compat_r.
732		generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
733		intros T3 T4; auto with real.
734		right; intros q H3.
735		generalize (ClosestMinOrMax b radix); unfold MinOrMaxP in \|- *; intros T.
736		case (T r q); auto; intros H4; clear T.
737		Contradict H2; apply Rle_not_lt.
738		replace (FtoRradix (RND_Min r)) with (FtoRradix q).
739		elim H3; intros T1 T2; unfold FtoRradix in \|- *; apply T2.
740		apply FcanonicBound with radix; apply RND_Max_canonic.
741		generalize (MinUniqueP b radix); unfold UniqueP in \|- *; intros T;
742		apply T with r; auto.
743		apply RND_Min_correct.
744		generalize (MaxUniqueP b radix); unfold UniqueP in \|- *; intros T;
745		apply T with r; auto.
746		apply RND_Max_correct.
747		case (OddEvenDec (Fnum (RND_Min r))); intros H3.
748		split.
749		split.
750		apply FcanonicBound with radix; apply RND_Max_canonic.
751		intros f H4; fold FtoRradix in \|- *.
752		rewrite Rabs_right in H1; [ idtac \| apply Rle_ge; apply V3; auto with real ].
753		rewrite Faux.Rabsolu_left1 in H1; [ idtac \| apply V4; auto with real ].
754		rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
755		case (Rle_or_lt f r); intros H5.
756		rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
757		apply Rle_trans with (1 := H1); apply Ropp_le_contravar;
758		unfold Rminus in \|- *; apply Rplus_le_compat_r.
759		generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
760		intros T3 T4; auto with real.
761		rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
762		unfold Rminus in \|- *; apply Rplus_le_compat_r.
763		generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
764		intros T3 T4; auto with real.
765		case (Req_EM_T (RND_Max r) (RND_Min r)); intros W.
766		right; intros q H4.
767		generalize (ClosestMinOrMax b radix); unfold MinOrMaxP in \|- *; intros T.
768		case (T r q); auto; intros H5; clear T.
769		fold FtoRradix in \|- *; rewrite W; generalize (MinUniqueP b radix);
770		unfold UniqueP in \|- *; intros T; apply T with r;
771		auto.
772		apply RND_Min_correct.
773		generalize (MaxUniqueP b radix); unfold UniqueP in \|- *; intros T;
774		apply T with r; auto.
775		apply RND_Max_correct.
776		left; unfold FNeven in \|- *.
777		rewrite FcanonicFnormalizeEq; auto with arith;
778		[ idtac \| apply RND_Max_canonic ].
779		replace (RND_Max r) with (FSucc b radix p (RND_Min r)).
780		apply FoddSuc; auto.
781		unfold RND_Max, RND_Min in \|- *; case (Rle_dec 0 r); intros W1.
782		unfold RND_Max_Pos in \|- *.
783		case (Req_EM_T r (RND_Min_Pos r)); intros W2; auto.
784		Contradict W.
785		pattern r at 1 in \|- *; rewrite W2.
786		apply sym_eq; unfold FtoRradix in \|- *;
787		apply RoundedModeProjectorIdemEq with b p (isMax b radix);
788		auto.
789		apply MaxRoundedModeP with p; auto.
790		apply FcanonicBound with radix; apply RND_Min_canonic.
791		replace (FtoR radix (RND_Min r)) with (FtoR radix (RND_Min_Pos r));
792		[ fold FtoRradix in \|- *; rewrite <- W2; apply RND_Max_correct \| idtac ].
793		fold FtoRradix in \|- ; unfold RND_Min in \|- ; auto with real.
794		case (Rle_dec 0 r); auto with real; intros W3; Contradict W1; auto with real.
795		unfold RND_Max_Pos in \|- *.
796		case (Req_EM_T (- r) (RND_Min_Pos (- r))); intros W2; auto.
797		Contradict W.
798		cut (r = FtoRradix (Fopp (RND_Min_Pos (- r)))); [ intros W3 \| idtac ].
799		pattern r at 1 in \|- *; rewrite W3.
800		apply sym_eq; unfold FtoRradix in \|- *;
801		apply RoundedModeProjectorIdemEq with b p (isMax b radix);
802		auto.
803		apply MaxRoundedModeP with p; auto.
804		apply FcanonicBound with radix; apply RND_Min_canonic.
805		replace (FtoR radix (RND_Min r)) with (- FtoR radix (RND_Min_Pos (- r)))%R;
806		[ fold FtoRradix in \|- *; rewrite <- W3 \| idtac ].
807		rewrite <- W2; rewrite Ropp_involutive; apply RND_Max_correct.
808		fold FtoRradix in \|- ; unfold RND_Min in \|- ; auto with real.
809		case (Rle_dec 0 r).
810		intros W4; Contradict W1; auto with real.
811		intros W4; unfold RND_Max_Pos in \|- *;
812		case (Req_EM_T (- r) (RND_Min_Pos (- r))); intros W5.
813		unfold FtoRradix in \|- *; rewrite Fopp_correct; ring.
814		Contradict W2; auto with real.
815		unfold FtoRradix in \|- ; rewrite Fopp_correct; fold FtoRradix in \|- ;
816		rewrite <- W2; ring.
817		pattern (RND_Min_Pos (- r)) at 1 in \|- *;
818		rewrite <- (Fopp_Fopp (RND_Min_Pos (- r))).
819		rewrite <- FPredFopFSucc; auto with arith.
820		apply FSucPred; auto with arith.
821		apply FcanonicFopp; apply RND_Min_Pos_canonic; auto with real.
822		split.
823		split.
824		apply FcanonicBound with radix; apply RND_Min_canonic.
825		intros f H4; fold FtoRradix in \|- *.
826		rewrite Rabs_right in H1; [ idtac \| apply Rle_ge; apply V3; auto with real ].
827		rewrite Faux.Rabsolu_left1 in H1; [ idtac \| apply V4; auto with real ].
828		case (Rle_or_lt f r); intros H5.
829		rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
830		rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
831		apply Ropp_le_contravar; unfold Rminus in \|- *; apply Rplus_le_compat_r.
832		generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
833		intros T3 T4; auto with real.
834		rewrite <- H2.
835		rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
836		rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
837		unfold Rminus in \|- *; apply Rplus_le_compat_r.
838		generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
839		intros T3 T4; auto with real.
840		left; unfold FNeven in \|- *.
841		rewrite FcanonicFnormalizeEq; auto with arith; apply RND_Min_canonic.
842		cut (Rabs (RND_Min r - r) < Rabs (RND_Max r - r))%R; auto with real;
843		intros H'.
844		cut (Rabs (RND_Min r - r) < Rabs (RND_Max r - r))%R; auto with real;
845		intros H''.
846		rewrite Faux.Rabsolu_left1 in H'; [ idtac \| apply V4; auto with real ].
847		rewrite Rabs_right in H'; [ idtac \| apply Rle_ge; apply V3; auto with real ].
848		split.
849		split.
850		apply FcanonicBound with radix; apply RND_Min_canonic.
851		intros f W1.
852		rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
853		case (Rle_or_lt f r); intros H2.
854		rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
855		apply Ropp_le_contravar; unfold Rminus in \|- *; apply Rplus_le_compat_r.
856		generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
857		intros T3 T4; auto with real.
858		rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
859		apply Rle_trans with (RND_Max r - r)%R; auto with real; unfold Rminus in \|- *;
860		apply Rplus_le_compat_r.
861		generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
862		intros T3 T4; auto with real.
863		right; intros q H3.
864		generalize (ClosestMinOrMax b radix); unfold MinOrMaxP in \|- *; intros T.
865		case (T r q); auto; intros H4; clear T.
866		generalize (MinUniqueP b radix); unfold UniqueP in \|- *; intros T;
867		apply T with r; auto.
868		apply RND_Min_correct.
869		Contradict H''; apply Rle_not_lt.
870		replace (FtoRradix (RND_Max r)) with (FtoRradix q).
871		elim H3; intros T1 T2; unfold FtoRradix in \|- *; apply T2.
872		apply FcanonicBound with radix; apply RND_Min_canonic.
873		generalize (MaxUniqueP b radix); unfold UniqueP in \|- *; intros T;
874		apply T with r; auto.
875		apply RND_Max_correct.
876		Qed.
877
878
879
880
881
882
883		End Round.⏎

-2

Others/Veltkamp.v less more

572	572	intros.
573	573	replace z with ((z-f)+f)%R;[idtac\|ring].
574	574	apply Rle_trans with (Rabs(z-f)+Rabs(f))%R;[apply Rabs_triang\|idtac].
575		apply Rplus_le_reg_l with (-Rabs(f))%R.
	575	apply Rplus_le_reg_l with (- Rabs(f))%R.
576	576	ring_simplify.
577	577	apply Rmult_le_reg_l with 2%nat; auto with real zarith.
578	578	apply Rle_trans with (Fulp b radix t f).

2872	2872	apply ClosestUlp; auto with zarith.
2873	2873	rewrite <- Rabs_Ropp.
2874	2874	replace (- (FtoR radix g - fext))%R with (fext - FtoR radix g)%R;[idtac\|ring].
2875		apply Rle_trans with (Rabs fext -Rabs (FtoR radix g))%R;[idtac\|apply Rabs_triang_inv].
	2875	apply Rle_trans with (Rabs fext - Rabs (FtoR radix g))%R;[idtac\|apply Rabs_triang_inv].
2876	2876	apply Rle_trans with ((powerRZ radix (n-1+Fexp (Fnormalize radix b0 n f))
2877	2877	- powerRZ radix (-1+ Fexp (Fnormalize radix b0 n f)))
2878	2878	- powerRZ radix (n-1-dExp b0))%R; [idtac\|unfold Rminus; apply Rplus_le_compat].

-1

Others/discriminant.v less more

1164	1164	rewrite Zpower_nat_Z_powerRZ; auto with real zarith; simpl; ring.
1165	1165	unfold Rminus; rewrite Rplus_assoc; apply Rplus_le_compat_l.
1166	1166	replace (Fexp p) with (Zsucc e);[unfold Zsucc\|rewrite p_eqF; simpl; auto with zarith].
1167		ring_simplify (-2+(e+1))%Z.
	1167	ring_simplify (e+1-2)%Z; unfold Zminus.
1168	1168	repeat rewrite powerRZ_add; auto with real zarith; simpl; right; field.
1169	1169	apply Rplus_le_reg_l with (p-(Float (Zpred (Zpower_nat radix precision)) e))%R.
1170	1170	apply Rle_trans with (-(b*b'-p))%R;[right;ring\|idtac].

-1

Others/discriminant2.v less more

1200	1200	rewrite Zpower_nat_Z_powerRZ; auto with real zarith; simpl; ring.
1201	1201	unfold Rminus; rewrite Rplus_assoc; apply Rplus_le_compat_l.
1202	1202	replace (Fexp p) with (Zsucc e);[unfold Zsucc\|rewrite p_eqF; simpl; auto with zarith].
1203		ring_simplify (-2+(e+1))%Z.
	1203	ring_simplify (e+1-2)%Z; unfold Zminus.
1204	1204	repeat rewrite powerRZ_add; auto with real zarith; simpl; right; field.
1205	1205	apply Rplus_le_reg_l with (p-(Float (Zpred (Zpower_nat radix precision)) e))%R.
1206	1206	apply Rle_trans with (-(b*b'-p))%R;[right;ring\|idtac].

+884

-0

RND.v less more

	0	Require Export ClosestMult.
	1
	2	Section Round.
	3	Variable b : Fbound.
	4	Variable radix : Z.
	5	Variable p : nat.
	6
	7	Coercion Local FtoRradix := FtoR radix.
	8	Hypothesis radixMoreThanOne : (1 < radix)%Z.
	9	Hypothesis pGreaterThanOne : 1 < p.
	10	Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix p.
	11
	12
	13	(** Various lemmas about exp, ln *)
	14
	15	Theorem exp_ln_powerRZ :
	16	forall u v : Z, (0 < u)%Z -> exp (ln u * v) = powerRZ u v.
	17	intros u v H1.
	18	cut (forall e f : nat, (0 < e)%Z -> exp (ln e * f) = powerRZ e f).
	19	intros H2.
	20	case (Zle_or_lt 0 v); intros H3.
	21	replace u with (Z_of_nat (Zabs_nat u));
	22	[ idtac \| apply inj_abs; auto with zarith ].
	23	replace v with (Z_of_nat (Zabs_nat v)); [ idtac \| apply inj_abs; auto ].
	24	repeat rewrite <- INR_IZR_INZ; apply H2.
	25	rewrite inj_abs; auto with zarith.
	26	replace v with (- Zabs_nat v)%Z.
	27	rewrite <- Rinv_powerRZ; auto with zarith real.
	28	replace u with (Z_of_nat (Zabs_nat u));
	29	[ idtac \| apply inj_abs; auto with zarith ].
	30	rewrite Ropp_Ropp_IZR; rewrite Ropp_mult_distr_r_reverse; rewrite exp_Ropp;
	31	repeat rewrite <- INR_IZR_INZ.
	32	rewrite H2; auto with real.
	33	rewrite inj_abs; auto with zarith.
	34	rewrite <- Zabs_absolu; rewrite <- Zabs_Zopp.
	35	rewrite Zabs_eq; auto with zarith.
	36	intros e f H2.
	37	induction f as [\| f Hrecf].
	38	simpl in \|- ; ring_simplify (ln e 0)%R; apply exp_0.
	39	replace (ln e * S f)%R with (ln e * f + ln e)%R.
	40	rewrite exp_plus; rewrite Hrecf; rewrite exp_ln; auto with real zarith.
	41	replace (Z_of_nat (S f)) with (f + 1)%Z.
	42	rewrite powerRZ_add; auto with real zarith.
	43	rewrite inj_S; auto with zarith.
	44	replace (INR (S f)) with (f + 1)%R; [ ring \| idtac ].
	45	apply trans_eq with (IZR (f + 1)).
	46	rewrite plus_IZR; simpl in \|- *; rewrite <- INR_IZR_INZ; auto with real.
	47	apply trans_eq with (IZR (Zsucc f)); auto with zarith real.
	48	rewrite <- inj_S; rewrite <- INR_IZR_INZ; auto with zarith real.
	49	Qed.
	50
	51	Theorem ln_radix_pos : (0 < ln radix)%R.
	52	rewrite <- ln_1.
	53	apply ln_increasing; auto with real zarith.
	54	Qed.
	55
	56	Theorem exp_le_inv : forall x y : R, (exp x <= exp y)%R -> (x <= y)%R.
	57	intros x y H; case H; intros H2.
	58	left; apply exp_lt_inv; auto.
	59	right; apply exp_inv; auto.
	60	Qed.
	61
	62	Theorem exp_monotone : forall x y : R, (x <= y)%R -> (exp x <= exp y)%R.
	63	intros x y H; case H; intros H2.
	64	left; apply exp_increasing; auto.
	65	right; auto with real.
	66	Qed.
	67
	68	Theorem firstNormalPos_eq :
	69	FtoRradix (firstNormalPos radix b p) = powerRZ radix (Zpred p + - dExp b).
	70	unfold firstNormalPos, nNormMin, FtoRradix, FtoR in \|- ; simpl in \|- .
	71	rewrite Zpower_nat_Z_powerRZ; rewrite powerRZ_add; auto with real zarith.
	72	replace (Z_of_nat (pred p)) with (Zpred p);
	73	[ ring \| rewrite inj_pred; auto with zarith ].
	74	Qed.
	75
	76
	77	(** Results about the ineger rounding down *)
	78
	79	Definition IRNDD (r : R) := Zpred (up r).
	80
	81	Theorem IRNDD_correct1 : forall r : R, (IRNDD r <= r)%R.
	82	intros r; unfold IRNDD in \|- *.
	83	generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
	84	unfold Zpred in \|- *; apply Rplus_le_reg_l with (1 + - r)%R.
	85	ring_simplify (1 + - r + r)%R.
	86	apply Rle_trans with (2 := H2).
	87	rewrite plus_IZR; right; simpl in \|- *; ring.
	88	Qed.
	89
	90	Theorem IRNDD_correct2 : forall r : R, (r < Zsucc (IRNDD r))%R.
	91	intros r; unfold IRNDD in \|- *.
	92	generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
	93	rewrite <- Zsucc_pred; auto.
	94	Qed.
	95
	96	Theorem IRNDD_correct3 : forall r : R, (r - 1 < IRNDD r)%R.
	97	intros r; unfold IRNDD in \|- *.
	98	generalize (archimed r); intros T; elim T; intros H1 H2; clear T.
	99	unfold Zpred, Rminus in \|- ; rewrite plus_IZR; simpl in \|- ; auto with real.
	100	Qed.
	101
	102	Hint Resolve IRNDD_correct1 IRNDD_correct2 IRNDD_correct3: real.
	103
	104
	105	Theorem IRNDD_pos : forall r : R, (0 <= r)%R -> (0 <= IRNDD r)%R.
	106	intros r H1; unfold IRNDD in \|- *.
	107	generalize (archimed r); intros T; elim T; intros H3 H2; clear T.
	108	replace 0%R with (IZR 0); auto with real; apply IZR_le.
	109	apply Zle_Zpred.
	110	apply lt_IZR; apply Rle_lt_trans with r; auto with real zarith.
	111	Qed.
	112
	113
	114	Theorem IRNDD_monotone : forall r s : R, (r <= s)%R -> (IRNDD r <= IRNDD s)%R.
	115	intros r s H.
	116	apply Rle_IZR; apply Zgt_succ_le; apply Zlt_gt; apply lt_IZR.
	117	apply Rle_lt_trans with r; auto with real.
	118	apply Rle_lt_trans with s; auto with real.
	119	Qed.
	120
	121
	122	Theorem IRNDD_eq :
	123	forall (r : R) (z : Z), (z <= r)%R -> (r < Zsucc z)%R -> IRNDD r = z.
	124	intros r z H1 H2.
	125	cut (IRNDD r - z < 1)%Z;
	126	[ intros H3 \| apply lt_IZR; rewrite <- Z_R_minus; simpl in \|- * ].
	127	cut (z - IRNDD r < 1)%Z;
	128	[ intros H4; auto with zarith
	129	\| apply lt_IZR; rewrite <- Z_R_minus; simpl in \|- * ].
	130	unfold Rminus in \|- *; apply Rle_lt_trans with (r + - IRNDD r)%R;
	131	auto with real.
	132	apply Rlt_le_trans with (r + - (r - 1))%R; auto with real; right; ring.
	133	unfold Rminus in \|- *; apply Rle_lt_trans with (r + - z)%R; auto with real.
	134	apply Rlt_le_trans with (Zsucc z + - z)%R; auto with real; right;
	135	unfold Zsucc in \|- ; rewrite plus_IZR; simpl in \|- ;
	136	ring.
	137	Qed.
	138
	139	Theorem IRNDD_projector : forall z : Z, IRNDD z = z.
	140	intros z.
	141	apply IRNDD_eq; auto with zarith real.
	142	Qed.
	143
	144
	145	(** Rounding down of a positive real *)
	146
	147	Definition RND_Min_Pos (r : R) :=
	148	match Rle_dec (firstNormalPos radix b p) r with
	149	\| left _ =>
	150	let e := IRNDD (ln r / ln radix + (- Zpred p)%Z) in
	151	Float (IRNDD (r * powerRZ radix (- e))) e
	152	\| right _ => Float (IRNDD (r * powerRZ radix (dExp b))) (- dExp b)
	153	end.
	154
	155
	156	Theorem RND_Min_Pos_bounded_aux :
	157	forall (r : R) (e : Z),
	158	(0 <= r)%R ->
	159	(- dExp b <= e)%Z ->
	160	(r < powerRZ radix (e + p))%R ->
	161	Fbounded b (Float (IRNDD (r * powerRZ radix (- e))) e).
	162	intros r e H1 H2 H3.
	163	split; auto.
	164	simpl in \|- *; rewrite pGivesBound; apply lt_IZR.
	165	rewrite Zpower_nat_Z_powerRZ; rewrite <- Faux.Rabsolu_Zabs.
	166	rewrite Rabs_right;
	167	[ idtac
	168	\| apply Rle_ge; apply IRNDD_pos; apply Rmult_le_pos; auto with real zarith ].
	169	apply Rle_lt_trans with (1 := IRNDD_correct1 (r * powerRZ radix (- e))).
	170	apply Rmult_lt_reg_l with (powerRZ radix e); auto with zarith real.
	171	rewrite Rmult_comm; rewrite Rmult_assoc.
	172	rewrite <- powerRZ_add; auto with zarith real.
	173	rewrite <- powerRZ_add; auto with zarith real.
	174	apply Rle_lt_trans with (2 := H3); ring_simplify (- e + e)%Z; simpl in \|- *; right;
	175	ring.
	176	Qed.
	177
	178
	179	Theorem RND_Min_Pos_canonic :
	180	forall r : R, (0 <= r)%R -> Fcanonic radix b (RND_Min_Pos r).
	181	intros r H1; unfold RND_Min_Pos in \|- *.
	182	generalize ln_radix_pos; intros W.
	183	case (Rle_dec (firstNormalPos radix b p) r); intros H2.
	184	cut (0 < r)%R; [ intros V \| idtac ].
	185	2: apply Rlt_le_trans with (2 := H2); rewrite firstNormalPos_eq;
	186	auto with real zarith.
	187	left; split.
	188	apply RND_Min_Pos_bounded_aux; auto.
	189	apply Zgt_succ_le; apply Zlt_gt.
	190	apply lt_IZR.
	191	apply
	192	Rle_lt_trans with (2 := IRNDD_correct2 (ln r / ln radix + (- Zpred p)%Z)).
	193	apply Rplus_le_reg_l with (Zpred p).
	194	apply Rmult_le_reg_l with (ln radix).
	195	apply ln_radix_pos.
	196	apply Rle_trans with (ln r).
	197	apply exp_le_inv.
	198	rewrite exp_ln; auto.
	199	replace (Zpred p + (- dExp b)%Z)%R with (IZR (Zpred p + - dExp b)).
	200	rewrite exp_ln_powerRZ; auto with zarith.
	201	apply Rle_trans with (2 := H2).
	202	rewrite firstNormalPos_eq; auto with real.
	203	rewrite plus_IZR; rewrite Ropp_Ropp_IZR; ring.
	204	rewrite Ropp_Ropp_IZR; right; field; auto with real.
	205	rewrite <- exp_ln_powerRZ; auto with zarith.
	206	pattern r at 1 in \|- *; rewrite <- (exp_ln r); auto.
	207	apply exp_increasing.
	208	rewrite plus_IZR.
	209	apply
	210	Rle_lt_trans with (ln radix * (ln r / ln radix + (- Zpred p)%Z - 1 + p))%R.
	211	rewrite Ropp_Ropp_IZR; unfold Zpred in \|- ; rewrite plus_IZR; simpl in \|- .
	212	repeat rewrite <- INR_IZR_INZ; right; field; auto with real.
	213	apply Rmult_lt_compat_l; auto with real.
	214	repeat rewrite <- INR_IZR_INZ.
	215	apply Rplus_lt_compat_r; auto with real.
	216	simpl in \|- ; rewrite pGivesBound; apply le_IZR; simpl in \|- .
	217	rewrite Zpower_nat_Z_powerRZ; rewrite Zabs_eq.
	218	2: apply le_IZR; rewrite Rmult_IZR; simpl in \|- *.
	219	2: apply Rmult_le_pos; auto with real zarith; apply IRNDD_pos;
	220	apply Rmult_le_pos; auto with real zarith.
	221	rewrite Rmult_IZR; pattern (Z_of_nat p) at 1 in \|- *;
	222	replace (Z_of_nat p) with (1 + Zpred p)%Z.
	223	2: unfold Zpred in \|- *; ring.
	224	rewrite powerRZ_add; auto with zarith real; simpl in \|- ; ring_simplify (radix 1)%R.
	225	apply Rmult_le_compat_l; auto with zarith real.
	226	rewrite <- inj_pred; auto with zarith.
	227	rewrite <- Zpower_nat_Z_powerRZ; apply IZR_le.
	228	apply Zgt_succ_le; apply Zlt_gt; apply lt_IZR; rewrite Ropp_Ropp_IZR.
	229	apply
	230	Rle_lt_trans
	231	with (r * powerRZ radix (- IRNDD (ln r / ln radix + - pred p)))%R.
	232	2: repeat rewrite <- INR_IZR_INZ; apply IRNDD_correct2.
	233	rewrite <- exp_ln_powerRZ; auto with zarith.
	234	rewrite Zpower_nat_Z_powerRZ; rewrite Ropp_Ropp_IZR.
	235	apply Rle_trans with (r * exp (ln radix * - (ln r / ln radix + - pred p)))%R.
	236	pattern r at 1 in \|- *; rewrite <- (exp_ln r); auto; rewrite <- exp_plus.
	237	replace (ln r + ln radix * - (ln r / ln radix + - pred p))%R with
	238	(ln radix * pred p)%R.
	239	2: field; auto with real.
	240	rewrite INR_IZR_INZ; rewrite exp_ln_powerRZ; auto with real zarith.
	241	apply Rmult_le_compat_l; auto with real.
	242	apply exp_monotone; auto with real.
	243	cut (r < powerRZ radix (Zpred p + - dExp b))%R; [ intros H3 \| idtac ].
	244	2: rewrite <- firstNormalPos_eq; auto with real.
	245	right; split.
	246	pattern (dExp b) at 2 in \|- *;
	247	replace (Z_of_N (dExp b)) with (- - dExp b)%Z; auto with zarith.
	248	apply RND_Min_Pos_bounded_aux; auto with zarith.
	249	apply Rlt_trans with (1 := H3); apply Rlt_powerRZ; auto with real zarith.
	250	rewrite Zplus_comm; auto with zarith.
	251	split; [ simpl in \|- *; auto \| idtac ].
	252	simpl in \|- *; rewrite pGivesBound; apply lt_IZR.
	253	rewrite Zpower_nat_Z_powerRZ; rewrite <- Faux.Rabsolu_Zabs.
	254	rewrite mult_IZR; rewrite Rabs_right;
	255	[ idtac
	256	\| apply Rle_ge; apply Rmult_le_pos; auto with real zarith; apply IRNDD_pos;
	257	apply Rmult_le_pos; auto with real zarith ].
	258	apply Rle_lt_trans with (radix * (r * powerRZ radix (dExp b)))%R;
	259	auto with real zarith.
	260	apply
	261	Rlt_le_trans
	262	with
	263	(radix * (powerRZ radix (Zpred p + - dExp b) * powerRZ radix (dExp b)))%R;
	264	auto with real zarith.
	265	rewrite <- powerRZ_add; auto with zarith real.
	266	pattern (IZR radix) at 1 in \|- *; replace (IZR radix) with (powerRZ radix 1);
	267	[ rewrite <- powerRZ_add \| simpl in \|- * ]; auto with zarith real;
	268	unfold Zpred in \|- *.
	269	ring_simplify (1 + (p + -1 + - dExp b + dExp b))%Z; auto with real.
	270	Qed.
	271
	272	Theorem RND_Min_Pos_Rle : forall r : R, (0 <= r)%R -> (RND_Min_Pos r <= r)%R.
	273	intros r H.
	274	unfold RND_Min_Pos in \|- *; case (Rle_dec (firstNormalPos radix b p) r);
	275	intros H2.
	276	unfold FtoRradix, FtoR in \|- ; simpl in \|- .
	277	apply
	278	Rle_trans
	279	with
	280	(r * powerRZ radix (- IRNDD (ln r / ln radix + (- Zpred p)%Z)) *
	281	powerRZ radix (IRNDD (ln r / ln radix + (- Zpred p)%Z)))%R;
	282	auto with real.
	283	rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
	284	ring_simplify
	285	(- IRNDD (ln r / ln radix + (- Zpred p)%Z) +
	286	IRNDD (ln r / ln radix + (- Zpred p)%Z))%Z; simpl in \|- *;
	287	auto with real.
	288	unfold FtoRradix, FtoR in \|- ; simpl in \|- .
	289	apply
	290	Rle_trans with (r * powerRZ radix (dExp b) * powerRZ radix (- dExp b))%R;
	291	auto with real.
	292	rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
	293	ring_simplify (dExp b + - dExp b)%Z; simpl in \|- *; auto with real.
	294	Qed.
	295
	296
	297
	298	Theorem RND_Min_Pos_monotone :
	299	forall r s : R,
	300	(0 <= r)%R -> (r <= s)%R -> (RND_Min_Pos r <= RND_Min_Pos s)%R.
	301	intros r s V1 H.
	302	cut (0 <= s)%R;
	303	[ intros V2 \| apply Rle_trans with (1 := V1); auto with real ].
	304	rewrite <-
	305	FPredSuc
	306	with
	307	(x := RND_Min_Pos s)
	308	(precision := p)
	309	(b := b)
	310	(radix := radix); auto with arith.
	311	2: apply RND_Min_Pos_canonic; auto.
	312	unfold FtoRradix in \|- *; apply FPredProp; auto with arith;
	313	fold FtoRradix in \|- *.
	314	apply RND_Min_Pos_canonic; auto.
	315	apply FSuccCanonic; auto with arith; apply RND_Min_Pos_canonic; auto.
	316	apply Rle_lt_trans with r; auto with real.
	317	apply RND_Min_Pos_Rle; auto.
	318	apply Rle_lt_trans with (1 := H).
	319	replace (FtoRradix (FSucc b radix p (RND_Min_Pos s))) with
	320	(RND_Min_Pos s + powerRZ radix (Fexp (RND_Min_Pos s)))%R.
	321	unfold RND_Min_Pos in \|- *; case (Rle_dec (firstNormalPos radix b p) s);
	322	intros H1.
	323	unfold FtoRradix, FtoR in \|- ; simpl in \|- .
	324	apply
	325	Rle_lt_trans
	326	with
	327	((s * powerRZ radix (- IRNDD (ln s / ln radix + (- Zpred p)%Z)) - 1) *
	328	powerRZ radix (IRNDD (ln s / ln radix + (- Zpred p)%Z)) +
	329	powerRZ radix (IRNDD (ln s / ln radix + (- Zpred p)%Z)))%R;
	330	auto with real.
	331	right; ring_simplify.
	332	rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with zarith real.
	333	ring_simplify
	334	(-IRNDD (ln s / ln radix + (- Zpred p)%Z) +
	335	IRNDD (ln s / ln radix + (- Zpred p)%Z))%Z;
	336	simpl; ring.
	337	unfold FtoRradix, FtoR in \|- ; simpl in \|- .
	338	apply
	339	Rle_lt_trans
	340	with
	341	((s * powerRZ radix (dExp b) - 1) * powerRZ radix (- dExp b) +
	342	powerRZ radix (- dExp b))%R; auto with real.
	343	right; ring_simplify.
	344	rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with zarith real.
	345	ring_simplify (dExp b + -dExp b)%Z; simpl in \|- *; ring.
	346	replace (powerRZ radix (Fexp (RND_Min_Pos s))) with
	347	(FtoR radix (Float 1%nat (Fexp (RND_Min_Pos s))));
	348	[ idtac \| unfold FtoR in \|- ; simpl in \|- ; ring ].
	349	rewrite <- FSuccDiff1 with b radix p (RND_Min_Pos s); auto with arith.
	350	rewrite Fminus_correct; auto with zarith; fold FtoRradix in \|- *; ring.
	351	cut (- nNormMin radix p < Fnum (RND_Min_Pos s))%Z; auto with zarith.
	352	apply Zlt_le_trans with 0%Z.
	353	replace 0%Z with (- (0))%Z; unfold nNormMin in \|- *; auto with arith zarith.
	354	apply le_IZR; unfold RND_Min_Pos in \|- *;
	355	case (Rle_dec (firstNormalPos radix b p) s); intros H1;
	356	simpl in \|- *; apply IRNDD_pos; apply Rmult_le_pos;
	357	auto with real zarith.
	358	Qed.
	359
	360
	361	Theorem RND_Min_Pos_projector :
	362	forall f : float,
	363	(0 <= f)%R -> Fcanonic radix b f -> FtoRradix (RND_Min_Pos f) = f.
	364	intros f H1 H2.
	365	unfold RND_Min_Pos in \|- *; case (Rle_dec (firstNormalPos radix b p) f);
	366	intros H3.
	367	replace (IRNDD (ln f / ln radix + (- Zpred p)%Z)) with (Fexp f).
	368	replace (f * powerRZ radix (- Fexp f))%R with (IZR (Fnum f)).
	369	rewrite IRNDD_projector; unfold FtoRradix, FtoR in \|- ; simpl in \|- ; ring.
	370	unfold FtoRradix, FtoR in \|- ; simpl in \|- .
	371	rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
	372	ring_simplify (Fexp f + - Fexp f)%Z; simpl in \|- *; ring.
	373	generalize ln_radix_pos; intros V1.
	374	cut (0 < Fnum f)%R; [ intros V2 \| idtac ].
	375	apply sym_eq; apply IRNDD_eq.
	376	unfold FtoRradix, FtoR in \|- ; simpl in \|- .
	377	rewrite ln_mult; auto with real zarith.
	378	unfold Rdiv in \|- *; rewrite Rmult_plus_distr_r.
	379	apply Rle_trans with (Zpred p + Fexp f + (- Zpred p)%Z)%R;
	380	[ rewrite Ropp_Ropp_IZR; right; ring \| idtac ].
	381	apply Rplus_le_compat_r; apply Rplus_le_compat.
	382	apply Rmult_le_reg_l with (ln radix); [ auto with real \| idtac ].
	383	apply Rle_trans with (ln (Fnum f)); [ idtac \| right; field; auto with real ].
	384	apply exp_le_inv.
	385	rewrite exp_ln; auto.
	386	rewrite exp_ln_powerRZ; auto with zarith.
	387	case H2; intros T; elim T; intros C1 C2.
	388	apply Rmult_le_reg_l with radix; auto with real zarith.
	389	apply Rle_trans with (IZR (Zpos (vNum b)));
	390	[ right; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ \| idtac ].
	391	pattern (Z_of_nat p) at 2 in \|- *; replace (Z_of_nat p) with (1 + Zpred p)%Z;
	392	[ rewrite powerRZ_add; auto with real zarith; simpl in \|- *; ring
	393	\| unfold Zpred in \|- *; ring ].
	394	rewrite <- (Rabs_right (radix * Fnum f)); auto with real zarith.
	395	rewrite <- mult_IZR; rewrite Faux.Rabsolu_Zabs; auto with real zarith.
	396	apply Rle_ge; apply Rmult_le_pos; auto with real zarith.
	397	Contradict H3; apply Rlt_not_le; unfold FtoRradix in \|- *;
	398	apply FsubnormalLtFirstNormalPos; auto with zarith.
	399	apply Rmult_le_reg_l with (ln radix); [ auto with real \| idtac ].
	400	apply Rle_trans with (ln (powerRZ radix (Fexp f)));
	401	[ idtac \| right; field; auto with real ].
	402	rewrite <- exp_ln_powerRZ; auto with zarith.
	403	rewrite ln_exp; auto with real.
	404	unfold FtoRradix, FtoR in \|- ; simpl in \|- .
	405	rewrite ln_mult; auto with real zarith.
	406	rewrite <- exp_ln_powerRZ; auto with zarith.
	407	rewrite ln_exp; auto with real.
	408	unfold Rdiv in \|- *; rewrite Rmult_plus_distr_r.
	409	apply Rlt_le_trans with (p + Fexp f + (- Zpred p)%Z)%R.
	410	2: rewrite Ropp_Ropp_IZR; unfold Zsucc, Zpred in \|- *;
	411	repeat rewrite plus_IZR; repeat rewrite <- INR_IZR_INZ;
	412	simpl in \|- *; right; ring.
	413	replace (ln radix * Fexp f * / ln radix)%R with (IZR (Fexp f));
	414	[ idtac \| field; auto with real ].
	415	apply Rplus_lt_compat_r; apply Rplus_lt_compat_r.
	416	apply Rmult_lt_reg_l with (ln radix); [ auto with real \| idtac ].
	417	apply Rle_lt_trans with (ln (Fnum f));
	418	[ right; field; auto with real \| idtac ].
	419	apply exp_lt_inv.
	420	rewrite exp_ln; auto.
	421	rewrite INR_IZR_INZ; rewrite exp_ln_powerRZ; auto with zarith.
	422	apply Rlt_le_trans with (IZR (Zpos (vNum b))).
	423	rewrite <- (Rabs_right (IZR (Fnum f))); auto with real.
	424	rewrite Faux.Rabsolu_Zabs; apply Rlt_IZR; cut (Fbounded b f);
	425	auto with real zarith float.
	426	apply FcanonicBound with radix; auto.
	427	apply Rle_ge; auto with real.
	428	right; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ; auto with real zarith.
	429	replace 0%R with (IZR 0); auto with real zarith; apply Rlt_IZR.
	430	apply LtR0Fnum with radix; auto with zarith; fold FtoRradix in \|- *.
	431	apply Rlt_le_trans with (2 := H3); rewrite firstNormalPos_eq;
	432	auto with real zarith.
	433	case H2; intros T; elim T; intros C1 C2.
	434	absurd (firstNormalPos radix b p <= f)%R; auto with real.
	435	unfold FtoRradix in \|- *; apply FnormalLtFirstNormalPos; auto with arith.
	436	elim C2; intros C3 C4.
	437	replace (f * powerRZ radix (dExp b))%R with (IZR (Fnum f)).
	438	rewrite IRNDD_projector; rewrite <- C3; unfold FtoRradix, FtoR in \|- *;
	439	simpl in \|- *; ring.
	440	unfold FtoRradix, FtoR in \|- *; rewrite C3.
	441	rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.
	442	ring_simplify (- dExp b + dExp b)%Z; simpl in \|- *; ring.
	443	Qed.
	444
	445	Theorem RND_Min_Pos_correct :
	446	forall r : R, (0 <= r)%R -> isMin b radix r (RND_Min_Pos r).
	447	intros r H1.
	448	split.
	449	apply FcanonicBound with radix; apply RND_Min_Pos_canonic; auto.
	450	split.
	451	apply RND_Min_Pos_Rle; auto.
	452	fold FtoRradix in \|- *; intros f H2 H3.
	453	case (Rle_or_lt 0 f); intros H4.
	454	unfold FtoRradix in \|- *; rewrite <- FnormalizeCorrect with radix b p f; auto;
	455	fold FtoRradix in \|- *.
	456	rewrite <- RND_Min_Pos_projector.
	457	apply RND_Min_Pos_monotone; unfold FtoRradix in \|- *;
	458	rewrite FnormalizeCorrect; auto.
	459	unfold FtoRradix in \|- *; rewrite FnormalizeCorrect; auto.
	460	apply FnormalizeCanonic; auto with arith.
	461	apply Rle_trans with 0%R; auto with real.
	462	unfold RND_Min_Pos in \|- *; case (Rle_dec (firstNormalPos radix b p) r);
	463	intros H5; unfold FtoRradix, FtoR in \|- ; simpl in \|- ;
	464	apply Rmult_le_pos; auto with real zarith; apply IRNDD_pos;
	465	apply Rmult_le_pos; auto with real zarith.
	466	Qed.
	467
	468
	469	(** Easily deduced, the rounding up of a positive real *)
	470
	471	Definition RND_Max_Pos (r : R) :=
	472	match Req_EM_T r (RND_Min_Pos r) with
	473	\| left _ => RND_Min_Pos r
	474	\| right _ => FSucc b radix p (RND_Min_Pos r)
	475	end.
	476
	477	Theorem RND_Max_Pos_canonic :
	478	forall r : R, (0 <= r)%R -> Fcanonic radix b (RND_Max_Pos r).
	479	intros r H; unfold RND_Max_Pos in \|- *.
	480	case (Req_EM_T r (RND_Min_Pos r)); intros H1.
	481	apply RND_Min_Pos_canonic; auto.
	482	apply FSuccCanonic; auto with arith; apply RND_Min_Pos_canonic; auto.
	483	Qed.
	484
	485	Theorem RND_Max_Pos_Rle : forall r : R, (0 <= r)%R -> (r <= RND_Max_Pos r)%R.
	486	intros r H.
	487	unfold RND_Max_Pos in \|- *; case (Req_EM_T r (RND_Min_Pos r)); intros H1.
	488	rewrite <- H1; auto with real.
	489	case (Rle_or_lt r (FSucc b radix p (RND_Min_Pos r))); auto; intros H2.
	490	generalize (RND_Min_Pos_correct r H); intros T; elim T; intros H3 T1; elim T1;
	491	intros H4 H5; clear T T1.
	492	absurd (FSucc b radix p (RND_Min_Pos r) <= RND_Min_Pos r)%R;
	493	auto with float zarith real.
	494	apply Rlt_not_le; auto with float zarith.
	495	unfold FtoRradix in \|- *; apply FSuccLt; auto with arith.
	496	Qed.
	497
	498	Theorem RND_Max_Pos_correct :
	499	forall r : R, (0 <= r)%R -> isMax b radix r (RND_Max_Pos r).
	500	intros r H.
	501	split.
	502	apply FcanonicBound with radix; apply RND_Max_Pos_canonic; auto.
	503	split.
	504	apply RND_Max_Pos_Rle; auto.
	505	unfold RND_Max_Pos in \|- *; case (Req_EM_T r (RND_Min_Pos r)); intros H1.
	506	fold FtoRradix in \|- *; intros f H2 H3; rewrite <- H1; auto with real.
	507	fold FtoRradix in \|- *; intros f H2 H3.
	508	case H3; intros V.
	509	case (Rle_or_lt (FSucc b radix p (RND_Min_Pos r)) f); auto; intros H4.
	510	absurd (f < f)%R; auto with real.
	511	apply Rle_lt_trans with (RND_Min_Pos r).
	512	rewrite <- FPredSuc with b radix p (RND_Min_Pos r); auto with arith.
	513	2: apply RND_Min_Pos_canonic; auto.
	514	unfold FtoRradix in \|- *; rewrite <- FnormalizeCorrect with radix b p f; auto.
	515	apply FPredProp; auto with arith float zarith.
	516	apply FSuccCanonic; auto with arith; apply RND_Min_Pos_canonic; auto.
	517	rewrite FnormalizeCorrect; auto with real.
	518	apply Rle_lt_trans with (2 := V).
	519	apply RND_Min_Pos_Rle; auto.
	520	Contradict H1.
	521	rewrite V; unfold FtoRradix in \|- *;
	522	rewrite <- FnormalizeCorrect with radix b p f; auto.
	523	fold FtoRradix in \|- *; apply sym_eq; apply RND_Min_Pos_projector;
	524	auto with zarith float.
	525	unfold FtoRradix in \|- ; rewrite FnormalizeCorrect; fold FtoRradix in \|- ;
	526	auto with real.
	527	apply Rle_trans with r; auto with real.
	528	Qed.
	529
	530	(** Roundings up and down of any real *)
	531
	532	Definition RND_Min (r : R) :=
	533	match Rle_dec 0 r with
	534	\| left _ => RND_Min_Pos r
	535	\| right _ => Fopp (RND_Max_Pos (- r))
	536	end.
	537
	538	Theorem RND_Min_canonic : forall r : R, Fcanonic radix b (RND_Min r).
	539	intros r.
	540	unfold RND_Min in \|- *; case (Rle_dec 0 r); intros H.
	541	apply RND_Min_Pos_canonic; auto.
	542	apply FcanonicFopp; apply RND_Max_Pos_canonic; auto with real.
	543	Qed.
	544
	545	Theorem RND_Min_correct : forall r : R, isMin b radix r (RND_Min r).
	546	intros r.
	547	unfold RND_Min in \|- *; case (Rle_dec 0 r); intros H.
	548	apply RND_Min_Pos_correct; auto.
	549	pattern r at 1 in \|- *; rewrite <- (Ropp_involutive r).
	550	apply MaxOppMin; apply RND_Max_Pos_correct; auto with real.
	551	Qed.
	552
	553	Definition RND_Max (r : R) :=
	554	match Rle_dec 0 r with
	555	\| left _ => RND_Max_Pos r
	556	\| right _ => Fopp (RND_Min_Pos (- r))
	557	end.
	558
	559	Theorem RND_Max_canonic : forall r : R, Fcanonic radix b (RND_Max r).
	560	intros r.
	561	unfold RND_Max in \|- *; case (Rle_dec 0 r); intros H.
	562	apply RND_Max_Pos_canonic; auto.
	563	apply FcanonicFopp; apply RND_Min_Pos_canonic; auto with real.
	564	Qed.
	565
	566	Theorem RND_Max_correct : forall r : R, isMax b radix r (RND_Max r).
	567	intros r.
	568	unfold RND_Max in \|- *; case (Rle_dec 0 r); intros H.
	569	apply RND_Max_Pos_correct; auto.
	570	pattern r at 1 in \|- *; rewrite <- (Ropp_involutive r).
	571	apply MinOppMax; apply RND_Min_Pos_correct; auto with real.
	572	Qed.
	573
	574	Definition RND_Zero (r : R) :=
	575	match Rle_dec 0 r with
	576	\| left _ => RND_Min r
	577	\| right _ => RND_Max r
	578	end.
	579
	580	Theorem RND_Zero_canonic : forall r : R, Fcanonic radix b (RND_Zero r).
	581	intros r.
	582	unfold RND_Zero in \|- *; case (Rle_dec 0 r); intros H.
	583	apply RND_Min_canonic; auto.
	584	apply RND_Max_canonic; auto.
	585	Qed.
	586
	587	Theorem RND_Zero_correct : forall r : R, ToZeroP b radix r (RND_Zero r).
	588	intros r.
	589	unfold ToZeroP, RND_Zero.
	590	case (Rle_dec 0 r); intros H.
	591	left; split; auto with real; apply RND_Min_correct; auto with real.
	592	right; split; auto with real;apply RND_Max_correct; auto with real.
	593	Qed.
	594
	595
	596	(** Rounding to the nearest of any real
	597	First, ClosestUp (when equality, the biggest is returned)
	598	Then, EvenClosest (when equality, the even is returned)
	599	*)
	600
	601	Definition RND_ClosestUp (r : R) :=
	602	match Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) with
	603	\| left _ => RND_Max r
	604	\| right _ => RND_Min r
	605	end.
	606
	607
	608	Theorem RND_ClosestUp_canonic :
	609	forall r : R, Fcanonic radix b (RND_ClosestUp r).
	610	intros r.
	611	unfold RND_ClosestUp in \|- *;
	612	case (Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)));
	613	intros H; [ apply RND_Max_canonic \| apply RND_Min_canonic ].
	614	Qed.
	615
	616	Theorem RND_ClosestUp_correct :
	617	forall r : R, Closest b radix r (RND_ClosestUp r).
	618	intros r.
	619	cut (RND_Min r <= r)%R; [ intros V1 \| idtac ].
	620	2: generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
	621	intros T3 T4; auto with real.
	622	cut (r <= RND_Max r)%R; [ intros V2 \| idtac ].
	623	2: generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
	624	intros T3 T4; auto with real.
	625	cut (forall v w : R, (v <= w)%R -> (0 <= w - v)%R); [ intros V3 \| idtac ].
	626	2: intros v w H; apply Rplus_le_reg_l with v; ring_simplify (v + (w - v))%R;
	627	ring_simplify (v + 0)%R; auto with real.
	628	cut (forall v w : R, (v <= w)%R -> (v - w <= 0)%R); [ intros V4 \| idtac ].
	629	2: intros v w H; apply Rplus_le_reg_l with w; ring_simplify; auto with real.
	630	unfold RND_ClosestUp in \|- *;
	631	case (Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)));
	632	intros H; split;
	633	[ apply FcanonicBound with radix; apply RND_Max_canonic
	634	\| intros f H1; fold FtoRradix in \|- *
	635	\| apply FcanonicBound with radix; apply RND_Min_canonic
	636	\| intros f H1; fold FtoRradix in \|- * ].
	637	rewrite Rabs_right in H; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	638	rewrite Faux.Rabsolu_left1 in H; [ idtac \| apply V4; auto with real ].
	639	rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	640	case (Rle_or_lt f r); intros H2.
	641	rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
	642	apply Rle_trans with (1 := H); apply Ropp_le_contravar; unfold Rminus in \|- *;
	643	apply Rplus_le_compat_r.
	644	generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
	645	intros T3 T4; auto with real.
	646	rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	647	unfold Rminus in \|- *; apply Rplus_le_compat_r.
	648	generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
	649	intros T3 T4; auto with real.
	650	cut (Rabs (RND_Min r - r) < Rabs (RND_Max r - r))%R; auto with real;
	651	intros H'.
	652	rewrite Faux.Rabsolu_left1 in H'; [ idtac \| apply V4; auto with real ].
	653	rewrite Rabs_right in H'; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	654	rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
	655	case (Rle_or_lt f r); intros H2.
	656	rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
	657	apply Ropp_le_contravar; unfold Rminus in \|- *; apply Rplus_le_compat_r.
	658	generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
	659	intros T3 T4; auto with real.
	660	rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	661	apply Rle_trans with (RND_Max r - r)%R; auto with real; unfold Rminus in \|- *;
	662	apply Rplus_le_compat_r.
	663	generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
	664	intros T3 T4; auto with real.
	665	Qed.
	666
	667
	668
	669	Definition RND_EvenClosest (r : R) :=
	670	match Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) with
	671	\| left H =>
	672	match
	673	Rle_lt_or_eq_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) H
	674	with
	675	\| left _ => RND_Max r
	676	\| right _ =>
	677	match OddEvenDec (Fnum (RND_Min r)) with
	678	\| left _ => RND_Max r
	679	\| right _ => RND_Min r
	680	end
	681	end
	682	\| right _ => RND_Min r
	683	end.
	684
	685
	686	Theorem RND_EvenClosest_canonic :
	687	forall r : R, Fcanonic radix b (RND_EvenClosest r).
	688	intros r; unfold RND_EvenClosest in \|- *.
	689	case (Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r))); intros H1.
	690	case (Rle_lt_or_eq_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) H1);
	691	intros H2.
	692	apply RND_Max_canonic.
	693	case (OddEvenDec (Fnum (RND_Min r))); intros H3.
	694	apply RND_Max_canonic.
	695	apply RND_Min_canonic.
	696	apply RND_Min_canonic.
	697	Qed.
	698
	699	Theorem RND_EvenClosest_correct :
	700	forall r : R, EvenClosest b radix p r (RND_EvenClosest r).
	701	intros r.
	702	cut (RND_Min r <= r)%R; [ intros V1 \| idtac ].
	703	2: generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
	704	intros T3 T4; auto with real.
	705	cut (r <= RND_Max r)%R; [ intros V2 \| idtac ].
	706	2: generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
	707	intros T3 T4; auto with real.
	708	cut (forall v w : R, (v <= w)%R -> (0 <= w - v)%R); [ intros V3 \| idtac ].
	709	2: intros v w H; apply Rplus_le_reg_l with v; ring_simplify; auto with real.
	710	cut (forall v w : R, (v <= w)%R -> (v - w <= 0)%R); [ intros V4 \| idtac ].
	711	2: intros v w H; apply Rplus_le_reg_l with w; ring_simplify; auto with real.
	712	unfold RND_EvenClosest in \|- *;
	713	case (Rle_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)));
	714	intros H1.
	715	case (Rle_lt_or_eq_dec (Rabs (RND_Max r - r)) (Rabs (RND_Min r - r)) H1);
	716	intros H2.
	717	split.
	718	split.
	719	apply FcanonicBound with radix; apply RND_Max_canonic.
	720	intros f H3; fold FtoRradix in \|- *.
	721	rewrite Rabs_right in H1; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	722	rewrite Faux.Rabsolu_left1 in H1; [ idtac \| apply V4; auto with real ].
	723	rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	724	case (Rle_or_lt f r); intros H4.
	725	rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
	726	apply Rle_trans with (1 := H1); apply Ropp_le_contravar;
	727	unfold Rminus in \|- *; apply Rplus_le_compat_r.
	728	generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
	729	intros T3 T4; auto with real.
	730	rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	731	unfold Rminus in \|- *; apply Rplus_le_compat_r.
	732	generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
	733	intros T3 T4; auto with real.
	734	right; intros q H3.
	735	generalize (ClosestMinOrMax b radix); unfold MinOrMaxP in \|- *; intros T.
	736	case (T r q); auto; intros H4; clear T.
	737	Contradict H2; apply Rle_not_lt.
	738	replace (FtoRradix (RND_Min r)) with (FtoRradix q).
	739	elim H3; intros T1 T2; unfold FtoRradix in \|- *; apply T2.
	740	apply FcanonicBound with radix; apply RND_Max_canonic.
	741	generalize (MinUniqueP b radix); unfold UniqueP in \|- *; intros T;
	742	apply T with r; auto.
	743	apply RND_Min_correct.
	744	generalize (MaxUniqueP b radix); unfold UniqueP in \|- *; intros T;
	745	apply T with r; auto.
	746	apply RND_Max_correct.
	747	case (OddEvenDec (Fnum (RND_Min r))); intros H3.
	748	split.
	749	split.
	750	apply FcanonicBound with radix; apply RND_Max_canonic.
	751	intros f H4; fold FtoRradix in \|- *.
	752	rewrite Rabs_right in H1; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	753	rewrite Faux.Rabsolu_left1 in H1; [ idtac \| apply V4; auto with real ].
	754	rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	755	case (Rle_or_lt f r); intros H5.
	756	rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
	757	apply Rle_trans with (1 := H1); apply Ropp_le_contravar;
	758	unfold Rminus in \|- *; apply Rplus_le_compat_r.
	759	generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
	760	intros T3 T4; auto with real.
	761	rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	762	unfold Rminus in \|- *; apply Rplus_le_compat_r.
	763	generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
	764	intros T3 T4; auto with real.
	765	case (Req_EM_T (RND_Max r) (RND_Min r)); intros W.
	766	right; intros q H4.
	767	generalize (ClosestMinOrMax b radix); unfold MinOrMaxP in \|- *; intros T.
	768	case (T r q); auto; intros H5; clear T.
	769	fold FtoRradix in \|- *; rewrite W; generalize (MinUniqueP b radix);
	770	unfold UniqueP in \|- *; intros T; apply T with r;
	771	auto.
	772	apply RND_Min_correct.
	773	generalize (MaxUniqueP b radix); unfold UniqueP in \|- *; intros T;
	774	apply T with r; auto.
	775	apply RND_Max_correct.
	776	left; unfold FNeven in \|- *.
	777	rewrite FcanonicFnormalizeEq; auto with arith;
	778	[ idtac \| apply RND_Max_canonic ].
	779	replace (RND_Max r) with (FSucc b radix p (RND_Min r)).
	780	apply FoddSuc; auto.
	781	unfold RND_Max, RND_Min in \|- *; case (Rle_dec 0 r); intros W1.
	782	unfold RND_Max_Pos in \|- *.
	783	case (Req_EM_T r (RND_Min_Pos r)); intros W2; auto.
	784	Contradict W.
	785	pattern r at 1 in \|- *; rewrite W2.
	786	apply sym_eq; unfold FtoRradix in \|- *;
	787	apply RoundedModeProjectorIdemEq with b p (isMax b radix);
	788	auto.
	789	apply MaxRoundedModeP with p; auto.
	790	apply FcanonicBound with radix; apply RND_Min_canonic.
	791	replace (FtoR radix (RND_Min r)) with (FtoR radix (RND_Min_Pos r));
	792	[ fold FtoRradix in \|- *; rewrite <- W2; apply RND_Max_correct \| idtac ].
	793	fold FtoRradix in \|- ; unfold RND_Min in \|- ; auto with real.
	794	case (Rle_dec 0 r); auto with real; intros W3; Contradict W1; auto with real.
	795	unfold RND_Max_Pos in \|- *.
	796	case (Req_EM_T (- r) (RND_Min_Pos (- r))); intros W2; auto.
	797	Contradict W.
	798	cut (r = FtoRradix (Fopp (RND_Min_Pos (- r)))); [ intros W3 \| idtac ].
	799	pattern r at 1 in \|- *; rewrite W3.
	800	apply sym_eq; unfold FtoRradix in \|- *;
	801	apply RoundedModeProjectorIdemEq with b p (isMax b radix);
	802	auto.
	803	apply MaxRoundedModeP with p; auto.
	804	apply FcanonicBound with radix; apply RND_Min_canonic.
	805	replace (FtoR radix (RND_Min r)) with (- FtoR radix (RND_Min_Pos (- r)))%R;
	806	[ fold FtoRradix in \|- *; rewrite <- W3 \| idtac ].
	807	rewrite <- W2; rewrite Ropp_involutive; apply RND_Max_correct.
	808	fold FtoRradix in \|- ; unfold RND_Min in \|- ; auto with real.
	809	case (Rle_dec 0 r).
	810	intros W4; Contradict W1; auto with real.
	811	intros W4; unfold RND_Max_Pos in \|- *;
	812	case (Req_EM_T (- r) (RND_Min_Pos (- r))); intros W5.
	813	unfold FtoRradix in \|- *; rewrite Fopp_correct; ring.
	814	Contradict W2; auto with real.
	815	unfold FtoRradix in \|- ; rewrite Fopp_correct; fold FtoRradix in \|- ;
	816	rewrite <- W2; ring.
	817	pattern (RND_Min_Pos (- r)) at 1 in \|- *;
	818	rewrite <- (Fopp_Fopp (RND_Min_Pos (- r))).
	819	rewrite <- FPredFopFSucc; auto with arith.
	820	apply FSucPred; auto with arith.
	821	apply FcanonicFopp; apply RND_Min_Pos_canonic; auto with real.
	822	split.
	823	split.
	824	apply FcanonicBound with radix; apply RND_Min_canonic.
	825	intros f H4; fold FtoRradix in \|- *.
	826	rewrite Rabs_right in H1; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	827	rewrite Faux.Rabsolu_left1 in H1; [ idtac \| apply V4; auto with real ].
	828	case (Rle_or_lt f r); intros H5.
	829	rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
	830	rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
	831	apply Ropp_le_contravar; unfold Rminus in \|- *; apply Rplus_le_compat_r.
	832	generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
	833	intros T3 T4; auto with real.
	834	rewrite <- H2.
	835	rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	836	rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	837	unfold Rminus in \|- *; apply Rplus_le_compat_r.
	838	generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
	839	intros T3 T4; auto with real.
	840	left; unfold FNeven in \|- *.
	841	rewrite FcanonicFnormalizeEq; auto with arith; apply RND_Min_canonic.
	842	cut (Rabs (RND_Min r - r) < Rabs (RND_Max r - r))%R; auto with real;
	843	intros H'.
	844	cut (Rabs (RND_Min r - r) < Rabs (RND_Max r - r))%R; auto with real;
	845	intros H''.
	846	rewrite Faux.Rabsolu_left1 in H'; [ idtac \| apply V4; auto with real ].
	847	rewrite Rabs_right in H'; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	848	split.
	849	split.
	850	apply FcanonicBound with radix; apply RND_Min_canonic.
	851	intros f W1.
	852	rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
	853	case (Rle_or_lt f r); intros H2.
	854	rewrite Faux.Rabsolu_left1; [ idtac \| apply V4; auto with real ].
	855	apply Ropp_le_contravar; unfold Rminus in \|- *; apply Rplus_le_compat_r.
	856	generalize (RND_Min_correct r); intros T; elim T; intros T1 T2; elim T2;
	857	intros T3 T4; auto with real.
	858	rewrite Rabs_right; [ idtac \| apply Rle_ge; apply V3; auto with real ].
	859	apply Rle_trans with (RND_Max r - r)%R; auto with real; unfold Rminus in \|- *;
	860	apply Rplus_le_compat_r.
	861	generalize (RND_Max_correct r); intros T; elim T; intros T1 T2; elim T2;
	862	intros T3 T4; auto with real.
	863	right; intros q H3.
	864	generalize (ClosestMinOrMax b radix); unfold MinOrMaxP in \|- *; intros T.
	865	case (T r q); auto; intros H4; clear T.
	866	generalize (MinUniqueP b radix); unfold UniqueP in \|- *; intros T;
	867	apply T with r; auto.
	868	apply RND_Min_correct.
	869	Contradict H''; apply Rle_not_lt.
	870	replace (FtoRradix (RND_Max r)) with (FtoRradix q).
	871	elim H3; intros T1 T2; unfold FtoRradix in \|- *; apply T2.
	872	apply FcanonicBound with radix; apply RND_Min_canonic.
	873	generalize (MaxUniqueP b radix); unfold UniqueP in \|- *; intros T;
	874	apply T with r; auto.
	875	apply RND_Max_correct.
	876	Qed.
	877
	878
	879
	880
	881
	882
	883	End Round.

-5

Zdivides.v less more

274	274	case (ZquotientProp m n); auto; intros z (H0, (H1, H2)).
275	275	case (Zle_or_lt (Zabs q) (Zabs (Zquotient m n))); intros Zl1; auto with arith.
276	276	case (Zle_lt_or_eq _ _ Zl1); clear Zl1; intros Zl1; auto with arith.
277		Contradict H1; apply Zlt_not_le.
	277	absurd ((Zabs (Zquotient m n * n) <= Zabs m)%Z); trivial.
	278	apply Zlt_not_le.
278	279	pattern m at 1 in \|- *; rewrite H'0.
279	280	apply Zle_lt_trans with (Zabs (q * n) + Zabs r)%Z; auto with zarith.
280	281	apply Zlt_le_trans with (Zabs (q * n) + Zabs n)%Z; auto with zarith.

304	305	apply Zle_lt_trans with (Zabs r + Zabs z)%Z; auto with zarith.
305	306	rewrite <- (Zabs_eq (1 + 1)); auto with zarith.
306	307	rewrite <- Zabs_Zmult; apply f_equal with (f := Zabs); auto with zarith.
307		Contradict H'1; apply Zlt_not_le.
	308	absurd ((Zabs (q * n) <= Zabs m)%Z); trivial.
	309	apply Zlt_not_le.
308	310	pattern m at 1 in \|- *; rewrite H0.
309	311	apply Zle_lt_trans with (Zabs (Zquotient m n * n) + Zabs z)%Z;
310	312	auto with zarith.

340	342	intros H'1.
341	343	case (ZquotientProp m q); auto; intros r1 (H'2, (H'3, H'4)); auto with zarith.
342	344	case (ZquotientProp n q); auto; intros r2 (H'5, (H'6, H'7)); auto with zarith.
343		Contradict H'6.
	345	absurd ((Zabs (Zquotient n q * q) <= Zabs n)%Z); trivial.
344	346	apply Zlt_not_le.
345	347	apply Zlt_le_trans with (1 := Z0).
346	348	rewrite H'2.

352	354	[ idtac \| unfold Zsucc in \|- *; ring ].
353	355	cut (0 < Zabs q)%Z; auto with zarith.
354	356	case (Zle_lt_or_eq 0 (Zabs q)); auto with zarith.
355		intros H'6; case Z1; auto.
356		generalize H'6; case q; simpl in \|- *; auto; intros; discriminate.
	357	intros H'8; case Z1; auto.
	358	generalize H'8; case q; simpl in \|- *; auto; intros; discriminate.
357	359	case (Zabs_eq_case _ _ Z0); intros Z1; rewrite Z1; auto with zarith.
358	360	rewrite ZquotientZopp; rewrite Zabs_Zopp; auto with zarith.
359	361	Qed.