Library CoqApprox.poly_inst_seq

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 NaryFunctions.
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_interval.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop ssralg.
Require Import seq_compl.
Require Import nary_tuple.
Require Import poly_datatypes.
Require Import basic_rec.
Require Import coeff_inst.
Require Import rpa_inst.

Implementation of PolyOps with sequences and operations in monomial basis

Set Implicit Arguments.

Import GRing.Theory.

Lemma eq_foldr (T0 T1 T2 : Type)
  (f0 : T1 -> T0 -> T0)
  (g : T2 -> T0 -> T0) (ftog : T1 -> T2) :
  (forall x y, f0 x y = g (ftog x) y) ->
  forall s x0, foldr f0 x0 s = foldr g x0 (map ftog s).

Lemma rev_iota k: map (subn k) (iota 0 k.+1)= rev (iota 0 k.+1).

Module SeqPolyMonomUp (Import C : MaskBaseOps) <: PolyOps C <: MonomPolyOps C.

Definition U := C.U.

Definition T := seq C.T.
Definition tzero := [::] : T.
Definition tone := [:: C.tone].
Fixpoint topp (p : T) :=
  match p with
    | [::] => [::]
    | a :: p1 => C.topp a :: topp p1
  end.

Lemma size_topp : forall p, size (topp p) = size p.

Section PrecIsPropagated.
Variable u : U.

Fixpoint tadd (p1 p2 : T) :=
  match p1 with
    | [::] => p2
    | a1 :: p3 => match p2 with
                    | [::] => p1
                    | a2 :: p4 => C.tadd u a1 a2 :: tadd p3 p4
                  end
  end.

Fixpoint tsub (p1 p2 : T) :=
  match p1 with
    | [::] => topp p2
    | a1 :: p3 => match p2 with
                    | [::] => p1
                    | a2 :: p4 => C.tsub u a1 a2 :: tsub p3 p4
                  end
  end.

Lemma size_tsub :
 forall p1 p2, size (tsub p1 p2) = maxn (size p1) (size p2).

Definition mul_coeff (p q : T) (n : nat) : C.T :=
  foldl (fun x i => C.tadd u
    (C.tmul u (nth C.tzero p i) (nth C.tzero q (n - i))) x)
  (C.tzero) (iota 0 n.+1).

Lemma mul_coeffE' p1 p2 k : mul_coeff p1 p2 k =
         \big[C.tadd u/C.tzero]_(i < k.+1) C.tmul u (nth C.tzero p1 (k - i))
                                                (nth C.tzero p2 i).

Definition tmul_trunc n p q := mkseq (mul_coeff p q) n.+1.

Definition tmul_tail n p q :=
  mkseq (fun i => mul_coeff p q (n.+1+i)) ((size p).-1 + (size q).-1 - n).

Definition tmul p q := mkseq (mul_coeff p q) (size p + size q).-1.


Definition tnth := nth C.tzero.
Definition trec1 := @rec1up C.T.
Definition trec2 := @rec2up C.T.
Definition trecN := @recNup C.T.
Definition tsize := @size C.T.

Definition tfold := @foldr C.T.
Definition teval p x :=
  @tfold C.T (fun a b => C.tadd u (C.tmul u b x) a) (C.tcst C.tzero x) p.
Definition tset_nth := @set_nth C.T C.tzero.
Definition tmap := @map C.T C.T.
Lemma tsize_map :
  forall (f : C.T -> C.T) (p : T),
  tsize (tmap f p) = tsize p.

Lemma tnth_map :
  forall (f : C.T -> C.T) (i : nat) (p : T),
  i < tsize p -> tnth (tmap f p) i = f (tnth p i).

Lemma tsize_tadd :
 forall p1 p2, tsize (tadd p1 p2) = maxn (tsize p1) (tsize p2).

Lemma tnth_tadd :
   forall p1 p2 k, k < minn (tsize p1) (tsize p2) ->
   tnth (tadd p1 p2) k = C.tadd u (tnth p1 k) (tnth p2 k).

Notation Local "a + b" := (C.tadd a b).
Notation Local "a * b" := (C.tmul a b).

Lemma tsize_trec1 F x n: tsize (trec1 F x n) = n.+1.

Lemma tsize_trec2 F x y n: tsize (trec2 F x y n) = n.+1.

Lemma trec1_spec0 :
  forall (F : C.T -> nat -> C.T) F0 k,
    tnth (trec1 F F0 k) 0 = F0.

Lemma 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.

For trec2

Lemma trec2_spec0 :
  forall (F : C.T -> C.T -> nat -> C.T) F0 F1 k,
    tnth (trec2 F F0 F1 k) 0 = F0.

Lemma trec2_spec1 :
  forall (F : C.T -> C.T -> nat -> C.T) F0 F1 k,
    tnth (trec2 F F0 F1 k.+1) 1 = F1.

Lemma 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.

For trecN

Lemma 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.

Definition tlastN : C.T -> forall N : nat, T -> C.T ^ N := @lastN C.T.
Lemma 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).

Lemma 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.

Lemma 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.

Definition tpolyCons := @Cons C.T.

Lemma tsize_polyCons : forall a p, tsize (tpolyCons a p) = (tsize p).+1.

Lemma 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.

Definition tpolyNil := @Nil C.T.

Lemma tpoly_ind : forall (f : T -> Type),
  f tpolyNil ->
  (forall a p, f p -> f (tpolyCons a p)) ->
  forall p, f p.

Lemma tnth_polyNil n: tnth tpolyNil n = C.tzero.

Lemma tsize_polyNil : tsize tpolyNil = 0.

Lemma tsize_mul_trunc n p q: tsize (tmul_trunc n p q) = n.+1.

Lemma tsize_mul_tail n p q:
     tsize (tmul_tail n p q) = ((tsize p).-1 + (tsize q).-1 - n).

Lemma tfold_polyNil : forall U f iv, @tfold U f iv tpolyNil = iv.

Lemma tfold_polyCons : forall U f iv c p,
  @tfold U f iv (tpolyCons c p) = f c (@tfold U f iv p).

Lemma tsize_set_nth p n val:
  n < tsize p ->
  tsize (tset_nth p n val) = tsize p.

Lemma tnth_set_nth_eq p n val:
 n < tsize p -> tnth (tset_nth p n val) n = val.

Lemma tnth_set_nth_neq p n val k:
 k <> n -> k < tsize p ->
 tnth (tset_nth p n val) k = tnth p k.

Lemma teval_polyNil : forall x, teval tpolyNil x = C.tcst C.tzero x.

Lemma teval_polyCons :
  forall c p x, teval (tpolyCons c p) x = C.tadd u (C.tmul u (teval p x) x) c.

Lemma tnth_out p n: tsize p <= n -> tnth p n = C.tzero.

End PrecIsPropagated.
End SeqPolyMonomUp.

Module ExactSeqPolyMonomUp (C : ExactFullOps) <: ExactMonomPolyOps C.
Include SeqPolyMonomUp C.
Module Import M := SeqPolyMonomUp C.

Canonical Cadd_monoid := Monoid.Law C.tadd_assoc C.tadd_zerol C.tadd_zeror.
Canonical Cadd_comm := Monoid.ComLaw C.tadd_comm.
Canonical Cmul_monoid := Monoid.Law C.tmul_assoc C.tmul_onel C.tmul_oner.
Canonical Cmul_comm := Monoid.ComLaw C.tmul_comm.
Canonical Cadd_addlaw := Monoid.AddLaw C.tmul_distrl C.tmul_distrr.


Lemma mask_big_helper :
  forall x n F, \big[C.tadd tt/C.tcst C.tzero x]_(i < n) F i =
  C.tcst (\big[C.tadd tt/C.tzero]_(i < n) F i) x.

Ltac magic_mask :=
 rewrite -!(C.mask_mul_l,C.mask_mul_r,C.mask_add_l,C.mask_add_r) !C.mask_idemp.

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

Lemma is_horner 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).

Lemma trunc_inc m p1 p2 : tmul_trunc tt m.+1 p1 p2 =
   tmul_trunc tt m p1 p2 ++ [:: tnth (tmul_trunc tt m.+1 p1 p2) m.+1].

Lemma trunc_leq p1 p2 n m : n <= m -> forall k, k < n.+1 ->
  tnth (tmul_trunc tt n p1 p2) k = tnth (tmul_trunc tt m p1 p2) k.

Lemma mul_coeffE p1 p2 k : mul_coeff tt p1 p2 k =
  \big[C.tadd tt /C.tzero]_(i < k.+1) C.tmul tt (nth C.tzero p1 i)
                                                (nth C.tzero p2 (k - i)).

Lemma tmul_trunc_nth 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)).

Lemma tmul_tail_nth 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 ExactSeqPolyMonomUp.

Module SeqPolyMonomUpInt (I : IntervalOps).
Module Int := FullInt I.
Include SeqPolyMonomUp Int.
End SeqPolyMonomUpInt.

Module SeqPolyMonomUpFloat (F : FloatOps with Definition even_radix := true).
Module Fl := MaskBaseF F.
Include SeqPolyMonomUp Fl.
End SeqPolyMonomUpFloat.

Module Type LinkIntXPr (I : IntervalOps).
Module Pol := SeqPolyMonomUpInt I.
Module PolX := ExactSeqPolyMonomUp FullXR.
Include LinkIntX I Pol PolX.
End LinkIntXPr.

Module LinkSeqPolyMonomUp (I : IntervalOps) <: LinkIntXPr I.
Module Import Pol := SeqPolyMonomUpInt I.
Module PolX := ExactSeqPolyMonomUp FullXR.

Local Coercion I.convert : I.type >-> interval. Definition contains_pointwise_until fi fx n : Prop :=
  forall k, k < n ->
  contains (I.convert (Pol.tnth fi k)) (PolX.tnth fx k).
Definition contains_pointwise fi fx : Prop :=
  Pol.tsize fi = PolX.tsize fx /\
  contains_pointwise_until fi fx (Pol.tsize fi).

Lemma link_tmul_trunc u fi gi fx gx:
  contains_pointwise fi fx ->
  contains_pointwise gi gx ->
  forall n, n < tsize fi -> n < tsize gi ->
  contains_pointwise_until
  (tmul_trunc u n fi gi) (PolX.tmul_trunc tt n fx gx) n.+1.

Lemma link_tmul_tail u fi gi fx gx:
  contains_pointwise fi fx ->
  contains_pointwise gi gx ->
  forall n,
  contains_pointwise_until (tmul_tail u n fi gi) (PolX.tmul_tail tt n fx gx)
  ((tsize fi).-1 + (tsize gi).-1 - n).

Lemma link_tsize_set_nth_nil n a b:
  PolX.tsize (PolX.tset_nth PolX.tpolyNil n a) =
  tsize (tset_nth tpolyNil n b).

Lemma link_tnth_set_nth_nil a b :
  contains (I.convert a) b ->
  forall k, k < tsize (tset_nth tpolyNil 0 a) ->
  contains (I.convert (tnth (tset_nth tpolyNil 0 a) k))
  (PolX.tnth (PolX.tset_nth PolX.tpolyNil 0 b) k).

End LinkSeqPolyMonomUp.