proposition: Theorem div_correct : forall prec, extension_2 Xdiv (div prec).
proof: Proof. intros prec [ | xl xu] [ | yl yu] [ | x] [ | y] ; try ( intros ; exact I ) ; [now unfold convert; case (_ && _).. |now unfold convert at 2; case (_ && _)|]. intros Hxlu Hylu. generalize Hxlu Hylu. unfold convert at -3. 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 [Hxl Hxu]. 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 [Hyl Hyu]. simpl. unfold bnd, contains, convert, Xdiv'. generalize (sign_strict_correct_ xl xu x Hxlu) ; case (sign_strict_ xl xu) ; intros (Hx0, Hx0') ; try ( generalize (sign_strict_correct_ yl yu y Hylu) ; case (sign_strict_ yl yu) ; intros (Hy0, Hy0') ) ; try exact I ; try simpl_is_zero ; unfold Rdiv ; 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 ) ; split ; rewrite F.zero_correct ; apply Rle_refl ) ; try ( (unfold Fdivz_DN || unfold Fdivz_UP) ; rewrite F.real_correct ; xreal_tac3 yl ; xreal_tac3 yu ; try rewrite F.zero_correct ) ; try ( rewrite (F'.valid_lb_real F.zero) ; [|now rewrite F.real_correct, F.zero_correct] ) ; try ( rewrite (F'.valid_ub_real F.zero) ; [|now rewrite F.real_correct, F.zero_correct] ) ; try ( destruct Hy0' as (_, (rHy0', (Hy0', _))) ; match type of Hy0' with | F.toX ?x = Xreal _ => match goal with | H : F.toX x = Xnan |- _ => rewrite H in Hy0' end end ; discriminate ) ; try match goal with | |- context [F.valid_lb (F.div_DN ?prec ?x ?y)] => elim (F.div_DN_correct prec x y); [intros Vl Hl; rewrite Vl| unfold F.is_real_ub, F.is_real_lb, F.is_neg_real, F.is_pos_real ] ; rewrite ?F.real_correct end ; try match goal with | |- context [F.valid_ub (F.div_UP ?prec ?x ?y)] => elim (F.div_UP_correct prec x y); [intros Vu Hu; rewrite Vu| unfold F.is_real_ub, F.is_real_lb, F.is_neg_real, F.is_pos_real ] ; rewrite ?F.real_correct end ; try split ; try ( clear_complex ; simpl ; eauto with mulauto2 ; fail ) ; try match goal with | |- context [F.toX (F.div_UP ?prec ?x ?y)] => xreal_tac2; revert Hu ; xreal_tac3 x; (try now simpl) ; xreal_tac3 y; (try now simpl) ; unfold Xdiv, Xdiv', Rdiv ; match goal with |- context [is_zero ?v] => case (is_zero v) ; [now simpl|] end ; apply Rle_trans ; clear_complex ; eauto 8 with mulauto | |- context [F.toX (F.div_DN ?prec ?x ?y)] => xreal_tac2; revert Hl ; xreal_tac3 x; (try now simpl) ; xreal_tac3 y; (try now simpl) ; unfold Xdiv, Xdiv', Rdiv ; match goal with |- context [is_zero ?v] => case (is_zero v) ; [now simpl|] end ; (let H := fresh "H" in intro H; apply Ropp_le_cancel in H; apply (Rle_trans _ _ _ H); clear H) ; clear_complex ; eauto 8 with mulauto end ; repeat match goal with | H:F.toX _ = _ |- _ => (try rewrite H) ; clear H end ; try destruct Hx0' as (Hx0', (rHx0, (Hx0'', Hx0'''))) ; try rewrite Hx0'' ; try apply Rlt_le in Hx0''' ; try destruct Hy0' as (Hy0', (rHy0, (Hy0'', Hy0'''))) ; try rewrite Hy0'' ; try ( match type of Hx0' with | context [F.toX ?x] => revert Hx0'; xreal_tac x; intro Hx0' end ) ; try apply Rlt_le in Hx0' ; try rewrite X0 ; try rewrite X1 ; try inversion Hy0'' ; try (now left) ; try (now right ; destruct (F.toX xl)) ; try (now (right; left)) ; try (now (right; right; left)) ; try (now (right; right; right)). Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval