Library CoqApprox.taylor_model_float_sharp

This file is part of the CoqApprox formalization of rigorous polynomial approximation in Coq:
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:
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 Interval_xreal.
Require Import Interval_xreal_derive.
Require Import Interval_missing.
Require Import Interval_generic_proof.
Require Import Rstruct.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop ssralg.
Require Import xreal_ssr_compat.
Require Import poly_datatypes.
Require Import interval_compl.
Require Import taylor_poly.
Require Import coeff_inst.
Require Import rpa_inst.
Require Import derive_compl.
Require Import taylor_model_int_sharp.

Set Implicit Arguments.

Module Type FloatIntervalOps (F : FloatOps with Definition even_radix := true)
  <: IntervalOps.
  Include FloatIntervalFull F.
End FloatIntervalOps.

Module RigPolyApproxFloat (F : FloatOps with Definition even_radix := true)
  (P : FloatPolyOps F) (I : FloatIntervalOps F).
Module Fl := MaskBaseF F.
Include RigPolyApprox I Fl P.
End RigPolyApproxFloat.

Module PolyMap (A : BaseOps) (PolA : PolyOps A) (B : BaseOps) (PolB : PolyOps B).

Definition tpolymap (f : A.T -> B.T) : PolA.T -> PolB.T :=
  @PolA.tfold _ (fun x => PolB.tpolyCons (f x) ) PolB.tpolyNil.

Lemma tsize_polymap (f : A.T -> B.T) (p : PolA.T) :
  PolB.tsize (tpolymap f p) = PolA.tsize p.

Lemma tnth_polymap (f : A.T -> B.T) (i : nat) (p : PolA.T) :
  i < PolA.tsize p -> PolB.tnth (tpolymap f p) i = f (PolA.tnth p i).

Definition tpolymap_polyCons (f : A.T -> B.T) a p :
  tpolymap f (PolA.tpolyCons a p) =
  PolB.tpolyCons (f a) (tpolymap f p).
Proof @PolA.tfold_polyCons _ _ _ _ _.

Definition tpolymap_polyNil (f : A.T -> B.T) :
  tpolymap f PolA.tpolyNil = PolB.tpolyNil.
Proof @PolA.tfold_polyNil _ _ _.

End PolyMap.

Module TaylorModelFloat (F : FloatOps with Definition even_radix := true)
  (PolF : FloatPolyOps F)
  (I : FloatIntervalOps F)
  (Import Pol : IntMonomPolyOps I)
  (PolX : ExactMonomPolyOps FullXR)
  (Link : LinkIntX I Pol PolX).
Module Import TM := TaylorModel I Pol PolX Link.
Module RPAF := RigPolyApproxFloat F PolF I.

Notation f_type := F.type.
Notation f_poly := PolF.T.
Notation f_rpa := RPAF.rpa.
Notation f_RPA := RPAF.RPA.
Notation f_error := RPAF.error.
Notation f_approx := RPAF.approx.

Notation i_type := I.type.
Notation i_poly := Pol.T.
Notation i_rpa := TM.RPA.rpa.
Notation i_RPA := TM.RPA.RPA.
Notation i_error := TM.RPA.error.
Notation i_approx := TM.RPA.approx.

Notation x_type := ExtendedR.
Notation x_poly := PolX.T.

Notation i_prec := I.precision.
Notation i_eval := Pol.teval.
Notation x_eval := (PolX.teval tt).

Definition i2f_mid : i_type -> f_type := I.midpoint.

Lemma i2f_mid_correct (xi : i_type) :
  (exists x : x_type, contains (I.convert xi) x) ->
  I.convert_bound (i2f_mid xi) =
  Xreal (proj_val (I.convert_bound (I.midpoint xi))) /\
  contains (I.convert xi) (I.convert_bound (I.midpoint xi)).

Definition f2i : f_type -> i_type := fun x => I.bnd x x.

Module MapI := PolyMap Pol.Int Pol Pol.Int Pol.
Module MapIF := PolyMap Pol.Int Pol PolF.Fl PolF.
Module MapFX := PolyMap PolF.Fl PolF FullXR PolX.

Notation i_poly_map := MapI.tpolymap.

Definition i2f_poly : i_poly -> f_poly := MapIF.tpolymap i2f_mid.

Definition i2f_rem (pr : i_prec) : i_poly -> i_poly :=
  i_poly_map (fun x => I.sub pr x (f2i (i2f_mid x))).

Notation f2x := I.convert_bound.

Definition f2x_poly : f_poly -> x_poly := MapFX.tpolymap f2x.

Notation i2ix := I.convert.

Notation subset_ := Interval_interval.subset.

Definition f_validTM
  (X0 X : interval) (M0 : f_rpa) (f : ExtendedR -> ExtendedR) :=
  [/\ contains (i2ix (f_error M0)) (Xreal 0),
    subset_ X0 X &
    forall xi0 x : ExtendedR, contains X0 xi0 -> contains X x ->
    contains (i2ix (f_error M0))
    (Xsub (f x) (x_eval (f2x_poly (f_approx M0)) (Xsub x xi0)))].

Definition i2f_tm (pr : i_prec) (X0 X : i_type) (M : i_rpa) : f_rpa :=
  (i2f_poly (i_approx M))
  (I.add pr (i_error M) (i_eval pr (i2f_rem pr (i_approx M)) (I.sub pr X X0))).

Lemma teval_contains_0 pr P (X : i_type) :
  (forall k, k < Pol.tsize P -> contains (I.convert(Pol.tnth P k)) (Xreal 0)) ->
  contains (I.convert X) (Xreal 0) ->
  contains (I.convert (i_eval pr P X)) (Xreal 0).

Lemma sub_midp_contains_0 pr (X : i_type) :
  (exists t : x_type, contains (I.convert X) t) ->
  contains (I.convert (I.sub pr X (f2i (i2f_mid X)))) (Xreal 0).

Lemma Xsub_Xnan_r (a : ExtendedR) : Xsub a Xnan = Xnan.

Lemma Xsub_diag_eq (x : ExtendedR) : Xsub x x = Xmask (Xreal 0) x.

Lemma Imask_mask (x y : i_type) : I.mask (I.mask x y) y = I.mask x y.

Lemma contains_bnd2 (fx : f_type) :
  f2x fx <> Xnan ->
  contains (I.convert (I.bnd fx fx)) (f2x fx).

Lemma i2f_mid_nan (x : i_type) :
  (exists t : ExtendedR, contains (i2ix x) t) ->
  f2x (I.midpoint x) <> Xnan.

Theorem i2f_tm_correct pr (X0 X : i_type) M f :
  (exists t, contains (I.convert X0) t) ->
  i_validTM (i2ix X0) (i2ix X) M f ->
  f_validTM (i2ix X0) (i2ix X) (i2f_tm pr X0 X M) f.

End TaylorModelFloat.