Library CoqApprox.taylor_poly

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 Fcore_Raux.
Require Import Interval_xreal.
Require Import Interval_generic Interval_interval.
Require Import Interval_definitions.
Require Import Interval_specific_ops.
Require Import Interval_float_sig.
Require Import Interval_interval_float.
Require Import Interval_interval_float_full.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop.
Require Import poly_datatypes.

Set Implicit Arguments.

Module TaylorRec (Import C : FullOps).

Section PrecIsPropagated.
Variable u : U.

Definition cst_rec (x : C.T) (n : nat) := C.tcst C.tzero x.

Definition var_rec (a b : C.T) (n : nat) := C.tcst (C.tcst C.tzero a) b.

Definition inv_rec (x : T) (a : T) (n : nat) : T := tdiv u a (topp x).

Definition exp_rec (a : T) (n : nat) : T := tdiv u a (tnat n).

Definition sin_rec (a b : T) (n : nat) : T :=
  tdiv u (topp a) (tmul u (tnat n) (tnat n.-1)).

Definition cos_rec (a b : T) (n : nat) : T :=
  tdiv u (topp a) (tmul u (tnat n) (tnat n.-1)).

Local Notation "i + j" := (tadd u i j).
Local Notation "i - j" := (tsub u i j).
Local Notation "i * j" := (tmul u i j).
Local Notation "i / j" := (tdiv u i j).

Definition sqrt_rec (x : T) (a : T) (n : nat) :=
  let nn := tnat n in
  let n1 := tnat n.-1 in
  let one := tnat 1 in
  let two := tnat 2 in
  (one - two * n1) * a / (two * x * nn).

Definition invsqrt_rec (x : T) (a : T) (n : nat) :=
  let nn := tnat n in
  let n1 := tnat n.-1 in
  let one := tnat 1 in
  let two := tnat 2 in
  topp (one + two * n1) * a / (two * x * nn).


End PrecIsPropagated.
End TaylorRec.

Module Type TaylorPolyOps (C : FullOps) (P : PolyOps C).

Parameter T_cst : C.T -> C.T -> nat -> P.T.
Note that in addition to the Taylor expansion point that is the 2nd parameter of T_cst, the first one is the value of the constant itself.

Parameter T_var : C.T -> nat -> P.T.

Parameter T_inv : P.U -> C.T -> nat -> P.T.

Parameter T_exp : P.U -> C.T -> nat -> P.T.

Parameter T_sin : P.U -> C.T -> nat -> P.T.

Parameter T_cos : P.U -> C.T -> nat -> P.T.

Parameter T_sqrt : P.U -> C.T -> nat -> P.T.

Parameter T_invsqrt : P.U -> C.T -> nat -> P.T.

End TaylorPolyOps.

Module TaylorPoly (C : FullOps) (P : PolyOps C) <: TaylorPolyOps C P.
Needs functions defining the recurrences, as well as trec1, trec2.
Module Rec := TaylorRec C.
Import P C Rec.

Definition T_cst c (x : C.T) := trec1 cst_rec (tcst c x).

Definition T_var x := trec2 var_rec x (tcst C.tone x).

Section PrecIsPropagated.
Variable u : P.U.

Definition T_inv x := trec1 (inv_rec u x) (tinv u x).

Definition T_exp x := trec1 (exp_rec u) (texp u x).

Definition T_sin x := trec2 (sin_rec u) (tsin u x) (tcos u x).

Definition T_cos x := trec2 (cos_rec u) (tcos u x) (C.topp (tsin u x)).

Definition T_sqrt x := trec1 (sqrt_rec u x) (tsqrt u x).

Definition T_invsqrt x := trec1 (invsqrt_rec u x) (tinvsqrt u x).

End PrecIsPropagated.
End TaylorPoly.