Library Interval.Poly.Bound_quad
This file is part of the CoqApprox formalization of rigorous
polynomial approximation in Coq:
http://tamadi.gforge.inria.fr/CoqApprox/
Copyright (C) 2010-2012, ENS de Lyon.
Copyright (C) 2010-2016, Inria.
Copyright (C) 2014-2016, IRIT.
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 ZArith Reals.
From Flocq Require Import Raux.
From mathcomp.ssreflect Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop.
Require Import Xreal.
Require Import Interval.
Require Import MathComp.
Require Import Datatypes.
Require Import Bound.
Set Implicit Arguments.
Module PolyBoundHornerQuad (I : IntervalOps) (Pol : PolyIntOps I)
<: PolyBound I Pol.
Module Import Bnd := PolyBoundHorner I Pol.
Module J := IntervalExt I.
Definition ComputeBound (prec : Pol.U) (pol : Pol.T) (x : I.type) : I.type :=
if 3 ≤ Pol.size pol then
let a1 := Pol.nth pol 1 in
let a2 := Pol.nth pol 2 in
let a2t2 := I.add prec a2 a2 in
let a2t4 := I.add prec a2t2 a2t2 in
let b1 := I.div prec a1 a2t2 in
let b2 := I.div prec (I.sqr prec a1) a2t4 in
if I.bounded b2 then
I.add prec
(I.add prec (I.sub prec (Pol.nth pol 0) b2)
(I.mul prec a2 (I.sqr prec (I.add prec x b1))))
(I.mul prec (I.power_int prec x 3)
(Pol.horner prec (Pol.tail 3 pol) x))
else Pol.horner prec pol x
else Pol.horner prec pol x.
Import Pol.Notations. Local Open Scope ipoly_scope.
Theorem ComputeBound_correct prec pi p :
pi >:: p →
J.extension (PolR.horner tt p) (ComputeBound prec pi).
Lemma ComputeBound_propagate :
∀ prec pi,
J.propagate (ComputeBound prec pi).
End PolyBoundHornerQuad.