doc(doc/lean/tutorial): update tutorial
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
84f017f127
commit
d83a13d044
1 changed files with 176 additions and 33 deletions
|
|
@ -38,6 +38,12 @@ the input value, and then evaluates it on different values.
|
|||
eval double 3 > 4
|
||||
```
|
||||
|
||||
Basics
|
||||
------
|
||||
|
||||
We can also view Lean as a suite of tools for evaluating and processing
|
||||
expressions representing terms, definitions, and theorems.
|
||||
|
||||
Every expression has a unique type in Lean. The command `check` returns the
|
||||
type of a given expression.
|
||||
|
||||
|
|
@ -62,7 +68,7 @@ using regular expressions
|
|||
|
||||
We say `Nat::ge` is a hierarchical name comprised of two parts: `Nat` and `ge`
|
||||
|
||||
The command `using` creates aliases based on give prefix. For example, the following
|
||||
The command `using` creates aliases based on a given prefix. For example, the following
|
||||
command creates aliases for all objects starting with `Nat`
|
||||
|
||||
```lean
|
||||
|
|
@ -70,43 +76,180 @@ command creates aliases for all objects starting with `Nat`
|
|||
check ge -- display the signature of the Nat::ge definition
|
||||
```
|
||||
|
||||
In Lean, proofs are also expressions, and theorems are essentially definitions.
|
||||
In the following example we prove that `double x = 2 * x`
|
||||
The command `variable` assigns a type to an identifier. The following command postulates/assumes
|
||||
that `n`, `m` and `o` have type `Nat`.
|
||||
|
||||
```lean
|
||||
theorem double_x_eq_2x (x : Nat) : double x = 2 * x :=
|
||||
calc double x = x + x : refl (double x)
|
||||
... = 1*x + 1*x : { symm (mul_onel x) }
|
||||
... = (1 + 1)*x : symm (distributel 1 1 x)
|
||||
... = 2 * x : { refl (1 + 1) }
|
||||
variable n : Nat
|
||||
variable m : Nat
|
||||
variable o : Nat
|
||||
```
|
||||
|
||||
In the example above, we provided the proof manually using a calculational proof style.
|
||||
The terms after `:` are proof terms. They justify the equalities in the left-hand-side.
|
||||
The proof term `refl (double x)` produces a proof for `t = s` where `t` and `s` have the same
|
||||
normal form of `(double x)`. The proof term `{ symm (mul_onel x) }` is a justification for
|
||||
the equality `x = 1*x`. The curly braces instruct Lean to replace `x` with `1*x`.
|
||||
Similarly `{ symm (distributel 1 1 x) }` is a proof for `1*x + 1*x = (1 + 1)*x`.
|
||||
The exact semantics of these expressions is not important at this point.
|
||||
The command `variables n m o : Nat` can be used a shorthand for the three commands above.
|
||||
|
||||
|
||||
|
||||
|
||||
Objects
|
||||
-------
|
||||
|
||||
In each Lean session, we create an enviroment, a sequence of named
|
||||
objects such as: definitions, axioms and theorems. Each object has
|
||||
a unique name. We use `hierarchical names` in Lean, i.e., a sequence
|
||||
of regular identifiers separated by `::`. Hierarchical names provide
|
||||
a cheap of simulating modules and namespaces in Lean.
|
||||
|
||||
Expressions
|
||||
-----------
|
||||
|
||||
Each expression has a unique type in Lean. The command `check` returns
|
||||
the type of an expression.
|
||||
In Lean, proofs are also expressions, and all functionality provided for manipulating
|
||||
expressions is also available for manipulating proofs. For example, `refl n` is a proof
|
||||
for `n == n`. In Lean, `refl` is the reflexivity axiom.
|
||||
|
||||
```lean
|
||||
check 1+2.
|
||||
check refl n
|
||||
```
|
||||
|
||||
The command `axiom` postulates that a given proposition (aka Boolean formula) is true.
|
||||
The following commands postulate two axioms `Ax1` and `Ax2` that state that `n = m` and
|
||||
`m = o`.
|
||||
|
||||
```lean
|
||||
axiom Ax1 : n = m
|
||||
axiom Ax2 : m = o
|
||||
```
|
||||
|
||||
`Ax1` and `Ax2` are not just names. For example, `trans Ax1 Ax2` is a proof that
|
||||
`n == o`, where `trans` is the transitivity axiom.
|
||||
|
||||
```lean
|
||||
check trans Ax1 Ax2
|
||||
```
|
||||
|
||||
The expression `trans Ax1 Ax2` is just a function application like any other.
|
||||
Moreover, in Lean, _propositions are types_. Any Boolean expression `P` can be used
|
||||
as a type. The elements of type `P` can be viewed as the proofs of `P`.
|
||||
Moreover, in Lean, _proof checking is type checking_. For example, the Lean type checker
|
||||
will reject the type incorrect term `trans Ax2 Ax1`.
|
||||
|
||||
Because we use _proposition as types_, we must support _empty types_. For example,
|
||||
the type `false` must be empty, since we don't have a proof for `false`.
|
||||
|
||||
Most systems based on _propositions as types_ paradigm are based on constructive logic.
|
||||
Lean on the other hand is based on classical logic. The _excluded middle_ is a theorem
|
||||
in Lean, and `em p` is a proof for `p ∨ ¬ p`.
|
||||
|
||||
```lean
|
||||
variable p : Bool
|
||||
check em p
|
||||
```
|
||||
|
||||
The commands `axiom` and `variable` are essentially the same command. We provide both
|
||||
just to make Lean files more readable. We encourage users to use `axiom` only for
|
||||
propostions, and `variable` for everything else.
|
||||
|
||||
Similarly, a theorem is just a definition. The following command defines a new theorem
|
||||
called `nat_trans3`
|
||||
|
||||
```lean
|
||||
theorem nat_trans3 (a b c d : Nat) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d
|
||||
:= trans (trans H1 (symm H2)) H3
|
||||
```
|
||||
|
||||
The theorem `nat_trans3` has 7 parameters, it takes for natural numbers `a`, `b`, `c` and `d,
|
||||
and three proofs showing that `a = b`, `c = b` and `c = d`, and returns a proof that `a = d`.
|
||||
In the example above, `symm` is the symmetry theorem. Now, we use `nat_trans3` in a simple
|
||||
example.
|
||||
|
||||
```lean
|
||||
variables x y z w : Nat
|
||||
axiom Hxy : x = y
|
||||
axiom Hzy : z = y
|
||||
axiom Hzw : z = w
|
||||
check nat_trans3 x y z w Hxy Hzy Hzw
|
||||
```
|
||||
|
||||
The theorem `nat_trans3` is somewhat inconvenient to use because it has 7 parameters.
|
||||
However, the first four parameters can be inferred from the last 3. We can `_` as placeholder
|
||||
that instructs Lean to synthesize this expression.
|
||||
|
||||
```lean
|
||||
check nat_trans3 _ _ _ _ Hxy Hzy Hzw
|
||||
```
|
||||
|
||||
Lean also supports _implicit arguments_.
|
||||
We mark implicit arguments using curly braces instead of parenthesis.
|
||||
In the following example, we define the theorem `nat_trans3i` using implicit arguments.
|
||||
|
||||
```lean
|
||||
theorem nat_trans3i {a b c d : Nat} (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d
|
||||
:= trans (trans H1 (symm H2)) H3
|
||||
```
|
||||
|
||||
It is identical to `nat_trans3`, the only difference is the use of curly braces.
|
||||
Lean will (try to) infer the implicit arguments. The idea behind implicit arguments
|
||||
is quite simple, we are just instructing Lean to automatically insert the placeholders
|
||||
`_` for us.
|
||||
|
||||
```lean
|
||||
check nat_trans3i Hxy Hzy Hzw
|
||||
```
|
||||
|
||||
Sometimes, Lean will not be able to infer the parameters automatically. So, whenever we
|
||||
define a theorem/definition/axiom/variable containing implicit arguments, Lean will
|
||||
automatically create an _explicit_ version where all parameters are explicit.
|
||||
The explicit version uses the same name with a `@` prefix.
|
||||
|
||||
```lean
|
||||
check @nat_trans3i
|
||||
```
|
||||
|
||||
The axiom `refl`, and the theorems `trans` and `symm` all have implicit arguments.
|
||||
|
||||
```lean
|
||||
check @refl
|
||||
check @trans
|
||||
check @symm
|
||||
```
|
||||
|
||||
We can also instruct Lean to display all implicit arguments. This is useful
|
||||
when debugging non-trivial problems.
|
||||
|
||||
```lean
|
||||
set_option pp::implicit true -- show implicit arguments
|
||||
check nat_trans3i Hxy Hzy Hzw
|
||||
set_option pp::implicit false -- hide implicit arguments
|
||||
```
|
||||
|
||||
Note that, in the examples above, we have seen two symbols for equality: `=` and `==`.
|
||||
Moreover, in the previous example, the `check` command stated that `nat_trans3i Hxy Hzy Hzw`
|
||||
has type `@eq ℕ x w`. For technical reasons, in Lean, we have heterogenous and homogeneous
|
||||
equality. In a nutshell, heterogenous is mainly used internally, and homogeneous are used externally
|
||||
when writing programs and specifications in Lean. Heterogenous equality allows us to compare
|
||||
elements of any type, and homogenous equality is just a definition on top of the heterogenous
|
||||
equality that expects arguments of the same type. The expression `t == s` is a heterogenous equality that is true
|
||||
iff `t` and `s` have the same interpretation. On the other hand `t = s` is a homogeneous equality,
|
||||
and is only type correct if `t` and `s` have the same type. The symbol `=` is actually notation for
|
||||
`eq t s`, where `eq` is defined (using heterogenous equality) as:
|
||||
|
||||
```
|
||||
definition eq {A : TypeU} (a b : A) : Bool
|
||||
:= a == b
|
||||
```
|
||||
|
||||
We strongly discourage users from directly using heterogeneous equality. The main problem is that it is very easy to
|
||||
write nonsensical expressions such as `2 == true`. On the other hand, the expression `2 = true` is type incorrect,
|
||||
and Lean will report the mistake to the user.
|
||||
|
||||
We have seen many occurrences of `TypeU`. It is just a definition: `(Type U)`, where `U` is a _universe variable_.
|
||||
In Lean, the type of `Nat` and `Bool` is `Type`.
|
||||
|
||||
```lean
|
||||
check Nat
|
||||
check Bool
|
||||
```
|
||||
|
||||
We say `Type` is the type of all _small_ types, but what is the type of `Type`?
|
||||
|
||||
```lean
|
||||
check Type
|
||||
```
|
||||
|
||||
Lean returns `(Type 1)`. Similarly, the type of `(Type 1)` is `(Type 2)`. In Lean, we also have _universe cumulativity_.
|
||||
That is, we can provide an element of type `(Type i)` where an element of type `(Type j)` is expected when `i ≤ j`.
|
||||
This makes the system more convenient to use. Otherwise, we would need a reflexivity axiom for `Type` (i.e., `(Type 0)`),
|
||||
`Type 1`, `Type 2`, etc. Universe cumulativity improves usability, but it is not enough because
|
||||
We would still have the question: how big should `i` be? Moreover, if we choose an `i` that is not big enough
|
||||
we have to go back and correct all libraries. This is not satisfactory and not modular.
|
||||
So, in Lean, we allow user to declare _universe variables_ and simple constraints between them. The Lean kernel defines
|
||||
one universe variable `U`, and states that `U ≥ 1` using the command `universe U ≥ 1`.
|
||||
The Lean type casting library defines another universe variable called `M` and states that `universe M ≥ 1` and `universe M ≥ U + 1`.
|
||||
Lean reports an universe inconsistency if the universe constraints are inconsistency. For example, it will return an error
|
||||
if execute the command `universe M ≥ U`. We can view universe variables as placeholders, and we can always solve
|
||||
the universe constraints and find and assignment for the universe variables used in our developments.
|
||||
This assignment allows us to produce a Lean specification that is not based on this particular feature.
|
||||
|
|
|
|||
Loading…
Reference in a new issue