CoRN.reals.faster.ARQ
Require Import
Program QArith Qdlog ZArith Qpossec Compress
MetricMorphisms Qmetric ARArith
theory.int_pow theory.nat_pow
stdlib_rationals stdlib_binary_integers.
Instance Q_approx: AppApprox Q := λ x k,
match k with
| Zneg p ⇒ approximateQ x (2 ^ p)
| _ ⇒ x
end.
Lemma Q_approx_correct (x : Q) (k : Z) : Qball (2 ^ k) (app_approx x k) x.
Proof.
destruct k as [|p|]; try reflexivity.
unfold app_approx, Q_approx.
setoid_replace (2 ^ Zneg p)%Qpos with (1 # (2 ^ p))%Qpos.
now apply ball_sym, approximateQ_correct.
change (/ Qpower (2%Z) p == 1 # 2 ^ p).
rewrite <-Qpower.Zpower_Qpower; auto with zarith.
now rewrite <- Zpower_Ppow.
Qed.
Instance Q_approx_div: AppDiv Q := λ x y k, app_approx (x / y) k.
Instance inject_Q_Q: Cast Q Q_as_MetricSpace := Datatypes.id.
Instance inverse_Q_Q: AppInverse inject_Q_Q := λ x ε, app_approx x (Qdlog2 ε).
Instance: AppRationals Q.
Proof.
split; try apply _.
repeat (split; try apply _).
split; try apply _. intros.
apply ball_weak_le with (2 ^ Qdlog2 ε)%Qpos.
now apply (Qpos_dlog2_spec ε).
now apply Q_approx_correct.
intros. now apply Q_approx_correct.
intros. now apply Q_approx_correct.
Qed.
Notation ARQ := (AR (AQ:=Q)).
Program QArith Qdlog ZArith Qpossec Compress
MetricMorphisms Qmetric ARArith
theory.int_pow theory.nat_pow
stdlib_rationals stdlib_binary_integers.
Instance Q_approx: AppApprox Q := λ x k,
match k with
| Zneg p ⇒ approximateQ x (2 ^ p)
| _ ⇒ x
end.
Lemma Q_approx_correct (x : Q) (k : Z) : Qball (2 ^ k) (app_approx x k) x.
Proof.
destruct k as [|p|]; try reflexivity.
unfold app_approx, Q_approx.
setoid_replace (2 ^ Zneg p)%Qpos with (1 # (2 ^ p))%Qpos.
now apply ball_sym, approximateQ_correct.
change (/ Qpower (2%Z) p == 1 # 2 ^ p).
rewrite <-Qpower.Zpower_Qpower; auto with zarith.
now rewrite <- Zpower_Ppow.
Qed.
Instance Q_approx_div: AppDiv Q := λ x y k, app_approx (x / y) k.
Instance inject_Q_Q: Cast Q Q_as_MetricSpace := Datatypes.id.
Instance inverse_Q_Q: AppInverse inject_Q_Q := λ x ε, app_approx x (Qdlog2 ε).
Instance: AppRationals Q.
Proof.
split; try apply _.
repeat (split; try apply _).
split; try apply _. intros.
apply ball_weak_le with (2 ^ Qdlog2 ε)%Qpos.
now apply (Qpos_dlog2_spec ε).
now apply Q_approx_correct.
intros. now apply Q_approx_correct.
intros. now apply Q_approx_correct.
Qed.
Notation ARQ := (AR (AQ:=Q)).