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 T.I.

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
  | InanInan
  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
  | InanInan
  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
  | InanInan
  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)
  | InanInan
  end.

Lemma pi4_mul2 :
   prec,
  F.valid_ub (F.mul_UP prec (upper (T.pi4 prec)) (F.fromZ 2)) = true
  le_upper (Xreal (PI/2))%XR (F.toX (F.mul_UP prec (upper (T.pi4 prec)) (F.fromZ 2))).

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)
  | InanInan
  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
  | InanInan
  end.

Theorem ln_correct :
   prec, extension Xln (ln prec).

End FloatIntervalFull.