Library Interval.Eval.Eval

This file is part of the Coq.Interval library for proving bounds of real-valued expressions in Coq: https://coqinterval.gitlabpages.inria.fr/
Copyright (C) 2007-2016, 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.

From Coq Require Import Bool Reals.
From Flocq Require Import Zaux Raux.
From Coq Require Import List.
From Coquelicot Require Import Coquelicot.
From mathcomp.ssreflect Require Import ssreflect.

Require Import Stdlib.
Require Import Coquelicot.
Require Import Xreal.
Require Import Xreal_derive.
Require Import Basic.
Require Import Interval.
Require Import Interval_compl.
Require Import Taylor_model.
Require Import Tree.
Require Import Prog.

Definition no_floor_op op :=
  match op with
  | Nearbyint _false
  | RoundFlt _ _ _ | ErrorFlt _ _ _false
  | RoundFix _ _ | ErrorFix _ _false
  | _true
  end.

Definition no_floor_term term :=
  match term with Unary op _no_floor_op op | _true end.

Definition no_floor_prog prog :=
  fold_left (fun r tr && no_floor_term t) prog true.

Lemma no_floor_prog_cons t prog :
  no_floor_prog (t :: prog) = no_floor_term t && no_floor_prog prog.

Lemma no_floor_prog_rcons t prog :
  no_floor_prog (prog ++ (t :: nil)) = no_floor_term t && no_floor_prog prog.

Lemma no_floor_prog_rev prog :
  no_floor_prog (rev prog) = no_floor_prog prog.

Definition ext_operations :=
  Build_operations (fun xXreal (IZR x)) Xnan
   (fun o
    match o with
    | NegXneg
    | AbsXabs
    | InvXinv
    | SqrXsqr
    | SqrtXsqrt
    | CosXcos
    | SinXsin
    | TanXtan
    | AtanXatan
    | ExpXexp
    | LnXln
    | PowerInt nfun xXpower_int x n
    | Nearbyint mXnearbyint m
    | RoundFlt m emin precXround_flt m emin prec
    | ErrorFlt m emin precXerror_flt m emin prec
    | RoundFix m eminXround_fix m emin
    | ErrorFix m eminXerror_fix m emin
    end)
   (fun o
    match o with
    | AddXadd
    | SubXsub
    | MulXmul
    | DivXdiv
    end)
   (fun xXcmp x (Xreal 0)).

Definition eval_ext :=
  eval_generic ext_operations.

Theorem eval_inductive_prop_fun :
   {T} A B P (opsA : operations A) (opsB : operations B),
 ( a1 a2, ( x : T, a1 x = a2 x) b, P a1 b P a2 b)
 ( o a b, P a b P (fun xunary opsA o (a x)) (unary opsB o b))
 ( o a1 a2 b1 b2, P a1 b1 P a2 b2 P (fun xbinary opsA o (a1 x) (a2 x)) (binary opsB o b1 b2))
   inpA inpB,
 ( n, P (fun xnth n (inpA x) (unknown opsA)) (nth n inpB (unknown opsB)))
   prog,
   n, P (fun xnth n (eval_generic opsA prog (inpA x)) (unknown opsA)) (nth n (eval_generic opsB prog inpB) (unknown opsB)).

Theorem eval_inductive_prop_floor_fun :
   {T} A B P (opsA : operations A) (opsB : operations B),
 ( a1 a2, ( x : T, a1 x = a2 x) b, P a1 b P a2 b)
 ( o a b, no_floor_op o = true P a b P (fun xunary opsA o (a x)) (unary opsB o b))
 ( o a1 a2 b1 b2, P a1 b1 P a2 b2 P (fun xbinary opsA o (a1 x) (a2 x)) (binary opsB o b1 b2))
   inpA inpB,
 ( n, P (fun xnth n (inpA x) (unknown opsA)) (nth n inpB (unknown opsB)))
   prog, no_floor_prog prog = true
   n, P (fun xnth n (eval_generic opsA prog (inpA x)) (unknown opsA)) (nth n (eval_generic opsB prog inpB) (unknown opsB)).

Lemma rewrite_inv_diff :
   u u',
  Xmul u' (Xneg (Xsqr (Xinv u))) = Xneg (Xdiv u' (Xsqr u)).

Lemma rewrite_div_diff :
   u v u' v',
  Xdiv (Xsub u' (Xmul v' (Xdiv u v))) v = Xdiv (Xsub (Xmul u' v) (Xmul v' u)) (Xmul v v).

Lemma nth_map :
   {T U} d' n (f : T U) l d,
  nth n (map f l) d =
    match le_lt_dec (length l) n with left _d | right _f (nth n l d') end.

Lemma nth_map_lt :
   {T U} d' n (f : T U) l d,
  (n < length l)%nat
  nth n (map f l) d = f (nth n l d').

Lemma xreal_to_real :
   (P1 : ExtendedR Prop) (P2 : R Prop),
  (P1 Xnan r, P2 r)
  ( r, P1 (Xreal r) P2 r)
   prog terms n,
  P1 (nth n (eval_ext prog (map Xreal terms)) Xnan)
  P2 (nth n (eval_real prog terms) 0%R).

Lemma continuous_unary :
   unop a b x,
  no_floor_op unop = true
  (notXnan b b = Xreal (a x) continuous a x)
  notXnan (unary ext_operations unop b)
  unary ext_operations unop b = Xreal (unary real_operations unop (a x))
  continuous (fun x0 : Runary real_operations unop (a x0)) x.

Fixpoint change_nth {T} n (l : list T) f {struct l} :=
  match l with
  | nilnil
  | h :: t
    match n with
    | Of h :: t
    | S nh :: change_nth n t f
    end
  end.

Lemma change_nth_correct :
   {T} n m (l : list T) d f,
  ((n < length l)%nat n = m nth n (change_nth m l f) d = f (nth n l d))
  nth n (change_nth m l f) d = nth n l d.

Lemma length_change_nth :
   {T} n (l : list T) f,
  length (change_nth n l f) = length l.

Module IntervalAlgos (I : IntervalOps).

Module J := IntervalExt I.

Definition contains_all xi x :=
  length xi = length x
   n, contains (I.convert (nth n xi I.nai)) (Xreal (nth n x 0)).

Definition bisect_step (bounds : list I.type) i (check : list I.type bool) cont :=
  if check bounds then true
  else
    let bounds' := change_nth i bounds (fun xifst (I.bisect xi)) in
    match cont bounds' with
    | true
      let bounds' := change_nth i bounds (fun xisnd (I.bisect xi)) in
      cont bounds'
    | falsefalse
    end.

Fixpoint bisect bounds idx check steps { struct steps } :=
  match steps, idx with
  | O, _check bounds
  | S _, nilcheck bounds
  | S steps, i :: idx
    let idx := app idx (i :: nil) in
    bisect_step bounds i check (fun bbisect b idx check steps)
  end.

Theorem bisect_correct :
   steps bounds idx check (P : _ Prop),
  ( xi x, contains_all xi x
    check xi = true P x )
  bisect bounds idx check steps = true
   x,
  contains_all bounds x
  P x.

Definition lookup_step fi (bounds : list I.type) i output cont :=
  if I.subset (fi bounds) output then output
  else
    let bounds' := change_nth i bounds (fun xifst (I.bisect xi)) in
    let output := cont bounds' output in
    if I.lower_bounded output || I.upper_bounded output then
      let bounds' := change_nth i bounds (fun xisnd (I.bisect xi)) in
      cont bounds' output
    else output.

Fixpoint lookup_main fi bounds idx output steps { struct steps } :=
  match steps, idx with
  | O, _I.join (fi bounds) output
  | S _, nilI.join (fi bounds) output
  | S steps, i :: idx
    let idx := app idx (i :: nil) in
    lookup_step fi bounds i output
      (fun bounds outputlookup_main fi bounds idx output steps)
  end.

Fixpoint lookup_piece bounds idx steps { struct steps } :=
  match steps, idx with
  | O, _bounds
  | S _, nilbounds
  | S steps, i :: idx
    let idx := app idx (i :: nil) in
    let bounds := change_nth i bounds (fun xifst (I.bisect xi)) in
    lookup_piece bounds idx steps
  end.

Definition lookup fi bounds idx extend steps :=
  let bounds' := lookup_piece bounds idx steps in
  let output := extend (fi bounds') in
  if I.lower_bounded output || I.upper_bounded output then
    lookup_main fi bounds idx output steps
  else output.

Lemma continuous_eval_ext :
   prog vars x m,
  no_floor_prog prog = true
  notXnan (nth m (eval_ext prog (Xreal x :: map Xreal vars)) Xnan)
  continuous (fun xnth m (eval_real prog (x :: vars)) 0%R) x.

Lemma contains_map_Xreal :
   xi x,
  contains_all xi x
   n,
  contains (I.convert (nth n xi I.nai)) (nth n (map Xreal x) Xnan).

Lemma contains_all_cons :
   li l xi x,
  contains_all li l
  contains (I.convert xi) (Xreal x)
  contains_all (xi :: li) (x :: l).

Module BndValuator.

Definition operations prec :=
  Build_operations (I.fromZ prec) I.nai
   (fun o
    match o with
    | NegI.neg
    | AbsI.abs
    | InvI.inv prec
    | SqrI.sqr prec
    | SqrtI.sqrt prec
    | CosI.cos prec
    | SinI.sin prec
    | TanI.tan prec
    | AtanI.atan prec
    | ExpI.exp prec
    | LnI.ln prec
    | PowerInt nfun xI.power_int prec x n
    | Nearbyint mI.nearbyint m
    | RoundFlt m emin pJ.round_flt prec m emin p
    | ErrorFlt m emin pI.error_flt prec m emin p
    | RoundFix m eminJ.round_fix prec m emin
    | ErrorFix m eminI.error_fix prec m emin
    end)
   (fun o
    match o with
    | AddI.add prec
    | SubI.sub prec
    | MulI.mul prec
    | DivI.div prec
    end)
    I.sign_strict.

Definition eval prec :=
  eval_generic (operations prec).

Lemma eval_correct_aux :
   prec prog bounds vars,
 ( n, contains (I.convert (nth n bounds I.nai)) (nth n vars Xnan))
   n,
  contains (I.convert (nth n (eval prec prog bounds) I.nai))
   (nth n (eval_ext prog vars) Xnan).

Theorem eval_correct :
   prec prog bounds vars,
  contains_all bounds vars
   n,
  contains
    (I.convert (nth n (eval prec prog bounds) I.nai))
    (nth n (eval_ext prog (map Xreal vars)) Xnan).

Theorem eval_correct' :
   prec prog bounds vars,
  contains_all bounds vars
   n,
  contains
    (I.convert (nth n (eval prec prog bounds) I.nai))
    (Xreal (nth n (eval_real prog vars) 0%R)).

Theorem eval_correct_ext :
   prec prog bounds vars,
  contains_all bounds vars
   n,
  I.extension
    (fun xnth n (eval_ext prog (x :: map Xreal vars)) Xnan)
    (fun bnth n (eval prec prog (b :: bounds)) I.nai).

Theorem eval_correct_ext' :
   prec prog bounds vars,
  contains_all bounds vars
   xi x,
  contains (I.convert xi) (Xreal x)
   n,
  contains
    (I.convert (nth n (eval prec prog (xi :: bounds)) I.nai))
    (Xreal (nth n (eval_real prog (x :: vars)) 0%R)).

Lemma continuous_eval :
   prec prog bounds vars,
  contains_all bounds vars
  no_floor_prog prog = true
   xi x,
  contains (I.convert xi) (Xreal x)
   m,
  I.convert (nth m (eval prec prog (xi :: bounds)) I.nai) Inan
  continuous (fun xnth m (eval_real prog (x :: vars)) 0%R) x.

Lemma ex_RInt_eval :
   prec prog bounds vars,
  contains_all bounds vars
  no_floor_prog prog = true
   a b xi,
  ( x, Rmin a b x Rmax a b contains (I.convert xi) (Xreal x))
   m,
  I.convert (nth m (eval prec prog (xi :: bounds)) I.nai) Inan
  ex_RInt (fun xnth m (eval_real prog (x :: vars)) R0) a b.

End BndValuator.

Module DiffValuator.

Definition diff_operations A (ops : @operations A) :=
  Build_operations
   (fun x(constant ops x, constant ops 0))
   (unknown ops, unknown ops)
   (fun o x
    match x with
    | (v, d)
      match o with
      | Neglet f := unary ops Neg in (f v, f d)
      | Abslet w := unary ops Abs v in (w,
        match sign ops v with Xltunary ops Neg d | Xgtd | _unknown ops end)
      | Invlet w := unary ops Inv v in (w,
        binary ops Mul d (unary ops Neg (unary ops Sqr w)))
      | Sqrlet w := binary ops Mul d v in (unary ops Sqr v, binary ops Add w w)
      | Sqrtlet w := unary ops Sqrt v in (w,
        binary ops Div d (binary ops Add w w))
      | Cos(unary ops Cos v,
        binary ops Mul d (unary ops Neg (unary ops Sin v)))
      | Sin(unary ops Sin v,
        binary ops Mul d (unary ops Cos v))
      | Tanlet w := unary ops Tan v in (w,
        binary ops Mul d (binary ops Add (constant ops 1) (unary ops Sqr w)))
      | Atan(unary ops Atan v,
        binary ops Div d (binary ops Add (constant ops 1) (unary ops Sqr v)))
      | Explet w := unary ops Exp v in (w,
        binary ops Mul d w)
      | Ln(unary ops Ln v,
        match sign ops v with Xgtbinary ops Div d v | _unknown ops end)
      | PowerInt n
        (unary ops o v, binary ops Mul d (binary ops Mul (constant ops n) (unary ops (PowerInt (n-1)) v)))
      | Nearbyint m(unary ops (Nearbyint m) v, unknown ops)
      | RoundFlt m emin prec(unary ops (RoundFlt m emin prec) v, unknown ops)
      | ErrorFlt m emin prec(unary ops (ErrorFlt m emin prec) v, unknown ops)
      | RoundFix m emin(unary ops (RoundFix m emin) v, unknown ops)
      | ErrorFix m emin(unary ops (ErrorFix m emin) v, unknown ops)
      end
    end)
   (fun o x y
    match x, y with
    | (vx, dx), (vy, dy)
      match o with
      | Addlet f := binary ops Add in (f vx vy, f dx dy)
      | Sublet f := binary ops Sub in (f vx vy, f dx dy)
      | Mullet f := binary ops Mul in (f vx vy,
        binary ops Add (f dx vy) (f dy vx))
      | Divlet f := binary ops Div in
        let w := f vx vy in
        (w, f (binary ops Sub dx (binary ops Mul dy w)) vy)
      end
    end)
   (fun xmatch x with (vx, _)sign ops vx end).

Lemma unary_diff_correct :
   o f d x,
  Xderive_pt f x d
  let v := unary (diff_operations _ ext_operations) o (f x, d) in
  unary ext_operations o (f x) = fst v
  Xderive_pt (fun x0unary ext_operations o (f x0)) x (snd v).

Lemma binary_diff_correct :
   o f1 f2 d1 d2 x,
  Xderive_pt f1 x d1
  Xderive_pt f2 x d2
  let v := binary (diff_operations _ ext_operations) o (f1 x, d1) (f2 x, d2) in
  binary ext_operations o (f1 x) (f2 x) = fst v
  Xderive_pt (fun x0binary ext_operations o (f1 x0) (f2 x0)) x (snd v).

Lemma eval_diff_correct :
   prog terms n x,
  let v := nth n (eval_generic (diff_operations _ ext_operations) prog ((x, Xmask (Xreal 1) x) :: map (fun v(Xreal v, Xmask (Xreal 0) x)) terms)) (Xnan, Xnan) in
  nth n (eval_ext prog (x :: map Xreal terms)) Xnan = fst v
  Xderive_pt (fun xnth n (eval_ext prog (x :: map Xreal terms)) Xnan) x (snd v).

Lemma unary_diff_bnd_correct :
   prec o f f',
  let u x := unary (diff_operations _ ext_operations) o (f x, f' x) in
   yi yi' xi,
 ( x, contains xi x contains (I.convert yi) (f x))
 ( x, contains xi x contains (I.convert yi') (f' x))
  let v := unary (diff_operations _ (BndValuator.operations prec)) o (yi, yi') in
 ( x, contains xi x contains (I.convert (snd v)) (snd (u x))).

Lemma binary_diff_bnd_correct :
   prec o f1 f2 f1' f2',
  let u x := binary (diff_operations _ ext_operations) o (f1 x, f1' x) (f2 x, f2' x) in
   yi1 yi2 yi1' yi2' xi,
 ( x, contains xi x contains (I.convert yi1) (f1 x))
 ( x, contains xi x contains (I.convert yi2) (f2 x))
 ( x, contains xi x contains (I.convert yi1') (f1' x))
 ( x, contains xi x contains (I.convert yi2') (f2' x))
  let v := binary (diff_operations _ (BndValuator.operations prec)) o (yi1, yi1') (yi2, yi2') in
 ( x, contains xi x contains (I.convert (snd v)) (snd (u x))).

Lemma eval_diff_bnd_correct :
   prec prog bounds vars,
  contains_all bounds vars
   n,
  let ff' x := nth n (eval_generic (diff_operations _ ext_operations) prog ((x, Xmask (Xreal 1) x) :: map (fun v(Xreal v, Xmask (Xreal 0) x)) vars)) (Xnan, Xnan) in
  let ffi' xi := nth n (eval_generic (diff_operations _ (BndValuator.operations prec)) prog
    ((xi, I.mask (I.fromZ_small 1) xi) :: map (fun b(b, I.mask I.zero xi)) bounds)) (I.nai, I.nai) in
   xi,
  nth n (BndValuator.eval prec prog (xi :: bounds)) I.nai = fst (ffi' xi)
 ( x, contains (I.convert xi) x contains (I.convert (snd (ffi' xi))) (snd (ff' x))).

Definition diff_refining_points prec xi di yi yi' ym yl yu :=
  match I.sign_large yi' with
  | Xund
    if I.bounded yi' then
      I.meet yi (I.add prec ym (I.mul prec di yi'))
    else yi
  | Xeqym
  | Xlt
    I.meet
     (if I.lower_bounded xi then I.lower_extent yl
      else I.whole)
     (if I.upper_bounded xi then I.upper_extent yu
      else I.whole)
  | Xgt
    I.meet
     (if I.lower_bounded xi then I.upper_extent yl
      else I.whole)
     (if I.upper_bounded xi then I.lower_extent yu
      else I.whole)
  end.

Definition diff_refining prec xi yi yi' fi :=
  match I.sign_large yi' with
  | Xund
    if I.bounded yi' then
      let mi := J.midpoint xi in
      I.meet yi
       (I.add prec (fi mi) (I.mul prec (I.sub prec xi mi) yi'))
    else yi
  | Xeq
    fi (J.midpoint xi)
  | Xlt
    I.meet
     (if I.lower_bounded xi then
        let l := I.lower xi in
        I.lower_extent (fi (I.bnd l l))
      else I.whole)
     (if I.upper_bounded xi then
        let u := I.upper xi in
        I.upper_extent (fi (I.bnd u u))
      else I.whole)
  | Xgt
    I.meet
     (if I.lower_bounded xi then
        let l := I.lower xi in
        I.upper_extent (fi (I.bnd l l))
      else I.whole)
     (if I.upper_bounded xi then
      let u := I.upper xi in
        I.lower_extent (fi (I.bnd u u))
      else I.whole)
  end.

Lemma diff_refining_aux_0 :
   f f' xi yi',
  Xderive f f'
  I.sign_large yi' Xund
 ( x, contains xi x contains (I.convert yi') (f' x))
   x, contains xi x
  x = Xreal (proj_val x)
   v,
  f x = Xreal (proj_fun v f (proj_val x))
  f' x = Xreal (proj_fun v f' (proj_val x)).

Lemma diff_refining_aux_1 :
   prec f f' xi yi' m mi ymi,
  Xderive f f'
  contains (I.convert mi) (Xreal m)
  contains (I.convert xi) (Xreal m)
  contains (I.convert ymi) (f (Xreal m))
 ( x, contains (I.convert xi) x contains (I.convert yi') (f' x))
   x, contains (I.convert xi) x
  contains (I.convert (I.add prec ymi (I.mul prec (I.sub prec xi mi) yi'))) (f x).

Lemma diff_refining_aux_2 :
   f f' xi m ymi,
  Xderive f f'
  contains xi (Xreal m)
  contains ymi (f (Xreal m))
 ( x, contains xi x contains (Ibnd (Xreal 0) (Xreal 0)) (f' x))
   x, contains xi x
  contains ymi (f x).

Theorem diff_refining_points_correct :
   prec f f' xi yi yi' ym yl yu,
  Xderive f f'
 ( x, contains (I.convert xi) x contains (I.convert yi) (f x))
 ( x, contains (I.convert xi) x contains (I.convert yi') (f' x))
  contains (I.convert ym) (f (I.F.convert (I.midpoint xi)))
 (if I.lower_bounded xi then
    contains (I.convert yl) (f (I.F.convert (I.lower xi)))
  else True)
 (if I.upper_bounded xi then
    contains (I.convert yu) (f (I.F.convert (I.upper xi)))
  else True)
   x, contains (I.convert xi) x
  contains (I.convert (diff_refining_points prec xi (I.sub prec xi (J.midpoint xi)) yi yi' ym yl yu)) (f x).

Lemma convert_bnd :
   l u v, contains (Ibnd l u) (I.F.convert v)
  contains (I.convert (I.bnd v v)) (I.F.convert v).

Theorem diff_refining_correct :
   prec f f' fi fi',
  I.extension f fi
  I.extension f' fi'
  Xderive f f'
  I.extension f (fun bdiff_refining prec b (fi b) (fi' b) fi).

Definition eval prec formula bounds n xi :=
  match nth n (eval_generic (diff_operations _ (BndValuator.operations prec)) formula
    ((xi, I.mask (I.fromZ_small 1) xi) :: map (fun b(b, I.mask I.zero xi)) bounds)) (I.nai, I.nai) with
  | (yi, yi')
    diff_refining prec xi yi yi'
      (fun bnth n (BndValuator.eval prec formula (b :: bounds)) I.nai)
  end.

Theorem eval_correct_ext :
   prec prog bounds vars,
  contains_all bounds vars
   n,
  I.extension
    (fun xnth n (eval_ext prog (x :: map Xreal vars)) Xnan)
    (fun beval prec prog bounds n b).

Theorem eval_correct :
   prec prog bounds vars,
  contains_all bounds vars
   n xi x,
  contains (I.convert xi) (Xreal x)
  contains (I.convert (eval prec prog bounds n xi))
    (Xreal (nth n (eval_real prog (x :: vars)) 0%R)).

Definition root prec formula bounds xi :=
  match nth 0 (eval_generic (diff_operations _ (BndValuator.operations prec)) formula
    ((xi, I.mask (I.fromZ_small 1) xi) :: map (fun b(b, I.mask I.zero xi)) bounds)) (I.nai, I.nai) with
  | (yi, yi')
    match I.sign_strict yi with
    | Xlt | XgtI.empty
    | _
      let mi := J.midpoint xi in
      let yi := nth 0 (BndValuator.eval prec formula (mi :: bounds)) I.nai in
      I.meet xi (I.sub prec mi (I.div prec yi yi'))
    end
  end.

Theorem root_correct_ext :
   prec prog bounds vars,
  contains_all bounds vars
   xi x,
  contains (I.convert xi) x
  nth 0 (eval_ext prog (x :: map Xreal vars)) Xnan = Xreal 0
  contains (I.convert (root prec prog bounds xi)) x.

Theorem root_correct :
   prec prog bounds vars,
  contains_all bounds vars
   xi x,
  contains (I.convert xi) (Xreal x)
  nth 0 (eval_real prog (x :: vars)) 0%R = 0%R
  contains (I.convert (root prec prog bounds xi)) (Xreal x).

End DiffValuator.

Module TaylorValuator.

Module TM := TM I.

Definition operations prec deg xi :=
  Build_operations
   (fun _TM.dummy)
   TM.dummy
   (fun o
    match o with
    | NegTM.opp (prec, deg) xi
    | AbsTM.abs (prec, deg) xi
    | InvTM.inv (prec, deg) xi
    | SqrTM.sqr (prec, deg) xi
    | SqrtTM.sqrt (prec, deg) xi
    | CosTM.cos (prec, deg) xi
    | SinTM.sin (prec, deg) xi
    | TanTM.tan (prec, deg) xi
    | AtanTM.atan (prec, deg) xi
    | ExpTM.exp (prec, deg) xi
    | LnTM.ln (prec, deg) xi
    | PowerInt nTM.power_int n (prec, deg) xi
    | Nearbyint mTM.nearbyint m (prec, deg) xi
    | RoundFlt m emin pTM.round_flt (prec, deg) m emin p xi
    | ErrorFlt m emin pTM.error_flt (prec, deg) m emin p xi
    | RoundFix m eminTM.round_fix (prec, deg) m emin xi
    | ErrorFix m eminTM.error_fix (prec, deg) m emin xi
    end)
   (fun o
    match o with
    | AddTM.add (prec, deg) xi
    | SubTM.sub (prec, deg) xi
    | MulTM.mul (prec, deg) xi
    | DivTM.div (prec, deg) xi
    end)
   (fun _Xund) .

Definition eval prec deg xi :=
  eval_generic (operations prec deg xi).

Theorem eval_correct_aux :
   prec deg prog bounds vars,
  contains_all bounds vars
   n xi,
  TM.approximates xi
    (nth n (eval prec deg xi prog (TM.var :: map TM.const bounds)) TM.dummy)
    (fun xnth n (eval_ext prog (Xreal x :: map Xreal vars)) Xnan).

Theorem eval_correct_aux' :
   prec deg prog bounds vars,
  contains_all bounds vars
   n xi,
  TM.approximates xi
    (nth n (eval prec deg xi prog (TM.var :: map TM.const bounds)) TM.dummy)
    (fun xXreal (nth n (eval_real prog (x :: vars)) 0)).

Theorem eval_correct_ext :
   prec deg prog bounds vars,
  contains_all bounds vars
   n yi,
  I.extension
    (Xbind (fun xnth n (eval_ext prog (Xreal x :: map Xreal vars)) Xnan))
    (fun bTM.eval (prec,deg) (nth n (eval prec deg yi prog (TM.var :: map TM.const bounds)) TM.dummy) yi b).

Theorem eval_correct :
   prec deg prog bounds vars,
  contains_all bounds vars
   n yi xi x,
  contains (I.convert xi) (Xreal x)
  contains (I.convert (TM.eval (prec,deg) (nth n (eval prec deg yi prog (TM.var :: map TM.const bounds)) TM.dummy) yi xi))
    (Xreal (nth n (eval_real prog (x :: vars)) 0%R)).

End TaylorValuator.

End IntervalAlgos.