From e1badb4a2ca89161048e17d34c400dcda54879fe Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Thu, 8 Jul 2021 16:23:16 +0200
Subject: [PATCH] [ieee/coq] Bplus_correct (Rx)

---
 src_common/ieee/coq/.nra.cache        | Bin 414 -> 1222 bytes
 src_common/ieee/coq/Correction_thms.v | 207 +++++++++++++++++++++++++-
 src_common/ieee/coq/Rextended.v       |  14 ++
 3 files changed, 220 insertions(+), 1 deletion(-)

diff --git a/src_common/ieee/coq/.nra.cache b/src_common/ieee/coq/.nra.cache
index d5f5a6b53198bfebac45c7c193bb90e4c8f0c71b..1e48d00680c8db820e245fdf2ea46806e94456c1 100644
GIT binary patch
literal 1222
zcmb_cJ5B>J5H&(dmzoPuMRY`>WVGQH<RX-jQc^ety(18HlqOv+kpsb-@7k*bRtQVp
zS<iary?JBr`t9?WQo6(B@xZf`>&Gu0rR;Or5K%5fi&D14Yj<=+YmJ{ubV?K0NfjR(
zo^8Vlc2#W%fW4+RD8cK1ml-g_Tk#<FZ`@<wnPAW7*5GEavldQpIAdQ}ANOQ&OW0)_
zca{cNRQZs!siM!zJb2vm9Oh*?2Wi@B4icNLZW3l2-QY2L>#(*Bycf4=jRFphMPgM7
z+FJALbu>rm=8yNBGhyN>@3w&PgYv4Sq!aAvPo?|=N1><;jqPZDUVca&4wt$*R<2>(
zmysI&!0*NM+rjS6=ofUn$Kf!3Tio9I%7BvICEqxr(ca9tk?CL&R{u5R7<$SJV#Uwl
Ow>++2<OzoqMf44G?-M%!

delta 7
OcmX@cIgfe6JVpQv76QNk

diff --git a/src_common/ieee/coq/Correction_thms.v b/src_common/ieee/coq/Correction_thms.v
index 9497ce7cf..2f67e8027 100644
--- a/src_common/ieee/coq/Correction_thms.v
+++ b/src_common/ieee/coq/Correction_thms.v
@@ -11,6 +11,17 @@ Context (Hemax : Prec_lt_emax prec emax).
 
 Definition float : Type := binary_float prec emax.
 
+
+Lemma B2SF_eq :
+  forall (x : float) y H, B2SF x = y -> x = SF2B y H.
+Proof.
+  intros.
+  apply B2SF_inj.
+  rewrite H0.
+  symmetry.
+  apply B2SF_SF2B.
+Qed.
+
 Lemma Bplus_correct :
   forall (m : mode) (x y : float),
   is_nan (Bplus m x y) = false ->
@@ -24,6 +35,200 @@ 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; try compute0.
-Admitted.
+  unfold add.
+  repeat rewrite (B2Rx_finite (B754_finite _ _ _ _)); auto.
+  unfold round.
+  assert (Fx : is_finite x = true) by (rewrite Ex; auto).
+  assert (Fy : is_finite y = true) by (rewrite Ey; auto).
+  pose proof (Bplus_correct _ _ _ _ m x y Fx Fy).
+  destruct (do_overflow _ _ _ _) eqn:Ho1.
+  - apply do_overflow_true in Ho1.
+    unfold dont_overflow in Ho1.
+    rewrite <- Ex, <- Ey in *.
+    unfold R_imax in Ho1.
+    rewrite Ho1 in H.
+    destruct H as [H1 H2].
+    apply (B2SF_eq _ _ (binary_overflow_correct _ _ _ _ _ _)) in H1.
+    destruct m eqn:Em, (sign (B2R x + B2R y)) eqn:Hs.
+    + simpl in *. rewrite H1; simpl. 
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_neg_inv in Hs.
+      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 m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_pos_inv in Hs.
+      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 m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_neg_inv in Hs.
+      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 m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_pos_inv in Hs.
+      change (Z.neg m2) with (- Z.pos m2)%Z in Hs.
+      change (Z.neg m3) with (- Z.pos m3)%Z in Hs.
+      repeat rewrite opp_IZR in Hs.
+      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 m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_neg_inv in Hs.
+      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 m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_pos_inv in Hs.
+      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 m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_neg_inv in Hs.
+      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 m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_pos_inv in Hs.
+      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 m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_neg_inv in Hs.
+      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 m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+    + simpl in *. rewrite H1; simpl.
+      fdestruct x; fdestruct y.
+      destruct s1, s2; simpl in *; try easy.
+      unfold Defs.F2R in Hs; simpl in Hs.
+      apply sign_pos_inv in Hs.
+      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 m2).
+      pose proof (H m3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e3).
+      pose proof (Raux.bpow_gt_0 Zaux.radix2 e5).
+      nra.
+  - apply do_overflow_false in Ho1.
+    unfold dont_overflow in Ho1.
+    rewrite <- Ex, <- Ey in *.
+    unfold R_imax in Ho1.
+    rewrite Ho1 in H.
+    now destruct H as [<- [Hf _]], (Bplus _ _ _).
+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 05dd21241..a75e85c5d 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -199,6 +199,13 @@ Proof.
   now rewrite <- Raux.negb_Rlt_bool, H.
 Qed.
 
+Lemma do_overflow_true :
+  forall m r, do_overflow m r = true -> dont_overflow m r = false.
+Proof.
+  intros. unfold do_overflow, dont_overflow in *.
+  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.
@@ -206,6 +213,13 @@ Proof.
   now rewrite <- Raux.negb_Rle_bool, Bool.negb_false_iff.
 Qed.
 
+Lemma dont_overflow_false : 
+  forall m r, dont_overflow m r = false -> do_overflow m r = true.
+Proof.
+  intros. unfold do_overflow, dont_overflow in *.
+  now rewrite <- Bool.negb_false_iff, Raux.negb_Rlt_bool.
+Qed.
+
 Lemma F2R_congr :
   forall m1 e1 m2 e2, m1 = m2 -> e1 = e2 ->
   @Defs.F2R Zaux.radix2 {| Defs.Fnum := m1; Defs.Fexp := e1 |} = 
-- 
GitLab