[ieee/coq] Proof of Rextended.round_id & refactor of Bplus_correct proof

src_common/ieee/coq/Correction_thms.v

+From Flocq Require Import IEEE754.BinarySingleNaN.
+From Coq Require Import ZArith Lia Reals Psatz.
+From F Require Import Utils Rextended.
+
+Section Correction.
+
+Variable prec : Z.
+Variable emax : Z.
+Context (Hprec : FLX.Prec_gt_0 prec).
+Context (Hemax : Prec_lt_emax prec emax).
+
+Definition float : Type := binary_float prec emax.
+
+Lemma Bplus_correct :
+  forall (m : mode) (x y : float),
+  is_nan (Bplus m x y) = false ->
+  B2Rx (Bplus m x y) = round m (add (B2Rx x) (B2Rx y)).
+Proof.
+  Ltac compute0 :=
+    match goal with
+    | [ m : mode |- _ ] =>
+      destruct m; simpl (B2Rx (B754_zero _)); (rewrite add_0_l || rewrite add_0_r); try apply round_id; apply round_0
+  end.
+  intros m x y HnanS.
+  destruct (Bplus_not_nan_inv _ _ _ HnanS) as [HnanX HnanY].
+  induction x as [ [ ] | [ ] | | ] eqn:Ex, y as [ [ ] | [ ] | | ] eqn:Ey; try easy; try compute0.
+Admitted.
+
+End Correction.
\ No newline at end of file

src_common/ieee/coq/Finterval.v → src_common/ieee/coq/Interval.v

 From Flocq Require Import IEEE754.BinarySingleNaN.
 From Coq Require Import QArith Psatz Reals Extraction.
-Require Import F.Futils F.Fdom.
+Require Import F.Utils F.Domains.
 
 (*********************************************************
        Interval arithmetic over floatting points

src_common/ieee/coq/Rextended.v

@@ -36,6 +36,12 @@ Proof.
   now destruct (Raux.Rlt_bool_spec r 0).
 Qed.
 
+Lemma minus_pos_lt :
+  forall r1 r2, (0 < r2)%R -> (r1 - r2 < r1)%R.
+Proof.
+  intros; lra.
+Qed.
+
 End Rutils.
 
 
@@ -128,6 +134,12 @@ Proof.
   now apply bounded_le_emax_minus_prec.
 Qed.
 
+Lemma Rimax_Rfmax :
+  (R_fmax < R_imax)%R.
+Proof.
+  apply minus_pos_lt, Raux.bpow_gt_0.
+Qed.
+
 Lemma Bleb_le :
   forall x y : float, is_finite x = true -> is_finite y = true ->
     Bleb x y = true -> (B2R x <= B2R y)%R.
@@ -141,6 +153,18 @@ Proof.
   + apply Raux.Rcompare_Lt_inv in E; lra.
 Qed.
 
+Lemma Bltb_lt :
+  forall x y : float, is_finite x = true -> is_finite y = true ->
+    Bltb x y = true -> (B2R x < B2R y)%R.
+Proof.
+  intros x y Fx Fy H.
+  unfold Bltb, SpecFloat.SFltb in H.
+  replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) in H by auto.
+  rewrite (Bcompare_correct _ _ x y Fx Fy) in H.
+  destruct (Raux.Rcompare) eqn:E in H; try easy.
+  apply Raux.Rcompare_Lt_inv in E; lra.
+Qed.
+
 Definition leb (x y : Rx) :=
   match x with
   | Inf true => true
@@ -175,6 +199,13 @@ Proof.
   now rewrite <- Raux.negb_Rlt_bool, H.
 Qed.
 
+Lemma dont_overflow_true : 
+  forall m r, dont_overflow m r = true -> do_overflow m r = false.
+Proof.
+  intros. unfold do_overflow, dont_overflow in *.
+  now rewrite <- Raux.negb_Rle_bool, Bool.negb_false_iff.
+Qed.
+
 Lemma F2R_congr :
   forall m1 e1 m2 e2, m1 = m2 -> e1 = e2 ->
   @Defs.F2R Zaux.radix2 {| Defs.Fnum := m1; Defs.Fexp := e1 |} = 
@@ -559,11 +590,39 @@ Lemma B2Rx_finite :
   is_finite f = true -> B2Rx f = Real (B2R f).
 Proof. now destruct f. Qed.
 
+Lemma bounded_dont_overflow :
+  forall mode s m e (H : SpecFloat.bounded prec emax m e = true),
+    dont_overflow mode (B2R (B754_finite s m e H)) = true.
+Proof.
+  intros.
+  unfold dont_overflow.
+  apply Raux.Rlt_bool_true.
+  apply Raux.Rabs_lt; split.
+  + rewrite Generic_fmt.round_generic by (intuition; apply generic_format_B2R).
+    rewrite <- Ropp_involutive.
+    apply Ropp_lt_contravar.
+    rewrite <- B2R_Bopp; simpl (Bopp _).
+    apply (Rle_lt_trans _ R_fmax).
+    - rewrite R2F_fmax. auto using Bleb_le, F_fmax_max.
+    - apply Rimax_Rfmax.
+  + rewrite Generic_fmt.round_generic by (intuition; apply generic_format_B2R).
+    apply (Rle_lt_trans _ R_fmax).
+    - rewrite R2F_fmax. auto using Bleb_le, F_fmax_max.
+    - apply Rimax_Rfmax.
+Qed.
+
 Lemma round_id :
   forall m (f : float),
     B2Rx f = round m (B2Rx f).
 Proof.
-Admitted.
+  intros m; destruct f as [ [ ] | [ ] | | ]; try easy.
+  + simpl (B2Rx _); apply round_0.
+  + simpl (B2Rx _); apply round_0.
+  + simpl (B2Rx _); apply round_0.
+  + unfold B2Rx, round.
+    rewrite (dont_overflow_true _ _ (bounded_dont_overflow m s m0 e e0)).
+    now rewrite Generic_fmt.round_generic by (intuition; apply generic_format_B2R).
+Qed.
 
 Lemma B2Rx_le :
   forall (x y : float),

src_common/ieee/coq/Fauto.v → src_common/ieee/coq/Tactics.v

 From Flocq Require Import IEEE754.BinarySingleNaN.
 From Coq Require Import QArith Psatz Reals.
-From F Require Import Futils Finterval.

src_common/ieee/coq/Futils.v → src_common/ieee/coq/Utils.v

@@ -92,11 +92,6 @@ Lemma le_infm_finite:
   forall x : float, is_finite x = true -> x <= -oo -> False.
 Proof. now intros [ ]. Qed.
 
-Definition dont_overflow (m : mode) (op : R -> R -> R) (x y : float) : bool :=
-  let fexp := SpecFloat.fexp prec emax in
-  let fmax := Raux.bpow Zaux.radix2 emax in
-  let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) (op (B2R x) (B2R y)) in
-  Raux.Rlt_bool (Rabs rsum) fmax.
 
 Lemma Bplus_not_nan_inv :
   forall m (x y : float),
@@ -175,7 +170,8 @@ Proof.
   - simpl (Bplus m _ (B754_zero _)).
     rewrite add_0_r.
     apply round_id.
-  - admit.
+  - Check (Bplus_correct).
+  admit.
 Admitted.
 
 End Utils.
@@ -187,3 +183,4 @@ Arguments is_nan_inv {prec} {emax}.
 Arguments is_infm {prec} {emax}.
 Arguments is_infp {prec} {emax}.
 Arguments is_inf {prec} {emax}.
+Arguments Bplus_not_nan_inv {prec} {emax} {Hprec} {Hemax}.

src_common/ieee/coq/_CoqProject

 -R ./ F
-./Fdom.v
-./Finterval.v
-./Fauto.v
+./Domains.v
+./Interval.v
+./Tactics.v
 ./Rextended.v
-./Futils.v
\ No newline at end of file
+./Utils.v
+./Correction_thms.v
\ No newline at end of file