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
|
Require Import ZArith Uint63 Floats.
Open Scope float_scope.
Definition two := Eval compute in of_uint63 2%uint63.
Definition three := Eval compute in of_uint63 3%uint63.
Definition six := Eval compute in of_uint63 6%uint63.
Check (eq_refl : six / three = two).
Check (eq_refl two <: six / three = two).
Check (eq_refl two <<: six / three = two).
Definition compute1 := Eval compute in six / three.
Check (eq_refl compute1 : two = two).
Definition huge := Eval compute in Z.ldexp one 1023%Z.
Definition tiny := Eval compute in Z.ldexp one (-1023)%Z.
Check (eq_refl : huge / tiny = infinity).
Check (eq_refl infinity <: huge / tiny = infinity).
Check (eq_refl infinity <<: huge / tiny = infinity).
Definition compute2 := Eval compute in huge / tiny.
Check (eq_refl compute2 : infinity = infinity).
Check (eq_refl : huge / huge = one).
Check (eq_refl one <: huge / huge = one).
Check (eq_refl one <<: huge / huge = one).
Definition compute3 := Eval compute in huge / huge.
Check (eq_refl compute3 : one = one).
Check (eq_refl : one / nan = nan).
Check (eq_refl nan <: one / nan = nan).
Check (eq_refl nan <<: one / nan = nan).
Definition compute4 := Eval compute in one / nan.
Check (eq_refl compute4 : nan = nan).
Check (eq_refl : infinity / infinity = nan).
Check (eq_refl nan <: infinity / infinity = nan).
Check (eq_refl nan <<: infinity / infinity = nan).
Definition compute5 := Eval compute in infinity / infinity.
Check (eq_refl compute5 : nan = nan).
Check (eq_refl : infinity / neg_infinity = nan).
Check (eq_refl nan <: infinity / neg_infinity = nan).
Check (eq_refl nan <<: infinity / neg_infinity = nan).
Definition compute6 := Eval compute in infinity / neg_infinity.
Check (eq_refl compute6 : nan = nan).
Check (eq_refl : zero / zero = nan).
Check (eq_refl nan <: zero / zero = nan).
Check (eq_refl nan <<: zero / zero = nan).
Check (eq_refl : neg_zero / zero = nan).
Check (eq_refl nan <: neg_zero / zero = nan).
Check (eq_refl nan <<: neg_zero / zero = nan).
Check (eq_refl : huge / neg_infinity = neg_zero).
Check (eq_refl neg_zero <: huge / neg_infinity = neg_zero).
Check (eq_refl neg_zero <<: huge / neg_infinity = neg_zero).
Check (eq_refl : one / tiny = huge).
Check (eq_refl huge <: one / tiny = huge).
Check (eq_refl huge <<: one / tiny = huge).
Check (eq_refl : one / huge = tiny).
Check (eq_refl tiny <: one / huge = tiny).
Check (eq_refl tiny <<: one / huge = tiny).
Check (eq_refl : zero / huge = zero).
Check (eq_refl zero <: zero / huge = zero).
Check (eq_refl zero <<: zero / huge = zero).
Check (eq_refl : zero / (-huge) = neg_zero).
Check (eq_refl neg_zero <: zero / (-huge) = neg_zero).
Check (eq_refl neg_zero <<: zero / (-huge) = neg_zero).
Check (eq_refl : tiny / one = tiny).
Check (eq_refl tiny <: tiny / one = tiny).
Check (eq_refl tiny <<: tiny / one = tiny).
Check (eq_refl : huge / one = huge).
Check (eq_refl huge <: huge / one = huge).
Check (eq_refl huge <<: huge / one = huge).
Check (eq_refl : infinity / one = infinity).
Check (eq_refl infinity <: infinity / one = infinity).
Check (eq_refl infinity <<: infinity / one = infinity).
Check (eq_refl : zero / infinity = zero).
Check (eq_refl zero <: zero / infinity = zero).
Check (eq_refl zero <<: zero / infinity = zero).
Check (eq_refl : infinity / zero = infinity).
Check (eq_refl infinity <: infinity / zero = infinity).
Check (eq_refl infinity <<: infinity / zero = infinity).
|
