proposition: Theorem binary_round_aux_correct : forall mode x mx ex lx, inbetween_float radix2 (Zpos mx) ex (Rabs x) lx -> (ex <= fexp (Zdigits radix2 (Zpos mx) + ex))%Z -> let z := binary_round_aux mode (Rlt_bool x 0) (Zpos mx) ex lx in valid_binary z = true /\ if Rlt_bool (Rabs (round radix2 fexp (round_mode mode) x)) (bpow radix2 emax) then SF2R radix2 z = round radix2 fexp (round_mode mode) x /\ is_finite_SF z = true /\ sign_SF z = Rlt_bool x 0 else z = binary_overflow mode (Rlt_bool x 0).
proof: Proof. Proof with auto with typeclass_instances. intros m x mx ex lx Bx Ex z. unfold binary_round_aux in z. revert z. rewrite shr_fexp_truncate. 2: easy. refine (_ (round_trunc_sign_any_correct _ _ (round_mode m) (choice_mode m) _ x (Zpos mx) ex lx Bx (or_introl _ Ex))). refine (_ (truncate_correct_partial _ _ _ _ _ _ _ Bx Ex)). destruct (truncate radix2 fexp (Zpos mx, ex, lx)) as ((m1, e1), l1). rewrite loc_of_shr_record_of_loc, shr_m_shr_record_of_loc. set (m1' := choice_mode m (Rlt_bool x 0) m1 l1). intros (H1a,H1b) H1c. rewrite H1c. assert (Hm: (m1 <= m1')%Z). unfold m1', choice_mode, cond_incr. case m ; try apply Z.le_refl ; match goal with |- (m1 <= if ?b then _ else _)%Z => case b ; [ apply Zle_succ | apply Z.le_refl ] end. assert (Hr: Rabs (round radix2 fexp (round_mode m) x) = F2R (Float radix2 m1' e1)). rewrite <- (Z.abs_eq m1'). rewrite <- (abs_cond_Zopp (Rlt_bool x 0) m1'). rewrite F2R_Zabs. now apply f_equal. apply Z.le_trans with (2 := Hm). apply Zlt_succ_le. apply gt_0_F2R with radix2 e1. apply Rle_lt_trans with (1 := Rabs_pos x). exact (proj2 (inbetween_float_bounds _ _ _ _ _ H1a)). assert (Br: inbetween_float radix2 m1' e1 (Rabs (round radix2 fexp (round_mode m) x)) loc_Exact). now apply inbetween_Exact. destruct m1' as [|m1'|m1']. rewrite shr_fexp_truncate. 2: apply Z.le_refl. generalize (truncate_0 radix2 fexp e1 loc_Exact). destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2). rewrite shr_m_shr_record_of_loc. intros Hm2. rewrite Hm2. repeat split. rewrite Rlt_bool_true. repeat split. apply sym_eq. case Rlt_bool ; apply F2R_0. rewrite <- F2R_Zabs, abs_cond_Zopp, F2R_0. apply bpow_gt_0. assert (He: (e1 <= fexp (Zdigits radix2 (Zpos m1') + e1))%Z). rewrite <- mag_F2R_Zdigits, <- Hr, mag_abs. 2: discriminate. rewrite H1b. rewrite cexp_abs. fold (cexp radix2 fexp (round radix2 fexp (round_mode m) x)). apply cexp_round_ge... rewrite H1c. case (Rlt_bool x 0). apply Rlt_not_eq. now apply F2R_lt_0. apply Rgt_not_eq. now apply F2R_gt_0. refine (_ (truncate_correct_partial _ _ _ _ _ _ _ Br He)). 2: now rewrite Hr ; apply F2R_gt_0. refine (_ (truncate_correct_format radix2 fexp (Zpos m1') e1 _ _ He)). 2: discriminate. rewrite shr_fexp_truncate. 2: easy. destruct (truncate radix2 fexp (Zpos m1', e1, loc_Exact)) as ((m2, e2), l2). rewrite shr_m_shr_record_of_loc. intros (H3,H4) (H2,_). destruct m2 as [|m2|m2]. elim Rgt_not_eq with (2 := H3). rewrite F2R_0. now apply F2R_gt_0. destruct (binary_fit_aux_correct m (Rlt_bool x 0) m2 e2) as [H5 H6]. apply Zeq_bool_true. rewrite Zpos_digits2_pos. rewrite <- mag_F2R_Zdigits by easy. now rewrite <- H3. apply (conj H5). revert H6. simpl. rewrite 2!F2R_cond_Zopp. now rewrite <- H3. elim Rgt_not_eq with (2 := H3). apply Rlt_trans with R0. now apply F2R_lt_0. now apply F2R_gt_0. rewrite <- Hr. apply generic_format_abs... apply generic_format_round... elim Rgt_not_eq with (2 := Hr). apply Rlt_le_trans with R0. now apply F2R_lt_0. apply Rabs_pos. apply Rlt_le_trans with (2 := proj1 (inbetween_float_bounds _ _ _ _ _ Bx)). now apply F2R_gt_0. clear. case m. exact inbetween_int_NE_sign. exact inbetween_int_ZR_sign. exact inbetween_int_DN_sign. exact inbetween_int_UP_sign. exact inbetween_int_NA_sign. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative