From 1509a1ab187dadc1bce6e578a95886cb9fd44933 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Dec 2020 09:02:29 -0800 Subject: [PATCH] doc: builtin types --- doc/SUMMARY.md | 13 ++++++- doc/array.md | 1 + doc/builtintypes.md | 25 ++++++++++++++ doc/char.md | 1 + doc/float.md | 1 + doc/int.md | 37 ++++++++++++++++++++ doc/list.md | 1 + doc/nat.md | 68 +++++++++++++++++++++++++++++++++++++ doc/option.md | 1 + doc/string.md | 1 + doc/task.md | 1 + doc/{thunks.md => thunk.md} | 8 ----- doc/uint.md | 1 + 13 files changed, 150 insertions(+), 9 deletions(-) create mode 100644 doc/array.md create mode 100644 doc/builtintypes.md create mode 100644 doc/char.md create mode 100644 doc/float.md create mode 100644 doc/int.md create mode 100644 doc/list.md create mode 100644 doc/nat.md create mode 100644 doc/option.md create mode 100644 doc/string.md create mode 100644 doc/task.md rename doc/{thunks.md => thunk.md} (98%) create mode 100644 doc/uint.md diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index a2f539e3ce..a7e630bcb9 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -17,10 +17,21 @@ - [Implicit Arguments](./implicit.md) - [Auto Bound Implicit Arguments](./autobound.md) - [Functions](./functions.md) +- [Builtin Types](./builtintypes.md) + - [Natural number](./nat.md) + - [Integer](./int.md) + - [Fixed precision unsigned integer](./uint.md) + - [Float](./float.md) + - [Array](./array.md) + - [List](./list.md) + - [Character](./char.md) + - [String](./string.md) + - [Option](./option.md) + - [Thunk](./thunk.md) + - [Task and Thread](./task.md) - [Type classes](./typeclass.md) - [The `do` Notation](./do.md) - [Tactics](./tactics.md) -- [Thunks, Tasks and Threads](./thunks.md) - [String interpolation](./stringinterp.md) # Other diff --git a/doc/array.md b/doc/array.md new file mode 100644 index 0000000000..662470c483 --- /dev/null +++ b/doc/array.md @@ -0,0 +1 @@ +# Array diff --git a/doc/builtintypes.md b/doc/builtintypes.md new file mode 100644 index 0000000000..11cf1b1b09 --- /dev/null +++ b/doc/builtintypes.md @@ -0,0 +1,25 @@ +# Builtin Types + +## Numeric Operations + +Lean supports the basic mathematical operations you’d expect for all of the number types: addition, subtraction, multiplication, division, and remainder. +The following code shows how you’d use each one in a `def` commands: + +```lean +-- addition +def sum := 5 + 10 + +-- subtraction +def difference := 95.5 - 4.3 + +-- multiplication +def product := 4 * 30 + +-- division +def quotient := 53.7 / 32.2 + +-- remainder/modulo +def modulo := 43 % 5 +``` + +Each expression in these statements uses a mathematical operator and evaluates to a single value. diff --git a/doc/char.md b/doc/char.md new file mode 100644 index 0000000000..d012232d9d --- /dev/null +++ b/doc/char.md @@ -0,0 +1 @@ +# Characters diff --git a/doc/float.md b/doc/float.md new file mode 100644 index 0000000000..f32689c30c --- /dev/null +++ b/doc/float.md @@ -0,0 +1 @@ +# Float diff --git a/doc/int.md b/doc/int.md new file mode 100644 index 0000000000..b747644489 --- /dev/null +++ b/doc/int.md @@ -0,0 +1,37 @@ +# Integers + +The `Int` type represents the arbitrary-precision integers. There are no overflows. +```lean +#eval (100000000000000000 : Int) * 200000000000000000000 * 1000000000000000000000 +``` +Recall that nonnegative numerals are considered to be a `Nat` if there are no typing constraints. +```lean +#check 1 -- Nat +#check -1 -- Int +#check (1:Int) -- Int +``` + +The operator `/` for `Int` implements integer division. +```lean +#eval -10 / 4 -- -2 +``` + +Similar to the `Nat, the internal representation of `Int` is optimized. Small integers are +represented by a single machine word. Big integers are implemented using [GMP](https://gmplib.org/manual/) numbers. +We recommend you use fixed precision numeric types only in performance critical code. + +The Lean kernel has not special support for reducing `Int` during type checking. +However, since `Int` is defined as +```lean +# namespace hidden +inductive Int : Type where + | ofNat : Nat → Int + | negSucc : Nat → Int +# end hidden +``` +the type checker will be able reduce `Int` expressions efficiently by relying on the special support for `Nat`. + +```lean +theorem ex : -2000000000 * 1000000000 = -2000000000000000000 := + rfl +``` diff --git a/doc/list.md b/doc/list.md new file mode 100644 index 0000000000..6811f7b83e --- /dev/null +++ b/doc/list.md @@ -0,0 +1 @@ +# List diff --git a/doc/nat.md b/doc/nat.md new file mode 100644 index 0000000000..c41c53347c --- /dev/null +++ b/doc/nat.md @@ -0,0 +1,68 @@ +# Natural numbers + +The `Nat` type represents the natural numbers, i.e., arbitrary-precision unsigned integers. +There are no overflows. + +```lean +#eval 100000000000000000 * 200000000000000000000 * 1000000000000000000000 +``` + +A numeral is considered to be a `Nat` if there are no typing constraints. +```lean +#check 10 -- Nat +#check id 10 -- Nat + +def f (x : Int) : Int := + x - 1 + +#eval f (3 - 5) -- 3 and 5 are `Int` since `f` expects an `Int`. +-- -3 +``` + +The operator `-` for `Nat` implements truncated subtraction. +```lean +#eval 10 - 5 -- 5 +#eval 5 - 10 -- 0 + +theorem ex : 5 - 10 = 0 := + rfl + +#eval (5:Int) - 10 -- -5 +``` + +The operator `/` for `Nat` implements Euclidean division. +```lean +#eval 10 / 4 -- 2 + +#check 10.0 / 4.0 -- Float +#eval 10.0 / 4.0 -- 2.5 +``` + +As we described in the previous sections, we define the `Nat` type as an `inductive` datatype. +```lean +# namespace hidden +inductive Nat where + | zero : Nat + | succ : Nat → Nat +# end hidden +``` +However, the internal representation of `Nat` is optimized. Small natural numbers (i.e., < `2^63` in a 64-bit machine) are +represented by a single machine word. Big numbers are implemented using [GMP](https://gmplib.org/manual/) numbers. +We recommend you use fixed precision numeric types only in performance critical code. + +The Lean kernel has builtin support for the `Nat` type too, and can efficiently reduce `Nat` expressions during type checking. +```lean +#reduce 100000000000000000 * 200000000000000000000 * 1000000000000000000000 + +theorem ex + : 1000000000000000 * 2000000000000000000 = 2000000000000000000000000000000000 := + rfl +``` +The sharp-eyed reader will notice that GMP is part of the Lean kernel trusted code base. +We believe this is not a problem because you can use external type checkers to double-check your developments, +and we consider GMP very thrustworthy. +Existing external type checkers for Lean 3 (e.g., [Trepplein](https://github.com/gebner/trepplein) and [TC](https://github.com/leanprover/tc)) +can be easily adapted to Lean 4. +If you are still concerned after checking your development with multiple different external checkers because +they may all rely on buggy arbitrary-precision libraries, +you can develop your own certified arbitrary-precision library and use it to implement your own type checker for Lean. diff --git a/doc/option.md b/doc/option.md new file mode 100644 index 0000000000..f33af4ff3f --- /dev/null +++ b/doc/option.md @@ -0,0 +1 @@ +# Option diff --git a/doc/string.md b/doc/string.md new file mode 100644 index 0000000000..ed218ce9a0 --- /dev/null +++ b/doc/string.md @@ -0,0 +1 @@ +# Strings diff --git a/doc/task.md b/doc/task.md new file mode 100644 index 0000000000..83a3f5dd2b --- /dev/null +++ b/doc/task.md @@ -0,0 +1 @@ +# Task diff --git a/doc/thunks.md b/doc/thunk.md similarity index 98% rename from doc/thunks.md rename to doc/thunk.md index 47d8b7d114..0dae01229f 100644 --- a/doc/thunks.md +++ b/doc/thunk.md @@ -102,11 +102,3 @@ and `add1` is still considered to be a pure function. The Lean compiler performs common subexpression elimination when compiling `double`, and the produced code for `double` executes `x ()` only once instead of twice. This transformation is safe because `x : Unit -> Nat` is pure. - -## Tasks - -TODO - -## Threads - -TODO \ No newline at end of file diff --git a/doc/uint.md b/doc/uint.md new file mode 100644 index 0000000000..0c9394edeb --- /dev/null +++ b/doc/uint.md @@ -0,0 +1 @@ +# Fixed precision unsigned integers