Module FloatIntervalsForward


Require Import Coqlib Utf8 Util FastArith.
Require Import AdomLib.
Require Import ZIntervals.
Require Import Integers.
Require Import FloatLib.
Require Import FloatIntervals.

Transparent Float.neg.

Definition forward_fabs (x:fitv+⊤) : fitv+⊤ :=
  match x with
  | Just (FITV mx Mx) =>
    match Bsign mx, Bsign Mx with
    | true, true => Just (FITV (Float.neg Mx) (Float.neg mx))
    | true, false =>
      Just (FITV (B754_zero false)
                (if Fleb Mx (Float.neg mx) then (Float.neg mx) else Mx))
    | false, false => x
    | false, true => All
    end
  | All => All
  end.

Lemma forward_fabs_correct:
  ∀ x x_ab, x ∈ γ x_ab -> (Float.abs x) ∈ γ (forward_fabs x_ab).
Proof.
  intros x [|[mx Mx]] []. easy. simpl.
  assert (forall m e e0,
             Float.abs (B754_finite true m e e0) = Float.neg (B754_finite true m e e0)) by easy.
  destruct mx as [[]|[]| |[]], x as [[]|[]| |[]], Mx as [[]|[]| |[]];
    try discriminate; split;
    try match goal with |- context [if ?b then _ else _] => destruct b eqn:? end;
    rewrite ?H, ?fneg_decr; try easy.
  eapply Fleb_trans.
  rewrite fneg_decr. apply H0.
  edestruct Fleb_total. 3:apply H2. easy. easy. congruence.
  eapply Fleb_trans; eauto.
Qed.

Definition forward_fadd (x y:fitv+⊤) : fitv+⊤+⊥ :=
  match x, y with
  | Just (FITV mx Mx), Just (FITV my My) =>
    if Fleb mx (B754_infinity true) && Fleb (B754_infinity false) My then
      NotBot All
    else if Fleb my (B754_infinity true) && Fleb (B754_infinity false) Mx then
           NotBot All
         else
           NotBot (Just (FITV (Float.add mx my) (Float.add Mx My)))
  | All, _ | _, All => NotBot All
  end.

Lemma fadd_is_nan:
  forall a b pl,
    is_nan a = false -> is_nan b = false ->
    (forall s, a = B754_infinity s -> b = B754_infinity (negb s) -> False) ->
    is_nan (Bplus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b) = false.
Proof.
  intros.
  destruct a as [[]| | |], b as [[]| | |]; try discriminate; try reflexivity.
  specialize (H1 _ eq_refl). destruct b, b0; now intuition.
  apply binary_normalize_is_nan.
Qed.

Lemma fadd_Fleb_compat:
  forall pl a b c,
    is_nan a = false ->
    (forall s, a = B754_infinity s ->
       b <> B754_infinity (negb s) /\ c <> B754_infinity (negb s)) ->
    Fleb b c = true ->
    Fleb (Bplus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b)
         (Bplus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a c) = true.
Proof.
  intros.
  assert (is_nan (Bplus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b) = false).
  { apply fadd_is_nan; eauto 2. intros. specialize (H0 s). intuition. }
  assert (is_nan (Bplus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a c) = false).
  { apply fadd_is_nan; eauto 2. intros. specialize (H0 s). intuition. }
  destruct (is_finite a) eqn:FINa.
  destruct (is_finite b) eqn:FINb.
  destruct (is_finite c) eqn:FINc.
  - pose proof H1. rewrite Fleb_Rle in H1 by auto. Rle_bool_case H1. 2:discriminate.
    use_float_specs.
    assert (round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (a + b) <=
            round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (a + c)).
    { apply round_le; auto. Psatz.lra. }
    repeat match goal with
    | A : ?X -> _, B:?X |- _ => specialize (A B)
    | H : context [Rlt_bool ?a ?b] |- _ =>
       Rlt_bool_case H;
       [destruct H as [? [? ?]]|
       destruct H as [H ?];
         unfold binary_overflow in H; simpl in H;
         apply B2FF_inj with (y:=@B754_infinity 53 _ _) in H]
    end.
    + rewrite Fleb_Rle by auto. rewrite H6, H7. auto using Rle_bool_true.
    + rewrite H6. replace (Bsign a) with false.
      match goal with |- Fleb ?f _ = true => destruct f as [| | |[]] end; try discriminate; reflexivity.
      assert (0 < round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (a + c)).
      { unfold Rabs in H9, H12. destruct Rcase_abs, Rcase_abs; Psatz.lra. }
      destruct a, c; try discriminate.
      * rewrite Rplus_0_l, round_0 in H14 by eauto. Psatz.lra.
      * destruct b1; simpl in H13 |- *. 2:congruence. subst b0.
        assert (forall x y, ~ x+y <= 0 -> x <= 0 -> y <= 0 -> False)
          by (intros ? ? A ? ?; apply A; Psatz.lra).
        edestruct H13; try apply F2R_le_0_compat.
        intro. contradict H14. erewrite <- round_0 by eauto.
        apply RIneq.Rle_not_lt, round_le; eauto.
        compute; discriminate. compute; discriminate.
    + rewrite H7. replace (Bsign a) with true.
      match goal with |- Fleb _ ?f = true => destruct f end; try discriminate; reflexivity.
      assert (round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (a + b) < 0).
      { unfold Rabs in H9, H11. destruct Rcase_abs, Rcase_abs; Psatz.lra. }
      destruct a, b; try discriminate.
      * rewrite Rplus_0_l, round_0 in H14 by eauto. Psatz.lra.
      * destruct b; simpl in H10 |- *. congruence. subst b0.
        assert (forall x y, ~ 0 <= x+y -> 0 <= x -> 0 <= y -> False)
          by (intros ? ? A ? ?; apply A; Psatz.lra).
        edestruct H10; try apply F2R_ge_0_compat.
        intro. contradict H14. erewrite <- round_0 by eauto.
        apply RIneq.Rle_not_lt, round_le; eauto.
        compute; discriminate. compute; discriminate.
    + rewrite H6, H7, H12. destruct c as [[]| | |[]]; try discriminate; reflexivity.
  - assert (is_nan c = false) by eauto.
    destruct c as [[]|[]| |[]]; try discriminate.
    destruct b as [| | |[]]; discriminate.
    destruct a; try discriminate;
    match goal with |- Fleb ?f _ = true => destruct f as [|[]| |[]] end;
      try discriminate; reflexivity.
  - assert (is_nan b = false) by eauto.
    destruct b as [[]|[]| |[]]; try discriminate.
    destruct a; try discriminate;
    match goal with |- Fleb _ ?f = true => destruct f as [|[]| |[]] end;
      try discriminate; reflexivity.
    destruct c as [|[]| |]; try discriminate. auto.
  - destruct a as [|[]| |], b as [|[]| |], c as [|[]| |]; try reflexivity; discriminate.
Qed.

Lemma forward_fadd_correct:
  ∀ x x_ab y y_ab, x ∈ γ x_ab -> y ∈ γ y_ab ->
    (Float.add x y) ∈ γ (forward_fadd x_ab y_ab).
Proof.
  Transparent Float.add.
  intros.
  destruct x_ab as [|[mx Mx]], y_ab as [|[my My]]; try easy.
  simpl in *. destruct H, H0.
  assert (Fleb mx Mx = true) by eauto using Fleb_trans.
  assert (Fleb my My = true) by eauto using Fleb_trans.
  destruct (Fleb mx (B754_infinity true) && Fleb (B754_infinity false) My) eqn:?. easy.
  destruct (Fleb my (B754_infinity true) && Fleb (B754_infinity false) Mx) eqn:?. easy.
  rewrite andb_false_iff in *.
  split; eapply Fleb_trans.
   - apply fadd_Fleb_compat with (c:=y); eauto.
     intuition; subst; destruct s; simpl in *; try congruence; discriminate.
   - rewrite !fadd_commut with (pl:=Float.binop_pl).
     apply fadd_Fleb_compat; eauto.
     intuition; subst; destruct s; simpl in *; try congruence; discriminate.
   - apply fadd_Fleb_compat with (c:=My); eauto.
     intuition; subst; destruct s; simpl in *; try congruence; discriminate.
   - rewrite !fadd_commut with (pl:=Float.binop_pl).
     apply fadd_Fleb_compat; eauto.
     intuition; subst; destruct s; simpl in *; try congruence; discriminate.
Qed.

Definition forward_fsub (x y:fitv+⊤) : fitv+⊤+⊥ :=
  forward_fadd x (forward_fneg y).

Lemma forward_fsub_correct:
  ∀ x x_ab y y_ab, x ∈ γ x_ab -> y ∈ γ y_ab ->
    (Float.sub x y) ∈ γ (forward_fsub x_ab y_ab).
Proof.
  intros.
  Transparent Float.sub.
  unfold Float.sub.
  apply forward_fadd_correct. auto.
  pose proof (forward_fneg_correct _ _ H0).
  destruct y; try apply H1. destruct forward_fneg; apply H1.
Qed.

Definition mult_nan_criterion (a b:float) : bool :=
  match a, b with
    | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => false
    | B754_nan _ _, _ | _, B754_nan _ _ => false
    | _, _ => true
  end.

Lemma fmult_is_nan:
  forall a b pl,
    mult_nan_criterion a b = true ->
    is_nan (Bmult 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b) = false.
Proof.
  intros.
  use_float_specs.
  destruct a as [| | |], b as [| | |]; try discriminate; try reflexivity.
  destruct Rlt_bool.
  - destruct H0 as [? []]. destruct Bmult; try discriminate; reflexivity.
  - destruct Bmult as [| |? []|]; try discriminate; reflexivity.
Qed.

Lemma fmult_Fleb_compat:
  forall pl a b c,
    mult_nan_criterion a b = true ->
    mult_nan_criterion a c = true ->
    Bsign a = false ->
    Fleb b c = true ->
    Fleb (Bmult 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b)
         (Bmult 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a c) = true.
Proof.
  intros.
  assert (is_nan (Bmult 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b) = false) by (apply fmult_is_nan; easy).
  assert (is_nan (Bmult 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a c) = false) by (apply fmult_is_nan; easy).
  destruct (is_finite a) eqn:FINa.
  destruct (is_finite b) eqn:FINb.
  destruct (is_finite c) eqn:FINc.
  - rewrite Fleb_Rle in H2 by auto. Rle_bool_case H2. 2:discriminate.
    use_float_specs.
    assert (round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (a * b) <=
            round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (a * c)).
    { apply round_le, Rmult_le_compat_l; auto.
      destruct a; try discriminate; simpl in H1; subst; simpl.
      Psatz.lra. apply F2R_ge_0_compat. compute; discriminate. }
    repeat match goal with H : context [Rlt_bool ?a ?b] |- _ =>
      Rlt_bool_case H;
      [rewrite FINa, ?FINb, ?FINc in H; destruct H as [H []]|
       unfold binary_overflow in H; simpl in H;
       apply B2FF_inj with (y:=@B754_infinity 53 _ _) in H]
    end.
    + rewrite Fleb_Rle, H6, H7 by auto. auto using Rle_bool_true.
    + rewrite H6, H1. replace (Bsign c) with false.
      match goal with |- Fleb ?f _ = true => destruct f as [| | |[]] end; try discriminate; reflexivity.
      assert (0 < round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (a * c)).
      { unfold Rabs in H9, H12. destruct Rcase_abs, Rcase_abs; Psatz.lra. }
      destruct a, c; try discriminate. simpl in H1; subst b0.
      destruct b1; simpl; try reflexivity.
      apply RIneq.Rle_not_lt in H13. easy.
      erewrite <- round_0 by eauto.
      apply round_le; auto.
      erewrite <- Rmult_0_r.
      apply Rmult_le_compat_l.
        apply F2R_ge_0_compat; compute; discriminate.
        apply F2R_le_0_compat; compute; discriminate.
    + rewrite H7, H1. replace (Bsign b) with true.
      match goal with |- Fleb _ ?f = true => destruct f end; try discriminate; reflexivity.
      assert (round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (a * b) < 0).
      { unfold Rabs in H9, H10. destruct Rcase_abs, Rcase_abs; Psatz.lra. }
      destruct a, b; try discriminate. simpl in H1; subst b0.
      destruct b; simpl; try reflexivity.
      apply RIneq.Rle_not_lt in H13. easy.
      erewrite <- round_0 by eauto.
      apply round_le, Rmult_le_pos; eauto;
      apply F2R_ge_0_compat; compute; discriminate.
    + assert (~ bpow radix2 1024 <= 0).
      { rewrite <- Z2R_Zpower by omega. intro.
        apply le_Z2R with (n:=Z0) in H11. apply H11. reflexivity. }
      rewrite H6, H7, H1. destruct b as [[]| | |[]], c as [[]| | |[]]; try discriminate; try reflexivity;
      try (rewrite Rmult_0_r, round_0, Rabs_R0 in * by auto; easy). simpl.
      eapply Rle_trans in H5.
      eapply RIneq.Rle_not_lt in H5.
      destruct H5. apply F2R_lt_0_compat. reflexivity.
      apply F2R_ge_0_compat. compute; discriminate.
  - destruct a, c; try discriminate.
    simpl in H1. subst.
    destruct b1. destruct b as [| | |[]]; discriminate.
    match goal with |- Fleb ?f _ = true => destruct f as [|[]| |[]] end; try reflexivity. discriminate.
  - destruct a, b; try discriminate.
    simpl in H1. subst.
    destruct b.
    match goal with |- Fleb _ ?f = true => destruct f as [|[]| |[]] end; try reflexivity. discriminate.
    destruct c as [|[]| |]; try discriminate; reflexivity.
  - destruct a; try discriminate.
    simpl in H1. subst.
    destruct b as [|[]| |[]], c as [|[]| |[]]; try discriminate; reflexivity.
Qed.

Lemma fmult_neg:
  forall pl a b,
    mult_nan_criterion a b = true ->
    Bmult 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE (Float.neg a) b =
      Float.neg (Bmult 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b).
Proof.
  intros.
  assert (Bsign_Bopp:forall f:float, Bsign (Bopp _ _ Float.neg_pl f) = negb (Bsign f))
    by (destruct f; easy).
  unfold Float.neg.
  destruct (is_finite a) eqn:?. destruct (is_finite b) eqn:?.
  - use_float_specs.
    unfold round_mode in H0.
    rewrite B2R_Bopp, Ropp_mult_distr_l_reverse, round_NE_opp, Rabs_Ropp, is_finite_Bopp in H0.
    fold (round_mode mode_NE) in H0.
    destruct Rlt_bool.
    + destruct H0 as [? []], H1 as [? []].
      apply B2R_Bsign_inj.
      * rewrite H2, Heqb0, Heqb1. easy.
      * rewrite is_finite_Bopp, H4, Heqb0, Heqb1. easy.
      * rewrite B2R_Bopp, H1, H0. easy.
      * rewrite Bsign_Bopp, H5, H3, negb_xorb_l, Bsign_Bopp. easy.
        clear - H2 Heqb0 Heqb1. destruct Bmult; try reflexivity.
        rewrite Heqb0, Heqb1 in H2; discriminate.
        apply fmult_is_nan. auto.
    + apply B2FF_inj. rewrite H0.
      pose proof (fmult_is_nan _ _ pl H).
      match goal with |- _ = B2FF (Bopp _ _ _ ?f) => destruct f end; try discriminate.
      inv H1. simpl.
      destruct a as [[]|[]|[]|[]], b as [[]|[]|[]|[]]; reflexivity.
  - destruct a, b; try discriminate. simpl. rewrite negb_xorb_l. reflexivity.
  - destruct a, b; try discriminate; simpl; rewrite negb_xorb_l; reflexivity.
Qed.

Lemma fmult_Fleb_compat_neg:
  forall pl a b c,
    mult_nan_criterion a b = true ->
    mult_nan_criterion a c = true ->
    Bsign a = true ->
    Fleb b c = true ->
    Fleb (Bmult 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a c)
         (Bmult 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b) = true.
Proof.
  intros.
  rewrite <- fneg_decr, <- !fmult_neg by easy.
  apply fmult_Fleb_compat; auto.
  destruct a; easy.
  destruct a; easy.
  destruct a; simpl in H1; subst; reflexivity.
Qed.

Lemma fmult_comm:
  forall a b pl,
    Bmult 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b =
    Bmult 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) (fun a b => pl b a) mode_NE b a.
Proof.
  intros.
  destruct a as [[]|[]| |], b as [[]|[]| |]; try reflexivity.
  apply B2FF_inj. simpl. rewrite !B2FF_FF2B.
  rewrite Pmult_comm, Zplus_comm, xorb_comm. reflexivity.
Qed.

Definition minmax4 (a b c d:float) : float*float :=
  match Fleb a b, Fleb c d with
    | true, true => (if Fleb a c then a else c, if Fleb b d then d else b)
    | true, false => (if Fleb a d then a else d, if Fleb b c then c else b)
    | false, true => (if Fleb b c then b else c, if Fleb a d then d else a)
    | false, false => (if Fleb b d then b else d, if Fleb a c then c else a)
  end.

Lemma minmax4_correct :
  forall a b c d,
    is_nan a = false -> is_nan b = false ->
    is_nan c = false -> is_nan d = false ->
    let '(m, M) := minmax4 a b c d in
    Fleb m a = true /\ Fleb m b = true /\ Fleb m c = true /\ Fleb m d = true /\
    Fleb a M = true /\ Fleb b M = true /\ Fleb c M = true /\ Fleb d M = true.
Proof.
  intros.
  unfold minmax4.
  repeat match goal with |- context [if Fleb ?x ?y then _ else _] =>
    destruct (Fleb x y) eqn:?;
      [|destruct (Fleb_total _ _ x y); [easy|easy|congruence|]]
  end; eauto 12 using Fleb_trans.
Qed.

Definition forward_fmult (x y:fitv+⊤) : fitv+⊤+⊥ :=
  match x, y with
  | Just (FITV mx Mx), Just (FITV my My) =>
    if ((is_finite mx && is_finite Mx) ||
        negb (Fleb my (B754_zero false) && Fleb (B754_zero false) My))
         &&
       ((is_finite my && is_finite My) ||
        negb (Fleb mx (B754_zero false) && Fleb (B754_zero false) Mx))
    then
      let '(m, M) := minmax4 (Float.mul mx my) (Float.mul mx My)
                             (Float.mul Mx my) (Float.mul Mx My)
      in NotBot (Just (FITV m M))
    else NotBot All
  | All, _ | _, All => NotBot All
  end.

Local Remove Hints trans_eq_bool.

Theorem forward_fmult_correct:
  ∀ x x_ab y y_ab, x ∈ γ x_ab -> y ∈ γ y_ab ->
    (Float.mul x y) ∈ γ (forward_fmult x_ab y_ab).
Proof.
  Transparent Float.mul.
  intros. unfold forward_fmult.
  destruct x_ab as [|[mx Mx]], y_ab as [|[my My]]; try easy.
  match goal with |- context [if ?c then _ else _] => destruct c eqn:? end; try easy.
  repeat rewrite ?orb_true_iff, ?andb_true_iff, ?orb_false_iff, ?andb_false_iff, ?negb_true_iff in Heqb.
  destruct H, H0, Heqb.
  assert (Fleb mx Mx = true) by eauto using Fleb_trans.
  assert (Fleb my My = true) by eauto using Fleb_trans.
  assert (forall x' y', Fleb mx x' = true -> Fleb x' Mx = true ->
                        Fleb my y' = true -> Fleb y' My = true ->
                        mult_nan_criterion x' y' = true).
  { intros. destruct x', y'; try reflexivity; exfalso; try discriminate.
    destruct H4 as [[]|[]].
    destruct b0, my as [| | |[]], My as [| | |[]]; discriminate.
    destruct mx as [|[]| |[]]; discriminate.
    destruct Mx as [|[]| |[]]; discriminate.
    destruct H3 as [[]|[]].
    destruct b, mx as [| | |[]], Mx as [| | |[]]; discriminate.
    destruct my as [|[]| |[]]; discriminate.
    destruct My as [|[]| |[]]; discriminate. }
  assert (forall x' y', mult_nan_criterion y' x' = true ->
                        mult_nan_criterion x' y' = true).
  { destruct x', y'; try discriminate; reflexivity. }
  pose proof (minmax4_correct (Float.mul mx my) (Float.mul mx My)
                               (Float.mul Mx my) (Float.mul Mx My)).
  destruct minmax4.
  destruct H9 as [?[?[?[?[?[?[]]]]]]]; try apply fmult_is_nan; eauto 6.
  split.
  - destruct (Bsign x) eqn:?.
    + destruct (Bsign My) eqn:?.
      * eapply Fleb_trans. apply H12.
        eapply Fleb_trans. unfold Float.mul. rewrite fmult_comm.
        apply fmult_Fleb_compat_neg with (b:=x); eauto 7.
        rewrite fmult_comm.
        apply fmult_Fleb_compat_neg; eauto 7.
      * eapply Fleb_trans. apply H10.
        eapply Fleb_trans. unfold Float.mul. rewrite fmult_comm.
        apply fmult_Fleb_compat with (c:=x); eauto 7.
        rewrite fmult_comm.
        apply fmult_Fleb_compat_neg; eauto 7.
    + destruct (Bsign my) eqn:?.
      * eapply Fleb_trans. apply H11.
        eapply Fleb_trans. unfold Float.mul. rewrite fmult_comm.
        apply fmult_Fleb_compat_neg with (b:=x); eauto 7.
        rewrite fmult_comm.
        apply fmult_Fleb_compat; eauto 7.
      * eapply Fleb_trans. apply H9.
        eapply Fleb_trans. unfold Float.mul. rewrite fmult_comm.
        apply fmult_Fleb_compat with (c:=x); eauto 7.
        rewrite fmult_comm.
        apply fmult_Fleb_compat; eauto 7.
  - destruct (Bsign x) eqn:?.
    + eapply Fleb_trans.
      apply fmult_Fleb_compat_neg with (b:=my); eauto 7.
      destruct (Bsign my) eqn:?.
      * eapply Fleb_trans. rewrite fmult_comm.
        apply fmult_Fleb_compat_neg with (b:=mx); eauto 7.
        rewrite <- fmult_comm. auto.
      * eapply Fleb_trans. rewrite fmult_comm.
        apply fmult_Fleb_compat with (c:=Mx); eauto 7.
        rewrite <- fmult_comm. auto.
    + eapply Fleb_trans.
      apply fmult_Fleb_compat with (c:=My); eauto 7.
      destruct (Bsign My) eqn:?.
      * eapply Fleb_trans. rewrite fmult_comm.
        apply fmult_Fleb_compat_neg with (b:=mx); eauto 7.
        rewrite <- fmult_comm. auto.
      * eapply Fleb_trans. rewrite fmult_comm.
        apply fmult_Fleb_compat with (c:=Mx); eauto 7.
        rewrite <- fmult_comm. auto.
Qed.

Definition div_nan_criterion (a b:float) : bool :=
  match a, b with
  | B754_infinity _, B754_infinity _ | B754_zero _, B754_zero _ => false
  | B754_nan _ _, _ | _, B754_nan _ _ => false
  | _, _ => true
  end.

Lemma fdiv_is_nan:
  forall a b pl,
    div_nan_criterion a b = true ->
    is_nan (Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b) = false.
Proof.
  intros.
  use_float_specs.
  destruct a as [| | |], b as [| | |]; try discriminate; try reflexivity.
  assert ((B754_finite b m0 e1 e2:R) ≠ 0).
  { intro. apply B2R_Bsign_inj with (y:=B754_zero b) in H1.
    discriminate. auto. auto. auto. }
  specialize (H0 H1). clear H1.
  destruct Rlt_bool.
  - destruct H0 as [? []].
    destruct Bdiv; try discriminate; reflexivity.
  - destruct Bdiv as [| |? []|]; try discriminate; reflexivity.
Qed.

Lemma fdiv_Fleb_compat_r:
  forall pl a b c,
    div_nan_criterion a b = true ->
    div_nan_criterion a c = true ->
    Bsign a = false ->
    Fleb b c = true ->
    Fleb b (B754_zero false) = false ->
    Fleb (Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a c)
         (Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b) = true.
Proof.
  intros pl a b c CRITab CRITac asign Hbc Hb.
  assert (is_nan (Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b) = false) by (apply fdiv_is_nan; easy).
  assert (is_nan (Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a c) = false) by (apply fdiv_is_nan; easy).
  use_float_specs.
  assert (bsign:Bsign b = false).
  { destruct b as [|[]| |[]]; try discriminate; reflexivity. }
  destruct (is_finite a) eqn:FINa.
  destruct (is_finite b) eqn:FINb.
  destruct (is_finite c) eqn:FINc.
  - rewrite Fleb_Rle in Hbc by auto. Rle_bool_case Hbc. 2:discriminate. clear Hbc. rename H3 into Hbc.
    rewrite Fleb_Rle in Hb by auto. Rle_bool_case Hb. discriminate. clear Hb. rename H3 into Hb. simpl in Hb.
    assert (bneq0:(b:R) <> 0) by (apply Rlt_dichotomy_converse; auto). specialize (H2 bneq0).
    assert (cneq0:(c:R) <> 0) by (apply Rlt_dichotomy_converse; right; Psatz.lra). specialize (H1 cneq0).
    assert (age0:0 <= a).
    { destruct a; try discriminate; simpl in asign; subst; simpl.
      auto with real. apply F2R_ge_0_compat, Pos2Z.is_nonneg. }
    assert (round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (a / c) <=
            round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (a / b)).
    { apply round_le, Rmult_le_compat_l, Rinv_le; auto. }
    repeat match goal with H : context [Rlt_bool ?a ?b] |- _ =>
      Rlt_bool_case H;
      [destruct H as [H []]|
       unfold binary_overflow in H; simpl in H;
       apply B2FF_inj with (y:=@B754_infinity 53 _ _) in H]
    end.
    + rewrite Fleb_Rle, H1, H2 by auto. auto using Rle_bool_true.
    + destruct (Rlt_not_le _ _ (Rlt_le_trans _ _ _ H4 H7)).
      rewrite !Rabs_pos_eq. auto.
      erewrite <- round_0 by eauto.
      apply round_le, Rmult_le_pos, Rlt_le, Rinv_0_lt_compat; eauto.
      erewrite <- round_0 by eauto.
      apply round_le, Rmult_le_pos, Rlt_le, Rinv_0_lt_compat; eauto.
      Psatz.lra.
    + rewrite H2, asign, bsign.
      match goal with |- Fleb ?f _ = true => destruct f as [| | |[]] end; try reflexivity; discriminate.
    + rewrite H1, H2, asign, bsign. destruct (Bsign c); easy.
  - destruct b; try discriminate.
    destruct a, c; try discriminate. reflexivity.
    simpl in asign, bsign; subst.
    assert ((B754_finite false m e e0:R) ≠ 0).
    { apply Rgt_not_eq, F2R_gt_0_compat. reflexivity. }
    specialize (H2 H3).
    match goal with |- Fleb _ ?f = true => destruct f as [|[]| |[]] end; try discriminate; try reflexivity.
    destruct Rlt_bool in H2. now intuition. discriminate.
    destruct Rlt_bool in H2. now intuition. discriminate.
  - destruct a, b; try discriminate. destruct c; try reflexivity; discriminate.
    simpl in asign, bsign; subst. destruct c; try reflexivity; discriminate.
  - destruct a; try discriminate. simpl in asign. subst.
    destruct b as [|[]| |[]], c as [|[]| |[]]; try discriminate; reflexivity.
Qed.

Lemma fdiv_Fleb_compat_l:
  forall pl a b c,
    div_nan_criterion b a = true ->
    div_nan_criterion c a = true ->
    Fleb a (B754_zero false) = false ->
    Fleb b c = true ->
    Fleb (Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE b a)
         (Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE c a) = true.
Proof.
  intros pl a b c CRITab CRITac Ha Hbc.
  assert (asign:Bsign a = false) by (destruct a as [[]|[]|[]|[]], b; try discriminate; reflexivity).
  assert (is_nan (Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE b a) = false) by (apply fdiv_is_nan; easy).
  assert (is_nan (Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE c a) = false) by (apply fdiv_is_nan; easy).
  use_float_specs.
  destruct a; try (destruct b; discriminate); simpl in asign; subst.
  - destruct b as [|[]| |[]], c as [|[]| |[]]; try discriminate; reflexivity.
  - assert (aneq0:(B754_finite false m e e0:R) <> 0).
    { apply Rgt_not_eq, F2R_gt_0_compat. reflexivity. }
    specialize (H1 aneq0). specialize (H2 aneq0).
    destruct (is_finite b) eqn:FINb.
    destruct (is_finite c) eqn:FINc.
    + assert (Hbc':=Hbc). rewrite Fleb_Rle in Hbc by easy.
      Rle_bool_case Hbc. 2:discriminate. clear Hbc. rename H3 into Hbc.
      assert (round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (b / B754_finite false m e e0) <=
              round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (c / B754_finite false m e e0)).
      { apply round_le, Rmult_le_compat_r; auto.
        apply Rlt_le, Rinv_0_lt_compat, F2R_gt_0_compat. reflexivity. }
      repeat match goal with H : context [Rlt_bool ?a ?b] |- _ =>
        Rlt_bool_case H;
          [destruct H as [H []]|
           unfold binary_overflow in H; simpl in H;
           apply B2FF_inj with (y:=@B754_infinity 53 _ _) in H]
      end.
      * rewrite Fleb_Rle, H1, H2 by auto. auto using Rle_bool_true.
      * rewrite H1. replace (Bsign c) with false.
        match goal with |- Fleb ?f _ = true => destruct f as [| | |[]] end; try reflexivity; discriminate.
        destruct c as [| | |[]]; try reflexivity; try discriminate.
        destruct b as [| | |[]]; try reflexivity; try discriminate.
        destruct (Rlt_not_le _ _ (Rlt_le_trans _ _ _ H4 H7)).
        rewrite !Rabs_left1. Psatz.lra.
        erewrite <- round_0 by eauto.
        apply round_le; auto.
        apply Ropp_le_cancel. unfold Rdiv.
        rewrite Ropp_0, <- Ropp_mult_distr_l_reverse.
        apply Rmult_le_pos, Rlt_le, Rinv_0_lt_compat. apply Ropp_0_ge_le_contravar, Rle_ge.
        apply F2R_le_0_compat. compute. discriminate.
        apply F2R_gt_0_compat. reflexivity.
        erewrite <- round_0 by eauto.
        apply round_le; auto.
        apply Ropp_le_cancel. unfold Rdiv.
        rewrite Ropp_0, <- Ropp_mult_distr_l_reverse.
        apply Rmult_le_pos, Rlt_le, Rinv_0_lt_compat. apply Ropp_0_ge_le_contravar, Rle_ge.
        apply F2R_le_0_compat. compute. discriminate.
        apply F2R_gt_0_compat. reflexivity.
      * rewrite H2. replace (Bsign b) with true.
        match goal with |- Fleb _ ?f = true => destruct f as [| | |] end; try reflexivity; discriminate.
        destruct b as [| | |[]]; try reflexivity; try discriminate.
        destruct c as [| | |[]]; try reflexivity; try discriminate.
        destruct (Rlt_not_le _ _ (Rlt_le_trans _ _ _ H5 H4)).
        rewrite !Rabs_pos_eq. auto.
        erewrite <- round_0 by eauto.
        apply round_le, Rmult_le_pos, Rlt_le, Rinv_0_lt_compat; eauto.
        apply F2R_ge_0_compat. compute. discriminate.
        apply F2R_gt_0_compat. reflexivity.
        erewrite <- round_0 by eauto.
        apply round_le, Rmult_le_pos, Rlt_le, Rinv_0_lt_compat; eauto.
        apply F2R_ge_0_compat. compute. discriminate.
        apply F2R_gt_0_compat. reflexivity.
      * rewrite H1, H2.
        destruct b as [| | |[]], c as [| | |[]]; try discriminate; reflexivity.
    + destruct c as [|[]| |]; try discriminate.
      destruct b as [| | |[]]; discriminate.
      match goal with |- Fleb ?f _ = true => destruct f as [|[]| |[]] end; try discriminate; reflexivity.
    + destruct b as [|[]| |], c as [|[]| |]; try discriminate; try reflexivity.
      match goal with |- Fleb _ ?f = true => destruct f as [|[]| |[]] end; try discriminate; reflexivity.
Qed.

Lemma fdiv_neg_r:
  forall pl a b,
    div_nan_criterion a b = true ->
    Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a (Float.neg b) =
      Float.neg (Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b).
Proof.
  intros.
  assert (Bsign_Bopp:forall f:float, Bsign (Bopp _ _ Float.neg_pl f) = negb (Bsign f))
    by (destruct f; easy).
  destruct (is_finite a) eqn:?.
  destruct b; try (destruct a; discriminate).
  - destruct a; try discriminate. destruct b, b0; reflexivity.
  - destruct a; try discriminate; destruct b, b0; reflexivity.
  - simpl.
    unfold Float.neg in *.
    use_float_specs. unfold Rdiv in *.
    assert (forall b', (B754_finite b' m e e0:R) <> 0).
    { intro. intro. apply F2R_eq_0_reg in H2.
      destruct b'; discriminate. }
    specialize (H0 (H2 _)).
    unfold round_mode in H.
    fold (Bopp _ _ Float.neg_pl (B754_finite b m e e0)) in H0.
    rewrite B2R_Bopp, <- Ropp_inv_permute, Ropp_mult_distr_r_reverse, round_NE_opp, Rabs_Ropp in H0 by auto.
    fold (round_mode mode_NE) in H0.
    specialize (H1 (H2 _)).
    simpl Bopp in *.
    destruct Rlt_bool.
    + destruct H0 as [? []], H1 as [? []].
      apply B2R_Bsign_inj.
      * congruence.
      * rewrite is_finite_Bopp. congruence.
      * rewrite B2R_Bopp. congruence.
      * rewrite Bsign_Bopp, H6, H4, negb_xorb_l. destruct b, (Bsign a); easy.
        apply fdiv_is_nan. destruct a; try reflexivity. discriminate.
        apply fdiv_is_nan. easy.
    + apply B2FF_inj. rewrite H0.
      pose proof (fdiv_is_nan _ _ pl H).
      match goal with |- _ = B2FF (Bopp _ _ _ ?f) => destruct f end; try discriminate.
      inv H1.
      destruct b, (Bsign a); easy.
  - destruct a, b; try discriminate; simpl; rewrite negb_xorb_r; reflexivity.
Qed.

Lemma fdiv_neg_l:
  forall pl a b,
    div_nan_criterion a b = true ->
    Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE (Float.neg a) b =
      Float.neg (Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) pl mode_NE a b).
Proof.
  intros.
  assert (Bsign_Bopp:forall f:float, Bsign (Bopp _ _ Float.neg_pl f) = negb (Bsign f))
    by (destruct f; easy).
  destruct (is_finite a) eqn:?.
  destruct b; try (destruct a; discriminate).
  - destruct a; try discriminate. destruct b, b0; reflexivity.
  - destruct a; try discriminate; destruct b, b0; reflexivity.
  - unfold Float.neg in *.
    use_float_specs. unfold Rdiv in *.
    assert ((B754_finite b m e e0:R) <> 0).
    { intro. apply F2R_eq_0_reg in H2.
      destruct b; discriminate. }
    specialize (H0 H2).
    unfold round_mode in H0.
    rewrite B2R_Bopp, Ropp_mult_distr_l_reverse, round_NE_opp, Rabs_Ropp, is_finite_Bopp in H0.
    fold (round_mode mode_NE) in H0.
    specialize (H1 H2).
    destruct Rlt_bool.
    + destruct H0 as [? []], H1 as [? []].
      apply B2R_Bsign_inj.
      * rewrite H3. easy.
      * rewrite is_finite_Bopp. congruence.
      * rewrite B2R_Bopp. congruence.
      * rewrite Bsign_Bopp, H6, H4, negb_xorb_l, Bsign_Bopp. easy.
        apply fdiv_is_nan. destruct a; try reflexivity. discriminate.
        apply fdiv_is_nan. easy.
    + apply B2FF_inj. rewrite H0.
      pose proof (fdiv_is_nan _ _ pl H).
      match goal with |- _ = B2FF (Bopp _ _ _ ?f) => destruct f end; try discriminate.
      inv H1. simpl. rewrite Bsign_Bopp. rewrite negb_xorb_l. reflexivity.
  - destruct a, b; try discriminate; simpl; rewrite negb_xorb_l; reflexivity.
Qed.

Definition forward_fdiv (x y:fitv+⊤) : fitv+⊤+⊥ :=
  match x, y with
  | Just (FITV mx Mx), Just (FITV my My) =>
    if (is_finite mx && is_finite Mx) || (is_finite my && is_finite My) then
      if Fleb my (B754_zero false) then
        if Fleb (B754_zero false) My then
          if (Fleb mx (B754_zero false) && Fleb (B754_zero false) Mx) then
            NotBot All
          else
            NotBot (Just (FITV (B754_infinity true) (B754_infinity false)))
        else NotBot
          (Just (FITV (Float.div Mx (if Bsign Mx then my else My))
                    (Float.div mx (if Bsign mx then My else my))))
      else NotBot
        (Just (FITV (Float.div mx (if Bsign mx then my else My))
                   (Float.div Mx (if Bsign Mx then My else my))))
    else
      NotBot All
  | All, _ | _, All => NotBot All
  end.

Theorem forward_fdiv_correct:
  ∀ x x_ab y y_ab, x ∈ γ x_ab -> y ∈ γ y_ab ->
    (Float.div x y) ∈ γ (forward_fdiv x_ab y_ab).
Proof.
  Transparent Float.div.
  intros. unfold forward_fdiv.
  destruct x_ab as [|[mx Mx]], y_ab as [|[my My]]; try easy.
  destruct H, H0.
  assert (Fleb mx Mx = true) by eauto using Fleb_trans.
  assert (Fleb my My = true) by eauto using Fleb_trans.
  assert (forall f, Bsign f = true -> Bsign (Float.neg f) = false)
    by (destruct f as [[]|[]|[]|[]]; auto).
  assert (forall a b c, Fleb a b = c -> Fleb (Float.neg b) (Float.neg a) = c)
    by (intros; rewrite fneg_decr; auto).
  assert (forall x' y', div_nan_criterion x' y' = true -> div_nan_criterion (Float.neg x') y' = true)
    by (destruct x'; easy).
  assert (forall x' y', div_nan_criterion x' y' = true -> div_nan_criterion x' (Float.neg y') = true)
    by (destruct y'; easy).
  unfold Float.div.
  repeat match goal with |- γ (if ?c then _ else _) _ => destruct c eqn:? end; try easy;
  repeat rewrite ?orb_true_iff, ?andb_true_iff, ?orb_false_iff, ?andb_false_iff, ?negb_true_iff in *.
  - assert (CRIT:div_nan_criterion x y = true).
    assert (is_nan x = false) by eauto;
    assert (is_nan y = false) by eauto;
    destruct x as [|[]| |], y as [|[]| |]; try reflexivity; try discriminate;
    destruct Heqb2, Heqb as [[]|[]];
    try (destruct mx as [|[]| |[]]; discriminate);
    try (destruct Mx as [|[]| |[]]; discriminate);
    try (destruct my as [|[]| |[]]; discriminate);
    try (destruct My as [|[]| |[]]; discriminate).
    apply fdiv_is_nan with (pl:=Float.binop_pl) in CRIT.
    destruct Bdiv as [|[]| |[]]; try discriminate; split; try reflexivity.
  - assert (forall x' y', Fleb mx x' = true -> Fleb x' Mx = true ->
                          Fleb my y' = true -> Fleb y' My = true ->
                          div_nan_criterion x' y' = true).
    { intros. destruct x', y'; try reflexivity; exfalso; try discriminate.
      destruct My as [|[]| |[]]; discriminate.
      destruct Heqb as [[]|[]].
      destruct b, mx as [| | |[]], Mx as [| | |[]]; discriminate.
      destruct b0, my as [| | |[]], My as [| | |[]]; discriminate. }
    assert (Fleb (Float.neg My) (B754_zero false) = false)
      by (destruct My as [|[]| |[]]; try discriminate; reflexivity).
    split.
    + apply Fleb_trans with (f2:=Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_pl mode_NE Mx y).
      * destruct (Bsign Mx) eqn:?; rewrite <- fneg_decr, <- !fdiv_neg_r; eauto 8.
        rewrite <- fneg_decr, <- !fdiv_neg_l; eauto 8.
        apply fdiv_Fleb_compat_r; eauto 8.
        rewrite <- not_true_iff_false in H10 |- *. contradict H10. eauto using Fleb_trans.
        apply fdiv_Fleb_compat_r; eauto 8.
      * rewrite <- fneg_decr, <- !fdiv_neg_r; eauto.
        apply fdiv_Fleb_compat_l; eauto 8.
        rewrite <- not_true_iff_false in H10 |- *. contradict H10. eauto using Fleb_trans.
    + apply Fleb_trans with (f2:=Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_pl mode_NE mx y).
      * rewrite <- fneg_decr, <- !fdiv_neg_r; eauto.
        apply fdiv_Fleb_compat_l; eauto.
        rewrite <- not_true_iff_false in H10 |- *. contradict H10. eauto using Fleb_trans.
      * destruct (Bsign mx) eqn:?; rewrite <- fneg_decr, <- !fdiv_neg_r; eauto 8.
        rewrite <- fneg_decr, <- !fdiv_neg_l; eauto 8.
        apply fdiv_Fleb_compat_r; eauto 8.
        apply fdiv_Fleb_compat_r; eauto 8.
        rewrite <- not_true_iff_false in H10 |- *. contradict H10. eauto using Fleb_trans.
  - assert (forall x' y', Fleb mx x' = true -> Fleb x' Mx = true ->
                          Fleb my y' = true -> Fleb y' My = true ->
                          div_nan_criterion x' y' = true).
    { intros. destruct x', y'; try reflexivity; exfalso; try discriminate.
      destruct my as [|[]| |[]]; discriminate.
      destruct Heqb as [[]|[]].
      destruct b, mx as [| | |[]], Mx as [| | |[]]; discriminate.
      destruct b0, my as [| | |[]], My as [| | |[]]; discriminate. }
    split.
    + apply Fleb_trans with (f2:=Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_pl mode_NE mx y).
      * destruct (Bsign mx) eqn:?.
        rewrite <- fneg_decr, <- !fdiv_neg_l; eauto 8.
        apply fdiv_Fleb_compat_r; eauto 8.
        apply fdiv_Fleb_compat_r; eauto 8.
        rewrite <- not_true_iff_false in Heqb0 |- *. contradict Heqb0. eauto using Fleb_trans.
      * apply fdiv_Fleb_compat_l; eauto 8.
        rewrite <- not_true_iff_false in Heqb0 |- *. contradict Heqb0. eauto using Fleb_trans.
    + apply Fleb_trans with (f2:=Bdiv 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_pl mode_NE Mx y).
      * apply fdiv_Fleb_compat_l; eauto.
        rewrite <- not_true_iff_false in Heqb0 |- *. contradict Heqb0. eauto using Fleb_trans.
      * destruct (Bsign Mx) eqn:?.
        rewrite <- fneg_decr, <- !fdiv_neg_l; eauto 8.
        apply fdiv_Fleb_compat_r; eauto 8.
        rewrite <- not_true_iff_false in Heqb0 |- *. contradict Heqb0. eauto using Fleb_trans.
        apply fdiv_Fleb_compat_r; eauto 8.
Qed.

Transparent Float.to_single Float.of_single.

Lemma Bconv_incr:
  ∀ prec emax prec' emax' Hprec' Hmax' pl f1 f2,
    Fleb f1 f2 = true ->
    Fleb (Bconv prec emax prec' emax' Hprec' Hmax' pl mode_NE f1)
         (Bconv prec emax prec' emax' Hprec' Hmax' pl mode_NE f2) = true.
Proof.
  intros.
  assert (is_nan f1 = false) by eauto.
  assert (is_nan f2 = false) by eauto.
  use_float_specs.
  destruct (is_finite f1) eqn:FIN1;
  [specialize (H2 eq_refl)|clear H2; destruct f1 as [|[]| |]; try discriminate];
  (destruct (is_finite f2) eqn:FIN2;
  [specialize (H3 eq_refl)|clear H3; destruct f2 as [|[]| |]; try discriminate]);
  try reflexivity;
  try (pose proof H; rewrite Fleb_Rle in H by auto; Rle_bool_case H; [|discriminate];
       apply (round_le radix2 (FLT_exp (3-emax'-prec') prec') (round_mode mode_NE)) in H5);
  repeat match goal with H : context [Rlt_bool ?a ?b] |- _ =>
    Rlt_bool_case H;
    [destruct H as [H []]|
     unfold binary_overflow in H; simpl in H;
     apply B2FF_inj with (y:=B754_infinity _) in H]
  end.
  - rewrite Fleb_Rle by auto. apply Rle_bool_true. rewrite H2, H3. auto.
  - rewrite H2. destruct (Bsign f1) eqn:SIG.
    destruct (Bconv _ _ _ _ Hprec' Hmax' pl mode_NE f2) as [|[]| |];
      try reflexivity; discriminate.
    exfalso. destruct f1 as [| | |[]]; try discriminate.
    apply Rabs_lt_inv in H6. destruct H6.
    apply Rabs_ge_inv in H9. destruct H9. 2:Psatz.lra.
    apply Rle_lt_trans with (r3:=0), Rlt_not_le in H9.
    2:apply Ropp_lt_gt_0_contravar, bpow_gt_0.
    erewrite <- round_0 in H9 by auto. apply H9, round_le; eauto.
    apply F2R_ge_0_compat. compute. discriminate.
  - rewrite H3. destruct (Bsign f2) eqn:SIG.
    2:destruct (Bconv _ _ _ _ Hprec' Hmax' pl mode_NE f1) as [|[]| |[]];
      try reflexivity; discriminate.
    exfalso. destruct f2 as [| | |[]]; try discriminate.
    apply Rabs_lt_inv in H7. destruct H7.
    apply Rabs_ge_inv in H6. destruct H6. Psatz.lra.
    apply Rlt_le_trans with (r1:=0), Rlt_not_le in H6.
    2:apply bpow_gt_0.
    erewrite <- round_0 in H6 by auto. apply H6, round_le; eauto.
    apply F2R_le_0_compat. compute. discriminate.
  - rewrite H2, H3.
    destruct f1 as [| | |[]], f2 as [| | |[]]; try discriminate; reflexivity.
  - destruct f1 as [| | |[]]; discriminate.
  - destruct f1 as [| | |[]]; discriminate.
  - destruct Bconv as [| | |[]]; try reflexivity; discriminate.
  - destruct Bconv as [|[]| |]; try reflexivity; discriminate.
  - destruct Bconv as [| | |[]]; try reflexivity; discriminate.
  - destruct Bconv as [|[]| |]; try reflexivity; discriminate.
  - destruct f2 as [| | |[]]; discriminate.
  - destruct f2 as [| | |[]]; discriminate.
Qed.

Lemma singleoffloat_incr:
  forall f1 f2,
    Fleb f1 f2 = true ->
    Fleb (Float.of_single (Float.to_single f1))
         (Float.of_single (Float.to_single f2)) = true.
Proof.
  intros. apply Bconv_incr, Bconv_incr, H.
Qed.

Definition forward_singleoffloat (x:fitv+⊤) : fitv+⊤ :=
  match x with
  | Just (FITV mx Mx) =>
    Just (FITV (Float.of_single (Float.to_single mx))
               (Float.of_single (Float.to_single Mx)))
  | All => All
  end.

Lemma forward_singleoffloat_correct:
  ∀ x x_ab, x ∈ γ x_ab -> (Float.of_single (Float.to_single x)) ∈ γ (forward_singleoffloat x_ab).
Proof.
  intros x [|[mx Mx]] Hx; simpl in *. auto. split; apply singleoffloat_incr; intuition.
Qed.

Lemma BofZ_incr:
  ∀ z1 z2 prec emax Hprec Hmax,
    (z1 <= z2)%Z ->
    Fleb (BofZ prec emax Hprec Hmax z1)
         (BofZ _ _ Hprec Hmax z2) = true.
Proof.
  intros. use_float_specs.
  repeat match goal with H : context [Rlt_bool ?a ?b] |- _ =>
    Rlt_bool_case H;
    [destruct H as [H []]|
     unfold binary_overflow in H; simpl in H;
     apply B2FF_inj with (y:=B754_infinity _) in H]
  end.
  - rewrite Fleb_Rle, H0, H1 by auto. apply Rle_bool_true.
    apply round_le; auto. apply Z2R_le. auto.
  - rewrite H0. destruct (Zlt_bool_spec z1 0).
    destruct (BofZ _ _ Hprec Hmax z2); try discriminate; reflexivity.
    exfalso. eapply Rlt_le_trans, Rlt_not_le in H5. 2:apply H2.
    apply H5. rewrite <- !round_NE_abs, <- !Z2R_abs, !Z.abs_eq by (auto; omega).
    apply round_le, Z2R_le, H; auto. apply (valid_rnd_round_mode mode_NE).
  - rewrite H1. destruct (Zlt_bool_spec z2 0).
    2:destruct (BofZ _ _ Hprec Hmax z1) as [| | |[]]; try discriminate; reflexivity.
    exfalso. eapply Rlt_le_trans, Rlt_not_le in H3. 2:apply H2.
    apply H3. rewrite <- !round_NE_abs, <- !Z2R_abs, !Z.abs_neq by (auto; omega).
    apply round_le, Z2R_le; auto. apply (valid_rnd_round_mode mode_NE). omega.
  - rewrite H0, H1. destruct (Zlt_bool_spec z1 0), (Zlt_bool_spec z2 0); try reflexivity. omega.
Qed.

Lemma floatofz_incr:
  forall i1 i2,
    (i1 <= i2)%Z -> Fleb (BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) i1)
                         (BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt)i2) = true.
Proof.
  intros. apply BofZ_incr, H.
Qed.

Definition forward_floatofz (x:zitv+⊤) : fitv+⊤ :=
  match x with
  | Just (ZITV mx Mx) =>
    Just (FITV (BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) (mx:Z))
               (BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) (Mx:Z)))
  | All => Just (FITV (B754_infinity true) (B754_infinity false))
  end.

Lemma forward_floatofz_correct:
  ∀ x x_ab, x ∈ γ x_ab -> (BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) x) ∈ γ (forward_floatofz x_ab).
Proof.
  intros x [|[mx Mx]] []; simpl in *.
  - pose proof (binary_normalize_is_nan 53 1024 eq_refl eq_refl x 0 false mode_NE).
    change (is_nan (BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) x) = false) in H.
    destruct BofZ as [|[]| |[]]; split; try reflexivity; discriminate.
  - split; apply floatofz_incr; auto.
Qed.

Lemma singleofz_incr:
  forall i1 i2,
    (i1 <= i2)%Z ->
    Fleb (Float.of_single (BofZ 24 128 (@eq_refl _ Lt) (@eq_refl _ Lt) i1))
         (Float.of_single (BofZ 24 128 (@eq_refl _ Lt) (@eq_refl _ Lt) i2)) = true.
Proof.
  intros.
  apply Bconv_incr, BofZ_incr, H.
Qed.

Definition forward_singleofz (x:zitv+⊤) : fitv+⊤ :=
  match x with
    | Just (ZITV mx Mx) =>
      Just (FITV (Float.of_single (BofZ 24 128 (@eq_refl _ Lt) (@eq_refl _ Lt) mx))
                 (Float.of_single (BofZ 24 128 (@eq_refl _ Lt) (@eq_refl _ Lt) Mx)))
    | All => Just (FITV (B754_infinity true) (B754_infinity false))
  end.

Lemma forward_singleofz_correct:
  ∀ x x_ab, x ∈ γ x_ab -> (Float.of_single (BofZ 24 128 (@eq_refl _ Lt) (@eq_refl _ Lt) x)) ∈ γ (forward_singleofz x_ab).
Proof.
  intros x [|[mx Mx]] []; simpl in *.
  - pose proof (binary_normalize_is_nan 24 128 eq_refl eq_refl x 0 false mode_NE).
    change (is_nan (BofZ 24 128 (@eq_refl _ Lt) (@eq_refl _ Lt) x) = false) in H.
    apply floatofsingle_nan in H.
    destruct Float.of_single as [|[]| |[]]; split; try reflexivity; try discriminate.
  - split; apply singleofz_incr; auto.
Qed.

Definition forward_zoffloat (x:fitv+⊤) : zitv+⊤ :=
  match x with
  | Just (FITV mx Mx) =>
    match ZofB mx, ZofB Mx with
    | Some m, Some M => Just (ZITV m M)
    | _, _ => All
    end
  | All => All
  end.

Lemma forward_zoffloat_correct:
  ∀ x x_ab y, x ∈ γ x_ab ->
    ZofB x = Some y ->
    y ∈ γ (forward_zoffloat x_ab).
Proof.
  intros x [|[mx Mx]] y [] EQ; simpl in *. easy.
  destruct (ZofB mx) eqn:?; [|exact I].
  destruct (ZofB Mx) eqn:?; [|exact I].
  split; eauto using zoffloat_incr.
Qed.
Generated by coq2html