proposition: Lemma iterate_stop_correct : forall (p:positive) (x:X), exists q:positive, iterate_stop p x ≡ iterate q x /\ (forall r, Pos.lt r q -> stop (iterate r x) ≡ false) /\ (p ≡ q \/ (Pos.lt q p /\ stop (iterate q x) ≡ true)).
proof: Proof. induction p. - intro x. simpl. destruct (stop (f x)) eqn:des1. exists xH. split. reflexivity. split. intros. exfalso; exact (Pos.nlt_1_r r H). right. split. rewrite Pos.xI_succ_xO. apply Pos.lt_1_succ. exact des1. destruct (stop (iterate_stop p (f x))) eqn:des. + specialize (IHp (f x)) as [q [itereq [H H0]]]. exists (Pos.succ q). split. rewrite itereq, iterate_succ, iterate_shift. reflexivity. split. apply (Pos.peano_case (fun r => (r < Pos.succ q)%positive → stop (iterate r x) ≡ false)). intros. exact des1. intros. rewrite iterate_succ, iterate_shift. apply H. apply Pos.succ_lt_mono in H1. exact H1. right. split. rewrite Pos.xI_succ_xO. rewrite <- Pos.succ_lt_mono. destruct H0. rewrite H0. rewrite <- Pos.add_diag. apply Pos.lt_add_r. apply (Pos.lt_trans _ p). apply H0. rewrite <- Pos.add_diag. apply Pos.lt_add_r. rewrite iterate_succ, iterate_shift, <- itereq. exact des. + pose proof (IHp (f x)) as [q [itereq [H H0]]]. destruct H0. 2: exfalso; destruct H0; rewrite <- itereq, des in H1; discriminate. subst q. specialize (IHp (iterate_stop p (f x))) as [q [qeq [H0 H1]]]. exists (Pos.succ q+p)%positive. split. rewrite qeq. rewrite <- Pos.add_1_r, <- Pos.add_assoc, iterate_add. apply f_equal. rewrite Pos.add_1_l, itereq, iterate_succ, iterate_shift. reflexivity. split. apply (Pos.peano_case (fun r => (r < Pos.succ q+p)%positive → stop (iterate r x) ≡ false)). intros. exact des1. intros r H2. rewrite iterate_succ, iterate_shift. destruct (Pos.lt_total r p). apply H, H3. destruct H3. rewrite H3. rewrite <- itereq. exact des. rewrite <- (Pplus_minus r p). 2: apply Pos.lt_gt, H3. rewrite Pos.add_comm, iterate_add, <- itereq. apply (H0 (r-p)%positive). rewrite <- (Pos.add_1_l q), <- Pos.add_assoc, Pos.add_1_l in H2. apply Pos.succ_lt_mono in H2. rewrite <- (Pplus_minus r p) in H2. 2: apply Pos.lt_gt, H3. rewrite Pos.add_comm in H2. apply Pos.add_lt_mono_r in H2. exact H2. destruct H1. left. rewrite H1. rewrite Pos.xI_succ_xO. rewrite <- (Pos.add_1_l q), <- Pos.add_assoc, Pos.add_1_l. rewrite Pos.add_diag. reflexivity. right. split. rewrite Pos.xI_succ_xO. rewrite <- Pos.add_1_l, <- Pos.add_assoc, Pos.add_1_l. rewrite <- Pos.succ_lt_mono, <- Pos.add_diag. apply Pos.add_lt_mono_r, H1. rewrite <- Pos.add_1_r, <- Pos.add_assoc, iterate_add. rewrite Pos.add_1_l, iterate_succ, iterate_shift. rewrite <- itereq. apply H1. - intro x. simpl. destruct (stop (iterate_stop p x)) eqn:des. + specialize (IHp x) as [q [itereq [H H0]]]. exists q. split. exact itereq. split. intros. apply H, H1. right. split. destruct H0. rewrite H0. rewrite <- Pos.add_diag. apply Pos.lt_add_r. apply (Pos.lt_trans _ p). apply H0. rewrite <- Pos.add_diag. apply Pos.lt_add_r. rewrite <- itereq. exact des. + pose proof (IHp x) as [q [itereq [H H0]]]. destruct H0. 2: exfalso; destruct H0; rewrite <- itereq, des in H1; discriminate. subst q. specialize (IHp (iterate_stop p x)) as [q [qeq [H0 H1]]]. exists (q+p)%positive. split. rewrite qeq, iterate_add. apply f_equal. exact itereq. split. intros. destruct (Pos.lt_total r p). apply H, H3. destruct H3. rewrite H3. clear H3 H2 r. rewrite <- itereq. exact des. rewrite <- (Pplus_minus r p). 2: apply Pos.lt_gt, H3. rewrite Pos.add_comm, iterate_add, <- itereq. apply (H0 (r-p)%positive). rewrite <- (Pplus_minus r p) in H2. 2: apply Pos.lt_gt, H3. rewrite Pos.add_comm in H2. apply Pos.add_lt_mono_r in H2. exact H2. destruct H1. left. rewrite H1. rewrite Pos.add_diag. reflexivity. right. split. rewrite <- Pos.add_diag. apply Pos.add_lt_mono_r, H1. rewrite iterate_add, <- itereq. apply H1. - intro x. exists xH. split. reflexivity. split. intros. exfalso; exact (Pos.nlt_1_r r H). left. reflexivity. Qed.
imports: CoRN.algebra.RSetoid CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric CoRN.metric2.Limit Coq.QArith.Qabs Coq.Arith.Arith Coq.QArith.Qpower CoRN.reals.fast.LazyNat Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.theory.streams MathClasses.theory.series MathClasses.interfaces.abstract_algebra MathClasses.theory.streams