CoRN.examples.RealFast

Require Import CRtrans.

Open Local Scope Q_scope.


Definition star := @refl_equal _ Lt.
Notation "∗" := star.


Definition answer (n:positive) (r:CR) : Z :=
 let m := (iter_pos n _ (Pmult 10) 1%positive) in
 let (a,b) := (approximate r (1#m)%Qpos)*m in
 Zdiv a b.


Time Eval vm_compute in answer 10 ('7)%CR.
Time Eval vm_compute in answer 10 ('(1#2))%CR.
Time Eval vm_compute in answer 50 (CRpi)%CR.
Time Eval vm_compute in answer 50 (rational_exp 1)%CR.
Time Eval vm_compute in answer 50 (rational_exp (-(1)))%CR.
Time Eval vm_compute in answer 20 (exp (compress CRpi) - CRpi)%CR.

Time Eval vm_compute in answer 20 (sin (compress (sin (compress (rational_sin 1)))))%CR.
Time Eval vm_compute in answer 20 (CRsqrt (compress CRpi))%CR.
Time Eval vm_compute in answer 20 (sin (compress (rational_exp 1)))%CR.
Time Eval vm_compute in answer 1 (exp (compress (exp (compress (rational_exp 1)))))%CR.

Time Eval vm_compute in answer 20 (CRsqrt (compress (rational_exp (1))*compress (CRinv_pos (3#1) CRpi)))%CR.
Time Eval vm_compute in answer 20 (sin (compress (CRpower_positive 3 (translate (1#1) (compress (rational_exp (1)))))))%CR.
Time Eval vm_compute in answer 10 (rational_sin (10^14))%CR.
Time Eval vm_compute in answer 10 (exp (compress (exp (compress (rational_exp (1#2))))))%CR.

Require Import CRsign.

Example xkcd217A : (exp (CRpi) - CRpi < '(20%Z:Q))%CR.
unfold CRlt.
Time CR_solve_pos (1#1000)%Qpos.
Qed.

Require Import Exponential.
Require Import Pi.


Example xkcd217B : (Exp Pi [-] Pi [<] (nring 20)).
Time IR_solve_ineq (1#1000)%Qpos.
Qed.

Require Import MultivariatePolynomials.