# Library Coqtail.Fresh.Reals.Rapprox

Require Import Raxiom Rconvenient Repsilon Rseq IZR.
Require Import ZArith.

Module Rapprox (Import T : CReals).
Module Rconvenient := (Rconvenient T). Import Rconvenient.
Module Repsilon := (Repsilon T). Import Repsilon.
Module Rsequence := (Rsequence T). Import Rsequence.
Module IZR := IZR. Import IZR.
Open Scope R_scope.

Definition po n := IPR (Ppow2 n).
Definition pop n : (po n ## R0) := Rdiscr_IPR_0 _.
Definition Zapprox x n := Rup (x × po n).

Definition Rseq_approx : RRseq := fun x n ⇒ ((IZR (Zapprox x n)) / po n) (pop n).

Lemma Ppow2_double : x, (Zpos (Ppow2 (S x)) = 2 × Zpos (Ppow2 x))%Z.
Proof.
reflexivity.
Qed.

Lemma Zle_S_Ppow2 : p, (Zpos (p + 1) Zpos (Ppow2 (Zabs_nat (Zpos p))))%Z.
Proof.
intros.
rewrite Zpos_plus_distr.
replace (Zpos p + 1)%Z with ((Z_of_nat (nat_of_P p)) + 1)%Z.
simpl.
induction (nat_of_P p).
simpl. intuition.
rewrite Ppow2_double. apply Zle_trans with (2× (Z_of_nat n + 1))%Z; zify; omega.
rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P. reflexivity.
Qed.

Lemma Zpos_Ppow2_increasing : n m, (n m)%nat → (Zpos (Ppow2 n) Zpos (Ppow2 m))%Z.
Proof.
intros n m Hnm.
induction Hnm. omega.
eapply Zle_trans; [apply IHHnm | ].
simpl. zify; omega.
Qed.

Lemma Rpos_witness : e, R0 < esigT (fun N n, le N nRinv (po n) (pop n) < e).
Proof.
intros e epos.
assert (de : e ## R0) by (right; auto).
pose (e' := Rinv e de).
pose (N := Zabs_nat (Rup e')).
N; intros n Hn.

apply Rmul_lt_cancel_l with (po n).
apply Rpos_IPR.

eapply Req_lt_compat_l; [ symmetry; apply Rinv_r | ].
apply Rmul_lt_cancel_r with e'.
apply Rinv_pos_compat; auto.

apply (Req_lt_compat e' (po n)).
ring_simplify; reflexivity.

unfold e'; rewrite Rmul_assoc, Rinv_r.
ring_simplify; reflexivity.

destruct (Rup_spec e') as (le', _).
apply Rlt_le_trans with (IZR (Rup e') + R1).
apply Radd_lt_cancel_r with (- IZR (Rup e')).
apply Req_lt_compat_r with R1.
ring.
apply le'.

apply Rle_trans with (po N).
change (IZR (Rup e') + IZR 1 po N).
eapply Req_le_compat_l; [ apply IZR_add | ].
change (IZR (Rup e' + 1) IZR (Zpos (Ppow2 N))); apply IZR_le.
unfold N; pose (r := Rup e'); fold r.
clearbody r; clear.
destruct r as [ | p | p ].
simpl; now auto with ×.

apply Zle_S_Ppow2.

apply Zle_trans with 1%Z; zify; omega.

change (IZR (Zpos (Ppow2 N)) IZR (Zpos (Ppow2 n))); apply IZR_le.
clearbody N e'; clear -Hn.
apply Zpos_Ppow2_increasing. apply Hn.
Qed.

Lemma Rseq_cv_approx : x, Rseq_cv (Rseq_approx x) x.
Proof.
intros x e epos.
destruct (Rpos_witness e epos) as (N, HN).
N; intros n Hn.
unfold Rdist, Rseq_approx, Zapprox.
destruct (Rup_spec (x × po n)) as (re, er).
split.
apply Rmul_lt_cancel_r with (po n).
apply Rpos_IPR.

eapply Req_lt_compat_l; [ symmetry; apply Rmul_add_distr_r | ].
eapply Req_lt_compat_l; [ eapply Radd_eq_compat_r; symmetry; apply Rdiv_mul_r | ].
apply Rlt_trans with R1.
apply Ropp_lt_contravar_reciprocal.
eapply Req_lt_compat_r; [ rewrite Ropp_add | apply er ].
ring.

apply Rmul_lt_cancel_r with (Rinv (po n) (pop n)).
apply Rinv_0_lt_compat, Rpos_IPR.
apply (Req_lt_compat (Rinv (po n) (pop n)) e).
ring_simplify; reflexivity.
rewrite Rmul_assoc, (Rmul_comm e), Rinv_r, Rmul_1_l; reflexivity.
auto.

apply Rmul_lt_cancel_r with (po n).
apply Rpos_IPR.
apply Rlt_trans with (- R1).
apply Rmul_lt_cancel_r with (Rinv (po n) (pop n)).
apply Rinv_pos_compat, Rpos_IPR.
apply (Req_lt_compat (- e) (- Rinv (po n) (pop n))).
rewrite Rmul_assoc, Rinv_r, Rmul_1_r; reflexivity.
ring_simplify; reflexivity.
apply Ropp_lt_contravar; auto.

eapply Req_lt_compat_r; [ symmetry; apply Rmul_add_distr_r | ].
apply Ropp_lt_contravar_reciprocal.
eapply Req_lt_compat_r; [ symmetry; apply Ropp_involutive | ].
apply (Req_lt_compat (x × po n - IZR (Rup (x × po n))) R1).
rewrite Rdiv_mul_r.
ring_simplify; reflexivity.

reflexivity.

auto.
Qed.

End Rapprox.