From 97ba681ca0a7062dfb06914a4def47addc683cf6 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Thu, 8 Jul 2021 14:42:03 +0200
Subject: [PATCH] [ieee/coq] Proof of Rextended.round_id & refactor of
 Bplus_correct proof

---
 src_common/ieee/coq/.nia.cache                | Bin 378 -> 0 bytes
 src_common/ieee/coq/Correction_thms.v         |  29 +++++++++
 src_common/ieee/coq/{Fdom.v => Domains.v}     |   0
 .../ieee/coq/{Finterval.v => Interval.v}      |   2 +-
 src_common/ieee/coq/Rextended.v               |  61 +++++++++++++++++-
 src_common/ieee/coq/{Fauto.v => Tactics.v}    |   1 -
 src_common/ieee/coq/{Futils.v => Utils.v}     |   9 +--
 src_common/ieee/coq/_CoqProject               |   9 +--
 8 files changed, 98 insertions(+), 13 deletions(-)
 delete mode 100644 src_common/ieee/coq/.nia.cache
 create mode 100644 src_common/ieee/coq/Correction_thms.v
 rename src_common/ieee/coq/{Fdom.v => Domains.v} (100%)
 rename src_common/ieee/coq/{Finterval.v => Interval.v} (99%)
 rename src_common/ieee/coq/{Fauto.v => Tactics.v} (70%)
 rename src_common/ieee/coq/{Futils.v => Utils.v} (94%)

diff --git a/src_common/ieee/coq/.nia.cache b/src_common/ieee/coq/.nia.cache
deleted file mode 100644
index c5004cbb4aec3cd10695911d1323ad04d2c8edee..0000000000000000000000000000000000000000
GIT binary patch
literal 0
HcmV?d00001

literal 378
zcmZpfx@;c<1A_$+gMc>(FIcd_(UIByKLjjTuxY{s2Zsq09h^bTi4G1({DlaPgF_3%
zEDx|r3=FA2Iu+9_paDShfMy}-g>cY}o`}V4U#Qu+KsuK?W-nL(bPe3`u}}*-fOH2o
Z3y@re88WC|LQx9#GAQIGf`ih*0RW><rGNkc

diff --git a/src_common/ieee/coq/Correction_thms.v b/src_common/ieee/coq/Correction_thms.v
new file mode 100644
index 000000000..9497ce7cf
--- /dev/null
+++ b/src_common/ieee/coq/Correction_thms.v
@@ -0,0 +1,29 @@
+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
diff --git a/src_common/ieee/coq/Fdom.v b/src_common/ieee/coq/Domains.v
similarity index 100%
rename from src_common/ieee/coq/Fdom.v
rename to src_common/ieee/coq/Domains.v
diff --git a/src_common/ieee/coq/Finterval.v b/src_common/ieee/coq/Interval.v
similarity index 99%
rename from src_common/ieee/coq/Finterval.v
rename to src_common/ieee/coq/Interval.v
index 00e5abc2c..fc4b6edb2 100644
--- a/src_common/ieee/coq/Finterval.v
+++ b/src_common/ieee/coq/Interval.v
@@ -1,6 +1,6 @@
 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
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index 67887e36f..05dd21241 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/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),
diff --git a/src_common/ieee/coq/Fauto.v b/src_common/ieee/coq/Tactics.v
similarity index 70%
rename from src_common/ieee/coq/Fauto.v
rename to src_common/ieee/coq/Tactics.v
index d6444de4c..6a9577937 100644
--- a/src_common/ieee/coq/Fauto.v
+++ b/src_common/ieee/coq/Tactics.v
@@ -1,3 +1,2 @@
 From Flocq Require Import IEEE754.BinarySingleNaN.
 From Coq Require Import QArith Psatz Reals.
-From F Require Import Futils Finterval.
diff --git a/src_common/ieee/coq/Futils.v b/src_common/ieee/coq/Utils.v
similarity index 94%
rename from src_common/ieee/coq/Futils.v
rename to src_common/ieee/coq/Utils.v
index 66bcff24e..7b03c20c9 100644
--- a/src_common/ieee/coq/Futils.v
+++ b/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}.
diff --git a/src_common/ieee/coq/_CoqProject b/src_common/ieee/coq/_CoqProject
index fb2963fe6..e1ce89b70 100644
--- a/src_common/ieee/coq/_CoqProject
+++ b/src_common/ieee/coq/_CoqProject
@@ -1,6 +1,7 @@
 -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
-- 
GitLab