Library CoqApprox.coeff_inst

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 Reals.
Require Import Interval_interval.
Require Import Interval_xreal.
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 interval_compl.
Require Import xreal_ssr_compat.
Require Import poly_datatypes.

Set Implicit Arguments.

Reserved Notation "--> e"
  (at level 10, e at level 8, no associativity, format "--> e").

Module BaseZ <: BaseOps.
Definition U := unit. Local Notation "--> e" := (fun _ : U => e).
Definition T := Z.
Definition tzero := Z0.
Definition tone := 1%Z.
Definition tadd := --> Zplus.
Definition tmul := --> Zmult.
Definition topp := Zopp.
Definition tsub := --> Zminus.
End BaseZ.

Module FullReal <: FullOps.
Definition U := unit.
Local Notation "--> e" := (fun _ : U => e).
Definition T := R.
Definition tzero := R0.
Definition tone := R1.
Definition topp := Ropp.
Definition tadd := --> Rplus.
Definition tsub := --> Rminus.
Definition tmul := --> Rmult.
Definition tdiv := --> Rdiv.
Definition tpower_int := --> powerRZ.
Definition texp := --> exp.
Definition tnat := INR.
Definition tinv := --> Rinv.
Definition tcos := --> cos.
Definition tsin := --> sin.
Definition tsqr := --> fun x => Rmult x x.
Definition tsqrt := --> sqrt.
Definition tinvsqrt := --> fun x => (Rinv (sqrt x)).
Definition tcst : T -> T -> T := fun c _ => c.
End FullReal.

Module FullXR <: ExactFullOps.
Definition U := unit.
Local Notation "--> e" := (fun _ : U => e).
Definition T := ExtendedR.
Definition tcst := Xmask.
Definition tzero := Xreal R0.
Definition tone := Xreal R1.
Definition topp := Xneg.
Definition tadd := --> Xadd.
Definition tsub := --> Xsub.
Definition tmul := --> Xmul.
Definition tdiv := --> Xdiv.
Definition tpower_int := --> Xpower_int.
Definition tpow := --> fun x n => Xpower_int x (Z_of_nat n).
Definition texp := --> Xexp.
Definition tnat := fun n => Xreal (INR n).
Definition tinv := --> Xinv.
Definition tcos := --> Xcos.
Definition tsin := --> Xsin.
Definition tsqr := --> fun x => Xmul x x.
Definition tsqrt := --> Xsqrt.
Definition tinvsqrt := --> fun x => Xinv (Xsqrt x).
Lemma tadd_zerol : left_id tzero (tadd tt).
Lemma tadd_zeror : right_id tzero (tadd tt).
Lemma tadd_comm : commutative (tadd tt).
Lemma tadd_assoc : associative (tadd tt).
Lemma tmul_onel : left_id tone (tmul tt).
Lemma tmul_oner : right_id tone (tmul tt).
Lemma tmul_comm : commutative (tmul tt).
Lemma tmul_assoc : associative (tmul tt).
Lemma tmul_distrl : left_distributive (tmul tt) (tadd tt).
Lemma tmul_distrr : right_distributive (tmul tt) (tadd tt).

Lemma mask_add_l : forall a b x, tcst (tadd tt a b) x = tadd tt (tcst a x) b.
Lemma mask_add_r : forall a b x, tcst (tadd tt a b) x = tadd tt a (tcst b x).
Lemma mask_mul_l : forall a b x, tcst (tmul tt a b) x = tmul tt (tcst a x) b.
Lemma mask_mul_r : forall a b x, tcst (tmul tt a b) x = tmul tt a (tcst b x).

Lemma tpow_0 : forall x, tpow tt x 0 = tcst tone x.

Lemma tpow_S (x : ExtendedR) (n : nat) :
  tpow tt x n.+1 = tmul tt x (tpow tt x n).

Lemma tpow_opp (x : ExtendedR) (n : Z) : x <> Xreal 0 ->
  tpower_int tt x (-n) = tinv tt (tpower_int tt x n).

Lemma big_distrr_spec :
  forall n F a, n <> 0 -> tmul tt a (\big[tadd tt/tzero]_(i < n) F i) =
  \big[tadd tt/tzero]_(i < n) tmul tt a (F i).

Lemma mask_idemp : forall a x, tcst (tcst a x) x = tcst a x.

Lemma mask_comm :
  
  forall a x y, tcst (tcst a x) y = tcst (tcst a y) x.

Lemma mask0mul_l : forall x, tmul tt tzero x = tcst tzero x.

Lemma mask0mul_r : forall x, tmul tt x tzero = tcst tzero x.
End FullXR.

Definition nuncurry2 {A1 A2 B : Type} : (A1 -> A2 -> B) -> A1 * A2 -> B :=
  fun (f : A1 -> A2 -> B) (p : A1 * A2) => let (a, b) := p in f a b.

Module MaskBaseF (F:FloatOps with Definition even_radix := true) <: MaskBaseOps.
Definition U := (rounding_mode * F.precision)%type.
Definition T := F.type.
Definition tzero := F.zero.
Definition tone := F.fromZ 1%Z.
Definition tadd : U -> T -> T -> T := nuncurry2 F.add.
Definition tmul : U -> T -> T -> T := nuncurry2 F.mul.
Definition topp : T -> T := F.neg.
Definition tsub : U -> T -> T -> T := nuncurry2 F.sub.
Definition tcst (c x : T) : T :=
  if F.real x then c else F.nan.
End MaskBaseF.

Module MaskBaseF_NE (F : FloatOps with Definition even_radix := true)
  <: MaskBaseOps.
Definition U := F.precision.
Definition T := F.type.
Definition tzero := F.zero.
Definition tone := F.fromZ 1%Z.
Definition tadd : U -> T -> T -> T := F.add rnd_NE.
Definition tmul : U -> T -> T -> T := F.mul rnd_NE.
Definition topp : T -> T := F.neg.
Definition tsub : U -> T -> T -> T := F.sub rnd_NE.
Definition tcst (c x : T) : T :=
  if F.real x then c else F.nan.
End MaskBaseF_NE.

Module FullInt (I : IntervalOps) <: FullOps.
Definition U := I.precision.
Definition T := I.type.
Definition tzero := I.fromZ Z0.
Lemma zero_correct : contains (I.convert tzero) (Xreal 0).
Definition tone := I.fromZ 1.
Definition topp := I.neg.
Definition tadd := I.add.
Definition tsub := I.sub.
Definition tmul := I.mul.
Definition tdiv := I.div.
Definition tpower_int := I.power_int.
Definition texp := I.exp.
Definition tnat := fun n => I.fromZ (Z_of_nat n).
Definition tinv := I.inv.
Definition tcos := I.cos.
Definition tsin := I.sin.
Definition tsqr := I.sqr.
Definition tsqrt := I.sqrt.
Definition tinvsqrt := fun prec x => I.inv prec (I.sqrt prec x).
Definition tcst : T -> T -> T := I.mask.
End FullInt.