Library CoqApprox.test_exp_sin

This file is part of the CoqApprox formalization of rigorous polynomial approximation in Coq: http://tamadi.gforge.inria.fr/CoqApprox/
Copyright (c) 2010-2013, ENS de Lyon and 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.

Require Import ZArith.
Require Import BigZ.
Require Import Interval_definitions.
Require Import Interval_specific_ops.
Require Import Interval_bigint_carrier.
Require Import Interval_interval_float.
Require Import Interval_interval_float_full.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
Require Import poly_datatypes.
Require Import poly_inst_seq.
Require Import taylor_model_int_sharp.
Require Import taylor_model_float_sharp.
Require Import coeff_inst.
Require Import rpa_inst.

Set Implicit Arguments.

Module C := BigIntRadix2.
Module F := SpecificFloat C.
Module I := FloatIntervalFull F.

Module PolX := ExactSeqPolyMonomUp FullXR.
Module Link := LinkSeqPolyMonomUp I.
Module PolI := SeqPolyMonomUpInt I.

Module PolF := SeqPolyMonomUpFloat F.
Module Import TMF := TaylorModelFloat F PolF I PolI PolX Link.
Import TMF.TM.

Local Open Scope bigZ_scope.

Notation "m *2^ e" := (Float m e) (at level 30).

A simple definition for outwards rounding
Definition Irnd prec xi :=
  match xi with
    | Inan => Inan
    | Ibnd xl xu => Ibnd (F.round rnd_DN prec xl) (F.round rnd_UP prec xu)
  end.

Module TM_comp_0.
Definition a := Float (1) (-1).
Definition b := Float (2) (-1).
Definition X := Ibnd a b.
Definition c := I.midpoint (Ibnd a b).
Definition X0 := Ibnd c c.
Definition deg := 10%nat.
Definition pr := 200%bigZ.
Definition tm_sin := TM_sin pr X0 X deg.
Definition tm := TM_comp pr (TM.TM_exp pr) tm_sin X0 X deg.
Definition tm' := i2f_tm pr X0 X tm.
End TM_comp_0.