Library CoqApprox.poly_datatypes

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 Reals.
Require Import NaryFunctions.
Require Import Fcore.
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 nary_tuple.

Set Implicit Arguments.

Module Type BaseOps.
Parameter U : Type.
Parameter T : Type.

Parameter tzero : T.
Parameter tone : T.
Parameter topp : T -> T.
Parameter tadd : U -> T -> T -> T.
Parameter tsub : U -> T -> T -> T.
Parameter tmul : U -> T -> T -> T.
End BaseOps.

Module Type SliceMaskBaseOps (Import A : BaseOps).
Parameter tcst : T -> T -> T.
the first argument is the constant
End SliceMaskBaseOps.

Module Type SlicePowDivOps (Import A : BaseOps).
Parameter tpower_int : U -> T -> Z -> T.
Parameter tsqr : U -> T -> T.
Parameter tinv : U -> T -> T.
Parameter tdiv : U -> T -> T -> T.
End SlicePowDivOps.

Module Type SliceFullOps (Import A : BaseOps).
Parameter tnat : nat -> T.
Parameter tsqrt : U -> T -> T.
Parameter tinvsqrt : U -> T -> T.
Parameter texp : U -> T -> T.
Parameter tsin : U -> T -> T.
Parameter tcos : U -> T -> T.
End SliceFullOps.

Module Type MaskBaseOps := BaseOps <+ SliceMaskBaseOps.
Module Type PowDivOps := MaskBaseOps <+ SlicePowDivOps.
Module Type FullOps := PowDivOps <+ SliceFullOps.

Module Type BaseOps0 := BaseOps with Definition U := unit.
Module Type MaskBaseOps0 := MaskBaseOps with Definition U := unit.
Module Type PowDivOps0 := PowDivOps with Definition U := unit.
Module Type FullOps0 := FullOps with Definition U := unit.

Module Type SliceExactBaseOps (Import A : BaseOps0).
Parameter 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).
Parameter tadd_zerol : left_id tzero (tadd tt).
Parameter tadd_zeror : right_id tzero (tadd tt).
Parameter tadd_comm : commutative (tadd tt).
Parameter tadd_assoc : associative (tadd tt).
Parameter tmul_onel : left_id tone (tmul tt).
Parameter tmul_oner : right_id tone (tmul tt).
Parameter tmul_comm : commutative (tmul tt).
Parameter tmul_assoc : associative (tmul tt).
Parameter tmul_distrl : left_distributive (tmul tt) (tadd tt).
Parameter tmul_distrr : right_distributive (tmul tt) (tadd tt).
End SliceExactBaseOps.

Module Type SliceExactMaskBaseOps (Import A : MaskBaseOps0).
Parameter mask_add_l :
  forall a b x, tcst (tadd tt a b) x = tadd tt (tcst a x) b.
Parameter mask_add_r :
  forall a b x, tcst (tadd tt a b) x = tadd tt a (tcst b x).
Parameter mask_mul_l :
  forall a b x, tcst (tmul tt a b) x = tmul tt (tcst a x) b.
Parameter mask_mul_r :
  forall a b x, tcst (tmul tt a b) x = tmul tt a (tcst b x).
Parameter mask0mul_l :
  forall x, tmul tt tzero x = tcst tzero x.
Parameter mask0mul_r :
  forall x, tmul tt x tzero = tcst tzero x.
Parameter mask_idemp :
  forall a x, tcst (tcst a x) x = tcst a x.
Parameter mask_comm :
  forall a x y, tcst (tcst a x) y = tcst (tcst a y) x.
End SliceExactMaskBaseOps.

Module Type SliceExactPowDivOps (Import A : PowDivOps0).
Local Notation tpow prec x n := (tpower_int prec x (Z_of_nat n)).
Parameter tpow_0 : forall x, tpow tt x 0 = tcst tone x.
Parameter tpow_S : forall x n, tpow tt x n.+1 = tmul tt x (tpow tt x n).
Parameter tpow_opp :
  forall x n, x <> tzero -> tpower_int tt x (-n) = tinv tt (tpower_int tt x n).
End SliceExactPowDivOps.

Module Type ExactFullOps :=
 FullOps0 <+ SliceExactBaseOps <+ SliceExactMaskBaseOps <+ SliceExactPowDivOps.

Module Type PolyOps (C : BaseOps) <: BaseOps.
Include Type BaseOps with Definition U := C.U. Parameter tmul_trunc : U -> nat -> T -> T -> T.
Parameter tmul_tail : U -> nat -> T -> T -> T.
Parameter tpolyNil : T.
Parameter tpolyCons : C.T -> T -> T.
Parameter teval : U -> T -> C.T -> C.T.
Parameter tnth : T -> nat -> C.T.
Parameter tsize : T -> nat.

Parameter trec1 : (C.T -> nat -> C.T) -> C.T -> nat -> T.
Parameter trec1_spec0 :
  forall (F : C.T -> nat -> C.T) F0 n,
  tnth (trec1 F F0 n) 0 = F0.
Parameter trec1_spec :
  forall (F : C.T -> nat -> C.T) F0 p k, k < p ->
  tnth (trec1 F F0 p) k.+1 = F (tnth (trec1 F F0 k) k) k.+1.

Parameter trec2 : (C.T -> C.T -> nat -> C.T) -> C.T -> C.T -> nat -> T.
Parameter trec2_spec0 :
  forall (F : C.T -> C.T -> nat -> C.T) F0 F1 n,
  tnth (trec2 F F0 F1 n) 0 = F0.
Parameter trec2_spec1 :
  forall (F : C.T -> C.T -> nat -> C.T) F0 F1 n,
  tnth (trec2 F F0 F1 n.+1) 1 = F1.
Parameter trec2_spec :
  forall (F : C.T -> C.T -> nat -> C.T) F0 F1 p k, k.+1 < p ->
  tnth (trec2 F F0 F1 p) k.+2 =
  F (tnth (trec2 F F0 F1 k) k) (tnth (trec2 F F0 F1 k.+1) k.+1) k.+2.

Parameter trecN :
  forall N : nat, C.T ^ N -> C.T ^^ N --> (nat -> C.T) -> nat -> T.
Parameter trecN_spec0 :
  forall (N : nat) (L0 : C.T ^ N) (F : C.T ^^ N --> (nat -> C.T)) (n k : nat)
  (d : C.T),
  k <= n -> k < N -> tnth (trecN L0 F n) k = nth d (Ttoseq L0) k.

Parameter tlastN : C.T -> forall N : nat, T -> C.T ^ N.
Parameter tlastN_spec :
  forall (d := C.tzero) N (p : T) (i : 'I_N),
  Tnth (tlastN d N p) i = tnth p (tsize p - N + val i).

Parameter trecN_spec :
  forall (N : nat) (L0 : C.T ^ N) (F : C.T ^^ N --> (nat -> C.T)) (n k : nat)
         (d : C.T),
  k <= n -> k >= N ->
  tnth (trecN L0 F n) k =
  (nuncurry F) (tlastN d N (trecN L0 F k.-1)) k.
Parameter tsize_trecN :
  forall (N : nat) (L0 : C.T ^ N) (F : C.T ^^ N --> (nat -> C.T)) (n k : nat)
         (d : C.T),
  tsize (trecN L0 F n) = n.+1.

Parameter tfold : forall V : Type, (C.T -> V -> V) -> V -> T -> V.
Parameter tset_nth : T -> nat -> C.T -> T.
Parameter tsize_trec1 : forall F x n, tsize (trec1 F x n) = n.+1.
Parameter tsize_trec2 : forall F x y n, tsize (trec2 F x y n) = n.+1.
Parameter tsize_mul_trunc : forall u n p q, tsize (tmul_trunc u n p q) = n.+1.
Parameter tsize_mul_tail :
  forall u n p q, tsize (tmul_tail u n p q) = ((tsize p).-1 + (tsize q).-1 - n).
Parameter tsize_tadd :
  forall u p1 p2,
  tsize (tadd u p1 p2) = maxn (tsize p1) (tsize p2).
Parameter tnth_tadd :
  forall u p1 p2 k, k < minn (tsize p1) (tsize p2) ->
  tnth (tadd u p1 p2) k = C.tadd u (tnth p1 k) (tnth p2 k).
Parameter tsize_polyCons : forall a p, tsize (tpolyCons a p) = (tsize p).+1.
Parameter tnth_polyCons : forall a p k, k <= tsize p ->
  tnth (tpolyCons a p) k = if k is k'.+1 then tnth p k' else a.
Parameter tnth_polyNil : forall n, tnth tpolyNil n = C.tzero.
Parameter tnth_out : forall p n, tsize p <= n -> tnth p n = C.tzero.
Note that we explicitely choose a default value here
Parameter tsize_polyNil : tsize tpolyNil = 0.
Parameter tsize_set_nth : forall p n val,
  n < tsize p ->
  tsize (tset_nth p n val) = tsize p.
Parameter tnth_set_nth_eq : forall p n val,
  n < tsize p ->
  tnth (tset_nth p n val) n = val.
Parameter tnth_set_nth_neq : forall p n val k,
  k <> n ->
  k < tsize p ->
  tnth (tset_nth p n val) k = tnth p k.
Parameter tfold_polyNil : forall U f iv, @tfold U f iv tpolyNil = iv.
Parameter tfold_polyCons : forall U f iv c p,
  @tfold U f iv (tpolyCons c p) = f c (@tfold U f iv p).
Parameter tpoly_ind : forall (f : T -> Type),
  f tpolyNil ->
  (forall a p, f p -> f (tpolyCons a p)) ->
  forall p, f p.
End PolyOps.

Module Type SliceMonomPolyOps (C : MaskBaseOps) (Import A : PolyOps C).
Horner evaluation of polynomial in monomial basis
Parameter teval_polyCons :
  forall u c p x,
  teval u (tpolyCons c p) x =
  C.tadd u (C.tmul u (teval u p x) x) c.
Parameter teval_polyNil :
  forall u x, teval u tpolyNil x = C.tcst C.tzero x.
End SliceMonomPolyOps.

Module Type MonomPolyOps (C : MaskBaseOps) := PolyOps C <+ SliceMonomPolyOps C.

Module Type SliceExactMonomPolyOps
  (C : PowDivOps0)
  (Import A : PolyOps C)
  (B : SliceMonomPolyOps C A).

Local Notation Ctpow prec x n := (C.tpower_int prec x (Z_of_nat n)).

Parameter is_horner :
 forall p x, teval tt p x =
  \big[C.tadd tt/C.tcst C.tzero x]_(i < tsize p)
  C.tmul tt (tnth p i) (Ctpow tt x i).

Parameter tmul_trunc_nth:
forall p1 p2 n k,
 k < n.+1 ->
 tnth (tmul_trunc tt n p1 p2) k =
  \big[C.tadd tt/C.tzero]_(i < k.+1) C.tmul tt (tnth p1 i) (tnth p2 (k -i)).

Parameter tmul_tail_nth:
forall p1 p2 n k,
 k < ((tsize p1).-1 + (tsize p2).-1 - n) ->
 tnth (tmul_tail tt n p1 p2) k =

 \big[C.tadd tt/C.tzero]_(i < (k+n.+1).+1)
   C.tmul tt (tnth p1 i) (tnth p2 ((k + n.+1) - i)).

End SliceExactMonomPolyOps.

Note that the implementations of the previous signature will rely on the choice of a particular polynomial basis, especially for the multiplication and polynomial evaluation.

Module Type ExactMonomPolyOps (C : PowDivOps0)
  := PolyOps C <+ SliceMonomPolyOps C <+ SliceExactMonomPolyOps C.

Module RigPolyApprox (I : IntervalOps) (C : BaseOps) (Pol : PolyOps C).

Rigorous Polynomial Approximation structure
Structure rpa : Type := RPA {
  approx : Pol.T;
  error : I.type

End RigPolyApprox.