proposition: Lemma sign_plus_overflow : forall m sx mx ex sy my ey, bounded mx ex = true -> bounded my ey = true -> let z := (F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) + F2R (Float radix2 (cond_Zopp sy (Zpos my)) ey))%R in (bpow radix2 emax <= Rabs (round radix2 fexp (round_mode m) z))%R -> sx = Rlt_bool z 0 /\ sx = sy.
proof: Proof. Proof with auto with typeclass_instances. intros m sx mx ex sy my ey Hx Hy z Bz. destruct (Bool.bool_dec sx sy) as [Hs|Hs]. refine (conj _ Hs). unfold z. rewrite Hs. apply sym_eq. case sy. apply Rlt_bool_true. rewrite <- (Rplus_0_r 0). apply Rplus_lt_compat. now apply F2R_lt_0. now apply F2R_lt_0. apply Rlt_bool_false. rewrite <- (Rplus_0_r 0). apply Rplus_le_compat. now apply F2R_ge_0. now apply F2R_ge_0. elim Rle_not_lt with (1 := Bz). generalize (bounded_lt_emax _ _ Hx) (bounded_lt_emax _ _ Hy). intros Bx By. generalize (canonical_bounded sx _ _ Hx) (canonical_bounded sy _ _ Hy). clear -Bx By Hs prec_gt_0_. intros Cx Cy. destruct sx. destruct sy. now elim Hs. clear Hs. apply Rabs_lt. split. apply Rlt_le_trans with (F2R (Float radix2 (cond_Zopp true (Zpos mx)) ex)). rewrite F2R_Zopp. now apply Ropp_lt_contravar. apply round_ge_generic... now apply generic_format_canonical. pattern (F2R (Float radix2 (cond_Zopp true (Zpos mx)) ex)) at 1 ; rewrite <- Rplus_0_r. apply Rplus_le_compat_l. now apply F2R_ge_0. apply Rle_lt_trans with (2 := By). apply round_le_generic... now apply generic_format_canonical. rewrite <- (Rplus_0_l (F2R (Float radix2 (Zpos my) ey))). apply Rplus_le_compat_r. now apply F2R_le_0. destruct sy. 2: now elim Hs. clear Hs. apply Rabs_lt. split. apply Rlt_le_trans with (F2R (Float radix2 (cond_Zopp true (Zpos my)) ey)). rewrite F2R_Zopp. now apply Ropp_lt_contravar. apply round_ge_generic... now apply generic_format_canonical. pattern (F2R (Float radix2 (cond_Zopp true (Zpos my)) ey)) at 1 ; rewrite <- Rplus_0_l. apply Rplus_le_compat_r. now apply F2R_ge_0. apply Rle_lt_trans with (2 := Bx). apply round_le_generic... now apply generic_format_canonical. rewrite <- (Rplus_0_r (F2R (Float radix2 (Zpos mx) ex))). apply Rplus_le_compat_l. now apply F2R_le_0. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative