Upgrade to flocq 2.4.0

2 files changed, 71 insertions, 0 deletions

diff --git a/flocq/Prop/Fprop_plus_error.v b/flocq/Prop/Fprop_plus_error.v
index ddae698c..950ca267 100644
--- a/flocq/Prop/Fprop_plus_error.v
+++ b/flocq/Prop/Fprop_plus_error.v
@@ -23,8 +23,12 @@ Require Import Fcore_Raux.
 Require Import Fcore_defs.
 Require Import Fcore_float_prop.
 Require Import Fcore_generic_fmt.
+Require Import Fcore_FIX.
+Require Import Fcore_FLX.
+Require Import Fcore_FLT.
 Require Import Fcalc_ops.
 
+
 Section Fprop_plus_error.
 
 Variable beta : radix.
@@ -232,3 +236,34 @@ apply Ropp_involutive.
 Qed.
 
 End Fprop_plus_zero.
+
+Section Fprop_plus_FLT.
+Variable beta : radix.
+
+Notation bpow e := (bpow beta e).
+
+Variable emin prec : Z.
+Context { prec_gt_0_ : Prec_gt_0 prec }.
+
+Theorem FLT_format_plus_small: forall x y,
+  generic_format beta (FLT_exp emin prec) x ->
+  generic_format beta (FLT_exp emin prec) y ->
+   (Rabs (x+y) <= bpow (prec+emin))%R ->
+    generic_format beta (FLT_exp emin prec) (x+y).
+Proof with auto with typeclass_instances.
+intros x y Fx Fy H.
+apply generic_format_FLT_FIX...
+rewrite Zplus_comm; assumption.
+apply generic_format_FIX_FLT, FIX_format_generic in Fx.
+apply generic_format_FIX_FLT, FIX_format_generic in Fy.
+destruct Fx as (nx,(H1x,H2x)).
+destruct Fy as (ny,(H1y,H2y)).
+apply generic_format_FIX.
+exists (Float beta (Fnum nx+Fnum ny)%Z emin).
+split;[idtac|reflexivity].
+rewrite H1x,H1y; unfold F2R; simpl.
+rewrite H2x, H2y.
+rewrite Z2R_plus; ring.
+Qed.
+
+End Fprop_plus_FLT.
diff --git a/flocq/Prop/Fprop_relative.v b/flocq/Prop/Fprop_relative.v
index a8cc1ff0..f0a8f344 100644
--- a/flocq/Prop/Fprop_relative.v
+++ b/flocq/Prop/Fprop_relative.v
@@ -703,6 +703,42 @@ Qed.
 
 End Fprop_relative_FLT.
 
+Lemma error_N_FLT :
+  forall (emin prec : Z), (0 < prec)%Z ->
+  forall (choice : Z -> bool),
+  forall (x : R),
+  exists eps eta : R,
+  (Rabs eps <= /2 * bpow (-prec + 1))%R /\
+  (Rabs eta <= /2 * bpow emin)%R /\
+  (eps * eta = 0)%R /\
+  (round beta (FLT_exp emin prec) (Znearest choice) x
+   = x * (1 + eps) + eta)%R.
+Proof.
+intros emin prec Pprec choice x.
+destruct (Rtotal_order x 0) as [Nx|[Zx|Px]].
+{ assert (Pmx : (0 < - x)%R).
+  { now rewrite <- Ropp_0; apply Ropp_lt_contravar. }
+  destruct (error_N_FLT_aux emin prec Pprec
+                            (fun t : Z => negb (choice (- (t + 1))%Z))
+                            (- x)%R Pmx)
+    as (d,(e,(Hd,(He,(Hde,Hr))))).
+  exists d; exists (- e)%R; split; [exact Hd|split; [|split]].
+  { now rewrite Rabs_Ropp. }
+  { now rewrite Ropp_mult_distr_r_reverse, <- Ropp_0; apply f_equal. }
+  rewrite <- (Ropp_involutive x), round_N_opp.
+  now rewrite Ropp_mult_distr_l_reverse, <- Ropp_plus_distr; apply f_equal. }
+{ assert (Ph2 : (0 <= / 2)%R).
+  { apply (Rmult_le_reg_l 2 _ _ Rlt_0_2).
+    rewrite Rmult_0_r, Rinv_r; [exact Rle_0_1|].
+    apply Rgt_not_eq, Rlt_gt, Rlt_0_2. }
+  exists R0; exists R0; rewrite Zx; split; [|split; [|split]].
+  { now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. }
+  { now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. }
+  { now rewrite Rmult_0_l. }
+  now rewrite Rmult_0_l, Rplus_0_l, round_0; [|apply valid_rnd_N]. }
+now apply error_N_FLT_aux.
+Qed.
+
 Section Fprop_relative_FLX.
 
 Variable prec : Z.