proposition: Lemma exp_consts_correct : forall i, (0 <= i <= 63)%Z -> Rabs (SF2R radix2 (Prim2SF consts.[of_Z i]) - Rtrigo_def.exp (IZR i * (Rpower.ln 2 / 64))) <= Rpow2 (-53).
proof: Proof. intros i Hi_. assert (Hi : snd (N.iter 64 (fun '(n, P) => (Z.succ n, i = n \/ P)) (0%Z, False))) by (cbn; lia). clear Hi_. cbn in Hi. repeat destruct Hi as [-> | Hi]. 65: easy. all: cbn -[bpow]; unfold F2R; cbn -[bpow]. all: interval with (i_prec 61). Qed.
imports: Coq(Reals Psatz PrimInt63 Uint63 Sint63 PArray Floats) Flocq(Core PrimFloat BinarySingleNaN) Missing.Flocq Xreal Basic Sig Interval Float Float_full Specific_bigint Specific_ops Primitive_ops Lang_expr Lang_tac Interval_helper