proposition: Lemma fromZ_DN_correct : forall p n, valid_lb (fromZ_DN p n) = true /\ le_lower (toX (fromZ_DN p n)) (Xreal (IZR n)).
proof: Proof. intros prec [ |p|p]; unfold fromZ_DN. { now compute; split; [ |right]. } { case Pos.compare_spec; intro Hp'. { now rewrite Hp'; compute; split; [ |left; lra]. } { generalize (classify_correct (of_int63 (of_pos p))). rewrite valid_lb_correct, real_correct. rewrite (of_int63_of_pos_exact _ Hp'). now intro H; split; [revert H; case classify|right]. } set (e := (_ - _)%Z). set (s := Z.shiftr _ _). split; [now rewrite valid_lb_next_down| ]. assert (Pe : (0 <= e)%Z). { unfold e. apply Zle_minus_le_0. refine (proj1 (Z.log2_le_pow2 _ _ _) _); [now simpl| ]. generalize (Pos2Z.pos_lt_pos _ _ Hp'); lia. } rewrite toX_Prim2B, next_down_equiv, ldexp_equiv. generalize (shiftr_pos p Pe); intros [H1 H2]; revert H1 H2; fold e s. intros [H1 _] H2. assert (Rips: toX (of_int63 (of_Z s)) = Xreal (IZR s)). { generalize H2. rewrite (is_int s) at -2. intros H3. apply of_int63_exact. generalize (proj1 (Int63.to_Z_bounded (of_Z s))); revert H3. change (2^53)%Z with 9007199254740992%Z. change wB with 9223372036854775808%Z. lia. split. now apply Z.shiftr_nonneg. now apply Z.lt_trans with (1 := H2). } set (f := Prim2B _). generalize (Bldexp_correct _ _ _ _ mode_NE f e). rewrite Generic_fmt.round_generic. 2:{ apply Generic_fmt.valid_rnd_N. } 2:{ now apply mult_bpow_pos_exact_FLT; [apply generic_format_B2R| ]. } set (f' := Bldexp _ _ _). case Rlt_bool_spec; intro Hlt. { intros [Hr [Hf Hs]]. generalize (Bpred_correct _ _ _ _ f'). rewrite Hf. unfold f; rewrite <-real_is_finite, B2Prim_Prim2B, real_correct. rewrite Rips. intro H; generalize (H (eq_refl _)); clear H. case Rlt_bool. 2:{ change (SpecFloat.S754_infinity true) with (@B2SF FloatOps.prec emax (B754_infinity true)). now intro H; rewrite (B2SF_inj _ _ _ _ H); clear H. } intros [Hr' [Hf' _]]. replace (BtoX _) with (Xreal (B2R (Bpred f'))). 2:{ revert Hf'. rewrite <-real_is_finite, real_correct, toX_Prim2B, Prim2B_B2Prim. case_eq (BtoX (Bpred f')); [now simpl|intros r'' Hr'']. now rewrite (BtoX_B2R _ _ Hr''). } simpl; rewrite Hr', Hr. apply Ropp_le_contravar, (Rle_trans _ _ _ (Ulp.pred_le_id _ _ _)). revert Rips; rewrite toX_Prim2B; fold f; intro H. rewrite <-(BtoX_B2R _ _ H); clear H. refine (Rle_trans _ _ _ _ (IZR_le _ _ H1)); fold e; right. rewrite mult_IZR. now fold e; apply f_equal2; [ |revert Pe; case e]. } intro Hf'. apply (le_lower_trans _ (BtoX (Bmax_float))). { revert Hf'. now case f' as [sf'|sf'| |sf' mf' ef' Bf']; unfold B2SF; case Bsign; (try now intro H; discriminate H); [ | ]; intro H; injection H; clear H; intros ->; [ |right]. } apply Ropp_le_contravar. generalize (IZR_le _ _ H1); apply Rle_trans. revert Rips; rewrite toX_Prim2B; fold f e; intro Rips. revert Hlt. rewrite mult_IZR, <-(BtoX_B2R _ _ Rips). rewrite Rabs_mult. rewrite Rabs_pos_eq; [ |now apply IZR_le, Z.shiftr_nonneg]. rewrite Rabs_pos_eq; [ |now apply bpow_ge_0]. rewrite <-(IZR_Zpower _ _ Pe). apply Rle_trans; compute; lra. } case Pos.compare_spec; intro Hp'. { now rewrite Hp'; compute; split; [ |left; lra]. } { generalize (classify_correct (- of_int63 (of_pos p))). rewrite valid_lb_correct, real_correct. generalize (of_int63_of_pos_exact _ Hp'). rewrite !toX_Prim2B, opp_equiv, BtoX_Bopp; intros ->. now intro H; split; [revert H; case classify|right]. } set (e := (_ - _)%Z). set (s := Z.shiftr _ _). assert (Pe : (0 <= e)%Z). { unfold e. apply Zle_minus_le_0. refine (proj1 (Z.log2_le_pow2 _ _ _) _); [now simpl| ]. generalize (Pos2Z.pos_lt_pos _ _ Hp'); lia. } rewrite <-(B2Prim_Prim2B (Z.ldexp _ _)) at 1; rewrite toX_Prim2B. rewrite ldexp_equiv, opp_equiv. rewrite Bldexp_Bopp_NE. rewrite BtoX_Bopp. change (Z.neg p) with (- (Z.pos p))%Z; rewrite opp_IZR. generalize (shiftr_pos p Pe); intros [H1 H2]; revert H1 H2; fold e s. intros [_ H1] H2. assert (Hips1 : (Int63.to_Z (of_Z s + 1) = s + 1)%Z). { generalize H2. rewrite (is_int s) at -2. intros H3. rewrite Int63.add_spec, Zmod_small; rewrite to_Z_1. easy. generalize (proj1 (Int63.to_Z_bounded (of_Z s))); revert H3. change (2^53)%Z with 9007199254740992%Z. change wB with 9223372036854775808%Z. lia. split. now apply Z.shiftr_nonneg. now apply Z.lt_trans with (1 := H2). } assert (H2' : (Int63.to_Z (of_Z s + 1) <= 2 ^ 53)%Z). { rewrite Hips1; lia. } assert (Rips := of_int63_exact _ H2'). set (f := Prim2B _). generalize (Bldexp_correct _ _ _ _ mode_NE f e). assert (Hsf : Bsign f = false). { revert Rips; unfold f. rewrite toX_Prim2B. intro H; apply (Bsign_pos _ _ H). apply IZR_lt. rewrite Hips1. apply Zle_lt_succ. now apply Z.shiftr_nonneg. } case Rlt_bool. 2:{ rewrite Hsf. change (binary_overflow _ _ _ _) with (@B2SF FloatOps.prec emax (B754_infinity false)). intro H; rewrite (B2SF_inj _ _ _ _ H), valid_lb_correct. now unfold classify; rewrite classify_spec, Prim2SF_B2Prim; split. } intros [Hr [Hf _]]; split. { rewrite valid_lb_correct. generalize (classify_correct (B2Prim (Bopp (Bldexp mode_NE f e)))). rewrite real_is_finite, is_finite_Bopp, Hf. replace (is_finite f) with true; [now case classify|symmetry]. now unfold f; rewrite <-real_is_finite, B2Prim_Prim2B, real_correct, Rips. } case_eq (BtoX (Bldexp mode_NE f e)); [now simpl|intros rx Hrx]. do 2 apply Ropp_le_contravar. rewrite (BtoX_B2R _ _ Hrx); clear rx Hrx; simpl; rewrite Hr. rewrite Generic_fmt.round_generic. 2:{ apply Generic_fmt.valid_rnd_N. } 2:{ now apply mult_bpow_pos_exact_FLT; [apply generic_format_B2R| ]. } revert Rips; rewrite toX_Prim2B; fold f. intro H; rewrite <-(BtoX_B2R _ _ H); clear H. apply (Rle_trans _ _ _ (Rlt_le _ _ (IZR_lt _ _ H1))); right. rewrite mult_IZR. now fold e; apply f_equal2; [rewrite Hips1|revert Pe; case e]. Qed.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig