proposition: Theorem Btrunc_correct : forall x, IZR (Btrunc x) = round radix2 (FIX_exp 0) Ztrunc (B2R x).
proof: Proof. assert (round_0_to_0 : 0%R = (round radix2 (FIX_exp 0) Ztrunc 0)). { symmetry. apply round_0. apply valid_rnd_ZR. } intros [sx | sx | | sx mx ex Hx]; simpl; try assumption. destruct (Bnearbyint_correct_aux mode_ZR sx mx ex) as [_ [H0 _]]; [easy |]. simpl round_mode in H0. rewrite <-H0. unfold SFnearbyint_binary, SFnearbyint_binary_aux. set (mrs' := (if (ex <? - prec)%Z then {| shr_m := 0; shr_r := false; shr_s := true |} else fst (shr {| shr_m := Z.pos mx; shr_r := false; shr_s := false |} ex (- ex)))). fold mrs'. set (n := choice_mode mode_ZR sx (shr_m mrs') (loc_of_shr_record mrs')). fold n. case Zle_bool_spec; intros H1. - simpl SF2R. unfold F2R. simpl Fnum. simpl bpow. destruct sx; unfold cond_Zopp; [rewrite Zopp_mult_distr_l |]; rewrite mult_IZR; apply f_equal; destruct ex; easy. - destruct n as [ | p | p] eqn:H2; [now destruct sx | |]. + generalize (shl_align_fexp_correct p 0). destruct shl_align_fexp. simpl SF2R. unfold F2R. simpl. intros [H3 H4]. rewrite Rmult_1_r in H3. destruct sx; unfold cond_Zopp; [| assumption]. rewrite 2Ropp_Ropp_IZR. rewrite <-Ropp_mult_distr_l. now rewrite H3. + unfold n in H2. destruct (le_choice_mode_le mode_ZR sx (shr_m mrs') (loc_of_shr_record mrs')) as [H3 _]. rewrite H2 in H3. unfold mrs' in H3. case (ex <? - prec)%Z in H3. * simpl in H3. lia. * destruct (le_shr_le ({| shr_m := Z.pos mx; shr_r := false; shr_s := false |}) ex (- ex)) as [[H4 _] _]; [simpl; lia | lia |]. elim (Zle_not_lt 0 (Z.neg p)). 2: easy. apply Z.le_trans with (2 := H3). apply Zmult_le_0_reg_r with (2 ^ (- ex))%Z. apply Z.lt_gt, (Zpower_gt_0 radix2). lia. now rewrite Zmult_comm. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative