From ec27a7090890d2db98106ca87b90be7ee8341a8b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Mar 2014 10:57:07 -0700 Subject: [PATCH] doc(*): update documentation and add link to Lean 0.1 Signed-off-by: Leonardo de Moura --- README.md | 2 ++ doc/design.md | 69 ++++++++++++++++++++++++-------------------- doc/lean/tutorial.md | 3 ++ 3 files changed, 43 insertions(+), 31 deletions(-) diff --git a/README.md b/README.md index 6159653d0..34d2a717e 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,8 @@ +**Remark: Lean 0.2 is under development. To try Lean, please use [version 0.1](https://github.com/leodemoura/lean0.1).** + About ----- diff --git a/doc/design.md b/doc/design.md index e4f1ba45f..96191fcde 100644 --- a/doc/design.md +++ b/doc/design.md @@ -1,67 +1,72 @@ Design ------ -In Lean, the main activity consists in building Environments containing: definitions, theorems, axioms and variable definitions. We *cannot* make a consistent environment *Env* inconsistent by adding definitions and/or theorems. This is guaranteed by the Lean Kernel. +In Lean, the main activity consists in building Environments containing: definitions, theorems, axioms and variable definitions. +We *cannot* make a consistent environment *Env* inconsistent by adding definitions and/or theorems. This is guaranteed by the Lean Kernel. On the other hand, a user can make the environment inconsistent by adding axioms and variable definitions. -Regarding variable definitions, the inconsistency can be introduced when a user declares that an empty type is inhabited. Actually, variable definitions and axioms have the same status from the Lean Kernel point of view. There is no real difference. An command `axiom H : a > 0` is conceptually identical to `variable H : a > 0`. Similarly, a Theorem is just a definition. -The Kernel does not provide any form of automation. It is just doing "bookkeeping" and type checking. In Lean, _proof checking is type checking_. +Regarding variable definitions, the inconsistency can be introduced when a user declares that an empty type is inhabited. +Actually, variable definitions and axioms have the same status from the Lean Kernel point of view. +There is no real difference. An command `axiom H : a > 0` is conceptually identical to `variable H : a > 0`. +Similarly, a Theorem is just a definition. +The Kernel does not provide any form of automation. It is just doing "bookkeeping" and type checking. +In Lean, _proof checking is type checking_. -Building objects such as definitions and theorems without any form of automation is quite laborious. So, one of the main goals of the Lean project is to provide a lot of building blocks to automate the process of creating new definitions and theorems. +Building objects such as definitions and theorems without any form of automation is quite laborious. +So, one of the main goals of the Lean project is to provide a lot of building blocks to automate the process of creating +new definitions and theorems. -In Lean, we allow users to provide partially specified objects such as definitions and theorems. A partially specified object is an object with **holes**. Holes mark the parts that must be automatically constructed by Lean. In a nutshell, Lean can be viewed as a system for synthesizing proofs, terms, types, etc. Here is a simple example: +In Lean, we allow users to provide partially specified objects such as definitions and theorems. +A partially specified object is an object with **holes**. Holes mark the parts that must be automatically constructed by Lean. +In a nutshell, Lean can be viewed as a system for synthesizing proofs, terms, types, etc. Here is a simple example: - variable a : Nat + variable a : nat axiom a > 0 theorem T : a >= 1 := _ We use `_` to denote holes. In the simple example above, the "whole proof" must be automatically computed by Lean. Here is another simple example: variable f : forall (A : Type), A -> A -> A - definition f00 : Nat := f _ 0 0 + definition f00 : nat := f _ 0 0 -In this example, Lean will automatically fill the hole with `Nat` (the type of the natural numbers). +In this example, Lean will automatically fill the hole with `nat` (the type of the natural numbers). Here is another example with multiple holes. variable g : forall (A : Type), A -> A - variable a : Nat - variable b : Nat + variable a : nat + variable b : nat axiom H1 : a = b axiom H2 : (g _ a) > 0 theorem T1 : (g _ b) > 0 := _ -Lean supports multiple frontends. The default frontend provides several features that automatically create holes for users. For example, we can write: +Lean supports multiple frontends. The default frontend provides several features that automatically create holes for users. +For example, we can write: variable g {A : Type} (a : A) : A `g` is a function with two arguments. The curly braces are used to mark _implicit arguments_. Then, whenever we write `g a`, the system automatically creates `g _ a`. -The _Lean elaborator_ is the module responsible for filling the holes. Actually, it only manages the collection of tools and components that do all the hard work. +The _Lean elaborator_ is the module responsible for filling the holes. +Actually, it only manages the collection of tools and components that do all the hard work. When we provide an object with holes to the elaborator, one of the following outputs is possible 1) The elaborator succeeds and fill all the holes, and the Lean Kernel accepts the elaborated object without holes. -2) The elaborator succeeds and fill all the holes, but the Lean Kernel rejects the elaborated object. The elaborator uses many different components. Some of these components may have bugs. The Lean Kernel is the last firewall that will prevent an ill-formed object from being included in the environment. +2) The elaborator succeeds and fill all the holes, but the Lean Kernel rejects the elaborated object. +The elaborator uses many different components. Some of these components may have bugs. +The Lean Kernel is the last firewall that will prevent an ill-formed object from being included in the environment. -3) The elaborator fails to fill the holes, and produces a new environment that demonstrates that it is impossible to fill the holes. We can view the new environment as a counter-example. Moreover, the new environment provides definitions and theorems for all user defined variables and axioms. Here is an example: +3) The elaborator fails to fill the holes, and produces a new environment that demonstrates that it is impossible to fill the holes. +We can view the new environment as a counter-example. Moreover, the new environment provides definitions and theorems for all user +defined variables and axioms. - variable a : Nat - axiom H : a > 0 - theorem T : a >= 2 := _ - -In this example, the Lean elaborator will provide a new environment containing - - definition a : Nat := 1 - theorem H : a > 0 := trivial - theorem T : not a >= 2 := trivial - -The `trivial` denotes a proof by evaluation. That is, if we replace `a` with `1` in `a > 0` and evaluate we prove the theorem `a > 0`. The new environment does not contain any variables or axioms. Thus, it is trivially consistent. It also contains a proof for the negation of `a >= 2` (the theorem we were trying to prove). - -4) Finally, the elaborator may fail because of its own limitations. In this case, it produces a trace explaining why a particular hole could not be filled. It might still be possible to fill the whole, but the elaborator does not know how to do it. Note that, the trace may contain an environment that provides definitions for some of the variables and axioms in the user environment. This partial environment may help the user to understand why a particular hole could not be filled. +4) Finally, the elaborator may fail because of its own limitations. In this case, it produces error messages and/or unsolved goals. +It might still be possible to fill the hole, but the elaborator does not know how to do it. Users may react by filling some of the holes themselves, or realizing that it is indeed impossible to fill the holes. -In Lean, we provide a frontend for the SMT 2.0 standard. It is very straightforward to map the SMT constructs into the framework above. For example, the SMT commands +In Lean, we will provide a frontend for the SMT 2.0 standard. It is very straightforward to map the SMT constructs into the framework above. +For example, the SMT commands (declare-fun a () Int) (declare-fun b () Int) @@ -71,10 +76,12 @@ In Lean, we provide a frontend for the SMT 2.0 standard. It is very straightforw are mapped to - variable a : Int - variable b : Int + variable a : int + variable b : int axiom H1 : a > 0 axiom H2 : b < a theorem Unsat : false := _ -If Lean can prove `false`, then it produces a proof that demonstrates that the set of SMT assertions is unsatisfiable. If the set of assertions is satisfiable, then it produces a new environment that provides definitions for `a` and `b` and theorems for each assertion. Of course, as we discussed above, Lean may also fail and return a trace describing why it failed. +If Lean can prove `false`, then it produces a proof that demonstrates that the set of SMT assertions is unsatisfiable. +If the set of assertions is satisfiable, then it produces a new environment that provides definitions for `a` and `b` +and theorems for each assertion. Of course, as we discussed above, Lean may also fail and return error messages describing why it failed. diff --git a/doc/lean/tutorial.md b/doc/lean/tutorial.md index 9f1235700..80470776b 100644 --- a/doc/lean/tutorial.md +++ b/doc/lean/tutorial.md @@ -1,6 +1,9 @@ Lean Tutorial ============= +**WARNING: This tutoral is for Lean 0.1, before major modifications performed in version 0.2. +Version 0.2 is still under development. [Here you can find a snapshot of Lean 0.1](https://github.com/leodemoura/lean0.1).** + Introduction ------------