proposition: Lemma TM_tan_correct (x0 : R) (X0 X : I.type) n : subset' (I.convert X0) (I.convert X) -> contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) (TM_tan X0 X n) Xtan'.
proof: Proof. move=> Hsubset Hex. rewrite /TM_tan. case E0: apart0. apply i_validTM_Ztech with (TR.T_tan tt); last 2 first =>//. exact: I.tan_correct. constructor. - by move=> ? ?; rewrite PolR.size_grec1. - { move=> {X0 n Hsubset Hex} x n k Hx H; rewrite /TR.T_tan /PolR.nth /PolR.grec1 (nth_grec1up_indep _ _ _ _ _ 0%R (m2 := k)) // nth_grec1up_last. have->: Derive_n (fun t => proj_val (Xtan' t)) k x = Derive_n tan k x. apply: (@Derive_n_ext_loc _ tan). have Hdef : cos x <> 0%R. move/apart0_correct in E0. by apply: E0; apply: J.cos_correct. eapply locally_open with (1 := open_comp cos (fun y => y <> 0%R) (fun y _ => continuous_cos y) (open_neq R0)) (3 := Hdef). move=> {Hdef Hx x} x Hdef. by rewrite /Xtan' is_zero_false. rewrite last_grec1up // head_gloop1. rewrite [size _]/= subn0. have Hdef : cos x <> 0%R. move/apart0_correct in E0. by apply: E0; apply: J.cos_correct. elim: k H x {Hx} Hdef =>[|k IHk] H x Hdef. + by rewrite /= !Rsimpl. + move/ltnW in H; move/(_ H) in IHk. rewrite [INR]lock [PolR.lift]lock [fact]lock /= -!lock. set qk := iteri k (fun i c => PolR.div_mixed_r tt _ (INR (i + 0).+1)) (PolR.lift 1 PolR.one) in IHk *. rewrite (@Derive_ext_loc _ (fun x => qk.[tan x] * INR (fact k))%R); first last. eapply locally_open with (1 := open_comp cos (fun y => y <> 0%R) (fun y _ => continuous_cos y) (open_neq 0%R)) (3 := Hdef). move=> t Hdef'; move/(_ t Hdef') in IHk. rewrite IHk /Rdiv Rmult_assoc Rinv_l ?Rmult_1_r //. exact: INR_fact_neq_0. clear IHk. rewrite PolR.horner_div_mixed_r. rewrite PolR.horner_add addn0. rewrite !PolR.horner_lift Derive_scal_l. rewrite Derive_comp; first last. * by eexists; apply: is_derive_tan. * exact: PolR.ex_derive_horner. rewrite !PolR.Derive_horner. rewrite (is_derive_unique _ _ _ (is_derive_tan _ Hdef)). rewrite /Rdiv Rmult_assoc. rewrite -simpl_fact Rinv_involutive. change eq with (@eq R); ring. exact: INR_fact_neq_0. } constructor. - by move=> *; rewrite PolR.size_grec1 Pol.size_grec1. - { move => {X0 X n Hsubset Hex E0} X0 xi0 n Hx. apply: Pol.grec1_correct =>//. + move=> qi q m Hq. by repeat first [apply: Pol.div_mixed_r_correct| apply: Pol.sub_correct| apply: Pol.add_correct| apply: Pol.deriv_correct| apply: Pol.lift_correct| apply: Pol.mul_mixed_correct| apply: R_from_nat_correct]. + move=> qi q m Hq. by repeat first [apply: J.div_correct| apply: J.power_int_correct| apply: Pol.horner_correct| apply: J.add_correct| apply: J.sqr_correct| apply: I.fromZ_correct| apply: Pol.one_correct| apply: J.tan_correct]. + apply: Pol.lift_correct; exact: Pol.one_correct. + move=> [/=|k]; rewrite /PolR.nth ?nth_default //; exact: J.zero_correct. } - { move => {X0 X n Hsubset Hex E0} X x Hx Dx n k Hk. apply/Pol.grec1_propagate =>//. move=> q _. apply/Pol.horner_propagate/contains_Xnan. rewrite -Dx. exact: I.tan_correct Hx. by rewrite Pol.size_grec1. } - move=> m x Hx. have {E0} E0: cos x <> R0. apply: apart0_correct E0. exact: J.cos_correct. eapply (@ex_derive_n_ext_loc tan); last first. exact: ex_derive_n_is_derive_n (is_derive_n_tan m E0). eapply locally_open with (1 := open_comp cos (fun y => y <> 0%R) (fun y _ => continuous_cos y) (open_neq 0%R)) (3 := E0). move => /= x1 Hx1. by rewrite /Xtan' is_zero_false. simpl. split =>//. by move=> *; apply I.nai_correct. by move=> Hx; rewrite /= I.nai_correct. by rewrite I.nai_correct. exact: Hsubset. exists (TR.T_tan tt x0 n); last by rewrite I.nai_correct. apply: Pol.grec1_correct; by repeat first [move=> *; apply: Pol.div_mixed_r_correct |apply: Pol.add_correct |apply: Pol.deriv_correct |apply: Pol.lift_correct |apply: Pol.deriv_correct |apply: R_from_nat_correct |move=> *; apply: Pol.horner_correct |apply: J.tan_correct |apply: Pol.lift_correct |apply: Pol.one_correct |move=> [|k]; rewrite /PolR.nth ?nth_default //; exact: J.zero_correct ]. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound