proposition: Lemma sinStream_correct : ∀ p : positive, Str_pth _ (sinStream (AQtoQ num / AQtoQ den)) p (1%positive, AQtoQ num / AQtoQ den) == let (_, r) := iterate _ (fS ARsinStream) 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. 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. field. intro abs. apply (strictly_order_preserving (cast AQ Q)) in dpos. rewrite rings.preserves_0, abs in dpos. exact (Qlt_irrefl 0 dpos). - intros p IHp. unfold Str_pth. unfold Str_pth in IHp. rewrite iterate_succ, iterate_succ. pose proof (sinStream_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 _ (sinStream (AQtoQ num * / AQtoQ den)%Q) p (1%positive, (AQtoQ num * / AQtoQ den)%Q)). simpl in H7. simpl in IHp. subst p0. unfold sinStream, snd, fst. rewrite IHp. clear IHp. pose proof (fS_fst ARsinStream p (num, den)). destruct (iterate _ (fS ARsinStream) p (1%positive, (num, den))) as [p0 p1]. simpl in H6. simpl. subst p0. 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. rewrite <- (Qmult_assoc (AQtoQ (snd p1) * AQtoQ den * AQtoQ den)). rewrite Qinv_mult_distr. setoid_replace (/ ((Z.pos (Pos.succ p)~0 # 1) * (Z.pos (Pos.succ p)~1 # 1))) with (1 # (Pos.succ p * (Pos.succ p)~1)~0) by reflexivity. do 2 rewrite Qinv_mult_distr. ring. Qed.
imports: Coq.QArith.Qround Coq.QArith.Qpower MathClasses.interfaces.abstract_algebra MathClasses.theory.nat_pow MathClasses.theory.int_pow CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.MetricMorphisms CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.util.Qdlog CoRN.stdlib_omissions.Q CoRN.reals.fast.CRsin CoRN.reals.fast.CRstreams CoRN.reals.fast.CRAlternatingSum CoRN.reals.fast.Compress CoRN.reals.faster.ARAlternatingSum CoRN.reals.faster.ARArith