Chebyshev Models in Coq

Mioara.Joldes@laas.fr

Florian.Steinberg@inria.fr

Laurent.Thery@inria.fr

Coq

         
    Check 1 + 2.
       1 + 2 : nat
         
    Compute 1 + 2.
       3 : nat
           
    Check addnC.
       addnC : forall x y : nat, x + y = y + x
   
    Check (addnC 1 2).
       addnC 1 2 : 1 + 2 = 2 + 1

Coq

         
    Check exp (1 + 2).
       exp (1 + 2) : R
                    
    Check exprD.
       exprD : forall x y : nat, exp (x + y) = exp x * exp y
   
    Compute exp (1 + 2).
       ???

Coq

Float \begin{array}{rcl} \\ \{ \texttt{num} : \mathbb{Z} ;\, \texttt{exp} : \mathbb{Z} \} & : & \textit{float} \\ \\ [ \{ \texttt{num} = n ;\, \texttt{exp} = e \} ]_f & = & n \times_r 2 ^ e : \mathbb{R} \\ \\ \forall\, f_1 f_2,\,\, [ f_1 +_f f_2 ]_f & = & [ f_1 ]_f +_r [ f_2 ]_f \\ \\ \end{array}

Coq

Interval \begin{array}{rcl} \\ \{ \texttt{l} : \textit{float} ;\, \texttt{r} : \textit{float} \} & : & \textit{interval} \\ \bot & : & \textit{interval} \\ \\ r \in \{ \texttt{l} = f_1 ;\, \texttt{r} = f_2 \} & \iff & [f_1]_f \le_r r \le_r [f_2]_f \\ r \in \bot & \iff & \textit{True} \\\\ \forall\, r\, i,\,\, r \in i & \Rightarrow & exp_r\, r \in exp_i\, i\\ \end{array}

Coq

Taylor Models

\begin{align*} e^x - 1 \approx x + 8388676 / 2^{24} x^2 + 11184876/2^{26} x^3 \end{align*}

             
  Lemma tang :
   forall x : R,
   -10831/1000000 <= x <= 10831/1000000 ->
   Rabs (exp x - 1 - 
         (x + 8388676 / 2^24 * x^2 + 11184876/2^26 * x^3))
    <= (23/27) / 2^33. 
  Proof.
  intros x H.
  interval with (i_bisect_taylor x 3, i_depth 8, i_prec 52).
  Qed.

Chebyshev Polynomials

Definition

$T_0 = 1$
$T_1 = x$
$T_{n+2} = 2x T_{n+1} - T_{n}$

Properties

$T_n.[1] = 1$ $\quad$ $T_n.[-1] = (-1) ^ n$
$ 2 x T_{n+1} = T_n + T_{n+2}$
$ 2 T_m T_n = T_{m + n} + T_{|m - n|}$

Chebyshev Polynomials

Definition

$[l]_c = \sum_{i = 1}^{\textit{size l}} l_i T_i$

Properties

$[l_1 +_c l_2]_c = [l_1]_c + [l_2]_c$
$[l_1 \times_c l_2]_c = [l_1]_c \times [l_2]_c$
$E_\textit{clenshaw}(l, x) = [l]_c . [x]$

Chebyshev Polynomials

Definition

$C_n(x) = cos (n\,\, acos(x))$

Properties

$T_n.[x] = C_n(x) \quad \textit{if} \quad -1 \le x \le 1 $

$${\small \int_{-1}^{1} T_m.[x] T_n.[x] / \sqrt{1 - x^2} \, dx = \begin{cases} 0\mbox{,} & \mbox{if }\quad m \neq n \\ \pi\mbox{,} & \mbox{if}\quad m = n = 0 \\ \pi/2\mbox{,} & \mbox{if}\quad m = n \neq 0 \\ \end{cases}}$$

Interpolation

Definition

${\small \textit{i}([], f) = 0}$
${\small \textit{i}(a :: l, f) = \textit{i}(l,f) + (f(a) - \textit{i}(l,f).[a])/\prod_{j \in l}(a - j) \,\, \prod_{j \in l}(x - j)}$

Properties

${\small i(l,f).[a] = f(a) \quad \textit{if} \quad a \in l}$

$${\small \exists z, |f(x) - i(l,f).[x]| \le 1 / \textit{size}(l)! \,\, f'^{(\textit{size}(l))}(z) \,\, \prod_{j \in l} (x - j)}$$

Interpolation

Lemma ierror_val : 
forall (f : R -> R) (n : nat) (l : seq R),
 n = size l ->
 uniq l ->
forall a b c1 c2 : R,
  c1 < a ->
  b < c2 ->
 (forall x : R, x \in l -> a <= x <= b) ->
 (forall (x : R) (k : nat),
   c1 < x < c2 -> k <= n -> ex_derive_n f k x) ->
 (forall (x : R) (k : nat),
  k <= n -> a <= x <= b -> continuous (Derive_n f k) x) ->
forall x : R,
  a <= x <= b ->
  ierror f l x != 0 ->
  exists z : R,
    a <= z <= b /\
    ierror f l x = 1 / n`! * Derive_n f n z * (prodl l).[x]

Interpolation on Chebyshev nodes

Definition

${\small l_c = [cos ((2i + 1)\,\pi\, /\, 2n) \quad | \quad 0 \le i < n]}$

Properties

$${\small |f(x) - i(l_c,f).[x]| \le \textit{max}_{-1 \le z \le 1} |f'^{n}(z)| \,\, / (2^{n-1} n!) }$$

$${\small |f(x) - i(l_c,f).[x]| \le \textit{max} \left(\begin{array}{l} |f(x) - i(l_c,f).[1]| \\ |f(x) - i(l_c,f).[-1]| \end{array}\right) }$$

Interpolation on Chebyshev nodes

Lemma ierror_cheby :
forall (f : R -> R) (c1 c2 : R),
  c1 < -1 ->
  1 < c2 ->
forall n : nat,
  (forall (x : R) (k : nat),
     c1 < x < c2 -> k <= n -> ex_derive_n f k x) ->
  (forall (x : R) (k : nat),
     k <= n -> -1 <= x <= 1 -> continuous (Derive_n f k) x) ->
forall x z : R,
 -1 <= x <= 1 ->
 (forall y : R, -1 <= y <= 1 -> Rabs (Derive_n f n y) <= z) ->
 Rabs (ierror f (cheby_nodes n) x) <= 1 / (2 ^ n.-1 * n`!) * z

Interpolation on Chebyshev nodes

Lemma interpolation_cheby_ge : 
  forall (n : nat) (c1 c2 : R) (f : R -> R) (x : R),
    c1 < -1 ->
    1 < c2 ->
    -1 <= x <= 1 ->
  (forall (m : nat) (x0 : R),
    (m <= n.+1)%N -> -1 <= x0 <= 1 -> 
    continuous (Derive_n f m) x0) ->
  (forall x0 : R, -1 <= x0 <= 1 -> Derive_n f n.+1 x0 <= 0) \/
  (forall x0 : R, -1 <= x0 <= 1 -> Derive_n f n.+1 x0 >= 0) ->
  (forall (m : nat) (x0 : R), 
    (m <= n.+1)%N -> c1 < x0 < c2 -> ex_derive_n f m x0) ->
  Rabs (ierror f (cheby_nodes n) x) <=
  Rmax (Rabs (ierror f (cheby_nodes n) (-1))) 
       (Rabs (ierror f (cheby_nodes n) 1))

Chebyshev Models

$$ \{ P : \textit{seq}\,\, \textit{interval};\,\, Delta : \textit{interval} \} : \textit{cms}$$
$$ \textit{correct}(a,b,n,f,\{P = P;\, Delta = D\}) \iff $$
$$ \begin{array}{lr} size(P) = n + 1 & \land \\ \exists p : \textit{seq}\,\, \mathbb{R}, \\ \quad \begin{array}{lr} \textit{size(p)} = n +1 & \land \\ \forall i,\,\, p_i \in P_i & \land \\ \forall x : \mathbb{R}, [a]_f \le x \le [b]_f \Rightarrow \\ \qquad\quad\exists d : \mathbb{R},\,\, d \in D \land f(x) = [p]_c.[x] + d \end{array} \end{array} $$

Chebyshev Models

$$ \textit{error}_\textit{cms} = \{ P = [0\dots 0],\,\, Delta = \bot \}$$
$$ \textit{correct}(a,b,n,f, \textit{error}_\textit{cms})$$
$$ \{ P = P_1,\,\, Delta = D_1 \} +_{\textit{cms}} \{ P = P_2,\,\, Delta = D_2 \}$$ $$ = \{ P = P_1 +_c P_2,\,\, Delta = D_1 +_I D_2 \} $$
$$ \begin{array}{l} \textit{correct}(a,b,n,f_1, cms_1) \land \textit{correct}(a,b,n,f_2, cms_2) \Rightarrow \\ \textit{correct}(a,b,n,f_1 + f_2, cms_1 +_{\textit{cms}} cms_2) \end{array} $$

Chebyshev Models

$$ {\small \begin{array}{rcl} e_1 +_e e_2 &:& expr \\ e_1 -_e e_2 &:& expr\\ e_1 *_e e_2 &:& expr\\ e_1 /_e e_2 &:& expr\\ e_1 \,o_e\, e_2 &:& expr\\ x &:& expr\\ \textit{const}(c_1,c_2) &:& expr\\ ln(x), sqrt(x), exp(x), 1/x, sin(x), cos(x) &:& expr \end{array} } $$

Chebyshev Models

$$ [e_1 +_e e_2]_{\mathbb{R}} = [e_1]_{\mathbb{R}} + [e_2]_{\mathbb{R}}$$
$$ [e_1 +_e e_2]_\textit{cms} = [e_1]_\textit{cms} +_\textit{cms} [e_2]_\textit{cms}$$
$$ \forall e : \textit{expr},\,\, \textit{correct}(a,b,n,[e]_\mathbb{R}, [e]_\textit{cms})$$

Chebyshev Models

$${\small \begin{array}{|l|l|l|} \hline f(x), I, n & \textit{Sollya} & \textit{Coq} \cr \hline \textit{sin}(x),[3,4], 10 & 1,19.10^{-14} & 1,19.10^{-14} \cr \hline \textit{exp}(1/\textit{cos}(x)),[0,1], 14 & 5.22.10^{-7} & 1.62.10^{-6} \cr \hline \textit{exp}(x)/(\textit{log}(2 + x) \textit{cos}(x)), [0; 1], 15 & 4.86.10^{-9} & 5.20.10^{-9}\cr \hline \textit{sin}(\textit{exp}(x)), [-1; 1], 10 & 2.53.10^{-5} & 9.96.10^{-6} \cr \hline \sqrt{x + 1.00001}, [-1; 0], 10 & 4.25.10^{-2} & 4.25.10^{-2} \cr \hline \sqrt{x + 1.00001} . \textit{sin}(x), [-1; 0], 10 & 3.89.10^{-2} & 3.89.10^{-2} \cr \hline 1/(1 + 4 . x^2), [-1, 1], 10 & 1.13.10^{-2} & 2.97.10^{-2} \cr \hline \textit{sin}^2(x) + \textit{cos}^2(x), [-1, 1], 10 & 3.92.10^{-9} & 3.92.10^{-9} \cr \hline \end{array}}$$

Definition tang :=
   exp(x) - 1 - (x + c(8388676, 2^24) * x * x
                     + c(11184876, 2^26) * x * x * x).

Lemma tang_correct :
 forall x,
 (-10831 / 1000000 <= x <= 10831 / 1000000) ->
  (-23 / (27 * 2^33)) <= 
    (exp x - 1 - (x + 8388676/ 2^24 * x * x 
                    + 11184876 / 2^26 * x * x * x))
                      <= 23 / (27 * 2^33).
Proof.
move=> x H.
cheby_solve_tac 52 7 3 tang H. 
Qed.

Conclusions

Reference Implementation
Almost straightforward translation
40 pages (x 40 lines) = 8600 lines of Coq
Still a prototype:
https://github.com/FlorianSteinberg/Cheby
More functions (arctan)
Integration