From d3ea06f37dc57ecf7ba30c6fe7d61864d3195f6f Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Fri, 18 Jun 2021 09:58:20 +0200
Subject: [PATCH] [ieee/flocq] cleaning
---
src_common/ieee/coq/{finterval.v => Finterval.v} | 4 ++++
src_common/ieee/coq/Futils.v | 9 ++++-----
2 files changed, 8 insertions(+), 5 deletions(-)
rename src_common/ieee/coq/{finterval.v => Finterval.v} (98%)
diff --git a/src_common/ieee/coq/finterval.v b/src_common/ieee/coq/Finterval.v
similarity index 98%
rename from src_common/ieee/coq/finterval.v
rename to src_common/ieee/coq/Finterval.v
index 8d3e27755..87e5aa381 100644
--- a/src_common/ieee/coq/finterval.v
+++ b/src_common/ieee/coq/Finterval.v
@@ -1,6 +1,10 @@
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import QArith Psatz Reals Extraction.
+(*********************************************************
+ Interval arithmetic over floatting points
+**********************************************************)
+
Definition emax := 128%Z.
Definition prec := 24%Z.
diff --git a/src_common/ieee/coq/Futils.v b/src_common/ieee/coq/Futils.v
index fcca5e6e3..b6347500c 100644
--- a/src_common/ieee/coq/Futils.v
+++ b/src_common/ieee/coq/Futils.v
@@ -1,6 +1,8 @@
From Flocq Require Import IEEE754.BinarySingleNaN.
From Coq Require Import ZArith Lia Reals Psatz.
+Section B32.
+
Definition emax := 128%Z.
Definition prec := 24%Z.
@@ -17,10 +19,7 @@ Lemma prec_gt_0 :
FLX.Prec_gt_0 prec.
Proof. def_op. Qed.
-Program Definition Fadd (m : mode) := @Bplus prec emax _ _ m.
-Solve All Obligations with def_op.
-
-Compute (Fadd mode_NE B754_nan B754_nan).
+End B32.
Program Definition Flt := @Bltb prec emax.
@@ -68,7 +67,7 @@ Proof.
pose proof (Hc1 := Bplus_correct prec emax H1 H2 m w y Fw Fy).
pose proof (Hc2 := Bplus_correct prec emax H1 H2 m x z Fx Fz).
rewrite Ho1 in Hc1. rewrite Ho2 in Hc2.
- unfold Fadd; simpl; intuition.
+ simpl; intuition.
rewrite H, H3.
apply Generic_fmt.round_le; try red; intuition; try ulia; lra.
Qed.
--
GitLab