proposition: Lemma arctanStream_correct : ∀ p : positive, Str_pth _ (arctanStream (AQtoQ num / AQtoQ den)) p (1%positive, AQtoQ num / AQtoQ den) == let (_, r) := iterate _ (fS ARarctanStream) p (1%positive, (num, den)) in AQtoQ (fst r) / AQtoQ (snd r).
proof: Proof. assert (forall n:Z, AQtoQ (ZtoAQ n) == (n#1)). { intro n. destruct n as [|n|n]. pose proof (rings.preserves_0 (f:=cast Z AQ)). rewrite H5. clear H5. rewrite rings.preserves_0. reflexivity. apply ZtoQ. change (Z.neg n) with (-Z.pos n)%Z. pose proof (rings.preserves_negate (f:=cast Z AQ)). rewrite H5. clear H5. rewrite rings.preserves_negate. rewrite ZtoQ. reflexivity. } apply Pos.peano_ind. - unfold Str_pth, iterate, arctanStream, snd. rewrite Qred_correct. simpl. do 6 rewrite rings.preserves_mult. rewrite rings.preserves_negate. rewrite H5, H5. unfold dec_recip, stdlib_rationals.Q_recip. unfold mult, stdlib_rationals.Q_mult. unfold negate, stdlib_rationals.Q_opp. rewrite Qmult_1_r. change (1#3) with (/3)%Q. unfold Qdiv. do 3 rewrite Qinv_mult_distr. do 3 rewrite Qmult_assoc. apply Qmult_comp. 2: reflexivity. do 2 rewrite Qmult_assoc. apply Qmult_comp. 2: reflexivity. ring. - intros p IHp. unfold Str_pth. unfold Str_pth in IHp. rewrite iterate_succ, iterate_succ. pose proof (arctanStream_fst (AQtoQ num / AQtoQ den) p) as H7. unfold dec_recip, stdlib_rationals.Q_recip. unfold dec_recip, stdlib_rationals.Q_recip in IHp. unfold mult, stdlib_rationals.Q_mult. unfold mult, stdlib_rationals.Q_mult in IHp. unfold Qdiv in H7. unfold Qdiv. unfold Qdiv in IHp. unfold Q_as_MetricSpace, msp_car. unfold Q_as_MetricSpace, msp_car in IHp. destruct (iterate _ (arctanStream (AQtoQ num * / AQtoQ den)%Q) p (1%positive, (AQtoQ num * / AQtoQ den)%Q)). simpl in H7. simpl in IHp. subst p0. unfold arctanStream, snd, fst. rewrite Qred_correct. rewrite IHp. clear IHp. pose proof (fS_fst ARarctanStream p (num, den)) as H6. destruct (iterate _ (fS ARarctanStream) p (1%positive, (num, den))) as [p0 p1]. simpl in H6. subst p0. unfold ARarctanStream, fS. simpl (fst (Pos.succ p, p1)). simpl (snd (Pos.succ p, p1)). replace (Pos.pred (Pos.succ p)~0) with (p~1)%positive. do 6 rewrite rings.preserves_mult. rewrite rings.preserves_negate. unfold mult, stdlib_rationals.Q_mult. unfold negate, stdlib_rationals.Q_opp. rewrite ZtoQ, ZtoQ. do 3 rewrite Qinv_mult_distr. setoid_replace (Z.pos p~1 # 2 + p~1)%Q with ((Z.pos p~1 # 1) * / (Z.pos (Pos.succ p)~1 # 1))%Q. ring. unfold Qinv, Qeq, Qmult, Qnum, Qden. rewrite Pos.mul_1_l, Z.mul_1_r. replace (2 + p~1)%positive with ((Pos.succ p)~1)%positive. reflexivity. change (p~1)%positive with (2*p+1)%positive. change ((Pos.succ p)~1)%positive with (2*Pos.succ p+1)%positive. rewrite Pplus_one_succ_l. rewrite Pos.mul_add_distr_l. reflexivity. rewrite Pplus_one_succ_l. change (p~1)%positive with (2*p+1)%positive. change ((1+p)~0)%positive with (2*(1+p))%positive. rewrite Pos.mul_add_distr_l. rewrite Pos.pred_sub. rewrite (Pos.add_comm (2*1)). rewrite <- Pos.add_sub_assoc. reflexivity. reflexivity. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.algebra.RSetoid CoRN.stdlib_omissions.Q CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRarctan_small CoRN.reals.fast.CRarctan CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.faster.ARAlternatingSum CoRN.reals.faster.ARsin CoRN.reals.faster.ARArith