CoRN.examples.IntegrationExamples

Require Import Integration.
Require Import AbstractIntegration.
Require SimpleIntegration.
Require Import CRtrans.
Require QnonNeg.
Import QnonNeg.notations.


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 3 (Integrate sin_uc 3 (1#2)).

Time Eval vm_compute in answer 3 (ContinuousSup01 cos_uc).

Time Eval vm_compute in answer 3 (ContinuousSup01 Cunit).


Definition sinsquare:= (uc_compose (CRpower_positive_bounded 2 (1#1)) sin_uc).
Definition quartersinsquare:=(uc_compose (scale (1#4)) sinsquare).
Definition body:=(uc_compose (translate 1) quartersinsquare).
Definition rootbody:=(uc_compose CRsqrt body).
Time Eval vm_compute in answer 1 (Integrate01 rootbody).