From 7ac41d60e63177dc51c7916c8fe6236742d06e1c Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Mon, 19 Jul 2021 16:00:19 +0200
Subject: [PATCH] Fix interval intersection + correction proof

---
 src_common/ieee/coq/Interval.v | 139 ++++++++++++++++++++++++++-------
 src_common/ieee/coq/Utils.v    |  41 ++++++++++
 2 files changed, 152 insertions(+), 28 deletions(-)

diff --git a/src_common/ieee/coq/Interval.v b/src_common/ieee/coq/Interval.v
index 5fa645d36..f08bcaf57 100644
--- a/src_common/ieee/coq/Interval.v
+++ b/src_common/ieee/coq/Interval.v
@@ -166,7 +166,7 @@ Definition inter_aux (I1 I2 : Interval_aux) : Interval_aux :=
   | 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 Bleb h l' || Bleb h' l then 
+    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')
   end.
@@ -177,14 +177,12 @@ Proof.
   intros [ | | l h ] [ | | l' h'] H1 H2; simpl in *; try easy.
   + now destruct nan.
   + now destruct nan.
-  + destruct (Bleb h l') eqn:Hhl'; simpl; try (now destruct nan, nan0).
-    destruct (Bleb h' l) eqn:Hh'l; simpl; try (now destruct nan, nan0).
-    apply Bleb_false_Bltb in Hh'l.
-    apply Bleb_false_Bltb in Hhl'.
+  + destruct (Bltb h l') eqn:Hhl'; simpl; try (now destruct nan, nan0).
+    destruct (Bltb h' l) eqn:Hh'l; simpl; try (now destruct nan, nan0).
+    apply Bltb_false_Bleb in Hh'l.
+    apply Bltb_false_Bleb in Hhl'.
     - destruct (Bmax_max_1 l l') as [-> | ->];
       destruct (Bmin_min_1 h h') as [-> | ->]; auto.
-      * now apply Bltb_Bleb in Hh'l.
-      * now apply Bltb_Bleb in Hhl'.
     - fdestruct h; fdestruct l.
     - fdestruct l'.
     - fdestruct h'; fdestruct l'.
@@ -198,54 +196,148 @@ Next Obligation.
   now apply valid_interval_inter.
 Defined.
 
-Program Lemma inter_correct_l :
+Program Lemma inter_precise_l :
   forall I1 I2, forall x, contains (inter I1 I2) x -> contains I1 x.
 Proof.
   intros [ [ | | ? ? [ ]] H1 ] [ [ | | ? ? [ ]] H2 ] x Hx; simpl in *; try easy.
   - intuition.
-  - destruct (Bleb h l0), (Bleb h0 l); simpl in *; try (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 (Bleb h l0) eqn:E1, (Bleb h0 l) eqn:E2; simpl in *; auto.
+    + 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 (Bleb h l0) eqn:E1, (Bleb h0 l) eqn:E2; simpl in *; auto.
+  - 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 (Bleb h l0) eqn:E1, (Bleb h0 l) eqn:E2; simpl in *; auto.
+  - 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.
-Qed.
+Defined.
 
-Program Lemma inter_correct_r :
+Program Lemma inter_precise_r :
   forall I1 I2, forall x, contains (inter I1 I2) x -> contains I2 x.
 Proof.
   intros [ [ | | ? ? [ ]] H1 ] [ [ | | ? ? [ ]] H2 ] x Hx; simpl in *; try easy.
   - rewrite Hx; intuition.
-  - destruct (Bleb h l0), (Bleb h0 l); simpl in *; try (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 (Bleb h l0), (Bleb h0 l); simpl in *; try easy.
+  - 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 (Bleb h l0), (Bleb h0 l); simpl in *; try easy.
+  - 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 (Bleb h l0), (Bleb h0 l); simpl in *; try easy.
+  - 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.
+
+
+Lemma classification :
+  forall (f : float),
+  (f = NaN \/ is_finite f = true \/ is_infm f = true \/ is_infp f = true).
+Proof.
+  intros; fdestruct f; intuition.
+Qed.
+
+Ltac classify f :=
+  destruct (classification f) as [ | [ | [ | ]]]; try (subst; easy).
+
+Lemma is_finite_not_nan :
+  forall (x : float), is_finite x = true -> is_nan x = false.
+Proof. fdestruct x. Qed.
+  
+
+Program Lemma inter_correct :
+  forall (I1 I2 : Interval) x,
+    contains I1 x -> contains I2 x -> contains (inter I1 I2) x.
+Proof.
+  intros [ [ | | ? ? [ ]] H1 ] [ [ | | ? ? [ ]] H2 ] x Hx1 Hx2; simpl in *; try easy.
+  - fdestruct x; intuition.
+  - destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |].
+  + pose proof (le_not_nan_r _ _ Hc1).
+    pose proof (le_not_nan_l _ _ H1).
+    pose proof (le_not_nan_r _ _ H1).
+    pose proof (le_not_nan_l _ _ H2).
+    pose proof (le_not_nan_r _ _ H2).
+    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.
+  + fdestruct x.
+  + fdestruct x.
+    destruct (Bltb h _), (Bltb h0); simpl; auto.
+  - destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |].
+  + pose proof (le_not_nan_r _ _ Hc1).
+    pose proof (le_not_nan_l _ _ H1).
+    pose proof (le_not_nan_r _ _ H1).
+    pose proof (le_not_nan_l _ _ H2).
+    pose proof (le_not_nan_r _ _ H2).
+    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.
+  + fdestruct x.
+  + fdestruct x.
+  - fdestruct x; intuition.
+  - destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |].
+  + pose proof (le_not_nan_r _ _ Hc1).
+    pose proof (le_not_nan_l _ _ H1).
+    pose proof (le_not_nan_r _ _ H1).
+    pose proof (le_not_nan_l _ _ H2).
+    pose proof (le_not_nan_r _ _ H2).
+    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.
+  + fdestruct x.
+  + fdestruct x.
+  - destruct Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |].
+  + pose proof (le_not_nan_r _ _ Hc1).
+    pose proof (le_not_nan_l _ _ H1).
+    pose proof (le_not_nan_r _ _ H1).
+    pose proof (le_not_nan_l _ _ H2).
+    pose proof (le_not_nan_r _ _ H2).
+    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.
+  + fdestruct x.
+  + fdestruct x.
 Qed.
 
 Ltac classify_nan x :=
@@ -259,14 +351,5 @@ Ltac classify_nan x :=
   | _ => fail "can't determine if" x "is NaN"
   end.
 
-Lemma classification :
-  forall (f : float),
-  (f = NaN \/ is_finite f = true \/ is_infm f = true \/ is_infp f = true).
-Proof.
-  intros; fdestruct f; intuition.
-Qed.
-
-Ltac classify f :=
-  destruct (classification f) as [ | [ | [ | ]]]; try (subst; easy).
 
 End Finterval.
\ No newline at end of file
diff --git a/src_common/ieee/coq/Utils.v b/src_common/ieee/coq/Utils.v
index 41758dcf4..191041f58 100644
--- a/src_common/ieee/coq/Utils.v
+++ b/src_common/ieee/coq/Utils.v
@@ -284,6 +284,47 @@ Proof.
   apply Rlt_Bltb; auto.
 Qed.
 
+Lemma Bltb_false_Bleb :
+  forall x y:float, is_nan x = false -> is_nan y = false -> Bltb x y = false -> Bleb y x = true.
+Proof.
+  intros x y Hx Hy Hxy.
+  destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
+  unfold Bltb, SpecFloat.SFltb in Hxy;
+  replace (SpecFloat.SFcompare (B2SF _) (B2SF _)) with (Bcompare x y) in Hxy by auto;
+  assert (Fx: is_finite x = true) by (rewrite Ex; auto);
+  assert (Fy: is_finite y = true) by (rewrite Ey; auto);
+  rewrite (Bcompare_correct _ _ x y Fx Fy) in Hxy; auto;
+  destruct (Raux.Rcompare _ _) eqn:E; try easy;
+  (apply Raux.Rcompare_Eq_inv in E || apply Raux.Rcompare_Gt_inv in E);
+  apply Rle_Bleb; auto; lra.
+Qed.
+
+Lemma Bltb_true_Bleb :
+  forall x y:float, is_nan x = false -> is_nan y = false -> Bltb x y = true -> Bleb y x = false.
+Proof.
+  intros x y Hx Hy Hxy.
+  destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
+  assert (Fx: is_finite x = true) by (rewrite Ex; auto);
+  assert (Fy: is_finite y = true) by (rewrite Ey; auto);
+  apply (Bltb_Rlt _ _ Fx Fy) in Hxy;
+  apply not_true_is_false; intros Hcontr;
+  apply (Bleb_Rle _ _ Fy Fx) in Hcontr;
+  lra.
+Qed.
+
+Lemma Bleb_true_Bltb :
+  forall x y:float, is_nan x = false -> is_nan y = false -> Bleb x y = true -> Bltb y x = false.
+Proof.
+  intros x y Hx Hy Hxy.
+  destruct x as [ | [ ] | | ] eqn:Ex, y as [ | [ ] | | ] eqn:Ey; try easy; rewrite <- Ex, <- Ey in *;
+  assert (Fx: is_finite x = true) by (rewrite Ex; auto);
+  assert (Fy: is_finite y = true) by (rewrite Ey; auto);
+  apply (Bleb_Rle _ _ Fx Fy) in Hxy;
+  apply not_true_is_false; intros Hcontr;
+  apply (Bltb_Rlt _ _ Fy Fx) in Hcontr;
+  lra.
+Qed.
+
 Definition Bmax (f1 f2 : float) : float :=
   if is_nan f1 || is_nan f2 then NaN
   else if Bleb f1 f2 then f2
-- 
GitLab