Library Flocq.Prop.Div_sqrt_error

This file is part of the Flocq formalization of floating-point arithmetic in Coq: https://flocq.gitlabpages.inria.fr/

This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Remainder of the division and square root are in the FLX format

From Coq Require Import ZArith Reals Psatz.

Require Import Core Operations Relative Sterbenz Mult_error.

Section Fprop_divsqrt_error.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Variable prec : Z.

Lemma generic_format_plus_prec :
  ∀ fexp, (∀ e, (fexp e ≤ e - prec)%Z) →
  ∀ x y (fx fy: float beta),
  (x = F2R fx)%R → (y = F2R fy)%R → (Rabs (x +y) < bpow (prec +Fexp fx))%R →
  (Rabs (x +y) < bpow (prec +Fexp fy))%R →
  generic_format beta fexp (x +y)%R.

Context { prec_gt_0_ : Prec_gt_0 prec }.

Notation format := (generic_format beta (FLX_exp prec)).
Notation cexp := (cexp beta (FLX_exp prec)).

Variable choice : Z → bool.

Remainder of the division in FLX

Theorem div_error_FLX :
  ∀ rnd { Zrnd : Valid_rnd rnd } x y,
  format x → format y →
  format (x - round beta (FLX_exp prec) rnd (x /y) × y)%R.

Remainder of the square in FLX (with p>1) and rounding to nearest

Variable Hp1 : Z.lt 1 prec.

Theorem sqrt_error_FLX_N :
  ∀ x, format x →
  format (x - Rsqr (round beta (FLX_exp prec) (Znearest choice) (sqrt x)))%R.

Lemma sqrt_error_N_FLX_aux1 x (Fx : format x) (Px : (0 < x)%R) :
  ∃ (mu : R) (e : Z ), (format mu ∧ x = mu × bpow (2 × e) :> R
                            ∧ 1 ≤ mu < bpow 2)%R.

Notation u_ro := (u_ro beta prec).

Lemma sqrt_error_N_FLX_aux2 x (Fx : format x) :
  (1 ≤ x)%R →
  (x = 1 :> R ∨ x = 1 + 2 × u_ro :> R ∨ 1 + 4 × u_ro ≤ x)%R.

Lemma sqrt_error_N_FLX_aux3 :
  (u_ro / sqrt (1 + 4 × u_ro) ≤ 1 - 1 / sqrt (1 + 2 × u_ro))%R.

Lemma om1ds1p2u_ro_pos : (0 ≤ 1 - 1 / sqrt (1 + 2 × u_ro))%R.

Lemma om1ds1p2u_ro_le_u_rod1pu_ro :
  (1 - 1 / sqrt (1 + 2 × u_ro) ≤ u_ro / (1 + u_ro ))%R.

Lemma s1p2u_rom1_pos : (0 ≤ sqrt (1 + 2 × u_ro) - 1)%R.

Theorem sqrt_error_N_FLX x (Fx : format x) :
  (Rabs (round beta (FLX_exp prec) (Znearest choice) (sqrt x) - sqrt x)
   ≤ (1 - 1 / sqrt (1 + 2 × u_ro)) × Rabs (sqrt x))%R.

Theorem sqrt_error_N_FLX_ex x (Fx : format x) :
  ∃ eps ,
  (Rabs eps ≤ 1 - 1 / sqrt (1 + 2 × u_ro))%R ∧
  round beta (FLX_exp prec) (Znearest choice) (sqrt x)
  = (sqrt x × (1 + eps ))%R.

Lemma sqrt_error_N_round_ex_derive :
  ∀ x rx,
  (∃ eps ,
   (Rabs eps ≤ 1 - 1 / sqrt (1 + 2 × u_ro))%R ∧ rx = (x × (1 + eps ))%R) →
  ∃ eps ,
  (Rabs eps ≤ sqrt (1 + 2 × u_ro) - 1)%R ∧ x = (rx × (1 + eps ))%R.

sqrt(1 + 2 u_ro) - 1 <= u_ro

Theorem sqrt_error_N_FLX_round_ex :
  ∀ x,
  format x →
  ∃ eps ,
  (Rabs eps ≤ sqrt (1 + 2 × u_ro) - 1)%R ∧
  sqrt x = (round beta (FLX_exp prec) (Znearest choice) (sqrt x) × (1 + eps ))%R.

Variable emin : Z.
Hypothesis Hemin : (emin ≤ 2 × (1 - prec ))%Z.

Theorem sqrt_error_N_FLT_ex :
  ∀ x,
  generic_format beta (FLT_exp emin prec) x →
  ∃ eps ,
  (Rabs eps ≤ 1 - 1 / sqrt (1 + 2 × u_ro))%R ∧
  round beta (FLT_exp emin prec) (Znearest choice) (sqrt x)
  = (sqrt x × (1 + eps ))%R.

sqrt(1 + 2 u_ro) - 1 <= u_ro

Theorem sqrt_error_N_FLT_round_ex :
  ∀ x,
  generic_format beta (FLT_exp emin prec) x →
  ∃ eps ,
  (Rabs eps ≤ sqrt (1 + 2 × u_ro) - 1)%R ∧
  sqrt x
  = (round beta (FLT_exp emin prec) (Znearest choice) (sqrt x) × (1 + eps ))%R.

End Fprop_divsqrt_error.

Section format_REM_aux.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Variable fexp : Z → Z.
Context { valid_exp : Valid_exp fexp }.
Context { monotone_exp : Monotone_exp fexp }.

Variable rnd : R → Z.
Context { valid_rnd : Valid_rnd rnd }.

Notation format := (generic_format beta fexp).

Lemma format_REM_aux:
  ∀ x y : R,
  format x → format y → (0 ≤ x)%R → (0 < y)%R →
  ((0 < x /y < /2)%R → rnd (x /y) = 0%Z) →
  format (x - IZR (rnd (x /y))×y).

End format_REM_aux.

Section format_REM.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Variable fexp : Z → Z.
Context { valid_exp : Valid_exp fexp }.
Context { monotone_exp : Monotone_exp fexp }.

Notation format := (generic_format beta fexp).

Theorem format_REM :
  ∀ rnd : R → Z, Valid_rnd rnd →
  ∀ x y : R,
  ((Rabs (x /y) < /2)%R → rnd (x /y)%R = 0%Z) →
  format x → format y →
  format (x - IZR (rnd (x /y)%R) × y).

Theorem format_REM_ZR:
  ∀ x y : R,
  format x → format y →
  format (x - IZR (Ztrunc (x /y)) × y).

Theorem format_REM_N :
  ∀ choice,
  ∀ x y : R,
  format x → format y →
  format (x - IZR (Znearest choice (x /y)) × y).

End format_REM.