[ieee/coq] wip on Iadd2_correct

src_common/ieee/coq/Fdom.v

+From Flocq Require Import IEEE754.BinarySingleNaN.
+From Coq Require Import ZArith.
+
+Definition Powerset (A : Type) := A -> Prop.
+
+Notation "𝓟( A )" := (Powerset A).
+
+Module Type Fformat.
+  Parameter prec : Z.
+  Parameter emax : Z.
+  Axiom Hprec : FLX.Prec_gt_0 prec.
+  Axiom Hemax : Prec_lt_emax prec emax.
+End Fformat.
+
+Module Fdom (F : Fformat).
+
+  Parameter Dom : Type.
+
+  Parameter γ : Dom -> 𝓟(binary_float F.prec F.emax).
+
+  Parameter add : Dom -> Dom -> Dom.
+
+  Axiom add_correct :
+    forall (m : mode) (d1 d2 : Dom) (x y : binary_float F.prec F.emax),
+      γ d1 x ->
+      γ d1 y ->
+      γ (add d1 d2) (@Bplus F.prec F.emax F.Hprec F.Hemax m x y).
+
+End Fdom.

src_common/ieee/coq/Finterval.v

 From Flocq Require Import IEEE754.BinarySingleNaN.
 From Coq Require Import QArith Psatz Reals Extraction.
-Require Import F.Futils.
+Require Import F.Futils F.Fdom.
 
 (*********************************************************
        Interval arithmetic over floatting points
@@ -45,7 +45,7 @@ Proof.
   intros.
   unfold top, γ; simpl.
   destruct (is_nan x) eqn:E.
-  - destruct (is_nan_inv _ _ x E); auto.
+  - destruct (is_nan_inv x E); auto.
   - left; split; fdestruct x.
 Qed.
 
@@ -126,8 +126,8 @@ Proof.
   - 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);
+      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;
@@ -156,11 +156,90 @@ Proof.
     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).
+Proof.
+  intros; fdestruct f; intuition.
+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

src_common/ieee/coq/Futils.v

@@ -194,4 +194,8 @@ End Utils.
 
 Arguments le_not_nan {prec} {emax}.
 Arguments le_not_nan_l {prec} {emax}.
-Arguments le_not_nan_r {prec} {emax}.
\ No newline at end of file
+Arguments le_not_nan_r {prec} {emax}.
+Arguments is_nan_inv {prec} {emax}.
+Arguments is_infm {prec} {emax}.
+Arguments is_infp {prec} {emax}.
+Arguments is_inf {prec} {emax}.

src_common/ieee/coq/_CoqProject

 -R ./ F
+./Fdom.v
 ./Finterval.v
 ./Fauto.v
 ./Rextended.v