Library Interval.Interval.Float_full
This file is part of the Coq.Interval library for proving bounds of
real-valued expressions in Coq: https://coqinterval.gitlabpages.inria.fr/
Copyright (C) 2007-2016, Inria
This library is governed by the CeCILL-C license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/or redistribute the library under the terms of the CeCILL-C
license as circulated by CEA, CNRS and Inria at the following URL:
http://www.cecill.info/
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the library's author, the holder of
the economic rights, and the successive licensors have only limited
liability. See the COPYING file for more details.
From Coq Require Import Reals Psatz.
Require Import Xreal.
Require Import Basic.
Require Import Sig.
Require Import Interval.
Require Import Float.
Require Import Transcend.
Module FloatIntervalFull (F'' : FloatOps with Definition sensible_format := true) <: IntervalOps.
Module T := TranscendentalFloatFast F''.
Include FloatInterval F''.
Definition c3 := F.fromZ 3.
Definition c4 := F.fromZ 4.
Definition c8 := F.fromZ 8.
Definition pi prec :=
mul2 prec (mul2 prec (T.pi4 prec)).
Lemma pi_correct :
∀ prec, contains (convert (pi prec)) (Xreal PI).
Definition cos prec xi :=
match abs xi with
| Ibnd xl xu ⇒
if F'.le' xu xl then T.cos_fast prec xl else
let pi4 := T.pi4 prec in
if F'.le' xu (F.mul_DN prec (lower pi4) c4) then
bnd (lower (T.cos_fast prec xu)) (upper (T.cos_fast prec xl))
else
if F'.le' xu (F.mul_DN prec (lower pi4) c8) then
if F'.le' (F.mul_UP prec (upper pi4) c4) xl then
bnd (lower (T.cos_fast prec xl)) (upper (T.cos_fast prec xu))
else
bnd cm1 (F.max (upper (T.cos_fast prec xl)) (upper (T.cos_fast prec xu)))
else
let d := F.sub_UP prec xu xl in
if F'.le' d c3 then
let m := F.midpoint xl xu in
let d := F.max (F.sub_UP prec xu m) (F.sub_UP prec m xl) in
let c := T.cos_fast prec m in
meet (bnd cm1 c1) (add prec c (bnd (F.neg d) d))
else bnd cm1 c1
| Inan ⇒ Inan
end.
Lemma cos_correct :
∀ prec, extension Xcos (cos prec).
Definition sin prec xi :=
match xi with
| Ibnd xl xu ⇒
if F'.le' xu xl then T.sin_fast prec xl else
let pi4 := T.pi4 prec in
let pi2 := F.mul_DN prec (lower pi4) c2 in
match F'.le' (F.neg pi2) xl, F'.le' xu pi2 with
| true, true ⇒
bnd (lower (T.sin_fast prec xl)) (upper (T.sin_fast prec xu))
| true, false ⇒
cos prec (sub prec (mul2 prec pi4) xi)
| _, _ ⇒
neg (cos prec (add prec xi (mul2 prec pi4)))
end
| Inan ⇒ Inan
end.
Theorem sin_correct :
∀ prec, extension Xsin (sin prec).
Definition tan prec xi :=
match xi with
| Ibnd xl xu ⇒
if F'.le' xu xl then T.tan_fast prec xl else
let pi2 := F.mul_DN prec (lower (T.pi4 prec)) c2 in
match F'.lt' (F.neg pi2) xl, F'.lt' xu pi2 with
| true, true ⇒
bnd (lower (T.tan_fast prec xl)) (upper (T.tan_fast prec xu))
| _, _ ⇒ Inan
end
| Inan ⇒ Inan
end.
Lemma tan_correct :
∀ prec, extension Xtan (tan prec).
Definition atan prec xi :=
match xi with
| Ibnd xl xu ⇒
Ibnd
(if F.real xl then lower (T.atan_fast prec xl)
else F.neg (F.mul_UP prec (upper (T.pi4 prec)) c2))
(if F.real xu then upper (T.atan_fast prec xu)
else F.mul_UP prec (upper (T.pi4 prec)) c2)
| Inan ⇒ Inan
end.
Lemma atan_correct :
∀ prec, extension Xatan (atan prec).
Definition exp prec xi :=
match xi with
| Ibnd xl xu ⇒
Ibnd
(if F.real xl then lower (T.exp_fast prec xl) else F.zero)
(if F.real xu then upper (T.exp_fast prec xu) else F.nan)
| Inan ⇒ Inan
end.
Theorem exp_correct :
∀ prec, extension Xexp (exp prec).
Definition ln prec xi :=
match xi with
| Ibnd xl xu ⇒
if F'.lt' F.zero xl then
Ibnd
(lower (T.ln_fast prec xl))
(if F.real xu then upper (T.ln_fast prec xu) else F.nan)
else Inan
| Inan ⇒ Inan
end.
Theorem ln_correct :
∀ prec, extension Xln (ln prec).
End FloatIntervalFull.