Module FloatIntervalsBackward


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

Definition RFF_lt (x:R) (y:full_float) :=
  if is_finite_FF y then (x < FF2R radix2 y)
  else y = F754_infinity false.

Definition RF_lt {prec emax} (x:R) (y:binary_float prec emax) :=
  RFF_lt x y.

Local Instance gammaR : gamma_op fitv R := fun i x =>
  let 'FITV mx Mx := i in
  RF_lt x Mx /\ RF_lt (-x) (Float.neg mx).

Definition next_ulp_ff prec emax (f:full_float) : full_float :=
  match f return _ with
  | F754_nan _ _ => f
  | F754_infinity true => binary_overflow prec emax mode_UP true
  | F754_finite true m e =>
    let m' := Pos.pred m in
    if Z.eqb e (3-emax-prec) then
      if Pos.eqb m 1 then F754_zero false
      else F754_finite true m' e
    else
      let minmant := (match 2 ^ (prec-1) with Zpos m => m | _ => xH end)%Z in
      if Pos.eqb m minmant then F754_finite true (Pos.pred_double minmant) (Z.pred e)
      else F754_finite true m' e
  | F754_zero _ => F754_finite false 1 (3-emax-prec)
  | F754_finite false m e =>
    let m' := Pos.succ m in
    let maxmant := (match 2 ^ prec with Zpos m => m | _ => xH end)%Z in
    if Pos.eqb m' maxmant then
      if Z.eqb e (emax-prec) then F754_infinity false
      else F754_finite false (Pos.div2 maxmant)%Z (Z.succ e)
    else
      F754_finite false m' e
  | F754_infinity false => f
  end.

Lemma next_ulp_ff_is_nan:
  forall prec emax f,
    is_nan_FF f = false ->
    is_nan_FF (next_ulp_ff prec emax f) = false.
Proof.
  destruct f as [|[]| |]; try reflexivity; try discriminate.
  intro. unfold next_ulp_ff.
  repeat match goal with
           | |- context [if ?b then _ else _] => destruct b
         end; reflexivity.
Qed.

Lemma pow2_pos :
  forall prec, (0 < prec)%Z ->
    exists n, (2 ^ (prec-1))%Z = Zpos n /\
              Z.pos (digits2_pos n) = prec /\
              Z.pos (digits2_pos (Pos.pred_double n)) = prec.
Proof.
  destruct prec; try discriminate.
  induction p using Pos.peano_ind. repeat econstructor. intro. clear H.
  destruct IHp as [n [Hn []]]. reflexivity.
  rewrite Pos2Z.inj_succ, Z.sub_succ_l, Z.pow_succ_r, Hn by (zify; omega).
  eexists. split. reflexivity. split. simpl. zify; omega.
  simpl. rewrite Pos2Z.inj_succ, H0. auto.
Qed.

Lemma next_ulp_ff_valid_binary:
  forall prec emax
         (prec_gt_0_ : (0 < prec)%Z) (Hmax : (prec < emax)%Z)
         (f:binary_float prec emax),
    valid_binary prec emax (next_ulp_ff prec emax f) = true.
Proof.
  intros.
  destruct f as [|[]| |[]]; try easy;
    unfold next_ulp_ff, B2FF, valid_binary, Fappli_IEEE.bounded, canonic_mantissa, FLT_exp,
           binary_overflow, overflow_to_inf, negb in *;
    rewrite ?andb_true_iff, ?Z.leb_le, <- ?Zeq_is_eq_bool in *.
  - simpl Z.pos. zify; omega.
  - destruct (pow2_pos prec) as [? [? []]]. omega.
    replace prec with (1+(prec-1))%Z by ring. rewrite Z.pow_add_r by omega. rewrite H.
    change (2 ^ 1 * Z.pos x - 1)%Z with (Z.pos (Pos.pred_double x)). cbv iota beta. rewrite H1.
    zify; omega.
  - destruct n. apply e.
  - destruct e0.
    destruct (Z.eqb_spec e (3-emax-prec)).
    + subst. destruct (Pos.eqb_spec m 1). auto.
      rewrite andb_true_iff, Z.leb_le. split; [|auto].
      rewrite <- Zeq_is_eq_bool, Z.max_r_iff, Zpos_digits2_pos in *.
      etransitivity; [|now eauto].
      apply Z.sub_le_mono_r, Z.add_le_mono_r, Zdigits_le.
      discriminate.
      rewrite <- (Pos.succ_pred m) at 2 by easy. zify; omega.
    + destruct (pow2_pos prec) as [? [? []]]. omega. rewrite H1.
      destruct (Pos.eqb_spec m x); rewrite andb_true_iff, Z.leb_le, <- Zeq_is_eq_bool;
      split; try (zify; omega).
      assert (Z.pos (digits2_pos m) = prec) by (zify; omega).
      rewrite Zpos_digits2_pos, Pos2Z.inj_pred
        by (intro; subst m prec; destruct x; simpl in H4; zify; omega).
      rewrite Zpos_digits2_pos in *. rewrite <- H at 2. f_equal. f_equal. f_equal.
      rewrite H4. apply Zdigits_unique. rewrite Z.abs_eq by (zify; omega).
      pose proof Zdigits_correct radix2 (Z.pos m). rewrite H4 in H5. destruct H5.
      simpl radix_val in *. zify; omega.
  - destruct (pow2_pos (prec+1)) as [? [? []]]. omega. rewrite Z.add_simpl_r in H. rewrite H.
    destruct (Pos.eqb_spec (Pos.succ m) x);
      [destruct (Z.eqb_spec e (emax-prec))|]; unfold B2FF; try easy;
    rewrite andb_true_iff, Z.leb_le, <- Zeq_is_eq_bool in *; split; try (zify; omega).
    + destruct e0.
      replace (Z.pos (digits2_pos (Pos.div2 x))) with (Z.pred (Z.pos (digits2_pos x)))
      by (destruct x; simpl Pos.div2; simpl digits2_pos; zify; omega).
      zify; omega.
    + assert (Z.pos (digits2_pos m) <= Z.pos (digits2_pos (Pos.succ m)))%Z.
      { rewrite !Zpos_digits2_pos. apply Zdigits_le; zify; omega. }
      assert (Z.pos (digits2_pos (Pos.succ m)) <= prec)%Z.
      { rewrite Zpos_digits2_pos in *. apply Zdigits_le_Zpower. rewrite Z.abs_eq by (zify; omega).
        simpl radix_val. cut (Z.pos m < 2 ^ prec)%Z. zify; omega.
        apply Zpower_gt_Zdigits with (x:=Z.pos m) (beta:=radix2). zify; omega. }
      zify; omega.
Qed.

Definition next_ulp prec emax prec_gt_0_ Hmax
           (f:binary_float prec emax) : binary_float prec emax :=
  FF2B prec emax _ (next_ulp_ff_valid_binary _ _ prec_gt_0_ Hmax f).

Lemma next_ulp_is_nan:
  forall prec emax prec_gt_0_ Hmax f,
    is_nan f = false ->
    is_nan (next_ulp prec emax prec_gt_0_ Hmax f) = false.
Proof.
  intros. unfold next_ulp. rewrite is_nan_FF2B.
  apply next_ulp_ff_is_nan. rewrite is_nan_FF_B2FF. auto.
Qed.

Lemma next_ulp_round :
  forall prec emax prec_gt_0_ Hmax, (1 < prec)%Z ->
  forall (f:binary_float prec emax), is_finite f = true ->
  forall x mode,
    (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode mode) x <= f) ->
    RF_lt x (next_ulp _ _ prec_gt_0_ Hmax f).
Proof.
  intros prec emax prec_gt_0_ Hmax prec_gt_1 f FINf x mode LE.
  unfold RF_lt, RFF_lt in *.
  rewrite FF2R_B2FF.
  rewrite is_finite_FF_B2FF.
  destruct (is_finite (next_ulp prec emax prec_gt_0_ Hmax f)) eqn : FINnext.
  Focus 2.
  destruct f; try discriminate.
  unfold next_ulp, next_ulp_ff in *. simpl in *.
  rewrite is_finite_FF2B in FINnext. rewrite B2FF_FF2B.
  repeat match type of FINnext with context [if ?b then _ else _] => destruct b eqn:? end;
    try discriminate. auto.
  destruct f as [|[]| |[]]; try discriminate.
  - apply Rnot_le_lt. intro. eapply round_ge_generic in H.
    pose proof (Rle_trans _ _ _ H LE).
    simpl in H0. apply F2R_le_0_reg in H0. omega. auto. auto.
    apply generic_format_B2R.
  - apply Rnot_le_lt. intro.
    eapply round_ge_generic in H; eauto. 2:apply generic_format_B2R.
    pose proof (Rle_trans _ _ _ H LE). clear H LE FINf.
    unfold next_ulp, next_ulp_ff in *. simpl in *.
    rewrite B2R_FF2B in H0. rewrite is_finite_FF2B in FINnext.
    repeat match type of FINnext with context [if ?b then _ else _] => destruct b eqn:? end.
    + apply F2R_ge_0_reg in H0. zify; omega.
    + apply Rmult_le_reg_r, le_Z2R in H0. apply H0. simpl. apply CompOpp_iff. apply Ppred_Plt.
      destruct m; discriminate.
      apply bpow_gt_0.
    + apply Pos.eqb_eq in Heqb0. rewrite <- Heqb0 in H0.
      unfold FF2R, F2R in H0. simpl in H0.
      replace (Z.pred e) with (-1 + e)%Z in H0 by omega. rewrite bpow_plus, <- Rmult_assoc in H0.
      apply Rmult_le_reg_r in H0. 2:apply bpow_gt_0.
      change (P2R (Pos.pred_double m)) with (Z.pos (Pos.pred (2*m)):R) in H0.
      rewrite Pos2Z.inj_pred, <- Z.sub_1_r, Z2R_minus, Pos2Z.inj_mul, Z2R_mult in H0 by discriminate.
      simpl in H0. rewrite Ropp_mult_distr_l_reverse, Rmult_minus_distr_r, Rinv_r_simpl_m in H0.
      Psatz.lra. apply (Z2R_neq 2 0). discriminate.
    + apply Rmult_le_reg_r, le_Z2R in H0. apply H0. simpl. apply CompOpp_iff. apply Ppred_Plt.
      2:apply bpow_gt_0.
      apply Z.eqb_neq in Heqb. change (e <> 3 - emax - prec)%Z in Heqb.
      unfold Fappli_IEEE.bounded, canonic_mantissa, FLT_exp in e0.
      rewrite Bool.andb_true_iff in e0. destruct e0.
      apply Zeq_bool_eq in H.
      intro. subst m. simpl digits2_pos in H. clear -Heqb H prec_gt_1. zify; omega.
  - apply Rnot_le_lt. intro.
    eapply round_ge_generic in H; eauto. 2:apply generic_format_B2R.
    pose proof (Rle_trans _ _ _ H LE). clear H LE FINf.
    unfold next_ulp, next_ulp_ff in *. simpl in *.
    rewrite B2R_FF2B in H0. rewrite is_finite_FF2B in FINnext.
    repeat match type of FINnext with context [if ?b then _ else _] => destruct b eqn:? end;
      try discriminate.
    + apply Pos.eqb_eq in Heqb. rewrite <- Heqb in H0.
      replace prec with (1+(prec-1))%Z in Heqb by ring. rewrite Z.pow_add_r in Heqb by omega.
      destruct (2^(prec-1))%Z eqn:EQ; try (destruct m; discriminate). simpl in Heqb.
      rewrite Heqb in H0. unfold FF2R, F2R in H0. simpl in H0.
      replace (Z.succ e) with (1+e)%Z in H0 by omega. rewrite bpow_plus, <- Rmult_assoc in H0.
      apply Rmult_le_reg_r in H0. 2:apply bpow_gt_0. change (Z.pos p * 2%Z <= P2R m) in H0.
      rewrite <- Z2R_mult, Z.mul_comm in H0. apply le_Z2R with (n:=Z.pos _) in H0. zify; omega.
    + apply Rmult_le_reg_r in H0. 2:apply bpow_gt_0.
      simpl in H0. apply le_Z2R with (m:=Z.pos _) (n:=Z.pos _) in H0. zify; omega.
Qed.

Lemma next_ulp_round_overflow :
    forall prec emax prec_gt_0_ Hmax x mode (f:binary_float _ _), (1 < prec)%Z ->
    (if Rlt_bool (Rabs (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode mode) x))
                 (bpow radix2 emax)
     then (f:R) = round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode mode) x /\
          is_finite f = true
     else (f:full_float) = binary_overflow prec emax mode (Rlt_bool x 0)) ->
  forall fM, Fleb f fM = true ->
  RF_lt x (next_ulp prec emax prec_gt_0_ Hmax fM).
Proof.
  intros.
  Rlt_bool_case H0; destruct (is_finite fM) eqn:?.
  - destruct H0.
    apply next_ulp_round with mode. auto. auto.
    rewrite <- H0. rewrite Fleb_Rle in H1 by auto.
    Rle_bool_case H1. auto. discriminate.
  - destruct H0.
    assert (is_nan fM = false) by eauto.
    destruct fM as [|[]| |]; try discriminate.
    destruct f as [| | |[]]; discriminate.
    reflexivity.
  - Rlt_bool_case H0.
    + rewrite Rabs_left1 in H2.
      2:erewrite <- round_0 by eauto; apply round_le; eauto; Psatz.lra.
      unfold RF_lt, RFF_lt. rewrite is_finite_FF_B2FF, FF2R_B2FF.
      destruct (is_finite (next_ulp prec emax prec_gt_0_ Hmax fM)) eqn:?.
      * apply Rnot_le_lt. intro.
        apply Ropp_le_contravar in H2. erewrite Ropp_involutive in H2.
        eapply Rle_trans in H2. 2:eapply round_le, H4; eauto.
        rewrite round_generic in H2. 2:auto. 2:apply generic_format_B2R.
        pose proof abs_B2R_lt_emax _ _ (next_ulp prec emax prec_gt_0_ Hmax fM).
        edestruct Rabs_lt_inv; eauto. Psatz.lra.
      * revert Heqb0. unfold next_ulp. rewrite is_finite_FF2B, B2FF_FF2B.
        destruct fM as [| | |[]]; try discriminate; unfold B2FF, next_ulp_ff.
        destruct Z.eqb. destruct Pos.eqb; discriminate. destruct Pos.eqb; discriminate.
        destruct Z.eqb. destruct Pos.eqb. auto. discriminate.
        destruct Pos.eqb; discriminate.
    + unfold binary_overflow in H0.
      destruct (overflow_to_inf mode false);
        destruct f as [| |? []|]; inv H0;
        destruct fM as [|[]| |]; inv H1;
        try reflexivity.
      unfold Fleb, Bcompare in H4. destruct b. discriminate.
      unfold RF_lt, RFF_lt, next_ulp. rewrite B2FF_FF2B. simpl.
      clear Heqb. unfold Fappli_IEEE.bounded in e1. rewrite Bool.andb_true_iff in e1. destruct e1.
      apply Zle_is_le_bool in H1.
      destruct (Z.compare_spec (emax - prec) e). 2:omega. 2:discriminate.
      subst e. rewrite Z.eqb_refl.
      edestruct pow2_pos with (prec:=(prec+1)%Z) as (? & ? & ? & ?). omega.
      rewrite Z.add_simpl_r in H5. rewrite H5 in *.
      assert (x0 <> 1)%positive by (intro; subst x0; simpl in H6; omega).
      destruct (Z.pos x0 - 1)%Z eqn:EQ; try (zify; omega).
      assert (x0 = Pos.succ p) by (zify; omega). subst x0.
      rewrite Pos.eqb_compare, Pos.compare_succ_succ by auto.
      rewrite Pos.compare_antisym. fold (p ?= m)%positive in H4.
      destruct (Pos.compare_spec p m). reflexivity. 2:discriminate. simpl.
      apply canonic_canonic_mantissa with (sx:=false) in H0.
      unfold canonic, F2R, Fnum, Fexp, cond_Zopp, canonic_exp, FLT_exp in H0.
      rewrite ln_beta_mult_bpow in H0.
      assert (2^prec <= Z.pos m)%Z by (zify; omega).
      apply Z2R_le in H10.
      rewrite Z2R_Zpower with (r:=radix2) in H10 by omega.
      apply ln_beta_le with (r:=radix2) in H10. 2:apply bpow_gt_0.
      rewrite ln_beta_bpow in H10. zify; omega.
      change R0 with (0%Z:R). apply Z2R_neq. discriminate.
  - assert (is_nan fM = false) by eauto.
    destruct fM as [|[]| |]; try discriminate. 2:reflexivity.
    destruct f as [|[]| |[]]; try discriminate.
    unfold binary_overflow in H0.
    destruct overflow_to_inf; inv H0.
    Rlt_bool_case H5. 2:discriminate.
    rewrite Rabs_left1 in H2.
    2:erewrite <- round_0 by eauto; apply round_le; eauto; Psatz.lra.
    unfold RF_lt, RFF_lt, next_ulp, next_ulp_ff. simpl is_finite_FF.
    rewrite FF2R_B2FF. unfold B2FF.
    apply Rnot_le_lt. intro.
    apply Ropp_le_contravar in H2. erewrite Ropp_involutive in H2.
    eapply Rle_trans in H2. 2:eapply round_le, H4; eauto.
    rewrite round_generic in H2. 2:auto. 2:apply generic_format_B2R.
    pose proof abs_B2R_lt_emax _ _
         (FF2B prec emax (binary_overflow prec emax mode_UP true)
               (next_ulp_ff_valid_binary prec emax prec_gt_0_ Hmax (B754_infinity true))).
    edestruct Rabs_lt_inv; eauto. Psatz.lra.
Qed.

Lemma next_ulp_lub:
  forall prec emax prec_gt_0_ Hmax (f1 f2:binary_float prec emax), (1 < prec)%Z ->
    is_nan f1 = false ->
    is_nan f2 = false ->
    Fleb f1 f2 = true \/
    Fleb (next_ulp _ _ prec_gt_0_ Hmax f2) f1 = true.
Proof.
  intros.
  destruct f1 as [|[]| |[]], f2 as [|[]| |[]]; try discriminate H0; try discriminate H1;
    try (left; reflexivity); try (right; reflexivity).
  - right. unfold next_ulp.
    generalize ((next_ulp_ff_valid_binary prec emax prec_gt_0_ Hmax (B754_finite true m e e0))).
    unfold next_ulp_ff, B2FF.
    repeat match goal with |- context [if ?b then _ else _] => destruct b eqn:? end;
      try (intro; reflexivity).
  - right. unfold next_ulp.
    generalize ((next_ulp_ff_valid_binary prec emax prec_gt_0_ Hmax (B754_finite true m e e0))).
    unfold next_ulp_ff, B2FF.
    repeat match goal with |- context [if ?b then _ else _] => destruct b eqn:? end;
      try (intro; reflexivity).
  - right. unfold next_ulp.
    generalize ((next_ulp_ff_valid_binary prec emax prec_gt_0_ Hmax (B754_finite false m e e0))).
    unfold next_ulp_ff, B2FF.
    repeat match goal with |- context [if ?b then _ else _] => destruct b eqn:? end;
      try (intro; reflexivity).
  - right. unfold next_ulp.
    generalize ((next_ulp_ff_valid_binary prec emax prec_gt_0_ Hmax (B754_infinity true))).
    unfold B2FF, next_ulp_ff, binary_overflow, overflow_to_inf, negb, FF2B, valid_binary, Fleb, Bcompare.
    intros _.
    clear H0 H1. apply -> andb_true_iff in e0. destruct e0.
    rewrite Z.leb_compare, Z.compare_antisym in H1.
    destruct Z.compare; inversion H1; clear H1; try reflexivity.
    unfold canonic_mantissa, FLT_exp in H0. apply Zeq_bool_eq in H0.
    assert (Z.pos (digits2_pos m) <= prec)%Z by (zify; omega).
    destruct (pow2_pos (prec+1)) as [? []]. omega. rewrite Z.add_simpl_r in H2. rewrite H2.
    pose proof (Zpower_lt radix2 0 prec). simpl in H4. rewrite H2 in H4.
    destruct (Z.pos x - 1)%Z eqn:EQ; try (zify; omega).
    fold (Pos.compare p m). destruct (Pos.compare_spec p m); auto.
    assert (x = Pos.succ p) by (zify; omega). subst x.
    rewrite Zpos_digits2_pos in H1. apply Zpower_gt_Zdigits in H1. simpl in H1. zify; omega.
  - clear H0 H1. unfold Fleb, next_ulp, Bcompare.
    generalize (next_ulp_ff_valid_binary prec emax prec_gt_0_ Hmax (B754_finite true m0 e1 e2)).
    unfold B2FF, next_ulp_ff, FF2B.
    repeat match goal with |- context [if ?b then _ else _] => destruct b eqn:? end; intros _.
    + unfold Fappli_IEEE.bounded, canonic_mantissa, FLT_exp in e0.
      rewrite andb_true_iff in e0. destruct e0. apply Zeq_bool_eq in H0.
      apply Z.eqb_eq in Heqb.
      left. destruct (Z.compare_spec e e1); auto; try (zify; omega).
      apply Pos.eqb_eq in Heqb0. subst m0. destruct m; auto.
    + rewrite Z.compare_antisym.
      destruct (Z.compare_spec e1 e); auto.
      simpl. fold (Pos.compare m m0). fold (Z.compare (Z.pos m) (Z.pos m0)).
      fold (Pos.compare (Pos.pred m0) m). fold (Z.compare (Z.pos (Pos.pred m0)) (Z.pos m)).
      apply Pos.eqb_neq in Heqb0. rewrite Pos2Z.inj_pred by auto.
      destruct (Z.compare_spec (Z.pos m) (Z.pos m0)); auto.
      right.
      destruct (Z.compare_spec (Z.pred (Z.pos m0)) (Z.pos m)); auto.
      zify; omega.
    + apply Pos.eqb_eq in Heqb0.
      destruct (pow2_pos prec prec_gt_0_) as (? & ? & ? & ?). rewrite H0 in *. subst x.
      destruct (Z.compare_spec (Z.pred e1) e); destruct (Z.compare_spec e e1); auto; try omega.
      * right.
        fold (Pos.compare (Pos.pred_double m0) m). destruct (Pos.compare_spec (Pos.pred_double m0) m);auto.
        assert (Z.pos (Pos.succ (Pos.pred_double m0)) < Z.succ (Z.pos m))%Z by (zify; omega).
        rewrite Pos.succ_pred_double in H6.
        replace (Z.pos m0~0) with (2*Z.pos m0)%Z in H6 by (zify; omega). rewrite <- H0 in H6.
        unfold Fappli_IEEE.bounded, canonic_mantissa, FLT_exp in e0. rewrite Bool.andb_true_iff in e0. destruct e0.
        apply Zeq_bool_eq in H7. assert (Z.pos (digits2_pos m) <= prec)%Z by (zify; omega).
        rewrite Zpos_digits2_pos in H9. apply Zpower_gt_Zdigits in H9. simpl in H9.
        change 2%Z with (2^1)%Z in H6 at 1. rewrite <- Zpower_plus in H6 by omega.
        replace (1+(prec-1))%Z with prec in H6 by ring. omega.
      * fold (Pos.compare m m0). destruct (Pos.compare_spec m m0); auto.
        unfold Fappli_IEEE.bounded, canonic_mantissa, FLT_exp in e0. rewrite Bool.andb_true_iff in e0. destruct e0.
        apply Zeq_bool_eq in H6. apply Z.eqb_neq in Heqb.
        assert (Z.pos (digits2_pos m) = prec) by (zify; omega).
        rewrite Zpos_digits2_pos in H8. pose proof Zdigits_correct radix2 (Z.pos m).
        rewrite H8 in H9. simpl radix_val in H9. zify; omega.
    + rewrite Z.compare_antisym. destruct (Z.compare_spec e1 e); auto. simpl.
      fold (Pos.compare (Pos.pred m0) m). destruct (Pos.compare_spec (Pos.pred m0) m); auto.
      fold (Pos.compare m m0). destruct (Pos.compare_spec m m0); auto.
      apply Pos.succ_lt_mono in H1. rewrite Pos.succ_pred in H1 by (zify; omega).
      zify; omega.
  - right. unfold next_ulp.
    generalize ((next_ulp_ff_valid_binary prec emax prec_gt_0_ Hmax (B754_zero b))).
    unfold next_ulp_ff, B2FF, FF2B, Fleb, Bcompare.
    intros _.
    destruct (Z.compare_spec (3-emax-prec) e).
    destruct m; reflexivity.
    auto.
    clear H0 H1.
    unfold Fappli_IEEE.bounded, canonic_mantissa, FLT_exp in e0.
    rewrite andb_true_iff in e0. destruct e0. apply Zeq_bool_eq in H0.
    zify; omega.
  - right. unfold next_ulp.
    generalize ((next_ulp_ff_valid_binary prec emax prec_gt_0_ Hmax (B754_finite true m0 e1 e2))).
    unfold next_ulp_ff, B2FF.
    repeat match goal with |- context [if ?b then _ else _] => destruct b eqn:? end;
      try (intro; reflexivity).
  - clear H H0. unfold Fleb, next_ulp, Bcompare.
    generalize (next_ulp_ff_valid_binary prec emax prec_gt_0_ Hmax (B754_finite false m0 e1 e2)).
    unfold B2FF, next_ulp_ff, FF2B.
    repeat match goal with |- context [if ?b then _ else _] => destruct b eqn:? end; intros _.
    + left. apply Pos.eqb_eq in Heqb. apply Z.eqb_eq in Heqb0.
      destruct (Z.compare_spec e e1); auto.
      * fold (Pos.compare m m0). destruct (Pos.compare_spec m m0); auto.
        destruct (pow2_pos (prec+1)) as (? & ? & ? & ?). omega.
        rewrite Z.add_simpl_r in H2. rewrite H2 in Heqb.
        assert (Z.pos x <= Z.pos m)%Z by (zify; omega).
        apply Zdigits_le with (beta:=radix2) in H5. 2:discriminate.
        rewrite <- !Zpos_digits2_pos in H5.
        unfold Fappli_IEEE.bounded, canonic_mantissa, FLT_exp in e0.
        rewrite andb_true_iff in e0. destruct e0. apply Zeq_bool_eq in H6. zify; omega.
      * unfold Fappli_IEEE.bounded, canonic_mantissa, FLT_exp in e0.
        rewrite andb_true_iff in e0. destruct e0. apply Z.leb_le in H2.
        zify; omega.
    + apply Pos.eqb_eq in Heqb. apply Z.eqb_neq in Heqb0.
      destruct (pow2_pos (prec+1)) as (? & ? & ? & ?). omega.
      rewrite Z.add_simpl_r in H. rewrite H in Heqb |- *.
      destruct (Z.compare_spec e e1), (Z.compare_spec (Z.succ e1) e); auto; try (zify; omega).
      * fold (Pos.compare m m0). destruct (Pos.compare_spec m m0); auto.
        assert (Z.pos (Pos.succ m0) <= Z.pos m)%Z by (zify; omega).
        rewrite Heqb, <- H in H6.
        apply Zdigits_gt_Zpower with (beta:=radix2) (x:=Z.pos m) in H6.
        rewrite <- Zpos_digits2_pos in *.
        unfold Fappli_IEEE.bounded, canonic_mantissa, FLT_exp in e0.
        rewrite andb_true_iff in e0. destruct e0. apply Zeq_bool_eq in H7.
        zify; omega.
      * unfold Fappli_IEEE.bounded, canonic_mantissa, FLT_exp in e0, e2. clear H1.
        replace prec with (1+(prec-1))%Z in H by ring. rewrite Zpower_plus in H by omega.
        simpl in H. destruct (2 ^ (prec - 1))%Z eqn:EQ; inversion H. subst x. simpl.
        fold (Pos.compare p m). destruct (Pos.compare_spec p m); auto.
        rewrite andb_true_iff in e0. destruct e0. apply Zeq_bool_eq in H6.
        rewrite andb_true_iff in e2. destruct e2. apply Zeq_bool_eq in H8.
        assert (Z.pos (digits2_pos m) = prec) by (zify; omega).
        rewrite Zpos_digits2_pos in H10.
        destruct (Zdigits_correct radix2 (Z.pos m)). rewrite H10 in H11.
        simpl radix_val in *. zify; omega.
    + rewrite Z.compare_antisym.
      destruct (Z.compare_spec e1 e); auto.
      simpl. fold (Pos.compare m m0). fold (Z.compare (Z.pos m) (Z.pos m0)).
      fold (Pos.compare (Pos.succ m0) m). fold (Z.compare (Z.pos (Pos.succ m0)) (Z.pos m)).
      destruct (Z.compare_spec (Z.pos m) (Z.pos m0)); auto.
      right.
      destruct (Z.compare_spec (Z.pos (Pos.succ m0)) (Z.pos m)); auto.
      zify; omega.
Qed.

Definition backward_round (x:fitv) : fitv :=
  let 'FITV mx Mx := x in
  FITV (Float.neg (next_ulp 53 1024 eq_refl eq_refl (Float.neg mx)))
       (next_ulp 53 1024 eq_refl eq_refl Mx).

Lemma backward_round_correct:
  forall x_r (x:float),
    (if Rlt_bool
          (Rabs (round radix2 (FLT_exp (3 - 1024 - 53) 53)
                       (round_mode mode_NE) x_r))
          (bpow radix2 1024)
     then (x:R) = round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) x_r /\
          is_finite x = true
     else (x:full_float) = binary_overflow 53 1024 mode_NE (Rlt_bool x_r 0)) ->
  forall x_ab, x ∈ γ x_ab ->
  x_r ∈ γ (backward_round x_ab).
Proof.
  intros.
  destruct x_ab; destruct H0; try easy. split.
  - eapply next_ulp_round_overflow; eauto. reflexivity.
  - Transparent Float.neg.
    unfold Float.neg.
    rewrite Bopp_involutive.
    rewrite <- fneg_decr in H0.
    eapply next_ulp_round_overflow with (mode:=mode_NE); eauto. reflexivity.
    rewrite round_NE_opp, Rabs_Ropp.
    unfold Float.neg. rewrite B2R_Bopp, is_finite_Bopp.
    unfold round_mode in H. Rlt_bool_case H.
    now intuition.
    destruct x as [| |?[]|]; inv H.
    destruct (Rlt_bool_spec x_r 0), (Rlt_bool_spec (-x_r) 0); try reflexivity; try Psatz.lra.
    destruct (Rcompare_spec x_r 0); try Psatz.lra.
    subst. rewrite round_0, Rabs_R0 in H2. pose proof (bpow_gt_0 radix2 1024). Psatz.lra.
    apply (valid_rnd_round_mode mode_NE).
    destruct f as [|[]| |]; try reflexivity; try discriminate.
    unfold next_ulp, next_ulp_ff, B2FF, Bopp. rewrite is_nan_FF2B.
    repeat (match goal with |- is_nan_FF (if ?b then _ else _) = false => destruct b end);
      reflexivity.
Qed.

Definition backward_floatofz (res_ab:fitv+⊤) (x_ab:zitv+⊤) : zitv+⊤+⊥ :=
  match res_ab with
  | Just res_ab' =>
    let 'FITV mx Mx := backward_round res_ab' in
    let low : option Zfast :=
      match Zoffloat_DN (Float.neg mx), x_ab with
      | Some m, Just (ZITV m' _) => Some (Zfastmax (Zfastopp m) m')
      | Some m, All => Some (Zfastopp m)
      | None, Just (ZITV m' _) => Some (m':Zfast)
      | None, All => None
      end
    in
    let high : option Zfast :=
      match Zoffloat_DN Mx, x_ab with
      | Some M, Just (ZITV _ M') => Some (Zfastmin M M')
      | Some M, All => Some (M:Zfast)
      | None, Just (ZITV _ M') => Some M'
      | None, All => None
      end
    in
    match low, high with
    | Some m, Some M =>
      if Zfastleb m M then NotBot (Just (ZITV m M))
      else Bot
    | _, _ => NotBot All
    end
  | All => NotBot All
  end.

Lemma backward_floatofz_correct :
  forall x x_ab, x ∈ γ x_ab ->
  forall res_ab, BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) x ∈ γ res_ab ->
    x ∈ γ (backward_floatofz res_ab x_ab).
Proof.
  intros. unfold backward_floatofz.
  destruct res_ab as [|res_ab]. auto.
  assert (gammaR (backward_round res_ab) x).
  { eapply backward_round_correct; eauto.
    use_float_specs.
    destruct Rlt_bool. intuition.
    destruct (Z.ltb_spec x 0), (Rlt_bool_spec x 0); auto.
    apply (le_Z2R 0 x) in H3. omega.
    apply (lt_Z2R x 0) in H3. omega. }
  destruct backward_round.
  destruct H1. unfold RF_lt, RFF_lt, F2R, Fnum, Fexp, bpow in H1, H2.
  rewrite is_finite_FF_B2FF, FF2R_B2FF in H1, H2.
  assert (forall m, Zoffloat_DN (Float.neg f) = Some m -> (-m <= x)%Z).
  { pose proof (Zoffloat_DN_correct (Float.neg f)).
    destruct (Zoffloat_DN (Float.neg f)). 2:easy.
    destruct H3. rewrite H3 in H2. intros. injection H5. intro. subst z. clear H5.
    apply Zopp_le_cancel, le_Z2R. rewrite Zopp_involutive, H4.
    unfold round, scaled_mantissa, canonic_exp, Fcore_FIX.FIX_exp, F2R, Fexp, Fnum,
           scaled_mantissa, bpow, round_mode, Zopp at 2.
    rewrite !Rmult_1_r.
    apply Z2R_le, Zfloor_lub.
    rewrite Z2R_opp. Psatz.lra. }
  assert (forall M, Zoffloat_DN f0 = Some M -> (x <= M)%Z).
  { pose proof (Zoffloat_DN_correct f0).
    destruct (Zoffloat_DN f0). 2:easy.
    destruct H4. rewrite H4 in H1. intros. injection H6. intro. subst z. clear H6.
    apply le_Z2R. rewrite H5.
    unfold round, scaled_mantissa, canonic_exp, Fcore_FIX.FIX_exp, F2R, Fexp, Fnum,
           scaled_mantissa, bpow, round_mode, Zopp.
    rewrite !Rmult_1_r.
    apply Z2R_le, Zfloor_lub. Psatz.lra. }
  destruct (Zoffloat_DN (Float.neg f)); [specialize (H3 _ eq_refl)|clear H3];
    (destruct (Zoffloat_DN f0); [specialize (H4 _ eq_refl)|clear H4]);
  destruct x_ab as [|[]]; destruct H; auto; try exact I; simpl; fastunwrap.
  destruct (Z.leb_spec (-z) z0); [split|]; simpl in *; Psatz.lia.
  destruct (Z.leb_spec (Z.max (-z) z1) (Z.min z0 z2)); [split|]; simpl in *; Psatz.lia.
  destruct (Z.leb_spec (Z.max (-z) z0) z1); [split|]; simpl in *; Psatz.lia.
  destruct (Z.leb_spec z0 (Z.min z z1)); [split|]; simpl in *; Psatz.lia.
  destruct (Z.leb_spec z z0); [split|]; simpl in *; Psatz.lia.
Qed.

Definition half_backward_zoffloat (a:Zfast)
           prec emax Hprec Hmax : binary_float prec emax :=
  if Zfastleb a F0 then
    next_ulp prec emax Hprec Hmax
      (binary_normalize prec emax Hprec Hmax mode_DN (Zfastsub a F1) 0 false)
  else
    binary_normalize prec emax Hprec Hmax mode_UP a 0 false.

Lemma half_backward_zoffloat_correct :
  forall prec emax Hprec Hmax (f:binary_float prec emax) i a, (1 < prec)%Z ->
    ZofB f = Some i ->
    (a <= i)%Z ->
    Fleb (half_backward_zoffloat a _ _ Hprec Hmax) f = true.
Proof.
  intros * Hprec1. intros. pose proof ZofB_correct _ _ f. rewrite H in H1.
  destruct (is_finite f) eqn:?; inv H1. unfold half_backward_zoffloat. fastunwrap.
  simpl Z.of_N. destruct (Z.leb_spec a 0).
  - use_float_specs.
    Rlt_bool_case H2.
    + destruct H2 as [? []].
      destruct (next_ulp_lub _ _ Hprec Hmax f (binary_normalize _ _ Hprec Hmax mode_DN (a - 1) 0 false) Hprec1).
      destruct f; try discriminate; reflexivity.
      destruct binary_normalize; try discriminate; reflexivity.
      2:auto.
      exfalso.
      rewrite Fleb_Rle, H2 in H6 by auto.
      Rle_bool_case H6; [|discriminate].
      apply round_le with (beta:=radix2) (fexp:=Fcore_FIX.FIX_exp 0) (rnd:=round_mode mode_ZR) in H7; eauto with typeclass_instances.
      apply Z2R_le in H0. simpl in H7. unfold round at 1 in H7.
      unfold F2R, scaled_mantissa in H7. simpl in H7.
      rewrite !Rmult_1_r in H7.
      pose proof (Rle_trans _ _ _ H0 H7).
      clear - H8 H1.
      assert (round radix2 (FLT_exp (3 - emax - prec) prec) (round_mode mode_DN) (a-1)%Z <= (a-1)%Z).
      { unfold round, F2R, Fnum, Fexp, scaled_mantissa. simpl.
        eapply Rle_trans.
        apply Rmult_le_compat_r. apply bpow_ge_0. apply Zfloor_lb.
        rewrite Rmult_assoc, <- bpow_plus, Z.add_opp_diag_l. simpl. ring_simplify. apply Rle_refl. }
      apply round_le with (beta:=radix2) (fexp:=Fcore_FIX.FIX_exp 0) (rnd:=round_mode mode_ZR) in H;
        eauto with typeclass_instances.
      pose proof (Rle_trans _ _ _ H8 H). clear H1 H8 H.
      rewrite round_generic in H0; eauto.
      apply le_Z2R in H0. omega.
      unfold generic_format, F2R, Fnum, Fexp, scaled_mantissa, Fcore_FIX.FIX_exp, canonic_exp.
      simpl. rewrite !Rmult_1_r, Ztrunc_Z2R. auto.
    + rewrite Rlt_bool_true in H2.
      destruct binary_normalize as [|[]|? []|]; try discriminate.
      destruct f; try discriminate; try reflexivity.
      destruct (next_ulp_lub _ _ Hprec Hmax (B754_finite b m e e0) (B754_infinity true) Hprec1); auto.
      destruct b; discriminate.
      unfold F2R, Fnum, Fexp, bpow. rewrite Rmult_1_r. apply Z2R_lt with (n:=0%Z).
      omega.
  - destruct f; try (inv H; omega).
    simpl in H0. pose proof Ztrunc_Z2R 0. simpl in H2. omega.
    destruct b.
    pose proof zoffloat_incr _ _ (B754_finite true m e e0) (B754_zero false) _ _ eq_refl H eq_refl. omega.
    assert (round radix2 (FLT_exp (3 - emax - prec) prec)
                  (round_mode mode_UP) (F2R (beta:=radix2) {| Fnum := a; Fexp := 0 |}) <=
            B754_finite false m e e0).
    { eapply round_le_generic; auto.
      apply generic_format_B2R.
      unfold F2R, Fnum, Fexp, bpow. rewrite Rmult_1_r.
      eapply Rle_trans.
      apply Z2R_le, H0.
      rewrite Ztrunc_floor. apply Zfloor_lb.
      apply F2R_ge_0_compat. compute. discriminate. }
    use_float_specs.
    rewrite Rlt_bool_true in H3.
    + destruct H3 as [? []]. rewrite Fleb_Rle; auto. apply Rle_bool_true. rewrite H3. auto.
    + rewrite Rabs_pos_eq.
      eapply Rle_lt_trans. eauto. eapply bounded_lt_emax; eauto.
      eapply round_ge_generic; auto. apply generic_format_0.
      apply Rmult_le_pos. apply Z2R_le with (m:=Z0). simpl; omega. apply bpow_ge_0.
Qed.

Definition backward_zoffloat (res_ab:zitv+⊤) : fitv+⊤ :=
  let new_x_ab :=
    match res_ab with
    | All =>
      FITV (FF2B 53 1024 (binary_overflow 53 1024 mode_UP true) eq_refl)
           (FF2B 53 1024 (binary_overflow 53 1024 mode_DN false) eq_refl)
    | Just (ZITV a b) =>
      FITV (half_backward_zoffloat a 53 1024 eq_refl eq_refl)
           (Float.neg (half_backward_zoffloat (Zfastopp b) 53 1024 eq_refl eq_refl))
    end
  in
  Just new_x_ab.

Transparent Float.cmp.

Lemma backward_zoffloat_correct :
  forall x res res_ab, res ∈ γ res_ab ->
    ZofB x = Some res ->
    x ∈ γ (backward_zoffloat res_ab).
Proof.
  intros. unfold backward_zoffloat. destruct res_ab as [|[]].
  - destruct x as [| | |[]]; try discriminate; split; try reflexivity;
      unfold Fleb, Float.cmp, Bcompare, binary_overflow, overflow_to_inf, FF2B, negb;
      pose proof e0; apply andb_true_iff in H1; destruct H1; apply Z.leb_le in H2;
      unfold canonic_mantissa, FLT_exp in H1; apply Zeq_bool_eq in H1;
      assert (Z.pos (digits2_pos m) <= 53)%Z by (zify; omega);
      apply Zpower_le with (r:=radix2) in H3; simpl radix_val in H3;
      rewrite Zpos_digits2_pos in *; destruct (Zdigits_correct radix2 (Z.pos m));
      simpl Z.abs in *; simpl radix_val in *.
    + destruct (Z.compare_spec (1024-53) e); try reflexivity; try omega. simpl.
      fold (Pos.compare 9007199254740991 m).
      destruct (Pos.compare_spec 9007199254740991 m); try reflexivity; try (zify; omega).
      assert (2^53 <= Z.pos m)%Z. unfold Zpower, Z.pow_pos. simpl. zify; omega.
      apply Zdigits_gt_Zpower with (beta:=radix2) (x:=Z.pos m) in H8. zify; omega.
    + destruct (Z.compare_spec e (1024-53)); try reflexivity; try omega.
      rewrite <- Pos.compare_cont_antisym with (c:=Eq). simpl.
      fold (Pos.compare 9007199254740991 m).
      destruct (Pos.compare_spec 9007199254740991 m); try reflexivity; try (zify; omega).
      assert (2^53 <= Z.pos m)%Z. unfold Zpower, Z.pow_pos. simpl. zify; omega.
      apply Zdigits_gt_Zpower with (beta:=radix2) (x:=Z.pos m) in H8. zify; omega.
  - destruct H; split.
    eapply half_backward_zoffloat_correct; eauto. reflexivity.
    rewrite <- fneg_decr. fastunwrap.
    replace (Float.neg (Float.neg (half_backward_zoffloat (-z0)%Z 53 1024 eq_refl eq_refl)))
    with (half_backward_zoffloat (-z0)%Z 53 1024 eq_refl eq_refl).
    apply half_backward_zoffloat_correct with (i:=Z.opp res). reflexivity.
    destruct x; inv H0.
    reflexivity.
    simpl. destruct e, b; inv H3; try reflexivity.
    destruct Z.pow_pos; reflexivity.
    destruct Z.pow_pos; reflexivity.
    rewrite Zopp_involutive; reflexivity.
    omega.
    unfold Float.neg.
    rewrite Bopp_involutive. auto.
    unfold half_backward_zoffloat.
    destruct Zfastleb. 2:apply binary_normalize_is_nan.
    pose proof (binary_normalize_is_nan 53 1024 eq_refl eq_refl (-z0 - 1) 0 false mode_DN).
    unfold next_ulp. rewrite is_nan_FF2B. simpl in *.
    destruct binary_normalize as [|[]| |[]]; try discriminate; try reflexivity; simpl;
    repeat match goal with |- context [if ?b then _ else _] => destruct b eqn:? end;
    reflexivity.
Qed.

Definition backward_le_l (y:fitv+⊤) : fitv :=
  let My := match y with
            | All => B754_infinity false
            | Just (FITV _ My) => My
            end in
  FITV (B754_infinity true) My.

Lemma backward_le_l_correct :
  forall x y y_ab, y ∈ γ y_ab ->
    Fleb x y = true ->
    x ∈ γ (backward_le_l y_ab).
Proof.
  intros.
  split. destruct x as [|[]| |[]]; try discriminate; now auto.
  destruct y_ab as [|[]]; simpl.
  destruct x as [|[]| |[]]; try discriminate; now auto.
  eapply Fleb_trans. eauto. apply H.
Qed.

Definition backward_eq_l (x y:fitv+⊤) (res:bool) : fitv+⊤+⊥ :=
  if res then
    Just (backward_le_l y) ⊓ forward_fneg (Just (backward_le_l (forward_fneg y)))
  else
    match y with
    | All => NotBot All
    | Just (FITV my My) =>
      if Fleb My my then
        match x with
        | All => NotBot All
        | Just (FITV mx Mx) =>
          if Float.cmp Ceq my mx then
            if Fleb Mx mx then Bot
            else NotBot (Just (FITV (next_ulp 53 1024 eq_refl eq_refl mx) (B754_infinity false)))
          else
            if Float.cmp Ceq my Mx then
              NotBot (Just (FITV (B754_infinity true)
                                 (Float.neg (next_ulp 53 1024 eq_refl eq_refl (Float.neg Mx)))))
            else NotBot All
        end
      else NotBot All
    end.

Lemma backward_eq_l_correct :
  forall x x_ab, x ∈ γ x_ab ->
  forall y y_ab, y ∈ γ y_ab ->
  forall res, Float.cmp Ceq x y = res ->
    x ∈ γ (backward_eq_l x_ab y_ab res).
Proof.
  intros. unfold backward_eq_l. destruct res.
  - apply meet_correct. split.
    + eapply backward_le_l_correct. eauto.
      unfold Fleb. unfold Float.cmp in H1. destruct Bcompare as [[]|]; auto.
    + replace x with (Float.neg (Float.neg x)) by (destruct x as [[]|[]|[]|[]]; auto).
      apply forward_fneg_correct. eapply backward_le_l_correct.
      apply forward_fneg_correct, H0.
      rewrite fneg_decr. rewrite <- Float.cmp_swap in H1.
      unfold Fleb. unfold Float.cmp in H1. simpl in H1.
      destruct Bcompare as [[]|]; auto.
  - destruct x_ab as [|[]], y_ab as [|[]]. auto. destruct @Fleb; auto. auto.
    assert (forall (a b:float), Fleb a b = true -> Fleb b a = true -> Bcompare _ _ a b = Some Eq).
    { unfold Fleb. intros. rewrite Bcompare_swap in H3.
      destruct Bcompare as [[]|]; auto; discriminate. }
    destruct (Fleb f2 f1) eqn:?. 2:exact I.
    assert (Bcompare _ _ x y = Some Eq -> False).
    { simpl in H1. intro. rewrite H3 in H1. discriminate. }
    clear H1.
    destruct (Float.cmp Ceq f1 f) eqn:?. 2:destruct (Float.cmp Ceq f1 f0) eqn:?.
    + assert (Fleb y x = true).
      { eapply Fleb_trans, Fleb_trans, Fleb_trans. apply H0. apply Heqb. 2:apply H.
        unfold Fleb. unfold Float.cmp in Heqb0. destruct (Bcompare _ _ f1 f) as [[]|]; auto. }
      edestruct (next_ulp_lub 53 1024 eq_refl eq_refl x f) as [LUB|LUB]. reflexivity.
      destruct H, x; auto. destruct H, f; auto.
      * destruct H3. eapply Bcompare_trans, Bcompare_trans. 2:apply H2, H; auto.
        4:eapply H2, Fleb_trans, Heqb; apply H0.
        destruct f, H; now auto. destruct f1, H0; now auto.
        rewrite Bcompare_swap. simpl in Heqb0. destruct Bcompare as [[]|]; auto; discriminate.
      * destruct (Fleb f0 f) eqn:?. apply H3.
        eapply Bcompare_trans, Bcompare_trans. 2:eapply H2, H; eapply Fleb_trans, Heqb1; apply H.
        4:eapply H2, Fleb_trans, Heqb; apply H0.
        destruct f, H; now auto. destruct f1, H0; now auto.
        rewrite Bcompare_swap. simpl in Heqb0. destruct (Bcompare _ _ f1 f) as [[]|]; auto; discriminate.
        split. auto. destruct x as [|[]| |[]]; auto. destruct y as [|[]| |[]]; discriminate.
    + split. destruct H, x as [|[]| |]; now auto.
      replace x with (Float.neg (Float.neg x)) by (destruct H, x as [[]|[]|[]|[]]; auto).
      rewrite fneg_decr.
      edestruct (next_ulp_lub 53 1024 eq_refl eq_refl (Float.neg x) (Float.neg f0)) as [LUB|LUB].
      reflexivity. 4:now auto.
      destruct H, x as [|[]| |]; auto. destruct f1 as [|[]| |[]], f0 as [|[]| |]; now auto.
      destruct H3. rewrite fneg_decr in LUB.
      eapply Bcompare_trans, Bcompare_trans. 2:eapply H2, LUB; apply H.
      4:eapply H2, Fleb_trans, Heqb; apply H0.
      destruct f0, H; now auto. destruct f1, H0; now auto.
      rewrite Bcompare_swap. simpl in Heqb1. destruct (Bcompare _ _ f1 f0) as [[]|]; auto; discriminate.
    + exact I.
Qed.

Definition backward_lt_l (y:fitv+⊤) : fitv :=
  let My := match y with
            | All => B754_infinity false
            | Just (FITV _ My) => My
            end in
  FITV (B754_infinity true)
       (Float.neg (next_ulp 53 1024 eq_refl eq_refl (Float.neg My))).

Lemma backward_lt_l_correct :
  forall x y y_ab, y ∈ γ y_ab ->
    Float.cmp Clt x y = true ->
    x ∈ γ (backward_lt_l y_ab).
Proof.
  intros.
  split. destruct x as [|[]| |[]]; try discriminate; now auto.
  replace x with (Float.neg (Float.neg x)) by
    (destruct x as [[]|[]| |[]]; try discriminate; now auto).
  rewrite fneg_decr.
  edestruct next_ulp_lub as [LUB|LUB]. 5:apply LUB.
  - reflexivity.
  - destruct x; auto.
  - destruct y_ab as [|[]]. auto.
    destruct f0, H; auto. destruct y as [|[]| |[]]; discriminate.
  - exfalso. rewrite fneg_decr in LUB. destruct y_ab as [|[]].
    + destruct x as [|[]| |], y as [|[]| |]; discriminate.
    + eapply Fleb_trans with (f2:=f0) in LUB. 2:apply H.
      rewrite <- Float.cmp_swap in H0. simpl in H0. unfold Fleb in LUB.
      destruct Bcompare as [[]|]; discriminate.
Qed.

Definition backward_not_ge_l (x y:fitv+⊤) : fitv+⊤ :=
  match x, y with
  | Just _, Just _ => Just (backward_lt_l y)
  | _, _ => All
  end.

Lemma backward_not_ge_l_correct :
  forall x x_ab, x ∈ γ x_ab ->
  forall y y_ab, y ∈ γ y_ab ->
    Fleb y x = false ->
    x ∈ γ (backward_not_ge_l x_ab y_ab).
Proof.
  destruct x_ab as [|[]], y_ab as [|[]]; intros; try auto.
  eapply backward_lt_l_correct. eauto.
  rewrite <- Float.cmp_swap. unfold Fleb in H1. simpl.
  pose proof Bcompare_nan _ _ y x. destruct Bcompare as [[]|]; auto.
  destruct H2. destruct H0, y; auto. destruct H, x; auto. auto.
Qed.

Definition backward_not_gt_l (x y:fitv+⊤) : fitv+⊤ :=
  match x, y with
  | Just _, Just _ => Just (backward_le_l y)
  | _, _ => All
  end.

Lemma backward_not_gt_l_correct :
  forall x x_ab, x ∈ γ x_ab ->
  forall y y_ab, y ∈ γ y_ab ->
    Float.cmp Cgt x y = false ->
    x ∈ γ (backward_not_gt_l x_ab y_ab).
Proof.
  destruct x_ab as [|[]], y_ab as [|[]]; intros; try auto.
  eapply backward_le_l_correct. eauto.
  unfold Fleb. simpl in H1.
  pose proof Bcompare_nan _ _ x y. destruct Bcompare as [[]|]; auto.
  destruct H2. destruct H, x; auto. destruct H0, y; auto. auto.
Qed.

Definition backward_cmpf_l (c:comparison) (x y:fitv+⊤) (res:bool) : fitv+⊤+⊥ :=
  match c, res with
  | Ceq, _ => backward_eq_l x y res
  | Cne, _ => backward_eq_l x y (negb res)
  | Cle, true =>
    NotBot (Just (backward_le_l y))
  | Cge, false =>
    NotBot (backward_not_ge_l x y)
  | Cge, true =>
    NotBot (forward_fneg (Just (backward_le_l (forward_fneg y))))
  | Cle, false =>
    NotBot (forward_fneg (backward_not_ge_l (forward_fneg x) (forward_fneg y)))
  | Clt, true =>
    NotBot (Just (backward_lt_l y))
  | Cgt, true =>
    NotBot (forward_fneg (Just (backward_lt_l (forward_fneg y))))
  | Cgt, false =>
    NotBot (backward_not_gt_l x y)
  | Clt, false =>
    NotBot (forward_fneg (backward_not_gt_l (forward_fneg x) (forward_fneg y)))
  end.

Lemma Bcompare_fneg:
  ∀ x y:float, Bcompare _ _ x y = Bcompare _ _ (Float.neg y) (Float.neg x).
Proof.
  intros. destruct x as [[]|[]| |[]], y as [[]|[]| |[]]; simpl; auto;
  rewrite <- Zcompare_antisym; destruct Z.compare; auto;
  rewrite Pos.compare_cont_antisym; auto.
Qed.

Lemma backward_cmpf_l_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y y_ab, y ∈ γ y_ab ->
  ∀ c res, Float.cmp c x y = res ->
    x ∈ γ (backward_cmpf_l c x_ab y_ab res).
Proof.
  intros. unfold backward_cmpf_l.
  destruct c, res.
  - eapply backward_eq_l_correct; eauto.
  - eapply backward_eq_l_correct; eauto.
  - eapply backward_eq_l_correct; eauto.
    rewrite Float.cmp_ne_eq in H1. destruct Float.cmp; auto.
  - eapply backward_eq_l_correct; eauto.
    rewrite Float.cmp_ne_eq in H1. destruct Float.cmp; auto.
  - eapply backward_lt_l_correct; eauto.
  - replace x with (Float.neg (Float.neg x)) by (destruct x as [[]|[]|[]|[]]; auto).
    eapply forward_fneg_correct, backward_not_gt_l_correct. apply forward_fneg_correct, H.
    apply forward_fneg_correct, H0. simpl in *. rewrite <- Bcompare_fneg, Bcompare_swap.
    destruct Bcompare as [[]|]; auto.
  - eapply backward_le_l_correct. eauto. simpl in H1. unfold Fleb. destruct Bcompare as [[]|]; auto.
  - replace x with (Float.neg (Float.neg x)) by (destruct x as [[]|[]|[]|[]]; auto).
    eapply forward_fneg_correct, backward_not_ge_l_correct.
    apply forward_fneg_correct, H. apply forward_fneg_correct, H0.
    rewrite fneg_decr. auto.
  - replace x with (Float.neg (Float.neg x)) by (destruct x as [[]|[]|[]|[]]; auto).
    eapply forward_fneg_correct, backward_lt_l_correct. apply forward_fneg_correct, H0.
    simpl in *. rewrite <- Bcompare_fneg, Bcompare_swap. destruct Bcompare as [[]|]; auto.
  - eapply backward_not_gt_l_correct; eauto.
  - replace x with (Float.neg (Float.neg x)) by (destruct x as [[]|[]|[]|[]]; auto).
    eapply forward_fneg_correct, backward_le_l_correct. apply forward_fneg_correct, H0.
    unfold Fleb. rewrite <- Bcompare_fneg, Bcompare_swap. simpl in H1. destruct Bcompare as [[]|]; auto.
  - eapply backward_not_ge_l_correct. eauto. eauto.
    simpl in H1. unfold Fleb. rewrite Bcompare_swap. destruct Bcompare as [[]|]; auto.
Qed.

Definition backward_absf (res_ab:fitv+⊤) : fitv+⊤+⊥ :=
  match res_ab with
  | All => NotBot All
  | Just (FITV _ _) =>
    do res_ab' <- res_ab ⊓ (Just (FITV (B754_zero false) (B754_infinity false)));
    forward_fneg res_ab' ⊔ res_ab'
  end.

Lemma backward_absf_correct :
  forall x res_ab, Float.abs x ∈ γ res_ab ->
    x ∈ γ (backward_absf res_ab).
Proof.
Transparent Float.abs.
  intros.
  destruct res_ab as [|[]]. apply H.
  eapply botbind_spec with (_:float).
  2:eapply meet_correct; split; eauto.
  intros. apply join_correct.
  destruct x as [|[]| |[]].
  right. destruct a; apply H0.
  left. apply forward_fneg_correct in H0. apply H0.
  right. apply H0.
  destruct H. discriminate.
  left. apply forward_fneg_correct in H0. apply H0.
  right. apply H0.
  destruct x as [|[]| |[]]; try (split; reflexivity).
  destruct H. discriminate.
Qed.

Definition backward_addf_l (res y:fitv+⊤) : fitv+⊤+⊥ :=
  match y with
  | All => NotBot All
  | Just (FITV my My) =>
    match res with
    | All => NotBot All
    | Just res =>
      let 'FITV mres Mres := backward_round res in
      let m:= Bminus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_pl mode_UP mres My in
      let M:= Bminus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_pl mode_DN Mres my in
      if is_nan m || is_nan M then NotBot All
      else NotBot (Just (FITV m M))
    end
  end.

Lemma backward_addf_l_correct:
  ∀ x y y_ab, y ∈ γ y_ab ->
  ∀ res_ab, (Float.add x y)%Z ∈ γ res_ab ->
    x ∈ γ (backward_addf_l res_ab y_ab).
Proof.
  intros.
  destruct y_ab as [|[]]; auto. destruct H. simpl.
  destruct res_ab as [|res_ab]; auto.
  Transparent Float.add. unfold Float.add in H1.
  destruct (is_finite x && is_finite y) eqn:?.
  - rewrite Bool.andb_true_iff in Heqb. destruct Heqb.
    pose proof backward_round_correct (x + y)
         (Bplus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_pl mode_NE x y).
    refine (let H4 := H4 _ _ H0 in _).
    { clear H4. use_float_specs.
      destruct Rlt_bool. intuition.
      destruct H4; auto. rewrite H4. f_equal.
      destruct (Rlt_bool_spec (x + y) 0);
      destruct x as [[]| | |[]], y as [[]| | |[]]; try discriminate;
      try reflexivity; simpl in *; try Psatz.lra.
      pose proof (F2R_gt_0_compat radix2 {| Fnum := Z.pos m; Fexp := e |} eq_refl);
        pose proof (F2R_gt_0_compat radix2 {| Fnum := Z.pos m0; Fexp := e1 |} eq_refl);
        Psatz.lra.
      pose proof (F2R_lt_0_compat radix2 {| Fnum := Z.neg m; Fexp := e |} eq_refl);
        pose proof (F2R_lt_0_compat radix2 {| Fnum := Z.neg m0; Fexp := e1 |} eq_refl);
        Psatz.lra. }
    clear H4.
    destruct backward_round; auto.
    destruct (is_nan (Bminus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_pl mode_UP f1 f0)) eqn:?,
             (is_nan (Bminus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_pl mode_DN f2 f)) eqn:?;
             try exact I.
    simpl in H5. unfold gammaR, RF_lt, RFF_lt, Float.neg in H5.
    rewrite !is_finite_FF_B2FF, !FF2R_B2FF, is_finite_Bopp, B2R_Bopp in H5.
    split.
    + destruct (is_finite f1) eqn:?. destruct (is_finite f0) eqn:?.
      * destruct H5.
        rewrite Fleb_Rle in H1 by auto. Rle_bool_case H1; [|discriminate]. simpl.
        assert (f1 - f0 <= x) by Psatz.lra.
        use_float_specs.
        unfold Z.compare, Pos.compare, Pos.compare_cont in H9.
        Rlt_bool_case H9.
        destruct H9 as [? []]; auto. rewrite Fleb_Rle by auto. apply Rle_bool_true.
        rewrite H9.
        apply round_le_generic; auto. apply generic_format_B2R; auto.
        destruct H9, Bminus as [|[]| |], (Bsign f1) eqn:?; auto; try discriminate.
        edestruct RIneq.Rle_not_lt. apply H10.
        rewrite Rabs_pos_eq. eapply Rle_lt_trans. apply round_le; eauto using Rlt_le.
        rewrite round_generic by (auto; apply generic_format_B2R).
        eapply Rle_lt_trans. apply Rle_abs. apply abs_B2R_lt_emax.
        eapply round_ge_generic; eauto. apply generic_format_0.
        assert (0 <= f1).
        { destruct f1 as [| | |[]]; try discriminate. apply Rle_refl.
          apply F2R_ge_0_compat. compute; discriminate. }
        assert (f0 <= 0).
        { destruct f0 as [| | |[]]; try discriminate. apply Rle_refl.
          apply F2R_le_0_compat. compute; discriminate. }
        Psatz.lra.
        inv H9.
        destruct (next_ulp_lub 53 1024 eq_refl eq_refl x (B754_infinity true) eq_refl).
        destruct x; try reflexivity; discriminate.
        reflexivity.
        destruct x as [| | |[]]; try discriminate.
        auto.
      * assert (is_nan f0 = false) by eauto.
        destruct f0; try discriminate.
        destruct b. destruct y as [| | |[]]; try discriminate.
        destruct f1, x; try discriminate; reflexivity.
      * destruct H5. destruct f1 as [|[]|? []|]; inv H5.
        destruct f0 as [|[]| |], x; try discriminate; try reflexivity.
    + destruct (is_finite f) eqn:?. destruct (is_finite f2) eqn:?.
      * destruct H5.
        rewrite Fleb_Rle in H by auto. Rle_bool_case H; [|discriminate].
        assert (x <= f2 - f) by Psatz.lra.
        use_float_specs.
        unfold Z.compare, Pos.compare, Pos.compare_cont in H9.
        Rlt_bool_case H8.
        destruct H8 as [? []]; auto. rewrite Fleb_Rle by auto. apply Rle_bool_true.
        rewrite H8.
        apply round_ge_generic; auto. apply generic_format_B2R; auto.
        clear Heqb.
        destruct H8, Bminus as [|[]| |], (Bsign f2) eqn:?; auto; try discriminate.
        edestruct RIneq.Rle_not_lt. apply H10.
        rewrite Rabs_left1. eapply Rle_lt_trans. apply Ropp_le_contravar.
        apply round_le; eauto.
        rewrite round_generic by (auto; apply generic_format_B2R).
        eapply Rle_lt_trans. apply Rle_abs. rewrite Rabs_Ropp. apply abs_B2R_lt_emax.
        eapply round_le_generic; eauto. apply generic_format_0.
        assert (0 <= f).
        { destruct f as [| | |[]]; try discriminate. apply Rle_refl.
          apply F2R_ge_0_compat. compute; discriminate. }
        assert (f2 <= 0).
        { destruct f2 as [| | |[]]; try discriminate. apply Rle_refl.
          apply F2R_le_0_compat. compute; discriminate. }
        Psatz.lra.
        inv H8. rewrite <- fneg_decr.
        destruct (next_ulp_lub 53 1024 eq_refl eq_refl (Float.neg x) (B754_infinity true) eq_refl).
        destruct x; try reflexivity; discriminate.
        reflexivity.
        destruct x as [| | |[]]; try discriminate.
        auto.
      * destruct H5. destruct f2 as [|[]|? []|]; inv H4.
        destruct f, x as [| | |[]]; try discriminate; try reflexivity.
      * assert (is_nan f = false) by eauto.
        destruct f; try discriminate.
        destruct b.
        destruct f2 as [|[]| |], x as [| | |[]]; try discriminate; reflexivity.
        destruct y as [| | |[]]; try discriminate.
  - destruct (backward_round res_ab) eqn:?. auto.
    destruct (is_nan (Bminus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_pl mode_UP f1 f0)) eqn:?,
             (is_nan (Bminus 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_pl mode_DN f2 f)) eqn:?;
             try exact I.
    destruct res_ab; inv Heqf1. destruct H0. split.
    + destruct x as [|[]| |];
      try
        (destruct y as [|[]| |]; try discriminate;
          match goal with |- context [Bminus _ _ _ _ _ _ ?f3' _] =>
            destruct f3' as [|[]| |] eqn:?; try reflexivity; try discriminate end;
          destruct f0 as [|[]| |], f3 as [|[]| |[]];
          try reflexivity; discriminate).
      match goal with |- context [Fleb ?m _] => destruct m as [|[]| |[]] end;
        try discriminate; reflexivity.
    + destruct x as [|[]| |[]];
      try
        (destruct y as [|[]| |]; try discriminate;
         match goal with |- context [Bminus _ _ _ _ _ _ ?f4' _] =>
           destruct f4' as [|[]| |] eqn:?; try reflexivity; try discriminate end;
         destruct f as [|[]| |[]], f4 as [|[]| |];
         try reflexivity; discriminate).
      match goal with |- context [Fleb _ ?m] => destruct m as [|[]| |[]] end;
        try discriminate; reflexivity.
Qed.

Definition backward_addf_r := backward_addf_l.

Lemma backward_addf_r_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y res_ab, (Float.add x y)%Z ∈ γ res_ab ->
    y ∈ γ (backward_addf_r res_ab x_ab).
Proof.
  intros. eapply backward_addf_l_correct; eauto.
  unfold Float.add. rewrite fadd_commut.
  destruct res_ab, x as [|[]| |], y as [|[]| |]; apply H0.
Qed.

Definition backward_subf_l (res y:fitv+⊤) : fitv+⊤+⊥ := backward_addf_l res (forward_fneg y).

Lemma backward_subf_l_correct:
  ∀ x y y_ab, y ∈ γ y_ab ->
  ∀ res_ab, (Float.sub x y)%Z ∈ γ res_ab ->
    x ∈ γ (backward_subf_l res_ab y_ab).
Proof.
  intros. eapply backward_addf_l_correct; eauto.
  eapply forward_fneg_correct. eauto.
  destruct res_ab, x, y; apply H0.
Qed.

Definition backward_subf_r (res x:fitv+⊤) : fitv+⊤+⊥ :=
  fmap forward_fneg (backward_addf_l res x).

Lemma backward_subf_r_correct:
  ∀ x x_ab, x ∈ γ x_ab ->
  ∀ y res_ab, (Float.sub x y)%Z ∈ γ res_ab ->
    y ∈ γ (backward_subf_r res_ab x_ab).
Proof.
  intros.
  eapply botbind_spec with (Float.neg y:float).
  2:eapply backward_addf_r_correct; eauto.
  intros. apply forward_fneg_correct in H1.
  destruct forward_fneg, y as [|[]| |[]]; try apply H1.
  destruct res_ab, x, y; apply H0.
Qed.

Definition binary32offloat_DN (f: float) : binary32 :=
  Bconv 53 1024 24 128 eq_refl eq_refl Float.to_single_pl mode_DN f.

Lemma binary32offloat_DN_Fleb :
  ∀ f1 f2,
    Fleb (Float.of_single f1) f2 = true ->
    Fleb f1 (binary32offloat_DN f2) = true.
Proof.
  intros. unfold binary32offloat_DN.
  destruct (floatofsingle_exact f1).
  assert (is_nan f2 = false) by eauto.
  assert (is_nan f1 = false).
  { destruct f1; try reflexivity; discriminate. }
  destruct (is_finite f2) eqn:?.
  - use_float_specs. specialize (H4 Heqb).
    Rlt_bool_case H4.
    + destruct H4 as (? & ? & ?); auto.
      destruct (is_finite f1) eqn:?.
      * rewrite Fleb_Rle in * by auto. apply Rle_bool_true. rewrite H4.
        Rle_bool_case H. 2:discriminate.
        apply round_ge_generic; auto using generic_format_B2R.
        rewrite <- H0. auto.
      * destruct f1 as [|[]| |]; try discriminate; try reflexivity.
        destruct Bconv; try discriminate; reflexivity.
        destruct f2; discriminate.
    + destruct f2; try discriminate.
      rewrite round_0, Rabs_R0 in H5 by auto. apply RIneq.Rle_not_lt in H5. destruct H5. apply bpow_gt_0.
      destruct b.
      * destruct (is_finite f1) eqn:?.
        rewrite Rabs_left1 in H5. rewrite Fleb_Rle in H by auto. Rle_bool_case H; [|discriminate].
        rewrite H0 in H6.
        eapply round_ge_generic with (rnd:=round_mode mode_DN) in H6.
        4:apply generic_format_B2R. 2:auto. 2:auto.
        destruct (Rabs_lt_inv _ _ (abs_B2R_lt_emax _ _ f1)).
        Psatz.lra.
        erewrite <- round_0. apply round_le. auto. auto. apply F2R_le_0_compat. compute. discriminate. auto.
        destruct f1 as [|[]| |]; try discriminate.
        destruct Bconv as [|[]|?[]|]; try discriminate. reflexivity.
      * destruct Bconv as [| |?[]|]; inv H4.
        destruct f1 as [|[]| |]; try discriminate; try reflexivity.
        unfold Fleb, Bcompare. destruct b. auto. clear H H0 H1 H3.
        unfold Fappli_IEEE.bounded in e3. rewrite Bool.andb_true_iff in e3. destruct e3.
        apply Zle_is_le_bool in H0.
        destruct (Z.compare_spec e1 104). 3:omega. 2:auto.
        rewrite Pos.compare_cont_spec. destruct (Pos.compare_spec m0 16777215); try discriminate.
        auto. auto.
        subst e1. apply canonic_canonic_mantissa with (sx:=false) in H.
        unfold canonic, canonic_exp, FLT_exp in H.
        rewrite ln_beta_F2R in H. 2:discriminate. simpl in H.
        assert (bpow radix2 24 <= P2R m0).
        { rewrite <- Z2R_Zpower by omega. apply Z2R_le with (n:=Z.pos m0).
          change (radix2 ^ 24)%Z with 16777216%Z. zify; omega. }
        apply ln_beta_le with (r:=radix2) in H1. 2:apply bpow_gt_0.
        rewrite ln_beta_bpow in H1. zify; omega.
  - destruct f2 as [|[]| |]; try discriminate.
    + destruct (Float.of_single f1) as [|[]| |]eqn:?; try discriminate.
      destruct f1 as [|[]| |]; try discriminate; try reflexivity.
      discriminate (H1 eq_refl).
      destruct b, f1 as [|[]| |]; discriminate.
    + destruct f1 as [|[]| |[]]; try reflexivity. discriminate.
Qed.

Definition backward_round_single (x:fitv) : fitv :=
  let 'FITV mx Mx := x in
  FITV (Float.neg (Float.of_single
                     (next_ulp 24 128 eq_refl eq_refl (binary32offloat_DN (Float.neg mx)))))
       (Float.of_single (next_ulp 24 128 eq_refl eq_refl (binary32offloat_DN Mx))).

Lemma backward_round_single_correct :
  forall x_r (x:float32),
    (if Rlt_bool
          (Rabs (round radix2 (FLT_exp (3 - 128 - 24) 24)
                       (round_mode mode_NE) x_r))
          (bpow radix2 128)
     then (x:R) = round radix2 (FLT_exp (3 - 128 - 24) 24) (round_mode mode_NE) x_r /\
          is_finite x = true
     else (x:full_float) = binary_overflow 24 128 mode_NE (Rlt_bool x_r 0)) ->
  forall x_ab, (Float.of_single x) ∈ γ x_ab ->
  gammaR (backward_round_single x_ab) x_r.
Proof.
  intros.
  destruct x_ab; destruct H0; try easy.
  apply binary32offloat_DN_Fleb in H1.
  rewrite <- fneg_decr in H0.
  Transparent Float.neg Float32.neg Float.of_single.
  assert (Float.neg (Float.of_single x) = Float.of_single (Float32.neg x))
    by (apply Bconv_Bopp; auto).
  rewrite H2 in H0.
  apply binary32offloat_DN_Fleb in H0.
  split.
  - eapply (next_ulp_round_overflow 24 128 eq_refl eq_refl) in H; eauto. 2:reflexivity.
    unfold RF_lt, RFF_lt in *. rewrite FF2R_B2FF, is_finite_FF_B2FF in *.
    assert (is_finite (next_ulp 24 128 eq_refl eq_refl (binary32offloat_DN f0)) =
            is_finite (Float.of_single
                         (next_ulp 24 128 eq_refl eq_refl (binary32offloat_DN f0)))).
    { destruct next_ulp; try reflexivity. rewrite (proj2 (floatofsingle_exact _)); auto. }
    rewrite <- H3. clear H3.
    destruct @is_finite. rewrite (proj1 (floatofsingle_exact _)). auto.
    destruct next_ulp as [| |? []|]; inv H. reflexivity.
  - apply (next_ulp_round_overflow 24 128 eq_refl eq_refl) with (x:=-x_r) (mode:=mode_NE) in H0.
    2:reflexivity.
    unfold RF_lt, RFF_lt in *. rewrite FF2R_B2FF, is_finite_FF_B2FF in *.
    assert (is_finite (next_ulp 24 128 eq_refl eq_refl (binary32offloat_DN (Float.neg f))) =
            is_finite (Float.neg (Float.neg
                        (Float.of_single
                           (next_ulp 24 128 eq_refl eq_refl
                                     (binary32offloat_DN (Float.neg f))))))).
    { destruct next_ulp; try reflexivity.
      unfold Float.neg. rewrite !is_finite_Bopp, (proj2 (floatofsingle_exact _)); auto. }
    rewrite <- H3. clear H3.
    clear H. destruct @is_finite.
    unfold Float.neg at 1 2. rewrite !B2R_Bopp, (proj1 (floatofsingle_exact _)).
    rewrite Ropp_involutive. auto.
    destruct next_ulp as [| |? []|]; inv H0. reflexivity.
    rewrite round_NE_opp, Rabs_Ropp. unfold round_mode in H.
    Rlt_bool_case H.
    destruct H. unfold Float32.neg. rewrite B2R_Bopp, is_finite_Bopp. split. f_equal. auto. auto.
    assert (x_r <> 0).
    { intro. subst x_r. rewrite round_0, Rabs_R0 in H3. 2:apply (valid_rnd_round_mode mode_NE).
      pose proof (bpow_gt_0 radix2 128). Psatz.lra. }
    assert (Rlt_bool (- x_r) 0 = negb (Rlt_bool x_r 0)).
    { destruct (Rcompare_spec x_r 0).
      rewrite Rlt_bool_false, Rlt_bool_true by Psatz.lra. auto.
      congruence.
      rewrite Rlt_bool_true, Rlt_bool_false by Psatz.lra. auto. }
    rewrite H5.
    destruct x as [| |? []|]; inv H. reflexivity.
Qed.

Definition backward_singleoffloat (res_ab:fitv+⊤) : fitv+⊤+⊥ :=
  match res_ab with
  | All => NotBot All
  | Just res_ab => NotBot (Just (backward_round_single res_ab))
  end.

Lemma backward_singleoffloat_correct :
  forall x res_ab, Float.of_single (Float.to_single x) ∈ γ res_ab ->
    x ∈ γ (backward_singleoffloat res_ab).
Proof.
  intros. destruct res_ab as [|res_ab]. auto.
  unfold backward_singleoffloat. destruct (is_finite x) eqn:?.
  - eapply backward_round_single_correct with (x_r := x) in H.
    destruct backward_round_single. destruct H.
    split.
    + unfold RF_lt, RFF_lt, Float.neg in H0.
      rewrite is_finite_FF_B2FF, FF2R_B2FF, is_finite_Bopp in H0.
      destruct (is_finite f) eqn:?.
      rewrite Fleb_Rle by auto. apply Rle_bool_true. rewrite B2R_Bopp in H0. Psatz.lra.
      destruct f as [|[]|? []|]; inv H0. destruct x; try discriminate; reflexivity.
    + unfold RF_lt, RFF_lt in H.
      rewrite is_finite_FF_B2FF, FF2R_B2FF in H.
      destruct (is_finite f0) eqn:?.
      rewrite Fleb_Rle by auto. apply Rle_bool_true. Psatz.lra.
      destruct f0 as [| |? []|]; inv H. destruct x as [|[]| |[]]; try discriminate; reflexivity.
    + Transparent Float.to_single. unfold Float.to_single.
      use_float_specs. specialize (H0 Heqb).
      Rlt_bool_case H0. now intuition.
      rewrite <- Bsign_pos0. auto.
      destruct x; try discriminate; reflexivity.
  - destruct res_ab. auto. destruct H. split.
    + assert (is_nan
                (Float.of_single
                   (next_ulp 24 128 eq_refl eq_refl
                             (binary32offloat_DN (Float.neg f)))) = false).
      { apply floatofsingle_nan, next_ulp_is_nan.
        destruct f; try reflexivity; try discriminate.
        apply binary_normalize_is_nan. }
      destruct x as [|[]| |], f as [|[]| |]; try discriminate; try reflexivity.
      destruct b; discriminate.
      clear - H1. destruct Float.of_single as [|[]| |[]]; try reflexivity; discriminate.
    + assert (is_nan
                (Float.of_single
                   (next_ulp 24 128 eq_refl eq_refl (binary32offloat_DN f0))) = false).
      { apply floatofsingle_nan, next_ulp_is_nan.
        apply Fleb_nan_r in H0.
        destruct f0; try reflexivity. discriminate.
        apply binary_normalize_is_nan. }
      destruct x as [|[]| |], f0 as [|[]| |]; try discriminate; try reflexivity.
      clear - H1. destruct Float.of_single as [|[]| |[]]; try reflexivity; discriminate.
Qed.

Definition backward_singleofz (res_ab:fitv+⊤) (x_ab:zitv+⊤) : zitv+⊤+⊥ :=
  match res_ab with
  | All => NotBot x_ab
  | Just res_ab =>
    let 'FITV mx Mx := backward_round_single res_ab in
    let low :=
      match Zoffloat_DN (Float.neg mx), x_ab with
      | Some m, Just (ZITV m' _) => Some (Zfastmax (Zfastopp m) m')
      | Some m, All => Some (Zfastopp m)
      | None, Just (ZITV m' _) => Some (m')
      | None, All => None
      end
    in
    let high :=
      match Zoffloat_DN Mx, x_ab with
      | Some M, Just (ZITV _ M') => Some (Zfastmin M M')
      | Some M, All => Some (M:Zfast)
      | None, Just (ZITV _ M') => Some (M')
      | None, All => None
      end
    in
    match low, high with
    | Some m, Some M =>
      if Zfastleb m M then NotBot (Just (ZITV m M))
      else Bot
    | _, _ => NotBot All
    end
  end.

Lemma backward_singleofz_correct :
  forall x x_ab, x ∈ γ x_ab ->
  forall res_ab, Float.of_single (BofZ 24 128 (@eq_refl _ Lt) (@eq_refl _ Lt) x) ∈ γ res_ab ->
    x ∈ γ (backward_singleofz res_ab x_ab).
Proof.
  intros.
  unfold backward_singleofz. destruct res_ab as [|res_ab]. auto.
  assert (gammaR (backward_round_single res_ab) x).
  { eapply backward_round_single_correct; eauto.
    use_float_specs.
    destruct Rlt_bool. intuition.
    destruct (Z.ltb_spec x 0), (Rlt_bool_spec x 0); auto.
    apply (le_Z2R 0 x) in H3. omega.
    apply (lt_Z2R x 0) in H3. omega. }
  destruct backward_round_single.
  destruct H1. unfold RF_lt, RFF_lt, F2R, Fnum, Fexp, bpow in H1, H2.
  rewrite is_finite_FF_B2FF, FF2R_B2FF in H1, H2.
  assert (forall m, Zoffloat_DN (Float.neg f) = Some m -> (-m <= x)%Z).
  { pose proof (Zoffloat_DN_correct (Float.neg f)).
    destruct (Zoffloat_DN (Float.neg f)). 2:easy.
    destruct H3. rewrite H3 in H2. intros. injection H5. intro. subst z. clear H5.
    apply Zopp_le_cancel, le_Z2R. rewrite Zopp_involutive, H4.
    unfold round, scaled_mantissa, canonic_exp, Fcore_FIX.FIX_exp, F2R, Fexp, Fnum,
           scaled_mantissa, bpow, round_mode, Zopp at 2.
    rewrite !Rmult_1_r.
    apply Z2R_le, Zfloor_lub.
    rewrite Z2R_opp. Psatz.lra. }
  assert (forall M, Zoffloat_DN f0 = Some M -> (x <= M)%Z).
  { pose proof (Zoffloat_DN_correct f0).
    destruct (Zoffloat_DN f0). 2:easy.
    destruct H4. rewrite H4 in H1. intros. injection H6. intro. subst z. clear H6.
    apply le_Z2R. rewrite H5.
    unfold round, scaled_mantissa, canonic_exp, Fcore_FIX.FIX_exp, F2R, Fexp, Fnum,
           scaled_mantissa, bpow, round_mode, Zopp.
    rewrite !Rmult_1_r.
    apply Z2R_le, Zfloor_lub. Psatz.lra. }
  destruct (Zoffloat_DN (Float.neg f)); [specialize (H3 _ eq_refl)|clear H3];
    (destruct (Zoffloat_DN f0); [specialize (H4 _ eq_refl)|clear H4]);
  destruct x_ab as [|[]]; destruct H; auto; try exact I; fastunwrap.
  destruct (Z.leb_spec (-z) z0); [split|]; simpl in *; Psatz.lia.
  destruct (Z.leb_spec (Z.max (-z) z1) (Z.min z0 z2)); [split|]; simpl in *; Psatz.lia.
  destruct (Z.leb_spec (Z.max (-z) z0) z1); [split|]; simpl in *; Psatz.lia.
  destruct (Z.leb_spec z0 (Z.min z z1)); [split|]; simpl in *; Psatz.lia.
  destruct (Z.leb_spec z z0); [split|]; simpl in *; Psatz.lia.
Qed.