proposition: Lemma argument_reduction : forall x : R, generic_format radix2 (FLT_exp (-1074) 53) x -> -746 <= x <= 710 -> let k := nearbyint (mul x InvLog2) in let tf := sub (sub x (mul k Log2h)) (mul k Log2l) in let te := x - k * ln 2 in Rabs tf <= 355 / 1024 /\ Rabs (tf - te) <= 65537 * pow2 (-71).
proof: Proof. Proof with auto with typeclass_instances. intros x Fx Bx k tf te. assert (Rabs x <= 5/16 \/ 5/16 <= Rabs x <= 746) as [Bx'|Bx'] by gappa. - assert (k = 0). clear -Bx'. refine (let H := _ in Rle_antisym _ _ (proj2 H) (proj1 H)). unfold k, mul, nearbyint, InvLog2, Log2h ; gappa. unfold tf, te, mul, sub. rewrite H. rewrite 2!Rmult_0_l. rewrite round_0... rewrite Rmult_0_l. rewrite 2!Rminus_0_r. rewrite 2!round_generic with (2 := Fx)... gappa. - assert (Hl: - 1 * pow2 (-102) <= Log2l - (ln 2 - Log2h) <= 0). unfold Log2l, Log2h ; interval with (i_prec 110). assert (Ax: x = x * InvLog2 * (1 / InvLog2)). field. unfold InvLog2 ; interval. unfold te. replace (x - k * ln 2) with (x - k * Log2h - k * (ln 2 - Log2h)) by ring. revert Hl Ax. unfold tf, te, k, sub, mul, nearbyint, InvLog2, Log2h, Log2l ; gappa. Qed.
imports: Coq(Reals) Flocq(Core) Gappa(Gappa_tactic) Interval(Tactic)