You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Floating-point numbers are a an approximation of the real numbers that are efficiently implemented in computer hardware.
27
27
Computations that use floating-point numbers are very efficient; however, the nature of the way that they approximate the real numbers is complex, with many corner cases.
28
-
The IEEE 754 standard, which defines the floating-point format that is used on modern computers, allows hardware designers to make certain choices, and real systems differ in these small details.
28
+
The IEEE 754 standard, which defines the floating-point format that is used on modern computers, allows hardware designers and programming language implementations to make certain choices, and real systems differ in these small details.
29
+
Any given combination of hardware, operating system, C compiler, library versions, and even compilation flags can result in different behavior.
29
30
For example, there are many distinct bit representations of `NaN`, the indicator that a result is undefined, and some platforms differ with respect to _which_ `NaN` is returned from adding two `NaN`s.
30
31
31
-
Lean exposes the underlying platform's floating-point values for use in programming, but they are not encoded inLean's logic.
32
-
They are represented by an opaque type.
33
-
This means that the {tech}[kernel] is not capable of computing with or reasoning about floating-point values without additional {ref "axioms"}[axioms].
34
-
A consequence of this is that equality of floating-point numbers is not decidable.
35
-
Furthermore, comparisons between floating-point values are decidable, but the code that does so is opaque; in practice, the decision procedure can only be used incompiled code.
32
+
To enable reasoning about floating-point numbers, Lean exposes a logical model of {name}`Float` that is used inproofs.
33
+
In particular, {name}`Float` and {name}`Float32` are implemented as wrappers around the logical model.
34
+
In compiled code, this logical model is replaced by efficient native code.
35
+
Differences between platforms are resolved by choosing specific representations (forexample, all `NaN` values are replaced by a single canonical `NaN` when any operation requests a bit representation) and by modeling only the subset of floating-point operations that are implemented identically on all supported platforms.
36
+
Other operations, such as trigonometric functions, are represented as opaque functions inLean's logic.
36
37
37
-
Lean provides two floating-point types: {name}`Float` represents 64-bit floating point values, while {name}`Float32` represents 32-bit floating point values.
38
+
The logical model is extensively empirically tested against the floating-point operations on all supported platforms.
39
+
As long as FFI code does not modify the floating-point environment, Lean's runtime floating-point primitives match the model's specification.
40
+
41
+
{docstring Float}
42
+
43
+
{docstring Float32}
44
+
45
+
# Logical Model
46
+
47
+
Lean provides two floating-point types: {name}`Float` represents 64-bit floating-point values, while {name}`Float32` represents 32-bit floating-point values.
38
48
The precision of {name}`Float` does not vary based on the platform that Lean is running on.
39
49
50
+
## Model Details
51
+
52
+
The logical models of {lean}`Float` and {lean}`Float32` consist of unsigned integers with validity predicates.
53
+
Each defined operation first interprets the integer into a {lean}`Float.Model.UnpackedFloat`, which is a higher-level model that is not specific to a bit width.
54
+
Then, the defined operation is implemented in terms of {name Float.Model.UnpackedFloat}`UnpackedFloat`, and the result is re-packed.
55
+
These definitions constitute a _logical specification_ designed for reasoning.
56
+
Although they can be executed, they will run significantly slower than native code.
57
+
Not all operations are defined; some are instead opaque functions whose behavior cannot be reasoned about in Lean's logic.
58
+
59
+
This model is not intended to serve as the basis for a more extensive floating-point library.
60
+
It exists only to support the reasoning tools available in Lean and is not suitable for larger-scale development.
61
+
Do not use this model as the basis of a more extensive floating-point library.
62
+
Instead, implement a suitable model, prove the equivalence of the its operations to this model, and then transfer lemmas using the equivalence.
63
+
64
+
{docstring Float.Model}
65
+
66
+
{docstring Float32.Model}
67
+
68
+
{docstring Float.Model.pack}
69
+
70
+
{docstring Float32.Model.pack}
71
+
72
+
{docstring Float.Model.unpack}
73
+
74
+
{docstring Float32.Model.unpack}
75
+
76
+
{docstring Float.Model.UnpackedFloat}
77
+
78
+
## Model Operations
79
+
80
+
The following operations are specified for floating-point values.
81
+
Other operators are represented byopaque functions and do not reduce in the kernel.
:::example"No Kernel Reasoning About Floating-Point Numbers"
123
+
{docstring Float.Model.UnpackedFloat.ofInt16}
124
+
125
+
{docstring Float.Model.UnpackedFloat.toInt32}
126
+
127
+
{docstring Float.Model.UnpackedFloat.ofInt32}
128
+
129
+
{docstring Float.Model.UnpackedFloat.toInt64}
130
+
131
+
{docstring Float.Model.UnpackedFloat.ofInt64}
132
+
133
+
{docstring Float.Model.UnpackedFloat.toISize}
134
+
135
+
{docstring Float.Model.UnpackedFloat.ofISize}
136
+
137
+
{docstring Float.Model.UnpackedFloat.toUInt8}
138
+
139
+
{docstring Float.Model.UnpackedFloat.ofUInt8}
140
+
141
+
{docstring Float.Model.UnpackedFloat.toUInt16}
142
+
143
+
{docstring Float.Model.UnpackedFloat.ofUInt16}
144
+
145
+
{docstring Float.Model.UnpackedFloat.toUInt32}
146
+
147
+
{docstring Float.Model.UnpackedFloat.ofUInt32}
148
+
149
+
{docstring Float.Model.UnpackedFloat.toUInt64}
150
+
151
+
{docstring Float.Model.UnpackedFloat.ofUInt64}
152
+
153
+
{docstring Float.Model.UnpackedFloat.toUSize}
154
+
155
+
{docstring Float.Model.UnpackedFloat.ofUSize}
156
+
157
+
:::example"Kernel Reasoning"
47
158
The Lean kernel can compare expressions of type {lean}`Float` for syntactic equality, so {lean (type := "Float")}`0.0` is definitionally equal to itself.
48
159
```lean
49
160
example : (0.0 : Float) = (0.0 : Float) := by rfl
50
161
```
51
162
52
-
Terms that require reduction to become syntactically equal cannot be checked by the kernel:
53
-
```lean +error (name := zeroPlusZero)
163
+
Additionally, terms that require reduction to become syntactically equal can be checked by the kernel when they use only operations that are modeled in Lean's logic:
164
+
```lean
54
165
example : (0.0 : Float) = (0.0 + 0.0 : Float) := by rfl
55
166
```
56
-
```leanOutput zeroPlusZero
57
-
Tactic `rfl` failed: The left-hand side
58
-
0.0
59
-
is not definitionally equal to the right-hand side
60
-
0.0 + 0.0
61
-
62
-
⊢ 0.0 = 0.0 + 0.0
63
-
```
64
-
65
-
Similarly, the kernel cannot evaluate {lean}`Bool`-valued comparisons of floating-point numbers while checking definitional equality:
66
-
```lean +error (name := zeroPlusZero') -keep
67
-
theoremFloat.zero_eq_zero_plus_zero :
68
-
((0.0 : Float) == (0.0 + 0.0 : Float)) = true :=
69
-
by rfl
167
+
The kernel cannot reduce terms that use operations that are not directly modeled, such as trigonometric functions:
168
+
```lean (name := sin0) +error
169
+
example : (0.0 : Float).sin = (0.0 : Float) := by rfl
70
170
```
71
-
```leanOutput zeroPlusZero'
171
+
```leanOutput sin0
72
172
Tactic `rfl` failed: The left-hand side
73
-
0.0 == 0.0 +0.0
173
+
Float.sin0.0
74
174
is not definitionally equal to the right-hand side
75
-
true
175
+
0.0
76
176
77
-
⊢ (0.0 == 0.0+0.0) = true
177
+
⊢ Float.sin 0.0=0.0
78
178
```
79
179
80
180
81
181
However, the {tactic}`native_decide` tactic can invoke the underlying platform's floating-point primitives that are used by Lean for run-time programs:
@@ -178,15 +280,6 @@ Floating-point numbers fall into one of three categories:
178
280
{docstring Float32.isFinite}
179
281
180
282
181
-
## Syntax
182
-
183
-
These operations exist to support the {inst}`OfScientific Float` and {inst}`OfScientific Float32` instances and are normally invoked indirectly as a result of a literal value.
184
-
185
-
{docstring Float.ofScientific}
186
-
187
-
{docstring Float32.ofScientific}
188
-
189
-
190
283
## Conversions
191
284
192
285
{docstring Float.toBits}
@@ -253,10 +346,6 @@ These operations exist to support the {inst}`OfScientific Float` and {inst}`OfSc
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?v=4&size=40){kind=avatar}
0 commit comments