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
{{ message }}
This repository was archived by the owner on Jan 5, 2025. It is now read-only.
There are, however, some important exceptions to this rule.
10
19
A number of types are treated specially by the compiler.
11
20
For example, the type `UInt32` is defined as `Fin (2 ^ 32)`, but it is replaced at run-time with an actual native implementation based on machine words.
12
21
Similarly, even though the definition of `Nat` suggests an implementation similar to `List Unit`, the actual run-time representation uses immediate machine words for sufficiently-small numbers and an efficient arbitrary-precision arithmetic library for larger numbers.
13
22
The Lean compiler translates from definitions that use pattern matching into the appropriate operations for this representation, and calls to operations like addition and subtraction are mapped to fast operations from the underlying arithmetic library.
14
23
After all, addition should not take time linear in the size of the addends.
The fact that some types have special representations also means that care is needed when working with them.
17
30
Most of these types consist of a `structure` that is treated specially by the compiler.
18
31
With these structures, using the constructor or the field accessors directly can trigger an expensive conversion from an efficient representation to a slow one that is convenient for proofs.
@@ -22,21 +35,36 @@ Arrays are represented similarly.
22
35
From the logical perspective, arrays are structures that contain a list of array elements, but the run-time representation is a dynamically-sized array.
23
36
At run time, the constructor translates the list into an array, and the field accessor allocates a linked list from the array.
24
37
The various array operations are replaced with efficient versions by the compiler that mutate the array when possible instead of allocating a new one.
Both types themselves and proofs of propositions are completely erased from compiled code.
27
44
In other words, they take up no space, and any computations that might have been performed as part of a proof are similarly erased.
28
45
This means that proofs can take advantage of the convenient interface to strings and arrays as inductively-defined lists, including using induction to prove things about them, without imposing slow conversion steps while the program is running.
29
46
For these built-in types, a convenient logical representation of the data does not imply that the program must be slow.
If a structure type has only a single non-type non-proof field, then the constructor itself disappears at run time, being replaced with its single argument.
32
53
In other words, a subtype is represented identically to its underlying type, rather than with an extra layer of indirection.
33
54
Similarly, `Fin` is just `Nat` in memory, and single-field structures can be created to keep track of different uses of `Nat`s or `String`s without paying a performance penalty.
34
55
If a constructor has no non-type non-proof arguments, then the constructor also disappears and is replaced with a constant value where the pointer would otherwise be used.
35
56
This means that `true`, `false`, and `none` are constant values, rather than pointers to heap-allocated objects.
The [definition of `Pos`](../type-classes/pos.html) does not take advantage of Lean's compilation of `Nat` to an efficient type.
54
99
At run time, it is essentially a linked list.
55
100
Alternatively, a subtype can be defined that allows Lean's fast `Nat` type to be used internally, as described [in the initial section on subtypes](../functor-applicative-monad/applicative.md#subtypes).
56
101
At run time, the proof will be erased.
57
102
Because the resulting structure has only a single data field, it is represented as that field, which means that this new representation of `Pos` is identical to that of `Nat`.
After proving the theorem `∀ {n k : Nat}, n ≠ 0 → k ≠ 0 → n + k ≠ 0`, define instances of `ToString`, and `Add` for this new representation of `Pos`. Then, define an instance of `Mul`, proving any necessary theorems along the way.
109
+
-->
110
+
111
+
定理 `∀ {n k : Nat}, n ≠ 0 → k ≠ 0 → n + k ≠ 0` を証明したのちに、この `Pos` の新しい表現への `ToString` と `Add` のインスタンスを定義してください。その次に、必要な定理を証明しながら `Mul` のインスタンスを定義してください。
0 commit comments