1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
|
Require Import Bignums.BigZ.BigZ CRArith model.totalorder.QposMinMax
ARbigD ARbigQ ARQ ARtrans ARsign.
Definition myAR := ARbigD.
Definition answer (n : positive) (r : ARbigD) : bigZ :=
let m := iter_pos _ (Pmult 10) 1%positive n in
let (a, b) := (approximate r (Qpos2QposInf (1#m)) : bigD) * 'Zpos m in
BigZ.shiftl a b.
(* To avoid timing the printing mechanism *)
Definition no_answer (n : positive) (r : myAR) :=
let m := iter_pos _ (Pmult 10) 1%positive n in
let _ := approximate r (Qpos2QposInf (1#m)) in
tt.
(* xkcd.org/217 *)
Definition xkcd : myAR := (ARexp ARpi)-ARpi.
Time Eval vm_compute in (answer 10 xkcd).
Example xkcd217A : ARltT xkcd ('20%Z).
Proof. Time AR_solve_ltT (-8)%Z. Defined.
(* Many of the following expressions are taken from the "Many Digits friendly competition" problem set *)
(* Instance resolution takes 3s *)
Time Definition P01 : myAR := ARsin (ARsin (AQsin 1)).
Time Eval vm_compute in (answer 500 P01).
Time Eval vm_compute in (no_answer 500 P01).
Definition P02 : myAR := ARsqrt (ARcompress ARpi).
Time Eval vm_compute in (answer 500 P02).
Definition P03 : myAR := ARsin (AQexp 1).
Time Eval vm_compute in (answer 500 P03).
Definition P04 : myAR := ARexp (ARcompress (ARpi * AQsqrt ('163%Z))).
Time Eval vm_compute in (answer 500 P04).
Definition P05 : myAR := ARexp (ARexp (AQexp 1)).
Time Eval vm_compute in (answer 500 P05).
Definition P07 : myAR := AQexp ('1000%Z).
Time Eval vm_compute in (answer 2000 P07).
Definition P08 : myAR := AQcos ('(10^50)%Z).
Time Eval vm_compute in (answer 2000 P08).
Definition C02_prf : ARapartT (ARpi : myAR) (0 : myAR).
Proof. AR_solve_apartT (-8)%Z. Defined.
Definition C02 : myAR := ARsqrt (AQexp 1 * ARinvT ARpi C02_prf).
Time Eval vm_compute in (answer 250 C02).
Definition C03 : myAR := ARsin (ARcompress ((AQexp 1 + 1) ^ (3:N))).
Time Eval vm_compute in (answer 500 C03).
Definition C04 : myAR := ARexp (ARcompress (ARpi * AQsqrt ('2011%Z))).
Time Eval vm_compute in (answer 500 C04).
Definition C05 : myAR := ARexp (ARexp (ARsqrt (AQexp 1))).
Time Eval vm_compute in (answer 500 C05).
(* slow *) (*
Definition C07 : myAR := ARpi ^ 1000%N.
Time Eval vm_compute in (answer 50 C07).
*)
Definition ARtest1 : myAR := ARpi.
Time Eval vm_compute in (answer 1500 ARtest1).
Definition ARtest2 : myAR := ARarctan (ARcompress ARpi).
Time Eval vm_compute in (answer 100 ARtest2).
Definition ARtest3 : myAR := ARsqrt 2.
Time Eval vm_compute in (answer 1000 ARtest3).
Definition ARtest4 : myAR := ARsin ARpi.
Time Eval vm_compute in (answer 500 ARtest4).
|
