cleaner intervals

src_common/ieee/coq/Colibri2_interval.v

+From Coq Require Import ZArith Extraction Bool.
+From F Require Import Utils Interval.
+From Flocq Require Import IEEE754.BinarySingleNaN FLX.
+
+Section Colibri2_interval.
+
+Variable prec : Z.
+Variable emax : Z.
+Context (Hprec : Prec_gt_0 prec).
+Context (Hemax : Prec_lt_emax prec emax).
+
+Definition float := binary_float prec emax.
+
+Inductive Interval' :=
+ | Inan : Interval'
+ | Intv : forall (lo hi : float) (nan : bool), Interval'.
+
+Definition valid (I : option Interval') :=
+  match I with
+  | Some (Intv lo hi _) => lo <= hi
+  | _ => True
+  end.
+
+Definition Interval := { I : option Interval' | valid I }.
+
+Program Definition contains (I : option Interval') (x : float) : Prop :=
+  match I with
+  | None => False
+  | Some Inan => is_nan x = true
+  | Some (Intv lo hi nan) =>
+    lo <= x <= hi \/ (is_nan x && nan = true)
+  end.
+
+Program Definition inter' (I1 I2 : option Interval') : option Interval' :=
+  match I1, I2 with
+  | None, _ => None
+  | _, None => None
+  | Some Inan, Some Inan => Some Inan
+  | Some Inan, Some (Intv _ _ nan) =>
+    if nan then Some Inan else None
+  | Some (Intv _ _ nan), Some (Inan) =>
+    if nan then Some (Inan) else None
+  | Some (Intv lo1 hi1 nan1), Some (Intv lo2 hi2 nan2) =>
+    if Bltb hi1 lo2 || Bltb hi2 lo1 then
+      if nan1 && nan2 then Some Inan else None
+    else
+      Some (Intv (Bmax lo1 lo2) (Bmin hi1 hi2) (nan1 && nan2))
+  end.
+
+Ltac ieasy :=
+  simpl in *; try easy; try (intuition; fail).
+
+Ltac sdestruct x :=
+  try destruct x; simpl; easy.
+  
+
+Program Definition inter (I1 I2 : Interval) : Interval :=
+  inter' I1 I2.
+Next Obligation with auto.
+  destruct I1 as [[[ | lo1 hi1 nan1]|] H1], I2 as [[[ | lo2 hi2 nan2]|] H2]; ieasy; try (now destruct nan1 || now destruct nan2).
+  case (Bltb (hi1) (lo2)) eqn:?, (Bltb (hi2) (lo1)) eqn:?; simpl; try (destruct nan1, nan2; simpl; easy).
+  pose proof (le_not_nan_l _ _ H1).
+  pose proof (le_not_nan_r _ _ H2).
+  pose proof (le_not_nan_r _ _ H1).
+  pose proof (le_not_nan_l _ _ H2).
+  auto using Bmax_le, Bmin_le, Bltb_false_Bleb.
+Defined.
+
+Program Lemma inter_precise_l :
+  forall I1 I2, forall x, contains (inter I1 I2) x -> contains I1 x.
+Proof with auto.
+  intros [[[|lo1 hi1 [ ]]|] H1] [[[|lo2 hi2 [ ]]|] H2] x Hx; simpl in *...
+  + intuition.
+  + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
+    left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
+  + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
+    - left; split; [apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
+    - destruct x...
+  + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
+    left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
+  + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
+    left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
+Qed.
+
+Program Lemma inter_precise_r :
+  forall I1 I2, forall x, contains (inter I1 I2) x -> contains I2 x.
+Proof with auto.
+  intros [[[|lo1 hi1 [ ]]|] H1] [[[|lo2 hi2 [ ]]|] H2] x Hx; simpl in *...
+  + intuition.
+  + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
+    left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
+  + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
+    left; split; [apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
+  + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
+    - left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
+    - destruct x...
+  + case (Bltb hi1 lo2) eqn:?, (Bltb hi2 lo1) eqn:?; simpl in *; intuition.
+    left; split; [ apply (Bmax_le_inv _ _ _ _ _ H0) | apply (Bmin_le_inv _ _ _ _ _ H3) ].
+Qed.
+
+Program Lemma inter_correct :
+  forall (I1 I2 : Interval), forall x,  contains I1 x -> contains I2 x -> contains (inter I1 I2) x.
+Proof with auto.
+  intros [[[|lo1 hi1 nan1]|] H1] [[[|lo2 hi2 nan2]|] H2] x Hx1 Hx2; simpl in *...
+  - fdestruct x; destruct nan2, Hx2; try easy.
+  - fdestruct x; destruct nan1, Hx1; try easy.
+  - 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 Hx1 as [[Hc1 Hc1'] |], Hx2 as [[Hc2 Hc2'] |]; try (fdestruct x ; fail).
+    + pose proof (Hlt1 := Bleb_trans _ _ _ _ _ Hc2 Hc1').
+      apply Bleb_true_Bltb in Hlt1...
+      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.
+      now right.
+Qed.
+
+End Colibri2_interval.
+
+Recursive Extraction Interval.
+
+
+
+

src_common/ieee/coq/Interval.v

 From Flocq Require Import IEEE754.BinarySingleNaN.
 From Coq Require Import QArith Psatz Reals Extraction.
-Require Import F.Utils F.Domains F.Correction_thms F.Rextended.
+Require Import  F.Utils F.Domains F.Correction_thms F.Rextended.
 
 (*********************************************************
        Interval arithmetic over floatting points
@@ -102,7 +102,7 @@ Program Lemma Iadd_correct :
 Proof.
   intros m [[ | | l h n ] H1] [[ | | l' h' n' ] H2] x y Hx Hy; 
   simpl in *; try easy.
-  - now (fdestruct x; rewrite Hy).
+  - 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.
@@ -173,20 +173,14 @@ Definition inter_aux (I1 I2 : Interval_aux) : Interval_aux :=
 
 Lemma valid_interval_inter :
   forall I1 I2, valid_interval I1 -> valid_interval I2 -> valid_interval (inter_aux I1 I2).
-Proof.
-  intros [ | | l h ] [ | | l' h'] H1 H2; simpl in *; try easy.
-  + now destruct nan.
-  + now destruct nan.
-  + 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.
-    - fdestruct h; fdestruct l.
-    - fdestruct l'.
-    - fdestruct h'; fdestruct l'.
-    - fdestruct l.
+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 :=

src_common/ieee/coq/_CoqProject

 -R ./ F
 ./Domains.v
 ./Interval.v
+./Colibri2_interval.v
 ./Tactics.v
 ./Rextended.v
 ./Utils.v