From 2cc9c3b543634c98acb676573912d5677bdc76e6 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Wed, 23 Jun 2021 15:15:30 +0200
Subject: [PATCH] [ieee/flocq] WIP on new util lemmas in Finterval
---
src_common/ieee/coq/Futils.v | 66 ++++++++++++++++++++++++++++++++++++
1 file changed, 66 insertions(+)
diff --git a/src_common/ieee/coq/Futils.v b/src_common/ieee/coq/Futils.v
index ac4209548..b4d740348 100644
--- a/src_common/ieee/coq/Futils.v
+++ b/src_common/ieee/coq/Futils.v
@@ -77,6 +77,12 @@ Definition dont_overflow (x y : binary_float prec emax) (m : mode) :=
let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) (B2R x + B2R y) in
Raux.Rlt_bool (Rabs rsum) fmax = true.
+Definition do_overflow (x y : binary_float prec emax) (m : mode) :=
+ 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) (B2R x + B2R y) in
+ Raux.Rlt_bool (Rabs rsum) fmax = false.
+
Lemma Fadd_le_compat_aux:
forall m w x y z H1 H2,
is_finite w = true ->
@@ -112,6 +118,66 @@ Proof.
intuition.
Qed.
+Lemma add_nan :
+ forall m x y H1 H2,
+ is_finite x = true ->
+ is_finite y = true ->
+ is_nan (@Bplus prec emax H1 H2 m x y) = false.
+Proof.
+ intros m [[ ] | [ ] | | ] [ [ ] | [ ] | | ] H1 H2 Fx Fy; try easy.
+ - now destruct m.
+ - now destruct m.
+ - unfold Bplus; auto using is_nan_binary_normalize.
+Qed.
+
+Lemma Rlt_bool_Rcompare :
+ forall x y, Raux.Rlt_bool x y = true -> Raux.Rcompare x y = Lt.
+Proof.
+ intros; unfold Raux.Rlt_bool in *.
+ now destruct Raux.Rcompare eqn:E.
+Qed.
+
+Lemma Rlt_bool_inv :
+ forall x y, Raux.Rlt_bool x y = true -> (x < y)%R.
+Proof.
+ auto using Rlt_bool_Rcompare, Raux.Rcompare_Lt_inv.
+Qed.
+
+Lemma no_overflow :
+ forall m x y x' y',
+ is_finite x = true ->
+ is_finite x' = true ->
+ is_finite y = true ->
+ is_finite y' = true ->
+ x <= x' ->
+ y <= y' ->
+ dont_overflow x' y' m ->
+ dont_overflow x y m.
+Proof.
+ intros m x y x' y' Fx Fx' Fy Fy' Hx Hy H. unfold dont_overflow in *.
+ apply Rlt_bool_inv in H.
+ apply Raux.Rlt_bool_true.
+ apply (Fle_Rle _ _ Fx Fx') in Hx.
+ apply (Fle_Rle _ _ Fy Fy') in Hy.
+ (* erewrite Generic_fmt.round_le in H. *)
+Admitted.
+
+(**
+
+IDEA : prove that if I1 & I2 bounds don't overflow when added,
+then for any x in I1, y in I2, x + y don't overflow.
+
+Then, redefined I1 + I2 as :
+
+if bounds of I1, I2 may overflow once added then
+ set new bounds & flag accordingly (correction still to be proved)
+else
+ just add the bounds
+ correction proof:
+ (1) if x in I1 & y in I2, then x + y dont overflow (to be proved)
+ (1) if x in I1 & y in I2, then x + y dont overflow (to be proved)
+*)
+
Lemma Fadd_le_compat:
forall m w x y z H1 H2,
is_finite w = true ->
--
GitLab