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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
Require Import
MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations
MathClasses.implementations.dyadics MathClasses.implementations.fast_integers.
Section wolfram_sqrt.
Context `{Integers Z} `{!RingOrder oZ} `{!TotalOrder oZ}
`{precedes_dec : ∀ (x y : Z), Decision (x ≤ y)}
`{!NatPowSpec Z (Z⁺) pw} `{!ShiftLSpec Z (Z⁺) sl}.
Fixpoint root_loop (x : Dyadic Z) (n : nat) : Dyadic Z * Dyadic Z :=
match n with
| O => (x, 0)
| S n => let (r, s) := root_loop x n in
if decide_rel (≤) (s + 1) r
then ((r - (s + 1)) ≪ 2, (s + 2) ≪ 1)
else (r ≪ 2, s ≪ 1)
end.
End wolfram_sqrt.
Definition fast_root_loop := root_loop (Z:=fastZ).
Let n : nat := Eval vm_compute in (10 * 10 * 10 * 10)%nat.
Time Eval vm_compute in (snd (fast_root_loop 2 n)).
Time Eval vm_compute in (
(fun _ _ _ _ _ _ _ _ _ _ => true)
(snd (fast_root_loop 2 n))
(snd (fast_root_loop 2 n))
(snd (fast_root_loop 2 n))
(snd (fast_root_loop 2 n))
(snd (fast_root_loop 2 n))
(snd (fast_root_loop 2 n))
(snd (fast_root_loop 2 n))
(snd (fast_root_loop 2 n))
(snd (fast_root_loop 2 n))
(snd (fast_root_loop 2 n))).
Require Import BigZ.
Open Scope bigZ_scope.
Notation bigD := (Dyadic bigZ).
Definition BigD_0 : bigD := (0 ▼ 0).
Definition BigD_1 : bigD := (1 ▼ 0).
Definition BigD_2 : bigD := (2 ▼ 0).
Definition BigD_plus (x y : bigD) : bigD :=
match BigZ.compare (expo x) (expo y) with
| Gt => BigZ.shiftl (mant x) (expo x - expo y) + mant y ▼ BigZ.min (expo x) (expo y)
| _ => mant x + BigZ.shiftl (mant y) (expo y - expo x) ▼ BigZ.min (expo x) (expo y)
end.
Definition BigD_opp (x : bigD) : bigD := -mant x ▼ expo x.
Definition BigD_mult (x y : bigD) : bigD := mant x * mant y ▼ expo x + expo y.
Definition BigD_shiftl (x : bigD) (n : bigZ) : bigD := mant x ▼ expo x + n.
Definition BigD_compare (x y : bigD) : comparison :=
match BigZ.compare (expo x) (expo y) with
| Gt => BigZ.compare (BigZ.shiftl (mant x) (expo x - expo y)) (mant y)
| _ => BigZ.compare (mant x) (BigZ.shiftl (mant y) (expo y - expo x))
end.
Fixpoint root_loop_alt (x : bigD) (n : nat) : bigD * bigD :=
match n with
| O => (x, BigD_0)
| S n => let (r, s) := root_loop_alt x n in
match BigD_compare (BigD_plus s BigD_1) r with
| Gt => (BigD_shiftl r 2, BigD_shiftl s 1)
| _ => (BigD_shiftl (BigD_plus r (BigD_opp (BigD_plus s BigD_1))) 2, BigD_shiftl (BigD_plus s BigD_2) 1)
end
end.
Time Eval vm_compute in (mant (snd (root_loop_alt BigD_2 n))).
Time Eval vm_compute in (
(fun _ _ _ _ _ _ _ _ _ _ => true)
(snd (root_loop_alt BigD_2 n))
(snd (root_loop_alt BigD_2 n))
(snd (root_loop_alt BigD_2 n))
(snd (root_loop_alt BigD_2 n))
(snd (root_loop_alt BigD_2 n))
(snd (root_loop_alt BigD_2 n))
(snd (root_loop_alt BigD_2 n))
(snd (root_loop_alt BigD_2 n))
(snd (root_loop_alt BigD_2 n))
(snd (root_loop_alt BigD_2 n))).
Definition BigD_4 : bigD := (4 ▼ 0).
Fixpoint root_loop_alt_mult (x : bigD) (n : nat) : bigD * bigD :=
match n with
| O => (x, BigD_0)
| S n => let (r, s) := root_loop_alt_mult x n in
match BigD_compare (BigD_plus s BigD_1) r with
| Gt => (BigD_mult BigD_4 r, BigD_mult BigD_2 s)
| _ => (BigD_mult BigD_4 (BigD_plus r (BigD_opp (BigD_plus s BigD_1))), BigD_mult BigD_2 (BigD_plus s BigD_2))
end
end.
Time Eval vm_compute in (mant (snd (root_loop_alt_mult BigD_2 n))).
Time Eval vm_compute in (
(fun _ _ _ _ _ _ _ _ _ _ => true)
(snd (root_loop_alt_mult BigD_2 n))
(snd (root_loop_alt_mult BigD_2 n))
(snd (root_loop_alt_mult BigD_2 n))
(snd (root_loop_alt_mult BigD_2 n))
(snd (root_loop_alt_mult BigD_2 n))
(snd (root_loop_alt_mult BigD_2 n))
(snd (root_loop_alt_mult BigD_2 n))
(snd (root_loop_alt_mult BigD_2 n))
(snd (root_loop_alt_mult BigD_2 n))
(snd (root_loop_alt_mult BigD_2 n))).
|
