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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
|
Require Import ZArith Uint63 Floats.
Open Scope float_scope.
Definition f0 := zero.
Definition f1 := neg_zero.
Definition f2 := Eval compute in Z.ldexp one 0.
Definition f3 := Eval compute in -f1.
(* smallest positive float *)
Definition f4 := Eval compute in Z.ldexp one (-1074).
Definition f5 := Eval compute in -f3.
Definition f6 := infinity.
Definition f7 := neg_infinity.
Definition f8 := Eval compute in Z.ldexp one (-1).
Definition f9 := Eval compute in -f8.
Definition f10 := Eval compute in of_uint63 42.
Definition f11 := Eval compute in -f10.
(* max float *)
Definition f12 := Eval compute in Z.ldexp (of_uint63 9007199254740991) 1024.
Definition f13 := Eval compute in -f12.
(* smallest positive normalized float *)
Definition f14 := Eval compute in Z.ldexp one (-1022).
Definition f15 := Eval compute in -f14.
Check (eq_refl : Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
Check (eq_refl : Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
Check (eq_refl : Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
Check (eq_refl : Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
Check (eq_refl : Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
Check (eq_refl : Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
Check (eq_refl : Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
Check (eq_refl : Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
Check (eq_refl : Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
Check (eq_refl : Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
Check (eq_refl : Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
Check (eq_refl : Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
Check (eq_refl : Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
Check (eq_refl : Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
Check (eq_refl : Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
Check (eq_refl : Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
Check (eq_refl : Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
Check (eq_refl : Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
Check (eq_refl : Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
Check (eq_refl : Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
Check (eq_refl : Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
Check (eq_refl : Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
Check (eq_refl : Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
Check (eq_refl : Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
Check (eq_refl : Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
Check (eq_refl : Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
Check (eq_refl : Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
Check (eq_refl : Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
Check (eq_refl : Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
Check (eq_refl : Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
Check (eq_refl : Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
Check (eq_refl : Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
Check (eq_refl (SF64succ (Prim2SF f0)) <: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
Check (eq_refl (SF64pred (Prim2SF f0)) <: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
Check (eq_refl (SF64succ (Prim2SF f1)) <: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
Check (eq_refl (SF64pred (Prim2SF f1)) <: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
Check (eq_refl (SF64succ (Prim2SF f2)) <: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
Check (eq_refl (SF64pred (Prim2SF f2)) <: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
Check (eq_refl (SF64succ (Prim2SF f3)) <: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
Check (eq_refl (SF64pred (Prim2SF f3)) <: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
Check (eq_refl (SF64succ (Prim2SF f4)) <: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
Check (eq_refl (SF64pred (Prim2SF f4)) <: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
Check (eq_refl (SF64succ (Prim2SF f5)) <: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
Check (eq_refl (SF64pred (Prim2SF f5)) <: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
Check (eq_refl (SF64succ (Prim2SF f6)) <: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
Check (eq_refl (SF64pred (Prim2SF f6)) <: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
Check (eq_refl (SF64succ (Prim2SF f7)) <: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
Check (eq_refl (SF64pred (Prim2SF f7)) <: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
Check (eq_refl (SF64succ (Prim2SF f8)) <: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
Check (eq_refl (SF64pred (Prim2SF f8)) <: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
Check (eq_refl (SF64succ (Prim2SF f9)) <: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
Check (eq_refl (SF64pred (Prim2SF f9)) <: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
Check (eq_refl (SF64succ (Prim2SF f10)) <: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
Check (eq_refl (SF64pred (Prim2SF f10)) <: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
Check (eq_refl (SF64succ (Prim2SF f11)) <: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
Check (eq_refl (SF64pred (Prim2SF f11)) <: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
Check (eq_refl (SF64succ (Prim2SF f12)) <: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
Check (eq_refl (SF64pred (Prim2SF f12)) <: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
Check (eq_refl (SF64succ (Prim2SF f13)) <: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
Check (eq_refl (SF64pred (Prim2SF f13)) <: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
Check (eq_refl (SF64succ (Prim2SF f14)) <: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
Check (eq_refl (SF64pred (Prim2SF f14)) <: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
Check (eq_refl (SF64succ (Prim2SF f15)) <: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
Check (eq_refl (SF64pred (Prim2SF f15)) <: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
Check (eq_refl (SF64succ (Prim2SF f0)) <<: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
Check (eq_refl (SF64pred (Prim2SF f0)) <<: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
Check (eq_refl (SF64succ (Prim2SF f1)) <<: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
Check (eq_refl (SF64pred (Prim2SF f1)) <<: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
Check (eq_refl (SF64succ (Prim2SF f2)) <<: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
Check (eq_refl (SF64pred (Prim2SF f2)) <<: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
Check (eq_refl (SF64succ (Prim2SF f3)) <<: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
Check (eq_refl (SF64pred (Prim2SF f3)) <<: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
Check (eq_refl (SF64succ (Prim2SF f4)) <<: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
Check (eq_refl (SF64pred (Prim2SF f4)) <<: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
Check (eq_refl (SF64succ (Prim2SF f5)) <<: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
Check (eq_refl (SF64pred (Prim2SF f5)) <<: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
Check (eq_refl (SF64succ (Prim2SF f6)) <<: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
Check (eq_refl (SF64pred (Prim2SF f6)) <<: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
Check (eq_refl (SF64succ (Prim2SF f7)) <<: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
Check (eq_refl (SF64pred (Prim2SF f7)) <<: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
Check (eq_refl (SF64succ (Prim2SF f8)) <<: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
Check (eq_refl (SF64pred (Prim2SF f8)) <<: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
Check (eq_refl (SF64succ (Prim2SF f9)) <<: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
Check (eq_refl (SF64pred (Prim2SF f9)) <<: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
Check (eq_refl (SF64succ (Prim2SF f10)) <<: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
Check (eq_refl (SF64pred (Prim2SF f10)) <<: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
Check (eq_refl (SF64succ (Prim2SF f11)) <<: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
Check (eq_refl (SF64pred (Prim2SF f11)) <<: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
Check (eq_refl (SF64succ (Prim2SF f12)) <<: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
Check (eq_refl (SF64pred (Prim2SF f12)) <<: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
Check (eq_refl (SF64succ (Prim2SF f13)) <<: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
Check (eq_refl (SF64pred (Prim2SF f13)) <<: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
Check (eq_refl (SF64succ (Prim2SF f14)) <<: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
Check (eq_refl (SF64pred (Prim2SF f14)) <<: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
Check (eq_refl (SF64succ (Prim2SF f15)) <<: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
Check (eq_refl (SF64pred (Prim2SF f15)) <<: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
Check (eq_refl : next_up nan = nan).
Check (eq_refl : next_down nan = nan).
Check (eq_refl : next_up neg_infinity = -0x1.fffffffffffffp+1023).
Check (eq_refl : next_down neg_infinity = neg_infinity).
Check (eq_refl : next_up (-0x1.fffffffffffffp+1023) = -0x1.ffffffffffffep+1023).
Check (eq_refl : next_down (-0x1.fffffffffffffp+1023) = neg_infinity).
Check (eq_refl : next_up (-0x1.ffffffffffffap+1023) = -0x1.ffffffffffff9p+1023).
Check (eq_refl : next_down (-0x1.ffffffffffffap+1023) = -0x1.ffffffffffffbp+1023).
Check (eq_refl : next_up (-0x1.fffffffffffff) = -0x1.ffffffffffffe).
Check (eq_refl : next_down (-0x1.fffffffffffff) = -0x1p+1).
Check (eq_refl : next_up (-0x1p1) = -0x1.fffffffffffff).
Check (eq_refl : next_down (-0x1p1) = -0x1.0000000000001p+1).
Check (eq_refl : next_up (-0x1p-1022) = -0x0.fffffffffffffp-1022).
Check (eq_refl : next_down (-0x1p-1022) = -0x1.0000000000001p-1022).
Check (eq_refl : next_up (-0x0.fffffffffffffp-1022) = -0x0.ffffffffffffep-1022).
Check (eq_refl : next_down (-0x0.fffffffffffffp-1022) = -0x1p-1022).
Check (eq_refl : next_up (-0x0.01p-1022) = -0x0.00fffffffffffp-1022).
Check (eq_refl : next_down (-0x0.01p-1022) = -0x0.0100000000001p-1022).
Check (eq_refl : next_up (-0x0.0000000000001p-1022) = -0).
Check (eq_refl : next_down (-0x0.0000000000001p-1022) = -0x0.0000000000002p-1022).
Check (eq_refl : next_up (-0) = 0x0.0000000000001p-1022).
Check (eq_refl : next_down (-0) = -0x0.0000000000001p-1022).
Check (eq_refl : next_up 0 = 0x0.0000000000001p-1022).
Check (eq_refl : next_down 0 = -0x0.0000000000001p-1022).
Check (eq_refl : next_up 0x0.0000000000001p-1022 = 0x0.0000000000002p-1022).
Check (eq_refl : next_down 0x0.0000000000001p-1022 = 0).
Check (eq_refl : next_up 0x0.01p-1022 = 0x0.0100000000001p-1022).
Check (eq_refl : next_down 0x0.01p-1022 = 0x0.00fffffffffffp-1022).
Check (eq_refl : next_up 0x0.fffffffffffffp-1022 = 0x1p-1022).
Check (eq_refl : next_down 0x0.fffffffffffffp-1022 = 0x0.ffffffffffffep-1022).
Check (eq_refl : next_up 0x1p-1022 = 0x1.0000000000001p-1022).
Check (eq_refl : next_down 0x1p-1022 = 0x0.fffffffffffffp-1022).
Check (eq_refl : next_up 0x1p1 = 0x1.0000000000001p+1).
Check (eq_refl : next_down 0x1p1 = 0x1.fffffffffffff).
Check (eq_refl : next_up 0x1.fffffffffffff = 0x1p+1).
Check (eq_refl : next_down 0x1.fffffffffffff = 0x1.ffffffffffffe).
Check (eq_refl : next_up 0x1.ffffffffffffap+1023 = 0x1.ffffffffffffbp+1023).
Check (eq_refl : next_down 0x1.ffffffffffffap+1023 = 0x1.ffffffffffff9p+1023).
Check (eq_refl : next_up 0x1.fffffffffffffp+1023 = infinity).
Check (eq_refl : next_down 0x1.fffffffffffffp+1023 = 0x1.ffffffffffffep+1023).
Check (eq_refl : next_up infinity = infinity).
Check (eq_refl : next_down infinity = 0x1.fffffffffffffp+1023).
|
