diff --git a/doc/lean/tutorial.md b/doc/lean/tutorial.md index c59371c183..367e3cabb8 100644 --- a/doc/lean/tutorial.md +++ b/doc/lean/tutorial.md @@ -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.