proposition: Theorem inv_correct : forall prec, extension Xinv (inv prec).
proof: Proof. intros prec [ | xl xu] [ | x] ; try ( intros ; exact I ) ; [now unfold convert; case (_ && _)|]. intros Hxlu. generalize Hxlu. unfold convert at 1. 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]. simpl. unfold bnd, contains, convert, Xinv'. generalize (sign_strict_correct_ xl xu x Hxlu). unfold c1. case (sign_strict_ xl xu) ; (intros (Hx0, (Hx0', (rHx0, (Hx0'', Hx0''')))) || intros (Hx0, Hx0')) ; try exact I ; try simpl_is_zero ; unfold Rdiv ; try ( (unfold Fdivz_DN, Fdivz_UP) ; rewrite 2!F.real_correct ; xreal_tac3 xl ; xreal_tac3 xu ; 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 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 ; rewrite F.fromZ_correct by easy ; xreal_tac3 y; (try now simpl) ; unfold Xdiv, Xdiv', Rdiv ; rewrite Rmult_1_l ; match goal with |- context [is_zero ?v] => case (is_zero v) ; [now simpl|] end ; apply Rle_trans ; try (revert Hxl; rewrite Hx0'') ; auto with mulauto | |- context [F.toX (F.div_DN ?prec ?x ?y)] => xreal_tac2; revert Hl ; rewrite F.fromZ_correct by easy ; xreal_tac3 y; (try now simpl) ; unfold Xdiv, Xdiv', Rdiv ; rewrite Rmult_1_l ; 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) ; try (revert Hxu; rewrite Hx0'') ; auto with mulauto end ; repeat match goal with | H:F.toX _ = _ |- _ => (try rewrite H) ; clear H end ; try rewrite F.fromZ_correct by easy ; try ( rewrite (F'.valid_lb_real (F.fromZ 1)) ; [|now rewrite F.real_correct, F.fromZ_correct] ) ; try ( rewrite (F'.valid_ub_real (F.fromZ 1)) ; [|now rewrite F.real_correct, F.fromZ_correct] ) ; set (H01 := Rlt_le _ _ Rlt_0_1) ; try (now left) ; try (now right) ; 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