From 356d5192eeef4c63ea0da6e7eb20630d95f36431 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Tue, 15 Jun 2021 15:51:53 +0200
Subject: [PATCH] [ieee/coq] correction of Iadd
---
.lia.cache | Bin 0 -> 36 bytes
src_common/ieee/coq/finterval.v | 209 ++++++++++++++++++++++++++++++++
2 files changed, 209 insertions(+)
create mode 100644 .lia.cache
diff --git a/.lia.cache b/.lia.cache
new file mode 100644
index 0000000000000000000000000000000000000000..7f35b0311a304a37cfee27e8f685073eecff91b1
GIT binary patch
literal 36
hcmZpfx@;c<1A_n%g8&x@FIcd_(UIByKLj{90060P49@@n
literal 0
HcmV?d00001
diff --git a/src_common/ieee/coq/finterval.v b/src_common/ieee/coq/finterval.v
index e69de29bb..79ed30d37 100644
--- a/src_common/ieee/coq/finterval.v
+++ b/src_common/ieee/coq/finterval.v
@@ -0,0 +1,209 @@
+From Flocq Require Import IEEE754.BinarySingleNaN.
+From Coq Require Import QArith Psatz Reals Extraction.
+
+Definition emax := 128%Z.
+Definition prec := 24%Z.
+
+Definition B32 := binary_float prec emax.
+
+Record Interval : Type := MK_INTERVAL {
+ lo : B32;
+ hi : B32;
+ nan : bool;
+}.
+
+Definition check (I : Interval) : bool :=
+ negb (is_nan (lo I)) && negb (is_nan (hi I)).
+
+Ltac def_op :=
+ unfold prec, emax; red; lia.
+
+Program Definition Fadd (m : mode) := @Bplus prec emax _ _ m.
+Solve All Obligations with def_op.
+
+Compute (Fadd mode_NE B754_nan B754_nan).
+
+Program Definition Fsub (m : mode) := @Bminus prec emax _ _ m.
+Solve All Obligations with def_op.
+
+Program Definition Flt := @Bltb prec emax.
+
+Program Definition Fle := @Bleb prec emax.
+
+Program Definition Feq := @Beqb prec emax.
+
+Notation "x <= y" := (Fle x y = true).
+Notation "x <= y <= z" := (Fle x y = true /\ Fle y z = true).
+
+Definition contains (I : Interval) (x : B32) : Prop :=
+ let a := lo I in
+ let b := hi I in
+ a <= x <= b.
+
+Notation "x ∈ I" := (contains I x) (at level 80).
+
+Definition is_infp (x : B32) :=
+ match x with
+ | B754_infinity s => negb s
+ | _ => false
+ end.
+
+Definition is_infm (x : B32) :=
+ match x with
+ | B754_infinity s => s
+ | _ => false
+ end.
+
+Definition are_opp_inf (x y : B32) :=
+ match x, y with
+ | B754_infinity s1, B754_infinity s2 =>
+ eqb s1 (negb s2)
+ | _, _ => false
+ end.
+
+Definition sum_to_nan (A B : Interval) : bool :=
+ let a1 := lo A in
+ let a2 := lo B in
+ let b1 := hi A in
+ let b2 := hi B in
+ are_opp_inf a1 a2 || are_opp_inf b1 b2.
+
+Lemma sum_to_nan_iff :
+ forall A B, sum_to_nan A B = true <-> (are_opp_inf (lo A) (lo B) = true \/ are_opp_inf (hi A) (hi B) = true).
+Proof.
+ intros; split; intros; unfold sum_to_nan in *.
+ - rewrite Bool.orb_true_iff in H.
+ destruct H; auto.
+ - destruct H; intuition.
+Qed.
+
+Lemma opp_inf_iff:
+ forall x y, are_opp_inf x y = true <->
+ (is_infp x = true /\ is_infm y = true) \/
+ (is_infp y = true /\ is_infm x = true).
+Proof.
+ intros [ ] [ ]; simpl; try intuition.
+ destruct s, s0; tauto.
+ + rewrite negb_true_iff in H.
+ rewrite H, H1; reflexivity.
+ + rewrite H, H1; reflexivity.
+Qed.
+
+Lemma is_infm_iff:
+ forall x, is_infm x = true <-> x = B754_infinity true.
+Proof.
+ intros [ ]; split; intros; try easy.
+ - destruct s; easy.
+ - destruct s; easy.
+Qed.
+
+Lemma is_infp_iff:
+ forall x, is_infp x = true <-> x = B754_infinity false.
+Proof.
+ intros [ ]; split; intros; try easy.
+ - destruct s; easy.
+ - destruct s; easy.
+Qed.
+
+Axiom add_not_nan :
+ forall m x y,
+ is_nan x = false ->
+ is_nan y = false ->
+ are_opp_inf x y = false ->
+ is_nan (Fadd m x y) = false.
+
+Definition infp : B32 := B754_infinity false.
+Definition infm : B32 := B754_infinity true.
+
+Definition Iadd (m : mode) (A B : Interval) : Interval :=
+ let a := Fadd m (lo A) (lo B) in
+ let b := Fadd m (hi A) (hi B) in
+ let nan := (nan A || nan B || sum_to_nan A B) in
+ match sum_to_nan A B with
+ | true => MK_INTERVAL infp infm nan
+ | false => MK_INTERVAL a b nan
+ end.
+
+Axiom Fle_trans_inv:
+ forall x y z, x <= y <= z -> x <= z.
+
+Axiom Fle_infp_finite:
+ forall x, is_finite x = true -> infp <= x -> False.
+
+Axiom Fle_infm_finite:
+ forall x, is_finite x = true -> x <= infm -> False.
+
+Axiom Fadd_le_compat:
+ forall m w x y z,
+ is_nan w = false ->
+ is_nan x = false ->
+ is_nan y = false ->
+ is_nan z = false ->
+ w <= x -> y <= z ->
+ Fadd m w y <= Fadd m x z.
+
+Lemma is_finite_nan :
+ forall x:B32, is_finite x = true -> is_nan x = false.
+Proof.
+ intros [ ] H; try easy.
+Qed.
+
+Lemma Iadd_correct :
+ forall m ix iy x y,
+ is_finite x = true ->
+ is_finite y = true ->
+ check ix = true ->
+ check iy = true ->
+ contains ix x ->
+ contains iy y ->
+ contains (Iadd m ix iy) (Fadd m x y).
+Proof.
+ intros m ix iy x y Fx Fy Hix Hiy [Hx1 Hx2] [Hy1 Hy2].
+ unfold contains in *; split.
+ - unfold Iadd; destruct sum_to_nan eqn:E; cbn.
+ + rewrite sum_to_nan_iff in E.
+ destruct E as [ H | H ];
+ rewrite opp_inf_iff in H;
+ destruct H as [ [H1 H2] | [H1 H2]];
+ rewrite is_infm_iff in *;
+ rewrite is_infp_iff in *.
+ * rewrite H1 in Hx1.
+ eauto using H1, Fle_infp_finite.
+ * rewrite H1 in Hy1.
+ eauto using Fle_infp_finite.
+ * rewrite H2 in Hy2.
+ eauto using Fle_infm_finite.
+ * rewrite H2 in Hx2.
+ eauto using Fle_infm_finite.
+ + unfold check in *.
+ rewrite andb_true_iff in *.
+ destruct Hix as [Hix1 Hix2].
+ destruct Hiy as [Hiy1 Hiy2].
+ rewrite negb_true_iff in *.
+ apply is_finite_nan in Fx.
+ apply is_finite_nan in Fy.
+ now apply Fadd_le_compat.
+ - unfold Iadd; destruct sum_to_nan eqn:E; cbn.
+ + rewrite sum_to_nan_iff in E.
+ destruct E as [ H | H ];
+ rewrite opp_inf_iff in H;
+ destruct H as [ [H1 H2] | [H1 H2]];
+ rewrite is_infm_iff in *;
+ rewrite is_infp_iff in *.
+ * rewrite H1 in Hx1.
+ eauto using H1, Fle_infp_finite.
+ * rewrite H1 in Hy1.
+ eauto using Fle_infp_finite.
+ * rewrite H2 in Hy2.
+ eauto using Fle_infm_finite.
+ * rewrite H2 in Hx2.
+ eauto using Fle_infm_finite.
+ + unfold check in *.
+ rewrite andb_true_iff in *.
+ destruct Hix as [Hix1 Hix2].
+ destruct Hiy as [Hiy1 Hiy2].
+ rewrite negb_true_iff in *.
+ apply is_finite_nan in Fx.
+ apply is_finite_nan in Fy.
+ now apply Fadd_le_compat.
+Qed.
\ No newline at end of file
--
GitLab