From d7e3a96d019152d0a507fb7cea06e20f219c06f6 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Fri, 23 Jul 2021 14:05:40 +0200
Subject: [PATCH] Add basic binary constraint propagators on Intervals

---
 src_common/ieee/coq/Interval.v  | 448 +++++++++++++-------------------
 src_common/ieee/coq/Rextended.v |  91 -------
 src_common/ieee/coq/Utils.v     | 121 +++++++++
 3 files changed, 299 insertions(+), 361 deletions(-)

diff --git a/src_common/ieee/coq/Interval.v b/src_common/ieee/coq/Interval.v
index 45217ccf5..dfcd035dd 100644
--- a/src_common/ieee/coq/Interval.v
+++ b/src_common/ieee/coq/Interval.v
@@ -118,9 +118,9 @@ Proof with auto.
     pose proof (le_not_nan_l _ _ H2).
     pose proof (le_not_nan_r _ _ H2).
     destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |]; try (fdestruct x ; fail).
-    + pose proof (Hlt1 := Bleb_trans _ _ _ _ _ Hc2 Hc1').
+    + pose proof (Hlt1 := Bleb_trans _ _ _ Hc2 Hc1').
       apply Bleb_true_Bltb in Hlt1...
-      pose proof (Hlt2 := Bleb_trans _ _ _ _ _ Hc1 Hc2').
+      pose proof (Hlt2 := Bleb_trans _ _ _ Hc1 Hc2').
       apply Bleb_true_Bltb in Hlt2...
       rewrite Hlt1, Hlt2; simpl; left; split; auto using Bmax_le, Bmin_le.
     + fdestruct x; destruct nan2, nan1, (Bltb hi1 _), (Bltb hi2); simpl; try easy.
@@ -195,309 +195,217 @@ Proof with auto.
   - right; fdestruct y; fdestruct x; destruct nan; simpl; intuition.
 Qed.
 
+Notation "'Interval+⊥'" := Interval_opt.
 
-(* Definition float := binary_float prec emax.
-
-Inductive Interval_aux :=
-  | I_Bot : Interval_aux
-  | I_nan : Interval_aux
-  | I_intv : forall (l h : float) (nan : bool), Interval_aux.
-
-Definition contains (I : Interval_aux) (x : float) : Prop :=
+Program Definition Ile (I : Interval) : Interval+⊥ :=
   match I with
-  | I_Bot => False
-  | I_nan => is_nan x = true
-  | I_intv l h n =>
-    l <= x <= h \/ (is_nan x && n = true)
+  | Inan => None
+  | Intv a b n =>
+    Some (Intv -oo b n)
   end.
+Next Obligation.
+  destruct I as [[|l1 h1] H1]; simpl in *; fdestruct b.
+  inversion Heq_I; subst.
+  fdestruct l1.
+Defined.
+
 
-Definition containsb (I : Interval_aux) (x : float) : bool :=
+Program Theorem Ile_correct :
+  forall (I : Interval) (x y : float), contains I y -> x <= y -> contains_opt (Ile I) x.
+Proof.
+  intros [[| l1 h1] H1] x y Hx Hxy; simpl in *.
+  - fdestruct y; fdestruct x.
+  - destruct (is_nan x), Hx as [ [H H'] | ];
+    try (left ; idtac; split; [ fdestruct x | apply (Bleb_trans _ _ _ Hxy H')]);
+    try (right ; fdestruct y; fdestruct x).
+Qed.
+
+Program Definition Ilt (I : Interval) : Interval+⊥ :=
   match I with
-  | I_Bot => true
-  | I_nan => is_nan x
-  | I_intv l h n =>
-    (Bleb l x && Bleb x h) || (is_nan x && n)
+  | Inan => None
+  | Intv a b n =>
+    Some (Intv -oo b n)
   end.
+Next Obligation.
+  destruct I as [[|l1 h1] H1]; simpl in *; fdestruct b;
+  inversion Heq_I; subst; fdestruct l1.
+Defined.
 
-Definition Iadd_up_to_NaN (I1 I2 : Interval_aux) : bool :=
-  match I1, I2 with
-  | I_Bot, _ => false
-  | _, I_Bot => false
-  | I_nan, _ => true
-  | _, I_nan => true
-  | I_intv l h n, I_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
-  | I_Bot, _ => I_Bot
-  | _, I_Bot => I_Bot
-  | I_nan, _ => I_nan
-  | _, I_nan => I_nan
-  | I_intv l h n, I_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 => I_nan
-      | false => I_intv +oo +oo true
-      end
-    | false =>
-      match is_nan sum2 with
-      | true => I_intv -oo -oo true
-      | false => I_intv sum1 sum2 (Iadd_up_to_NaN I1 I2)
-      end
-    end
-  end.
+Program Theorem Ilt_correct :
+  forall (I : Interval) (x y : float), contains I y -> Bltb x y = true -> contains_opt (Ilt I) x.
+Proof.
+  intros [[| l1 h1] H1] x y Hx Hxy; simpl in *.
+  - fdestruct y; fdestruct x.
+  - apply Bltb_Bleb in Hxy.
+    destruct (is_nan x), Hx as [ [H H'] | ];
+    try (left ; idtac; split; [ fdestruct x | apply (Bleb_trans _ _ _ Hxy H')]);
+    try (right ; fdestruct y; fdestruct x).
+Qed.
 
-Definition valid_interval (I : Interval_aux) : Prop :=
+Program Definition Ige (I : Interval) : Interval+⊥ :=
   match I with
-  | I_intv l h _ => l <= h
-  | _ => True
+  | Inan => None
+  | Intv a b n =>
+    Some (Intv a +oo n)
   end.
+Next Obligation.
+  destruct I as [[|l1 h1] H1]; simpl in *; fdestruct b;
+  inversion Heq_I; subst; fdestruct l1.
+Defined.
 
-Lemma valid_interval_Iadd :
-  forall m I1 I2, valid_interval I1 -> valid_interval I2 -> valid_interval (Iadd_aux m I1 I2).
+Program Theorem Ige_correct :
+  forall (I : Interval) (x y : float), contains I y -> Bleb y x = true -> contains_opt (Ige I) x.
 Proof.
-  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_mono_l _ _ _ (le_B2Rx _ _ H)).
-  - apply (add_leb_mono_r _ _ _ (le_B2Rx _ _ H')).
+  intros [[| l1 h1] H1] x y Hx Hxy; simpl in *.
+  - fdestruct y; fdestruct x.
+  - destruct (is_nan x), Hx as [ [H H'] | ];
+    try (left ; idtac; split; [ apply (Bleb_trans _ _ _ H Hxy) | fdestruct x; fdestruct y ]);
+    try (right ; fdestruct y; fdestruct x).
 Qed.
 
-Definition Interval := { I : Interval_aux | valid_interval I }.
-
-Program Definition Iadd (m : mode) (I1 I2 : Interval) : Interval :=
-  Iadd_aux m I1 I2.
+Program Definition Igt (I : Interval) : Interval+⊥ :=
+  match I with
+  | Inan => None
+  | Intv a b n =>
+    Some (Intv a +oo n)
+  end.
 Next Obligation.
-  apply valid_interval_Iadd;
-  now destruct I1, I2.
+  destruct I as [[|l1 h1] H1]; simpl in *; fdestruct b;
+  inversion Heq_I; subst; fdestruct l1.
 Defined.
 
-Program Lemma Iadd_correct :
-  forall m (I1 I2 : Interval) (x y : float), contains I1 x -> contains I2 y -> contains (Iadd m I1 I2) (Bplus m x y).
+Program Theorem Igt_correct :
+  forall (I : Interval) (x y : float), contains I y -> Bltb y x = true -> contains_opt (Ige I) x.
 Proof.
-  intros m [[ | | l h n ] H1] [[ | | l' h' n' ] H2] x y Hx Hy; 
-  simpl in *; try easy.
-  - fdestruct x.
-  - fdestruct x.
-  - fdestruct x; fdestruct y.
-  - 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.
+  intros [[| l1 h1] H1] x y Hx Hxy; simpl in *.
+  - fdestruct y; fdestruct x.
+  - apply Bltb_Bleb in Hxy.
+    destruct (is_nan x), Hx as [ [H H'] | ];
+    try (left ; idtac; split; [ apply (Bleb_trans _ _ _ H Hxy) | fdestruct x; fdestruct y ]);
+    try (right ; fdestruct y; fdestruct x).
 Qed.
 
-Definition inter_aux (I1 I2 : Interval_aux) : Interval_aux :=
+Program Definition inter_opt (I1 I2 : Interval+⊥) : Interval+⊥ :=
   match I1, I2 with
-  | I_Bot, _ => I_Bot
-  | _, I_Bot => I_Bot
-  | I_nan, I_nan => I_nan
-  | I_nan, I_intv _ _ b => if b then I_nan else I_Bot
-  | I_intv _ _ b, I_nan => if b then I_nan else I_Bot
-  | I_intv l h b, I_intv l' h' b' =>
-    if Bltb h l' || Bltb h' l then 
-      if (b && b') then I_nan else I_Bot 
-    else I_intv (Bmax l l') (Bmin h h') (b && b')
+  | None, _ => None
+  | _, None => None
+  | Some i1, Some i2 => inter i1 i2
   end.
+Next Obligation.
+  destruct I1 as [[[|l1 h1 n1]|] H1]; simpl in *; now inversion Heq_I1.
+Defined.
+Next Obligation.
+  destruct I2 as [[[|l1 h1 n1]|] H1]; simpl in *; now inversion Heq_I2.
+Defined.
 
-Lemma valid_interval_inter :
-  forall I1 I2, valid_interval I1 -> valid_interval I2 -> valid_interval (inter_aux I1 I2).
-Proof with auto.
-  intros [ | | l h] [ | | l' h'] H1 H2; simpl in *; try (now destruct nan); try easy.
-  case (Bltb h l') eqn:?, (Bltb h' l) eqn:?; simpl; try (now destruct nan, nan0).
-  pose proof (le_not_nan_r _ _ H1);
-  pose proof (le_not_nan_l _ _ H1);
-  pose proof (le_not_nan_r _ _ H2);
-  pose proof (le_not_nan_l _ _ H2).
-  auto using Bmax_le, Bmin_le, Bltb_false_Bleb.
-Qed.
-
-Program Definition inter (I1 I2 : Interval) : Interval :=
-  inter_aux I1 I2.
+Program Definition to_opt (I : Interval) : Interval+⊥ :=
+  Some (I :>).
 Next Obligation.
-  destruct I1, I2; simpl.
-  now apply valid_interval_inter.
+  now destruct I as [[| l h n ] H].
 Defined.
 
-Program Lemma inter_precise_l :
-  forall I1 I2, forall x, contains (inter I1 I2) x -> contains I1 x.
+Coercion to_opt : Interval >-> Interval_opt.
+
+Ltac fall_cases x :=
+  try (fdestruct x; fail).
+
+Ltac fall_cases2 x y :=
+  try (fdestruct x; fdestruct y; fail).
+
+
+Definition Ige_inv (I1 I2 : Interval) : Interval+⊥ * Interval+⊥ :=
+  (inter_opt (Ige I2) I1, inter_opt (Ile I1) I2).
+
+Program Theorem Ige_inv_correct : 
+  forall (I1 I2 : Interval) (x y : float),
+    contains I1 x -> contains I2 y ->
+    y <= x ->
+    contains_opt (fst (Ige_inv I1 I2)) x /\
+    contains_opt (snd (Ige_inv I1 I2)) y.
 Proof.
-  intros [ [ | | ? ? [ ]] H1 ] [ [ | | ? ? [ ]] H2 ] x Hx; simpl in *; try easy.
-  - intuition.
-  - destruct (Bltb h l0), (Bltb h0 l); simpl in *; try (rewrite Hx; intuition).
-    destruct Hx as [ [Hc1 Hc2] | ]; auto; left; split.
-    + now apply Bmax_le_inv in Hc1.
-    + now apply Bmin_le_inv in Hc2.
-  - destruct (Bltb h l0) eqn:E1, (Bltb h0 l) eqn:E2; simpl in *; auto.
-    destruct Hx as [ [ Hc1 Hc2 ] |  ]; auto; left; split.
-    + apply Bmax_le_inv in Hc1; intuition.
-    + apply Bmin_le_inv in Hc2; intuition.
-    + fdestruct x.
-    + fdestruct x.
-  - destruct (Bltb h l0) eqn:E1, (Bltb h0 l) eqn:E2; simpl in *; auto.
-    destruct Hx as [ [ Hc1 Hc2 ] |  ]; auto; left; split.
-    + apply Bmax_le_inv in Hc1; intuition.
-    + apply Bmin_le_inv in Hc2; intuition.
-  - destruct (Bltb h l0) eqn:E1, (Bltb h0 l) eqn:E2; simpl in *; auto.
-    destruct Hx as [ [ Hc1 Hc2 ] |  ]; auto; left; split.
-    + apply Bmax_le_inv in Hc1; intuition.
-    + apply Bmin_le_inv in Hc2; intuition.
-Defined.
+  intros [[|l1 h1 n1] H1] [[|l2 h2 n2] H2] x y Hx Hy Hxy; fall_cases2 x y.
+  split; apply inter_correct; simpl in *; auto.
+  + destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; fall_cases2 y x.
+    left; split; [ apply (Bleb_trans _ _ _ Hy Hxy) | fdestruct x ].
+  + destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; fall_cases2 y x.
+    left; split; [ fdestruct y; fdestruct x | apply (Bleb_trans _ _ _ Hxy Hx') ].
+Qed.
 
-Program Lemma inter_precise_r :
-  forall I1 I2, forall x, contains (inter I1 I2) x -> contains I2 x.
+
+Definition Igt_inv (I1 I2 : Interval) : Interval+⊥ * Interval+⊥ :=
+  (inter_opt (Igt I2) I1, inter_opt (Ilt I1) I2).
+
+Program Theorem Igt_inv_correct : 
+  forall (I1 I2 : Interval) (x y : float),
+    contains I1 x -> contains I2 y ->
+    Bltb y x = true ->
+    contains_opt (fst (Igt_inv I1 I2)) x /\
+    contains_opt (snd (Igt_inv I1 I2)) y.
 Proof.
-  intros [ [ | | ? ? [ ]] H1 ] [ [ | | ? ? [ ]] H2 ] x Hx; simpl in *; try easy.
-  - rewrite Hx; intuition.
-  - destruct (Bltb h l0), (Bltb h0 l); simpl in *; try (rewrite Hx; intuition).
-    destruct Hx as [ [Hc1 Hc2] | ]; auto; left; split.
-    + now apply Bmax_le_inv in Hc1.
-    + now apply Bmin_le_inv in Hc2.
-  - destruct (Bltb h l0), (Bltb h0 l); simpl in *; try easy.
-    destruct Hx as [ [Hc1 Hc2] | ]; auto; left; split.
-    + now apply Bmax_le_inv in Hc1.
-    + now apply Bmin_le_inv in Hc2.
-  - destruct (Bltb h l0), (Bltb h0 l); simpl in *; try easy.
-    destruct Hx as [ [Hc1 Hc2] | ]; auto; left; split.
-    + now apply Bmax_le_inv in Hc1.
-    + now apply Bmin_le_inv in Hc2.
-    + fdestruct x.
-    + fdestruct x.
-  - destruct (Bltb h l0), (Bltb h0 l); simpl in *; try easy.
-    destruct Hx as [ [Hc1 Hc2] | ]; auto; left; split.
-    + now apply Bmax_le_inv in Hc1.
-    + now apply Bmin_le_inv in Hc2.
-Defined.
+  intros [[|l1 h1 n1] H1] [[|l2 h2 n2] H2] x y Hx Hy Hxy; fall_cases2 x y.
+  split; apply inter_correct; simpl in *; auto; destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; auto; fall_cases2 x y.
+  + left; split.
+    * apply (Bleb_trans _ _ _ Hy (Bltb_Bleb _ _ _ _ Hxy)).
+    * fdestruct x.
+  + left; split.
+    * fdestruct y.
+    * apply (Bleb_trans _ _ _ (Bltb_Bleb _ _ _ _ Hxy) Hx').
+Qed.
 
+Definition Ilt_inv (I1 I2 : Interval) : Interval+⊥ * Interval+⊥ :=
+  (inter_opt (Ilt I2) I1, inter_opt (Igt I1) I2).
 
-Lemma classification :
-  forall (f : float),
-  (f = NaN \/ is_finite f = true \/ is_infm f = true \/ is_infp f = true).
+Program Theorem Ilt_inv_correct : 
+  forall (I1 I2 : Interval) (x y : float),
+    contains I1 x -> contains I2 y ->
+    Bltb x y = true ->
+    contains_opt (fst (Ilt_inv I1 I2)) x /\
+    contains_opt (snd (Ilt_inv I1 I2)) y.
 Proof.
-  intros; fdestruct f; intuition.
+  intros [[|l1 h1 n1] H1] [[|l2 h2 n2] H2] x y Hx Hy Hxy; fall_cases2 x y.
+  split; apply inter_correct; simpl in *; auto; destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; auto; fall_cases2 x y.
+  + left; split; fall_cases x.
+    apply (Bleb_trans _ _ _ (Bltb_Bleb _ _ _ _ Hxy) Hy').
+  + left; split; fall_cases y.
+    apply (Bleb_trans _ _ _ Hx (Bltb_Bleb _ _ _ _ Hxy)).
 Qed.
 
-Ltac classify f :=
-  destruct (classification f) as [ | [ | [ | ]]]; try (subst; easy).
-
-Ltac classify_nan x :=
-  match goal with
-  | [ H : is_nan x = true |- _ ] =>
-    rewrite (is_nan_inv x H) in *
-  | [ H : Bleb _ x = true |- _ ] =>
-    assert (is_nan x = false) by apply (le_not_nan_r _ _ H)
-  | [ H : Bleb x _ = true |- _ ] =>
-    assert (is_nan x = false) by apply (le_not_nan_l _ _ H)
-  | _ => fail "can't determine if" x "is NaN"
-  end.
+Definition Ile_inv (I1 I2 : Interval) : Interval+⊥ * Interval+⊥ :=
+  (inter_opt (Ile I2) I1, inter_opt (Ige I1) I2).
 
-Lemma is_finite_not_nan :
-  forall (x : float), is_finite x = true -> is_nan x = false.
-Proof. fdestruct x. Qed.
-  
+Program Theorem Ile_inv_correct : 
+  forall (I1 I2 : Interval) (x y : float),
+    contains I1 x -> contains I2 y ->
+    x <= y ->
+    contains_opt (fst (Ile_inv I1 I2)) x /\
+    contains_opt (snd (Ile_inv I1 I2)) y.
+Proof.
+  intros [[|l1 h1 n1] H1] [[|l2 h2 n2] H2] x y Hx Hy Hxy; fall_cases2 x y.
+  split; apply inter_correct; simpl in *; auto; destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; auto; fall_cases2 x y.
+  + left; split; fall_cases x.
+    apply (Bleb_trans _ _ _ Hxy Hy').
+  + left; split; fall_cases y.
+    apply (Bleb_trans _ _ _ Hx Hxy).
+Qed.
 
-Program Lemma inter_correct :
-  forall (I1 I2 : Interval) x,
-    contains I1 x -> contains I2 x -> contains (inter I1 I2) x.
+Definition Ieq_inv (I1 I2 : Interval) : Interval+⊥ * Interval+⊥ :=
+  (inter_opt I1 I2, inter_opt I1 I2).
+
+  Program Theorem Ieq_inv_correct : 
+  forall (I1 I2 : Interval) (x y : float),
+    contains I1 x -> contains I2 y ->
+    Beqb x y = true ->
+    contains_opt (fst (Ile_inv I1 I2)) x /\
+    contains_opt (snd (Ile_inv I1 I2)) y.
 Proof.
-  intros [ [ | | ? ? [ ]] H1 ] [ [ | | ? ? [ ]] H2 ] x Hx1 Hx2; simpl in *;
-  try easy; try (fdestruct x; intuition; fail).
-  - destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |]; try (fdestruct x ; fail).
-  + classify_nan l; classify_nan h; classify_nan l0; classify_nan h0.
-    destruct (Bltb h l0) eqn:E1, (Bltb h0 l) eqn:E2; simpl in *; try easy.
-    * apply Bltb_true_Bleb in E1; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc2 Hc1') in E1.
-    * apply Bltb_true_Bleb in E1; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc2 Hc1') in E1.
-    * apply Bltb_true_Bleb in E2; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc1 Hc2') in E2.
-    * left; split; [ now apply Bmax_le | now apply Bmin_le ].
-  + fdestruct x.
-    destruct (Bltb h _), (Bltb h0); simpl; auto.
-  - destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |]; try (fdestruct x ; fail).
-    classify_nan l; classify_nan h; classify_nan l0; classify_nan h0.
-    destruct (Bltb h l0) eqn:E1, (Bltb h0 l) eqn:E2; simpl in *; try easy.
-    * apply Bltb_true_Bleb in E1; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc2 Hc1') in E1.
-    * apply Bltb_true_Bleb in E1; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc2 Hc1') in E1.
-    * apply Bltb_true_Bleb in E2; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc1 Hc2') in E2.
-    * left; split; [ now apply Bmax_le | now apply Bmin_le ].
-  - destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |]; try (fdestruct x; fail).
-    classify_nan l; classify_nan h; classify_nan l0; classify_nan h0.
-    destruct (Bltb h l0) eqn:E1, (Bltb h0 l) eqn:E2; simpl in *; try easy.
-    * apply Bltb_true_Bleb in E1; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc2 Hc1') in E1.
-    * apply Bltb_true_Bleb in E1; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc2 Hc1') in E1.
-    * apply Bltb_true_Bleb in E2; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc1 Hc2') in E2.
-    * left; split; [ now apply Bmax_le | now apply Bmin_le ].
-  - destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |]; try (fdestruct x; fail).
-    classify_nan l; classify_nan h; classify_nan l0; classify_nan h0.
-    destruct (Bltb h l0) eqn:E1, (Bltb h0 l) eqn:E2; simpl in *; try easy.
-    * apply Bltb_true_Bleb in E1; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc2 Hc1') in E1.
-    * apply Bltb_true_Bleb in E1; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc2 Hc1') in E1.
-    * apply Bltb_true_Bleb in E2; auto.
-      now rewrite (Bleb_trans _ _ _ _ _ Hc1 Hc2') in E2.
-    * left; split; [ now apply Bmax_le | now apply Bmin_le ].
-Qed. *)
-
-End Finterval.
\ No newline at end of file
+  intros [[|l1 h1 n1] H1] [[|l2 h2 n2] H2] x y Hx Hy Hxy; fall_cases2 x y.
+  split; apply inter_correct; simpl in *; auto; destruct Hx as [[Hx Hx'] | Hx], Hy as [[Hy Hy'] | Hy]; auto; fall_cases2 x y.
+  + left; split; fall_cases x.
+    apply (Bleb_trans _ _ _ (Beqb_Bleb _ _ _ _ Hxy) Hy').
+  + left; split; fall_cases y.
+  apply (Bleb_trans _ _ _ Hx (Beqb_Bleb _ _ _ _ Hxy)).
+Qed.
+
+End Finterval.
+
diff --git a/src_common/ieee/coq/Rextended.v b/src_common/ieee/coq/Rextended.v
index 593261921..5262270bc 100644
--- a/src_common/ieee/coq/Rextended.v
+++ b/src_common/ieee/coq/Rextended.v
@@ -8,63 +8,6 @@ From F Require Import Utils.
 
 Set Implicit Arguments.
 
-(**
-  Usefull facts & definitions about R
-*)
-Section Rutils.
-
-Definition sign (r : R) :=
-  Raux.Rlt_bool r 0.
-
-Lemma sign_pos_inv :
-  forall r, sign r = false -> (0 <= r)%R.
-Proof.
-  intros.
-  unfold sign in H.
-  now destruct (Raux.Rlt_bool_spec r 0).
-Qed.
-
-Lemma sign_neg_inv :
-  forall r, sign r = true -> (r <= 0)%R.
-Proof.
-  intros.
-  unfold sign in H. left.
-  now destruct (Raux.Rlt_bool_spec r 0).
-Qed.
-
-Lemma sign_neg_inv_strict:
-  forall r, sign r = true -> (r < 0)%R.
-Proof.
-  intros.
-  unfold sign in H.
-  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.
-
-Lemma IZR_neg :
-  (forall x, IZR (Z.neg x) < 0)%R.
-Proof.
-  induction x; try lra;
-  apply (Rgt_trans _ (IZR (Z.neg x))); auto;
-  apply IZR_lt; lia.
-Qed.
-
-Lemma IZR_pos :
-  (forall x, IZR (Z.pos x) > 0)%R.
-Proof.
-  induction x; try lra;
-  apply (Rgt_trans _ (IZR (Z.pos x))); auto;
-  apply IZR_lt; lia.
-Qed.
-
-End Rutils.
-
-
 (**
   Inject BinarySingleNan in R extended with infinities
 *)
@@ -199,10 +142,6 @@ Lemma F2R_congr :
   @Defs.F2R Zaux.radix2 {| Defs.Fnum := m2; Defs.Fexp := e2 |}.
 Proof. congruence. Qed.
 
-
-
-
-
 Definition round (m : mode) (r : Rx) : Rx :=
   match r with
   | Real x =>
@@ -214,37 +153,7 @@ Definition round (m : mode) (r : Rx) : Rx :=
   | _  => r
   end.
 
-Lemma pos_Rleb_neg :
-  forall r1 r2, 
-    sign r1 = false ->
-    sign r2 = true ->
-    Raux.Rle_bool r1 r2 = false.
-Proof.
-  intros. unfold sign in *.
-  destruct (Raux.Rlt_bool_spec r1 0); try easy.
-  destruct (Raux.Rlt_bool_spec r2 0); try easy.
-  apply Raux.Rle_bool_false; lra.
-Qed.
 
-Lemma Rleb_Rle :
-  forall r1 r2, Raux.Rle_bool r1 r2 = true -> (r1 <= r2)%R.
-Proof.
-  intros.
-  now destruct (Raux.Rle_bool_spec r1 r2).
-Qed.
-
-Lemma Rltb_Rlt :
-  forall r1 r2, Raux.Rlt_bool r1 r2 = true -> (r1 < r2)%R.
-Proof.
-  intros.
-  now destruct (Raux.Rlt_bool_spec r1 r2).
-Qed.
-
-Lemma Rsign_split :
-  forall (r : R), (r < 0 \/ r = 0 \/ r > 0)%R.
-Proof.
-  intros. lra.
-Qed.
 
 Lemma dont_overflow_inv :
   forall m (r : R),
diff --git a/src_common/ieee/coq/Utils.v b/src_common/ieee/coq/Utils.v
index 191041f58..277f1a5c4 100644
--- a/src_common/ieee/coq/Utils.v
+++ b/src_common/ieee/coq/Utils.v
@@ -2,6 +2,101 @@ From Flocq Require Import IEEE754.BinarySingleNaN.
 From Coq Require Import ZArith Lia Reals Psatz Bool.
 (* From F Require Import Rextended. *)
 
+(**
+  Usefull facts & definitions about R
+*)
+Section Rutils.
+
+Definition sign (r : R) :=
+  Raux.Rlt_bool r 0.
+
+Lemma sign_pos_inv :
+  forall r, sign r = false -> (0 <= r)%R.
+Proof.
+  intros.
+  unfold sign in H.
+  now destruct (Raux.Rlt_bool_spec r 0).
+Qed.
+
+Lemma sign_neg_inv :
+  forall r, sign r = true -> (r <= 0)%R.
+Proof.
+  intros.
+  unfold sign in H. left.
+  now destruct (Raux.Rlt_bool_spec r 0).
+Qed.
+
+Lemma sign_neg_inv_strict:
+  forall r, sign r = true -> (r < 0)%R.
+Proof.
+  intros.
+  unfold sign in H.
+  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.
+
+Lemma IZR_neg :
+  (forall x, IZR (Z.neg x) < 0)%R.
+Proof.
+  induction x; try lra;
+  apply (Rgt_trans _ (IZR (Z.neg x))); auto;
+  apply IZR_lt; lia.
+Qed.
+
+Lemma IZR_pos :
+  (forall x, IZR (Z.pos x) > 0)%R.
+Proof.
+  induction x; try lra;
+  apply (Rgt_trans _ (IZR (Z.pos x))); auto;
+  apply IZR_lt; lia.
+Qed.
+
+Lemma pos_Rleb_neg :
+  forall r1 r2, 
+    sign r1 = false ->
+    sign r2 = true ->
+    Raux.Rle_bool r1 r2 = false.
+Proof.
+  intros. unfold sign in *.
+  destruct (Raux.Rlt_bool_spec r1 0); try easy.
+  destruct (Raux.Rlt_bool_spec r2 0); try easy.
+  apply Raux.Rle_bool_false; lra.
+Qed.
+
+Lemma Rleb_Rle :
+  forall r1 r2, Raux.Rle_bool r1 r2 = true -> (r1 <= r2)%R.
+Proof.
+  intros.
+  now destruct (Raux.Rle_bool_spec r1 r2).
+Qed.
+
+Lemma Reqb_Req :
+  forall r1 r2, Raux.Req_bool r1 r2 = true -> (r1 = r2)%R.
+Proof.
+  intros.
+  now destruct (Raux.Req_bool_spec r1 r2).
+Qed.
+
+Lemma Rltb_Rlt :
+  forall r1 r2, Raux.Rlt_bool r1 r2 = true -> (r1 < r2)%R.
+Proof.
+  intros.
+  now destruct (Raux.Rlt_bool_spec r1 r2).
+Qed.
+
+Lemma Rsign_split :
+  forall (r : R), (r < 0 \/ r = 0 \/ r > 0)%R.
+Proof.
+  intros. lra.
+Qed.
+
+End Rutils.
+
 (*********************************************************
        Simple & usefull results on floats
 **********************************************************)
@@ -60,6 +155,14 @@ Proof.
   exact (proj2 (le_not_nan x y H)).
 Qed.
 
+Lemma infm_min :
+  forall (x : float), is_nan x = false -> -oo <= x.
+Proof. fdestruct x. Qed.
+
+Lemma infp_max :
+  forall (x : float), is_nan x = false -> x <= +oo.
+Proof. fdestruct x. Qed.
+
 Lemma infp_le_is_infp :
   forall x : float, +oo <= x -> x = +oo.
 Proof.
@@ -252,6 +355,15 @@ Proof.
   lra.
 Qed.
 
+Lemma Beqb_Bleb :
+  forall x y : float, Beqb x y = true -> Bleb x y = true.
+Proof.
+  intros x y Hxy.
+  fdestruct x; fdestruct y; rewrite Beqb_correct in Hxy; auto;
+  apply Rle_Bleb; auto; right;
+  now apply Reqb_Req in Hxy.
+Qed.
+
 Lemma Bleb_refl :
   forall x:float, is_nan x = false -> Bleb x x = true.
 Proof.
@@ -455,6 +567,13 @@ Proof.
     now apply (Bleb_trans z y x).
 Qed.
 
+Lemma Bpred_not_nan :
+  forall (x : float), is_nan x = false -> is_nan (Bpred x) = false.
+Proof.
+  intros x <-.
+  apply is_nan_Bpred.
+Qed.
+
 End Utils.
 
 Arguments le_not_nan {prec} {emax}.
@@ -472,3 +591,5 @@ Arguments Bmax_max_1 {prec} {emax}.
 Arguments Bmax_max_2 {prec} {emax}.
 Arguments Bmin_min_1 {prec} {emax}.
 Arguments Bmin_min_2 {prec} {emax}.
+Arguments Bleb_trans {prec} {emax}.
+Arguments Bltb_Bleb_trans {prec} {emax}.
-- 
GitLab