proposition: Theorem mul_mixed_correct : forall prec yf, extension (fun x => Xmul x (F.toX yf)) (fun xi => mul_mixed prec xi yf).
proof: Proof. intros prec yf [|xl xu] [|x]; trivial; [now unfold convert; case (_ && _)|]. unfold convert. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; exfalso; lra]. intros Vxu Vxl. intros (Hxl, Hxu). simpl. generalize (F.classify_correct yf). rewrite F.cmp_correct, F.zero_correct, F.real_correct, F'.classify_zero. case_eq (F.classify yf); intro Cyf; [xreal_tac2; [easy|]|xreal_tac2; [|easy]..]; intros _; [|easy..]. unfold Xcmp. case Rcompare_spec; intro Hr. { elim (F.mul_DN_correct prec xu yf). { intros Vl Hl; rewrite Vl. elim (F.mul_UP_correct prec xl yf). { intros Vu Hu; rewrite Vu. apply le_contains. { apply (le_lower_trans _ _ _ Hl). rewrite X. revert Hxu; xreal_tac2; [now simpl|]; intro Hx. now apply Ropp_le_contravar, Rmult_le_compat_neg_r; [apply Rlt_le|]. } revert Hu; apply le_upper_trans. rewrite X. revert Hxl; xreal_tac2; [now simpl|]; intro Hx. now apply Rmult_le_compat_neg_r; [apply Rlt_le|]. } unfold F.is_non_neg', F.is_non_pos', F.is_non_pos_real, F.is_non_neg_real. rewrite X. case (F.toX xl). { right; left. split. easy. now apply Rlt_le. } intro r'; case (Rlt_or_le 0 r'); intro Hr'. { now do 3 right; split; apply Rlt_le. } right; left. split. easy. now apply Rlt_le. } unfold F.is_non_neg_real, F.is_non_pos_real, F.is_non_pos', F.is_non_neg'. rewrite X. case (F.toX xu). { right; right; left. split. easy. now apply Rlt_le. } intro r'; case (Rlt_or_le 0 r'); intro Hr'. { now do 2 right; left; split; apply Rlt_le. } right; left. split. easy. now apply Rlt_le. } { rewrite Hr, Rmult_0_r. rewrite F'.valid_lb_real, ?F'.valid_ub_real; [|now rewrite F.real_correct, F.zero_correct..]. now apply le_contains; rewrite F.zero_correct; right. } elim (F.mul_DN_correct prec xl yf). { intros Vl Hl; rewrite Vl. elim (F.mul_UP_correct prec xu yf). { intros Vu Hu; rewrite Vu. apply le_contains. { apply (le_lower_trans _ _ _ Hl). rewrite X. revert Hxl; xreal_tac2; [now simpl|]; intro Hx. now apply Ropp_le_contravar, Rmult_le_compat_r; [apply Rlt_le|]. } revert Hu; apply le_upper_trans. rewrite X. revert Hxu; xreal_tac2; [now simpl|]; intro Hx. now apply Rmult_le_compat_r; [apply Rlt_le|]. } unfold F.is_non_neg', F.is_non_pos', F.is_non_pos_real, F.is_non_neg_real. rewrite X. case (F.toX xu). { left. split. easy. now apply Rlt_le. } intro r'; case (Rlt_or_le 0 r'); intro Hr'. { left. now split; apply Rlt_le. } do 2 right; left. split. easy. now apply Rlt_le. } unfold F.is_non_neg_real, F.is_non_pos_real, F.is_non_pos', F.is_non_neg'. rewrite X. case (F.toX xl). { do 3 right. split. easy. now apply Rlt_le. } intro r'; case (Rlt_or_le 0 r'); intro Hr'. { now left; split; apply Rlt_le. } do 3 right. split. easy. now apply Rlt_le. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval