diff --git a/src_common/ieee/coq/.nra.cache b/src_common/ieee/coq/.nra.cache
index a3ffd9207cbe64a8ee0e7dcb6a377133632e88ac..502adeb20c295b5f83fd327abd532f7b65d4c977 100644
Binary files a/src_common/ieee/coq/.nra.cache and b/src_common/ieee/coq/.nra.cache differ
diff --git a/src_common/ieee/coq/Correction_thms.v b/src_common/ieee/coq/Correction_thms.v
index 29969ef9ad64be112e2ba5de0e867abd6adb7a4d..06342589ccf0da95442ce59a36e8db81976064da 100644
--- a/src_common/ieee/coq/Correction_thms.v
+++ b/src_common/ieee/coq/Correction_thms.v
@@ -189,4 +189,72 @@ Proof.
now apply Raux.Rle_bool_true.
Qed.
+Theorem Bplus_le_compat_l:
+ forall m (a b c : float),
+ is_nan (Bplus m c a) = false ->
+ is_nan (Bplus m c b) = false ->
+ a <= b ->
+ Bplus m c a <= Bplus m c b.
+Proof.
+ intros m a b c Hnan1 Hnan2 Hab.
+ apply B2Rx_le; try easy.
+ rewrite (Bplus_correct m c a Hnan1).
+ rewrite (Bplus_correct m c b Hnan2).
+ apply round_le.
+ apply add_leb_compat_l.
+ fdestruct a; fdestruct b; simpl.
+ - apply Raux.Rle_bool_true; lra.
+ - apply Raux.Rle_bool_true; lra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_pos m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - apply Raux.Rle_bool_true; lra.
+ - apply Raux.Rle_bool_true; lra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_pos m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_neg m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - destruct s; simpl; try easy.
+ unfold Defs.F2R; simpl.
+ apply Raux.Rle_bool_true.
+ pose proof (IZR_neg m0).
+ pose proof (Raux.bpow_gt_0 Zaux.radix2 e).
+ nra.
+ - destruct s, s0; simpl; try easy;
+ apply Bleb_le in Hab; auto;
+ now apply Raux.Rle_bool_true.
+Qed.
+
+Theorem Bplus_le_compat':
+ forall m (a b c d : float),
+ is_nan (Bplus m a b) = false ->
+ is_nan (Bplus m c d) = false ->
+ a <= c ->
+ b <= d ->
+ Bplus m a b <= Bplus m c d.
+Proof.
+ intros.
+ apply B2Rx_le; try easy.
+ rewrite (Bplus_correct m a b); auto.
+ rewrite (Bplus_correct m c d); auto.
+ eapply leb_trans.
+ - apply round_le.
+ apply add_leb_compat.
+ apply (le_B2Rx _ _ H1).
+ - apply round_le.
+ apply add_leb_compat_l.
+ apply (le_B2Rx _ _ H2).
+Qed.
+
End Correction.
\ No newline at end of file
diff --git a/src_common/ieee/coq/Interval.v b/src_common/ieee/coq/Interval.v
index fc4b6edb2f4787cf6f4574a49e7934a5f6bf0bd0..243f26afa618f497e2b21f8c3c33bd85f1c919a3 100644
--- a/src_common/ieee/coq/Interval.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.Utils F.Domains.
+Require Import F.Utils F.Domains F.Correction_thms F.Rextended.
(*********************************************************
Interval arithmetic over floatting points
@@ -15,79 +15,161 @@ Context (Hemax : Prec_lt_emax prec emax).
Definition float := binary_float prec emax.
-Record Interval := MK_INTERVAL {
- lo : float;
- hi : float;
- nan : bool;
-}.
-
-Definition check (I : Interval) :=
- lo I <= hi I \/ (lo I = NaN /\ hi I = NaN).
-
-Definition ð“Ÿ (A : Type) := A -> Prop.
-
-Definition γ (I : Interval) : ð“Ÿ(float) :=
- fun x => lo I <= x <= hi I \/ (is_nan x && nan I) = true.
-
-Definition top := MK_INTERVAL (-oo) (+oo) true.
+Inductive Interval_aux :=
+ | Aux_Bot : Interval_aux
+ | Aux_nan : Interval_aux
+ | Aux_intv : forall (l h : float) (nan : bool), Interval_aux.
+
+Definition contains (I : Interval_aux) (x : float) : Prop :=
+ match I with
+ | Aux_Bot => False
+ | Aux_nan => x = NaN
+ | Aux_intv l h n =>
+ l <= x <= h \/ (is_nan x && n = true)
+ end.
-Notation "⊤" := top.
+Definition containsb (I : Interval_aux) (x : float) : bool :=
+ match I with
+ | Aux_Bot => true
+ | Aux_nan => is_nan x
+ | Aux_intv l h n =>
+ (Bleb l x && Bleb x h) || (is_nan x && n)
+ end.
-Notation "x ∈ I" := (γ I x) (at level 80).
+Definition Iadd_up_to_NaN (I1 I2 : Interval_aux) : bool :=
+ match I1, I2 with
+ | Aux_Bot, _ => false
+ | _, Aux_Bot => false
+ | Aux_nan, _ => true
+ | _, Aux_nan => true
+ | Aux_intv l h n, Aux_intv l' h' n' =>
+ n || n' || (containsb I1 +oo && containsb I2 -oo) || (containsb I1 -oo && containsb I2 +oo)
+ end.
+Definition Iadd_aux (m : mode) (I1 I2 : Interval_aux) : Interval_aux :=
+ match I1, I2 with
+ | Aux_Bot, _ => Aux_Bot
+ | _, Aux_Bot => Aux_Bot
+ | Aux_nan, _ => Aux_nan
+ | _, Aux_nan => Aux_nan
+ | Aux_intv l h n, Aux_intv l' h' n' =>
+ let sum1 := Bplus m l l' in
+ let sum2 := Bplus m h h' in
+ match is_nan sum1 with
+ | true =>
+ match is_nan sum2 with
+ | true => Aux_nan
+ | false => Aux_intv +oo +oo true
+ end
+ | false =>
+ match is_nan sum2 with
+ | true => Aux_intv -oo -oo true
+ | false => Aux_intv sum1 sum2 (Iadd_up_to_NaN I1 I2)
+ end
+ end
+ end.
-Lemma top_check : check ⊤.
-Proof. unfold check; auto. Qed.
+Definition valid_interval (I : Interval_aux) : Prop :=
+ match I with
+ | Aux_intv l h _ => l <= h
+ | _ => True
+ end.
-Lemma top_spec :
- forall x, x ∈ ⊤.
+Lemma valid_interval_Iadd :
+ forall m I1 I2, valid_interval I1 -> valid_interval I2 -> valid_interval (Iadd_aux m I1 I2).
Proof.
- intros.
- unfold top, γ; simpl.
- destruct (is_nan x) eqn:E.
- - destruct (is_nan_inv x E); auto.
- - left; split; fdestruct x.
+ intros m [ | | l h ] [ | | l' h' ] H H'; simpl; try easy.
+ destruct (is_nan (Bplus m l l')) eqn:E1, (is_nan (Bplus m h h')) eqn:E2; try easy.
+ apply B2Rx_le; auto.
+ repeat (rewrite Bplus_correct; auto).
+ apply round_le.
+ eapply leb_trans.
+ - apply (add_leb_compat _ _ _ (le_B2Rx _ _ H)).
+ - apply (add_leb_compat_l _ _ _ (le_B2Rx _ _ H')).
Qed.
-Definition contains_infp (I : Interval) :=
- Bleb (lo I) +oo || Bleb (hi I) +oo.
-Definition contains_infm (I : Interval) :=
- Bleb (lo I) -oo || Bleb (hi I) -oo.
-Definition Iadd (m : mode) (I₠I₂ : Interval) : Interval := ⊤.
+Definition Interval := { I : Interval_aux | valid_interval I }.
-Lemma Iadd_correct :
- forall m Iâ‚ Iâ‚‚ x y,
- x ∈ I₠->
- y ∈ I₂ ->
- (Bplus m x y) ∈ Iadd m I₠I₂.
+Lemma Bplus_nan_inv :
+ forall (m : mode) (x y:float), is_nan (Bplus m x y) = true ->
+ x = +oo /\ y = -oo \/ x = -oo /\ y = +oo \/ x = NaN \/ y = NaN.
Proof.
- intros; unfold Iadd.
- apply top_spec.
+ intros; fdestruct x; fdestruct y; auto.
+ - now destruct m.
+ - now destruct m.
+ - now rewrite Bplus_finites_not_nan in H.
Qed.
-Lemma Iadd_check :
- forall m Iâ‚ Iâ‚‚, check Iâ‚ -> check Iâ‚‚ -> check (Iadd m Iâ‚ Iâ‚‚).
+Lemma Bplus_not_nan_inv' :
+ forall (m : mode) (x y:float), is_nan (Bplus m x y) = false ->
+ ~(x = +oo /\ y = -oo) /\ ~(x = -oo /\ y = +oo) /\ (is_nan x = false) /\ (is_nan y = false).
Proof.
- intros; unfold Iadd.
- apply top_check.
+ intros; repeat split; fdestruct x; fdestruct y.
Qed.
-Definition Iadd2 (m : mode) (A B : Interval) : Interval :=
- let nan := (nan A) || (nan B) in
- match Bplus m (lo A) (lo B) with
- | NaN =>
- match Bplus m (hi A) (hi B) with
- | NaN => MK_INTERVAL NaN NaN true
- | _ => MK_INTERVAL +oo +oo true
- end
- | a =>
- match Bplus m (hi A) (hi B) with
- | NaN => MK_INTERVAL -oo -oo true
- | b => MK_INTERVAL a b nan
- end
- end.
+Program Lemma Iadd_correct :
+ forall m (I1 I2 : Interval) (x y : float), contains I1 x -> contains I2 y -> contains (Iadd_aux m I1 I2) (Bplus m x y).
+Proof.
+ intros m I1 I2 x y Hx Hy;
+ destruct I1 as [[ | | l h n ] H1] eqn:EI1, I2 as [[ | | l' h' n' ] H2] eqn:EI2;
+ simpl in *; try easy.
+ - now rewrite Hx.
+ - now rewrite Hx.
+ - now (fdestruct x; rewrite Hy).
+ - destruct (is_nan (Bplus m l l')) eqn:E1, (is_nan (Bplus m h h')) eqn:E2; intuition.
+ + destruct (Bplus_nan_inv _ _ _ E1); intuition; subst; try easy.
+ * rewrite (infp_le_is_infp _ _ _ H0) in *.
+ rewrite (infp_le_is_infp _ _ _ H1) in *.
+ fdestruct h'.
+ now rewrite (le_infm_is_infm _ _ _ H5) in *.
+ * rewrite (infp_le_is_infp _ _ _ H2) in *.
+ rewrite (infp_le_is_infp _ _ _ H4) in *.
+ fdestruct h.
+ now rewrite (le_infm_is_infm _ _ _ H3) in *.
+ + destruct (Bplus_nan_inv _ _ _ E1); intuition; subst; try easy.
+ * fdestruct y; fdestruct x.
+ * fdestruct y; fdestruct x.
+ + fdestruct x; fdestruct y.
+ + fdestruct x; fdestruct y.
+ + destruct (Bplus_nan_inv _ _ _ E1); intuition; subst; try easy.
+ * rewrite (infp_le_is_infp _ _ _ H0) in *.
+ rewrite (infp_le_is_infp _ _ _ H3) in *.
+ fdestruct y; simpl; auto.
+ * rewrite (infp_le_is_infp _ _ _ H2) in *.
+ rewrite (infp_le_is_infp _ _ _ H4) in *.
+ fdestruct x; simpl; auto.
+ + right; fdestruct x; fdestruct y.
+ + right; fdestruct x; fdestruct y.
+ + right; fdestruct x; fdestruct y.
+ + destruct (Bplus_nan_inv _ _ _ E2); intuition; subst.
+ * rewrite (le_infm_is_infm _ _ _ H5) in *.
+ rewrite (le_infm_is_infm _ _ _ H2) in *.
+ fdestruct x; simpl; auto.
+ * rewrite (le_infm_is_infm _ _ _ H1) in *.
+ rewrite (le_infm_is_infm _ _ _ H3) in *.
+ fdestruct y; simpl; auto.
+ * fdestruct x.
+ * fdestruct y.
+ + fdestruct y; fdestruct x; simpl; auto.
+ + fdestruct x; simpl; auto.
+ + fdestruct x; simpl; auto.
+ + simpl; destruct (is_nan (Bplus m x y)) eqn:E.
+ * right. destruct (Bplus_nan_inv _ _ _ E) as [ [-> ->] | [ [ -> -> ] | ] ].
+ ** rewrite (le_infm_is_infm _ _ _ H4) in *.
+ rewrite (infp_le_is_infp _ _ _ H3) in *.
+ fdestruct l; simpl; fdestruct h'; simpl; intuition.
+ ** rewrite (le_infm_is_infm _ _ _ H0) in *.
+ rewrite (infp_le_is_infp _ _ _ H5) in *.
+ simpl in *.
+ fdestruct l'; simpl; fdestruct h; simpl; intuition.
+ ** destruct H as [-> | ->]; [ fdestruct h | fdestruct h' ].
+ * left; split; now apply Bplus_le_compat'.
+ + fdestruct y; fdestruct x; destruct n'; simpl; intuition.
+ + fdestruct y; fdestruct x; destruct n; simpl; intuition.
+ + fdestruct y; fdestruct x; destruct n; simpl; intuition.
+Qed.
Ltac classify_nan x :=
match goal with
@@ -100,72 +182,6 @@ Ltac classify_nan x :=
| _ => fail "can't determine if" x "is NaN"
end.
-Lemma Iadd2_nnan :
- forall m I1 I2,
- is_nan (Bplus m (lo I1) (lo I2)) = false ->
- is_nan (Bplus m (hi I1) (hi I2)) = false ->
- Iadd2 m I1 I2 = MK_INTERVAL (Bplus m (lo I1) (lo I2)) (Bplus m (hi I1) (hi I2)) (nan I1 || nan I2).
-Proof.
- intros; unfold Iadd2.
- fdestruct (Bplus m (lo I1) (lo I2));
- fdestruct (Bplus m (hi I1) (hi I2)).
-Qed.
-
-Axiom add_le_compat :
- forall m x1 y1 x2 y2,
- is_nan (Bplus m x1 x2) = false ->
- is_nan (Bplus m y1 y2) = false ->
- x1 <= y1 ->
- x2 <= y2 ->
- Bplus m x1 x2 <= Bplus m y1 y2.
-
-Lemma Iadd2_check :
- forall m Iâ‚ Iâ‚‚, check Iâ‚ -> check Iâ‚‚ -> check (Iadd2 m Iâ‚ Iâ‚‚).
-Proof.
- intros m [ ] [ ] [ ] [ ]; simpl in *.
- - destruct (is_nan (Bplus m lo0 lo1)) eqn:E1;
- destruct (is_nan (Bplus m hi0 hi1)) eqn:E2.
- + unfold Iadd2; simpl.
- rewrite (is_nan_inv _ E1).
- rewrite (is_nan_inv _ E2);
- unfold check; auto.
- + unfold Iadd2; simpl.
- apply Bplus_nan_if in E1; intuition; subst; try easy; simpl;
- fdestruct (Bplus m hi0 hi1); unfold check; simpl; auto;
- try (classify_nan lo0; auto);
- try (classify_nan lo1; auto).
- + unfold Iadd2; simpl.
- apply Bplus_nan_if in E2; intuition; subst; try easy; simpl;
- fdestruct (Bplus m lo0 lo1); unfold check; simpl; auto;
- try (classify_nan hi0; auto);
- try (classify_nan hi1; auto).
- + set (I1 := {| lo := lo0; hi := hi0; nan := nan0 |}).
- set (I2 := {| lo := lo1; hi := hi1; nan := nan1 |}).
- replace (lo0) with (lo I1) in * by auto.
- replace (lo1) with (lo I2) in * by auto.
- replace (hi0) with (hi I1) in * by auto.
- replace (hi1) with (hi I2) in * by auto.
- rewrite (Iadd2_nnan m I1 I2 E1 E2).
- unfold check; simpl; left.
- now apply add_le_compat.
- - destruct H0 as [-> ->].
- unfold check, Iadd2; destruct lo0, hi0; simpl; auto.
- - destruct H as [-> ->].
- unfold check, Iadd2; destruct lo1, hi1; simpl; auto.
- - destruct H as [-> ->].
- unfold check, Iadd2; destruct lo1, hi1; simpl; auto.
-Qed.
-
-Lemma Iadd2_nan_l :
- forall m I1 I2, nan I1 = true -> nan (Iadd2 m I1 I2) = true.
-Proof.
-Admitted.
-
-Lemma Iadd2_nan_r :
- forall m I1 I2, nan I2 = true -> nan (Iadd2 m I1 I2) = true.
-Proof.
-Admitted.
-
Lemma classification :
forall (f : float),
(f = NaN \/ is_finite f = true \/ is_infm f = true \/ is_infp f = true).
@@ -176,72 +192,4 @@ Qed.
Ltac classify f :=
destruct (classification f) as [ | [ | [ | ]]]; try (subst; easy).
-
-
-Lemma Iadd2_correct :
- forall m (x y : float) I1 I2, check I1 -> check I2 ->
- x ∈ I1 -> y ∈ I2 ->
- Bplus m x y ∈ Iadd2 m I1 I2.
-Proof.
- intros m x y [ ] [ ] [ ] [ ] [ ] [ ]; simpl in *.
- - classify lo0.
- + left; simpl; classify lo1; admit.
- + left; simpl; apply is_infm_inv in H3; subst. admit.
- + apply is_infp_inv in H3; subst.
- destruct H1.
- apply infp_le_is_infp in H1; rewrite H1 in *.
- apply infp_le_is_infp in H3; rewrite H3 in *.
- unfold Iadd2; fdestruct lo1; simpl; fdestruct hi1; simpl;
- fdestruct y; simpl; solve [left; intuition | right; intuition ].
- - apply Bool.andb_true_iff in H2.
- destruct H2 as [Hynan Hnan1].
- right; rewrite Iadd2_nan_r by auto.
- classify_nan y; fdestruct x.
- - apply Bool.andb_true_iff in H1.
- destruct H1 as [Hynan Hnan0].
- right; rewrite Iadd2_nan_l by auto.
- classify_nan x; fdestruct y.
- - apply Bool.andb_true_iff in H1.
- destruct H1 as [Hynan Hnan0].
- right; rewrite Iadd2_nan_l by auto.
- classify_nan x; fdestruct y.
- - now destruct H0 as [-> ->].
- - destruct H0 as [-> ->].
- unfold Iadd2; simpl.
- fdestruct lo0; fdestruct hi0; simpl;
- apply Bool.andb_true_iff in H2;
- destruct H2 as [Hynan Hnan1];
- right; simpl; classify_nan y;
- fdestruct x.
- - destruct H0 as [-> ->].
- unfold Iadd2; simpl.
- fdestruct lo0; fdestruct hi0.
- - destruct H0 as [-> ->].
- unfold Iadd2; simpl.
- fdestruct lo0; fdestruct hi0; simpl;
- apply Bool.andb_true_iff in H2;
- destruct H2 as [Hynan Hnan1];
- right; simpl; classify_nan y;
- fdestruct x.
- - now destruct H as [-> ->].
- - now destruct H as [-> ->].
- - destruct H as [-> ->].
- unfold Iadd2; simpl.
- apply Bool.andb_true_iff in H1.
- destruct H1 as [Hynan Hnan1].
- right; simpl; classify_nan x; reflexivity.
- - destruct H as [-> ->].
- unfold Iadd2; simpl.
- apply Bool.andb_true_iff in H1.
- destruct H1 as [Hynan Hnan1].
- right; simpl; classify_nan x; reflexivity.
- - now destruct H as [-> ->].
- - now destruct H as [-> ->].
- - now destruct H0 as [-> ->].
- - apply Bool.andb_true_iff in H1; destruct H1.
- apply Bool.andb_true_iff in H2; destruct H2.
- classify_nan x; classify_nan y; simpl.
- right; rewrite Iadd2_nan_l by auto; reflexivity.
-Admitted.
-
End Finterval.
\ No newline at end of file
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index f15c5136b161398deaf694cfa03def1f4e3499e0..af26311fde27c3f8bb1850ded07b1bee0737c7e0 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -596,6 +596,16 @@ Definition add (x y : Rx) : Rx :=
end
end.
+Lemma leb_trans :
+ forall x y z : Rx, leb x y = true -> leb y z = true -> leb x z = true.
+Proof.
+ intros [ rx | [ ] ] [ ry | [ ] ] [ rz | [ ] ] Hxy Hyz; simpl in *; try easy.
+ apply Rle_le in Hxy.
+ apply Rle_le in Hyz.
+ apply Raux.Rle_bool_true.
+ lra.
+Qed.
+
Lemma add_leb_compat :
forall x y z : Rx,
leb x y = true -> leb (add x z) (add y z) = true.
@@ -614,6 +624,17 @@ Proof.
- now destruct b, b0, b1.
Qed.
+Lemma add_leb_compat_l :
+ forall x y z : Rx,
+ leb x y = true -> leb (add z x) (add z y) = true.
+Proof.
+ intros [ | [ ]] [ | [ ]] [ | [ ]] H; try easy.
+ simpl in *.
+ apply Rle_le in H.
+ apply Raux.Rle_bool_true.
+ lra.
+Qed.
+
Lemma add_real :
forall (r1 r2 : R), add (Real r1) (Real r2) = Real (r1 + r2)%R.
Proof. reflexivity. Qed.