proposition: Lemma Bmult_correct_aux : forall m sx mx ex (Hx : bounded mx ex = true) sy my ey (Hy : bounded my ey = true), let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in let y := F2R (Float radix2 (cond_Zopp sy (Zpos my)) ey) in let z := binary_round_aux m (xorb sx sy) (Zpos (mx * my)) (ex + ey) loc_Exact in valid_binary z = true /\ if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (x * y))) (bpow radix2 emax) then SF2R radix2 z = round radix2 fexp (round_mode m) (x * y) /\ is_finite_SF z = true /\ sign_SF z = xorb sx sy else z = binary_overflow m (xorb sx sy).
proof: Proof. intros m sx mx ex Hx sy my ey Hy x y. unfold x, y. rewrite <- F2R_mult. simpl. replace (xorb sx sy) with (Rlt_bool (F2R (Float radix2 (cond_Zopp sx (Zpos mx) * cond_Zopp sy (Zpos my)) (ex + ey))) 0). apply binary_round_aux_correct. constructor. rewrite <- F2R_abs. apply F2R_eq. rewrite Zabs_Zmult. now rewrite 2!abs_cond_Zopp. change (Zpos (mx * my)) with (Zpos mx * Zpos my)%Z. assert (forall m e, bounded m e = true -> fexp (Zdigits radix2 (Zpos m) + e) = e)%Z. clear. intros m e Hb. destruct (andb_prop _ _ Hb) as (H,_). apply Zeq_bool_eq. now rewrite <- Zpos_digits2_pos. generalize (H _ _ Hx) (H _ _ Hy). clear x y sx sy Hx Hy H. unfold fexp, FLT_exp. refine (_ (Zdigits_mult_ge radix2 (Zpos mx) (Zpos my) _ _)) ; try discriminate. refine (_ (Zdigits_gt_0 radix2 (Zpos mx) _) (Zdigits_gt_0 radix2 (Zpos my) _)) ; try discriminate. generalize (Zdigits radix2 (Zpos mx)) (Zdigits radix2 (Zpos my)) (Zdigits radix2 (Zpos mx * Zpos my)). intros dx dy dxy Hx Hy Hxy. unfold emin. generalize (prec_lt_emax prec emax). lia. case sx ; case sy. apply Rlt_bool_false. now apply F2R_ge_0. apply Rlt_bool_true. now apply F2R_lt_0. apply Rlt_bool_true. now apply F2R_lt_0. apply Rlt_bool_false. now apply F2R_ge_0. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative