From ef392fbc514dfea6877d6b70d72f5e881a3e8c8a Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Thu, 8 Jul 2021 16:53:24 +0200
Subject: [PATCH] [ieee/coq] Bplus_le_compat

---
 src_common/ieee/coq/.nra.cache        | Bin 1222 -> 1557 bytes
 src_common/ieee/coq/Correction_thms.v |  75 ++++++++++++++++++++++++++
 src_common/ieee/coq/Rextended.v       |  19 +++++++
 3 files changed, 94 insertions(+)

diff --git a/src_common/ieee/coq/.nra.cache b/src_common/ieee/coq/.nra.cache
index 1e48d00680c8db820e245fdf2ea46806e94456c1..ddc240ee3583d254990ee9fa18e1ff3d2d5b7431 100644
GIT binary patch
delta 158
zcmX@cIhAL_F_y`7EbP3>3=p6Jq%<biGRaJy&dA5>0~O5%(%B$U_6Z9d9Gn&`m@LO6
z!{abv$>IqU943J9WOhd7$=b|(lSP=+CZ6L&(<#d=V*u5;X~Keu4h{}b-a-c;e*%n;
HY@h=GRdg>K

delta 7
OcmbQrbBuGtF%|#}1On>-

diff --git a/src_common/ieee/coq/Correction_thms.v b/src_common/ieee/coq/Correction_thms.v
index 2f67e8027..16ad45b4a 100644
--- a/src_common/ieee/coq/Correction_thms.v
+++ b/src_common/ieee/coq/Correction_thms.v
@@ -231,4 +231,79 @@ Proof.
     now destruct H as [<- [Hf _]], (Bplus _ _ _).
 Qed.
 
+Theorem Bplus_le_compat:
+  forall m (a b c : float),
+    is_nan (Bplus m a c) = false ->
+    is_nan (Bplus m b c) = false ->
+    a <= b ->
+    Bplus m a c <= Bplus m b c.
+Proof.
+  intros m a b c Hnan1 Hnan2 Hab.
+  apply B2Rx_le; try easy.
+  rewrite (Bplus_correct m a c Hnan1).
+  rewrite (Bplus_correct m b c Hnan2).
+  apply round_le.
+  apply add_leb_compat.
+  fdestruct a; fdestruct b; simpl.
+  - apply Raux.Rle_bool_true; lra.
+  - apply Raux.Rle_bool_true; lra.
+  - destruct s; simpl; try easy.
+    unfold Defs.F2R; simpl.
+    apply Raux.Rle_bool_true.
+    assert (forall x, IZR (Z.pos x) > 0)%R.
+    { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+    }
+    pose proof (H m0).
+    pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+    nra.
+  - apply Raux.Rle_bool_true; lra.
+  - apply Raux.Rle_bool_true; lra.
+  - destruct s; simpl; try easy.
+    unfold Defs.F2R; simpl.
+    apply Raux.Rle_bool_true.
+    assert (forall x, IZR (Z.pos x) > 0)%R.
+    { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.pos x))); auto.
+          apply IZR_lt; lia.
+    }
+    pose proof (H m0).
+    pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+    nra.
+  - destruct s; simpl; try easy.
+    unfold Defs.F2R; simpl.
+    apply Raux.Rle_bool_true.
+    assert (forall x, IZR (Z.neg x) < 0)%R.
+    { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+    }
+    pose proof (H m0).
+    pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+    nra.
+  - destruct s; simpl; try easy.
+    unfold Defs.F2R; simpl.
+    apply Raux.Rle_bool_true.
+    assert (forall x, IZR (Z.neg x) < 0)%R.
+    { induction x; try lra.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+        + apply (Rgt_trans _ (IZR (Z.neg x))); auto.
+          apply IZR_lt; lia.
+    }
+    pose proof (H m0).
+    pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+    nra.
+  - destruct s, s0; simpl; try easy;
+      apply Bleb_le in Hab; auto;
+      now apply Raux.Rle_bool_true.
+Qed.
+
 End Correction.
\ No newline at end of file
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index a75e85c5d..3fda6b864 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -580,6 +580,24 @@ Definition add (x y : Rx) : Rx :=
     end
   end.
 
+Lemma add_leb_compat :
+  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 Raux.Rle_bool_true.
+    lra.
+  - now destruct b.
+  - now destruct b.
+  - now destruct b, b0.
+  - now destruct b.
+  - now destruct b, b0.
+  - now destruct b, b0.
+  - now destruct b, b0, b1.
+Qed.
+
 Lemma add_real :
   forall (r1 r2 : R), add (Real r1) (Real r2) = Real (r1 + r2)%R.
 Proof. reflexivity. Qed.
@@ -698,6 +716,7 @@ Qed.
 End Rextended.
 
 Arguments round {prec} {emax} {Hprec} {Hemax}.
+Arguments round_le {prec} {emax} {Hprec} {Hemax}.
 Arguments B2Rx {prec} {emax}.
 Arguments B2Rx_le {prec} {emax}.
 Arguments le_B2Rx {prec} {emax}.
-- 
GitLab