clean inter_correct proof

src_common/ieee/coq/Interval.v

@@ -257,6 +257,17 @@ 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.
+
 Lemma is_finite_not_nan :
   forall (x : float), is_finite x = true -> is_nan x = false.
 Proof. fdestruct x. Qed.
@@ -266,14 +277,10 @@ 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).
+  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.
@@ -282,16 +289,10 @@ Proof.
     * 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 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.
@@ -300,16 +301,8 @@ Proof.
     * 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 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.
@@ -318,15 +311,8 @@ Proof.
     * 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 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.
@@ -335,21 +321,6 @@ Proof.
     * 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 :=
-  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.
-
-
 End Finterval.
\ No newline at end of file