[ieee/coq] backup the wip on proofs

src_common/ieee/coq/Finterval.v

@@ -119,6 +119,8 @@ Axiom add_le_compat :
     x2 <= y2 ->
     Bplus m x1 x2 <= Bplus m y1 y2.
 
+Check (Bplus_correct).
+
 Lemma Iadd2_check :
   forall m I₁ I₂, check I₁ -> check I₂ -> check (Iadd2 m I₁ I₂).
 Proof.
@@ -176,6 +178,8 @@ 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 ->

src_common/ieee/coq/Rextended.v

@@ -20,21 +20,7 @@ Inductive Rx : Type :=
   | Real : R -> Rx
   | Inf  : bool -> Rx.
 
-Definition round (m : mode) (r : Rx) : Rx :=
-  match r with
-  | Real x =>
-    Real (Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax) (round_mode m) x)
-  | _  => r
-  end.
-
-Lemma round_inf :
-  forall m b, round m (Inf b) = Inf b.
-Proof. reflexivity. Qed.
-
-Lemma round_real :
-  forall m r,
-    round m (Real r) = Real (Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax) (round_mode m) r).
-Proof. reflexivity. Qed.
+Definition fmax : R := Raux.bpow Zaux.radix2 emax.
 
 Definition leb (x y : Rx) :=
   match x with
@@ -51,6 +37,202 @@ Definition leb (x y : Rx) :=
     end
   end.
 
+Definition do_overflow (m : mode) (x : R) : bool :=
+  let fexp := SpecFloat.fexp prec emax in
+  let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) x in
+  Raux.Rle_bool fmax (Rabs rsum).
+
+Definition dont_overflow (m : mode) (x : R) : bool :=
+  let fexp := SpecFloat.fexp prec emax in
+  let rsum := Generic_fmt.round Zaux.radix2 fexp (round_mode m) x in
+  Raux.Rlt_bool (Rabs rsum) fmax.
+
+Lemma do_overflow_false :
+  forall m r, do_overflow m r = false -> dont_overflow m r = true.
+Proof.
+  intros. unfold do_overflow, dont_overflow in *.
+  now rewrite <- Raux.negb_Rlt_bool, H.
+Qed.
+
+Definition sign (r : R) :=
+  Raux.Rlt_bool r 0.
+
+Definition round (m : mode) (r : Rx) : Rx :=
+  match r with
+  | Real x =>
+    if do_overflow m x then 
+      if overflow_to_inf m (sign x) then Inf (sign x)
+      else Real (if (sign x) then -fmax else fmax)
+    else
+      Real (Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax) (round_mode m) x)
+  | _  => r
+  end.
+
+Lemma sign_le :
+  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 Rle_le :
+  forall r1 r2, Raux.Rle_bool r1 r2 = true -> (r1 <= r2)%R.
+Proof.
+  intros.
+  now destruct (Raux.Rle_bool_spec r1 r2).
+Qed.
+
+Lemma fmax_gt_0: (fmax > 0)%R.
+  apply Raux.bpow_gt_0.
+Qed.
+
+Theorem do_overflow_iff:
+  forall m x,
+    let fexp := SpecFloat.fexp prec emax in
+    let rx := Generic_fmt.round Zaux.radix2 fexp (round_mode m) x in
+    do_overflow m x = true <-> (Raux.Rle_bool fmax rx = true \/ Raux.Rle_bool rx (-fmax)%R = true).
+Proof.
+  intros; split; intros.
+  - unfold do_overflow in H.
+    unfold Rabs in H.
+    destruct Rcase_abs.
+    + apply Rle_le in H.
+      right. apply Raux.Rle_bool_true.
+      apply Ropp_le_contravar in H.
+      replace (rx) with (--rx)%R by lra.
+      subst rx; auto.
+    + apply Rle_le in H.
+      left. apply Raux.Rle_bool_true.
+      auto.
+  - destruct H; apply Raux.Rle_bool_true; apply Rle_le in H.
+    + eauto using Rle_trans, H, Rle_abs.
+    + apply Ropp_le_contravar in H.
+      replace (--fmax)%R with fmax in H by lra.
+      pose proof fmax_gt_0.
+      assert (0 <= -rx)%R by lra.
+      assert (0 > rx)%R by lra.
+      assert (-rx > rx)%R by lra.
+      assert (Rabs rx = - rx)%R by auto using Rabs_left.
+      rewrite <- H4 in H.
+      auto.
+Qed.
+
+Lemma overflow_le :
+  forall m r1 r2, 
+    (r1 <= r2)%R ->
+    (0 <= r1)%R ->
+    do_overflow m r1 = true ->
+    do_overflow m r2 = true.
+Proof.
+  intros m r1 r2 Hle Hr1 Ho.
+  rewrite do_overflow_iff in Ho. destruct Ho as [H | H].
+  - apply Rle_le in H.
+    rewrite do_overflow_iff. left.
+    apply Raux.Rle_bool_true.
+    eapply Generic_fmt.round_le in Hle.
+    + eapply Rle_trans; [apply H | apply Hle].
+    + now apply fexp_correct.
+    + intuition.
+  - apply Rle_le in H.
+    assert (-fmax < 0)%R.
+    { assert (fmax > 0)%R by apply fmax_gt_0. lra. }
+    pose proof H0.
+    apply Rlt_le in H1.
+    eapply Generic_fmt.round_le in Hr1.
+    + erewrite Generic_fmt.round_0 in Hr1.
+      assert (0 < 0)%R.
+      eapply Rle_lt_trans.
+      apply Hr1.
+      eapply Rle_lt_trans.
+      apply H.
+      apply H0.
+      lra.
+      intuition.
+    + now apply fexp_correct.
+    + intuition.
+Qed.
+
+Lemma sign_false_0 :
+  forall r, sign r = false -> (0 <= r)%R.
+Proof.
+  intros.
+  unfold sign in H.
+  now destruct (Raux.Rlt_bool_spec r 0).
+Qed.
+
+Theorem round_le:
+  forall (m : mode) (r1 r2 : Rx), leb r1 r2 = true -> leb (round m r1) (round m r2) = true.
+Proof.
+  intros m [r1 | s1 ] [r2 | s2] H.
+  - simpl in H. simpl round.
+    destruct (do_overflow m r1) eqn:Ho1;
+    destruct (overflow_to_inf m (sign r1)) eqn:Hi1;
+    destruct (do_overflow m r2) eqn:Ho2;
+    destruct (overflow_to_inf m (sign r2)) eqn:Hi2.
+    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; auto.
+      now rewrite (sign_le _ _ Hs1 Hs2) in H.
+    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
+      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
+      * now destruct m.
+    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
+      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
+      * apply Rle_le in H.
+        now rewrite (overflow_le m H (sign_false_0 r1 Hs1) Ho1) in Ho2.
+    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
+      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
+      * apply Rle_le in H.
+        now rewrite (overflow_le m H (sign_false_0 r1 Hs1) Ho1) in Ho2.
+    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
+      * now destruct m.
+      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
+    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
+      * unfold Raux.Rle_bool.
+        destruct Raux.Rcompare eqn:E; try easy.
+        apply Raux.Rcompare_Gt_inv in E; lra.
+      * unfold Raux.Rle_bool.
+        destruct Raux.Rcompare eqn:E; try easy.
+        apply Raux.Rcompare_Gt_inv in E.
+        assert (fmax > 0)%R. {
+          unfold fmax, Zaux.radix2;
+          red in Hemax, Hprec.
+          assert (emax > 0)%Z by lia.
+          apply Raux.bpow_gt_0; auto.
+        }
+        lra.
+      * now rewrite (sign_le _ _ Hs1 Hs2) in H.
+      * unfold Raux.Rle_bool.
+        destruct Raux.Rcompare eqn:E; try easy.
+        apply Raux.Rcompare_Gt_inv in E; lra.
+    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
+      * apply Raux.Rle_bool_true.
+      * apply Raux.Rle_bool_true; admit.
+      * apply Raux.Rle_bool_true; admit.
+      * apply Raux.Rle_bool_true; admit.
+    + destruct (sign r1) eqn:Hs1, (sign r2) eqn:Hs2; simpl; auto.
+      * destruct (do_overflow_iff _ _ Ho1).
+        ** apply Raux.Rle_bool_true.
+          apply Rle_le in H.
+          apply Rle_le in H0.
+
+Admitted.
+
+
+Lemma round_inf :
+  forall m b, round m (Inf b) = Inf b.
+Proof. reflexivity. Qed.
+
+Lemma round_real :
+  forall m r,
+    round m (Real r) = Real (Generic_fmt.round Zaux.radix2 (SpecFloat.fexp prec emax) (round_mode m) r).
+Proof. reflexivity. Qed.
+
+
+
 Example leb_infp_true :
   forall x, leb x (Inf false) = true.
 Proof. now induction x as [ | [ ] ]. Qed.