progress on lemmas

1 files changed, 81 insertions, 1 deletions

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index a76daab4..7e0e7260 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1174,7 +1174,7 @@ Proof.
   destruct Rcase_abs in ABS; lra.
 Qed.
 
-Theorem ZofB_ne_range:
+Theorem ZofB_ne_ball:
   forall f n, ZofB_ne f = Some n -> (IZR n-1/2 <= B2R _ _ f <= IZR n+1/2)%R.
 Proof.
   intros. rewrite ZofB_ne_correct in H. destruct (is_finite prec emax f) eqn:FIN; inversion H.
@@ -1183,6 +1183,86 @@ Proof.
   lra.
 Qed.
 
+(*
+Theorem ZofB_ne_minus:
+  forall minus_nan m f p q,
+  ZofB_ne f = Some p -> 0 <= p < 2*q -> q <= 2^prec -> (IZR q <= B2R _ _ f)%R ->
+  ZofB_ne (Bminus _ _ _ Hmax minus_nan m f (BofZ q)) = Some (p - q).
+Proof.
+  intros.
+  assert (Q: -2^prec <= q <= 2^prec).
+  { split; auto.  generalize (Zpower_ge_0 radix2 prec); simpl; lia. }
+  assert (RANGE: (IZR p -1/2 <= B2R _ _ f <= IZR p + 1/2)%R) by ( apply ZofB_ne_ball; auto ).    
+  rewrite ZofB_ne_correct in H. destruct (is_finite prec emax f) eqn:FIN; try discriminate.
+  assert (PQ2: (IZR p + 1 <= IZR q * 2)%R).
+  { l_IZR. apply IZR_le. lia. }
+  assert (EXACT: round radix2 fexp (round_mode m) (B2R _ _ f - IZR q)%R = (B2R _ _ f - IZR q)%R).
+  { apply round_generic. apply valid_rnd_round_mode.
+    apply sterbenz_aux. now apply FLT_exp_valid. apply FLT_exp_monotone. apply generic_format_B2R.
+    apply integer_representable_n. auto. lra. }
+  destruct (BofZ_exact q Q) as (A & B & C).
+  generalize (Bminus_correct _ _ _ Hmax minus_nan m f (BofZ q) FIN B).
+  rewrite Rlt_bool_true.
+- fold emin; fold fexp. intros (D & E & F).
+  rewrite ZofB_ne_correct. rewrite E. rewrite D. rewrite A. rewrite EXACT.
+  inversion H. f_equal.
+  rewrite ! Ztrunc_floor. apply Zfloor_minus.
+  lra. lra.
+- rewrite A. fold emin; fold fexp. rewrite EXACT.
+  apply Rle_lt_trans with (bpow radix2 prec).
+  apply Rle_trans with (IZR q). apply Rabs_le. lra.
+  rewrite <- IZR_Zpower. apply IZR_le; auto. red in prec_gt_0_; lia.
+  apply bpow_lt. auto.
+Qed.
+ *)
+
+Definition ZofB_ne_range (f: binary_float) (zmin zmax: Z): option Z :=
+  match ZofB_ne f with
+  | None => None
+  | Some z => if Z.leb zmin z && Z.leb z zmax then Some z else None
+  end.
+
+Theorem ZofB_ne_range_correct:
+  forall f min max,
+  let n := ZnearestE (B2R _ _ f) in
+  ZofB_ne_range f min max =
+  if is_finite _ _ f && Z.leb min n && Z.leb n max then Some n else None.
+Proof.
+  intros. unfold ZofB_ne_range. rewrite ZofB_ne_correct. fold n.
+  destruct (is_finite prec emax f); auto.
+Qed.
+
+Lemma ZofB_ne_range_inversion:
+  forall f min max n,
+  ZofB_ne_range f min max = Some n ->
+  min <= n /\ n <= max /\ ZofB_ne f = Some n.
+Proof.
+  intros. rewrite ZofB_ne_range_correct in H. rewrite ZofB_ne_correct.
+  destruct (is_finite prec emax f); try discriminate.
+  set (n1 := ZnearestE (B2R _ _ f)) in *.
+  destruct (min <=? n1) eqn:MIN; try discriminate.
+  destruct (n1 <=? max) eqn:MAX; try discriminate.
+  simpl in H. inversion H. subst n.
+  split. apply Zle_bool_imp_le; auto.
+  split. apply Zle_bool_imp_le; auto.
+  auto.
+Qed.
+
+
+(*
+Theorem ZofB_ne_range_minus:
+  forall minus_nan m f p q,
+  ZofB_ne_range f 0 (2 * q - 1) = Some p -> q <= 2^prec -> (IZR q <= B2R _ _ f)%R ->
+  ZofB_ne_range (Bminus _ _ _ Hmax minus_nan m f (BofZ q)) (-q) (q - 1) = Some (p - q).
+Proof.
+  intros. destruct (ZofB_ne_range_inversion _ _ _ _ H) as (A & B & C).
+  set (f' := Bminus prec emax prec_gt_0_ Hmax minus_nan m f (BofZ q)).
+  assert (D: ZofB_ne f' = Some (p - q)).
+  { apply ZofB_ne_minus. auto. lia. auto. auto. }
+  unfold ZofB_range. rewrite D. rewrite Zle_bool_true by lia. rewrite Zle_bool_true by lia. auto.
+Qed.
+ *)
+
 (** ** Algebraic identities *)
 
 (** Commutativity of addition and multiplication *)