proposition: Theorem nearbyint_correct m u (Y : I.type) tf f : approximates Y tf f -> approximates Y (nearbyint m u Y tf) (fun x => Xnearbyint m (f x)).
proof: Proof. move=> Hf. rewrite /nearbyint. set i := I.nearbyint _ _. set i1 := I.bnd _ _. set i2 := I.bnd _ _. set i3 := I.div _ _ _. set i4 := I.div _ _ _. set i5 := I.div _ _ _. case E1 : Iconst => /=. { have H := Iconst_true_correct E1. move=> Y0; right. exists (Xlower (I.convert i)); last first. { move=> x Hx; apply: H. apply: I.nearbyint_correct. by have := eval_correct u Hf Hx. } have Hi : not_empty (I.convert i). { rewrite /i. have [y Hy] := Y0. apply (not_empty_contains _ (Xlift (Rnearbyint m) (Xbind f (Xreal y)))). apply: I.nearbyint_correct. exact: eval_correct. } rewrite I.bnd_correct /=. - rewrite -I.lower_correct //. case/andP: E1 => /I.bounded_correct [/I.lower_bounded_correct [-> _] _] _; lra. - exact: I.valid_lb_lower. - apply: I.valid_ub_real. by case/andP: E1 => /I.bounded_correct [/I.lower_bounded_correct [-> _] _] _. } apply: (@approximates_ext (fun x : R => Xadd (f x) (Xsub (Xlift (Rnearbyint m) (f x)) (f x)))). { by move=> x; case: (f x) => //= r; congr Xreal; lra. } set vv := match m with rnd_UP => _ | rnd_DN => _ | rnd_NE => _ |rnd_ZR => _ end. rewrite (surjective_pairing vv). apply: add_correct => //=. intros He. split=> //=. - move=> x Hx. have /(@I.nearbyint_correct m) := eval_correct u Hf Hx. rewrite -/i /=. case: (f x) => //= Hi _. apply: I.mask_propagate_r. by case: I.convert Hi. - move=> HY. have F1 : contains (I.convert Y) Xnan by rewrite HY. apply: I.mask_propagate_r. have /= := eval_correct u Hf F1. have := I.nearbyint_correct m (eval u tf Y Y) Xnan. case: I.convert => //=. rewrite -/i. by case: I.convert => /=. - rewrite {}/vv; case m => //=; try apply: contains_fromZ_lower_upper_div; try lia. case: I.sign_large; try apply: contains_fromZ_lower_upper_div; try lia. by apply: contains_fromZ_lower_upper; lia. - exact: contains_midpoint. move: E1. have F1 : Pol.contains_pointwise (Pol.polyC i3) (PolR.polyC (1/2)). apply: Pol.polyC_correct. rewrite (_ : Xreal _ = Xdiv (Xreal 1) (Xreal 2)). apply: I.div_correct; exact: I.fromZ_small_correct. rewrite /= /Xdiv'. now rewrite is_zero_false. have Him1 : not_empty (I.convert im1). { rewrite /im1. by exists (IZR (-1)); apply: I.fromZ_small_correct. } have Hi1 : not_empty (I.convert (TM.i1)). { rewrite /TM.i1. by exists (IZR 1); apply: I.fromZ_small_correct. } have Hlim1 : I.valid_lb (I.lower im1) by exact: I.valid_lb_lower. have Hui1 : I.valid_ub (I.upper TM.i1) by exact: I.valid_ub_upper. have F2 : contains (I.convert (I.mask i4 i)) (Xreal (- (1/2))). { apply: I.mask_correct'. rewrite (_ : Xreal (- (1 / 2)) = Xdiv (Xreal (-1)) (Xreal 2)); last first. rewrite /= /Xdiv'. by case: is_zero_spec; try lra; move=> _; congr Xreal; lra. apply: I.div_correct; last by exact: I.fromZ_small_correct. rewrite I.bnd_correct // I.lower_correct // I.upper_correct //. refine (_ (I.fromZ_small_correct (-1) _) (I.fromZ_small_correct 1 _)) ; [|easy..]. by ((do 2 case: I.convert) => //= [] [|x1] [|y1] //; try lra) => [] [|x2] [|y2] //; lra. } have F3 r : contains (I.convert (I.mask i4 i)) (Xreal (Rnearbyint rnd_UP r - r - 1 / 2)). { apply: I.mask_correct' => /=. set ir := IZR _. rewrite (_ : Xreal _ = Xdiv (Xreal (2 * (ir - r - 1/2))) (Xreal 2)); last first. rewrite /= /Xdiv'. case: is_zero_spec; try lra; move=> _. by congr Xreal; lra. apply: I.div_correct; last by exact: I.fromZ_small_correct. rewrite I.bnd_correct // /contains. refine (_ (I.fromZ_small_correct (-1) _) (I.fromZ_small_correct 1 _)) ; [|easy ..]. rewrite I.lower_correct // I.upper_correct //. set iv1 := I.convert _. set iv2 := I.convert _. have HR := Rnearbyint_error_UP r. rewrite /= -/ir in HR. by case: iv1 => [|[|x1] [|x2]] /=; case: iv2 => [|[|x3] [|x4]] //=; try lra. } have F4 : Pol.contains_pointwise (Pol.polyC i5) (PolR.polyC (- (1/2))). apply: Pol.polyC_correct. rewrite (_ : Xreal _ = Xdiv (Xreal (-1)) (Xreal 2)). by apply: I.div_correct; exact: I.fromZ_small_correct. { rewrite /= /Xdiv'. by case: is_zero_spec; try lra; move=> _; congr Xreal; lra. } have F5 : contains (I.convert (I.mask i4 i)) (Xreal (1/2)). { apply: I.mask_correct'. rewrite (_ : Xreal (1 / 2) = Xdiv (Xreal 1) (Xreal 2)); last first. rewrite /= /Xdiv'. by case: is_zero_spec; try lra; move=> _; congr Xreal; lra. apply: I.div_correct; last by exact: I.fromZ_small_correct. rewrite I.bnd_correct // I.lower_correct // I.upper_correct //. refine (_ (I.fromZ_small_correct (-1) _) (I.fromZ_small_correct 1 _)) ; [|easy..]. by ((do 2 case: I.convert) => //= [] [|x1] [|y1] //; try lra) => [] [|x2] [|y2] //; lra. } have F6 r : contains (I.convert (I.mask i4 i)) (Xreal (Rnearbyint rnd_DN r - r + 1 / 2)). { apply: I.mask_correct' => /=. set ir := IZR _. rewrite (_ : Xreal _ = Xdiv (Xreal (2 * (ir - r + 1/2))) (Xreal 2)); last first. rewrite /= /Xdiv'. case: is_zero_spec; try lra; move=> _. by congr Xreal; lra. apply: I.div_correct; last by exact: I.fromZ_small_correct. rewrite I.bnd_correct //. rewrite /contains. refine (_ (I.fromZ_small_correct (-1) _) (I.fromZ_small_correct 1 _)) ; [|easy..]. rewrite I.lower_correct // I.upper_correct //. set iv1 := I.convert _. set iv2 := I.convert _. have HR := Rnearbyint_error_DN r. rewrite /= -/ir in HR. by case: iv1 => [|[|x1] [|x2]] /=; case: iv2 => [|[|x3] [|x4]] //=; try lra. } move: F2 F3 F5 F6. rewrite {}/vv {}/i1 {}/i. case: m => //=; set i := I.nearbyint _ _ => F2 F3 F5 F6 E1. - exists (PolR.polyC (1/2)) => //= y _. rewrite Rmult_0_l Rplus_0_l. case: (f y) => [|r] //=. by rewrite Rminus_0_l. - exists (PolR.polyC (-(1/2))) => //= y _. rewrite Rmult_0_l Rplus_0_l /Rminus Ropp_involutive. case: (f y) => //=. by rewrite Rplus_0_l. - case: I.sign_large (I.sign_large_correct (eval u tf Y Y)) => Hsign. - exists (PolR.polyC (-(1/2))) => //= y Cy. rewrite Rmult_0_l Rplus_0_l. case Er : (f y) => [|r] //=. by rewrite Rminus_0_l Ropp_involutive. rewrite {1}/Rminus Ropp_involutive. rewrite Raux.Ztrunc_floor //. have : f y = Xreal 0. apply: Hsign. by apply: (eval_correct u Hf Cy). by rewrite Er => [[]]; lra. - exists (PolR.polyC (1/2)) => //= y Cy. rewrite Rmult_0_l Rplus_0_l. case Er : (f y) => [|r] //=. by rewrite Rminus_0_l. rewrite Raux.Ztrunc_ceil //. have [_ /=] := Hsign _ (eval_correct u Hf Cy). by rewrite Er. - exists (PolR.polyC (-(1/2))) => //= y Cy. rewrite Rmult_0_l Rplus_0_l. case Er : (f y) => [|r] /=. by rewrite Rminus_0_l Ropp_involutive. rewrite Raux.Ztrunc_floor //. rewrite /Rminus Ropp_involutive. by apply F6. have [_ /=] := Hsign _ (eval_correct u Hf Cy). by rewrite Er. - exists (PolR.polyC 0) => //= [|y _]. apply: Pol.polyC_correct. by apply: J.zero_correct. rewrite Rmult_0_l Rplus_0_l. case Er : (f y) => [|r] /=. rewrite Rminus_0_l. apply: I.mask_correct'. rewrite I.bnd_correct // I.lower_correct // I.upper_correct //. refine (_ (I.fromZ_small_correct (-1) _) (I.fromZ_small_correct 1 _)) ; [|easy..]. by ((do 2 case: I.convert) => //= [] [|x1] [|y1] //; try lra) => [] [|x2] [|y2] //; lra. apply: I.mask_correct'. rewrite I.bnd_correct //. rewrite /contains. refine (_ (I.fromZ_small_correct (-1) _) (I.fromZ_small_correct 1 _)) ; [|easy..]. rewrite I.lower_correct // I.upper_correct //. set iv1 := I.convert _. set iv2 := I.convert _. have HR := Rnearbyint_error_ZR r. rewrite /= in HR. by case: iv1 => [|[|x1] [|x2]] /=; case: iv2 => [|[|x3] [|x4]] //=; try lra. exists (PolR.polyC 0) => //= [|y Cy]. apply: Pol.polyC_correct; exact: J.zero_correct. rewrite Rmult_0_l Rplus_0_r Rminus_0_r. case: (f y) => /=. apply: I.mask_correct'. rewrite (_ : Xreal _ = Xdiv (Xreal 0) (Xreal 2)); last first. rewrite /= /Xdiv'. by case: is_zero_spec; try lra; move=> _; congr Xreal; lra. apply: I.div_correct; last by exact: I.fromZ_small_correct. rewrite I.bnd_correct // I.lower_correct // I.upper_correct //. refine (_ (I.fromZ_small_correct (-1) _) (I.fromZ_small_correct 1 _)) ; [|easy..]. by ((do 2 case: I.convert) => //= [] [|x1] [|y1] //; try lra) => [] [|x2] [|y2] //; lra. move=> r. apply: I.mask_correct'. set ir := IZR _. rewrite (_ : Xreal _ = Xdiv (Xreal (2 * (ir - r))) (Xreal 2)); last first. rewrite /= /Xdiv'. case: is_zero_spec; try lra; move=> _. by congr Xreal; lra. apply: I.div_correct; last by exact: I.fromZ_small_correct. rewrite I.bnd_correct //. rewrite /contains. refine (_ (I.fromZ_small_correct (-1) _) (I.fromZ_small_correct 1 _)) ; [|easy..]. rewrite I.lower_correct // I.upper_correct //. set iv1 := I.convert _. set iv2 := I.convert _. have HR := Rnearbyint_error_NE r. rewrite /= -/ir in HR. by case: iv1 => [|[|x1] [|x2]] /=; case: iv2 => [|[|x3] [|x4]] //=; try lra. Qed.
imports: Coq(Reals ZArith Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq bigop) Interval Xreal Basic Interval_compl Datatypes Taylor_model_sharp Bound Bound_quad Univariate_sig