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
|
Require Import ZArith Uint63 Floats.
Open Scope float_scope.
Definition three := Eval compute in of_uint63 3%uint63.
Definition nine := Eval compute in of_uint63 9%uint63.
Check (eq_refl : sqrt nine = three).
Check (eq_refl three <: sqrt nine = three).
Definition compute1 := Eval compute in sqrt nine.
Check (eq_refl : three = three).
Definition huge := Eval compute in Z.ldexp one (1023)%Z.
Definition tiny := Eval compute in Z.ldexp one (-1023)%Z.
Definition denorm := Eval compute in Z.ldexp one (-1074)%Z.
Goal (Prim2SF (sqrt huge) = SF64sqrt (Prim2SF huge)).
now compute. Undo. now vm_compute.
Qed.
Goal (Prim2SF (sqrt tiny) = SF64sqrt (Prim2SF tiny)).
now compute. Undo. now vm_compute.
Qed.
Goal (Prim2SF (sqrt denorm) = SF64sqrt (Prim2SF denorm)).
now compute. Undo. now vm_compute.
Qed.
Check (eq_refl : sqrt neg_zero = neg_zero).
Check (eq_refl neg_zero <: sqrt neg_zero = neg_zero).
Check (eq_refl neg_zero <<: sqrt neg_zero = neg_zero).
Check (eq_refl : sqrt zero = zero).
Check (eq_refl zero <: sqrt zero = zero).
Check (eq_refl zero <<: sqrt zero = zero).
Check (eq_refl : sqrt one = one).
Check (eq_refl one <: sqrt one = one).
Check (eq_refl one <<: sqrt one = one).
Check (eq_refl : sqrt (-one) = nan).
Check (eq_refl nan <: sqrt (-one) = nan).
Check (eq_refl nan <<: sqrt (-one) = nan).
Check (eq_refl : sqrt infinity = infinity).
Check (eq_refl infinity <: sqrt infinity = infinity).
Check (eq_refl infinity <<: sqrt infinity = infinity).
Check (eq_refl : sqrt neg_infinity = nan).
Check (eq_refl nan <: sqrt neg_infinity = nan).
Check (eq_refl nan <<: sqrt neg_infinity = nan).
Check (eq_refl : sqrt infinity = infinity).
Check (eq_refl infinity <: sqrt infinity = infinity).
Check (eq_refl infinity <<: sqrt infinity = infinity).
|
