diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index db4fbec7..56b90727 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -963,6 +963,7 @@ Proof. lra. Qed. +(* Can be also done with Znearest_opp and functional extensionality *) Lemma ZnearestE_opp : forall x : R, ZnearestE (- x) = - ZnearestE x. Proof. @@ -1017,6 +1018,44 @@ Qed. Theorem ZofB_ne_correct: forall f, ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None. +Proof. + destruct f as [s|s|s p H|s m e H]; simpl; auto. +- f_equal. symmetry. apply (ZnearestE_IZR 0). +- destruct e; f_equal. + + unfold F2R; cbn. rewrite Rmult_1_r. rewrite ZnearestE_IZR. auto. + + unfold F2R; cbn. rewrite <- mult_IZR. rewrite ZnearestE_IZR. auto. + + unfold F2R; cbn. rewrite IZR_cond_Zopp. rewrite <- cond_Ropp_mult_l. + assert (EQ: forall x, ZnearestE (cond_Ropp s x) = cond_Zopp s (ZnearestE x)). + { intros. destruct s; cbn; auto. apply ZnearestE_opp. } + rewrite EQ. f_equal. + generalize (Zpower_pos_gt_0 2 p (eq_refl _)); intros. + set (p2p := (Z.pow_pos 2 p)) in *. + set (zm := Z.pos m) in *. + unfold Zdiv_ne, Z.succ in *. + case Z.compare_spec; intro CMP. + * admit. + * symmetry. + apply Znearest_imp with (n := zm / p2p). + apply Rabs_lt. + split. + { admit. } + assert (0 < 2*(IZR p2p * IZR (zm / p2p) - IZR zm) + (IZR p2p))%R as LT. + { rewrite <- mult_IZR. + rewrite <- minus_IZR. + rewrite <- mult_IZR. + rewrite <- plus_IZR. + apply IZR_lt. + lia. } + assert (0 < IZR p2p)%R. + { apply IZR_lt. assumption. } + assert (0 < -(IZR zm * / IZR p2p - IZR (zm / p2p) - / 2))%R as GT. + 2: lra. + field_simplify. + 2: lra. + apply Rdiv_lt_0_compat. + 2: lra. + lra. + * admit. Admitted. |