End of Veltkamp + Beginning FTS

src/Translate/Ftranslate_flocq2Pff.v

@@ -55,6 +55,15 @@ omega.
 Qed.
 
 
+Lemma FtoR_F2R: forall (f:Float.float) (g: float beta), Float.Fnum f = Fnum g -> Float.Fexp f = Fexp g -> 
+  FtoR beta f = F2R g.
+Proof.
+intros f g H1 H2; unfold FtoR, F2R.
+rewrite H1, H2, Z2R_IZR.
+now rewrite bpow_powerRZ, Z2R_IZR.
+Qed.
+
+
 End Bounds.
 Section b_Bounds.
 
@@ -101,27 +110,52 @@ exact H0.
 Qed.
 
 
+Lemma format_is_pff_format': forall r,
+   (generic_format beta (FLT_exp (-dExp b) p) r) ->
+    Fbounded b (Float.Float (Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) r))
+                            (canonic_exp beta (FLT_exp (-dExp b) p) r)).
+Proof.
+intros x; unfold generic_format.
+set (ex := canonic_exp beta (FLT_exp (-dExp b) p) x).
+set (mx := Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) x)).
+intros Hx; repeat split ; simpl.
+apply lt_Z2R.
+rewrite pGivesBound, Z2R_Zpower_nat. 
+apply Rmult_lt_reg_r with (bpow beta ex).
+apply bpow_gt_0.
+rewrite <- bpow_plus.
+rewrite inj_abs; try omega.
+change (F2R (Float beta (Zabs mx) ex) < bpow beta (p + ex))%R.
+rewrite F2R_Zabs.
+rewrite <- Hx.
+destruct (Req_dec x 0) as [Hx0|Hx0].
+rewrite Hx0, Rabs_R0.
+apply bpow_gt_0.
+unfold canonic_exp in ex.
+destruct (ln_beta beta x) as (ex', He).
+simpl in ex.
+specialize (He Hx0).
+apply Rlt_le_trans with (1 := proj2 He).
+apply bpow_le.
+cut (ex' - p <= ex)%Z. omega.
+unfold ex, FLT_exp.
+apply Zle_max_l.
+apply Zle_max_r.
+Qed.
+
+
 Lemma format_is_pff_format: forall r,
   (generic_format beta (FLT_exp (-dExp b) p) r)
   -> exists f, FtoR beta f = r /\ Fbounded b f.
 intros r Hr.
-apply FLT_format_generic in Hr; auto with zarith.
-destruct Hr as (f,(Hf1,(Hf2,Hf3))).
-exists (Float.Float (Fnum f) (Fexp f)); split.
-rewrite Hf1.
-unfold F2R, FtoR; simpl.
-rewrite Z2R_IZR.
-rewrite bpow_powerRZ.
-rewrite Z2R_IZR; reflexivity.
-split.
-apply Zlt_le_trans with (1:=Hf2).
-rewrite pGivesBound.
-rewrite Zpower_Zpower_nat; auto with zarith.
-exact Hf3.
-unfold Prec_gt_0;auto with zarith.
+eexists; split.
+2: apply (format_is_pff_format' _ Hr).
+rewrite Hr at 3; unfold FtoR, F2R; simpl.
+now rewrite Z2R_IZR, bpow_powerRZ, Z2R_IZR.
 Qed.
 
 
+
 Lemma equiv_RNDs_aux: forall z, Zeven z = true -> Even z.
 intros z; unfold Zeven, Even.
 case z.

src/Translate/Missing_theos.v

 Require Import Fcore.
 Require Import Fprop_plus_error.
 Require Import Fprop_mult_error.
-
+Require Import Fast2Sum.
 Require Import FmaErr.
 Require Import Ftranslate_flocq2Pff.
 
 Open Scope R_scope.
 
+Section FTS.
+Variable emin prec : Z.
+Hypothesis precisionNotZero : (1 < prec)%Z.
+Context { prec_gt_0_ : Prec_gt_0 prec }.
+Hypothesis emin_neg: (emin <= 0)%Z.
+
+Notation format := (generic_format radix2 (FLT_exp emin prec)).
+Notation round_flt :=(round radix2 (FLT_exp emin prec) ZnearestE).
+Notation bpow e := (bpow radix2 e).
+
+(** inputs *)
+Variable x y:R.
+Hypothesis Fx: format x.
+Hypothesis Fy: format y.
+
+(** algorithm *)
+Let a := round_flt (x+y).
+Let b := round_flt (round_flt (a-x)-y).
+
+(** Theorem *)
+Theorem FastTwoSum: Rabs y <= Rabs x -> a+b=x+y.
+Proof with auto with typeclass_instances.
+intros H.
+(* *)
+destruct (format_is_pff_format radix2 (make_bound radix2 prec emin)
+   prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero x)
+  as (fx,(Hfx,Hfx')).
+rewrite make_bound_Emin; try assumption.
+replace (--emin)%Z with emin by omega; assumption.
+destruct (format_is_pff_format radix2 (make_bound radix2 prec emin)
+   prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero y)
+  as (fy,(Hfy,Hfy')).
+rewrite make_bound_Emin; try assumption.
+replace (--emin)%Z with emin by omega; assumption.
+(* *)
+pose (Iplus := fun (f g:float) => (Float.Float 
+   (Ztrunc (scaled_mantissa radix2 (FLT_exp (emin) prec) (FtoR radix2 f+FtoR radix2 g)))
+   (canonic_exp radix2 (FLT_exp (emin) prec) (round_flt (FtoR radix2 f+FtoR radix2 g))))).
+pose (Iminus := fun (f g:float) => (Float.Float 
+   (Ztrunc (scaled_mantissa radix2 (FLT_exp (emin) prec) (FtoR radix2 f-FtoR radix2 g)))
+   (canonic_exp radix2 (FLT_exp (emin) prec) (round_flt (FtoR radix2 f-FtoR radix2 g))))).
+assert (H1: forall x y, FtoR 2 (Iplus x y) = round_flt (FtoR 2 x + FtoR 2 y)).
+clear; intros x y.
+assert (format (round_flt (FtoR 2 x + FtoR 2 y))).
+apply generic_format_round...
+
+BLOP.
+
+
+admit.
+
+rewrite H; unfold Iplus.
+change 2%Z with (radix_val radix2).
+apply FtoR_F2R; try easy.
+
+
+
+
+
+assert (K: FtoR 2 (Iminus fy (Iminus (Iplus fx fy) fx)) =
+       FtoR 2 fx + FtoR 2 fy - FtoR 2 (Iplus fx fy)).
+apply Dekker with (make_bound radix2 prec emin) (Zabs_nat prec); try assumption.
+apply Nat2Z.inj_lt.
+rewrite inj_abs; simpl; omega.
+apply make_bound_p; omega.
+
+admit.
+admit.
+admit.
+
+change 2%Z with (radix_val radix2).
+rewrite Hfx, Hfy; assumption.
+
+
+replace 2%nat with (Zabs_nat 2) by easy.
+apply Zabs_nat_le; omega.
+apply Nat2Z.inj_le.
+rewrite inj_abs; try omega.
+rewrite inj_minus, Zmax_r; rewrite inj_abs; simpl; omega.
+rewrite Hfx; rewrite inj_abs; try omega.
+rewrite bpow_powerRZ in Hfp'; rewrite Z2R_IZR i
+
+
+
+format_is_pff_format'
+
+
+
+destruct (round_NE_is_pff_round radix2 (make_bound radix2 prec emin)
+   prec (make_bound_p radix2 prec emin precisionNotZero) precisionNotZero 
+  (x+y))
+  as (fa,(Hfa, (Hfa',Hfa''))).
+rewrite make_bound_Emin in Hfa''; try assumption.
+replace (--emin)%Z with emin in Hfa'' by omega.
+(* *)
+apply Rplus_eq_reg_r with (-y).
+ring_simplify (x+y+-y).
+unfold a; rewrite <- Hfa'', <- Hfx, <- Hfy.
+
+
+
+(* *)
+
+
+apply Dekker.
+
+
+Qed.
+
+End FTS.
+
+
 Section Veltkamp.
 
 Variable beta : radix.
@@ -160,14 +272,79 @@ apply make_bound_p; omega.
 Qed.
 
 
-Theorem Veltkamp_tail:
+Theorem Veltkamp_Tail:
  x = hx+tx /\  generic_format beta (FLT_exp emin s) tx.
 Proof with auto with typeclass_instances.
-
-TODO.
+destruct (format_is_pff_format beta (make_bound beta prec emin)
+   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero x)
+  as (fx,(Hfx,Hfx')).
+rewrite make_bound_Emin; try assumption.
+replace (--emin)%Z with emin by omega; assumption.
+destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
+   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero 
+  (x*(bpow s+1)))
+  as (fp,(Hfp, (Hfp',Hfp''))).
+rewrite make_bound_Emin in Hfp''; try assumption.
+replace (--emin)%Z with emin in Hfp'' by omega.
+destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
+   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero 
+  (x-p))
+  as (fq,(Hfq, (Hfq',Hfq''))).
+rewrite make_bound_Emin in Hfq''; try assumption.
+replace (--emin)%Z with emin in Hfq'' by omega.
+destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
+   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero 
+  (q+p))
+  as (fhx,(Hfhx, (Hfhx',Hfhx''))).
+rewrite make_bound_Emin in Hfhx''; try assumption.
+replace (--emin)%Z with emin in Hfhx'' by omega.
+destruct (round_NE_is_pff_round beta (make_bound beta prec emin)
+   prec (make_bound_p beta prec emin precisionNotZero) precisionNotZero 
+  (x-hx))
+  as (ftx,(Hftx, (Hftx',Hftx''))).
+rewrite make_bound_Emin in Hftx''; try assumption.
+replace (--emin)%Z with emin in Hftx'' by omega.
+(* *)
+destruct Veltkamp_tail with beta (make_bound beta prec emin) (Zabs_nat s) 
+   (Zabs_nat prec) fx fp fq fhx ftx as (tx', (H1,(H2,(H3,H4)))); try assumption.
+apply radix_gt_1.
+apply make_bound_p; omega.
+replace 2%nat with (Zabs_nat 2) by easy.
+apply Zabs_nat_le; omega.
+apply Nat2Z.inj_le.
+rewrite inj_abs; try omega.
+rewrite inj_minus, Zmax_r; rewrite inj_abs; simpl; omega.
+rewrite Hfx; rewrite inj_abs; try omega.
+rewrite bpow_powerRZ in Hfp'; rewrite Z2R_IZR in Hfp'; apply Hfp'.
+rewrite Hfx, Hfp''; apply Hfq'.
+rewrite Hfp'', Hfq''; apply Hfhx'.
+rewrite Hfhx'', Hfx; apply Hftx'.
+(* *)
+split.
+rewrite <- Hfx, <-H2, Hfhx'', H1, Hftx''; easy.
+unfold tx; rewrite <- Hftx'', <- H1.
+replace emin with (-dExp (Bound
+       (Pos.of_succ_nat
+                 (Peano.pred (Z.abs_nat (Zpower_nat beta (Z.abs_nat s)))))
+       (dExp (make_bound beta prec emin))))%Z.
+apply pff_format_is_format; try assumption; try omega.
+simpl.
+rewrite Zpos_P_of_succ_nat, inj_pred.
+rewrite <- Zsucc_pred.
+apply inj_abs.
+apply Zpower_NR0.
+apply Zlt_le_weak; apply radix_gt_0.
+apply notEqLt, lt_Zlt_inv.
+rewrite inj_abs.
+apply Zpower_nat_less.
+apply radix_gt_1.
+apply Zpower_NR0.
+apply Zlt_le_weak; apply radix_gt_0.
+simpl.
+rewrite Zabs2N.id_abs.
+rewrite Z.abs_neq; omega.
 Qed.
 
-
 End Veltkamp.
 
 Section ErrFMA.