proposition: Theorem mul_correct : forall prec, extension_2 Xmul (mul prec).
proof: Proof. intros prec [ | xl xu] [ | yl yu] [ | x] [ | y] ; trivial; [| |intros _|]; [now unfold convert; case (_ && _)..|]. intros Hxlu Hylu. generalize Hxlu Hylu. 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. case_eq (F.valid_lb yl); [|intros _ _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub yu); [|intros _ _ _ [H0 H1]; exfalso; lra]. intros Vyu Vyl. intros (Hxl, Hxu) (Hyl, Hyu). simpl. unfold bnd, contains, convert. generalize (sign_large_correct_ xl xu x Hxlu). case (sign_large_ xl xu) ; intros (Hx0, Hx0') ; try ( generalize (sign_large_correct_ yl yu y Hylu) ; case (sign_large_ yl yu) ; intros (Hy0, Hy0') ) ; try ( rewrite F'.valid_lb_real, ?F'.valid_ub_real; [|now rewrite F.real_correct, F.zero_correct..] ; simpl ; try ( rewrite Hx0 ; rewrite Rmult_0_l ) ; try ( rewrite Hy0 ; rewrite Rmult_0_r ) ; split ; rewrite F.zero_correct ; apply Rle_refl ) ; try ( match goal with | |- context [F.valid_lb (F.mul_DN ?prec ?x ?y)] => elim (F'.mul_DN_correct prec x y); [intros Vl Hl; rewrite Vl| unfold F.is_non_neg_real, F.is_non_pos_real; unfold F.is_non_neg, F.is_non_pos] end ; [ match goal with | |- context [F.valid_ub (F.mul_UP ?prec ?x ?y)] => elim (F'.mul_UP_correct prec x y); [intros Vu Hu; rewrite Vu| unfold F.is_non_neg_real, F.is_non_pos_real; unfold F.is_non_neg, F.is_non_pos] end|] ; [split; match goal with | |- context [F.toX (F.mul_DN ?prec ?x ?y)] => xreal_tac2; revert Hl; (xreal_tac x; [now simpl|]); (xreal_tac y; [now simpl|]); (let H := fresh "H" in intro H; apply Ropp_le_cancel in H; apply (Rle_trans _ _ _ H); clear H) | |- context [F.toX (F.mul_UP ?prec ?x ?y)] => xreal_tac2; revert Hu; (xreal_tac x; [now simpl|]); (xreal_tac y; [now simpl|]); apply Rle_trans end ; clear_complex; try ( eauto with mulauto ; fail ) | |] ; try (destruct Hx0' as (Hx0', (rHx0, (Hx0'', Hx0'''))); rewrite Hx0'') ; try (destruct Hy0' as (Hy0', (rHy0, (Hy0'', Hy0'''))); rewrite Hy0'') ; try (now left); try (now (right; left)); try (now (right; right; left)); try (now (right; right; right)) ). elim (F'.mul_DN_correct prec xl yu); [intros Vxlyu Hxlyu |now (try (now left); try (now (right; left)); try (now (right; right; left)); try (now (right; right; right)))]. elim (F'.mul_DN_correct prec xu yl); [intros Vxuyl Hxuyl |now (try (now left); try (now (right; left)); try (now (right; right; left)); try (now (right; right; right)))]. elim (F'.mul_UP_correct prec xl yl); [intros Vxlyl Hxlyl |now (try (now left); try (now (right; left)); try (now (right; right; left)); try (now (right; right; right)))]. elim (F'.mul_UP_correct prec xu yu); [intros Vxuyu Hxuyu |now (try (now left); try (now (right; left)); try (now (right; right; left)); try (now (right; right; right)))]. elim (F'.min_valid_lb _ _ Vxlyu Vxuyl). intros Vmin Hmin. elim (F'.max_valid_ub _ _ Vxlyl Vxuyu). intros Vmax Hmax. rewrite Vmin, Vmax, Hmin, Hmax. split. { do 2 xreal_tac2. simpl; apply <-Rmin_Rle. destruct (Rle_or_lt x 0) as [Hx|Hx]; [left|right; generalize (Rlt_le _ _ Hx); clear Hx; intro Hx]; [revert Hxlyu; xreal_tac xl; [now simpl|]; xreal_tac yu; [now simpl|] |revert Hxuyl; xreal_tac xu; [now simpl|]; xreal_tac yl; [now simpl|]]; (let H := fresh "H" in intro H; apply Ropp_le_cancel in H; apply (Rle_trans _ _ _ H); clear H); clear_complex ; eauto with mulauto. } do 2 xreal_tac2. simpl; apply <-Rmax_Rle. destruct (Rle_or_lt x 0) as [Hx|Hx]; [left|right; generalize (Rlt_le _ _ Hx); clear Hx; intro Hx]; [revert Hxlyl; xreal_tac xl; [now simpl|]; xreal_tac yl; [now simpl|] |revert Hxuyu; xreal_tac xu; [now simpl|]; xreal_tac yu; [now simpl|]]; apply Rle_trans; clear_complex ; eauto with mulauto. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval