From 041e82e2a4af2aa5227a88b43ef63c123d0c26ca Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Mon, 12 Jul 2021 16:44:53 +0200
Subject: [PATCH] [ieee/coq] organizing the lemmas in modules

---
 src_common/ieee/coq/Correction_thms.v |  12 +-
 src_common/ieee/coq/Interval.v        | 187 +--------------
 src_common/ieee/coq/Rextended.v       | 140 +++--------
 src_common/ieee/coq/Utils.v           | 327 +++++++++++++++++++++-----
 4 files changed, 311 insertions(+), 355 deletions(-)

diff --git a/src_common/ieee/coq/Correction_thms.v b/src_common/ieee/coq/Correction_thms.v
index 06342589c..ae8eae891 100644
--- a/src_common/ieee/coq/Correction_thms.v
+++ b/src_common/ieee/coq/Correction_thms.v
@@ -154,7 +154,7 @@ Proof.
   rewrite (Bplus_correct m a c Hnan1).
   rewrite (Bplus_correct m b c Hnan2).
   apply round_le.
-  apply add_leb_compat.
+  apply add_leb_mono_l.
   fdestruct a; fdestruct b; simpl.
   - apply Raux.Rle_bool_true; lra.
   - apply Raux.Rle_bool_true; lra.
@@ -185,7 +185,7 @@ Proof.
     pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
     nra.
   - destruct s, s0; simpl; try easy;
-      apply Bleb_le in Hab; auto;
+      apply Bleb_Rle in Hab; auto;
       now apply Raux.Rle_bool_true.
 Qed.
 
@@ -201,7 +201,7 @@ Proof.
   rewrite (Bplus_correct m c a Hnan1).
   rewrite (Bplus_correct m c b Hnan2).
   apply round_le.
-  apply add_leb_compat_l.
+  apply add_leb_mono_r.
   fdestruct a; fdestruct b; simpl.
   - apply Raux.Rle_bool_true; lra.
   - apply Raux.Rle_bool_true; lra.
@@ -232,7 +232,7 @@ Proof.
     pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
     nra.
   - destruct s, s0; simpl; try easy;
-      apply Bleb_le in Hab; auto;
+      apply Bleb_Rle in Hab; auto;
       now apply Raux.Rle_bool_true.
 Qed.
 
@@ -250,10 +250,10 @@ Proof.
   rewrite (Bplus_correct m c d); auto.
   eapply leb_trans.
   - apply round_le.
-    apply add_leb_compat.
+    apply add_leb_mono_l.
     apply (le_B2Rx _ _ H1).
   - apply round_le.
-    apply add_leb_compat_l.
+    apply add_leb_mono_r.
     apply (le_B2Rx _ _ H2).
 Qed.
 
diff --git a/src_common/ieee/coq/Interval.v b/src_common/ieee/coq/Interval.v
index f2351dbb6..5fa645d36 100644
--- a/src_common/ieee/coq/Interval.v
+++ b/src_common/ieee/coq/Interval.v
@@ -84,11 +84,10 @@ Proof.
   repeat (rewrite Bplus_correct; auto).
   apply round_le.
   eapply leb_trans.
-  - apply (add_leb_compat _ _ _ (le_B2Rx _ _ H)).
-  - apply (add_leb_compat_l _ _ _ (le_B2Rx _ _ H')).
+  - apply (add_leb_mono_l _ _ _ (le_B2Rx _ _ H)).
+  - apply (add_leb_mono_r _ _ _ (le_B2Rx _ _ H')).
 Qed.
 
-
 Definition Interval := { I : Interval_aux | valid_interval I }.
 
 Program Definition Iadd (m : mode) (I1 I2 : Interval) : Interval :=
@@ -98,23 +97,6 @@ Next Obligation.
   now destruct I1, I2.
 Defined.
 
-Lemma Bplus_nan_inv :
-  forall (m : mode) (x y:float), is_nan (Bplus m x y) = true ->
-  x = +oo /\ y = -oo \/ x = -oo /\ y = +oo \/ x = NaN \/ y = NaN.
-Proof.
-  intros; fdestruct x; fdestruct y; auto.
-  - now destruct m.
-  - now destruct m.
-  - now rewrite Bplus_finites_not_nan in H.
-Qed.
-
-Lemma Bplus_not_nan_inv' :
-  forall (m : mode) (x y:float), is_nan (Bplus m x y) = false ->
-    ~(x = +oo /\ y = -oo) /\ ~(x = -oo /\ y = +oo) /\ (is_nan x = false) /\ (is_nan y = false).
-Proof.
-  intros; repeat split; fdestruct x; fdestruct y.
-Qed.
-
 Program Lemma Iadd_correct :
   forall m (I1 I2 : Interval) (x y : float), contains I1 x -> contains I2 y -> contains (Iadd m I1 I2) (Bplus m x y).
 Proof.
@@ -176,168 +158,6 @@ Proof.
   + fdestruct y; fdestruct x; destruct n; simpl; intuition.
 Qed.
 
-Lemma Bleb_refl :
-  forall x:float, is_nan x = false -> Bleb x x = true.
-Proof.
-  intros x Hx; fdestruct x.
-  apply le_Bleb; auto; lra.
-Qed.
-
-Lemma Bleb_false_Bltb :
-  forall x y:float, is_nan x = false -> is_nan y = false -> Bleb x y = false -> Bltb y x = true.
-Proof.
-  intros x y Hx Hy Hxy.
-  destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
-  unfold Bleb, SpecFloat.SFleb in Hxy;
-  replace (SpecFloat.SFcompare (B2SF _) (B2SF _)) with (Bcompare x y) in Hxy by auto;
-  assert (Fx: is_finite x = true) by (rewrite Ex; auto);
-  assert (Fy: is_finite y = true) by (rewrite Ey; auto);
-  rewrite (Bcompare_correct _ _ x y Fx Fy) in Hxy; auto;
-  destruct (Raux.Rcompare _ _) eqn:E; try easy;
-  apply Raux.Rcompare_Gt_inv in E;
-  apply lt_Bltb; auto.
-Qed.
-
-Definition Bmax (f1 f2 : float) : float :=
-  if is_nan f1 || is_nan f2 then NaN
-  else if Bleb f1 f2 then f2
-  else f1.
-
-Definition Bmin (f1 f2 : float) : float :=
-  if is_nan f1 || is_nan f2 then NaN
-  else if Bleb f1 f2 then f1
-  else f2.
-
-Lemma Bmax_max_1 :
-  forall x y, (Bmax x y = x \/ Bmax x y = y).
-Proof.
-  intros [ ] [ ]; unfold Bmax; destruct Bleb; intuition.
-Qed.
-
-Lemma Bltb_Bleb :
-  forall x y : float, Bltb x y  = true -> Bleb x y = true.
-Proof.
-  intros x y Hxy.
-  fdestruct x; fdestruct y;
-  apply le_Bleb; auto;
-  apply Bltb_lt in Hxy; auto;
-  lra.
-Qed.
-
-Lemma Bmax_max_2 :
-  forall x y, is_finite x = true -> is_finite y = true -> x <= Bmax x y  /\ y <= Bmax x y.
-Proof.
-  intros x y Fx Fy; unfold Bmax.
-  assert (HnanX: is_nan x = false) by fdestruct x.
-  assert (HnanY: is_nan y = false) by fdestruct y.
-  rewrite HnanX, HnanY; simpl.
-  split.
-  - destruct (Bleb x y) eqn:?; auto.
-    apply Bleb_refl; fdestruct x.
-  - destruct (Bleb x y) eqn:E.
-    + apply Bleb_refl; fdestruct y.
-    + apply Bleb_false_Bltb in E; auto.
-      now apply Bltb_Bleb in E.
-Qed.
-
-Lemma Bmax_le :
-  forall x y z : float, x <= z -> y <= z -> Bmax x y <= z.
-Proof.
-  intros x y z Hxz Hyz.
-  assert (HnanX: is_nan x = false) by fdestruct x.
-  assert (HnanY: is_nan y = false) by fdestruct y.
-  unfold Bmax.
-  rewrite HnanX, HnanY; simpl.
-  now destruct (Bleb x y).
-Qed.
-
-Lemma Bmax_not_nan_inv :
-  forall x y, is_nan (Bmax x y) = false -> is_nan x = false /\ is_nan y = false.
-Proof.
-  intros; split.
-  + fdestruct x.
-  + fdestruct x; fdestruct y.
-Qed.
-
-Lemma Bmin_not_nan_inv :
-  forall x y, is_nan (Bmin x y) = false -> is_nan x = false /\ is_nan y = false.
-Proof.
-  intros; split.
-  + fdestruct x.
-  + fdestruct x; fdestruct y.
-Qed.
-
-Lemma Bmax_le_inv :
-  forall x y z : float, Bmax x y <= z -> x <= z /\ y <= z.
-Proof.
-  intros x y z Hxyz.
-  assert (is_nan (Bmax x y) = false) by (fdestruct (Bmax x y)).
-  unfold Bmax in Hxyz.
-  apply Bmax_not_nan_inv in H.
-  destruct H as [H1 H2].
-  rewrite H1, H2 in Hxyz.
-  simpl in *.
-  destruct (Bleb x y) eqn:E; split; auto.
-  - now apply (Bleb_trans _ _ x y z).
-  - apply Bleb_false_Bltb in E; auto.
-    apply Bltb_Bleb in E; auto.
-    now apply (Bleb_trans _ _ y x z).
-Qed.
-
-Lemma Bmin_min_1 :
-  forall x y, (Bmin x y = x \/ Bmin x y = y).
-Proof.
-  intros [ ] [ ]; unfold Bmin; destruct Bleb; intuition.
-Qed.
-
-Lemma Bmin_min_2 :
-  forall x y, is_finite x = true -> is_finite y = true -> Bmin x y <= x /\ Bmin x y <= y.
-Proof.
-  intros x y Fx Fy; unfold Bmin.
-  assert (HnanX: is_nan x = false) by fdestruct x.
-  assert (HnanY: is_nan y = false) by fdestruct y.
-  rewrite HnanX, HnanY; simpl.
-  split.
-  - destruct (Bleb x y) eqn:?.
-    + apply Bleb_refl; fdestruct x.
-    + assert (Hx : is_nan x = false) by (fdestruct x).
-      assert (Hy : is_nan y = false) by (fdestruct y).
-      apply Bleb_false_Bltb in Heqb; auto.
-      apply Bltb_lt in Heqb; auto.
-      apply le_Bleb; auto.
-      lra.
-  - destruct (Bleb x y) eqn:E; auto.
-    apply Bleb_refl; fdestruct y.
-Qed.
-
-Lemma Bmin_le :
-  forall x y z : float, z <= x -> z <= y -> z <= Bmin x y.
-Proof.
-  intros x y z Hxz Hyz.
-  assert (HnanX: is_nan x = false) by (fdestruct z; fdestruct x).
-  assert (HnanY: is_nan y = false) by (fdestruct z; fdestruct y).
-  unfold Bmin.
-  rewrite HnanX, HnanY; simpl.
-  now destruct (Bleb x y).
-Qed.
-
-Lemma Bmin_le_inv :
-  forall x y z : float, z <= Bmin x y -> z <= x /\ z <= y.
-Proof.
-  intros x y z Hxyz.
-  assert (is_nan (Bmin x y) = false) by (fdestruct (Bmin x y); fdestruct z).
-  unfold Bmin in Hxyz.
-  apply Bmin_not_nan_inv in H.
-  destruct H as [H1 H2].
-  rewrite H1, H2 in Hxyz.
-  simpl in *.
-  destruct (Bleb x y) eqn:E; split; auto.
-  - now apply (Bleb_trans _ _ z x y).
-  - apply Bleb_false_Bltb in E; auto.
-    apply Bltb_Bleb in E.
-    now apply (Bleb_trans _ _ z y x).
-Qed.
-
 Definition inter_aux (I1 I2 : Interval_aux) : Interval_aux :=
   match I1, I2 with
   | I_Bot, _ => I_Bot
@@ -351,7 +171,6 @@ Definition inter_aux (I1 I2 : Interval_aux) : Interval_aux :=
     else I_intv (Bmax l l') (Bmin h h') (b && b')
   end.
 
-
 Lemma valid_interval_inter :
   forall I1 I2, valid_interval I1 -> valid_interval I2 -> valid_interval (inter_aux I1 I2).
 Proof.
@@ -379,8 +198,6 @@ Next Obligation.
   now apply valid_interval_inter.
 Defined.
 
-Compute (inter_aux (I_intv (-oo) (-oo) true) (I_intv (+oo) (+oo) true)).
-
 Program Lemma inter_correct_l :
   forall I1 I2, forall x, contains (inter I1 I2) x -> contains I1 x.
 Proof.
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index 0a84bffab..a2b262955 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -1,12 +1,16 @@
-From Flocq Require Import IEEE754.BinarySingleNaN.
-From Coq Require Import ZArith Psatz Reals.
-
 (*********************************************************
        Extension of R with special values +oo, -oo
 **********************************************************)
 
+From Flocq Require Import IEEE754.BinarySingleNaN.
+From Coq Require Import ZArith Psatz Reals.
+From F Require Import Utils.
+
 Set Implicit Arguments.
 
+(**
+  Usefull facts & definitions about R
+*)
 Section Rutils.
 
 Definition sign (r : R) :=
@@ -61,6 +65,9 @@ Qed.
 End Rutils.
 
 
+(**
+  Inject BinarySingleNan in R extended with infinities
+*)
 Section Rextended.
 
 Variable prec : Z.
@@ -106,61 +113,20 @@ Proof.
     + lia.
 Qed.
 
-(** Futils *)
-Lemma le_Bleb :
-  forall (x y : float),
-    is_finite x = true ->
-    is_finite y = true ->
-    (B2R x <= B2R y)%R ->
-    Bleb x y = true.
-Proof.
-  intros x y Fx Fy Hxy.
-  unfold Bleb, SpecFloat.SFleb.
-  replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) by auto.
-  rewrite (Bcompare_correct _ _ x y Fx Fy).
-  destruct Raux.Rcompare eqn:E; try easy.
-  apply Raux.Rcompare_Gt_inv in E; lra.
-Qed.
-
-Lemma lt_Bltb :
-  forall (x y : float),
-    is_finite x = true ->
-    is_finite y = true ->
-    (B2R x < B2R y)%R ->
-    Bltb x y = true.
-Proof.
-  intros x y Fx Fy Hxy.
-  unfold Bltb, SpecFloat.SFltb.
-  replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) by auto.
-  rewrite (Bcompare_correct _ _ x y Fx Fy).
-  destruct Raux.Rcompare eqn:E; auto.
-  - apply Raux.Rcompare_Eq_inv in E; lra.
-  - apply Raux.Rcompare_Gt_inv in E; lra.
-Qed.
-
 Lemma F_fmax_max :
   forall (x : float), is_finite x = true -> Bleb x F_fmax = true. 
 Proof.
   intros [ [ ] | [ ] | | [ ] m e Hbound'] Fx; auto.
-  apply le_Bleb; auto.
+  apply Rle_Bleb; auto.
   rewrite <- R2F_fmax.
   now apply bounded_le_emax_minus_prec.
 Qed.
 
-(** Futils *)
-Lemma pos_Bopp_neg :
-  forall m e Hb, @B754_finite prec emax true m e Hb = Bopp (B754_finite false m e Hb).
-Proof. reflexivity. Qed.
-
-Lemma neg_Bopp_pos :
-  forall m e Hb, @B754_finite prec emax false m e Hb = Bopp (B754_finite true m e Hb).
-Proof. reflexivity. Qed.
-
 Lemma F_fmax_min :
   forall (x : float), is_finite x = true -> Bleb (Bopp F_fmax) x = true. 
 Proof.
   intros [ [ ] | [ ] | | [ ] m e Hbound'] Fx; auto.
-  apply le_Bleb; auto.
+  apply Rle_Bleb; auto.
   rewrite pos_Bopp_neg, B2R_Bopp, B2R_Bopp, <- R2F_fmax.
   apply Ropp_le_contravar.
   now apply bounded_le_emax_minus_prec.
@@ -172,31 +138,6 @@ 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.
-Proof.
-  intros x y Fx Fy H.
-  unfold Bleb, SpecFloat.SFleb 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_Eq_inv in E; lra.
-  + 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
@@ -279,7 +220,7 @@ Definition round (m : mode) (r : Rx) : Rx :=
   | _  => r
   end.
 
-Lemma sign_le :
+Lemma pos_Rleb_neg :
   forall r1 r2, 
     sign r1 = false ->
     sign r2 = true ->
@@ -291,7 +232,7 @@ Proof.
   apply Raux.Rle_bool_false; lra.
 Qed.
 
-Lemma Rle_le :
+Lemma Rleb_Rle :
   forall r1 r2, Raux.Rle_bool r1 r2 = true -> (r1 <= r2)%R.
 Proof.
   intros.
@@ -339,7 +280,7 @@ Proof.
   apply generic_format_Rimax.
 Qed.
 
-Lemma Rlt_lt :
+Lemma Rltb_lt :
   forall x y, Raux.Rlt_bool x y = true -> (x < y)%R.
 Proof.
   intros.
@@ -382,15 +323,15 @@ Proof.
   - unfold do_overflow in H.
     unfold Rabs in H.
     destruct Rcase_abs.
-    + apply Rle_le in H.
+    + apply Rleb_Rle in H.
       right. apply Raux.Rle_bool_true.
       apply Ropp_le_contravar in H.
       replace (rx) with (--rx)%R by lra.
       subst rx; auto.
-    + apply Rle_le in H.
+    + apply Rleb_Rle in H.
       left. apply Raux.Rle_bool_true.
       auto.
-  - destruct H; apply Raux.Rle_bool_true; apply Rle_le in H.
+  - destruct H; apply Raux.Rle_bool_true; apply Rleb_Rle in H.
     + eauto using Rle_trans, H, Rle_abs.
     + apply Ropp_le_contravar in H.
       replace (--R_imax)%R with R_imax in H by lra.
@@ -403,12 +344,7 @@ Proof.
       auto.
 Qed.
 
-
-
-
-
-
-Lemma overflow_le :
+Lemma overflow_is_le :
   forall m r1 r2, 
     (r1 <= r2)%R ->
     (0 <= r1)%R ->
@@ -417,14 +353,14 @@ Lemma overflow_le :
 Proof.
   intros m r1 r2 Hle Hr1 Ho.
   rewrite do_overflow_iff in Ho. destruct Ho as [H | H].
-  - apply Rle_le in H.
+  - apply Rleb_Rle in H.
     rewrite do_overflow_iff. left.
     apply Raux.Rle_bool_true.
     eapply Generic_fmt.round_le in Hle.
     + eapply Rle_trans; [apply H | apply Hle].
     + now apply fexp_correct.
     + intuition.
-  - apply Rle_le in H.
+  - apply Rleb_Rle in H.
     assert (-R_imax < 0)%R.
     { assert (R_imax > 0)%R by apply R_imax_gt_0. lra. }
     pose proof H0.
@@ -443,7 +379,7 @@ Proof.
     + intuition.
 Qed.
 
-Lemma overflow_le' :
+Lemma overflow_is_ge :
   forall m r1 r2, 
     (r1 <= r2)%R ->
     (r2 <= 0)%R ->
@@ -452,7 +388,7 @@ Lemma overflow_le' :
 Proof.
   intros m r1 r2 Hle Hr1 Ho.
   rewrite do_overflow_iff in Ho. destruct Ho as [H | H].
-  - apply Rle_le in H.
+  - apply Rleb_Rle in H.
     rewrite <- (round_Rimax m) in H.
     eapply (Generic_fmt.round_le Zaux.radix2 fexp (round_mode m)) in Hr1; intuition.
     rewrite Generic_fmt.round_0 in Hr1.
@@ -464,7 +400,7 @@ Proof.
       rewrite (round_Rimax m) in H0.
       lra.
     + intuition.
-  - apply Rle_le in H.
+  - apply Rleb_Rle in H.
     rewrite do_overflow_iff. right.
     apply Raux.Rle_bool_true.
     apply (Generic_fmt.round_le Zaux.radix2 fexp (round_mode m)) in Hle.
@@ -499,12 +435,12 @@ Proof.
     | [ Ho1 : do_overflow _ _ = false |- _ ] =>
       apply Raux.Rle_bool_true;
       destruct (dont_overflow_inv _ _ Ho1) as (f & [?Hreq ?Hf]);
-      rewrite ?Hreq; first [now apply Bleb_le, F_fmax_min | now apply Bleb_le, F_fmax_max ]
+      rewrite ?Hreq; first [now apply Bleb_Rle, F_fmax_min | now apply Bleb_Rle, F_fmax_max ]
   end.
   Ltac freals :=
     match goal with
     | [ H : Raux.Rle_bool _ _ = true |- _ ] =>
-      apply Raux.Rle_bool_true; apply Rle_le in H;
+      apply Raux.Rle_bool_true; apply Rleb_Rle in H;
       now apply Generic_fmt.round_le; fformat
   end.
   Ltac finfinites :=
@@ -512,7 +448,7 @@ Proof.
   Ltac absurd_sign :=
     match goal with
     | [ Hs2 : sign _ = true, Hs1 : sign _ = false, H : Raux.Rle_bool _ _ = true |- _ ] =>
-      now rewrite (sign_le _ _ Hs1 Hs2) in H
+      now rewrite (pos_Rleb_neg _ _ Hs1 Hs2) in H
   end.
   Ltac absurd_mode :=
     match goal with
@@ -525,19 +461,19 @@ Proof.
         Ho1 : do_overflow _ _ = true,
         Ho2 : do_overflow _ _ = false
         |- _ 
-      ] => apply Rle_le in H; now rewrite (overflow_le _ H (sign_pos_inv _ Hs) Ho1) in Ho2
+      ] => apply Rleb_Rle in H; now rewrite (overflow_is_le _ H (sign_pos_inv _ Hs) Ho1) in Ho2
     | [ H : Raux.Rle_bool _ _ = true,
         Hs : sign _ = true,
         Ho1 : do_overflow _ _ = false,
         Ho2 : do_overflow _ _ = true
       |- _
-      ] => apply Rle_le in H; now rewrite (overflow_le' _ H (sign_neg_inv _ Hs) Ho2) in Ho1
+      ] => apply Rleb_Rle in H; now rewrite (overflow_is_ge _ H (sign_neg_inv _ Hs) Ho2) in Ho1
     | [ H : Raux.Rle_bool _ _ = false,
       Hs : sign _ = true,
       Ho1 : do_overflow _ _ = true,
       Ho2 : do_overflow _ _ = false
       |- _ 
-    ] => apply Rle_le in H; now rewrite (overflow_le' _ H (sign_neg_inv _ Hs) Ho2) in Ho1
+    ] => apply Rleb_Rle in H; now rewrite (overflow_is_ge _ H (sign_neg_inv _ Hs) Ho2) in Ho1
     | [ H1 : overflow_to_inf _ _ = true, H2 : overflow_to_inf _ _ = false |- _ ] =>
       now rewrite H1 in H2
     end.
@@ -616,19 +552,19 @@ Lemma leb_trans :
   forall x y z : Rx, leb x y = true -> leb y z = true -> leb x z = true.
 Proof.
   intros [ rx | [ ] ] [ ry | [ ] ] [ rz | [ ] ] Hxy Hyz; simpl in *; try easy.
-  apply Rle_le in Hxy.
-  apply Rle_le in Hyz.
+  apply Rleb_Rle in Hxy.
+  apply Rleb_Rle in Hyz.
   apply Raux.Rle_bool_true.
   lra.
 Qed.
 
-Lemma add_leb_compat :
+Lemma add_leb_mono_l :
   forall x y z : Rx,
   leb x y = true -> leb (add x z) (add y z) = true.
 Proof.
   intros [ ] [ ] [ ] H.
   - simpl in *.
-    apply Rle_le in H.
+    apply Rleb_Rle in H.
     apply Raux.Rle_bool_true.
     lra.
   - now destruct b.
@@ -640,13 +576,13 @@ Proof.
   - now destruct b, b0, b1.
 Qed.
 
-Lemma add_leb_compat_l :
+Lemma add_leb_mono_r :
   forall x y z : Rx,
   leb x y = true -> leb (add z x) (add z y) = true.
 Proof.
   intros [ | [ ]] [ | [ ]] [ | [ ]] H; try easy.
   simpl in *.
-  apply Rle_le in H.
+  apply Rleb_Rle in H.
   apply Raux.Rle_bool_true.
   lra.
 Qed.
@@ -688,11 +624,11 @@ Proof.
     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.
+    - rewrite R2F_fmax. auto using Bleb_Rle, 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.
+    - rewrite R2F_fmax. auto using Bleb_Rle, F_fmax_max.
     - apply Rimax_Rfmax.
 Qed.
 
diff --git a/src_common/ieee/coq/Utils.v b/src_common/ieee/coq/Utils.v
index 3899ac9ec..41758dcf4 100644
--- a/src_common/ieee/coq/Utils.v
+++ b/src_common/ieee/coq/Utils.v
@@ -1,6 +1,6 @@
 From Flocq Require Import IEEE754.BinarySingleNaN.
-From Coq Require Import ZArith Lia Reals Psatz.
-From F Require Import Rextended.
+From Coq Require Import ZArith Lia Reals Psatz Bool.
+(* From F Require Import Rextended. *)
 
 (*********************************************************
        Simple & usefull results on floats
@@ -92,15 +92,6 @@ Lemma le_infm_finite:
   forall x : float, is_finite x = true -> x <= -oo -> False.
 Proof. now intros [ ]. Qed.
 
-
-Lemma Bplus_not_nan_inv :
-  forall m (x y : float),
-  is_nan (Bplus m x y) = false ->
-  is_nan x = false /\ is_nan y = false.
-Proof.
-  fdestruct x; fdestruct y.
-Qed.
-
 Lemma Bplus_finites_not_nan :
   forall m (x y : float),
   is_finite x = true ->
@@ -114,7 +105,24 @@ Proof.
     auto using (is_nan_binary_normalize prec emax).
 Qed.
 
-Lemma Bplus_nan_if :
+Lemma Bplus_nan_inv :
+  forall (m : mode) (x y:float), is_nan (Bplus m x y) = true ->
+  x = +oo /\ y = -oo \/ x = -oo /\ y = +oo \/ x = NaN \/ y = NaN.
+Proof.
+  intros; fdestruct x; fdestruct y; auto.
+  - now destruct m.
+  - now destruct m.
+  - now rewrite Bplus_finites_not_nan in H.
+Qed.
+
+Lemma Bplus_not_nan_inv :
+  forall (m : mode) (x y:float), is_nan (Bplus m x y) = false ->
+    ~(x = +oo /\ y = -oo) /\ ~(x = -oo /\ y = +oo) /\ (is_nan x = false) /\ (is_nan y = false).
+Proof.
+  intros; repeat split; fdestruct x; fdestruct y.
+Qed.
+
+(* Lemma Bplus_nan_if :
   forall m (x y : float),
   is_nan x = false ->
   is_nan y = false ->
@@ -125,7 +133,7 @@ Proof.
   fdestruct x; fdestruct y; try now destruct m; intuition.
   assert (is_nan (Bplus m (B754_finite s m0 e e0) (B754_finite s0 m1 e1 e2)) = false) by auto using Bplus_finites_not_nan.
   rewrite H1 in H2; discriminate.
-Qed.
+Qed. *)
 
 Lemma Bplus_zero :
   forall m b (x : float),
@@ -136,14 +144,78 @@ Proof.
   - simpl; destruct m; reflexivity.
 Qed.
 
+Lemma pos_Bopp_neg :
+  forall m e Hb, @B754_finite prec emax true m e Hb = Bopp (B754_finite false m e Hb).
+Proof. reflexivity. Qed.
+
+Lemma neg_Bopp_pos :
+  forall m e Hb, @B754_finite prec emax false m e Hb = Bopp (B754_finite true m e Hb).
+Proof. reflexivity. Qed.
+
+Lemma Rle_Bleb :
+  forall (x y : float),
+    is_finite x = true ->
+    is_finite y = true ->
+    (B2R x <= B2R y)%R ->
+    Bleb x y = true.
+Proof.
+  intros x y Fx Fy Hxy.
+  unfold Bleb, SpecFloat.SFleb.
+  replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) by auto.
+  rewrite (Bcompare_correct _ _ x y Fx Fy).
+  destruct Raux.Rcompare eqn:E; try easy.
+  apply Raux.Rcompare_Gt_inv in E; lra.
+Qed.
+
+Lemma Rlt_Bltb :
+  forall (x y : float),
+    is_finite x = true ->
+    is_finite y = true ->
+    (B2R x < B2R y)%R ->
+    Bltb x y = true.
+Proof.
+  intros x y Fx Fy Hxy.
+  unfold Bltb, SpecFloat.SFltb.
+  replace (SpecFloat.SFcompare (_ x) (_ y)) with (Bcompare x y) by auto.
+  rewrite (Bcompare_correct _ _ x y Fx Fy).
+  destruct Raux.Rcompare eqn:E; auto.
+  - apply Raux.Rcompare_Eq_inv in E; lra.
+  - apply Raux.Rcompare_Gt_inv in E; lra.
+Qed.
+
+Lemma Bleb_Rle :
+  forall x y : float, is_finite x = true -> is_finite y = true ->
+    Bleb x y = true -> (B2R x <= B2R y)%R.
+Proof.
+  intros x y Fx Fy H.
+  unfold Bleb, SpecFloat.SFleb 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_Eq_inv in E; lra.
+  + apply Raux.Rcompare_Lt_inv in E; lra.
+Qed.
+
+Lemma Bltb_Rlt :
+  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.
+
 Lemma Bleb_trans :
   forall (x y z : float), x <= y -> y <= z -> x <= z.
 Proof.
   intros x y z Hxy Hyz.
   fdestruct x; fdestruct y; fdestruct z;
-  apply le_Bleb; auto;
-  apply Bleb_le in Hxy; auto;
-  apply Bleb_le in Hyz; auto;
+  apply Rle_Bleb; auto;
+  apply Bleb_Rle in Hxy; auto;
+  apply Bleb_Rle in Hyz; auto;
   lra.
 Qed.
 
@@ -152,9 +224,9 @@ Lemma Bltb_trans :
 Proof.
   intros x y z Hxy Hyz.
   fdestruct x; fdestruct y; fdestruct z;
-  apply lt_Bltb; auto;
-  apply Bltb_lt in Hxy; auto;
-  apply Bltb_lt in Hyz; auto;
+  apply Rlt_Bltb; auto;
+  apply Bltb_Rlt in Hxy; auto;
+  apply Bltb_Rlt in Hyz; auto;
   lra.
 Qed.
 
@@ -163,9 +235,9 @@ Lemma Bltb_Bleb_trans :
 Proof.
   intros x y z Hxy Hyz.
   fdestruct x; fdestruct y; fdestruct z;
-  apply lt_Bltb; auto;
-  apply Bltb_lt in Hxy; auto;
-  apply Bleb_le in Hyz; auto;
+  apply Rlt_Bltb; auto;
+  apply Bltb_Rlt in Hxy; auto;
+  apply Bleb_Rle in Hyz; auto;
   lra.
 Qed.
 
@@ -174,49 +246,173 @@ Lemma Bleb_Bltb_trans :
 Proof.
   intros x y z Hxy Hyz.
   fdestruct x; fdestruct y; fdestruct z;
-  apply lt_Bltb; auto;
-  apply Bleb_le in Hxy; auto;
-  apply Bltb_lt in Hyz; auto;
+  apply Rlt_Bltb; auto;
+  apply Bleb_Rle in Hxy; auto;
+  apply Bltb_Rlt in Hyz; auto;
   lra.
 Qed.
 
-(* Lemma Bplus_correct_full :
-  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.
-  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.
-  - simpl (Bplus m (B754_zero _) _).
-    simpl (B2Rx (B754_zero _)).
-    rewrite add_0_l. apply round_0.
-  - simpl (Bplus m (B754_zero _) _).
-    simpl (B2Rx (B754_zero _)).
-    rewrite add_0_l. destruct m; auto using round_0.
-  - simpl (Bplus m (B754_zero true) _).
-    simpl (B2Rx (B754_zero _)).
-    rewrite add_0_l.
-    apply round_id.
-  - simpl (Bplus m (B754_zero _) _).
-    simpl (B2Rx (B754_zero _)).
-    rewrite add_0_r. destruct m; auto using round_0.
-  - simpl (Bplus m (B754_zero _) _).
-    rewrite add_0_l.
-    simpl (B2Rx _).
-    apply round_0.
-  - simpl (Bplus m (B754_zero _) _).
-    rewrite add_0_l.
-    apply round_id.
-  - simpl (Bplus m _ (B754_zero _)).
-    rewrite add_0_r.
-    apply round_id.
-  - simpl (Bplus m _ (B754_zero _)).
-    rewrite add_0_r.
-    apply round_id.
-  - Check (Bplus_correct).
-  admit.
-Admitted. *)
+Lemma Bleb_refl :
+  forall x:float, is_nan x = false -> Bleb x x = true.
+Proof.
+  intros x Hx; fdestruct x.
+  apply Rle_Bleb; auto; lra.
+Qed.
+
+Lemma Bltb_Bleb :
+  forall x y : float, Bltb x y  = true -> Bleb x y = true.
+Proof.
+  intros x y Hxy.
+  fdestruct x; fdestruct y;
+  apply Rle_Bleb; auto;
+  apply Bltb_Rlt in Hxy; auto;
+  lra.
+Qed.
+
+Lemma Bleb_false_Bltb :
+  forall x y:float, is_nan x = false -> is_nan y = false -> Bleb x y = false -> Bltb y x = true.
+Proof.
+  intros x y Hx Hy Hxy.
+  destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
+  unfold Bleb, SpecFloat.SFleb in Hxy;
+  replace (SpecFloat.SFcompare (B2SF _) (B2SF _)) with (Bcompare x y) in Hxy by auto;
+  assert (Fx: is_finite x = true) by (rewrite Ex; auto);
+  assert (Fy: is_finite y = true) by (rewrite Ey; auto);
+  rewrite (Bcompare_correct _ _ x y Fx Fy) in Hxy; auto;
+  destruct (Raux.Rcompare _ _) eqn:E; try easy;
+  apply Raux.Rcompare_Gt_inv in E;
+  apply Rlt_Bltb; auto.
+Qed.
+
+Definition Bmax (f1 f2 : float) : float :=
+  if is_nan f1 || is_nan f2 then NaN
+  else if Bleb f1 f2 then f2
+  else f1.
+
+Definition Bmin (f1 f2 : float) : float :=
+  if is_nan f1 || is_nan f2 then NaN
+  else if Bleb f1 f2 then f1
+  else f2.
+
+Lemma Bmax_max_1 :
+  forall x y, (Bmax x y = x \/ Bmax x y = y).
+Proof.
+  intros [ ] [ ]; unfold Bmax; destruct Bleb; intuition.
+Qed.
+
+Lemma Bmax_max_2 :
+  forall x y, is_finite x = true -> is_finite y = true -> x <= Bmax x y  /\ y <= Bmax x y.
+Proof.
+  intros x y Fx Fy; unfold Bmax.
+  assert (HnanX: is_nan x = false) by fdestruct x.
+  assert (HnanY: is_nan y = false) by fdestruct y.
+  rewrite HnanX, HnanY; simpl.
+  split.
+  - destruct (Bleb x y) eqn:?; auto.
+    apply Bleb_refl; fdestruct x.
+  - destruct (Bleb x y) eqn:E.
+    + apply Bleb_refl; fdestruct y.
+    + apply Bleb_false_Bltb in E; auto.
+      now apply Bltb_Bleb in E.
+Qed.
+
+Lemma Bmax_le :
+  forall x y z : float, x <= z -> y <= z -> Bmax x y <= z.
+Proof.
+  intros x y z Hxz Hyz.
+  assert (HnanX: is_nan x = false) by fdestruct x.
+  assert (HnanY: is_nan y = false) by fdestruct y.
+  unfold Bmax.
+  rewrite HnanX, HnanY; simpl.
+  now destruct (Bleb x y).
+Qed.
+
+Lemma Bmax_not_nan_inv :
+  forall x y, is_nan (Bmax x y) = false -> is_nan x = false /\ is_nan y = false.
+Proof.
+  intros; split.
+  + fdestruct x.
+  + fdestruct x; fdestruct y.
+Qed.
+
+Lemma Bmin_not_nan_inv :
+  forall x y, is_nan (Bmin x y) = false -> is_nan x = false /\ is_nan y = false.
+Proof.
+  intros; split.
+  + fdestruct x.
+  + fdestruct x; fdestruct y.
+Qed.
+
+Lemma Bmax_le_inv :
+  forall x y z : float, Bmax x y <= z -> x <= z /\ y <= z.
+Proof.
+  intros x y z Hxyz.
+  assert (is_nan (Bmax x y) = false) by (fdestruct (Bmax x y)).
+  unfold Bmax in Hxyz.
+  apply Bmax_not_nan_inv in H.
+  destruct H as [H1 H2].
+  rewrite H1, H2 in Hxyz.
+  simpl in *.
+  destruct (Bleb x y) eqn:E; split; auto.
+  - now apply (Bleb_trans x y z).
+  - apply Bleb_false_Bltb in E; auto.
+    apply Bltb_Bleb in E; auto.
+    now apply (Bleb_trans y x z).
+Qed.
+
+Lemma Bmin_min_1 :
+  forall x y, (Bmin x y = x \/ Bmin x y = y).
+Proof.
+  intros [ ] [ ]; unfold Bmin; destruct Bleb; intuition.
+Qed.
+
+Lemma Bmin_min_2 :
+  forall x y, is_finite x = true -> is_finite y = true -> Bmin x y <= x /\ Bmin x y <= y.
+Proof.
+  intros x y Fx Fy; unfold Bmin.
+  assert (HnanX: is_nan x = false) by fdestruct x.
+  assert (HnanY: is_nan y = false) by fdestruct y.
+  rewrite HnanX, HnanY; simpl.
+  split.
+  - destruct (Bleb x y) eqn:?.
+    + apply Bleb_refl; fdestruct x.
+    + assert (Hx : is_nan x = false) by (fdestruct x).
+      assert (Hy : is_nan y = false) by (fdestruct y).
+      apply Bleb_false_Bltb in Heqb; auto.
+      apply Bltb_Rlt in Heqb; auto.
+      apply Rle_Bleb; auto.
+      lra.
+  - destruct (Bleb x y) eqn:E; auto.
+    apply Bleb_refl; fdestruct y.
+Qed.
+
+Lemma Bmin_le :
+  forall x y z : float, z <= x -> z <= y -> z <= Bmin x y.
+Proof.
+  intros x y z Hxz Hyz.
+  assert (HnanX: is_nan x = false) by (fdestruct z; fdestruct x).
+  assert (HnanY: is_nan y = false) by (fdestruct z; fdestruct y).
+  unfold Bmin.
+  rewrite HnanX, HnanY; simpl.
+  now destruct (Bleb x y).
+Qed.
+
+Lemma Bmin_le_inv :
+  forall x y z : float, z <= Bmin x y -> z <= x /\ z <= y.
+Proof.
+  intros x y z Hxyz.
+  assert (is_nan (Bmin x y) = false) by (fdestruct (Bmin x y); fdestruct z).
+  unfold Bmin in Hxyz.
+  apply Bmin_not_nan_inv in H.
+  destruct H as [H1 H2].
+  rewrite H1, H2 in Hxyz.
+  simpl in *.
+  destruct (Bleb x y) eqn:E; split; auto.
+  - now apply (Bleb_trans z x y).
+  - apply Bleb_false_Bltb in E; auto.
+    apply Bltb_Bleb in E.
+    now apply (Bleb_trans z y x).
+Qed.
 
 End Utils.
 
@@ -228,3 +424,10 @@ Arguments is_infm {prec} {emax}.
 Arguments is_infp {prec} {emax}.
 Arguments is_inf {prec} {emax}.
 Arguments Bplus_not_nan_inv {prec} {emax} {Hprec} {Hemax}.
+Arguments Bplus_nan_inv {prec} {emax} {Hprec} {Hemax}.
+Arguments Bmin {prec} {emax}.
+Arguments Bmax {prec} {emax}.
+Arguments Bmax_max_1 {prec} {emax}.
+Arguments Bmax_max_2 {prec} {emax}.
+Arguments Bmin_min_1 {prec} {emax}.
+Arguments Bmin_min_2 {prec} {emax}.
-- 
GitLab